Expected aggregate claims and positive safety loading: erSafetyLoading_pos

Proved

ActuarialValuation.erSafetyLoading_pos

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

actuarial-sciencecompound-poisson-ruin-renewalformal-verification

Safety loading strictly positive under the expected premium adequacy condition. The exact assumptions, units and boundary conventions are recorded separately in the formal statement.

Mathematical relation:

\begin{aligned}\text{Safety loading strictly positive under the expected premium} \\ \text{adequacy condition.}\end{aligned}

Preamble

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

Formal statement

namespace ActuarialValuation

theorem erSafetyLoading_pos (c lambda beta : ℝ) (h : lambda<c*beta) : 0<erSafetyLoading c lambda beta := 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