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 sayjis a Jordan decomposition of a signed measuresifs = j.posPart - j.negPart.MeasureTheory.SignedMeasure.toJordanDecomposition: the Jordan decomposition of a signed measure.MeasureTheory.SignedMeasure.toJordanDecompositionEquiv: is theEquivbetweenMeasureTheory.SignedMeasureandMeasureTheory.JordanDecompositionformed byMeasureTheory.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 : MeasurableSpace α} (x y : MeasureTheory.JordanDecomposition α),
x.posPart = y.posPart → x.negPart = y.negPart → x = y
theorem
MeasureTheory.JordanDecomposition.ext_iff
{α : Type u_3}
:
∀ {inst : MeasurableSpace α} (x y : MeasureTheory.JordanDecomposition α),
x = y ↔ x.posPart = y.posPart ∧ x.negPart = y.negPart
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 : MeasureTheory.Measure.MutuallySingular self.posPart self.negPart
Instances For
Equations
- MeasureTheory.JordanDecomposition.instZero = { zero := MeasureTheory.JordanDecomposition.mk 0 0 (_ : MeasureTheory.Measure.MutuallySingular 0 0) }
Equations
- MeasureTheory.JordanDecomposition.instInhabited = { default := 0 }
Equations
- MeasureTheory.JordanDecomposition.instInvolutiveNeg = InvolutiveNeg.mk (_ : ∀ (x : MeasureTheory.JordanDecomposition α), - -x = x)
Equations
- One or more equations did not get rendered due to their size.
Equations
- MeasureTheory.JordanDecomposition.instSMulReal = { smul := fun (r : ℝ) (j : MeasureTheory.JordanDecomposition α) => if 0 ≤ r then Real.toNNReal r • j else -(Real.toNNReal (-r) • j) }
@[simp]
theorem
MeasureTheory.JordanDecomposition.zero_posPart
{α : Type u_1}
[MeasurableSpace α]
:
0.posPart = 0
@[simp]
theorem
MeasureTheory.JordanDecomposition.zero_negPart
{α : Type u_1}
[MeasurableSpace α]
:
0.negPart = 0
@[simp]
theorem
MeasureTheory.JordanDecomposition.neg_posPart
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
:
@[simp]
theorem
MeasureTheory.JordanDecomposition.neg_negPart
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
:
@[simp]
theorem
MeasureTheory.JordanDecomposition.smul_posPart
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
(r : NNReal)
:
@[simp]
theorem
MeasureTheory.JordanDecomposition.smul_negPart
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
(r : NNReal)
:
theorem
MeasureTheory.JordanDecomposition.real_smul_def
{α : Type u_1}
[MeasurableSpace α]
(r : ℝ)
(j : MeasureTheory.JordanDecomposition α)
:
r • j = if 0 ≤ r then Real.toNNReal r • j else -(Real.toNNReal (-r) • j)
@[simp]
theorem
MeasureTheory.JordanDecomposition.coe_smul
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
(r : NNReal)
:
theorem
MeasureTheory.JordanDecomposition.real_smul_nonneg
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
(r : ℝ)
(hr : 0 ≤ r)
:
r • j = Real.toNNReal r • j
theorem
MeasureTheory.JordanDecomposition.real_smul_neg
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
(r : ℝ)
(hr : r < 0)
:
theorem
MeasureTheory.JordanDecomposition.real_smul_posPart_nonneg
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
(r : ℝ)
(hr : 0 ≤ r)
:
(r • j).posPart = Real.toNNReal r • j.posPart
theorem
MeasureTheory.JordanDecomposition.real_smul_negPart_nonneg
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
(r : ℝ)
(hr : 0 ≤ r)
:
(r • j).negPart = Real.toNNReal r • j.negPart
theorem
MeasureTheory.JordanDecomposition.real_smul_posPart_neg
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
(r : ℝ)
(hr : r < 0)
:
(r • j).posPart = Real.toNNReal (-r) • j.negPart
theorem
MeasureTheory.JordanDecomposition.real_smul_negPart_neg
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
(r : ℝ)
(hr : r < 0)
:
(r • j).negPart = Real.toNNReal (-r) • j.posPart
def
MeasureTheory.JordanDecomposition.toSignedMeasure
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
:
The signed measure associated with a Jordan decomposition.
Equations
Instances For
theorem
MeasureTheory.JordanDecomposition.toSignedMeasure_smul
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
(r : NNReal)
:
theorem
MeasureTheory.JordanDecomposition.exists_compl_positive_negative
{α : Type u_1}
[MeasurableSpace α]
(j : MeasureTheory.JordanDecomposition α)
:
∃ (S : Set α),
MeasurableSet S ∧ MeasureTheory.VectorMeasure.restrict (MeasureTheory.JordanDecomposition.toSignedMeasure j) S ≤ MeasureTheory.VectorMeasure.restrict 0 S ∧ MeasureTheory.VectorMeasure.restrict 0 Sᶜ ≤ MeasureTheory.VectorMeasure.restrict (MeasureTheory.JordanDecomposition.toSignedMeasure j) 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 α)
:
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
- One or more equations did not get rendered due to their size.
Instances For
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ᶜ),
(MeasureTheory.SignedMeasure.toJordanDecomposition s).posPart = MeasureTheory.SignedMeasure.toMeasureOfZeroLE s i hi₁ hi₂ ∧ (MeasureTheory.SignedMeasure.toJordanDecomposition s).negPart = MeasureTheory.SignedMeasure.toMeasureOfLEZero s iᶜ (_ : MeasurableSet iᶜ) hi₃
@[simp]
theorem
MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition
{α : Type u_1}
[MeasurableSpace α]
(s : MeasureTheory.SignedMeasure α)
:
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)
:
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)
:
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)
:
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)
:
theorem
MeasureTheory.JordanDecomposition.toSignedMeasure_injective
{α : Type u_1}
[MeasurableSpace α]
:
Function.Injective MeasureTheory.JordanDecomposition.toSignedMeasure
The Jordan decomposition of a signed measure is unique.
@[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_smul
{α : Type u_1}
[MeasurableSpace α]
(s : MeasureTheory.SignedMeasure α)
(r : NNReal)
:
theorem
MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real
{α : Type u_1}
[MeasurableSpace α]
(s : MeasureTheory.SignedMeasure α)
(r : ℝ)
:
theorem
MeasureTheory.SignedMeasure.toJordanDecomposition_eq
{α : Type u_1}
[MeasurableSpace α]
{s : MeasureTheory.SignedMeasure α}
{j : MeasureTheory.JordanDecomposition α}
(h : s = MeasureTheory.JordanDecomposition.toSignedMeasure j)
:
def
MeasureTheory.SignedMeasure.totalVariation
{α : Type u_1}
[MeasurableSpace α]
(s : MeasureTheory.SignedMeasure α)
:
The total variation of a signed measure.
Equations
Instances For
theorem
MeasureTheory.SignedMeasure.null_of_totalVariation_zero
{α : Type u_1}
[MeasurableSpace α]
(s : MeasureTheory.SignedMeasure α)
{i : Set α}
(hs : ↑↑(MeasureTheory.SignedMeasure.totalVariation s) i = 0)
:
↑s i = 0
theorem
MeasureTheory.SignedMeasure.absolutelyContinuous_ennreal_iff
{α : Type u_1}
[MeasurableSpace α]
(s : MeasureTheory.SignedMeasure α)
(μ : MeasureTheory.VectorMeasure α ENNReal)
:
theorem
MeasureTheory.SignedMeasure.totalVariation_absolutelyContinuous_iff
{α : Type u_1}
[MeasurableSpace α]
(s : MeasureTheory.SignedMeasure α)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.Measure.AbsolutelyContinuous (MeasureTheory.SignedMeasure.totalVariation s) μ ↔ MeasureTheory.Measure.AbsolutelyContinuous (MeasureTheory.SignedMeasure.toJordanDecomposition s).posPart μ ∧ MeasureTheory.Measure.AbsolutelyContinuous (MeasureTheory.SignedMeasure.toJordanDecomposition s).negPart μ
theorem
MeasureTheory.SignedMeasure.mutuallySingular_iff
{α : Type u_1}
[MeasurableSpace α]
(s : MeasureTheory.SignedMeasure α)
(t : MeasureTheory.SignedMeasure α)
:
theorem
MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff
{α : Type u_1}
[MeasurableSpace α]
(s : MeasureTheory.SignedMeasure α)
(μ : MeasureTheory.VectorMeasure α ENNReal)
:
theorem
MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff
{α : Type u_1}
[MeasurableSpace α]
(s : MeasureTheory.SignedMeasure α)
(μ : MeasureTheory.Measure α)
: