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

.

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

- measurable_set' : set α → Prop
- measurable_set_empty : c.measurable_set' ∅
- measurable_set_compl : ∀ (s : set α), c.measurable_set' s → c.measurable_set' sᶜ
- measurable_set_Union : ∀ (f : ℕ → set α), (∀ (i : ℕ), c.measurable_set' (f i)) → c.measurable_set' (⋃ (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

`measurable_set s`

means that `s`

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

)

## Equations

- measurable_set = _inst_1.measurable_set'

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

- measurable_set_singleton : ∀ (x : α), measurable_set {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₁.measurable_set' ≤ m₂.measurable_set', lt := preorder.lt._default (λ (m₁ m₂ : measurable_space α), m₁.measurable_set' ≤ m₂.measurable_set'), 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 = {measurable_set' := λ (s : set α), s ∈ g, measurable_set_empty := _, measurable_set_compl := _, measurable_set_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 α | measurable_set 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 = {measurable_set' := λ (s : set β), m.measurable_set' (f ⁻¹' s), measurable_set_empty := _, measurable_set_compl := _, measurable_set_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 = {measurable_set' := λ (s : set α), ∃ (s' : set β), m.measurable_set' s' ∧ f ⁻¹' s' = s, measurable_set_empty := _, measurable_set_compl := _, measurable_set_Union := _}

A function `f`

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

## Equations

- measurable f = ∀ ⦃t : set β⦄, measurable_set t → measurable_set (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 (measurable_set_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 := _}

- exists_measurable_subset : ∀ ⦃s : set α⦄, s ∈ f → (∃ (t : set α) (H : t ∈ f), measurable_set 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`

.