A nonnegative aggregate distribution yields nonnegative stop-loss premium
ProvedActuarialValuation.discreteStopLossPremium_nonnegactuarial-scienceaggregate-claimsformal-verification
Every realised stop-loss payout is a nonnegative integer. Nonnegative probability masses make all weighted claim payments nonnegative and hence their finite sum, the pure stop-loss premium, cannot be negative.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_discreteStopLossPremium
Formal statement
namespace ActuarialValuation theorem discreteStopLossPremium_nonneg (w : ℕ → ℝ) (bound deductible : ℕ) (hw : ∀ s, 0 ≤ w s) : 0 ≤ discreteStopLossPremium 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. Every stop-loss claim payment is a nonnegative natural number, and all coefficients w(s) are separately assumed nonnegative. Their products form a finite collection of nonnegative summands. Hence the expected ceded net premium is nonnegative, including deductibles greater than the maximum supported claim.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.