Measurable spaces and measurable functions #
This file provides properties of measurable spaces and the functions and isomorphisms
between them. The definition of a measurable space is in MeasureTheory.MeasurableSpaceDef
.
A measurable space is a set equipped with a σ-algebra, a collection of subsets closed under complementation and countable union. A function between measurable spaces is measurable if the preimage of each measurable subset is measurable.
σ-algebras on a fixed set α
form a complete lattice. Here we order
σ-algebras by writing m₁ ≤ m₂
if every set which is m₁
-measurable is
also m₂
-measurable (that is, m₁
is a subset of m₂
). In particular, any
collection of subsets of α
generates a smallest σ-algebra which
contains all of them. A function f : α → β
induces a Galois connection
between the lattices of σ-algebras on α
and β
.
A measurable equivalence between measurable spaces is an equivalence which respects the σ-algebras, that is, for which both directions of the equivalence are measurable functions.
We say that a filter f
is measurably generated if every set s ∈ f
includes a measurable
set t ∈ f
. This property is useful, e.g., to extract a measurable witness of Filter.Eventually
.
Notation #
- We write
α ≃ᵐ β
for measurable equivalences between the measurable spacesα
andβ
. This should not be confused with≃ₘ
which is used for diffeomorphisms between manifolds.
Implementation notes #
Measurability of a function f : α → β
between measurable spaces is
defined in terms of the Galois connection induced by f.
References #
- https://en.wikipedia.org/wiki/Measurable_space
- https://en.wikipedia.org/wiki/Sigma-algebra
- https://en.wikipedia.org/wiki/Dynkin_system
Tags #
measurable space, σ-algebra, measurable function, measurable equivalence, dynkin system, π-λ theorem, π-system
The forward image of a measurable space under a function. map f m
contains the sets
s : Set β
whose preimage under f
is measurable.
Instances For
The reverse image of a measurable space under a function. comap f m
contains the sets
s : Set α
such that s
is the f
-preimage of a measurable set in β
.
Instances For
Alias of the forward direction of measurable_iff_le_map
.
Alias of the reverse direction of measurable_iff_le_map
.
Alias of the reverse direction of measurable_iff_comap_le
.
Alias of the forward direction of measurable_iff_comap_le
.
A version of measurable_const
that assumes f x = f y
for all x, y
. This version works
for functions between empty types.
This is slightly different from Measurable.piecewise
. It can be used to show
Measurable (ite (x=0) 0 1)
by
exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const
,
but replacing Measurable.ite
by Measurable.piecewise
in that example proof does not work.
The measurability of a set A
is equivalent to the measurability of the indicator function
which takes a constant value b ≠ 0
on a set A
and 0
elsewhere.
If a function coincides with a measurable function outside of a countable set, it is measurable.
Alias of Measurable.subtype_coe
.
A MeasurableSpace
structure on the product of two measurable spaces.
Instances For
A piecewise function on countably many pieces is measurable if all the data is measurable.
Let t i
be a countable covering of a set T
by measurable sets. Let f i : t i → β
be a
family of functions that agree on the intersections t i ∩ t j
. Then the function
Set.iUnionLift t f _ _ : T → β
, defined as f i ⟨x, hx⟩
for hx : x ∈ t i
, is measurable.
Let t i
be a countable covering of α
by measurable sets. Let f i : t i → β
be a family of
functions that agree on the intersections t i ∩ t j
. Then the function Set.liftCover t f _ _
,
defined as f i ⟨x, hx⟩
for hx : x ∈ t i
, is measurable.
Let t i
be a nonempty countable family of measurable sets in α
. Let g i : α → β
be a
family of measurable functions such that g i
agrees with g j
on t i ∩ t j
. Then there exists
a measurable function f : α → β
that agrees with each g i
on t i
.
We only need the assumption [Nonempty ι]
to prove [Nonempty (α → β)]
.
Given countably many disjoint measurable sets t n
and countably many measurable
functions g n
, one can construct a measurable function that coincides with g n
on t n
.
The function update f a : π a → Π a, π a
is always measurable.
This doesn't require f
to be measurable.
This should not be confused with the statement that update f a x
is measurable.
Equations
- TProd.instMeasurableSpace π [] = PUnit.instMeasurableSpace
- TProd.instMeasurableSpace π (head :: is) = Prod.instMeasurableSpace
Alias of the reverse direction of measurableSet_inl_image
.
Alias of the reverse direction of measurableSet_inr_image
.
- injective : Function.Injective f
A measurable embedding is injective.
- measurable : Measurable f
A measurable embedding is a measurable function.
- measurableSet_image' : ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)
The image of a measurable set under a measurable embedding is a measurable set.
A map f : α → β
is called a measurable embedding if it is injective, measurable, and sends
measurable sets to measurable sets. The latter assumption can be replaced with “f
has measurable
inverse g : Set.range f → α
”, see MeasurableEmbedding.measurable_rangeSplitting
,
MeasurableEmbedding.of_measurable_inverse_range
, and
MeasurableEmbedding.of_measurable_inverse
.
One more interpretation: f
is a measurable embedding if it defines a measurable equivalence to its
range and the range is a measurable set. One implication is formalized as
MeasurableEmbedding.equivRange
; the other one follows from
MeasurableEquiv.measurableEmbedding
, MeasurableEmbedding.subtype_coe
, and
MeasurableEmbedding.comp
.
Instances For
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- measurable_toFun : Measurable ↑s.toEquiv
The forward function of a measurable equivalence is measurable.
- measurable_invFun : Measurable ↑s.symm
The inverse function of a measurable equivalence is measurable.
Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.
Instances For
Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.
Instances For
Any measurable space is equivalent to itself.
Instances For
The composition of equivalences between measurable spaces.
Instances For
The inverse of an equivalence between measurable spaces.
Instances For
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Instances For
See Note [custom simps projection]
Instances For
A measurable equivalence is a measurable embedding.
Equal measurable spaces are equivalent.
Instances For
Any two types with unique elements are measurably equivalent.
Instances For
Products of equivalent measurable spaces are equivalent.
Instances For
Products of measurable spaces are symmetric.
Instances For
Products of measurable spaces are associative.
Instances For
Sums of measurable spaces are symmetric.
Instances For
s ×ˢ t ≃ (s × t)
as measurable spaces.
Instances For
univ α ≃ α
as measurable spaces.
Instances For
{a} ≃ Unit
as measurable spaces.
Instances For
α
is equivalent to its image in α ⊕ β
as measurable spaces.
Instances For
β
is equivalent to its image in α ⊕ β
as measurable spaces.
Instances For
Products distribute over sums (on the right) as measurable spaces.
Instances For
Products distribute over sums (on the left) as measurable spaces.
Instances For
Products distribute over sums as measurable spaces.
Instances For
A family of measurable equivalences Π a, β₁ a ≃ᵐ β₂ a
generates a measurable equivalence
between Π a, β₁ a
and Π a, β₂ a
.
Instances For
Pi-types are measurably equivalent to iterated products.
Instances For
If α
has a unique term, then the type of function α → β
is measurably equivalent to β
.
Instances For
The space Π i : Fin 2, α i
is measurably equivalent to α 0 × α 1
.
Instances For
The space Fin 2 → α
is measurably equivalent to α × α
.
Instances For
Measurable equivalence between (dependent) functions on a type and pairs of functions on
{i // p i}
and {i // ¬p i}
. See also Equiv.piEquivPiSubtypeProd
.
Instances For
If s
is a measurable set in a measurable space, that space is equivalent
to the sum of s
and sᶜ
.
Instances For
A set is equivalent to its image under a function f
as measurable spaces,
if f
is a measurable embedding
Instances For
The domain of f
is equivalent to its range as measurable spaces,
if f
is a measurable embedding
Instances For
The measurable Schröder-Bernstein Theorem: given measurable embeddings
α → β
and β → α
, we can find a measurable equivalence α ≃ᵐ β
.
Instances For
- isCountablyGenerated : ∃ b, Set.Countable b ∧ m = MeasurableSpace.generateFrom b
We say a measurable space is countably generated if it can be generated by a countable set of sets.
Instances
If a measurable space is countably generated and separates points, it admits a measurable
injection into the Cantor space ℕ → Bool
(equipped with the product sigma algebra).
A filter f
is measurably generates if each s ∈ f
includes a measurable t ∈ f
.
Instances
Alias of the reverse direction of Filter.principal_isMeasurablyGenerated_iff
.
We say that a collection of sets is countably spanning if a countable subset spans the
whole type. This is a useful condition in various parts of measure theory. For example, it is
a needed condition to show that the product of two collections generate the product sigma algebra,
see generateFrom_prod_eq
.