integrable_toReal_rnDeriv — Mathlib

English

If μ is finite, then the function x ↦ (μ.rnDeriv ν)(x) toReal is integrable with respect to ν.

Русский

Если μ конечна, то функция x ↦ (μ.rnDeriv ν)(x) в степени toReal интегрируема по ν.

LaTeX

$$$$\text{Integrable}\left(x \mapsto (\mu\,\text{rnDeriv}\,\nu\,x)^{\toReal}\right)\nu.$$$$

Lean4

@[fun_prop]
theorem integrable_toReal_rnDeriv [IsFiniteMeasure μ] : Integrable (fun x ↦ (μ.rnDeriv ν x).toReal) ν :=
  integrable_toReal_of_lintegral_ne_top (Measure.measurable_rnDeriv _ _).aemeasurable
    (Measure.lintegral_rnDeriv_lt_top _ _).ne

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