Prove2Me

Finite aggregate loss reserve and stop-loss valuation: panjerAggregateCDF_zero

Proved
ActuarialValuation.panjerAggregateCDF_zero

by WillR · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

actuarial-sciencecompound-claims-panjerformal-verification

First aggregate cumulative probability equals the zero-loss atom. 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:

G0=g0G_0=g_0
Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Definitions.Def_actuarial_panjerAggregateCDF
Formal statement
namespace ActuarialValuation

theorem panjerAggregateCDF_zero (g : ℕ → ℝ) : panjerAggregateCDF g 0 = g 0 := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 22. Harry H. Panjer, Recursive Evaluation of a Family of Compound Distributions, ASTIN Bulletin 12 (1981), pp. 22-26, https://www.casact.org/sites/default/files/database/astin_vol12no1_22.pdf; Sundt and Jewell, Further Results on Recursive Evaluation of Compound Distributions, ASTIN Bulletin 12 (1981), https://www.casact.org/sites/default/files/database/astin_vol12no1_27.pdf. Parent topic: Finite lattice claim severities, compound Poisson aggregate claim coefficients and Panjer recurrence with strictly positive claim sizes. 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_vol12no1_22.pdf
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 11, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph