English
If ν is mutually singular to ν' and both μ and ν are σ-finite, then μ.rnDeriv(ν+ν') = μ.rnDeriv ν almost everywhere on ν.
Русский
Если ν взаимно отличается ν' и μ, ν— σ-конечны, то μ.rnDeriv(ν+ν') = μ.rnDeriv ν почти наверху ν.
LaTeX
$$$μ.rnDeriv(ν+ν') =_{ν}^{ae} μ.rnDeriv ν$$$
Lean4
theorem rnDeriv_add_right_of_mutuallySingular {ν' : Measure α} [SigmaFinite μ] [SigmaFinite ν] [SigmaFinite ν']
(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_mutuallySingular' (?_ : μ.singularPart ν' ⟂ₘ ν') hνν'
· have h₄ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv (ν + ν') =ᵐ[ν] 0 :=
by
refine rnDeriv_eq_zero_of_mutuallySingular ?_ h_ac
exact hνν'.symm.withDensity
have h₅ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv ν =ᵐ[ν] 0 :=
by
rw [rnDeriv_eq_zero]
exact hνν'.symm.withDensity
filter_upwards [h₃, h₄, h₅] with x hx₃ hx₄ hx₅
rw [Pi.add_apply, Pi.add_apply, hx₃, hx₄, hx₅]
exact mutuallySingular_singularPart μ ν'
