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 #
MeasureTheory.Measure.HaveLebesgueDecomposition: A pair of measuresμandνis said toHaveLebesgueDecompositionif there exist a measureξand a measurable functionf, such thatξis mutually singular with respect toνandμ = ξ + ν.withDensity fMeasureTheory.Measure.singularPart: If a pair of measuresHaveLebesgueDecomposition, thensingularPartchooses the measure fromHaveLebesgueDecomposition, otherwise it returns the zero measure.MeasureTheory.Measure.rnDeriv: If a pair of measuresHaveLebesgueDecomposition, thenrnDerivchooses the measurable function fromHaveLebesgueDecomposition, otherwise it returns the zero function.
Main results #
MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite: the Lebesgue decomposition theorem.MeasureTheory.Measure.eq_singularPart: Given measuresμandν, ifsis a measure mutually singular toνandfis a measurable function such thatμ = s + fν, thens = μ.singularPart ν.MeasureTheory.Measure.eq_rnDeriv: Given measuresμandν, ifsis a measure mutually singular toνandfis a measurable function such thatμ = s + fν, thenf = μ.rnDeriv ν.
Tags #
Lebesgue decomposition theorem
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.
- lebesgue_decomposition : ∃ (p : MeasureTheory.Measure α × (α → ENNReal)), Measurable p.2 ∧ p.1.MutuallySingular ν ∧ μ = p.1 + ν.withDensity p.2
Instances
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 ν).
Equations
- μ.singularPart ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).1 else 0
Instances For
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 ν).
Equations
- μ.rnDeriv ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).2 else 0
Instances For
For the versions of this lemma where ν.withDensity (μ.rnDeriv ν) or μ.singularPart ν are
isolated, see MeasureTheory.Measure.measure_sub_singularPart and
MeasureTheory.Measure.measure_sub_rnDeriv.
For the versions of this lemma where μ.singularPart ν or ν.withDensity (μ.rnDeriv ν) are
isolated, see MeasureTheory.Measure.measure_sub_singularPart and
MeasureTheory.Measure.measure_sub_rnDeriv.
The Radon-Nikodym derivative of a sigma-finite measure μ with respect to another
measure ν is ν-almost everywhere finite.
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.
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.
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.
The Radon-Nikodym derivative of f ν with respect to ν is f.
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.
Radon-Nikodym derivative of the scalar multiple of a measure.
See also rnDeriv_smul_left', which requires sigma-finite ν and μ.
Radon-Nikodym derivative of the scalar multiple of a measure.
See also rnDeriv_smul_left_of_ne_top', which requires sigma-finite ν and μ.
Radon-Nikodym derivative with respect to the scalar multiple of a measure.
See also rnDeriv_smul_right', which requires sigma-finite ν and μ.
Radon-Nikodym derivative with respect to the scalar multiple of a measure.
See also rnDeriv_smul_right_of_ne_top', which requires sigma-finite ν and μ.
Radon-Nikodym derivative of a sum of two measures.
See also rnDeriv_add', which requires sigma-finite ν₁, ν₂ and μ.
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 ν, 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.
Equations
- MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν = {f : α → ENNReal | Measurable f ∧ ∀ (A : Set α), MeasurableSet A → ∫⁻ (x : α) in A, f x ∂μ ≤ ν A}
Instances For
measurableLEEval μ ν is the set of ∫⁻ x, f x ∂μ for all f ∈ measurableLE μ ν.
Equations
- MeasureTheory.Measure.LebesgueDecomposition.measurableLEEval μ ν = (fun (f : α → ENNReal) => ∫⁻ (x : α), f x ∂μ) '' MeasureTheory.Measure.LebesgueDecomposition.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.
If any finite measure has a Lebesgue decomposition with respect to ν,
then the same is true for any s-finite measure.
The Lebesgue decomposition theorem:
Any s-finite measure μ has Lebesgue decomposition with respect to any σ-finite measure ν.
That is to say, there exist a measure ξ and a measurable function f,
such that ξ is mutually singular with respect to ν and μ = ξ + ν.withDensity f
Radon-Nikodym derivative of the scalar multiple of a measure.
See also rnDeriv_smul_left, which has no hypothesis on μ but requires finite ν.
Radon-Nikodym derivative of the scalar multiple of a measure.
See also rnDeriv_smul_left_of_ne_top, which has no hypothesis on μ but requires finite ν.
Radon-Nikodym derivative with respect to the scalar multiple of a measure.
See also rnDeriv_smul_right, which has no hypothesis on μ but requires finite ν.
Radon-Nikodym derivative with respect to the scalar multiple of a measure.
See also rnDeriv_smul_right_of_ne_top, which has no hypothesis on μ but requires finite ν.
Radon-Nikodym derivative of a sum of two measures.
See also rnDeriv_add, which has no hypothesis on μ but requires finite ν₁ and ν₂.