Finite count, severity and convolution transforms: cxPGF_one
ProvedActuarialValuation.cxPGF_oneactuarial-sciencecompound-risk-transformsformal-verification
The one-category generating function is the zero-size mass. 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_cxPGF
Formal statement
namespace ActuarialValuation theorem cxPGF_one (f : ℕ → ℝ) (z : ℝ) : cxPGF f 1 z = f 0 := by sorry end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 393. S. David Promislow, Fundamentals of Actuarial Mathematics, third edition (2015), Chapter 21, https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml; H. H. Panjer, Recursive Evaluation of a Family of Compound Distributions (1981), https://doi.org/10.1017/S0515036100006796. Parent topic: Compound aggregate risk: convolution and probability generating functions, zero claim severity mass, first two moments and (a,b,0) Panjer recurrence. 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.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.