integral_rnDeriv_smul — Mathlib

English

A variant of the previous result, with relaxed hypotheses, showing a.e. equality of the RN-deriv of ν₁ ∗ₘ ν₂ with the product of RN-derivs with respect to μ.

Русский

Вариант предыдущего результата с ослабленными предположениями: a.e. равенство RN-дерививов конволюции.

LaTeX

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

Lean4

theorem integral_rnDeriv_smul (hμν : μ ≪ ν) : ∫ x, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ x, f x ∂μ := by
  rw [← integral_withDensity_eq_integral_toReal_smul (measurable_rnDeriv _ _) (rnDeriv_lt_top _ _),
    withDensity_rnDeriv_eq _ _ hμν]

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