Nonnegative component frequencies imply nonnegative combined frequency

Proved

ActuarialValuation.poissonSuperposedRate_nonneg

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

actuarial-scienceaggregate-claimsformal-verification

The intensity of a combined set of independent claim classes is the sum of their individual intensities. If both rates are legitimate nonnegative claim frequencies, the combined rate remains nonnegative.

Mathematical statement

\lambda_1,\lambda_2\ge0\Rightarrow\lambda_1+\lambda_2\ge0

Preamble

import Mathlib
import Definitions.Def_actuarial_poissonSuperposedRate

Formal statement

namespace ActuarialValuation

theorem poissonSuperposedRate_nonneg (a b : ℝ)
  (ha : 0 ≤ a) (hb : 0 ≤ b) :
  0 ≤ poissonSuperposedRate a b := by sorry

end ActuarialValuation

Source

S David Promislow (2015), Fundamentals of Actuarial Mathematics (3rd ed), ch 21 sections 21.8-21.9, library PDF pages 411-413; Poisson count thinning and splitting, plus actuarial claim-type superposition. See also SCMA469 Actuarial Statistics chapter 5 https://pairote-sat.github.io/SCMA469/poisson-processes.html

Read-back

What the Lean code literally says, in plain math · gpt-6

Independent mathematical reading. Both component rates are assumed at least zero, so their sum is nonnegative. That makes the source's superposed rate a legitimate Poisson intensity. No declaration of joint independence is involved in this positivity property; the count-convolution identity handles the actual distributional part.

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