Prove2Me

Independent-shock Marshall–Olkin survivor law: csMarginalOne_start

Proved
ActuarialValuation.csMarginalOne_start

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

actuarial-sciencecompeting-risks-common-shockformal-verification

Each observed life has unit marginal survivor factor at duration zero.

Mathematical relation:

csMarginalOne_startcsMarginalOne\_start

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.Exp
import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Definitions.Def_actuarial_csMarginalOneExp
Formal statement
namespace ActuarialValuation

theorem csMarginalOne_start (a c : ℝ) : csMarginalOneExp a c 0 = 1 := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics inspired by Promislow (2015), chapters 11, 17 and 19, published book reference https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/; supporting published actuarial reference https://doi.org/10.1080/01621459.1967.10482885. The proposed model is rooted in Promislow chapter 11, 17 and 19. The target Lean identity is an original derivation, not a verbatim published result. Published source page 271 gives the thematic chapter context, rather than an exact statement of this new formal theorem.
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