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 ∧ MeasureTheory.Measure.MutuallySingular p.1 ν ∧ μ = p.1 + MeasureTheory.Measure.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 ν).
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 ν).
Instances For
Equations
Equations
Equations
- (_ : MeasureTheory.Measure.HaveLebesgueDecomposition (r • μ) ν) = (_ : MeasureTheory.Measure.HaveLebesgueDecomposition (r • μ) ν)
Equations
- (_ : MeasureTheory.Measure.HaveLebesgueDecomposition μ (r • ν)) = (_ : MeasureTheory.Measure.HaveLebesgueDecomposition μ (r • ν))
Equations
Equations
Equations
Equations
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- (_ : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.restrict μ (S.set n))) = (_ : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.restrict μ (S.set n)))
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
Equations
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 ν₂.