# mathlibdocumentation

measure_theory.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 #

• 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 meausre 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
@[ext]
structure measure_theory.jordan_decomposition (α : Type u_3)  :
Type u_3
• pos_part :
• neg_part :
• pos_part_finite :
• neg_part_finite :
• mutually_singular : self.pos_part ⊥ₘ self.neg_part

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

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
@[instance]
Equations
@[instance]
Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
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 : ℝ≥0) :
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)
theorem measure_theory.jordan_decomposition.real_smul_pos_part_nonneg {α : Type u_1} (r : ) (hr : 0 r) :
(r j).pos_part =
theorem measure_theory.jordan_decomposition.real_smul_neg_part_nonneg {α : Type u_1} (r : ) (hr : 0 r) :
(r j).neg_part =

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]

The total variation of a signed measure.

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