# Documentation

Mathlib.MeasureTheory.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 #

• MeasureTheory.Measure.HaveLebesgueDecomposition : A pair of measures μ and ν is said to HaveLebesgueDecomposition if there exist a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.withDensity f
• MeasureTheory.Measure.singularPart : If a pair of measures HaveLebesgueDecomposition, then singularPart chooses the measure from HaveLebesgueDecomposition, otherwise it returns the zero measure.
• MeasureTheory.Measure.rnDeriv: If a pair of measures HaveLebesgueDecomposition, then rnDeriv chooses the measurable function from HaveLebesgueDecomposition, otherwise it returns the zero function.
• MeasureTheory.SignedMeasure.HaveLebesgueDecomposition : A signed measure s and a measure μ is said to HaveLebesgueDecomposition if both the positive part and negative part of s HaveLebesgueDecomposition with respect to μ.
• MeasureTheory.SignedMeasure.singularPart : 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 μ.
• MeasureTheory.SignedMeasure.rnDeriv : 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 #

• MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite : the Lebesgue decomposition theorem.
• MeasureTheory.Measure.eq_singularPart : Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then s = μ.singularPart ν.
• MeasureTheory.Measure.eq_rnDeriv : Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then f = μ.rnDeriv ν.
• MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq : the Lebesgue decomposition theorem between a signed measure and a σ-finite positive measure.

# Tags #

Lebesgue decomposition theorem

class MeasureTheory.Measure.HaveLebesgueDecomposition {α : Type u_1} {m : } (μ : ) (ν : ) :

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

Instances
theorem MeasureTheory.Measure.singularPart_def {α : Type u_3} {m : } (μ : ) (ν : ) :
= if h : then (Classical.choose (_ : p, Measurable p.snd μ = p.fst + )).fst else 0
@[irreducible]
def MeasureTheory.Measure.singularPart {α : Type u_3} {m : } (μ : ) (ν : ) :

If a pair of measures HaveLebesgueDecomposition, then singularPart chooses the measure from HaveLebesgueDecomposition, otherwise it returns the zero measure. For sigma-finite measures, μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν).

Instances For
@[irreducible]
def MeasureTheory.Measure.rnDeriv {α : Type u_3} {m : } (μ : ) (ν : ) :
αENNReal

If a pair of measures HaveLebesgueDecomposition, then rnDeriv chooses the measurable function from HaveLebesgueDecomposition, otherwise it returns the zero function. For sigma-finite measures, μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν).

Instances For
theorem MeasureTheory.Measure.rnDeriv_def {α : Type u_3} {m : } (μ : ) (ν : ) :
= if h : then (Classical.choose (_ : p, Measurable p.snd μ = p.fst + )).snd else 0
theorem MeasureTheory.Measure.haveLebesgueDecomposition_spec {α : Type u_1} {m : } (μ : ) (ν : ) :
theorem MeasureTheory.Measure.haveLebesgueDecomposition_add {α : Type u_1} {m : } (μ : ) (ν : ) :
instance MeasureTheory.Measure.haveLebesgueDecomposition_smul {α : Type u_1} {m : } (μ : ) (ν : ) (r : NNReal) :
theorem MeasureTheory.Measure.measurable_rnDeriv {α : Type u_1} {m : } (μ : ) (ν : ) :
theorem MeasureTheory.Measure.mutuallySingular_singularPart {α : Type u_1} {m : } (μ : ) (ν : ) :
theorem MeasureTheory.Measure.singularPart_le {α : Type u_1} {m : } (μ : ) (ν : ) :
theorem MeasureTheory.Measure.withDensity_rnDeriv_le {α : Type u_1} {m : } (μ : ) (ν : ) :
instance MeasureTheory.Measure.singularPart.instIsFiniteMeasure {α : Type u_1} {m : } {μ : } {ν : } :
instance MeasureTheory.Measure.singularPart.instSigmaFinite {α : Type u_1} {m : } {μ : } {ν : } :
instance MeasureTheory.Measure.withDensity.instIsFiniteMeasure {α : Type u_1} {m : } {μ : } {ν : } :
instance MeasureTheory.Measure.withDensity.instSigmaFinite {α : Type u_1} {m : } {μ : } {ν : } :
theorem MeasureTheory.Measure.lintegral_rnDeriv_lt_top_of_measure_ne_top {α : Type u_1} {m : } {μ : } (ν : ) {s : Set α} (hs : μ s ) :
∫⁻ (x : α) in s, ν <
theorem MeasureTheory.Measure.lintegral_rnDeriv_lt_top {α : Type u_1} {m : } (μ : ) (ν : ) :
∫⁻ (x : α), ν <
theorem MeasureTheory.Measure.rnDeriv_lt_top {α : Type u_1} {m : } (μ : ) (ν : ) :
∀ᵐ (x : α) ∂ν,

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

theorem MeasureTheory.Measure.eq_singularPart {α : Type u_1} {m : } {μ : } {ν : } {s : } {f : αENNReal} (hf : ) (hs : ) (hadd : ) :

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

This theorem provides the uniqueness of the singularPart in the Lebesgue decomposition theorem, while MeasureTheory.Measure.eq_rnDeriv provides the uniqueness of the rnDeriv.

theorem MeasureTheory.Measure.singularPart_zero {α : Type u_1} {m : } (ν : ) :
theorem MeasureTheory.Measure.singularPart_smul {α : Type u_1} {m : } (μ : ) (ν : ) (r : NNReal) :
theorem MeasureTheory.Measure.singularPart_add {α : Type u_1} {m : } (μ₁ : ) (μ₂ : ) (ν : ) :
theorem MeasureTheory.Measure.singularPart_withDensity {α : Type u_1} {m : } (ν : ) {f : αENNReal} (hf : ) :
theorem MeasureTheory.Measure.eq_withDensity_rnDeriv {α : Type u_1} {m : } {μ : } {ν : } {s : } {f : αENNReal} (hf : ) (hs : ) (hadd : ) :

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

This theorem provides the uniqueness of the rnDeriv in the Lebesgue decomposition theorem, while MeasureTheory.Measure.eq_singularPart provides the uniqueness of the singularPart. Here, the uniqueness is given in terms of the measures, while the uniqueness in terms of the functions is given in eq_rnDeriv.

theorem MeasureTheory.Measure.eq_rnDeriv {α : Type u_1} {m : } {μ : } {ν : } {s : } {f : αENNReal} (hf : ) (hs : ) (hadd : ) :

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

This theorem provides the uniqueness of the rnDeriv in the Lebesgue decomposition theorem, while MeasureTheory.Measure.eq_singularPart provides the uniqueness of the singularPart. Here, the uniqueness is given in terms of the functions, while the uniqueness in terms of the functions is given in eq_withDensity_rnDeriv.

theorem MeasureTheory.Measure.rnDeriv_withDensity {α : Type u_1} {m : } (ν : ) {f : αENNReal} (hf : ) :

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

theorem MeasureTheory.Measure.rnDeriv_restrict {α : Type u_1} {m : } (ν : ) {s : Set α} (hs : ) :

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

theorem MeasureTheory.Measure.exists_positive_of_not_mutuallySingular {α : Type u_1} {m : } (μ : ) (ν : ) :
ε, 0 < ε E, 0 < ν 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.

def MeasureTheory.Measure.LebesgueDecomposition.measurableLE {α : Type u_1} {m : } (μ : ) (ν : ) :
Set (αENNReal)

Given two measures μ and ν, measurableLE μ ν 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.

Instances For
theorem MeasureTheory.Measure.LebesgueDecomposition.sup_mem_measurableLE {α : Type u_1} {m : } {μ : } {ν : } {f : αENNReal} {g : αENNReal} :
(fun a => f a g a)
theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_succ_eq_sup {α : Sort u_3} (f : αENNReal) (m : ) (a : α) :
⨆ (k : ) (_ : k m + 1), f k a = f () a ⨆ (k : ) (_ : k m), f k a
theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE {α : Type u_1} {m : } {μ : } {ν : } (f : αENNReal) (hf : ∀ (n : ), ) (n : ) :
(fun x => ⨆ (k : ) (_ : k n), f k x)
theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE' {α : Type u_1} {m : } {μ : } {ν : } (f : αENNReal) (hf : ∀ (n : ), ) (n : ) :
⨆ (k : ) (_ : k n), f k
theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone {α : Type u_3} (f : αENNReal) :
Monotone fun n x => ⨆ (k : ) (_ : k n), f k x
theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone' {α : Type u_3} (f : αENNReal) (x : α) :
Monotone fun n => ⨆ (k : ) (_ : k n), f k x
theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le {α : Type u_3} (f : αENNReal) (n : ) (k : ) (hk : k n) :
f k fun x => ⨆ (k : ) (_ : k n), f k x

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

Instances For

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

This is not an instance since this is also shown for the more general σ-finite measures with MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite.

instance MeasureTheory.Measure.restrict.instIsFiniteMeasure {α : Type u_1} {m : } {μ : } {S : } (n : ) :
instance MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite {α : Type u_1} {m : } (μ : ) (ν : ) :

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

class MeasureTheory.SignedMeasure.HaveLebesgueDecomposition {α : Type u_1} {m : } (s : ) (μ : ) :
• posPart :
• negPart :

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

Instances
instance MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul {α : Type u_1} {m : } (s : ) (μ : ) (r : NNReal) :
instance MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul_real {α : Type u_1} {m : } (s : ) (μ : ) (r : ) :
def MeasureTheory.SignedMeasure.singularPart {α : Type u_1} {m : } (s : ) (μ : ) :

Given a signed measure s and a measure μ, s.singularPart μ is the signed measure such that s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s and s.singularPart μ is mutually singular with respect to μ.

Instances For
def MeasureTheory.SignedMeasure.rnDeriv {α : Type u_1} {m : } (s : ) (μ : ) :
α

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

rnDeriv s μ satisfies μ.withDensityᵥ (s.rnDeriv μ) = s if and only if s is absolutely continuous with respect to μ and this fact is known as MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensity_rnDeriv_eq and can be found in MeasureTheory.Decomposition.RadonNikodym.

Instances For
theorem MeasureTheory.SignedMeasure.rnDeriv_def {α : Type u_1} {m : } (s : ) (μ : ) :
= fun x =>
theorem MeasureTheory.SignedMeasure.measurable_rnDeriv {α : Type u_1} {m : } (s : ) (μ : ) :
theorem MeasureTheory.SignedMeasure.integrable_rnDeriv {α : Type u_1} {m : } (s : ) (μ : ) :

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 MeasureTheory.SignedMeasure.haveLebesgueDecomposition_mk {α : Type u_1} {m : } {s : } {t : } (μ : ) {f : α} (hf : ) (hadd : ) :
theorem MeasureTheory.SignedMeasure.eq_singularPart {α : Type u_1} {m : } {μ : } {s : } (t : ) (f : α) (hadd : ) :

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

theorem MeasureTheory.SignedMeasure.singularPart_zero {α : Type u_1} {m : } (μ : ) :
theorem MeasureTheory.SignedMeasure.singularPart_neg {α : Type u_1} {m : } (s : ) (μ : ) :
theorem MeasureTheory.SignedMeasure.singularPart_smul_nnreal {α : Type u_1} {m : } (s : ) (μ : ) (r : NNReal) :
theorem MeasureTheory.SignedMeasure.singularPart_smul {α : Type u_1} {m : } (s : ) (μ : ) (r : ) :
theorem MeasureTheory.SignedMeasure.eq_rnDeriv {α : Type u_1} {m : } {μ : } {s : } (t : ) (f : α) (hfi : ) (hadd : ) :

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

theorem MeasureTheory.SignedMeasure.rnDeriv_smul {α : Type u_1} {m : } (s : ) (μ : ) (r : ) :
class MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition {α : Type u_1} {m : } (c : ) (μ : ) :

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

Instances
def MeasureTheory.ComplexMeasure.singularPart {α : Type u_1} {m : } (c : ) (μ : ) :

The singular part between a complex measure c and a positive measure μ is the complex measure satisfying c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c. This property is given by MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq.

Instances For
def MeasureTheory.ComplexMeasure.rnDeriv {α : Type u_1} {m : } (c : ) (μ : ) :
α

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

Instances For
theorem MeasureTheory.ComplexMeasure.integrable_rnDeriv {α : Type u_1} {m : } (c : ) (μ : ) :