setIntegral_rnDeriv_smul — Mathlib

English

A symmetric statement for RN-deriv under mconv', expressing equality almost everywhere with respect to μ.

Русский

Симметричное утверждение для RN-деривива при mconv', равенство почти всюду по μ.

LaTeX

$$$$ (ν₁ ∗ₘ ν₂).rnDeriv μ =^\mathrm{ae}_{μ} (ν₁.rnDeriv μ) ⋆ₘₗ[μ] (ν₂.rnDeriv μ) $$$$

Lean4

/-- See also `setIntegral_rnDeriv_smul'` for a version that requires both measures to be σ-finite,
but doesn't require `s` to be a measurable set. -/
theorem setIntegral_rnDeriv_smul (hμν : μ ≪ ν) {s : Set α} (hs : MeasurableSet s) :
    ∫ x in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ x in s, f x ∂μ :=
  by
  rw [← setIntegral_withDensity_eq_setIntegral_toReal_smul, withDensity_rnDeriv_eq _ _ hμν]
  exacts [measurable_rnDeriv _ _, ae_restrict_of_ae (rnDeriv_lt_top _ _), hs]

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