Prove2Me

Cohort probability extensions: survival antitone finite

Proved
ActuarialFoundations.fa_survival_antitone_finite

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

actuarial-scienceformal-verificationlife-table-commutation

Finite-horizon survival lies between zero and one and cannot increase as duration advances. The claim is restricted to ages within the finite cohort boundary.

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_antitone_finite (l : ℕ → ℝ) (ω x t u : ℕ) (h : faFiniteCohortValid l ω) (hp : 0 < l x) (ht : x+t+u ≤ ω) : 0 ≤ faSurvival l x (t+u) ∧ faSurvival l x (t+u) ≤ faSurvival l x t ∧ faSurvival l x t ≤ 1 := by sorry

end ActuarialFoundations
Source
S. David Promislow (2015), Fundamentals of Actuarial Mathematics, 3rd ed., Chapter 3 (life-table survival and mortality); Wiley https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521 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