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 toHaveLebesgueDecomposition
if there exist a measureξ
and a measurable functionf
, such thatξ
is mutually singular with respect toν
andμ = ξ + ν.withDensity f
MeasureTheory.Measure.singularPart
: If a pair of measuresHaveLebesgueDecomposition
, thensingularPart
chooses the measure fromHaveLebesgueDecomposition
, otherwise it returns the zero measure.MeasureTheory.Measure.rnDeriv
: If a pair of measuresHaveLebesgueDecomposition
, thenrnDeriv
chooses 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ν
, ifs
is a measure mutually singular toν
andf
is a measurable function such thatμ = s + fν
, thens = μ.singularPart ν
.MeasureTheory.Measure.eq_rnDeriv
: Given measuresμ
andν
, ifs
is a measure mutually singular toν
andf
is 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 ν)
.
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
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
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
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 ν₂
.