English
For a complex measure c and μ with Lebesgue decompositions, the sum of the singular part and the density part equals c.
Русский
Для комплексной меры c и μ с разложением Лебега сумма сингулярной части и плотности равна c.
LaTeX
$$$ c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c $$$
Lean4
theorem singularPart_add_withDensity_rnDeriv_eq [c.HaveLebesgueDecomposition μ] :
c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c :=
by
conv_rhs => rw [← c.toComplexMeasure_to_signedMeasure]
ext i hi : 1
rw [VectorMeasure.add_apply, SignedMeasure.toComplexMeasure_apply]
apply Complex.ext
· rw [Complex.add_re, withDensityᵥ_apply (c.integrable_rnDeriv μ) hi, ← RCLike.re_eq_complex_re, ←
integral_re (c.integrable_rnDeriv μ).integrableOn, RCLike.re_eq_complex_re, ← withDensityᵥ_apply _ hi]
· change (c.re.singularPart μ + μ.withDensityᵥ (c.re.rnDeriv μ)) i = _
rw [c.re.singularPart_add_withDensity_rnDeriv_eq μ]
· exact SignedMeasure.integrable_rnDeriv _ _
· rw [Complex.add_im, withDensityᵥ_apply (c.integrable_rnDeriv μ) hi, ← RCLike.im_eq_complex_im, ←
integral_im (c.integrable_rnDeriv μ).integrableOn, RCLike.im_eq_complex_im, ← withDensityᵥ_apply _ hi]
· change (c.im.singularPart μ + μ.withDensityᵥ (c.im.rnDeriv μ)) i = _
rw [c.im.singularPart_add_withDensity_rnDeriv_eq μ]
· exact SignedMeasure.integrable_rnDeriv _ _
