Prove2Me

Exponential Gompertz Makeham hazards and insurance valuation: svSurvival_from_hazard_positive

Proved
ActuarialValuation.svSurvival_from_hazard_positive

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

actuarial-scienceformal-verificationstochastic-survival-hazard

Finite real cumulative hazard always generates strictly positive exponential survival.

Mathematical relation:

svSurvival_from_hazard_positivesvSurvival\_from\_hazard\_positive

Original derived theorem target; the Lean statement gives the exact conditions and result.

Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Definitions.Def_actuarial_svSurvivalFromCumulativeHazard
Formal statement
namespace ActuarialValuation

theorem svSurvival_from_hazard_positive (h : ℝ) : 0 < svSurvivalFromCumulativeHazard h := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics inspired by Promislow (2015), chapters 14, 8 and Appendix A, published book reference https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/; supporting published actuarial reference https://www.actuaries.org.uk/system/files/field/document/Technical%20Workshop%20October%202019%20Slide%20Deck.pdf. Published source page 211 of Promislow's 2015 edition provides the thematic mathematical context. The target Lean identity is an original derivation, not a verbatim published result.
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