Convolution preserves nonnegative probability masses
ProvedActuarialValuation.aggregateConvolution_nonnegactuarial-scienceaggregate-claimsformal-verification
Each summand is a product of nonnegative component probabilities. The finite sum of such products is nonnegative, which ensures that combining two valid discrete probability distributions cannot create negative aggregate mass.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_aggregateConvolution
Formal statement
namespace ActuarialValuation theorem aggregateConvolution_nonneg (f g : ℕ → ℝ) (s : ℕ) (hf : ∀ k, 0 ≤ f k) (hg : ∀ k, 0 ≤ g k) : 0 ≤ aggregateConvolution f g s := by sorry end ActuarialValuation
Source
R J Verrall (1989), The individual risk model: a compound distribution, Journal of the Institute of Actuaries 116(1), 101–107, https://doi.org/10.1017/S0020268100036465; N De Pril (1989), The Aggregate Claims Distribution in the Individual Model with Arbitrary Positive Claims, ASTIN Bulletin 19(1), 9–24, https://doi.org/10.2143/AST.19.1.2014913; original finite convolution and support formalisation
Read-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. Each input coefficient function is assumed nonnegative at every natural index, including values beyond the requested claim s. Thus every finite term f(k)g(s-k) in the convolution is a nonnegative product and the entire sum cannot be negative. No unit-mass condition is needed for this simple positivity result.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.