Jordan decomposition from signed measure subtraction

This file develops the Jordan decomposition of the signed measure μ - ν for finite measures μ and ν, expressing it as the pair (μ - ν, ν - μ) of mutually singular finite measures.

The key tool is the Hahn decomposition theorem, which yields a measurable partition of the space where μ ≤ ν and ν ≤ μ, and the measure difference behaves like a signed measure difference.

Main results

• toJordanDecomposition_toSignedMeasure_sub: The Jordan decomposition of μ.toSignedMeasure - ν.toSignedMeasure is given by (μ - ν, ν - μ). It relies on the following intermediate results.
• mutually_singular_measure_sub: The measures μ - ν and ν - μ are mutually singular.
• sub_toSignedMeasure_eq_toSignedMeasure_sub: The signed measure μ.toSignedMeasure - ν.toSignedMeasure equals (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure.

theorem MeasureTheory.Measure.sub_apply_eq_zero_of_isHahnDecomposition {X : Type u_1} {mX : MeasurableSpace X} {s : Set X} {μ ν : Measure X} (hs : IsHahnDecomposition μ ν s) : (μ - ν) s = 0

theorem MeasureTheory.Measure.mutually_singular_measure_sub {X : Type u_1} {mX : MeasurableSpace X} {μ ν : Measure X} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : (μ - ν).MutuallySingular (ν - μ)

theorem MeasureTheory.Measure.toSignedMeasure_restrict_sub {X : Type u_1} {mX : MeasurableSpace X} {s : Set X} {μ ν : Measure X} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hs : IsHahnDecomposition μ ν s) : ((ν - μ).restrict s).toSignedMeasure = VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s

theorem MeasureTheory.Measure.sub_toSignedMeasure_eq_toSignedMeasure_sub {X : Type u_1} {mX : MeasurableSpace X} {μ ν : Measure X} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure

noncomputable def MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub {X : Type u_1} {mX : MeasurableSpace X} (μ ν : Measure X) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : JordanDecomposition X

The Jordan decomposition associated to the pair of mutually singular measures μ - ν and ν - μ.

Equations

• μ.jordanDecompositionOfToSignedMeasureSub ν = { posPart := μ - ν, negPart := ν - μ, posPart_finite := ⋯, negPart_finite := ⋯, mutuallySingular := ⋯ }

theorem MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_posPart {X : Type u_1} {mX : MeasurableSpace X} {μ ν : Measure X} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : (μ.jordanDecompositionOfToSignedMeasureSub ν).posPart = μ - ν

theorem MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_negPart {X : Type u_1} {mX : MeasurableSpace X} {μ ν : Measure X} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : (μ.jordanDecompositionOfToSignedMeasureSub ν).negPart = ν - μ

theorem MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_toSignedMeasure {X : Type u_1} {mX : MeasurableSpace X} {μ ν : Measure X} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure = μ.toSignedMeasure - ν.toSignedMeasure

@[simp]

theorem MeasureTheory.Measure.toJordanDecomposition_toSignedMeasure_sub {X : Type u_1} {mX : MeasurableSpace X} {μ ν : Measure X} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition = μ.jordanDecompositionOfToSignedMeasureSub ν

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