Lundberg adjustment coefficient and exponential-moment martingale factor: erLundbergGap_at_zero

Proved

ActuarialValuation.erLundbergGap_at_zero

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

actuarial-sciencecompound-poisson-ruin-renewalformal-verification

Zero adjustment parameter is always a trivial solution to the cumulant equation. The exact assumptions, units and boundary conventions are recorded separately in the formal statement.

Mathematical relation:

\begin{aligned}\text{Zero adjustment parameter is always a trivial solution to the} \\ \text{cumulant equation.}\end{aligned}

Preamble

import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Definitions.Def_actuarial_erLundbergGap

Formal statement

namespace ActuarialValuation

theorem erLundbergGap_at_zero (lambda premium beta : ℝ) (hb : beta≠0) : erLundbergGap lambda premium beta 0=0 := 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