# mathlib3documentation

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

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

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

Instances for measure_theory.jordan_decomposition
theorem measure_theory.jordan_decomposition.ext {α : Type u_3} {_inst_2 : measurable_space α} (h : x.pos_part = y.pos_part) (h_1 : x.neg_part = y.neg_part) :
x = y
@[protected, instance]
Equations
@[protected, instance]
noncomputable def measure_theory.jordan_decomposition.has_smul {α : Type u_1}  :
Equations
@[protected, instance]
noncomputable def measure_theory.jordan_decomposition.has_smul_real {α : Type u_1}  :
Equations
theorem measure_theory.jordan_decomposition.real_smul_def {α : Type u_1} (r : )  :
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} (r : nnreal) :
r j = r j
theorem measure_theory.jordan_decomposition.real_smul_nonneg {α : Type u_1} (r : ) (hr : 0 r) :
r j = r.to_nnreal j
theorem measure_theory.jordan_decomposition.real_smul_neg {α : Type u_1} (r : ) (hr : r < 0) :
r j = -((-r).to_nnreal j)

The signed measure associated with a Jordan decomposition.

Equations

A Jordan decomposition provides a Hahn 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
theorem measure_theory.signed_measure.to_jordan_decomposition_spec {α : Type u_1}  :
(i : set α) (hi₁ : (hi₂ : (hi₃ : , s.to_jordan_decomposition.pos_part = 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.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} {u v w : set α} (hu : measurable_set u) (hv : measurable_set v) (hw : measurable_set w) (hsu : 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 positive set u.

theorem measure_theory.signed_measure.subset_negative_null_set {α : Type u_1} {u v w : set α} (hu : measurable_set u) (hv : measurable_set v) (hw : measurable_set w) (hsu : 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} {u v : set α} (hu : measurable_set u) (hv : measurable_set v) (hsu : 0.restrict u ) (hsv : 0.restrict 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} {u v : set α} (hu : measurable_set u) (hv : measurable_set v) (hsu : 0.restrict u) (hsv : 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} {u v w : set α} (hu : measurable_set u) (hv : measurable_set v) (hw : measurable_set w) (hsu : 0.restrict u ) (hsv : 0.restrict 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} {u v w : set α} (hu : measurable_set u) (hv : measurable_set v) (hw : measurable_set w) (hsu : 0.restrict u) (hsv : 0.restrict v) (hs : s (u v) = 0) :
s (w u) = s (w v)

The Jordan decomposition of a signed measure is unique.

@[simp]
@[simp]

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

Equations
@[simp]
noncomputable def measure_theory.signed_measure.total_variation {α : Type u_1}  :

The total variation of a signed measure.

Equations