Theorems · Theorem · measure theory

MeasureTheory.Measure.toJordanDecomposition_toSignedMeasure_sub

∀ {X : Type u_1} {mX : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν],
  (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition = μ.jordanDecompositionOfToSignedMeasureSub ν

The Jordan decomposition of μ.toSignedMeasure - ν.toSignedMeasure is (μ - ν, ν - μ).

Defined in

Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

Cited by

0 results in Mathlib

Foundations

Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure