# The Borel sigma-algebra on Polish spaces #

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 standard Borel spaces.

- A
`StandardBorelSpace α`

is a typeclass for measurable spaces which arise as the Borel sets of some Polish topology.

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

`MeasureTheory.AnalyticSet 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`ℕ → ℕ`

.`MeasureTheory.AnalyticSet.image_of_continuous`

: a continuous image of an analytic set is analytic.`MeasurableSet.analyticSet`

: 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.

`MeasurablySeparable s t`

states that there exists a measurable set containing`s`

and disjoint from`t`

.`AnalyticSet.measurablySeparable`

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.

`MeasurableSet.image_of_continuousOn_injOn`

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.measurableEmbedding`

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

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

states that a measurable injective map from a standard Borel space to a second-countable topological space is a measurable embedding.`isClopenable_iff_measurableSet`

: 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.

`PolishSpace.measurableEquivOfNotCountable`

: Any two uncountable standard Borel spaces are Borel isomorphic.`PolishSpace.Equiv.measurableEquiv`

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

### Standard Borel Spaces #

A standard Borel space is a measurable space arising as the Borel sets of some Polish topology. This is useful in situations where a space has no natural topology or the natural topology in a space is non-Polish.

To endow a standard Borel space `α`

with a compatible Polish topology, use
`letI := upgradeStandardBorel α`

. One can then use `eq_borel_upgradeStandardBorel α`

to
rewrite the `MeasurableSpace α`

instance to `borel α t`

, where `t`

is the new topology.

- polish : ∃ (x : TopologicalSpace α), BorelSpace α ∧ PolishSpace α
There exists a compatible Polish topology.

## Instances

There exists a compatible Polish topology.

A convenience class similar to `UpgradedPolishSpace`

. No instance should be registered.
Instead one should use `letI := upgradeStandardBorel α`

.

## Instances

Use as `letI := upgradeStandardBorel α`

to endow a standard Borel space `α`

with
a compatible Polish topology.

Warning: following this with `borelize α`

will cause an error. Instead, one can
rewrite with `eq_borel_upgradeStandardBorel α`

.
TODO: fix the corresponding bug in `borelize`

.

## Equations

- upgradeStandardBorel α = (fun (τ : TopologicalSpace α) (x : BorelSpace α ∧ PolishSpace α) => UpgradedStandardBorel.mk) (Classical.choose ⋯) ⋯

## Instances For

The `MeasurableSpace α`

instance on a `StandardBorelSpace`

`α`

is equal to
the borel sets of `upgradeStandardBorel α`

.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

A product of two standard Borel spaces is standard Borel.

## Equations

- ⋯ = ⋯

A product of countably many standard Borel spaces is standard Borel.

## Equations

- ⋯ = ⋯

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

.

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

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

## Equations

## Instances For

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

.

A Borel-measurable set in a Polish space is analytic.

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 standard Borel space under a measurable map is an analytic set.

Preimage of an analytic set 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

- MeasureTheory.MeasurablySeparable s t = ∃ (u : Set α), s ⊆ u ∧ Disjoint t u ∧ MeasurableSet u

## Instances For

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 `AnalyticSet.measurablySeparable`

).
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 → Z`

is a surjective Borel measurable map from a standard Borel space
to a countably separated measurable space, 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
standard Borel space.

If `f : X → Z`

is a Borel measurable map from a standard Borel space to a
countably separated measurable space then the preimage of a set `s`

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

.

If `f : X → Z`

is a Borel measurable map from a standard Borel space to a
countably separated measurable space and the range of `f`

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

is measurable
if and only if the intersection with `Set.range f`

is measurable.

If `f : X → Z`

is a Borel measurable map from a standard Borel space
to a countably separated measurable space,
then for any measurable space `β`

and `g : Z → β`

, the composition `g ∘ f`

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

to the range of `f`

is measurable.

If `f : X → Z`

is a surjective Borel measurable map from a standard Borel space
to a countably separated measurable space,
then for any measurable space `α`

and `g : Z → α`

, the composition
`g ∘ f`

is measurable if and only if `g`

is measurable.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

When the subgroup `N < G`

is not necessarily `Normal`

, we have a `CosetSpace`

as opposed
to `QuotientGroup`

(the next `instance`

).
TODO: typeclass inference should normally find this, but currently doesn't.
E.g., `MeasurableSMul G (G ⧸ Γ)`

fails to synthesize, even though `G ⧸ Γ`

is the quotient
of `G`

by the action of `Γ`

; it seems unable to pick up the `BorelSpace`

instance.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

### 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 standard Borel space,
then its image under a measurable injective map taking values in a
countably separate measurable 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 standard Borel space to a countably separated measurable space is a measurable embedding.

If one Polish topology on a type refines another, they have the same Borel sets.

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

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

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

If `s`

is a measurable set in a standard Borel space, there is a compatible Polish topology
making `s`

clopen.

A measurable subspace of a standard Borel space is standard Borel.

### The Borel Isomorphism Theorem #

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

## Equations

- PolishSpace.borelSchroederBernstein fmeas finj gmeas ginj = ⋯.schroederBernstein ⋯

## Instances For

Any uncountable standard Borel space is Borel isomorphic to the Cantor space `ℕ → Bool`

.

## Equations

## Instances For

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

## Equations

## Instances For

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

## Equations

- PolishSpace.Equiv.measurableEquiv e = if h : Countable α then { toEquiv := e, measurable_toFun := ⋯, measurable_invFun := ⋯ } else PolishSpace.measurableEquivOfNotCountable h ⋯