Year-start survival splits into death and later survival
ProvedActuarialValuation.finiteLifeInForce_partitionactuarial-sciencehattendorffprospective-reserves
The in-force event at time t is the disjoint sum of death in year t and still being in force at t+1.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_finiteLifeDeathIndicator import Definitions.Def_actuarial_finiteLifeInForceIndicator open MeasureTheory
Formal statement
namespace ActuarialValuation theorem finiteLifeInForce_partition (K t : ℕ) : finiteLifeInForceIndicator K t = finiteLifeDeathIndicator K t + finiteLifeInForceIndicator K (t + 1) := by sorry end ActuarialValuation
Source
Shiu and Xiong (2021), An elementary derivation of Hattendorff's theorem, European Actuarial Journal 11 319-323, especially equations (1), (3)-(5), https://doi.org/10.1007/s13385-020-00256-9; Gerber (1997), Life Insurance Mathematics, third ed., Chapter 6 section 6.7, https://doi.org/10.1007/978-3-662-03460-6
Read-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. For any natural K and t, being in force at time t means either death occurs during year t or the policy remains in force at time t+1. These outcomes are disjoint and exhaustive, so the real indicator 1[t≤K] equals 1[K=t]+1[t+1≤K]. The theorem is a pointwise identity, not a mortality-probability formula.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.