measurable_paretoPDFReal — Mathlib

English

For fixed t and r, the real-valued Pareto pdf as a function of x is measurable.

Русский

При фиксированных t и r функцией Плотности Парето в отношении x является измеримой.

LaTeX

$$$\\mathrm{Measurable}(\\mathrm{paretoPDFReal}(t,r,\\cdot))$$$

Lean4

/-- The Pareto pdf is measurable. -/
@[measurability, fun_prop]
theorem measurable_paretoPDFReal (t r : ℝ) : Measurable (paretoPDFReal t r) :=
  Measurable.ite measurableSet_Ici ((measurable_id.pow_const _).const_mul _) measurable_const

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