stronglyMeasurable_paretoPDFReal — Mathlib

English

For fixed t and r, the Pareto pdfReal is strongly measurable.

Русский

Для фиксированных t и r плотность Парето является сильно измеримой.

LaTeX

$$$\\mathrm{StronglyMeasurable}(\\mathrm{paretoPDFReal}(t,r))$$$

Lean4

/-- The Pareto pdf is strongly measurable. -/
@[fun_prop, measurability]
theorem stronglyMeasurable_paretoPDFReal (t r : ℝ) : StronglyMeasurable (paretoPDFReal t r) :=
  (measurable_paretoPDFReal t r).stronglyMeasurable

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