Zero cashflow has zero expected value
ProvedActuarialValuation.finiteScenarioExpectation_zeroactuarial-sciencehattendorffpolicy-reserves
Zero in every scenario implies zero weighted expectation.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_finiteScenarioExpectation open MeasureTheory
Formal statement
namespace ActuarialValuation
theorem finiteScenarioExpectation_zero {Ω : Type*} [Fintype Ω] (w : Ω → ℝ)
:
finiteScenarioExpectation w (fun _ => 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. If the scenario cashflow is zero at every outcome, then all weighted terms w(ω)·0 vanish. Therefore its finite weighted expectation is zero even without unit mass or nonnegative weight assumptions. The theorem is an elementary identity of the introduced expectation definition.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.