English
If ν₁ and ν₂ are absolutely continuous w.r.t μ and μ is Lebesgue-decomposed, then their mconv has Lebesgue decomposition with density given by the convolution of RN-derivatives with μ.
Русский
Если ν₁, ν₂ абсолютно непрерывны по μ и μ имеет разложение Лебега, то mconv ν₁ ν₂ имеет разложение Лебега с плотностью, равной свёртке RN-дерививов по μ.
LaTeX
$$$$ (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ = ⟨0, (ν₁.rnDeriv μ) ⋆ₘₗ[μ] (ν₂.rnDeriv μ)⟩ $$$$
Lean4
/-- A version of `setIntegral_rnDeriv_smul` that requires both measures to be σ-finite,
but doesn't require `s` to be a measurable set. -/
theorem setIntegral_rnDeriv_smul' [SigmaFinite ν] (hμν : μ ≪ ν) (s : Set α) :
∫ 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 _ _)]
