mathlib documentation

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 ν.

The Lebesgue decomposition provides the Radon-Nikodym theorem readily.

Main definitions #

Main results #

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
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.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) :

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 μ.singular_part ν
theorem measure_theory.measure.singular_part_add {α : Type u_1} {m : measurable_space α} (μ₁ μ₂ ν : measure_theory.measure α) [μ₁.have_lebesgue_decomposition ν] [μ₂.have_lebesgue_decomposition ν] :
(μ₁ + μ₂).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.

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∞) (hf : f measure_theory.measure.lebesgue_decomposition.measurable_le μ ν) (hg : g measure_theory.measure.lebesgue_decomposition.measurable_le μ ν) (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.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_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

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

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 μ.

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 μ.

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 μ.