Prove2Me

Admissible independent policy probabilities give nonnegative aggregate masses

Proved
ActuarialValuation.aggregatePortfolioPMF_nonneg

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

actuarial-scienceaggregate-claimsformal-verification

Every participating individual claim probability lies within zero and one, so each Bernoulli claim mass is nonnegative. Convolving these mass functions from the empty portfolio preserves nonnegativity for every attainable and unattainable aggregate claim amount.

Mathematical statement

0≤pi≤1⟹gn(s)≥00\le p_i\le1\Longrightarrow g_n(s)\ge0
Preamble
import Mathlib
import Definitions.Def_actuarial_aggregatePortfolioPMF
Formal statement
namespace ActuarialValuation

theorem aggregatePortfolioPMF_nonneg (p : ℕ → ℝ) (b : ℕ → ℕ)
  (n s : ℕ) (h : ∀ i, i < n → 0 ≤ p i ∧ p i ≤ 1) :
  0 ≤ aggregatePortfolioPMF p b n 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. For every index below n, the policy probability is constrained to the closed unit interval, guaranteeing that both Bernoulli event masses are nonnegative. Induction across n and positivity of finite convolution imply that every aggregate claim coefficient is nonnegative. The resulting bound is for an arbitrary requested loss s, not only those below maximum benefit.

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