mathlib3documentation

measure_theory.decomposition.lebesgue

Lebesgue decomposition #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• measure_theory.measure.have_lebesgue_decomposition : A pair of measures μ and ν is said to have_lebesgue_decomposition if there exist 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]

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 of this typeclass
@[irreducible]
noncomputable def measure_theory.measure.singular_part {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :

If a pair of measures have_lebesgue_decomposition, then singular_part chooses the measure from have_lebesgue_decomposition, otherwise it returns the zero measure. For sigma-finite measures, μ = μ.singular_part ν + ν.with_density (μ.rn_deriv ν).

Equations
• = (λ (h : , 0)
Instances for measure_theory.measure.singular_part
@[irreducible]
noncomputable def measure_theory.measure.rn_deriv {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) :

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. For sigma-finite measures, μ = μ.singular_part ν + ν.with_density (μ.rn_deriv ν).

Equations
@[measurability]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem measure_theory.measure.rn_deriv_lt_top {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α)  :
∀ᵐ (x : α) ν, μ.rn_deriv ν x <

The Radon-Nikodym derivative of a sigma-finite measure μ with respect to another measure ν is ν-almost everywhere finite.

theorem measure_theory.measure.eq_singular_part {α : Type u_1} {m : measurable_space α} {μ ν s : measure_theory.measure α} {f : α ennreal} (hf : measurable f) (hs : s.mutually_singular ν) (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_add {α : Type u_1} {m : measurable_space α} (μ₁ μ₂ ν : measure_theory.measure α)  :
(μ₁ + μ₂).singular_part ν = μ₁.singular_part ν + μ₂.singular_part ν
theorem measure_theory.measure.eq_with_density_rn_deriv {α : Type u_1} {m : measurable_space α} {μ ν s : measure_theory.measure α} {f : α ennreal} (hf : measurable f) (hs : s.mutually_singular ν) (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. Here, the uniqueness is given in terms of the measures, while the uniqueness in terms of the functions is given in eq_rn_deriv.

theorem measure_theory.measure.eq_rn_deriv {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} {s : measure_theory.measure α} {f : α ennreal} (hf : measurable f) (hs : s.mutually_singular ν) (hadd : μ = s + ν.with_density f) :
f =ᵐ[ν] μ.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 ν.

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. Here, the uniqueness is given in terms of the functions, while the uniqueness in terms of the functions is given in eq_with_density_rn_deriv.

The Radon-Nikodym derivative of f ν with respect to ν is f.

The Radon-Nikodym derivative of the restriction of a measure to a measurable set is the indicator function of this set.

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.sup_mem_measurable_le {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} {f g : α ennreal}  :
(λ (a : α), f a g a)
theorem measure_theory.measure.lebesgue_decomposition.supr_succ_eq_sup {α : Sort u_1} (f : ) (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 : ) (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 : ) (hf : (n : ), ) (n : ) :
( (k : ) (hk : k n), f k)
theorem measure_theory.measure.lebesgue_decomposition.supr_monotone {α : Type u_1} (f : ) :
monotone (λ (n : ) (x : α), (k : ) (hk : k n), f k x)
theorem measure_theory.measure.lebesgue_decomposition.supr_monotone' {α : Type u_1} (f : ) (x : α) :
monotone (λ (n : ), (k : ) (hk : k n), f k x)
theorem measure_theory.measure.lebesgue_decomposition.supr_le_le {α : Type u_1} (f : ) (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.

@[protected, 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 of this typeclass
@[protected, instance]

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
noncomputable 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 : α ) (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 : μ) (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 μ.

@[class]
• re_part :
• im_part :

A complex measure is said to have_lebesgue_decomposition with respect to a positive measure if both its real and imaginary part have_lebesgue_decomposition with respect to that measure.

The singular part between a complex measure c and a positive measure μ is the complex measure satisfying c.singular_part μ + μ.with_densityᵥ (c.rn_deriv μ) = c. This property is given by measure_theory.complex_measure.singular_part_add_with_density_rn_deriv_eq.

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

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

Equations