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
such that a set is μ
-null iff it is μ.toFinite
-null.
In particular, MeasureTheory.ae μ.toFinite = MeasureTheory.ae μ
and μ.toFinite = 0
iff μ = 0
.
As a corollary, μ
can be represented as μ.toFinite.withDensity (μ.rnDeriv μ.toFinite)
.
Our definition of MeasureTheory.Measure.toFinite
ensures some extra properties:
- if
μ
is a finite measure, thenμ.toFinite = μ[|univ] = (μ univ)⁻¹ • μ
; - in particular,
μ.toFinite = μ
for a probability measure; - if
μ ≠ 0
, thenμ.toFinite
is a probability measure.
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
(deprecated, useMeasureTheory.Measure.rnDeriv
): the Radon-Nikodym derivative ofμ.toFinite
with respect toμ
.
Main statements #
absolutelyContinuous_toFinite
:μ ≪ μ.toFinite
.toFinite_absolutelyContinuous
:μ.toFinite ≪ μ
.ae_toFinite
:ae μ.toFinite = ae μ
.
Auxiliary definition for MeasureTheory.Measure.toFinite
.
Equations
- μ.toFiniteAux = if MeasureTheory.IsFiniteMeasure μ then μ else ⋯.choose
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
Alias of MeasureTheory.sfiniteSeq_absolutelyContinuous_toFinite
.
A measurable function such that μ.toFinite.withDensity μ.densityToFinite = μ
.
See withDensity_densitytoFinite
.
Equations
- μ.densityToFinite a = μ.rnDeriv μ.toFinite a