Measure spaces #
The definition of a measure and a measure space are in MeasureTheory.MeasureSpaceDef
, with
only a few basic properties. This file provides many more properties of these objects.
This separation allows the measurability tactic to import only the file MeasureSpaceDef
, and to
be available in MeasureSpace
(through MeasurableSpace
).
Given a measurable space α
, a measure on α
is a function that sends measurable sets to the
extended nonnegative reals that satisfies the following conditions:
μ ∅ = 0
;μ
is countably additive. This means that the measure of a countable union of pairwise disjoint sets is equal to the measure of the individual sets.
Every measure can be canonically extended to an outer measure, so that it assigns values to all subsets, not just the measurable subsets. On the other hand, a measure that is countably additive on measurable sets can be restricted to measurable sets to obtain a measure. In this file a measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.
Measures on α
form a complete lattice, and are closed under scalar multiplication with ℝ≥0∞
.
We introduce the following typeclasses for measures:
IsProbabilityMeasure μ
:μ univ = 1
;IsFiniteMeasure μ
:μ univ < ∞
;SigmaFinite μ
: there exists a countable collection of sets that coveruniv
whereμ
is finite;IsLocallyFiniteMeasure μ
:∀ x, ∃ s ∈ 𝓝 x, μ s < ∞
;NoAtoms μ
:∀ x, μ {x} = 0
; possibly should be redefined as∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s
.
Given a measure, the null sets are the sets where μ s = 0
, where μ
denotes the corresponding
outer measure (so s
might not be measurable). We can then define the completion of μ
as the
measure on the least σ
-algebra that also contains all null sets, by defining the measure to be 0
on the null sets.
Main statements #
completion
is the completion of a measure to all null measurable sets.Measure.ofMeasurable
andOuterMeasure.toMeasure
are two important ways to define a measure.
Implementation notes #
Given μ : Measure α
, μ s
is the value of the outer measure applied to s
.
This conveniently allows us to apply the measure to sets without proving that they are measurable.
We get countable subadditivity for all sets, but only countable additivity for measurable sets.
You often don't want to define a measure via its constructor. Two ways that are sometimes more convenient:
Measure.ofMeasurable
is a way to define a measure by only giving its value on measurable sets and proving the properties (1) and (2) mentioned above.OuterMeasure.toMeasure
is a way of obtaining a measure from an outer measure by showing that all measurable sets in the measurable space are Carathéodory measurable.
To prove that two measures are equal, there are multiple options:
ext
: two measures are equal if they are equal on all measurable sets.ext_of_generateFrom_of_iUnion
: two measures are equal if they are equal on a π-system generating the measurable sets, if the π-system contains a spanning increasing sequence of sets where the measures take finite value (in particular the measures are σ-finite). This is a special case of the more generalext_of_generateFrom_of_cover
ext_of_generate_finite
: two finite measures are equal if they are equal on a π-system generating the measurable sets. This is a special case ofext_of_generateFrom_of_iUnion
usingC ∪ {univ}
, but is easier to work with.
A MeasureSpace
is a class that is a measurable space with a canonical measure.
The measure is denoted volume
.
References #
- https://en.wikipedia.org/wiki/Measure_(mathematics)
- https://en.wikipedia.org/wiki/Complete_measure
- https://en.wikipedia.org/wiki/Almost_everywhere
Tags #
measure, almost everywhere, measure space, completion, null set, null measurable set
See also MeasureTheory.ae_restrict_uIoc_iff
.
The measure of an a.e. disjoint union (even uncountable) of null-measurable sets is at least the sum of the measures of the sets.
The measure of a disjoint union (even uncountable) of measurable sets is at least the sum of the measures of the sets.
If s
is a countable set, then the measure of its preimage can be found as the sum of measures
of the fibers f ⁻¹' {y}
.
If s
is a Finset
, then the measure of its preimage can be found as the sum of measures
of the fibers f ⁻¹' {y}
.
If s ⊆ t
, μ t ≤ μ s
, μ t ≠ ∞
, and s
is measurable, then s =ᵐ[μ] t
.
Pigeonhole principle for measure spaces: if ∑' i, μ (s i) > μ univ
, then
one of the intersections s i ∩ s j
is not empty.
Pigeonhole principle for measure spaces: if s
is a Finset
and
∑ i in s, μ (t i) > μ univ
, then one of the intersections t i ∩ t j
is not empty.
If two sets s
and t
are included in a set u
, and μ s + μ t > μ u
,
then s
intersects t
. Version assuming that t
is measurable.
If two sets s
and t
are included in a set u
, and μ s + μ t > μ u
,
then s
intersects t
. Version assuming that s
is measurable.
Continuity from below: the measure of the union of a directed sequence of (not necessarily -measurable) sets is the supremum of the measures.
Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the infimum of the measures.
Continuity from below: the measure of the union of an increasing sequence of measurable sets is the limit of the measures.
Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the limit of the measures.
The measure of the intersection of a decreasing sequence of measurable sets indexed by a linear order with first countable topology is the limit of the measures.
One direction of the Borel-Cantelli lemma: if (sᵢ) is a sequence of sets such
that ∑ μ sᵢ
is finite, then the limit superior of the sᵢ
is a null set.
Obtain a measure by giving an outer measure where all sets in the σ-algebra are Carathéodory measurable.
Instances For
If u
is a superset of t
with the same (finite) measure (both sets possibly non-measurable),
then for any measurable set s
one also has μ (t ∩ s) = μ (u ∩ s)
.
The measurable superset toMeasurable μ t
of t
(which has the same measure as t
)
satisfies, for any measurable set s
, the equality μ (toMeasurable μ t ∩ s) = μ (u ∩ s)
.
Here, we require that the measure of t
is finite. The conclusion holds without this assumption
when the measure is sigma_finite, see measure_toMeasurable_inter_of_sigmaFinite
.
The ℝ≥0∞
-module of measures #
Coercion to function as an additive monoid homomorphism.
Instances For
The complete lattice of measures #
Measures are partially ordered.
The definition of less equal here is equivalent to the definition without the
measurable set condition, and this is shown by Measure.le_iff'
. It is defined
this way since, to prove μ ≤ ν
, we may simply intros s hs
instead of rewriting followed
by intros s hs
.
Pushforward and pullback #
Lift a linear map between OuterMeasure
spaces such that for each measure μ
every measurable
set is caratheodory-measurable w.r.t. f μ
to a linear map between Measure
spaces.
Instances For
The pushforward of a measure as a linear map. It is defined to be 0
if f
is not
a measurable function.
Instances For
The pushforward of a measure. It is defined to be 0
if f
is not an almost everywhere
measurable function.
Instances For
We can evaluate the pushforward on measurable sets. For non-measurable sets, see
MeasureTheory.Measure.le_map_apply
and MeasurableEquiv.map_apply
.
Even if s
is not measurable, we can bound map f μ s
from below.
See also MeasurableEquiv.map_apply
.
Even if s
is not measurable, map f μ s = 0
implies that μ (f ⁻¹' s) = 0
.
Pullback of a Measure
as a linear map. If f
sends each measurable set to a measurable
set, then for each measurable set s
we have comapₗ f μ s = μ (f '' s)
.
If the linearity is not needed, please use comap
instead, which works for a larger class of
functions.
Instances For
Pullback of a Measure
. If f
sends each measurable set to a null-measurable set,
then for each measurable set s
we have comap f μ s = μ (f '' s)
.
Instances For
Subtype of a measure space #
Restricting a measure #
Restrict a measure μ
to a set s
as an ℝ≥0∞
-linear map.
Instances For
Restrict a measure μ
to a set s
.
Instances For
This lemma shows that restrict
and toOuterMeasure
commute. Note that the LHS has a
restrict on measures and the RHS has a restrict on outer measures.
If t
is a measurable set, then the measure of t
with respect to the restriction of
the measure to s
equals the outer measure of t ∩ s
. An alternate version requiring that s
be measurable instead of t
exists as Measure.restrict_apply'
.
Restriction of a measure to a subset is monotone both in set and in measure.
Restriction of a measure to a subset is monotone both in set and in measure.
If s
is a measurable set, then the outer measure of t
with respect to the restriction of
the measure to s
equals the outer measure of t ∩ s
. This is an alternate version of
Measure.restrict_apply
, requiring that s
is measurable instead of t
.
If μ s ≠ 0
, then μ.restrict s ≠ 0
, in terms of NeZero
instances.
The restriction of the pushforward measure is the pushforward of the restriction. For a version
assuming only AEMeasurable
, see restrict_map_of_aemeasurable
.
If two measures agree on all measurable subsets of s
and t
, then they agree on all
measurable subsets of s ∪ t
.
This lemma shows that Inf
and restrict
commute for measures.
Extensionality results #
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using Union
).
Alias of the reverse direction of MeasureTheory.Measure.ext_iff_of_iUnion_eq_univ
.
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using Union
).
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using biUnion
).
Alias of the reverse direction of MeasureTheory.Measure.ext_iff_of_biUnion_eq_univ
.
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using biUnion
).
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using sUnion
).
Alias of the reverse direction of MeasureTheory.Measure.ext_iff_of_sUnion_eq_univ
.
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using sUnion
).
Two measures are equal if they are equal on the π-system generating the σ-algebra,
and they are both finite on an increasing spanning sequence of sets in the π-system.
This lemma is formulated using sUnion
.
Two measures are equal if they are equal on the π-system generating the σ-algebra,
and they are both finite on an increasing spanning sequence of sets in the π-system.
This lemma is formulated using iUnion
.
FiniteSpanningSetsIn.ext
is a reformulation of this lemma.
Sum of an indexed family of measures.
Instances For
Absolute continuity #
We say that μ
is absolutely continuous with respect to ν
, or that μ
is dominated by ν
,
if ν(A) = 0
implies that μ(A) = 0
.
Instances For
We say that μ
is absolutely continuous with respect to ν
, or that μ
is dominated by ν
,
if ν(A) = 0
implies that μ(A) = 0
.
Instances For
Alias of the forward direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous
.
Alias of the reverse direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous
.
Alias of the reverse direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous
.
Alias of the reverse direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous
.
Quasi measure preserving maps (a.k.a. non-singular maps) #
- measurable : Measurable f
- absolutelyContinuous : MeasureTheory.Measure.AbsolutelyContinuous (MeasureTheory.Measure.map f μa) μb
A map f : α → β
is said to be quasi measure preserving (a.k.a. non-singular) w.r.t. measures
μa
and μb
if it is measurable and μb s = 0
implies μa (f ⁻¹' s) = 0
.
Instances For
By replacing a measurable set that is almost invariant with the limsup
of its preimages, we
obtain a measurable set that is almost equal and strictly invariant.
(The liminf
would work just as well.)
The filter of sets s
such that sᶜ
has finite measure.
Instances For
The preimage of a null measurable set under a (quasi) measure preserving map is a null measurable set.