Prove2Me

Lundberg adjustment coefficient and exponential-moment martingale factor: erSeverityTail_positive

Proved
ActuarialValuation.erSeverityTail_positive

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

actuarial-sciencecompound-poisson-ruin-renewalformal-verification

The exponential survival tail is positive for every finite real threshold. The exact assumptions, units and boundary conventions are recorded separately in the formal statement.

Mathematical relation:

The exponential survival tail is positive for every finite realthreshold.\begin{aligned}\text{The exponential survival tail is positive for every finite real} \\ \text{threshold.}\end{aligned}
Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Definitions.Def_actuarial_erSeverityTail
Formal statement
namespace ActuarialValuation

theorem erSeverityTail_positive (beta x : ℝ) : 0<erSeverityTail beta x := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 438. S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 23, sections 23.3–23.7; Hanspeter Schmidli, Risk Theory (2017), Springer Actuarial, https://link.springer.com/book/10.1007/978-3-319-72005-0; Palmowski et al. 2020, https://doi.org/10.1007/s13385-020-00223-4. Parent topic: Compound Poisson surplus with exponentially distributed claims, net profit, adjustment root, exact candidate ruin function and renewal differential/integral equation. 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://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml
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