English
Auxiliary lemma: the Radon–Nikodym derivative with a left density commutes with an additional left density under appropriate finiteness assumptions.
Русский
Вспомогательная лемма: производная радона-никодима после левого взведения плотности совпадает с другой такой же производной почти наверху ν, при подходящих условиях конечности.
LaTeX
$$$((\\nu.\\mathrm{withDensity}(\\mu.\\mathrm{rnDeriv}\\nu)).\\mathrm{withDensity} f).rnDeriv \\nu =_{\\nu}^{ae} (\\mu.\\mathrm{withDensity} f).rnDeriv \\nu$$$
Lean4
/-- Auxiliary lemma for `rnDeriv_withDensity_left`. -/
theorem rnDeriv_withDensity_withDensity_rnDeriv_left (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν]
(hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ∞) :
((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᵐ[ν] (μ.withDensity f).rnDeriv ν :=
by
conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm, withDensity_add_measure]
have : SigmaFinite ((μ.singularPart ν).withDensity f) :=
SigmaFinite.withDensity_of_ne_top (ae_mono (Measure.singularPart_le _ _) hf_ne_top)
have : SigmaFinite ((ν.withDensity (μ.rnDeriv ν)).withDensity f) :=
SigmaFinite.withDensity_of_ne_top (ae_mono (Measure.withDensity_rnDeriv_le _ _) hf_ne_top)
exact (rnDeriv_add_of_mutuallySingular _ _ _ (mutuallySingular_singularPart μ ν).withDensity).symm
