# Documentation

Mathlib.MeasureTheory.Decomposition.Jordan

# 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
@[simp]
theorem MeasureTheory.JordanDecomposition.zero_posPart {α : Type u_1} [] :
0.posPart = 0
@[simp]
theorem MeasureTheory.JordanDecomposition.zero_negPart {α : Type u_1} [] :
0.negPart = 0
@[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 else -( 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 =
theorem MeasureTheory.JordanDecomposition.real_smul_neg {α : Type u_1} [] (r : ) (hr : r < 0) :
r j = -( j)
theorem MeasureTheory.JordanDecomposition.real_smul_posPart_nonneg {α : Type u_1} [] (r : ) (hr : 0 r) :
(r j).posPart = j.posPart
theorem MeasureTheory.JordanDecomposition.real_smul_negPart_nonneg {α : Type u_1} [] (r : ) (hr : 0 r) :
(r j).negPart = j.negPart
theorem MeasureTheory.JordanDecomposition.real_smul_posPart_neg {α : Type u_1} [] (r : ) (hr : r < 0) :
(r j).posPart = j.negPart
theorem MeasureTheory.JordanDecomposition.real_smul_negPart_neg {α : Type u_1} [] (r : ) (hr : r < 0) :
(r j).negPart = j.posPart

The signed measure associated with a Jordan decomposition.

Instances For
theorem MeasureTheory.JordanDecomposition.exists_compl_positive_negative {α : Type u_1} [] :
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.

Instances For
theorem MeasureTheory.SignedMeasure.toJordanDecomposition_spec {α : Type u_1} [] (s : ) :
i hi₁ hi₂ hi₃, = =
@[simp]

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 (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 (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 (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 (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]
@[simp]

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

Instances For

The total variation of a signed measure.

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