# Jordan decomposition #

This file proves the existence and uniqueness of the Jordan decomposition for signed measures. The Jordan decomposition theorem states that, given a signed measure s, there exists a unique pair of mutually singular measures μ and ν, such that s = μ - ν.

The Jordan decomposition theorem for measures is a corollary of the Hahn decomposition theorem and is useful for the Lebesgue decomposition theorem.

## Main definitions #

• MeasureTheory.JordanDecomposition: a Jordan decomposition of a measurable space is a pair of mutually singular finite measures. We say j is a Jordan decomposition of a signed measure s if s = j.posPart - j.negPart.
• MeasureTheory.SignedMeasure.toJordanDecomposition: the Jordan decomposition of a signed measure.
• MeasureTheory.SignedMeasure.toJordanDecompositionEquiv: is the Equiv between MeasureTheory.SignedMeasure and MeasureTheory.JordanDecomposition formed by MeasureTheory.SignedMeasure.toJordanDecomposition.

## Main results #

• MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition : the Jordan decomposition theorem.
• MeasureTheory.JordanDecomposition.toSignedMeasure_injective : the Jordan decomposition of a signed measure is unique.

## Tags #

Jordan decomposition theorem

theorem MeasureTheory.JordanDecomposition.ext {α : Type u_3} :
∀ {inst : } (x y : ), x.posPart = y.posPartx.negPart = y.negPartx = y
theorem MeasureTheory.JordanDecomposition.ext_iff {α : Type u_3} :
∀ {inst : } (x y : ), x = y x.posPart = y.posPart x.negPart = y.negPart
structure MeasureTheory.JordanDecomposition (α : Type u_3) [] :
Type u_3

A Jordan decomposition of a measurable space is a pair of mutually singular, finite measures.

Instances For
theorem MeasureTheory.JordanDecomposition.mutuallySingular {α : Type u_3} [] (self : ) :
self.posPart.MutuallySingular self.negPart
Equations
• MeasureTheory.JordanDecomposition.instZero = { zero := }
Equations
• MeasureTheory.JordanDecomposition.instInhabited = { default := 0 }
Equations
• MeasureTheory.JordanDecomposition.instInvolutiveNeg =
Equations
• One or more equations did not get rendered due to their size.
Equations
• MeasureTheory.JordanDecomposition.instSMulReal = { smul := fun (r : ) (j : ) => if 0 r then r.toNNReal j else -((-r).toNNReal j) }
@[simp]
theorem MeasureTheory.JordanDecomposition.neg_posPart {α : Type u_1} [] :
(-j).posPart = j.negPart
@[simp]
theorem MeasureTheory.JordanDecomposition.neg_negPart {α : Type u_1} [] :
(-j).negPart = j.posPart
@[simp]
theorem MeasureTheory.JordanDecomposition.smul_posPart {α : Type u_1} [] (r : NNReal) :
(r j).posPart = r j.posPart
@[simp]
theorem MeasureTheory.JordanDecomposition.smul_negPart {α : Type u_1} [] (r : NNReal) :
(r j).negPart = r j.negPart
theorem MeasureTheory.JordanDecomposition.real_smul_def {α : Type u_1} [] (r : ) :
r j = if 0 r then r.toNNReal j else -((-r).toNNReal j)
@[simp]
theorem MeasureTheory.JordanDecomposition.coe_smul {α : Type u_1} [] (r : NNReal) :
r j = r j
theorem MeasureTheory.JordanDecomposition.real_smul_nonneg {α : Type u_1} [] (r : ) (hr : 0 r) :
r j = r.toNNReal j
theorem MeasureTheory.JordanDecomposition.real_smul_neg {α : Type u_1} [] (r : ) (hr : r < 0) :
r j = -((-r).toNNReal j)
theorem MeasureTheory.JordanDecomposition.real_smul_posPart_nonneg {α : Type u_1} [] (r : ) (hr : 0 r) :
(r j).posPart = r.toNNReal j.posPart
theorem MeasureTheory.JordanDecomposition.real_smul_negPart_nonneg {α : Type u_1} [] (r : ) (hr : 0 r) :
(r j).negPart = r.toNNReal j.negPart
theorem MeasureTheory.JordanDecomposition.real_smul_posPart_neg {α : Type u_1} [] (r : ) (hr : r < 0) :
(r j).posPart = (-r).toNNReal j.negPart
theorem MeasureTheory.JordanDecomposition.real_smul_negPart_neg {α : Type u_1} [] (r : ) (hr : r < 0) :
(r j).negPart = (-r).toNNReal j.posPart

The signed measure associated with a Jordan decomposition.

Equations
• j.toSignedMeasure = j.posPart.toSignedMeasure - j.negPart.toSignedMeasure
Instances For
theorem MeasureTheory.JordanDecomposition.toSignedMeasure_neg {α : Type u_1} [] :
(-j).toSignedMeasure = -j.toSignedMeasure
theorem MeasureTheory.JordanDecomposition.toSignedMeasure_smul {α : Type u_1} [] (r : NNReal) :
(r j).toSignedMeasure = r j.toSignedMeasure
theorem MeasureTheory.JordanDecomposition.exists_compl_positive_negative {α : Type u_1} [] :
∃ (S : Set α), MeasureTheory.VectorMeasure.restrict j.toSignedMeasure S MeasureTheory.VectorMeasure.restrict j.toSignedMeasure S j.posPart S = 0 j.negPart S = 0

A Jordan decomposition provides a Hahn decomposition.

Given a signed measure s, s.toJordanDecomposition is the Jordan decomposition j, such that s = j.toSignedMeasure. This property is known as the Jordan decomposition theorem, and is shown by MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition.

Equations
Instances For
theorem MeasureTheory.SignedMeasure.toJordanDecomposition_spec {α : Type u_1} [] (s : ) :
∃ (i : Set α) (hi₁ : ) (hi₂ : ) (hi₃ : ), s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ s.toJordanDecomposition.negPart = s.toMeasureOfLEZero i hi₃
@[simp]
theorem MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition {α : Type u_1} [] (s : ) :
s.toJordanDecomposition.toSignedMeasure = s

The Jordan decomposition theorem: Given a signed measure s, there exists a pair of mutually singular measures μ and ν such that s = μ - ν. In this case, the measures μ and ν are given by s.toJordanDecomposition.posPart and s.toJordanDecomposition.negPart respectively.

Note that we use MeasureTheory.JordanDecomposition.toSignedMeasure to represent the signed measure corresponding to s.toJordanDecomposition.posPart - s.toJordanDecomposition.negPart.

theorem MeasureTheory.SignedMeasure.subset_positive_null_set {α : Type u_1} [] {s : } {u : Set α} {v : Set α} {w : Set α} (hu : ) (hv : ) (hw : ) (hw₁ : s w = 0) (hw₂ : w u) (hwt : v w) :
s v = 0

A subset v of a null-set w has zero measure if w is a subset of a positive set u.

theorem MeasureTheory.SignedMeasure.subset_negative_null_set {α : Type u_1} [] {s : } {u : Set α} {v : Set α} {w : Set α} (hu : ) (hv : ) (hw : ) (hw₁ : s w = 0) (hw₂ : w u) (hwt : v w) :
s v = 0

A subset v of a null-set w has zero measure if w is a subset of a negative set u.

theorem MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_positive {α : Type u_1} [] {s : } {u : Set α} {v : Set α} (hu : ) (hv : ) (hs : s (symmDiff u v) = 0) :
s (u \ v) = 0 s (v \ u) = 0

If the symmetric difference of two positive sets is a null-set, then so are the differences between the two sets.

theorem MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_negative {α : Type u_1} [] {s : } {u : Set α} {v : Set α} (hu : ) (hv : ) (hs : s (symmDiff u v) = 0) :
s (u \ v) = 0 s (v \ u) = 0

If the symmetric difference of two negative sets is a null-set, then so are the differences between the two sets.

theorem MeasureTheory.SignedMeasure.of_inter_eq_of_symmDiff_eq_zero_positive {α : Type u_1} [] {s : } {u : Set α} {v : Set α} {w : Set α} (hu : ) (hv : ) (hw : ) (hs : s (symmDiff u v) = 0) :
s (w u) = s (w v)
theorem MeasureTheory.SignedMeasure.of_inter_eq_of_symmDiff_eq_zero_negative {α : Type u_1} [] {s : } {u : Set α} {v : Set α} {w : Set α} (hu : ) (hv : ) (hw : ) (hs : s (symmDiff u v) = 0) :
s (w u) = s (w v)
theorem MeasureTheory.JordanDecomposition.toSignedMeasure_injective {α : Type u_1} [] :
Function.Injective MeasureTheory.JordanDecomposition.toSignedMeasure

The Jordan decomposition of a signed measure is unique.

@[simp]
theorem MeasureTheory.JordanDecomposition.toJordanDecomposition_toSignedMeasure {α : Type u_1} [] :
j.toSignedMeasure.toJordanDecomposition = j
@[simp]
theorem MeasureTheory.SignedMeasure.toJordanDecompositionEquiv_apply (α : Type u_3) [] (s : ) :
= s.toJordanDecomposition
@[simp]

MeasureTheory.SignedMeasure.toJordanDecomposition and MeasureTheory.JordanDecomposition.toSignedMeasure form an Equiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasureTheory.SignedMeasure.toJordanDecomposition_neg {α : Type u_1} [] (s : ) :
(-s).toJordanDecomposition = -s.toJordanDecomposition
theorem MeasureTheory.SignedMeasure.toJordanDecomposition_smul {α : Type u_1} [] (s : ) (r : NNReal) :
(r s).toJordanDecomposition = r s.toJordanDecomposition
theorem MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real {α : Type u_1} [] (s : ) (r : ) :
(r s).toJordanDecomposition = r s.toJordanDecomposition
theorem MeasureTheory.SignedMeasure.toJordanDecomposition_eq {α : Type u_1} [] {s : } (h : s = j.toSignedMeasure) :
s.toJordanDecomposition = j

The total variation of a signed measure.

Equations
• s.totalVariation = s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart
Instances For
theorem MeasureTheory.SignedMeasure.totalVariation_neg {α : Type u_1} [] (s : ) :
(-s).totalVariation = s.totalVariation
theorem MeasureTheory.SignedMeasure.null_of_totalVariation_zero {α : Type u_1} [] (s : ) {i : Set α} (hs : s.totalVariation i = 0) :
s i = 0
theorem MeasureTheory.SignedMeasure.absolutelyContinuous_ennreal_iff {α : Type u_1} [] (s : ) :
s.totalVariation.AbsolutelyContinuous μ.ennrealToMeasure
theorem MeasureTheory.SignedMeasure.totalVariation_absolutelyContinuous_iff {α : Type u_1} [] (s : ) (μ : ) :
s.totalVariation.AbsolutelyContinuous μ s.toJordanDecomposition.posPart.AbsolutelyContinuous μ s.toJordanDecomposition.negPart.AbsolutelyContinuous μ
theorem MeasureTheory.SignedMeasure.mutuallySingular_iff {α : Type u_1} [] (s : ) (t : ) :
s.totalVariation.MutuallySingular t.totalVariation
theorem MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff {α : Type u_1} [] (s : ) :
s.totalVariation.MutuallySingular μ.ennrealToMeasure
theorem MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff {α : Type u_1} [] (s : ) (μ : ) :
s.totalVariation.MutuallySingular μ s.toJordanDecomposition.posPart.MutuallySingular μ s.toJordanDecomposition.negPart.MutuallySingular μ