stronglyMeasurable_poissonPMFReal

English

The Poisson pmfReal is strongly measurable in its rate parameter.

Русский

Плотность Пуассона по параметру скорости является сильно измеримой.

LaTeX

$$$\\mathrm{StronglyMeasurable}(\\mathrm{poissonPMFReal}(r))$$$

Lean4

@[fun_prop, measurability]
theorem stronglyMeasurable_poissonPMFReal (r : ℝ≥0) : StronglyMeasurable (poissonPMFReal r) :=
  stronglyMeasurable_iff_measurable.mpr (measurable_poissonPMFReal r)

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