Prove2Me

Term and endowment assurances: endowment assurance cashflow

Proved
ActuarialFoundations.fa_endowment_assurance_cashflow

by WillR · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

actuarial-scienceformal-verificationlife-table-commutation

Combining term death benefits with an exact-maturity survival benefit gives (M_x−M_(x+n)+D_(x+n))/D_x. Both source benefits are separately defined.

Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Definitions.Def_actuarial_faDiscountedLives
import Definitions.Def_actuarial_faEndowmentAssuranceOriginal
import Definitions.Def_actuarial_faM
Formal statement
namespace ActuarialFoundations

theorem fa_endowment_assurance_cashflow (l : ℕ → ℝ) (v : ℝ) (ω x n : ℕ) (hp : 0 < l x) (hv : 0 < v) (hxn : x+n ≤ ω) : faEndowmentAssuranceOriginal l v x n = (faM l v ω x - faM l v ω (x+n) + faDiscountedLives l v (x+n)) / faDiscountedLives l v x := by sorry

end ActuarialFoundations
Source
David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2020), Actuarial Mathematics for Life Contingent Risks, 3rd ed., Chapters 4–5; Cambridge University Press https://doi.org/10.1017/9781108784184 Original-derived finite-cohort Lean statement; this exact theorem wording is not attributed to the text.
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 11, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph