Prove2Me

Expected combined benefits add

Proved
actuarial_c_epv_add

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

actuarial-scienceinsurancelife-contingency

Expected combined benefits add.

Mathematical relation:

E[Zb+c]=E[Zb]+E[Zc]\mathbb{E}[Z_{b+c}]=\mathbb{E}[Z_b]+\mathbb{E}[Z_c]

For this statement, the yearly death event, valuation origin and life-law normalisation follow the stated hypotheses. Death benefits are settled at the end of the policy year, whereas a maturity amount is payable at its anniversary. Every formula represents a currently open formal obligation unless it is a definition.

Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Definitions.Def_actuarial_c_death
import Definitions.Def_actuarial_c_path
import Definitions.Def_actuarial_c_epv

open ActuarialAssurances
Formal statement
theorem actuarial_c_epv_add (h : ℕ) (v : ℝ) (b c p : ℕ → ℝ) : epv h v (fun j => b j+c j) p=epv h v b p+epv h v c p := by sorry
Source
Original derived finite life-contingency specification; S. David Promislow (2015), Fundamentals of Actuarial Mathematics, 3rd edition, Chapter 5, Section 5.2, year-end death claim present value, printed p. 62. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml. The cited material establishes actuarial context and payment conventions. This particular finite Lean declaration is not a verbatim published theorem.
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 13, 2026

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

View graph