Nonnegative frequency and severity masses yield nonnegative aggregate mass
ProvedActuarialValuation.compoundPoissonAggregatePMF_nonnegPoisson weights are nonnegative at every claim count for a nonnegative rate. Repeated finite convolution of nonnegative claim-severity masses remains nonnegative. Their finite weighted mixture therefore yields no negative aggregate-loss probability coefficient.
Mathematical statement
import Mathlib import Definitions.Def_actuarial_compoundPoissonAggregatePMF import Definitions.Def_actuarial_compoundPoissonCountWeight import Definitions.Def_actuarial_compoundPoissonSeverityPower
namespace ActuarialValuation theorem compoundPoissonAggregatePMF_nonneg (rate : ℝ) (f : ℕ → ℝ) (s : ℕ) (hr : 0 ≤ rate) (hf : ∀ k, 0 ≤ f k) : 0 ≤ compoundPoissonAggregatePMF rate f s := by sorry end ActuarialValuation
Read-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. A nonnegative rate makes all Poisson weights nonnegative, and a nonnegative severity array stays nonnegative under each finite convolution power. Every finite term in the mixture for the requested aggregate s is consequently nonnegative. The formal claim is only coefficient nonnegativity, not total normalisation of an unbounded infinite aggregate distribution.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.