geometricMeasure — Mathlib

English

Geometric measure on natural numbers defined by geometricPMF hp_pos hp_le_one.

Русский

Геометрическая мера на множестве натуральных чисел, задаваемая геометрической pmf.

LaTeX

$$$\text{geometricMeasure}(hp\_pos: 0

Lean4

/-- Measure defined by the geometric distribution -/
noncomputable def geometricMeasure (hp_pos : 0 < p) (hp_le_one : p ≤ 1) : Measure ℕ :=
  (geometricPMF hp_pos hp_le_one).toMeasure

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