This file defines measurable spaces and the functions and isomorphisms between them.
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.
The main theorem of this file is Dynkin's π-λ theorem, which appears here as an induction principle induction_on_inter. Suppose s is a collection of subsets of α such that the intersection of two members of s belongs to s whenever it is nonempty. Let m be the σ-algebra generated by s. In order to check that a predicate C holds on every member of m, it suffices to check that C holds on the members of s and that C is preserved by complementation and disjoint countable unions.
Measurability of a function f : α → β between measurable spaces is defined in terms of the Galois connection induced by f.
measurable space, measurable function, dynkin system
is_measurable s means that s is measurable (in the ambient measure space on α)
The smallest σ-algebra containing a collection s of basic sets
Construct the smallest measure space containing a collection of basic sets
The forward image of a measure space under a function. map f m contains the sets s : set β whose preimage under f is measurable.
The reverse image of a measure space under a function. comap f m contains the sets s : set α such that s is the f-preimage of a measurable set in β.
A function f between measurable spaces is measurable if the preimage of every measurable set is measurable.
Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.
Dynkin systems The main purpose of Dynkin systems is to provide a powerful induction rule for σ-algebras generated by intersection stable set systems.
The least Dynkin system containing a collection of basic sets.