Residual dispersion and one-step uncertainty: mackVarianceNumerator_zero
ProvedActuarialValuation.mackVarianceNumerator_zeroactuarial-scienceformal-verificationmack-reserve-variability
No observed cohorts produce no residual variance numerator. The full Lean declaration specifies the finite boundaries, exact units and any positivity, independence or regularity assumptions. This is an original derived Actuarial mathematical statement, not a claim of a numbered previously published theorem.
Mathematical relation:
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Algebra.BigOperators.Group.Finset.Basic import Definitions.Def_actuarial_mackVarianceNumerator
Formal statement
namespace ActuarialValuation theorem mackVarianceNumerator_zero (a b e : ℕ → ℝ) : mackVarianceNumerator a b e 0 = 0 := by sorry end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 213. Thomas Mack (1993), Distribution-free Calculation of the Standard Error of Chain Ladder Reserve Estimates, ASTIN Bulletin 23(2), pp. 213-225, https://www.casact.org/sites/default/files/database/astin_vol23no2_213.pdf; Thomas Mack (1999), The Standard Error of Chain Ladder Reserve Estimates: Recursive Calculation and Inclusion of a Tail Factor, https://www.casact.org/sites/default/files/database/astin_vol29no2_361.pdf. Parent topic: Mack claims reserving uncertainty, finite conditional development factor moments, process variance and estimation uncertainty. The particular Lean formula is a new finite/real-algebraic formalisation and remains an unproved theorem target if labelled theorem. Relevant published actuarial derivation: https://www.casact.org/sites/default/files/database/astin_vol23no2_213.pdf
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.