Prove2Me

Increasing finite-term benefits: increasing term assurance cashflow

Proved
ActuarialFoundations.fa_increasing_term_assurance_cashflow

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

actuarial-scienceformal-verificationlife-table-commutation

The independently specified increasing death claims, paid at year ends, equal the corrected finite R/M commutation expression divided by D_x.

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_faIncreasingTermAssuranceOriginal
import Definitions.Def_actuarial_faM
import Definitions.Def_actuarial_faR
Formal statement
namespace ActuarialFoundations

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

end ActuarialFoundations
Source
Institute of Actuaries (1969–1971), International Actuarial Notation, commutation functions and increasing assurance; https://www.actuaries.org.uk/system/files/documents/pdf/0042-0071.pdf 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