s-finite measures can be written as withDensity
of a finite measure #
If μ
is an s-finite measure, then there exists a finite measure μ.toFinite
and a measurable
function densityToFinite μ
such that μ = μ.toFinite.withDensity μ.densityToFinite
. If μ
is
zero this is the zero measure, and otherwise we can choose a probability measure for μ.toFinite
.
That measure is not unique, and in particular our implementation leads to μ.toFinite ≠ μ
even if
μ
is a probability measure.
We use this construction to define a set μ.sigmaFiniteSet
, such that μ.restrict μ.sigmaFiniteSet
is sigma-finite, and for all measurable sets s ⊆ μ.sigmaFiniteSetᶜ
, either μ s = 0
or μ s = ∞
.
Main definitions #
In these definitions and the results below, μ
is an s-finite measure (SFinite μ
).
MeasureTheory.Measure.toFinite
: a finite measure withμ ≪ μ.toFinite
andμ.toFinite ≪ μ
. Ifμ ≠ 0
, this is a probability measure.MeasureTheory.Measure.densityToFinite
: a measurable function such thatμ = μ.toFinite.withDensity μ.densityToFinite
.
Main statements #
absolutelyContinuous_toFinite
:μ ≪ μ.toFinite
.toFinite_absolutelyContinuous
:μ.toFinite ≪ μ
.withDensity_densitytoFinite
:μ.toFinite.withDensity μ.densityToFinite = μ
.
Auxiliary definition for MeasureTheory.Measure.toFinite
.
Equations
- μ.toFiniteAux = MeasureTheory.Measure.sum fun (n : ℕ) => (2 ^ (n + 1) * (MeasureTheory.sFiniteSeq μ n) Set.univ)⁻¹ • MeasureTheory.sFiniteSeq μ n
Instances For
A finite measure obtained from an s-finite measure μ
, such that
μ = μ.toFinite.withDensity μ.densityToFinite
(see withDensity_densitytoFinite
).
If μ
is non-zero, this is a probability measure.
Equations
- μ.toFinite = ProbabilityTheory.cond μ.toFiniteAux Set.univ
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A measurable function such that μ.toFinite.withDensity μ.densityToFinite = μ
.
See withDensity_densitytoFinite
.
Equations
- μ.densityToFinite a = ∑' (n : ℕ), (MeasureTheory.sFiniteSeq μ n).rnDeriv μ.toFinite a