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.

Main results

• poissonMeasure_conv_poissonMeasure: Poisson(r₁) ∗ Poisson(r₂) = Poisson(r₁ + r₂).
• IndepFun.hasLaw_add_poissonMeasure: the sum of two independent Poisson random variables is again Poisson.

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

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

Equations

• ProbabilityTheory.poissonMeasure r = MeasureTheory.Measure.sum fun (n : ℕ) => ENNReal.ofReal (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • MeasureTheory.Measure.dirac n

def ProbabilityTheory.«termPo(_)» : Lean.ParserDescr

The Poisson probability distribution with rate r.

Equations

• One or more equations did not get rendered due to their size.

def ProbabilityTheory.«termPo(_,_)» : Lean.ParserDescr

The Poisson probability distribution with rate r valued in the AddMonoidWithOne R.

Equations

• One or more equations did not get rendered due to their size.

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.instIsProbabilityMeasureNatPoissonMeasure (r : NNReal) : MeasureTheory.IsProbabilityMeasure (poissonMeasure r)

instance ProbabilityTheory.instIsProbabilityMeasureMapNatCastPoissonMeasure (r : NNReal) {R : Type u_1} [NatCast R] [MeasurableSpace R] : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map Nat.cast (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.integrable_map_cast_poissonMeasure_iff {E : Type u_1} [NormedAddCommGroup E] {R : Type u_2} [NatCast R] [MeasurableSpace R] {r : NNReal} [Countable R] [MeasurableSingletonClass R] {f : R → E} : MeasureTheory.Integrable f (MeasureTheory.Measure.map Nat.cast (poissonMeasure r)) ↔ MeasureTheory.Integrable (f ∘ Nat.cast) (poissonMeasure r)

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_map_cast_poissonMeasure' {E : Type u_1} [NormedAddCommGroup E] {R : Type u_2} [NatCast R] [MeasurableSpace R] [NormedSpace ℝ E] [CompleteSpace E] [Countable R] [MeasurableSingletonClass R] {r : NNReal} {f : R → E} (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.map Nat.cast (poissonMeasure r))) : ∫ (x : R), f x ∂MeasureTheory.Measure.map Nat.cast (poissonMeasure r) = ∑' (n : ℕ), (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • f ↑n

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.

theorem ProbabilityTheory.integral_map_cast_poissonMeasure {E : Type u_1} [NormedAddCommGroup E] {R : Type u_2} [NatCast R] [MeasurableSpace R] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (r : NNReal) [Countable R] [MeasurableSingletonClass R] (f : R → E) : ∫ (x : R), f x ∂MeasureTheory.Measure.map Nat.cast (poissonMeasure r) = ∑' (n : ℕ), (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • f ↑n

theorem ProbabilityTheory.charFun_map_cast_poissonMeasure (r : NNReal) (t : ℝ) : MeasureTheory.charFun (MeasureTheory.Measure.map Nat.cast (poissonMeasure r)) t = Complex.exp (↑↑r * (Complex.exp (↑t * Complex.I) - 1))

The characteristic function of the Poisson distribution with rate r is t ↦ exp(r(exp(it) - 1)).

Convolution of Poisson measures

theorem ProbabilityTheory.poissonMeasure_conv_poissonMeasure (r₁ r₂ : NNReal) : (poissonMeasure r₁).conv (poissonMeasure r₂) = poissonMeasure (r₁ + r₂)

theorem ProbabilityTheory.map_cast_poissonMeasure_conv {R : Type u_1} [AddMonoidWithOne R] {mR : MeasurableSpace R} [MeasurableAdd₂ R] (r₁ r₂ : NNReal) : (MeasureTheory.Measure.map Nat.cast (poissonMeasure r₁)).conv (MeasureTheory.Measure.map Nat.cast (poissonMeasure r₂)) = MeasureTheory.Measure.map Nat.cast (poissonMeasure (r₁ + r₂))

theorem ProbabilityTheory.IndepFun.hasLaw_add_poissonMeasure {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {r₁ r₂ : NNReal} {X Y : Ω → ℕ} (hXY : IndepFun X Y P) (hX : HasLaw X (poissonMeasure r₁) P) (hY : HasLaw Y (poissonMeasure r₂) P) : HasLaw (X + Y) (poissonMeasure (r₁ + r₂)) P

The sum of two independent Poisson random variables with rates r₁, r₂ is a Poisson random variable with rate r₁ + r₂.

theorem ProbabilityTheory.IndepFun.hasLaw_add_map_cast_poissonMeasure {R : Type u_1} [AddMonoidWithOne R] {mR : MeasurableSpace R} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasurableAdd₂ R] {r₁ r₂ : NNReal} {X Y : Ω → R} (hXY : IndepFun X Y P) (hX : HasLaw X (MeasureTheory.Measure.map Nat.cast (poissonMeasure r₁)) P) (hY : HasLaw Y (MeasureTheory.Measure.map Nat.cast (poissonMeasure r₂)) P) : HasLaw (X + Y) (MeasureTheory.Measure.map Nat.cast (poissonMeasure (r₁ + r₂))) P

The sum of two independent Poisson random variables with rates r₁, r₂ taking values in R is a Poisson random variable with rate r₁ + r₂.

@[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 ℝ

Equations

• ProbabilityTheory.poissonPMFReal r n = Real.exp (-↑r) * ↑r ^ n / ↑n.factorial

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

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

Alias of ProbabilityTheory.hasSum_one_poissonMeasure.

@[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.

Equations

• ProbabilityTheory.poissonPMF r = ⟨fun (n : ℕ) => ENNReal.ofReal (ProbabilityTheory.poissonPMFReal r n), ⋯⟩

@[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)