Prove2Me

Ruin events and finite-horizon Lundberg bound: ruFiniteRuinBound_le_one

Proved
ActuarialValuation.ruFiniteRuinBound_le_one

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

actuarial-scienceformal-verificationmartingale-ruin-stopping

Positive adjustment coefficient and initial capital make the exponential bound no larger than one.

Mathematical relation:

ruFiniteRuinBound_le_oneruFiniteRuinBound\_le\_one

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

Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Analysis.SpecialFunctions.Exp
import Definitions.Def_actuarial_ruFiniteRuinBound
Formal statement
namespace ActuarialValuation

theorem ruFiniteRuinBound_le_one (R u : ℝ) (hR : 0≤R) (hu : 0≤u) : ruFiniteRuinBound R u ≤ 1 := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics inspired by Promislow (2015), chapters 18 and 23, published book reference https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/; supporting published actuarial reference https://ocw.mit.edu/courses/18-440-probability-and-random-variables-spring-2014/resources/mit18_440s14_lecture35/. The proposed model is rooted in Promislow chapter 18 and 23. The target Lean identity is an original derivation, not a verbatim published result. Published source page 426 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