measurable_geometricPMFReal — Mathlib

English

Geometric distribution with success probability p: pmf is PMF Real defined by geometricPMFReal(p,n).

Русский

Геометрическое распределение с вероятностью успеха p имеет вероятностную функцию геометрического pmfReal(p,n).

LaTeX

$$$\text{geometricPMF}(p,n) = (1-p)^{n} p$, for p ∈ (0,1].$$

Lean4

/-- The geometric pmf is measurable. -/
@[fun_prop, measurability]
theorem measurable_geometricPMFReal : Measurable (geometricPMFReal p) := by fun_prop

Похожие утверждения