A nonnegative Poisson rate produces nonnegative count coefficients
ProvedActuarialValuation.poissonCountMass_nonnegactuarial-scienceaggregate-claimsformal-verification
The exponential factor is positive, the nth power of a nonnegative rate is nonnegative, and the real-cast factorial denominator is strictly positive. Therefore each Poisson count mass is nonnegative.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_poissonCountMass
Formal statement
namespace ActuarialValuation theorem poissonCountMass_nonneg (rate : ℝ) (n : ℕ) (hr : 0 ≤ rate) : 0 ≤ poissonCountMass rate n := 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. The only model assumption is that rate is nonnegative. Its nth real power is then nonnegative, the exponential multiplier is positive and the factorial denominator is positive. Together these give a nonnegative probability coefficient for every natural count, not an independent proof that the count masses sum to one.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.