poissonMeasure — Mathlib

English

The Poisson measure on natural numbers is defined from the Poisson PMF via the corresponding toMeasure construction.

Русский

Мера Пуассона на множествах натуральных чисел определяется через соответствующую PMF.

LaTeX

$$$\\mathrm{poissonMeasure}(r)=(\\mathrm{poissonPMF}(r)).\\mathrm{toMeasure}$$$

Lean4

/-- Measure defined by the Poisson distribution -/
noncomputable def poissonMeasure (r : ℝ≥0) : Measure ℕ :=
  (poissonPMF r).toMeasure

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