English
For signed measures s and t with Lebesgue decompositions relative to μ, the RN-derivative of s + t equals the sum of RN-derivatives almost everywhere.
Русский
Для знаковых мер s и t с разложением Лебега по отношению к μ, производная RN от s + t равна сумме RN-дериватов почти наверняка.
LaTeX
$$$ (s + t).rnDeriv \\mu =^{{\\mu}}_{a.e.} s.rnDeriv \\mu + t.rnDeriv \\mu $$$
Lean4
theorem rnDeriv_add (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ]
[t.HaveLebesgueDecomposition μ] [(s + t).HaveLebesgueDecomposition μ] :
(s + t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ + t.rnDeriv μ :=
by
refine
Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) ((integrable_rnDeriv _ _).add (integrable_rnDeriv _ _))
?_
rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add, add_assoc,
add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ), singularPart_add_withDensity_rnDeriv_eq, ←
add_assoc, singularPart_add_withDensity_rnDeriv_eq]
