Finite probability martingales and bounded stopping: ruMean_zero
ProvedActuarialValuation.ruMean_zeroactuarial-scienceformal-verificationmartingale-ruin-stopping
The expectation of an everywhere-zero random cashflow is zero.
Mathematical relation:
Original derived theorem target; the Lean statement gives the exact conditions and result.
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Data.Fintype.Basic import Mathlib.Algebra.BigOperators.Group.Finset.Basic import Mathlib.Analysis.SpecialFunctions.Exp import Definitions.Def_actuarial_ruMean
Formal statement
namespace ActuarialValuation
theorem ruMean_zero {m : ℕ} (p : Fin m → ℝ) : ruMean p (fun _ => 0) = 0 := by sorry
end ActuarialValuationSource
Original derived actuarial mathematics inspired by Promislow (2015), chapters 18 and 23, published book reference https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/; supporting published actuarial reference https://ocw.mit.edu/courses/18-440-probability-and-random-variables-spring-2014/resources/mit18_440s14_lecture35/. The proposed model is rooted in Promislow chapter 18 and 23. The target Lean identity is an original derivation, not a verbatim published result. Published source page 426 gives the thematic chapter context, rather than an exact statement of this new formal theorem.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.