mutuallySingular_singularPart — Mathlib

English

The Jordan decomposition of the signed measure associated to the subtracted signed measures equals the Jordan decomposition of the sub.

Русский

Джорданово разложение для знаковой меры, связанной с разностью, совпадает с разложением для вычитания.

LaTeX

$$$(\text{jordanDecompositionOfToSignedMeasureSub} \mu \nu).toSignedMeasure = \mu.toSignedMeasure - \nu.toSignedMeasure$$$

Lean4

nonrec theorem mutuallySingular_singularPart (s : SignedMeasure α) (μ : Measure α) :
    singularPart s μ ⟂ᵥ μ.toENNRealVectorMeasure :=
  by
  rw [mutuallySingular_ennreal_iff, singularPart_totalVariation, VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure]
  exact (mutuallySingular_singularPart _ _).add_left (mutuallySingular_singularPart _ _)

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