Poisson distributions over ℕ

Define the Poisson measure over the natural numbers. For r : ℝ≥0, poissonMeasure r is the measure which to {n} associates exp (-r) * r ^ n / (n)!.

Main definition

• poissonMeasure r: a Poisson measure on ℕ, parametrized by its rate r : ℝ≥0.

noncomputable def ProbabilityTheory.poissonMeasure (r : NNReal) : MeasureTheory.Measure ℕ

The poisson measure with rate r : ℝ≥0 as a measure over ℕ.

theorem ProbabilityTheory.poissonMeasure_singleton (r : NNReal) (n : ℕ) : (poissonMeasure r) {n} = ENNReal.ofReal (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial)

theorem ProbabilityTheory.poissonMeasure_real_singleton (r : NNReal) (n : ℕ) : (poissonMeasure r).real {n} = Real.exp (-↑r) * ↑r ^ n / ↑n.factorial

theorem ProbabilityTheory.poissonMeasure_real_singleton_pos {r : NNReal} (n : ℕ) (hr : 0 < r) : 0 < (poissonMeasure r).real {n}

theorem ProbabilityTheory.hasSum_one_poissonMeasure (r : NNReal) : HasSum (fun (n : ℕ) => Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) 1

instance ProbabilityTheory.isProbabilityMeasure_poissonMeasure (r : NNReal) : MeasureTheory.IsProbabilityMeasure (poissonMeasure r)

theorem ProbabilityTheory.integrable_poissonMeasure_iff {E : Type u_1} [NormedAddCommGroup E] {r : NNReal} {f : ℕ → E} : MeasureTheory.Integrable f (poissonMeasure r) ↔ Summable fun (n : ℕ) => Real.exp (-↑r) * ↑r ^ n / ↑n.factorial * ‖f n‖

theorem ProbabilityTheory.hasSum_integral_poissonMeasure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {r : NNReal} {f : ℕ → E} (hf : MeasureTheory.Integrable f (poissonMeasure r)) : HasSum (fun (n : ℕ) => (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • f n) (∫ (n : ℕ), f n ∂poissonMeasure r)

theorem ProbabilityTheory.integral_poissonMeasure' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {r : NNReal} {f : ℕ → E} (hf : MeasureTheory.Integrable f (poissonMeasure r)) : ∫ (n : ℕ), f n ∂poissonMeasure r = ∑' (n : ℕ), (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • f n

If a function is integrable with respect to poissonMeasure r, then its integral against this measure is given by its sum weighted by exp (-r) * r ^ n / n!.

See integral_poissonMeasure for a version where the codomain is finite-dimensional and does not require the integrability hypothesis.

theorem ProbabilityTheory.integral_poissonMeasure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (r : NNReal) (f : ℕ → E) : ∫ (n : ℕ), f n ∂poissonMeasure r = ∑' (n : ℕ), (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • f n

The integral of a function taking values in a finite-dimensional space against poissonMeasure r is given by its sum weighted by exp (-r) * r ^ n / n!. This version does not require integrability, as the integral exists if and only if the sum exists, and otherwise they are both defined to be zero.

See integral_poissonMeasure' with a general codomain which assumes integrability.

@[deprecated ProbabilityTheory.poissonMeasure (since := "2026-03-08")]

noncomputable def ProbabilityTheory.poissonPMFReal (r : NNReal) (n : ℕ) : ℝ

The pmf of the Poisson distribution depending on its rate, as a function to ℝ

@[deprecated ProbabilityTheory.hasSum_one_poissonMeasure (since := "2026-03-08")]

theorem ProbabilityTheory.poissonPMFRealSum (r : NNReal) : HasSum (fun (n : ℕ) => poissonPMFReal r n) 1

@[deprecated ProbabilityTheory.poissonMeasure_real_singleton_pos (since := "2026-03-08")]

theorem ProbabilityTheory.poissonPMFReal_pos {r : NNReal} {n : ℕ} (hr : 0 < r) : 0 < poissonPMFReal r n

@[deprecated MeasureTheory.measureReal_nonneg (since := "2026-03-08")]

theorem ProbabilityTheory.poissonPMFReal_nonneg {r : NNReal} {n : ℕ} : 0 ≤ poissonPMFReal r n

@[deprecated ProbabilityTheory.poissonMeasure (since := "2026-03-08")]

noncomputable def ProbabilityTheory.poissonPMF (r : NNReal) : PMF ℕ

The pmf of the Poisson distribution depending on its rate, as a PMF.

@[deprecated ProbabilityTheory.poissonMeasure (since := "2026-03-08")]

theorem ProbabilityTheory.poissonPMFReal_ofReal_eq_poissonPMF (r : NNReal) (n : ℕ) : ENNReal.ofReal (poissonPMFReal r n) = (poissonPMF r) n

@[deprecated Measurable.of_discrete (since := "2026-03-08")]

theorem ProbabilityTheory.measurable_poissonPMFReal (r : NNReal) : Measurable (poissonPMFReal r)

@[deprecated MeasureTheory.StronglyMeasurable.of_discrete (since := "2026-03-08")]

theorem ProbabilityTheory.stronglyMeasurable_poissonPMFReal (r : NNReal) : MeasureTheory.StronglyMeasurable (poissonPMFReal r)