Prove2Me

Increasing annuity cashflow comm

Proved
ActuarialFoundations.fa_increasing_annuity_cashflow_comm

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

actuarial-scienceformal-verificationlife-table-commutation

Prove equality of independently defined original cashflows and the corresponding commutation expression for the stated exact Lean assumptions, directly from the life-table and cashflow definitions. Survivor benefits are valued on beginning-year anniversaries, with zero-lives boundary treatment. No commutation equivalence or desired result may be inserted as a hypothesis.

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_faS
import Definitions.Def_actuarial_faIncreasingAnnuityOriginal
Formal statement
namespace ActuarialFoundations

theorem fa_increasing_annuity_cashflow_comm (l : ℕ → ℝ) (v : ℝ) (ω x : ℕ) (hx : l x ≠ 0) (hv : v ≠ 0) : faIncreasingAnnuityOriginal l v ω x = faS l v ω x / faDiscountedLives l v x := by sorry

end ActuarialFoundations
Source
Institute of Actuaries (1971), International Actuarial Notation, commutation functions, p.50, https://www.actuaries.org.uk/system/files/documents/pdf/0042-0071.pdf. Original derived theorem; not a verbatim textbook theorem.
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