def
IsPoissonRV
{Ω : Type u_1}
[MeasurableSpace Ω]
(X : Ω → ℕ)
(μ : MeasureTheory.Measure Ω)
(r : NNReal)
:
IsPoissonRV X μ r says that X : Ω → ℕ is a Poisson random variable with parameter
r ≥ 0 under the measure μ: for every k ∈ ℕ, P(X = k) = r^k e^{-r} / k! (Lecture 17,
Definition (Poisson random variable)).