isProbabilityMeasure_geometricMeasure

English

Let p be a real number with 0 < p ≤ 1. The geometric distribution with parameter p defines a probability measure on the natural numbers.

Русский

Пусть p ∈ (0,1]. Геометрическое распределение с параметром p задаёт вероятностную меру на множестве натуральных чисел.

LaTeX

$$$ (0 < p) \land (p \\le 1) \\Rightarrow \\text{IsProbabilityMeasure}(\\text{geometricMeasure}(p)) $$$

Lean4

theorem isProbabilityMeasure_geometricMeasure (hp_pos : 0 < p) (hp_le_one : p ≤ 1) :
    IsProbabilityMeasure (geometricMeasure hp_pos hp_le_one) :=
  PMF.toMeasure.isProbabilityMeasure (geometricPMF hp_pos hp_le_one)

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