English
If ν₁, ν₂, μ are σ-finite, then (ν₁ + ν₂).rnDeriv μ =ᵐ μ ν₁.rnDeriv μ + ν₂.rnDeriv μ.
Русский
Если все меры σ-финитны, то производная по сумме равна сумме производных.
LaTeX
$$$$ (\\nu_1 + \\nu_2).rnDeriv \\mu =^{a.e.}_{\\mu} \\nu_1.rnDeriv \\mu + \\nu_2.rnDeriv \\mu. $$$$
Lean4
/-- Radon-Nikodym derivative of a sum of two measures.
See also `rnDeriv_add`, which has no hypothesis on `μ` but requires finite `ν₁` and `ν₂`. -/
theorem rnDeriv_add' (ν₁ ν₂ μ : Measure α) [SigmaFinite ν₁] [SigmaFinite ν₂] [SigmaFinite μ] :
(ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ :=
by
rw [← withDensity_eq_iff_of_sigmaFinite]
· suffices
(ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
(ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
by rwa [add_right_inj] at this
rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add, withDensity_add_left (measurable_rnDeriv _ _),
add_assoc, add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ), ←
ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]
· exact (measurable_rnDeriv _ _).aemeasurable
· exact ((measurable_rnDeriv _ _).add (measurable_rnDeriv _ _)).aemeasurable
