Independent annual returns on actual product scenarios: siGrossSecond_nonneg
ProvedActuarialValuation.siGrossSecond_nonnegactuarial-scienceformal-verificationstochastic-investment-accumulation
Second gross return moments are nonnegative. 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_siGrossSecond
Formal statement
namespace ActuarialValuation
theorem siGrossSecond_nonneg {m : ℕ} (p : Fin m → ℝ) (r : Fin m → ℝ) (hp : ∀ j, 0≤p j) : 0≤siGrossSecond p r := 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.