Development factors and volume-weighted exposure: mackDenominator_zero
ProvedActuarialValuation.mackDenominator_zeroactuarial-scienceformal-verificationmack-reserve-variability
Empty triangle has no selected link-factor exposure. 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_mackDenominator
Formal statement
namespace ActuarialValuation theorem mackDenominator_zero (c : ℕ → ℕ → ℝ) (j : ℕ) : mackDenominator c 0 j = 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.