mathlib documentation

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 #

Main results #

Tags #

Jordan decomposition theorem

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

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 α} (x y : measure_theory.jordan_decomposition α) (h : x.pos_part = y.pos_part) (h_1 : x.neg_part = y.neg_part) :
x = y
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))

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
@[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} [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.

If the symmetric difference of two positive sets is a null-set, then so are the differences between the two sets.

If the symmetric difference of two negative sets is a null-set, then so are the differences between the two sets.