Independent annual returns on actual product scenarios: siGrossMean_zero_rates
ProvedActuarialValuation.siGrossMean_zero_ratesactuarial-scienceformal-verificationstochastic-investment-accumulation
Unit expected accumulation results from zero annual rates. This original derived actuarial relation uses the parameter restrictions, endpoints and units stated in the separate formal theorem or definition.
Mathematical relation:
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Algebra.BigOperators.Group.Finset.Basic import Mathlib.Data.Fintype.Basic import Definitions.Def_actuarial_siGrossMean
Formal statement
namespace ActuarialValuation
theorem siGrossMean_zero_rates {m : ℕ} (p : Fin m → ℝ) (hp : (∑ j : Fin m, p j)=1) : siGrossMean p (fun _ => 0)=1 := by sorry
end ActuarialValuationSource
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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.