totalVariation_mutuallySingular_iff

English

The total variation of s is mutually singular with μ if and only if the posPart and negPart of s’s Jordan decomposition are mutually singular with μ as well.

Русский

Полная вариация меры s взаимно-связана с μ тогда и только тогда, когда posPart и negPart разложения Йордана также взаимно-связаны с μ.

LaTeX

$$$$ s.totalVariation \perp_m μ \iff (s.toJordanDecomposition.posPart \perp_m μ) \land (s.toJordanDecomposition.negPart \perp_m μ). $$$$

Lean4

theorem totalVariation_mutuallySingular_iff (s : SignedMeasure α) (μ : Measure α) :
    s.totalVariation ⟂ₘ μ ↔ s.toJordanDecomposition.posPart ⟂ₘ μ ∧ s.toJordanDecomposition.negPart ⟂ₘ μ :=
  Measure.MutuallySingular.add_left_iff

Похожие утверждения