English
If t is mutually singular to μ.toENNRealVectorMeasure and f is measurable, then the sum t^{+} + μ.withDensityᵥ f and t^{-} + μ.withDensityᵥ (−f) are mutually singular.
Русский
Если t взаимно сингулярна с μ.toENNRealVectorMeasure и f измерима, то суммы t^{+} + μ.withDensityᵥ f и t^{-} + μ.withDensityᵥ (−f) взаимно сингулярны.
LaTeX
$$$\text{MutuallySingular }(t^{+} + μ.withDensityᵥ f,\ t^{-} + μ.withDensityᵥ (-f))$$$
Lean4
/-- **The Lebesgue Decomposition theorem between a signed measure and a measure**:
Given a signed measure `s` and a σ-finite measure `μ`, there exist a signed measure `t` and a
measurable and integrable function `f`, such that `t` is mutually singular with respect to `μ`
and `s = t + μ.withDensityᵥ f`. In this case `t = s.singularPart μ` and
`f = s.rnDeriv μ`. -/
theorem singularPart_add_withDensity_rnDeriv_eq [s.HaveLebesgueDecomposition μ] :
s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s :=
by
conv_rhs => rw [← toSignedMeasure_toJordanDecomposition s, JordanDecomposition.toSignedMeasure]
rw [singularPart, rnDeriv_def,
withDensityᵥ_sub' (integrable_toReal_of_lintegral_ne_top _ _) (integrable_toReal_of_lintegral_ne_top _ _),
withDensityᵥ_toReal, withDensityᵥ_toReal, sub_eq_add_neg, sub_eq_add_neg,
add_comm (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure, ← add_assoc,
add_assoc (-(s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure), ← toSignedMeasure_add, add_comm, ←
add_assoc, ← neg_add, ← toSignedMeasure_add, add_comm, ← sub_eq_add_neg]
· convert rfl
· exact s.toJordanDecomposition.posPart.haveLebesgueDecomposition_add μ
· rw [add_comm]
exact s.toJordanDecomposition.negPart.haveLebesgueDecomposition_add μ
all_goals
first
| exact (lintegral_rnDeriv_lt_top _ _).ne
| measurability
