Poisson distributions over ℕ

Define the Poisson measure over the natural numbers

Main definitions

• poissonPMFReal: the function fun n ↦ exp (- λ) * λ ^ n / n! for n ∈ ℕ, which is the probability density function of a Poisson distribution with rate λ > 0.
• poissonPMF: ℝ≥0∞-valued pdf, poissonPMF λ = ENNReal.ofReal (poissonPMFReal λ).
• poissonMeasure: a Poisson measure on ℕ, parametrized by its rate λ.

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 / ↑(Nat.factorial n)

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

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

The Poisson pmf is positive for all natural numbers

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

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

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

Equations

• ProbabilityTheory.poissonPMF r = { val := fun (n : ℕ) => ENNReal.ofReal (ProbabilityTheory.poissonPMFReal r n), property := ⋯ }

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

The Poisson pmf is measurable.

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

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

Measure defined by the Poisson distribution

Equations

• ProbabilityTheory.poissonMeasure r = PMF.toMeasure (ProbabilityTheory.poissonPMF r)

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

Equations

• ⋯ = ⋯