Prove2Me

Survival bounds

Proved
ActuarialFoundations.fa_survival_bounds

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

actuarial-scienceformal-verificationlife-table-commutation

Prove unit-interval conditional survival bounds 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_faFiniteCohortValid
import Definitions.Def_actuarial_faSurvival
Formal statement
namespace ActuarialFoundations

theorem fa_survival_bounds (l : ℕ → ℝ) (ω x n : ℕ) (h : faFiniteCohortValid l ω) (hx : x < ω) (hp : 0 < l x) (hn : x+n ≤ ω) : 0 ≤ faSurvival l x n ∧ faSurvival l x n ≤ 1 := by sorry

end ActuarialFoundations
Source
S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapters 3 to 5, https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521. Original derived formulation.
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