English
If ν' is mutually singular to ν, then μ.rnDeriv(ν+ν') = μ.rnDeriv ν almost everywhere with respect to ν.
Русский
Если ν' взаимоисключимо ν, то μ.rnDeriv(ν+ν') = μ.rnDeriv ν почти всюду по ν.
LaTeX
$$$μ.rnDeriv(ν+ν') =_{ν}^{ae} μ.rnDeriv ν$$$
Lean4
/-- Auxiliary lemma for `rnDeriv_add_right_of_mutuallySingular`. -/
theorem rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular {ν' : Measure α} [HaveLebesgueDecomposition μ ν]
[HaveLebesgueDecomposition μ (ν + ν')] [SigmaFinite ν] (hμν : μ ≪ ν) (hνν' : ν ⟂ₘ ν') :
μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν := by
let t := hνν'.nullSet
have ht : MeasurableSet t := hνν'.measurableSet_nullSet
refine ae_of_ae_restrict_of_ae_restrict_compl t (by simp [t]) ?_
change μ.rnDeriv (ν + ν') =ᵐ[ν.restrict tᶜ] μ.rnDeriv ν
rw [←
withDensity_eq_iff_of_sigmaFinite (μ := ν.restrict tᶜ) (Measure.measurable_rnDeriv _ _).aemeasurable
(Measure.measurable_rnDeriv _ _).aemeasurable]
have : (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = ((ν + ν').restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) :=
by simp [t]
rw [this, ← restrict_withDensity ht.compl, ← restrict_withDensity ht.compl,
Measure.withDensity_rnDeriv_eq _ _ (hμν.add_right ν'), Measure.withDensity_rnDeriv_eq _ _ hμν]
