Measure spaces #
This file defines measure spaces, the almost-everywhere filter and ae_measurable functions.
measure_theory.measure_space 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 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.
α 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
measure_theory.measure_space for ways to construct measures and proving
that two measure are equal.
measure_space is a class that is a measurable space with a canonical measure.
The measure is denoted
This file does not import
measure_theory.measurable_space, but only
measure, almost everywhere, measure space
- to_outer_measure : measure_theory.outer_measure α
- m_Union : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), measurable_set (f i)) → pairwise (disjoint on f) → self.to_outer_measure.measure_of (⋃ (i : ℕ), f i) = ∑' (i : ℕ), self.to_outer_measure.measure_of (f i)
- trimmed : self.to_outer_measure.trim = self.to_outer_measure
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
measure_of 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
A version of
measure_Union_null_iff for unions indexed by Props
TODO: in the long run it would be better to combine this with
The almost everywhere filter #
The “almost everywhere” filter of co-null sets.
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.
- measure_theory.to_measurable μ s = dite (∃ (t : set α) (H : t ⊇ s), measurable_set t ∧ t =ᵐ[μ] s) (λ (h : ∃ (t : set α) (H : t ⊇ s), measurable_set t ∧ t =ᵐ[μ] s), h.some) (λ (h : ¬∃ (t : set α) (H : t ⊇ s), measurable_set t ∧ t =ᵐ[μ] s), dite (∃ (t : set α) (H : t ⊇ s), measurable_set t ∧ ∀ (u : set α), measurable_set u → ⇑μ (t ∩ u) = ⇑μ (s ∩ u)) (λ (h' : ∃ (t : set α) (H : t ⊇ s), measurable_set t ∧ ∀ (u : set α), measurable_set u → ⇑μ (t ∩ u) = ⇑μ (s ∩ u)), h'.some) (λ (h' : ¬∃ (t : set α) (H : t ⊇ s), measurable_set t ∧ ∀ (u : set α), measurable_set u → ⇑μ (t ∩ u) = ⇑μ (s ∩ u)), _.some))
A measure space is a measurable space equipped with a
measure, referred to as
Instances of this typeclass
Instances of other typeclasses for
Almost everywhere measurable functions #
A function is almost everywhere measurable if it coincides almost everywhere with a measurable
function. We define this property, called
ae_measurable f μ. It's properties are discussed in
A function is almost everywhere measurable if it coincides almost everywhere with a measurable function.
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.