Measure spaces #
This file defines measure spaces, the almost-everywhere filter and ae_measurable functions.
See 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.
Measures on α
form a complete lattice, and are closed under scalar multiplication with ℝ≥0∞
.
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.
See the documentation of MeasureTheory.MeasureSpace
for ways to construct measures and proving
that two measure are equal.
A MeasureSpace
is a class that is a measurable space with a canonical measure.
The measure is denoted volume
.
This file does not import MeasureTheory.MeasurableSpace.Basic
, but only MeasurableSpace.Defs
.
References #
Tags #
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.
- trim_le : self.trim ≤ self.toOuterMeasure
Instances For
Notation for Measure
with respect to a non-standard σ-algebra in the domain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- MeasureTheory.Measure.instFunLike = { coe := fun (μ : MeasureTheory.Measure α) => ⇑μ.toOuterMeasure, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
General facts about measures #
Obtain a measure by giving a countably additive function that sends ∅
to 0
.
Equations
- MeasureTheory.Measure.ofMeasurable m m0 mU = { toOuterMeasure := MeasureTheory.inducedOuterMeasure m ⋯ m0, m_iUnion := ⋯, trim_le := ⋯ }
Instances For
A variant of measure_eq_iInf
which has a single iInf
. This is useful when applying a
lemma next that only works for non-empty infima, in which case you can use
nonempty_measurable_superset
.
For every set there exists a measurable superset of the same measure.
For every set s
and a countable collection of measures μ i
there exists a measurable
superset t ⊇ s
such that each measure μ i
takes the same value on s
and t
.
The almost everywhere filter #
Given a predicate on β
and Set α
where both α
and β
are measurable spaces, if the
predicate holds for almost every x : β
and
∅ : Set α
- a family of sets generating the σ-algebra of
α
Moreover, if for almost everyx : β
, the predicate is closed under complements and countable disjoint unions, then the predicate holds for almost everyx : β
and all measurable sets ofα
.
This is an AE version of MeasurableSpace.induction_on_inter
where the condition is dependent
on a measurable space β
.
A measurable set t ⊇ s
such that μ t = μ s
. It even satisfies μ (t ∩ u) = μ (s ∩ u)
for
any measurable set u
if μ s ≠ ∞
, see measure_toMeasurable_inter
.
(This property holds without the assumption μ s ≠ ∞
when the space is s-finite -- for example
σ-finite), see measure_toMeasurable_inter_of_sFinite
).
If s
is a null measurable set, then
we also have t =ᵐ[μ] s
, see NullMeasurableSet.toMeasurable_ae_eq
.
This notion is sometimes called a "measurable hull" in the literature.
Equations
Instances For
A measure space is a measurable space equipped with a
measure, referred to as volume
.
- measurableSet_empty : MeasureTheory.MeasureSpace.toMeasurableSpace.MeasurableSet' ∅
- volume : MeasureTheory.Measure α
volume
is the canonical measure onα
.
Instances
∀ᵐ a, p a
means that p a
for a.e. a
, i.e. p
holds true away from a null set.
This is notation for Filter.Eventually P (MeasureTheory.ae MeasureSpace.volume)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
∃ᵐ a, p a
means that p
holds frequently, i.e. on a set of positive measure,
w.r.t. the volume measure.
This is notation for Filter.Frequently P (MeasureTheory.ae MeasureSpace.volume)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The tactic exact volume
, to be used in optional (autoParam
) arguments.
Equations
- MeasureTheory.tacticVolume_tac = Lean.ParserDescr.node `MeasureTheory.tacticVolume_tac 1024 (Lean.ParserDescr.nonReservedSymbol "volume_tac" false)
Instances 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 AEMeasurable f μ
. It's properties are discussed in
MeasureTheory.MeasureSpace
.
A function is almost everywhere measurable if it coincides almost everywhere with a measurable function.
Equations
- AEMeasurable f μ = ∃ (g : α → β), Measurable g ∧ f =ᵐ[μ] g
Instances For
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.
Equations
- AEMeasurable.mk f h = Classical.choose h