Prove2Me

Due Arrears Boundary

Proved
ActuarialAnnuities.due_arrears_boundary

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

actuarial-scienceannuity-cashflowsingle-life-annuitiestiming

Finite due-minus-arrears difference includes the contingent terminal arrears payment.

Mathematical relation:

a¨h‾∣−ah‾∣=1−vhSh(h)\ddot a_{\overline{h}|}-a_{\overline{h}|}=1-v^{h}S_h(h)

Timing and admissibility conditions are the exact conditions of the declaration. Cash amounts are per instalment and present values are at valuation time zero.

Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Definitions.Def_actuarial_bTotal
import Definitions.Def_actuarial_bSurvival
import Definitions.Def_actuarial_bExpectedPV
import Definitions.Def_actuarial_bLevel
Formal statement
namespace ActuarialAnnuities

theorem due_arrears_boundary (h : ℕ) (v : ℝ) (p : ℕ → ℝ) (hp : bTotal h p = 1) : bExpectedPV h 0 h 0 0 v (bLevel 1) p-bExpectedPV h 0 h 0 1 v (bLevel 1) p = 1-v^h*bSurvival h p h := by sorry

end ActuarialAnnuities
Source
Original derived finite-cashflow result, contextual source page 148, Immediate life annuities (Chapter 5, section 5.4.3). D. C. M. Dickson, M. R. Hardy and H. R. Waters (2020), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press. https://www.cambridge.org/highereducation/books/actuarial-mathematics-for-life-contingent-risks/281DA4E8D523A6B23280ADC3D165AFDA/contents/4EB4E907782E2CD9CF0447D8F5DF1F6E. The cited page identifies the surrounding topic, not a numbered theorem with this exact Lean signature.
Human review

  • Endorsed by Shuze Chen · Oct 15, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 15, 2026

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

View graph