English
Auxiliary lemma: the Radon–Nikodym derivative with a right density remains the same under a density change to ν, up to almost everywhere equality.
Русский
Вспомогательная лемма: производная Радона–Никодима после правой плотности остаётся равной почти повсюду при изменении плотности по ν.
LaTeX
$$$(\\nu.\\mathrm{withDensity}(\\mu.rnDeriv ν)).rnDeriv(\\nu.withDensity f) =_{ν}^{ae} μ.rnDeriv(ν.withDensity f)$$$
Lean4
/-- Auxiliary lemma for `rnDeriv_withDensity_right`. -/
theorem rnDeriv_withDensity_withDensity_rnDeriv_right (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν]
(hf : AEMeasurable f ν) (hf_ne_zero : ∀ᵐ x ∂ν, f x ≠ 0) (hf_ne_top : ∀ᵐ x ∂ν, f x ≠ ∞) :
(ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f) :=
by
conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm]
have hν_ac : ν ≪ ν.withDensity f := withDensity_absolutelyContinuous' hf hf_ne_zero
refine hν_ac.ae_eq ?_
have : SigmaFinite (ν.withDensity f) := SigmaFinite.withDensity_of_ne_top hf_ne_top
refine (rnDeriv_add_of_mutuallySingular _ _ _ ?_).symm
exact ((mutuallySingular_singularPart μ ν).symm.withDensity).symm
