A zero-rate Poisson piece has no arrivals almost surely

Proved

AvramDividend.Classical.poisson_zero_rate_ae_zero

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

active-mark-piecesavram-classicalpoissonzero-intensity

Any natural-valued random count whose law is Poisson with mean zero is almost surely zero. Show that the zero-intensity Poisson measure equals a Dirac mass at zero using its singleton probabilities, then apply HasLaw.ae_eq_of_dirac. This prevents zero-mass partition pieces, whose dummy point laws can have time atoms, from generating active marks in the canonical Poisson construction.

Preamble

import Mathlib

open ProbabilityTheory MeasureTheory
open scoped ENNReal

Formal statement

theorem AvramDividend.Classical.poisson_zero_rate_ae_zero
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    [IsProbabilityMeasure P] (K : Ω → ℕ)
    (hK : HasLaw K (poissonMeasure 0) P) :
    ∀ᵐ ω ∂P, K ω = 0 := by sorry

Source

Mathlib.Probability.Distributions.Poisson.Basic: poissonMeasure_singleton, Measure.ext_of_singleton, HasLaw.ae_eq_of_dirac; LeanLevy PoissonPointFamily zero-mass fallback.

View graph