# mathlibdocumentation

measure_theory.decomposition.lebesgue

# Lebesgue decomposition #

This file proves the Lebesgue decomposition theorem. The Lebesgue decomposition theorem states that, given two σ-finite measures μ and ν, there exists a finite measure ξ and a measurable function f such that μ = ξ + fν and ξ is mutually singular with respect to ν.

## Main definitions #

• measure_theory.measure.have_lebesgue_decomposition : A pair of measures μ and ν is said to have_lebesgue_decomposition if there exists a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.with_density f
• measure_theory.measure.singular_part : If a pair of measures have_lebesgue_decomposition, then singular_part chooses the measure from have_lebesgue_decomposition, otherwise it returns the zero measure.
• measure_theory.measure.rn_deriv: If a pair of measures have_lebesgue_decomposition, then rn_deriv chooses the measurable function from have_lebesgue_decomposition, otherwise it returns the zero function.
• measure_theory.signed_measure.have_lebesgue_decomposition : A signed measure s and a measure μ is said to have_lebesgue_decomposition if both the positive part and negative part of s have_lebesgue_decomposition with respect to μ.
• measure_theory.signed_measure.singular_part : The singular part between a signed measure s and a measure μ is simply the singular part of the positive part of s with respect to μ minus the singular part of the negative part of s with respect to μ.
• measure_theory.signed_measure.rn_deriv : The Radon-Nikodym derivative of a signed measure s with respect to a measure μ is the Radon-Nikodym derivative of the positive part of s with respect to μ minus the Radon-Nikodym derivative of the negative part of s with respect to μ.

## Main results #

• measure_theory.measure.have_lebesgue_decomposition_of_sigma_finite : the Lebesgue decomposition theorem.
• measure_theory.measure.eq_singular_part : Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then s = singular_part μ ν.
• measure_theory.measure.eq_rn_deriv : Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then f = rn_deriv μ ν.
• measure_theory.signed_measure.singular_part_add_with_density_rn_deriv_eq : the Lebesgue decomposition theorem between a signed measure and a σ-finite positive measure.

# Tags #

Lebesgue decomposition theorem

@[class]
structure measure_theory.measure.have_lebesgue_decomposition {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :
Prop

A pair of measures μ and ν is said to have_lebesgue_decomposition if there exists a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.with_density f.

Instances

If a pair of measures have_lebesgue_decomposition, then singular_part chooses the measure from have_lebesgue_decomposition, otherwise it returns the zero measure.

Equations
• = (λ (h : , 0)
def measure_theory.measure.rn_deriv {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :
α → ℝ≥0∞

If a pair of measures have_lebesgue_decomposition, then rn_deriv chooses the measurable function from have_lebesgue_decomposition, otherwise it returns the zero function.

Equations
theorem measure_theory.measure.singular_part_le {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :
μ
theorem measure_theory.measure.lintegral_rn_deriv_lt_top {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α)  :
∫⁻ (x : α), μ.rn_deriv ν x ν <
theorem measure_theory.measure.eq_singular_part {α : Type u_1} {m : measurable_space α} {μ ν s : measure_theory.measure α} {f : α → ℝ≥0∞} (hf : measurable f) (hs : s ⊥ₘ ν) (hadd : μ = s + ν.with_density f) :
s =

Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then s = singular_part μ ν.

This theorem provides the uniqueness of the singular_part in the Lebesgue decomposition theorem, while measure_theory.measure.eq_rn_deriv provides the uniqueness of the rn_deriv.

theorem measure_theory.measure.singular_part_smul {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) (r : ℝ≥0) :
(r μ).singular_part ν = r
theorem measure_theory.measure.singular_part_add {α : Type u_1} {m : measurable_space α} (μ₁ μ₂ ν : measure_theory.measure α)  :
(μ₁ + μ₂).singular_part ν = μ₁.singular_part ν + μ₂.singular_part ν
theorem measure_theory.measure.eq_rn_deriv {α : Type u_1} {m : measurable_space α} {μ ν s : measure_theory.measure α} {f : α → ℝ≥0∞} (hf : measurable f) (hs : s ⊥ₘ ν) (hadd : μ = s + ν.with_density f) :

Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then f = rn_deriv μ ν.

This theorem provides the uniqueness of the rn_deriv in the Lebesgue decomposition theorem, while measure_theory.measure.eq_singular_part provides the uniqueness of the singular_part.

theorem measure_theory.measure.exists_positive_of_not_mutually_singular {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) (h : ¬μ ⊥ₘ ν) :
∃ (ε : ℝ≥0), 0 < ε ∃ (E : set α), 0 < ν E 0.restrict E (μ.to_signed_measure - ν).to_signed_measure).restrict E

If two finite measures μ and ν are not mutually singular, there exists some ε > 0 and a measurable set E, such that ν(E) > 0 and E is positive with respect to μ - εν.

This lemma is useful for the Lebesgue decomposition theorem.

Given two measures μ and ν, measurable_le μ ν is the set of measurable functions f, such that, for all measurable sets A, ∫⁻ x in A, f x ∂μ ≤ ν A.

This is useful for the Lebesgue decomposition theorem.

Equations
theorem measure_theory.measure.lebesgue_decomposition.max_measurable_le {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} (f g : α → ℝ≥0∞) (A : set α) (hA : measurable_set A) :
∫⁻ (a : α) in A, max (f a) (g a) μ ∫⁻ (a : α) in A {a : α | f a g a}, g a μ + ∫⁻ (a : α) in A {a : α | g a < f a}, f a μ
theorem measure_theory.measure.lebesgue_decomposition.sup_mem_measurable_le {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} {f g : α → ℝ≥0∞}  :
(λ (a : α), f a g a)
theorem measure_theory.measure.lebesgue_decomposition.supr_succ_eq_sup {α : Sort u_1} (f : α → ℝ≥0∞) (m : ) (a : α) :
(⨆ (k : ) (hk : k m + 1), f k a) = f m.succ a ⨆ (k : ) (hk : k m), f k a
theorem measure_theory.measure.lebesgue_decomposition.supr_mem_measurable_le {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} (f : α → ℝ≥0∞) (hf : ∀ (n : ), ) (n : ) :
(λ (x : α), ⨆ (k : ) (hk : k n), f k x)
theorem measure_theory.measure.lebesgue_decomposition.supr_mem_measurable_le' {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} (f : α → ℝ≥0∞) (hf : ∀ (n : ), ) (n : ) :
(⨆ (k : ) (hk : k n), f k)
theorem measure_theory.measure.lebesgue_decomposition.supr_monotone {α : Type u_1} (f : α → ℝ≥0∞) :
monotone (λ (n : ) (x : α), ⨆ (k : ) (hk : k n), f k x)
theorem measure_theory.measure.lebesgue_decomposition.supr_monotone' {α : Type u_1} (f : α → ℝ≥0∞) (x : α) :
monotone (λ (n : ), ⨆ (k : ) (hk : k n), f k x)
theorem measure_theory.measure.lebesgue_decomposition.supr_le_le {α : Type u_1} (f : α → ℝ≥0∞) (n k : ) (hk : k n) :
f k λ (x : α), ⨆ (k : ) (hk : k n), f k x

measurable_le_eval μ ν is the set of ∫⁻ x, f x ∂μ for all f ∈ measurable_le μ ν.

Equations

Any pair of finite measures μ and ν, have_lebesgue_decomposition. That is to say, there exist a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.with_density f.

This is not an instance since this is also shown for the more general σ-finite measures with measure_theory.measure.have_lebesgue_decomposition_of_sigma_finite.

@[instance]

The Lebesgue decomposition theorem: Any pair of σ-finite measures μ and ν have_lebesgue_decomposition. That is to say, there exist a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.with_density f

@[class]
• pos_part :
• neg_part :

A signed measure s is said to have_lebesgue_decomposition with respect to a measure μ if the positive part and the negative part of s both have_lebesgue_decomposition with respect to μ.

Instances

Given a signed measure s and a measure μ, s.singular_part μ is the signed measure such that s.singular_part μ + μ.with_densityᵥ (s.rn_deriv μ) = s and s.singular_part μ is mutually singular with respect to μ.

Equations
def measure_theory.signed_measure.rn_deriv {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) :
α →

The Radon-Nikodym derivative between a signed measure and a positive measure.

rn_deriv s μ satisfies μ.with_densityᵥ (s.rn_deriv μ) = s if and only if s is absolutely continuous with respect to μ and this fact is known as measure_theory.signed_measure.absolutely_continuous_iff_with_density_rn_deriv_eq and can be found in measure_theory.decomposition.radon_nikodym.

Equations

The Lebesgue Decomposition theorem between a signed measure and a measure: Given a signed measure s and a σ-finite measure μ, there exist a signed measure t and a measurable and integrable function f, such that t is mutually singular with respect to μ and s = t + μ.with_densityᵥ f. In this case t = s.singular_part μ and f = s.rn_deriv μ.

theorem measure_theory.signed_measure.eq_singular_part {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α → ) (htμ : t ⊥ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + ) :
t =

Given a measure μ, signed measures s and t, and a function f such that t is mutually singular with respect to μ and s = t + μ.with_densityᵥ f, we have t = singular_part s μ, i.e. t is the singular part of the Lebesgue decomposition between s and μ.

theorem measure_theory.signed_measure.eq_rn_deriv {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α → ) (hfi : μ) (htμ : t ⊥ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + ) :
f =ᵐ[μ] s.rn_deriv μ

Given a measure μ, signed measures s and t, and a function f such that t is mutually singular with respect to μ and s = t + μ.with_densityᵥ f, we have f = rn_deriv s μ, i.e. f is the Radon-Nikodym derivative of s and μ.

theorem measure_theory.signed_measure.rn_deriv_smul {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (r : ) :
(r s).rn_deriv μ =ᵐ[μ] r s.rn_deriv μ