# Measurable spaces and measurable functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides properties of measurable spaces and the functions and isomorphisms
between them. The definition of a measurable space is in `measure_theory.measurable_space_def`

.

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.

## Equations

- measurable_space.map f m = {measurable_set' := λ (s : set β), measurable_set (f ⁻¹' s), measurable_set_empty := _, measurable_set_compl := _, measurable_set_Union := _}

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

.

## Equations

- measurable_space.comap f m = {measurable_set' := λ (s : set α), ∃ (s' : set β), measurable_set s' ∧ f ⁻¹' s' = s, measurable_set_empty := _, measurable_set_compl := _, measurable_set_Union := _}

**Alias** of the forward direction of `measurable_iff_le_map`

.

**Alias** of the reverse direction of `measurable_iff_le_map`

.

**Alias** of the forward direction of `measurable_iff_comap_le`

.

**Alias** of the reverse 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 (measurable_set_singleton 0) measurable_const measurable_const`

,
but replacing `measurable.ite`

by `measurable.piecewise`

in that example proof does not work.

If a function coincides with a measurable function outside of a countable set, it is measurable.

## Equations

## Equations

## Equations

## Equations

## Equations

## Equations

## Equations

## Equations

- quot.measurable_space = measurable_space.map (quot.mk r) m

## Equations

## Equations

A `measurable_space`

structure on the product of two measurable spaces.

## Equations

- m₁.prod m₂ = measurable_space.comap prod.fst m₁ ⊔ measurable_space.comap prod.snd m₂

## Equations

- prod.measurable_space = m₁.prod m₂

A piecewise function on countably many pieces is measurable if all the data is measurable.

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`

.

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

**Alias** of the reverse direction of `measurable_set_set_of`

.

**Alias** of the reverse direction of `measurable_mem`

.

The sigma-algebra generated by a single set `s`

is `{∅, s, sᶜ, univ}`

.

- injective : function.injective f
- measurable : measurable f
- measurable_set_image' : ∀ ⦃s : set α⦄, measurable_set s → measurable_set (f '' s)

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 : range f → α`

”, see `measurable_embedding.measurable_range_splitting`

,
`measurable_embedding.of_measurable_inverse_range`

, and
`measurable_embedding.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
`measurable_embedding.equiv_range`

; the other one follows from
`measurable_equiv.measurable_embedding`

, `measurable_embedding.subtype_coe`

, and
`measurable_embedding.comp`

.

- to_equiv : α ≃ β
- measurable_to_fun : measurable ⇑(self.to_equiv)
- measurable_inv_fun : measurable ⇑(self.to_equiv.symm)

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

## Instances for `measurable_equiv`

- measurable_equiv.has_sizeof_inst
- measurable_equiv.has_coe_to_fun
- measurable_equiv.inhabited

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 := _}

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

## Equations

See Note [custom simps projection]

## Equations

A measurable equivalence is a measurable embedding.

Equal measurable spaces are equivalent.

## Equations

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

Any two types with unique elements are measurably equivalent.

## Equations

- measurable_equiv.of_unique_of_unique α β = {to_equiv := equiv.equiv_of_unique α β _inst_8, 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 := _}

`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 := _}

`α`

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 := _}

If `α`

has a unique term, then the type of function `α → β`

is measurably equivalent to `β`

.

## Equations

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

The space `Π i : fin 2, α i`

is measurably equivalent to `α 0 × α 1`

.

## Equations

- measurable_equiv.pi_fin_two α = {to_equiv := pi_fin_two_equiv α, measurable_to_fun := _, measurable_inv_fun := _}

The space `fin 2 → α`

is measurably equivalent to `α × α`

.

## Equations

- measurable_equiv.fin_two_arrow = measurable_equiv.pi_fin_two (λ (_x : fin 2), α)

Measurable equivalence between `Π j : fin (n + 1), α j`

and
`α i × Π j : fin n, α (fin.succ_above i j)`

.

## Equations

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

Measurable equivalence between (dependent) functions on a type and pairs of functions on
`{i // p i}`

and `{i // ¬p i}`

. See also `equiv.pi_equiv_pi_subtype_prod`

.

## Equations

- measurable_equiv.pi_equiv_pi_subtype_prod π p = {to_equiv := equiv.pi_equiv_pi_subtype_prod p π (λ (a : δ'), _inst_7 a), measurable_to_fun := _, measurable_inv_fun := _}

If `s`

is a measurable set in a measurable space, that space is equivalent
to the sum of `s`

and `sᶜ`

.

## Equations

- measurable_equiv.sum_compl hs = {to_equiv := equiv.sum_compl s (λ (a : α), _inst_7 a), measurable_to_fun := _, measurable_inv_fun := _}

Convert a measurable involutive function `f`

to a measurable permutation with
`to_fun = inv_fun = f`

. See also `function.involutive.to_perm`

.

## Equations

- measurable_equiv.of_involutive f hf hf' = {to_equiv := {to_fun := (function.involutive.to_perm f hf).to_fun, inv_fun := (function.involutive.to_perm f hf).inv_fun, left_inv := _, right_inv := _}, measurable_to_fun := hf', measurable_inv_fun := hf'}

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

as measurable spaces,
if `f`

is a measurable embedding

## Equations

- measurable_embedding.equiv_image s hf = {to_equiv := equiv.set.image f s _, measurable_to_fun := _, measurable_inv_fun := _}

The domain of `f`

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

is a measurable embedding

## Equations

- hf.equiv_range = (measurable_equiv.set.univ α).symm.trans ((measurable_embedding.equiv_image set.univ hf).trans (measurable_equiv.cast measurable_embedding.equiv_range._proof_1 measurable_embedding.equiv_range._proof_2))

The **`measurable Schröder-Bernstein Theorem**: Given measurable embeddings`

α → β`and`

β → α`, we can find a measurable equivalence`

α ≃ᵐ β`.

## Equations

- hf.schroeder_bernstein hg = let F : set α → set α := λ (A : set α), (g '' (f '' A)ᶜ)ᶜ in (let X : ℕ → set α := λ (n : ℕ), F^[n] set.univ in ⟨set.Inter X, _⟩).cases_on (λ (A : set α) (this_snd : measurable_set A ∧ F A = A), this_snd.dcases_on (λ (Ameas : measurable_set A) (Afp : F A = A), let B : set β := f '' A in (measurable_equiv.sum_compl Ameas).symm.trans (((measurable_embedding.equiv_image A hf).sum_congr (_.mpr (measurable_embedding.equiv_image Bᶜ hg).symm)).trans (measurable_equiv.sum_compl _))))

We say a measurable space is countably generated if can be generated by a countable set of sets.

## Instances of this typeclass

If a measurable space is countably generated, it admits a measurable injection
into the Cantor space `ℕ → bool`

(equipped with the product sigma algebra).

- 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 of this typeclass

- 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
- nhds_within_Icc_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
- nhds_within_uIcc_is_measurably_generated

**Alias** of the reverse direction of `filter.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`

.

### Typeclasses on `subtype measurable_set`

#

## Equations

- measurable_set.subtype.has_mem = {mem := λ (a : α) (s : subtype measurable_set), a ∈ ↑s}

## Equations

- measurable_set.subtype.has_insert = {insert := λ (a : α) (s : subtype measurable_set), ⟨has_insert.insert a ↑s, _⟩}

## Equations

- measurable_set.subtype.has_compl = {compl := λ (x : subtype measurable_set), ⟨(↑x)ᶜ, _⟩}

## Equations

- measurable_set.subtype.has_union = {union := λ (x y : subtype measurable_set), ⟨↑x ∪ ↑y, _⟩}

## Equations

- measurable_set.subtype.has_inter = {inter := λ (x y : subtype measurable_set), ⟨↑x ∩ ↑y, _⟩}

## Equations

- measurable_set.subtype.has_sdiff = {sdiff := λ (x y : subtype measurable_set), ⟨↑x \ ↑y, _⟩}

## Equations

- measurable_set.subtype.partial_order = partial_order.lift coe measurable_set.subtype.partial_order._proof_1

## Equations

- measurable_set.subtype.distrib_lattice = {sup := has_union.union measurable_set.subtype.has_union, le := partial_order.le measurable_set.subtype.partial_order, lt := partial_order.lt measurable_set.subtype.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inter.inter measurable_set.subtype.has_inter, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

## Equations

- measurable_set.subtype.boolean_algebra = {sup := distrib_lattice.sup measurable_set.subtype.distrib_lattice, le := distrib_lattice.le measurable_set.subtype.distrib_lattice, lt := distrib_lattice.lt measurable_set.subtype.distrib_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := distrib_lattice.inf measurable_set.subtype.distrib_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := has_compl.compl measurable_set.subtype.has_compl, sdiff := has_sdiff.sdiff measurable_set.subtype.has_sdiff, himp := λ (x y : subtype measurable_set), distrib_lattice.sup y xᶜ, top := bounded_order.top measurable_set.subtype.bounded_order, bot := bounded_order.bot measurable_set.subtype.bounded_order, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _}