English
If t is a candidate in a Lebesgue decomposition with respect to μ and f is a density, then t equals the singular part of s with respect to μ when s = t + μ.withDensityᵥ f.
Русский
Если t — кандидат на разложение Лебега относительно μ и имеется плотность f, то при s = t + μ.withDensityᵥ f, t равно сингулярной части s по μ.
LaTeX
$$$t = s.singularPart μ$ given $s = t + μ.withDensityᵥ f$ and htμ mutually singular$$
Lean4
/-- Given a measure `μ`, signed measures `s` and `t`, and a function `f` such that `t` is
mutually singular with respect to `μ` and `s = t + μ.withDensityᵥ f`, we have
`t = singularPart s μ`, i.e. `t` is the singular part of the Lebesgue decomposition between
`s` and `μ`. -/
theorem eq_singularPart (t : SignedMeasure α) (f : α → ℝ) (htμ : t ⟂ᵥ μ.toENNRealVectorMeasure)
(hadd : s = t + μ.withDensityᵥ f) : t = s.singularPart μ :=
by
by_cases hfi : Integrable f μ
· refine eq_singularPart' t hfi.1.measurable_mk (hfi.congr hfi.1.ae_eq_mk) htμ ?_
convert hadd using 2
exact WithDensityᵥEq.congr_ae hfi.1.ae_eq_mk.symm
· rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd
refine eq_singularPart' t measurable_zero (integrable_zero _ _ μ) htμ ?_
rwa [withDensityᵥ_zero, add_zero]
