integrableOn_toReal_rnDeriv — Mathlib

English

Variant: reciprocal RN-derivative relation under σ-finiteness, similar to inv_rnDeriv'.

Русский

Вариант: отношение обратного RN-дериватива при σ-конечности, аналогично inv_rnDeriv'.

LaTeX

$$$(ν.rnDeriv μ)^{-1} =_{μ}^{ae} μ.rnDeriv ν$$$

Lean4

theorem integrableOn_toReal_rnDeriv {s : Set α} (hμs : μ s ≠ ∞) : IntegrableOn (fun x ↦ (μ.rnDeriv ν x).toReal) s ν :=
  by
  refine integrable_toReal_of_lintegral_ne_top (Measure.measurable_rnDeriv _ _).aemeasurable ?_
  exact ((setLIntegral_rnDeriv_le _).trans_lt hμs.lt_top).ne

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