English
A variant of rnDeriv_mconv' ensuring equality almost everywhere for ν₁ ∗ₘ ν₂ when ν₁, ν₂ are absolutely continuous with respect to μ.
Русский
Вариант rnDeriv_mconv' с условием, что ν₁ ∗ₘ ν₂ имеет RN-деривив по μ аналогично произведению RN-дерививов.
LaTeX
$$$$ (ν₁ ∗ₘ ν₂).rnDeriv μ =^\mathrm{ae}_{μ} (ν₁.rnDeriv μ) ⋆ₘₗ[μ] (ν₂.rnDeriv μ) $$$$
Lean4
@[to_additive]
theorem rnDeriv_mconv [SFinite μ] {ν₁ ν₂ : Measure G} [IsFiniteMeasure ν₁] [IsFiniteMeasure ν₂]
[ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ] (hν₁ : ν₁ ≪ μ) (hν₂ : ν₂ ≪ μ) :
(ν₁ ∗ₘ ν₂).rnDeriv μ =ᵐ[μ] (ν₁.rnDeriv μ) ⋆ₘₗ[μ] (ν₂.rnDeriv μ) :=
by
have := HaveLebesgueDecomposition.mconv hν₁ hν₂
rw [← withDensity_eq_iff (by fun_prop) (by fun_prop), withDensity_rnDeriv_eq _ _ (mconv_absolutelyContinuous hν₂),
mconv_eq_withDensity_mlconvolution_rnDeriv hν₁ hν₂]
exact (lintegral_rnDeriv_lt_top (ν₁ ∗ₘ ν₂) μ).ne
