ProbabilityTheory.geometricPMFReal_pos
theorem ProbabilityTheory.geometricPMFReal_pos :
∀ {p : ℝ} {n : ℕ}, 0 < p → p < 1 → 0 < ProbabilityTheory.geometricPMFReal p n
This theorem states that the probability mass function (pmf) of the geometric distribution is always positive for all natural numbers. More precisely, given any real number `p` between 0 and 1 (exclusive) and any natural number `n`, the value of the geometric pmf, which is defined as `(1 - p) ^ n * p`, is always positive. This reflects the fact that the probability of any particular outcome in a geometric distribution is always a positive value.
More concisely: For all real numbers `p` with `0 < p < 1` and natural numbers `n`, the geometric pmf `(1 - p) ^ n * p` is a positive value.
|
ProbabilityTheory.measurable_geometricPMFReal
theorem ProbabilityTheory.measurable_geometricPMFReal : ∀ {p : ℝ}, Measurable (ProbabilityTheory.geometricPMFReal p)
This theorem states that the probability mass function (pmf) of the geometric distribution, which depends on its success probability `p`, is a measurable function. In the context of this theorem, a function is measurable if for every measurable set, its preimage under the function is also a measurable set. Here, the measurability of the geometric pmf means that for any measurable set of real numbers, the set of all natural numbers whose corresponding geometric pmf values are in that set is also measurable.
More concisely: The geometric distribution's probability mass function is a measurable function.
|