Retained loss is nonnegative for nonnegative inputs

Proved

ActuarialValuation.retainedExcessLoss_nonnegative

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

dynamic-programmingfinite-horizonreinsurance

The minimum of two nonnegative monetary amounts is nonnegative.

Mathematical statement

z,a\ge0\implies r(z,a)\ge0

Preamble

import Mathlib
import Definitions.Def_actuarial_retainedExcessLoss
open MeasureTheory

Formal statement

namespace ActuarialValuation

theorem retainedExcessLoss_nonnegative (z a : ℝ) (hz : 0 ≤ z) (ha : 0 ≤ a)
  :
  0 ≤ retainedExcessLoss z a := by sorry

end ActuarialValuation

Source

Brachetta and Ceci (2019), Optimal Excess-of-Loss Reinsurance for Stochastic Factor Risk Models, Risks 7(2) 48, DOI https://doi.org/10.3390/risks7020048, §2 retained loss min(z,alpha), §3 HJB optimisation; Puterman (1994), Markov Decision Processes: Discrete Stochastic Dynamic Programming, Chapter 4 finite-horizon Bellman/backward induction, https://doi.org/10.1002/9780470316887.ch4

Read-back

What the Lean code literally says, in plain math · gpt-6

Independent mathematical reading. If both gross claim z and retention a are nonnegative, their minimum is nonnegative. This supplies a necessary economic constraint on realised retained loss while preserving the general signed definition used elsewhere.

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by WillR · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph