Measure spaces #
This file defines measure spaces, the almost-everywhere filter and ae_measurable functions.
MeasureTheory.MeasureSpace for their properties and for extended documentation.
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 sum of the measures 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, an outer 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.
α form a complete lattice, and are closed under scalar multiplication with
Implementation notes #
μ : Measure α,
μ s is the value of the outer measure applied to
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.
See the documentation of
MeasureTheory.MeasureSpace for ways to construct measures and proving
that two measure are equal.
This file does not import
MeasureTheory.MeasurableSpace.Basic, but only
measure, almost everywhere, measure space
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.
Measure projections for a measure space.
For measurable sets this returns the measure assigned by the
measureOf field in
But we can extend this to all sets, but using the outer measure. This gives us monotonicity and
subadditivity for all sets.
General facts about measures #
Obtain a measure by giving a countably additive function that sends
For every set
s and a countable collection of measures
μ i there exists a measurable
t ⊇ s such that each measure
μ i takes the same value on
The almost everywhere filter #
A measurable set
t ⊇ s such that
μ t = μ s. It even satisfies
μ (t ∩ u) = μ (s ∩ u) for
any measurable set
μ s ≠ ∞, see
(This property holds without the assumption
μ s ≠ ∞ when the space is sigma-finite,
s is a null measurable set, then
we also have
t =ᵐ[μ] s, see
This notion is sometimes called a "measurable hull" in the literature.
A measure space is a measurable space equipped with a
measure, referred to as
Almost everywhere measurable functions #
A function is almost everywhere measurable if it coincides almost everywhere with a measurable
function. We define this property, called
AEMeasurable f μ. It's properties are discussed in
Given an almost everywhere measurable function
f, associate to it a measurable function
that coincides with it almost everywhere.
f is explicit in the definition to make sure that
it shows in pretty-printing.