English
If μ ≪ ν and both ν and ν' are σ-finite with ν ⟂ ν', then μ.rnDeriv(ν+ν') = μ.rnDeriv ν almost everywhere on ν.
Русский
Если μ ≪ ν и ν и ν' σ-подмеры и ν ⟂ ν', то μ.rnDeriv(ν+ν') = μ.rnDeriv ν почти наверху ν.
LaTeX
$$$μ.rnDeriv(ν+ν') =_{ν}^{ae} μ.rnDeriv ν$$$
Lean4
/-- Auxiliary lemma for `rnDeriv_add_right_of_mutuallySingular`. -/
theorem rnDeriv_add_right_of_mutuallySingular' {ν' : Measure α} [SigmaFinite μ] [SigmaFinite ν] [SigmaFinite ν']
(hμν' : μ ⟂ₘ ν') (hνν' : ν ⟂ₘ ν') : μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν :=
by
have h_ac : ν ≪ ν + ν' := Measure.AbsolutelyContinuous.rfl.add_right _
rw [haveLebesgueDecomposition_add μ ν]
have h₁ := rnDeriv_add' (μ.singularPart ν) (ν.withDensity (μ.rnDeriv ν)) (ν + ν')
have h₂ := rnDeriv_add' (μ.singularPart ν) (ν.withDensity (μ.rnDeriv ν)) ν
refine (Filter.EventuallyEq.trans (h_ac.ae_le h₁) ?_).trans h₂.symm
have h₃ :=
rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular (withDensity_absolutelyContinuous ν (μ.rnDeriv ν))
hνν'
have h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᵐ[ν] 0 :=
by
refine h_ac.ae_eq ?_
simp only [rnDeriv_eq_zero, MutuallySingular.add_right_iff]
exact ⟨mutuallySingular_singularPart μ ν, hμν'.singularPart ν⟩
have h₅ : (μ.singularPart ν).rnDeriv ν =ᵐ[ν] 0 := rnDeriv_singularPart μ ν
filter_upwards [h₃, h₄, h₅] with x hx₃ hx₄ hx₅
simp only [Pi.add_apply]
rw [hx₃, hx₄, hx₅]
