English
The singular part is additive in the left argument: (μ1 + μ2).singularPart ν = μ1.singularPart ν + μ2.singularPart ν, when μ1, μ2 have Lebesgue decompositions w.r.t ν.
Русский
Сингулярная часть аддитивна по левому аргументу: (μ1 + μ2).singularPart ν = μ1.singularPart ν + μ2.singularPart ν, если μ1, μ2 имеют разложения по ν.
LaTeX
$$$ (μ_1 + μ_2).singularPart ν = μ_1.singularPart ν + μ_2.singularPart ν $$$
Lean4
theorem singularPart_add (μ₁ μ₂ ν : Measure α) [HaveLebesgueDecomposition μ₁ ν] [HaveLebesgueDecomposition μ₂ ν] :
(μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν :=
by
refine
(eq_singularPart ((measurable_rnDeriv μ₁ ν).add (measurable_rnDeriv μ₂ ν))
((mutuallySingular_singularPart _ _).add_left (mutuallySingular_singularPart _ _)) ?_).symm
rw [← Pi.add_def, withDensity_add_left (measurable_rnDeriv μ₁ ν)]
conv_rhs => rw [add_assoc, add_comm (μ₂.singularPart ν), ← add_assoc, ← add_assoc]
rw [← haveLebesgueDecomposition_add μ₁ ν, add_assoc, add_comm (ν.withDensity (μ₂.rnDeriv ν)), ←
haveLebesgueDecomposition_add μ₂ ν]
