English
If f is measurable and htμ holds that t is mutually singular to μ.toENNRealVectorMeasure, then the sum t^{+} + μ.withDensityᵥ (ofReal f) is mutually singular to t^{-} + μ.withDensityᵥ (ofReal (-f)).
Русский
Если f измерим и htμ: t взаимно сингулярна с μ.toENNRealVectorMeasure, то суммы t^{+} + μ.withDensityᵥ( f ) и t^{-} + μ.withDensityᵥ(−f) взаимно сингулярны.
LaTeX
$$$\text{MutuallySingular }\bigl(t^{+} + μ.withDensity\; (f),\ t^{-} + μ.withDensity\; (-f)\bigr)$$$
Lean4
theorem jordanDecomposition_add_withDensity_mutuallySingular {f : α → ℝ} (hf : Measurable f)
(htμ : t ⟂ᵥ μ.toENNRealVectorMeasure) :
(t.toJordanDecomposition.posPart + μ.withDensity fun x : α => ENNReal.ofReal (f x)) ⟂ₘ
t.toJordanDecomposition.negPart + μ.withDensity fun x : α => ENNReal.ofReal (-f x) :=
by
rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff,
VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure] at htμ
exact
((JordanDecomposition.mutuallySingular _).add_right
(htμ.1.mono_ac (refl _) (withDensity_absolutelyContinuous _ _))).add_left
((htμ.2.symm.mono_ac (withDensity_absolutelyContinuous _ _) (refl _)).add_right
(withDensity_ofReal_mutuallySingular hf))
