mathlib3 documentation

measure_theory.decomposition.jordan

Jordan decomposition #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

measure_theory.jordan_decomposition: 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.pos_part - j.neg_part.
measure_theory.signed_measure.to_jordan_decomposition: the Jordan decomposition of a signed measure.
measure_theory.signed_measure.to_jordan_decomposition_equiv: is the equiv between measure_theory.signed_measure and measure_theory.jordan_decomposition formed by measure_theory.signed_measure.to_jordan_decomposition.

Main results #

measure_theory.signed_measure.to_signed_measure_to_jordan_decomposition : the Jordan decomposition theorem.
measure_theory.jordan_decomposition.to_signed_measure_injective : the Jordan decomposition of a signed measure is unique.

Tags #

Jordan decomposition theorem

theorem measure_theory.jordan_decomposition.ext_iff {α : Type u_3} {_inst_2 : measurable_space α} (x y : measure_theory.jordan_decomposition α) :

x = y ↔ x.pos_part = y.pos_part ∧ x.neg_part = y.neg_part

@[ext]

structure measure_theory.jordan_decomposition (α : Type u_3) [measurable_space α] :

Type u_3

pos_part : measure_theory.measure α
neg_part : measure_theory.measure α
pos_part_finite : measure_theory.is_finite_measure self.pos_part
neg_part_finite : measure_theory.is_finite_measure self.neg_part
mutually_singular : self.pos_part.mutually_singular self.neg_part

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

Instances for measure_theory.jordan_decomposition

measure_theory.jordan_decomposition.has_sizeof_inst
measure_theory.jordan_decomposition.has_zero
measure_theory.jordan_decomposition.inhabited
measure_theory.jordan_decomposition.has_involutive_neg
measure_theory.jordan_decomposition.has_smul
measure_theory.jordan_decomposition.has_smul_real

theorem measure_theory.jordan_decomposition.ext {α : Type u_3} {_inst_2 : measurable_space α} (x y : measure_theory.jordan_decomposition α) (h : x.pos_part = y.pos_part) (h_1 : x.neg_part = y.neg_part) :

x = y

@[protected, instance]

def measure_theory.jordan_decomposition.has_zero {α : Type u_1} [measurable_space α] :

has_zero (measure_theory.jordan_decomposition α)

Equations

measure_theory.jordan_decomposition.has_zero = {zero := {pos_part := 0, neg_part := 0, pos_part_finite := _, neg_part_finite := _, mutually_singular := _}}

@[protected, instance]

def measure_theory.jordan_decomposition.inhabited {α : Type u_1} [measurable_space α] :

inhabited (measure_theory.jordan_decomposition α)

Equations

measure_theory.jordan_decomposition.inhabited = {default := 0}

@[protected, instance]

def measure_theory.jordan_decomposition.has_involutive_neg {α : Type u_1} [measurable_space α] :

has_involutive_neg (measure_theory.jordan_decomposition α)

Equations

measure_theory.jordan_decomposition.has_involutive_neg = {neg := λ (j : measure_theory.jordan_decomposition α), {pos_part := j.neg_part, neg_part := j.pos_part, pos_part_finite := _, neg_part_finite := _, mutually_singular := _}, neg_neg := _}

@[protected, instance]

noncomputable def measure_theory.jordan_decomposition.has_smul {α : Type u_1} [measurable_space α] :

has_smul nnreal (measure_theory.jordan_decomposition α)

Equations

measure_theory.jordan_decomposition.has_smul = {smul := λ (r : nnreal) (j : measure_theory.jordan_decomposition α), {pos_part := r • j.pos_part, neg_part := r • j.neg_part, pos_part_finite := _, neg_part_finite := _, mutually_singular := _}}

@[protected, instance]

noncomputable def measure_theory.jordan_decomposition.has_smul_real {α : Type u_1} [measurable_space α] :

has_smul ℝ (measure_theory.jordan_decomposition α)

Equations

measure_theory.jordan_decomposition.has_smul_real = {smul := λ (r : ℝ) (j : measure_theory.jordan_decomposition α), dite (0 ≤ r) (λ (hr : 0 ≤ r), r.to_nnreal • j) (λ (hr : ¬0 ≤ r), -((-r).to_nnreal • j))}

@[simp]

theorem measure_theory.jordan_decomposition.zero_pos_part {α : Type u_1} [measurable_space α] :

@[simp]

theorem measure_theory.jordan_decomposition.zero_neg_part {α : Type u_1} [measurable_space α] :

@[simp]

theorem measure_theory.jordan_decomposition.neg_pos_part {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) :

(-j).pos_part = j.neg_part

@[simp]

theorem measure_theory.jordan_decomposition.neg_neg_part {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) :

(-j).neg_part = j.pos_part

@[simp]

theorem measure_theory.jordan_decomposition.smul_pos_part {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) (r : nnreal) :

(r • j).pos_part = r • j.pos_part

@[simp]

theorem measure_theory.jordan_decomposition.smul_neg_part {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) (r : nnreal) :

(r • j).neg_part = r • j.neg_part

theorem measure_theory.jordan_decomposition.real_smul_def {α : Type u_1} [measurable_space α] (r : ℝ) (j : measure_theory.jordan_decomposition α) :

r • j = dite (0 ≤ r) (λ (hr : 0 ≤ r), r.to_nnreal • j) (λ (hr : ¬0 ≤ r), -((-r).to_nnreal • j))

@[simp]

theorem measure_theory.jordan_decomposition.coe_smul {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) (r : nnreal) :

↑r • j = r • j

theorem measure_theory.jordan_decomposition.real_smul_nonneg {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) (r : ℝ) (hr : 0 ≤ r) :

r • j = r.to_nnreal • j

theorem measure_theory.jordan_decomposition.real_smul_neg {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) (r : ℝ) (hr : r < 0) :

r • j = -((-r).to_nnreal • j)

theorem measure_theory.jordan_decomposition.real_smul_pos_part_nonneg {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) (r : ℝ) (hr : 0 ≤ r) :

(r • j).pos_part = r.to_nnreal • j.pos_part

theorem measure_theory.jordan_decomposition.real_smul_neg_part_nonneg {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) (r : ℝ) (hr : 0 ≤ r) :

(r • j).neg_part = r.to_nnreal • j.neg_part

theorem measure_theory.jordan_decomposition.real_smul_pos_part_neg {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) (r : ℝ) (hr : r < 0) :

(r • j).pos_part = (-r).to_nnreal • j.neg_part

theorem measure_theory.jordan_decomposition.real_smul_neg_part_neg {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) (r : ℝ) (hr : r < 0) :

(r • j).neg_part = (-r).to_nnreal • j.pos_part

noncomputable def measure_theory.jordan_decomposition.to_signed_measure {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) :

measure_theory.signed_measure α

The signed measure associated with a Jordan decomposition.

Equations

j.to_signed_measure = j.pos_part.to_signed_measure - j.neg_part.to_signed_measure

theorem measure_theory.jordan_decomposition.to_signed_measure_zero {α : Type u_1} [measurable_space α] :

0.to_signed_measure = 0

theorem measure_theory.jordan_decomposition.to_signed_measure_neg {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) :

(-j).to_signed_measure = -j.to_signed_measure

theorem measure_theory.jordan_decomposition.to_signed_measure_smul {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) (r : nnreal) :

(r • j).to_signed_measure = r • j.to_signed_measure

theorem measure_theory.jordan_decomposition.exists_compl_positive_negative {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) :

∃ (S : set α), measurable_set S ∧ measure_theory.vector_measure.restrict j.to_signed_measure S ≤ 0.restrict S ∧ 0.restrict Sᶜ ≤ measure_theory.vector_measure.restrict j.to_signed_measure Sᶜ ∧ ⇑(j.pos_part) S = 0 ∧ ⇑(j.neg_part) Sᶜ = 0

A Jordan decomposition provides a Hahn decomposition.

noncomputable def measure_theory.signed_measure.to_jordan_decomposition {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) :

measure_theory.jordan_decomposition α

Given a signed measure s, s.to_jordan_decomposition is the Jordan decomposition j, such that s = j.to_signed_measure. This property is known as the Jordan decomposition theorem, and is shown by measure_theory.signed_measure.to_signed_measure_to_jordan_decomposition.

Equations

s.to_jordan_decomposition = let i : set α := classical.some _, hi : measurable_set (classical.some _) ∧ 0.restrict (classical.some _) ≤ measure_theory.vector_measure.restrict s (classical.some _) ∧ measure_theory.vector_measure.restrict s (classical.some _)ᶜ ≤ 0.restrict (classical.some _)ᶜ := _ in {pos_part := s.to_measure_of_zero_le i _ _, neg_part := s.to_measure_of_le_zero iᶜ _ _, pos_part_finite := _, neg_part_finite := _, mutually_singular := _}

theorem measure_theory.signed_measure.to_jordan_decomposition_spec {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) :

∃ (i : set α) (hi₁ : measurable_set i) (hi₂ : 0.restrict i ≤ measure_theory.vector_measure.restrict s i) (hi₃ : measure_theory.vector_measure.restrict s iᶜ ≤ 0.restrict iᶜ), s.to_jordan_decomposition.pos_part = s.to_measure_of_zero_le i hi₁ hi₂ ∧ s.to_jordan_decomposition.neg_part = s.to_measure_of_le_zero iᶜ _ hi₃

@[simp]

theorem measure_theory.signed_measure.to_signed_measure_to_jordan_decomposition {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) :

s.to_jordan_decomposition.to_signed_measure = 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.to_jordan_decomposition.pos_part and s.to_jordan_decomposition.neg_part respectively.

Note that we use measure_theory.jordan_decomposition.to_signed_measure to represent the signed measure corresponding to s.to_jordan_decomposition.pos_part - s.to_jordan_decomposition.neg_part.

theorem measure_theory.signed_measure.subset_positive_null_set {α : Type u_1} [measurable_space α] {s : measure_theory.signed_measure α} {u v w : set α} (hu : measurable_set u) (hv : measurable_set v) (hw : measurable_set w) (hsu : 0.restrict u ≤ measure_theory.vector_measure.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 measure_theory.signed_measure.subset_negative_null_set {α : Type u_1} [measurable_space α] {s : measure_theory.signed_measure α} {u v w : set α} (hu : measurable_set u) (hv : measurable_set v) (hw : measurable_set w) (hsu : measure_theory.vector_measure.restrict s u ≤ 0.restrict 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 measure_theory.signed_measure.of_diff_eq_zero_of_symm_diff_eq_zero_positive {α : Type u_1} [measurable_space α] {s : measure_theory.signed_measure α} {u v : set α} (hu : measurable_set u) (hv : measurable_set v) (hsu : 0.restrict u ≤ measure_theory.vector_measure.restrict s u) (hsv : 0.restrict v ≤ measure_theory.vector_measure.restrict s v) (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 measure_theory.signed_measure.of_diff_eq_zero_of_symm_diff_eq_zero_negative {α : Type u_1} [measurable_space α] {s : measure_theory.signed_measure α} {u v : set α} (hu : measurable_set u) (hv : measurable_set v) (hsu : measure_theory.vector_measure.restrict s u ≤ 0.restrict u) (hsv : measure_theory.vector_measure.restrict s v ≤ 0.restrict v) (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 measure_theory.signed_measure.of_inter_eq_of_symm_diff_eq_zero_positive {α : Type u_1} [measurable_space α] {s : measure_theory.signed_measure α} {u v w : set α} (hu : measurable_set u) (hv : measurable_set v) (hw : measurable_set w) (hsu : 0.restrict u ≤ measure_theory.vector_measure.restrict s u) (hsv : 0.restrict v ≤ measure_theory.vector_measure.restrict s v) (hs : ⇑s (u ∆ v) = 0) :

⇑s (w ∩ u) = ⇑s (w ∩ v)

theorem measure_theory.signed_measure.of_inter_eq_of_symm_diff_eq_zero_negative {α : Type u_1} [measurable_space α] {s : measure_theory.signed_measure α} {u v w : set α} (hu : measurable_set u) (hv : measurable_set v) (hw : measurable_set w) (hsu : measure_theory.vector_measure.restrict s u ≤ 0.restrict u) (hsv : measure_theory.vector_measure.restrict s v ≤ 0.restrict v) (hs : ⇑s (u ∆ v) = 0) :

⇑s (w ∩ u) = ⇑s (w ∩ v)

theorem measure_theory.jordan_decomposition.to_signed_measure_injective {α : Type u_1} [measurable_space α] :

function.injective measure_theory.jordan_decomposition.to_signed_measure

The Jordan decomposition of a signed measure is unique.

@[simp]

theorem measure_theory.jordan_decomposition.to_jordan_decomposition_to_signed_measure {α : Type u_1} [measurable_space α] (j : measure_theory.jordan_decomposition α) :

j.to_signed_measure.to_jordan_decomposition = j

@[simp]

theorem measure_theory.signed_measure.to_jordan_decomposition_equiv_apply (α : Type u_1) [measurable_space α] (s : measure_theory.signed_measure α) :

⇑(measure_theory.signed_measure.to_jordan_decomposition_equiv α) s = s.to_jordan_decomposition

noncomputable def measure_theory.signed_measure.to_jordan_decomposition_equiv (α : Type u_1) [measurable_space α] :

measure_theory.signed_measure α ≃ measure_theory.jordan_decomposition α

measure_theory.signed_measure.to_jordan_decomposition and measure_theory.jordan_decomposition.to_signed_measure form a equiv.

Equations

measure_theory.signed_measure.to_jordan_decomposition_equiv α = {to_fun := measure_theory.signed_measure.to_jordan_decomposition _inst_2, inv_fun := measure_theory.jordan_decomposition.to_signed_measure _inst_2, left_inv := _, right_inv := _}

@[simp]

theorem measure_theory.signed_measure.to_jordan_decomposition_equiv_symm_apply (α : Type u_1) [measurable_space α] (j : measure_theory.jordan_decomposition α) :

⇑((measure_theory.signed_measure.to_jordan_decomposition_equiv α).symm) j = j.to_signed_measure

theorem measure_theory.signed_measure.to_jordan_decomposition_zero {α : Type u_1} [measurable_space α] :

0.to_jordan_decomposition = 0

theorem measure_theory.signed_measure.to_jordan_decomposition_neg {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) :

(-s).to_jordan_decomposition = -s.to_jordan_decomposition

theorem measure_theory.signed_measure.to_jordan_decomposition_smul {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) (r : nnreal) :

(r • s).to_jordan_decomposition = r • s.to_jordan_decomposition

theorem measure_theory.signed_measure.to_jordan_decomposition_smul_real {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) (r : ℝ) :

(r • s).to_jordan_decomposition = r • s.to_jordan_decomposition

theorem measure_theory.signed_measure.to_jordan_decomposition_eq {α : Type u_1} [measurable_space α] {s : measure_theory.signed_measure α} {j : measure_theory.jordan_decomposition α} (h : s = j.to_signed_measure) :

s.to_jordan_decomposition = j

noncomputable def measure_theory.signed_measure.total_variation {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) :

measure_theory.measure α

The total variation of a signed measure.

Equations

s.total_variation = s.to_jordan_decomposition.pos_part + s.to_jordan_decomposition.neg_part

theorem measure_theory.signed_measure.total_variation_zero {α : Type u_1} [measurable_space α] :

0.total_variation = 0

theorem measure_theory.signed_measure.total_variation_neg {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) :

(-s).total_variation = s.total_variation

theorem measure_theory.signed_measure.null_of_total_variation_zero {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) {i : set α} (hs : ⇑(s.total_variation) i = 0) :

⇑s i = 0

theorem measure_theory.signed_measure.absolutely_continuous_ennreal_iff {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) (μ : measure_theory.vector_measure α ennreal) :

measure_theory.vector_measure.absolutely_continuous s μ ↔ s.total_variation.absolutely_continuous μ.ennreal_to_measure

theorem measure_theory.signed_measure.total_variation_absolutely_continuous_iff {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) :

s.total_variation.absolutely_continuous μ ↔ s.to_jordan_decomposition.pos_part.absolutely_continuous μ ∧ s.to_jordan_decomposition.neg_part.absolutely_continuous μ

theorem measure_theory.signed_measure.mutually_singular_iff {α : Type u_1} [measurable_space α] (s t : measure_theory.signed_measure α) :

measure_theory.vector_measure.mutually_singular s t ↔ s.total_variation.mutually_singular t.total_variation

theorem measure_theory.signed_measure.mutually_singular_ennreal_iff {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) (μ : measure_theory.vector_measure α ennreal) :

measure_theory.vector_measure.mutually_singular s μ ↔ s.total_variation.mutually_singular μ.ennreal_to_measure

theorem measure_theory.signed_measure.total_variation_mutually_singular_iff {α : Type u_1} [measurable_space α] (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) :

s.total_variation.mutually_singular μ ↔ s.to_jordan_decomposition.pos_part.mutually_singular μ ∧ s.to_jordan_decomposition.neg_part.mutually_singular μ