# Measurable spaces and measurable functions

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.

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`

.

## Main statements

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.

## 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

- is_measurable' : set α → Prop
- is_measurable_empty : c.is_measurable' ∅
- is_measurable_compl : ∀ (s : set α), c.is_measurable' s → c.is_measurable' sᶜ
- is_measurable_Union : ∀ (f : ℕ → set α), (∀ (i : ℕ), c.is_measurable' (f i)) → c.is_measurable' (⋃ (i : ℕ), f i)

A measurable space is a space equipped with a σ-algebra.

## Instances

- measure_theory.measure_space.to_measurable_space
- order_dual.measurable_space
- empty.measurable_space
- punit.measurable_space
- bool.measurable_space
- nat.measurable_space
- int.measurable_space
- rat.measurable_space
- subtype.measurable_space
- prod.measurable_space
- measurable_space.pi
- tprod.measurable_space
- sum.measurable_space
- sigma.measurable_space
- real.measurable_space
- nnreal.measurable_space
- ennreal.measurable_space
- complex.measurable_space
- continuous_linear_map.measurable_space
- measure_theory.measure.measurable_space
- Meas.measurable_space

`is_measurable s`

means that `s`

is measurable (in the ambient measure space on `α`

)

## Equations

- is_measurable = _inst_1.is_measurable'

Every set has a measurable superset. Declare this as local instance as needed.

- is_measurable_singleton : ∀ (x : α), is_measurable {x}

A typeclass mixin for `measurable_space`

s such that each singleton is measurable.

## Equations

- measurable_space.partial_order = {le := λ (m₁ m₂ : measurable_space α), m₁.is_measurable' ≤ m₂.is_measurable', lt := preorder.lt._default (λ (m₁ m₂ : measurable_space α), m₁.is_measurable' ≤ m₂.is_measurable'), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

- basic : ∀ {α : Type u_1} (s : set (set α)) (u : set α), u ∈ s → measurable_space.generate_measurable s u
- empty : ∀ {α : Type u_1} (s : set (set α)), measurable_space.generate_measurable s ∅
- compl : ∀ {α : Type u_1} (s : set (set α)) (s_1 : set α), measurable_space.generate_measurable s s_1 → measurable_space.generate_measurable s s_1ᶜ
- union : ∀ {α : Type u_1} (s : set (set α)) (f : ℕ → set α), (∀ (n : ℕ), measurable_space.generate_measurable s (f n)) → measurable_space.generate_measurable s (⋃ (i : ℕ), f i)

The smallest σ-algebra containing a collection `s`

of basic sets

Construct the smallest measure space containing a collection of basic sets

## Equations

If `g`

is a collection of subsets of `α`

such that the `σ`

-algebra generated from `g`

contains
the same sets as `g`

, then `g`

was already a `σ`

-algebra.

## Equations

- measurable_space.mk_of_closure g hg = {is_measurable' := λ (s : set α), s ∈ g, is_measurable_empty := _, is_measurable_compl := _, is_measurable_Union := _}

We get a Galois insertion between `σ`

-algebras on `α`

and `set (set α)`

by using `generate_from`

on one side and the collection of measurable sets on the other side.

## Equations

- measurable_space.gi_generate_from = {choice := λ (g : set (set α)) (hg : {t : set α | is_measurable t} ≤ g), measurable_space.mk_of_closure g _, gc := _, le_l_u := _, choice_eq := _}

## Equations

The forward image of a measure space under a function. `map f m`

contains the sets `s : set β`

whose preimage under `f`

is measurable.

## Equations

- measurable_space.map f m = {is_measurable' := λ (s : set β), m.is_measurable' (f ⁻¹' s), is_measurable_empty := _, is_measurable_compl := _, is_measurable_Union := _}

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 `β`

.

## Equations

- measurable_space.comap f m = {is_measurable' := λ (s : set α), ∃ (s' : set β), m.is_measurable' s' ∧ f ⁻¹' s' = s, is_measurable_empty := _, is_measurable_compl := _, is_measurable_Union := _}

A function `f`

between measurable spaces is measurable if the preimage of every
measurable set is measurable.

## Equations

- measurable f = ∀ ⦃t : set β⦄, is_measurable t → is_measurable (f ⁻¹' t)

**Alias** of `measurable_iff_le_map`

.

**Alias** of `measurable_iff_le_map`

.

**Alias** of `measurable_iff_comap_le`

.

**Alias** of `measurable_iff_comap_le`

.

this is slightly different from `measurable.piecewise`

. It can be used to show
`measurable (ite (x=0) 0 1)`

by
`exact measurable.ite (is_measurable_singleton 0) measurable_const measurable_const`

,
but replacing `measurable.ite`

by `measurable.piecewise`

in that example proof does not work.

## Equations

## Equations

## Equations

## Equations

## Equations

## Equations

- measurable_space.pi = ⨆ (a : δ), measurable_space.comap (λ (b : Π (a : δ), «π» a), b a) (m a)

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

## Equations

## Equations

- sigma.measurable_space = ⨅ (a : α), measurable_space.map (sigma.mk a) (m a)

- to_equiv : α ≃ β
- measurable_to_fun : measurable c.to_equiv.to_fun
- measurable_inv_fun : measurable c.to_equiv.inv_fun

Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.

Any measurable space is equivalent to itself.

## Equations

- measurable_equiv.refl α = {to_equiv := equiv.refl α, measurable_to_fun := _, measurable_inv_fun := _}

## Equations

- measurable_equiv.inhabited = {default := measurable_equiv.refl α _inst_1}

The composition of equivalences between measurable spaces.

## Equations

- ab.trans bc = {to_equiv := ab.to_equiv.trans bc.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}

The inverse of an equivalence between measurable spaces.

## Equations

- ab.symm = {to_equiv := ab.to_equiv.symm, measurable_to_fun := _, measurable_inv_fun := _}

Equal measurable spaces are equivalent.

## Equations

- measurable_equiv.cast h hi = {to_equiv := equiv.cast h, measurable_to_fun := _, measurable_inv_fun := _}

Products of equivalent measurable spaces are equivalent.

## Equations

- ab.prod_congr cd = {to_equiv := ab.to_equiv.prod_congr cd.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}

Products of measurable spaces are symmetric.

## Equations

- measurable_equiv.prod_comm = {to_equiv := equiv.prod_comm α β, measurable_to_fun := _, measurable_inv_fun := _}

Products of measurable spaces are associative.

## Equations

- measurable_equiv.prod_assoc = {to_equiv := equiv.prod_assoc α β γ, measurable_to_fun := _, measurable_inv_fun := _}

Sums of measurable spaces are symmetric.

## Equations

- ab.sum_congr cd = {to_equiv := ab.to_equiv.sum_congr cd.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}

`set.prod s t ≃ (s × t)`

as measurable spaces.

## Equations

- measurable_equiv.set.prod s t = {to_equiv := equiv.set.prod s t, measurable_to_fun := _, measurable_inv_fun := _}

`univ α ≃ α`

as measurable spaces.

## Equations

- measurable_equiv.set.univ α = {to_equiv := equiv.set.univ α, measurable_to_fun := _, measurable_inv_fun := _}

`{a} ≃ unit`

as measurable spaces.

## Equations

- measurable_equiv.set.singleton a = {to_equiv := equiv.set.singleton a, measurable_to_fun := _, measurable_inv_fun := _}

A set is equivalent to its image under a function `f`

as measurable spaces,
if `f`

is an injective measurable function that sends measurable sets to measurable sets.

## Equations

- measurable_equiv.set.image f s hf hfm hfi = {to_equiv := equiv.set.image f s hf, measurable_to_fun := _, measurable_inv_fun := _}

The domain of `f`

is equivalent to its range as measurable spaces,
if `f`

is an injective measurable function that sends measurable sets to measurable sets.

## Equations

- measurable_equiv.set.range f hf hfm hfi = (measurable_equiv.set.univ α).symm.trans ((measurable_equiv.set.image f set.univ hf hfm hfi).trans (measurable_equiv.cast _ _))

`α`

is equivalent to its image in `α ⊕ β`

as measurable spaces.

## Equations

- measurable_equiv.set.range_inl = {to_equiv := {to_fun := λ (ab : ↥(set.range sum.inl)), measurable_equiv.set.range_inl._match_1 ab, inv_fun := λ (a : α), ⟨sum.inl a, _⟩, left_inv := _, right_inv := _}, measurable_to_fun := _, measurable_inv_fun := _}
- measurable_equiv.set.range_inl._match_1 ⟨sum.inr b, p⟩ = have this : false, from _, this.elim
- measurable_equiv.set.range_inl._match_1 ⟨sum.inl a, _x⟩ = a

`β`

is equivalent to its image in `α ⊕ β`

as measurable spaces.

## Equations

- measurable_equiv.set.range_inr = {to_equiv := {to_fun := λ (ab : ↥(set.range sum.inr)), measurable_equiv.set.range_inr._match_1 ab, inv_fun := λ (b : β), ⟨sum.inr b, _⟩, left_inv := _, right_inv := _}, measurable_to_fun := _, measurable_inv_fun := _}
- measurable_equiv.set.range_inr._match_1 ⟨sum.inr b, _x⟩ = b
- measurable_equiv.set.range_inr._match_1 ⟨sum.inl a, p⟩ = have this : false, from _, this.elim

Products distribute over sums (on the right) as measurable spaces.

## Equations

- measurable_equiv.sum_prod_distrib α β γ = {to_equiv := equiv.sum_prod_distrib α β γ, measurable_to_fun := _, measurable_inv_fun := _}

Products distribute over sums (on the left) as measurable spaces.

Products distribute over sums as measurable spaces.

## Equations

- measurable_equiv.sum_prod_sum α β γ δ = (measurable_equiv.sum_prod_distrib α β (γ ⊕ δ)).trans ((measurable_equiv.prod_sum_distrib α γ δ).sum_congr (measurable_equiv.prod_sum_distrib β γ δ))

A family of measurable equivalences `Π a, β₁ a ≃ᵐ β₂ a`

generates a measurable equivalence
between `Π a, β₁ a`

and `Π a, β₂ a`

.

## Equations

- measurable_equiv.Pi_congr_right e = {to_equiv := equiv.Pi_congr_right (λ (a : δ'), (e a).to_equiv), measurable_to_fun := _, measurable_inv_fun := _}

Pi-types are measurably equivalent to iterated products.

## Equations

- measurable_equiv.pi_measurable_equiv_tprod hnd h = {to_equiv := list.tprod.pi_equiv_tprod hnd h, measurable_to_fun := _, measurable_inv_fun := _}

A pi-system is a collection of subsets of `α`

that is closed under intersections of sets that
are not disjoint. Usually it is also required that the collection is nonempty, but we don't do
that here.

- has : set α → Prop
- has_empty : c.has ∅
- has_compl : ∀ {a : set α}, c.has a → c.has aᶜ
- has_Union_nat : ∀ {f : ℕ → set α}, pairwise (disjoint on f) → (∀ (i : ℕ), c.has (f i)) → c.has (⋃ (i : ℕ), f i)

A Dynkin system is a collection of subsets of a type `α`

that contains the empty set,
is closed under complementation and under countable union of pairwise disjoint sets.
The disjointness condition is the only difference with `σ`

-algebras.

The main purpose of Dynkin systems is to provide a powerful induction rule for σ-algebras generated by intersection stable set systems.

A Dynkin system is also known as a "λ-system" or a "d-system".

## Equations

- measurable_space.dynkin_system.partial_order = {le := λ (m₁ m₂ : measurable_space.dynkin_system α), m₁.has ≤ m₂.has, lt := preorder.lt._default (λ (m₁ m₂ : measurable_space.dynkin_system α), m₁.has ≤ m₂.has), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

Every measurable space (σ-algebra) forms a Dynkin system

## Equations

- measurable_space.dynkin_system.of_measurable_space m = {has := m.is_measurable', has_empty := _, has_compl := _, has_Union_nat := _}

- basic : ∀ {α : Type u_1} (s : set (set α)) (t : set α), t ∈ s → measurable_space.dynkin_system.generate_has s t
- empty : ∀ {α : Type u_1} (s : set (set α)), measurable_space.dynkin_system.generate_has s ∅
- compl : ∀ {α : Type u_1} (s : set (set α)) {a : set α}, measurable_space.dynkin_system.generate_has s a → measurable_space.dynkin_system.generate_has s aᶜ
- Union : ∀ {α : Type u_1} (s : set (set α)) {f : ℕ → set α}, pairwise (disjoint on f) → (∀ (i : ℕ), measurable_space.dynkin_system.generate_has s (f i)) → measurable_space.dynkin_system.generate_has s (⋃ (i : ℕ), f i)

The least Dynkin system containing a collection of basic sets. This inductive type gives the underlying collection of sets.

The least Dynkin system containing a collection of basic sets.

## Equations

- measurable_space.dynkin_system.generate s = {has := measurable_space.dynkin_system.generate_has s, has_empty := _, has_compl := _, has_Union_nat := _}

If a Dynkin system is closed under binary intersection, then it forms a `σ`

-algebra.

## Equations

- d.to_measurable_space h_inter = {is_measurable' := d.has, is_measurable_empty := _, is_measurable_compl := _, is_measurable_Union := _}

If `s`

is in a Dynkin system `d`

, we can form the new Dynkin system `{s ∩ t | t ∈ d}`

.

## Equations

- d.restrict_on h = {has := λ (t : set α), d.has (t ∩ s), has_empty := _, has_compl := _, has_Union_nat := _}

If we have a collection of sets closed under binary intersections, then the Dynkin system it generates is equal to the σ-algebra it generates. This result is known as the π-λ theorem. A collection of sets closed under binary intersection is called a "π-system" if it is non-empty.

- exists_measurable_subset : ∀ ⦃s : set α⦄, s ∈ f → (∃ (t : set α) (H : t ∈ f), is_measurable t ∧ t ⊆ s)

A filter `f`

is measurably generates if each `s ∈ f`

includes a measurable `t ∈ f`

.

## Instances

- filter.is_measurably_generated_bot
- filter.is_measurably_generated_top
- filter.inf_is_measurably_generated
- filter.infi_is_measurably_generated
- measure_theory.ae_is_measurably_generated
- nhds_is_measurably_generated
- nhds_within_Ici_is_measurably_generated
- nhds_within_Iic_is_measurably_generated
- at_top_is_measurably_generated
- at_bot_is_measurably_generated
- nhds_within_Ioi_is_measurably_generated
- nhds_within_Iio_is_measurably_generated

**Alias** of `principal_is_measurably_generated_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 `generate_from_prod_eq`

.