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

structure MeasureTheory.JordanDecomposition (α : Type u_2) [MeasurableSpace α] : Type u_2

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

• posPart : MeasureTheory.Measure α
• negPart : MeasureTheory.Measure α
• posPart_finite : MeasureTheory.IsFiniteMeasure self.posPart
• negPart_finite : MeasureTheory.IsFiniteMeasure self.negPart
• mutuallySingular : self.posPart.MutuallySingular self.negPart

theorem MeasureTheory.JordanDecomposition.ext {α : Type u_2} : ∀ {inst : MeasurableSpace α} {x y : MeasureTheory.JordanDecomposition α}, x.posPart = y.posPart → x.negPart = y.negPart → x = y

theorem MeasureTheory.JordanDecomposition.posPart_finite {α : Type u_2} [MeasurableSpace α] (self : MeasureTheory.JordanDecomposition α) : MeasureTheory.IsFiniteMeasure self.posPart

theorem MeasureTheory.JordanDecomposition.negPart_finite {α : Type u_2} [MeasurableSpace α] (self : MeasureTheory.JordanDecomposition α) : MeasureTheory.IsFiniteMeasure self.negPart

theorem MeasureTheory.JordanDecomposition.mutuallySingular {α : Type u_2} [MeasurableSpace α] (self : MeasureTheory.JordanDecomposition α) : self.posPart.MutuallySingular self.negPart

instance MeasureTheory.JordanDecomposition.instZero {α : Type u_1} [MeasurableSpace α] : Zero (MeasureTheory.JordanDecomposition α)

Equations

• MeasureTheory.JordanDecomposition.instZero = { zero := MeasureTheory.JordanDecomposition.mk 0 0 ⋯ }

instance MeasureTheory.JordanDecomposition.instInhabited {α : Type u_1} [MeasurableSpace α] : Inhabited (MeasureTheory.JordanDecomposition α)

Equations

• MeasureTheory.JordanDecomposition.instInhabited = { default := 0 }

instance MeasureTheory.JordanDecomposition.instInvolutiveNeg {α : Type u_1} [MeasurableSpace α] : InvolutiveNeg (MeasureTheory.JordanDecomposition α)

Equations

• MeasureTheory.JordanDecomposition.instInvolutiveNeg = InvolutiveNeg.mk ⋯

instance MeasureTheory.JordanDecomposition.instSMul {α : Type u_1} [MeasurableSpace α] : SMul NNReal (MeasureTheory.JordanDecomposition α)

Equations

• One or more equations did not get rendered due to their size.

instance MeasureTheory.JordanDecomposition.instSMulReal {α : Type u_1} [MeasurableSpace α] : SMul ℝ (MeasureTheory.JordanDecomposition α)

Equations

• MeasureTheory.JordanDecomposition.instSMulReal = { smul := fun (r : ℝ) (j : MeasureTheory.JordanDecomposition α) => if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j) }

@[simp]

theorem MeasureTheory.JordanDecomposition.zero_posPart {α : Type u_1} [MeasurableSpace α] : MeasureTheory.JordanDecomposition.posPart 0 = 0

@[simp]

theorem MeasureTheory.JordanDecomposition.zero_negPart {α : Type u_1} [MeasurableSpace α] : MeasureTheory.JordanDecomposition.negPart 0 = 0

@[simp]

theorem MeasureTheory.JordanDecomposition.neg_posPart {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) : (-j).posPart = j.negPart

@[simp]

theorem MeasureTheory.JordanDecomposition.neg_negPart {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) : (-j).negPart = j.posPart

@[simp]

theorem MeasureTheory.JordanDecomposition.smul_posPart {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : NNReal) : (r • j).posPart = r • j.posPart

@[simp]

theorem MeasureTheory.JordanDecomposition.smul_negPart {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : NNReal) : (r • j).negPart = r • j.negPart

theorem MeasureTheory.JordanDecomposition.real_smul_def {α : Type u_1} [MeasurableSpace α] (r : ℝ) (j : MeasureTheory.JordanDecomposition α) : r • j = if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)

@[simp]

theorem MeasureTheory.JordanDecomposition.coe_smul {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : NNReal) : ↑r • j = r • j

theorem MeasureTheory.JordanDecomposition.real_smul_nonneg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ℝ) (hr : 0 ≤ r) : r • j = r.toNNReal • j

theorem MeasureTheory.JordanDecomposition.real_smul_neg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ℝ) (hr : r < 0) : r • j = -((-r).toNNReal • j)

theorem MeasureTheory.JordanDecomposition.real_smul_posPart_nonneg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ℝ) (hr : 0 ≤ r) : (r • j).posPart = r.toNNReal • j.posPart

theorem MeasureTheory.JordanDecomposition.real_smul_negPart_nonneg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ℝ) (hr : 0 ≤ r) : (r • j).negPart = r.toNNReal • j.negPart

theorem MeasureTheory.JordanDecomposition.real_smul_posPart_neg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ℝ) (hr : r < 0) : (r • j).posPart = (-r).toNNReal • j.negPart

theorem MeasureTheory.JordanDecomposition.real_smul_negPart_neg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ℝ) (hr : r < 0) : (r • j).negPart = (-r).toNNReal • j.posPart

def MeasureTheory.JordanDecomposition.toSignedMeasure {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) : MeasureTheory.SignedMeasure α

The signed measure associated with a Jordan decomposition.

Equations

• j.toSignedMeasure = j.posPart.toSignedMeasure - j.negPart.toSignedMeasure

theorem MeasureTheory.JordanDecomposition.toSignedMeasure_zero {α : Type u_1} [MeasurableSpace α] : MeasureTheory.JordanDecomposition.toSignedMeasure 0 = 0

theorem MeasureTheory.JordanDecomposition.toSignedMeasure_neg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) : (-j).toSignedMeasure = -j.toSignedMeasure

theorem MeasureTheory.JordanDecomposition.toSignedMeasure_smul {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : NNReal) : (r • j).toSignedMeasure = r • j.toSignedMeasure

theorem MeasureTheory.JordanDecomposition.exists_compl_positive_negative {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) : ∃ (S : Set α), MeasurableSet S ∧ MeasureTheory.VectorMeasure.restrict j.toSignedMeasure S ≤ MeasureTheory.VectorMeasure.restrict 0 S ∧ MeasureTheory.VectorMeasure.restrict 0 Sᶜ ≤ MeasureTheory.VectorMeasure.restrict j.toSignedMeasure Sᶜ ∧ j.posPart S = 0 ∧ j.negPart Sᶜ = 0

A Jordan decomposition provides a Hahn decomposition.

def MeasureTheory.SignedMeasure.toJordanDecomposition {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) : MeasureTheory.JordanDecomposition α

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

• s.toJordanDecomposition = MeasureTheory.JordanDecomposition.mk (s.toMeasureOfZeroLE ⋯.choose ⋯ ⋯) (s.toMeasureOfLEZero ⋯.chooseᶜ ⋯ ⋯) ⋯

theorem MeasureTheory.SignedMeasure.toJordanDecomposition_spec {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) : ∃ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i) (hi₃ : MeasureTheory.VectorMeasure.restrict s iᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 iᶜ), s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧ s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃

@[simp]

theorem MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) : 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} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u : Set α} {v : Set α} {w : Set α} (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w) (hsu : MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u) (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} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u : Set α} {v : Set α} {w : Set α} (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w) (hsu : MeasureTheory.VectorMeasure.restrict s u ≤ MeasureTheory.VectorMeasure.restrict 0 u) (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} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u : Set α} {v : Set α} (hu : MeasurableSet u) (hv : MeasurableSet v) (hsu : MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u) (hsv : MeasureTheory.VectorMeasure.restrict 0 v ≤ MeasureTheory.VectorMeasure.restrict s v) (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} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u : Set α} {v : Set α} (hu : MeasurableSet u) (hv : MeasurableSet v) (hsu : MeasureTheory.VectorMeasure.restrict s u ≤ MeasureTheory.VectorMeasure.restrict 0 u) (hsv : MeasureTheory.VectorMeasure.restrict s v ≤ MeasureTheory.VectorMeasure.restrict 0 v) (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} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u : Set α} {v : Set α} {w : Set α} (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w) (hsu : MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u) (hsv : MeasureTheory.VectorMeasure.restrict 0 v ≤ MeasureTheory.VectorMeasure.restrict s v) (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} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u : Set α} {v : Set α} {w : Set α} (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w) (hsu : MeasureTheory.VectorMeasure.restrict s u ≤ MeasureTheory.VectorMeasure.restrict 0 u) (hsv : MeasureTheory.VectorMeasure.restrict s v ≤ MeasureTheory.VectorMeasure.restrict 0 v) (hs : ↑s (symmDiff u v) = 0) : ↑s (w ∩ u) = ↑s (w ∩ v)

theorem MeasureTheory.JordanDecomposition.toSignedMeasure_injective {α : Type u_1} [MeasurableSpace α] : Function.Injective MeasureTheory.JordanDecomposition.toSignedMeasure

The Jordan decomposition of a signed measure is unique.

@[simp]

theorem MeasureTheory.JordanDecomposition.toJordanDecomposition_toSignedMeasure {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) : j.toSignedMeasure.toJordanDecomposition = j

def MeasureTheory.SignedMeasure.toJordanDecompositionEquiv (α : Type u_2) [MeasurableSpace α] : MeasureTheory.SignedMeasure α ≃ MeasureTheory.JordanDecomposition α

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.SignedMeasure.toJordanDecompositionEquiv_symm_apply (α : Type u_2) [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) : (MeasureTheory.SignedMeasure.toJordanDecompositionEquiv α).symm j = j.toSignedMeasure

@[simp]

theorem MeasureTheory.SignedMeasure.toJordanDecompositionEquiv_apply (α : Type u_2) [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) : (MeasureTheory.SignedMeasure.toJordanDecompositionEquiv α) s = s.toJordanDecomposition

theorem MeasureTheory.SignedMeasure.toJordanDecomposition_zero {α : Type u_1} [MeasurableSpace α] : MeasureTheory.SignedMeasure.toJordanDecomposition 0 = 0

theorem MeasureTheory.SignedMeasure.toJordanDecomposition_neg {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) : (-s).toJordanDecomposition = -s.toJordanDecomposition

theorem MeasureTheory.SignedMeasure.toJordanDecomposition_smul {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (r : NNReal) : (r • s).toJordanDecomposition = r • s.toJordanDecomposition

theorem MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (r : ℝ) : (r • s).toJordanDecomposition = r • s.toJordanDecomposition

theorem MeasureTheory.SignedMeasure.toJordanDecomposition_eq {α : Type u_1} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {j : MeasureTheory.JordanDecomposition α} (h : s = j.toSignedMeasure) : s.toJordanDecomposition = j

def MeasureTheory.SignedMeasure.totalVariation {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) : MeasureTheory.Measure α

The total variation of a signed measure.

Equations

• s.totalVariation = s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart

theorem MeasureTheory.SignedMeasure.totalVariation_zero {α : Type u_1} [MeasurableSpace α] : MeasureTheory.SignedMeasure.totalVariation 0 = 0

theorem MeasureTheory.SignedMeasure.totalVariation_neg {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) : (-s).totalVariation = s.totalVariation

theorem MeasureTheory.SignedMeasure.null_of_totalVariation_zero {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) {i : Set α} (hs : s.totalVariation i = 0) : ↑s i = 0

theorem MeasureTheory.SignedMeasure.absolutelyContinuous_ennreal_iff {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.VectorMeasure α ENNReal) : MeasureTheory.VectorMeasure.AbsolutelyContinuous s μ ↔ s.totalVariation.AbsolutelyContinuous μ.ennrealToMeasure

theorem MeasureTheory.SignedMeasure.totalVariation_absolutelyContinuous_iff {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) : s.totalVariation.AbsolutelyContinuous μ ↔ s.toJordanDecomposition.posPart.AbsolutelyContinuous μ ∧ s.toJordanDecomposition.negPart.AbsolutelyContinuous μ

theorem MeasureTheory.SignedMeasure.mutuallySingular_iff {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (t : MeasureTheory.SignedMeasure α) : MeasureTheory.VectorMeasure.MutuallySingular s t ↔ s.totalVariation.MutuallySingular t.totalVariation

theorem MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.VectorMeasure α ENNReal) : MeasureTheory.VectorMeasure.MutuallySingular s μ ↔ s.totalVariation.MutuallySingular μ.ennrealToMeasure

theorem MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) : s.totalVariation.MutuallySingular μ ↔ s.toJordanDecomposition.posPart.MutuallySingular μ ∧ s.toJordanDecomposition.negPart.MutuallySingular μ