Documentation

Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

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 #

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

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

Equations
Instances For
    @[simp]

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