English
Let s and t be signed measures with Lebesgue decomposition with respect to μ. Then the singular part of their sum equals the sum of their singular parts.
Русский
Пусть s и t — знаковые меры, имеющие разложение Лебега по отношению к μ. Тогда сингулярная часть суммы равна сумме сингулярных частей.
LaTeX
$$$ (s + t).singularPart \\mu = s.singularPart \\mu + t.singularPart \\mu $$$
Lean4
theorem singularPart_add (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ]
[t.HaveLebesgueDecomposition μ] : (s + t).singularPart μ = s.singularPart μ + t.singularPart μ :=
by
refine
(eq_singularPart _ (s.rnDeriv μ + t.rnDeriv μ)
((mutuallySingular_singularPart s μ).add_left (mutuallySingular_singularPart t μ)) ?_).symm
rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), add_assoc, add_comm (t.singularPart μ),
add_assoc, add_comm _ (t.singularPart μ), singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
singularPart_add_withDensity_rnDeriv_eq]
