ProbabilityTheory.measurable_poissonPMFReal
theorem ProbabilityTheory.measurable_poissonPMFReal : ∀ (r : NNReal), Measurable (ProbabilityTheory.poissonPMFReal r)
This theorem states that the probability mass function (pmf) of the Poisson distribution, which depends on its rate, is a measurable function for every nonnegative real number `r`. In other words, for every `r` in the set of nonnegative real numbers, the preimage of every measurable set under the Poisson pmf is also measurable. This is an important property in probability theory, which ensures that we can perform meaningful probability calculations with the Poisson pmf. This function, `ProbabilityTheory.poissonPMFReal`, takes a rate `r` and a natural number `n`, and returns a real number calculated by the formula $e^{-r} \cdot r^n / n!$.
More concisely: For every non-negative real number `r`, the Poisson probability mass function `r => (n: ℕ) => e^(-r) * r^n / (n!): ℝ` is a measurable function.
|
ProbabilityTheory.poissonPMFReal_pos
theorem ProbabilityTheory.poissonPMFReal_pos :
∀ {r : NNReal} {n : ℕ}, 0 < r → 0 < ProbabilityTheory.poissonPMFReal r n
The theorem states that the probability mass function (pmf) of the Poisson distribution is always positive for all natural numbers. This holds true for all nonnegative real numbers `r` that are greater than zero (i.e., they are positive) and for any natural number `n`. In other words, if `r` is the rate of a Poisson distribution, then the value of the pmf at any natural number `n` is always positive when the rate `r` is positive.
More concisely: For all positive real numbers `r` and natural numbers `n`, the probability mass function of the Poisson distribution with rate `r` is a positive value.
|