An empty annual gain series totals zero
ProvedActuarialValuation.discountedAnnualGainSum_zero_termactuarial-sciencehattendorffpolicy-reserves
No years means no discounted cashflow contributions.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_discountedAnnualGainSum open MeasureTheory
Formal statement
namespace ActuarialValuation
theorem discountedAnnualGainSum_zero_term {Ω : Type*} (G : ℕ → Ω → ℝ) (v : ℝ) (ω : Ω)
:
discountedAnnualGainSum G v 0 ω = 0 := by sorry
end ActuarialValuationSource
Gerber (1997), Life Insurance Mathematics, third edition, §6.7 equations (6.7.3), (6.7.6)-(6.7.10); Bladt et al., An elementary derivation of Hattendorff's theorem (2021), https://doi.org/10.1007/s13385-020-00256-9; R. Norberg (1992), Hattendorff's theorem and Thiele's differential equation generalized, https://doi.org/10.1080/03461238.1992.10413894
Read-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. When n is set to zero the index range for year contributions is empty and the discounted gain total is zero for every outcome. This is a numerical identity independent of the discount factor and the pattern of gain amounts in later years.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.