Aggregate tail probability is nonnegative
ProvedActuarialValuation.discreteStopLossTail_nonnegactuarial-scienceaggregate-claimsformal-verification
The tail is an indicator-weighted sum over discrete losses above the attachment point. Every included probability mass is nonnegative, so the total excess-claim probability is nonnegative.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_discreteStopLossTail
Formal statement
namespace ActuarialValuation theorem discreteStopLossTail_nonneg (w : ℕ → ℝ) (bound deductible : ℕ) (hw : ∀ s, 0 ≤ w s) : 0 ≤ discreteStopLossTail w bound deductible := by sorry end ActuarialValuation
Source
H H Panjer (1980), The aggregate claims distribution and stop-loss reinsurance, Transactions of the Society of Actuaries 32, 523–535; H H Panjer and G E Willmot (1982), Recursions for compound distributions, ASTIN Bulletin; Willmot, Drekic and Cai (2005), Equilibrium compound distributions and stop-loss moments, https://doi.org/10.1080/03461230510009691; exact finite discrete stop-loss specialisation
Read-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. The formal tail sum selects the coefficients at claims strictly above deductible and replaces all other contributions by zero. If every coefficient is nonnegative, so is this sum. The theorem does not need unit total probability to establish its sign.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.