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)
:
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 ν]
:
def
MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub
{X : Type u_1}
{mX : MeasurableSpace X}
(μ ν : Measure X)
[IsFiniteMeasure μ]
[IsFiniteMeasure ν]
:
The Jordan decomposition associated to the pair of mutually singular measures μ - ν
and ν - μ
.
Equations
Instances For
theorem
MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_posPart
{X : Type u_1}
{mX : MeasurableSpace X}
{μ ν : Measure X}
[IsFiniteMeasure μ]
[IsFiniteMeasure ν]
:
theorem
MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_negPart
{X : Type u_1}
{mX : MeasurableSpace X}
{μ ν : Measure X}
[IsFiniteMeasure μ]
[IsFiniteMeasure ν]
:
theorem
MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_toSignedMeasure
{X : Type u_1}
{mX : MeasurableSpace X}
{μ ν : Measure X}
[IsFiniteMeasure μ]
[IsFiniteMeasure ν]
:
@[simp]
theorem
MeasureTheory.Measure.toJordanDecomposition_toSignedMeasure_sub
{X : Type u_1}
{mX : MeasurableSpace X}
{μ ν : Measure X}
[IsFiniteMeasure μ]
[IsFiniteMeasure ν]
:
The Jordan decomposition of μ.toSignedMeasure - ν.toSignedMeasure
is (μ - ν, ν - μ)
.