# The Borel sigma-algebra on Polish spaces #

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

We discuss several results pertaining to the relationship between the topology and the Borel structure on Polish spaces.

## Main definitions and results #

First, we define the class of analytic sets and establish its basic properties.

`measure_theory.analytic_set s`

: a set in a topological space is analytic if it is the continuous image of a Polish space. Equivalently, it is empty, or the image of`ℕ → ℕ`

.`measure_theory.analytic_set.image_of_continuous`

: a continuous image of an analytic set is analytic.`measurable_set.analytic_set`

: in a Polish space, any Borel-measurable set is analytic.

Then, we show Lusin's theorem that two disjoint analytic sets can be separated by Borel sets.

`measurably_separable s t`

states that there exists a measurable set containing`s`

and disjoint from`t`

.`analytic_set.measurably_separable`

shows that two disjoint analytic sets are separated by a Borel set.

We then prove the Lusin-Souslin theorem that a continuous injective image of a Borel subset of a Polish space is Borel. The proof of this nontrivial result relies on the above results on analytic sets.

`measurable_set.image_of_continuous_on_inj_on`

asserts that, if`s`

is a Borel measurable set in a Polish space, then the image of`s`

under a continuous injective map is still Borel measurable.`continuous.measurable_embedding`

states that a continuous injective map on a Polish space is a measurable embedding for the Borel sigma-algebra.`continuous_on.measurable_embedding`

is the same result for a map restricted to a measurable set on which it is continuous.`measurable.measurable_embedding`

states that a measurable injective map from a Polish space to a second-countable topological space is a measurable embedding.`is_clopenable_iff_measurable_set`

: in a Polish space, a set is clopenable (i.e., it can be made open and closed by using a finer Polish topology) if and only if it is Borel-measurable.

We use this to prove several versions of the Borel isomorphism theorem.

`polish_space.measurable_equiv_of_not_countable`

: Any two uncountable Polish spaces are Borel isomorphic.`polish_space.equiv.measurable_equiv`

: Any two Polish spaces of the same cardinality are Borel isomorphic.

### Analytic sets #

An analytic set is a set which is the continuous image of some Polish space. There are several
equivalent characterizations of this definition. For the definition, we pick one that avoids
universe issues: a set is analytic if and only if it is a continuous image of `ℕ → ℕ`

(or if it
is empty). The above more usual characterization is given
in `analytic_set_iff_exists_polish_space_range`

.

Warning: these are analytic sets in the context of descriptive set theory (which is why they are
registered in the namespace `measure_theory`

). They have nothing to do with analytic sets in the
context of complex analysis.

The image of an open set under a continuous map is analytic.

A set is analytic if and only if it is the continuous image of some Polish space.

The continuous image of an analytic set is analytic

A countable intersection of analytic sets is analytic.

A countable union of analytic sets is analytic.

Given a Borel-measurable set in a Polish space, there exists a finer Polish topology making
it clopen. This is in fact an equivalence, see `is_clopenable_iff_measurable_set`

.

Given a Borel-measurable function from a Polish space to a second-countable space, there exists a finer Polish topology on the source space for which the function is continuous.

The image of a measurable set in a Polish space under a measurable map is an analytic set.

### Separating sets with measurable sets #

Two sets `u`

and `v`

in a measurable space are measurably separable if there
exists a measurable set containing `u`

and disjoint from `v`

.
This is mostly interesting for Borel-separable sets.

## Equations

- measure_theory.measurably_separable s t = ∃ (u : set α), s ⊆ u ∧ disjoint t u ∧ measurable_set u

The hard part of the Lusin separation theorem saying that two disjoint analytic sets are
contained in disjoint Borel sets (see the full statement in `analytic_set.measurably_separable`

).
Here, we prove this when our analytic sets are the ranges of functions from `ℕ → ℕ`

.

The Lusin separation theorem: if two analytic sets are disjoint, then they are contained in disjoint Borel sets.

**Suslin's Theorem**: in a Hausdorff topological space, an analytic set with an analytic
complement is measurable.

### Measurability of preimages under measurable maps #

If `f : X → Y`

is a surjective Borel measurable map from a Polish space to a topological space
with second countable topology, then the preimage of a set `s`

is measurable if and only if the set
is measurable.
One implication is the definition of measurability, the other one heavily relies on `X`

being a
Polish space.

If `f : X → Y`

is a Borel measurable map from a Polish space to a topological space with second
countable topology, then the preimage of a set `s`

is measurable if and only if the set is
measurable in `set.range f`

.

If `f : X → Y`

is a Borel measurable map from a Polish space to a topological space with second
countable topology and the range of `f`

is measurable, then the preimage of a set `s`

is measurable
if and only if the intesection with `set.range f`

is measurable.

If `f : X → Y`

is a Borel measurable map from a Polish space to a topological space with second
countable topology, then for any measurable space `β`

and `g : Y → β`

, the composition `g ∘ f`

is
measurable if and only if the restriction of `g`

to the range of `f`

is measurable.

If `f : X → Y`

is a surjective Borel measurable map from a Polish space to a topological space
with second countable topology, then for any measurable space `α`

and `g : Y → α`

, the composition
`g ∘ f`

is measurable if and only if `g`

is measurable.

### Injective images of Borel sets #

The Lusin-Souslin theorem: the range of a continuous injective function defined on a Polish space is Borel-measurable.

The Lusin-Souslin theorem: if `s`

is Borel-measurable in a Polish space, then its image under
a continuous injective map is also Borel-measurable.

The Lusin-Souslin theorem: if `s`

is Borel-measurable in a Polish space, then its image under
a measurable injective map taking values in a second-countable topological space
is also Borel-measurable.

An injective continuous function on a Polish space is a measurable embedding.

If `s`

is Borel-measurable in a Polish space and `f`

is continuous injective on `s`

, then
the restriction of `f`

to `s`

is a measurable embedding.

An injective measurable function from a Polish space to a second-countable topological space is a measurable embedding.

In a Polish space, a set is clopenable if and only if it is Borel-measurable.

The set of points for which a measurable sequence of functions converges is measurable.

### The Borel Isomorphism Theorem #

If two Polish spaces admit Borel measurable injections to one another, then they are Borel isomorphic.

## Equations

- polish_space.borel_schroeder_bernstein fmeas finj gmeas ginj = _.schroeder_bernstein _

Any uncountable Polish space is Borel isomorphic to the Cantor space `ℕ → bool`

.

The **Borel Isomorphism Theorem**: Any two uncountable Polish spaces are Borel isomorphic.

The **Borel Isomorphism Theorem**: If two Polish spaces have the same cardinality,
they are Borel isomorphic.

## Equations

- polish_space.equiv.measurable_equiv e = dite (countable α) (λ (h : countable α), let _inst : countable α := h, _inst_9 : countable β := _ in {to_equiv := e, measurable_to_fun := _, measurable_inv_fun := _}) (λ (h : ¬countable α), polish_space.measurable_equiv_of_not_countable h _)

Any Polish Borel space is measurably equivalent to a subset of the reals.

Any Polish Borel space embeds measurably into the reals.