Prove2Me

Finite-scenario investment returns and fixed random rates: siFixedMean_one

Proved
ActuarialValuation.siFixedMean_one

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

actuarial-scienceformal-verificationstochastic-investment-accumulation

A fixed uncertain return for one year has the same law as a variable return. This original derived actuarial relation uses the parameter restrictions, endpoints and units stated in the separate formal theorem or definition.

Mathematical relation:

Sn=(1+I)n,E[Sn]=∑ωpω(1+Iω)nS_n=(1+I)^n,\quad \mathbb{E}[S_n]=\sum_{\omega}p_{\omega}(1+I_{\omega})^n
Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fintype.Basic
import Definitions.Def_actuarial_siFixedMean
import Definitions.Def_actuarial_siGrossMean
Formal statement
namespace ActuarialValuation

theorem siFixedMean_one {m : ℕ} (p : Fin m → ℝ) (r : Fin m → ℝ) : siFixedMean p r 1=siGrossMean p r := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 13. S. David Promislow, Fundamentals of Actuarial Mathematics (2015), Chapters on stochastic rates and annuity accumulation; Shreve (2004), Stochastic Calculus for Finance I, Chapter 1, https://link.springer.com/book/10.1007/978-0-387-22527-2. Parent topic: Finite-scenario expectation and variance; fixed random rate versus independent annual rates, product sample space and fund contribution moments. The particular Lean formula is a new finite/real-algebraic formalisation and remains an unproved theorem target if labelled theorem. Relevant published actuarial derivation: https://link.springer.com/book/10.1007/978-0-387-22527-2
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