English
If μ ≪ ν and ν ⟂ ν' (mutually singular), then μ.rnDeriv(ν+ν') = μ.rnDeriv ν almost everywhere with respect to ν.
Русский
Если μ ≪ ν и ν и ν' взаимоисключимы, то μ.rnDeriv(ν+ν') = μ.rnDeriv ν почти всюду по ν.
LaTeX
$$$μ.rnDeriv(ν+ν') =_{ν}^{ae} μ.rnDeriv ν \\quad (ν ⟂ ν')$$$
Lean4
/-- Auxiliary lemma for `rnDeriv_withDensity_right`. -/
theorem rnDeriv_withDensity_right_of_absolutelyContinuous {ν : Measure α} [HaveLebesgueDecomposition μ ν]
[SigmaFinite ν] (hμν : μ ≪ ν) (hf : AEMeasurable f ν) (hf_ne_zero : ∀ᵐ x ∂ν, f x ≠ 0)
(hf_ne_top : ∀ᵐ x ∂ν, f x ≠ ∞) : μ.rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x :=
by
have : SigmaFinite (ν.withDensity f) := SigmaFinite.withDensity_of_ne_top hf_ne_top
refine (withDensity_absolutelyContinuous' hf hf_ne_zero).ae_eq ?_
refine (Measure.eq_rnDeriv₀ (ν := ν.withDensity f) ?_ Measure.MutuallySingular.zero_left ?_).symm
· exact (hf.inv.mono_ac (withDensity_absolutelyContinuous _ _)).mul (Measure.measurable_rnDeriv _ _).aemeasurable
· ext1 s hs
conv_lhs => rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]
rw [zero_add, withDensity_apply _ hs, withDensity_apply _ hs]
rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
· simp only [Pi.mul_apply]
have : (fun a ↦ f a * ((f a)⁻¹ * μ.rnDeriv ν a)) =ᵐ[ν] μ.rnDeriv ν :=
by
filter_upwards [hf_ne_zero, hf_ne_top] with x hx1 hx2
simp [← mul_assoc, ENNReal.mul_inv_cancel, hx1, hx2]
rw [lintegral_congr_ae (ae_restrict_of_ae this)]
· refine ae_restrict_of_ae ?_
filter_upwards [hf_ne_top] with x hx using hx.lt_top
· exact hf.restrict
