# mathlib3documentation

measure_theory.constructions.polish

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

@[irreducible]
def measure_theory.analytic_set {α : Type u_1} (s : set α) :
Prop

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.

Equations
theorem measure_theory.analytic_set_range_of_polish_space {α : Type u_1} {β : Type u_2} [polish_space β] {f : β α} (f_cont : continuous f) :
theorem is_open.analytic_set_image {α : Type u_1} {β : Type u_2} [polish_space β] {s : set β} (hs : is_open s) {f : β α} (f_cont : continuous f) :

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

theorem measure_theory.analytic_set_iff_exists_polish_space_range {α : Type u_1} {s : set α} :
(β : Type) (h : (h' : (f : β α), = s

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

theorem measure_theory.analytic_set.image_of_continuous_on {α : Type u_1} {β : Type u_2} {s : set α} (hs : measure_theory.analytic_set s) {f : α β} (hf : s) :

The continuous image of an analytic set is analytic

theorem measure_theory.analytic_set.image_of_continuous {α : Type u_1} {β : Type u_2} {s : set α} (hs : measure_theory.analytic_set s) {f : α β} (hf : continuous f) :
theorem measure_theory.analytic_set.Inter {α : Type u_1} {ι : Type u_2} [hι : nonempty ι] [countable ι] [t2_space α] {s : ι set α} (hs : (n : ι), ) :

A countable intersection of analytic sets is analytic.

theorem measure_theory.analytic_set.Union {α : Type u_1} {ι : Type u_2} [countable ι] {s : ι set α} (hs : (n : ι), ) :

A countable union of analytic sets is analytic.

theorem is_closed.analytic_set {α : Type u_1} [polish_space α] {s : set α} (hs : is_closed s) :
theorem measurable_set.is_clopenable {α : Type u_1} [polish_space α] [borel_space α] {s : set α} (hs : measurable_set s) :

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.

theorem measurable_set.analytic_set {α : Type u_1} [t : topological_space α] [polish_space α] [borel_space α] {s : set α} (hs : measurable_set s) :
theorem measurable.exists_continuous {α : Type u_1} {β : Type u_2} [t : topological_space α] [polish_space α] [borel_space α] [tβ : topological_space β] {f : α β} (hf : measurable f) :
(t' : , t' t

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.

theorem measurable_set.analytic_set_image {X : Type u_1} {Y : Type u_2} [polish_space X] [borel_space X] {f : X Y} {s : set X} (hs : measurable_set s) (hf : measurable f) :

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

### Separating sets with measurable sets #

def measure_theory.measurably_separable {α : Type u_1} (s t : set α) :
Prop

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
theorem measure_theory.measurably_separable.Union {ι : Type u_2} [countable ι] {α : Type u_1} {s t : ι set α} (h : (m n : ι), (t n)) :
measure_theory.measurably_separable ( (n : ι), s n) ( (m : ι), t m)
theorem measure_theory.measurably_separable_range_of_disjoint {α : Type u_1} [t2_space α] {f g : ( ) α} (hf : continuous f) (hg : continuous g) (h : (set.range g)) :

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 #

theorem measurable.measurable_set_preimage_iff_of_surjective {X : Type u_3} {Y : Type u_4} [polish_space X] [borel_space X] [t2_space Y] {f : X Y} (hf : measurable f) (hsurj : function.surjective f) {s : set Y} :

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.

theorem measurable.map_measurable_space_eq {X : Type u_3} {Y : Type u_4} [polish_space X] [borel_space X] [t2_space Y] {f : X Y} (hf : measurable f) (hsurj : function.surjective f) :
_inst_4 = _inst_8
theorem measurable.map_measurable_space_eq_borel {X : Type u_3} {Y : Type u_4} [polish_space X] [borel_space X] [t2_space Y] {f : X Y} (hf : measurable f) (hsurj : function.surjective f) :
_inst_4 =
theorem measurable.borel_space_codomain {X : Type u_3} {Y : Type u_4} [polish_space X] [borel_space X] [t2_space Y] {f : X Y} (hf : measurable f) (hsurj : function.surjective f) :

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.

theorem measurable.measurable_comp_iff_restrict {X : Type u_3} {Y : Type u_4} {β : Type u_5} [polish_space X] [borel_space X] [t2_space Y] {f : X Y} (hf : measurable f) {g : Y β} :

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.

theorem measurable.measurable_comp_iff_of_surjective {X : Type u_3} {Y : Type u_4} {β : Type u_5} [polish_space X] [borel_space X] [t2_space Y] {f : X Y} (hf : measurable f) (hsurj : function.surjective f) {g : Y β} :

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.

theorem continuous.map_eq_borel {X : Type u_1} {Y : Type u_2} [polish_space X] [borel_space X] [t2_space Y] {f : X Y} (hf : continuous f) (hsurj : function.surjective f) :
_inst_4 =
theorem continuous.map_borel_eq {X : Type u_1} {Y : Type u_2} [polish_space X] [t2_space Y] {f : X Y} (hf : continuous f) (hsurj : function.surjective f) :
=
@[protected, instance]
def quotient.borel_space {X : Type u_1} [polish_space X] [borel_space X] {s : setoid X} [t2_space (quotient s)]  :
@[protected, instance]
@[protected, instance]

### Injective images of Borel sets #

theorem measure_theory.measurable_set_range_of_continuous_injective {γ : Type u_3} [tγ : topological_space γ] [polish_space γ] {β : Type u_1} [t2_space β] [borel_space β] {f : γ β} (f_cont : continuous f) (f_inj : function.injective f) :

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

theorem is_closed.measurable_set_image_of_continuous_on_inj_on {γ : Type u_3} [tγ : topological_space γ] [polish_space γ] {β : Type u_1} [t2_space β] [borel_space β] {s : set γ} (hs : is_closed s) {f : γ β} (f_cont : s) (f_inj : s) :
theorem measurable_set.image_of_continuous_on_inj_on {γ : Type u_3} [tγ : topological_space γ] [polish_space γ] [hγb : borel_space γ] {β : Type u_4} [tβ : topological_space β] [t2_space β] [borel_space β] {s : set γ} {f : γ β} (hs : measurable_set s) (f_cont : s) (f_inj : s) :

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.

theorem measurable_set.image_of_measurable_inj_on {γ : Type u_3} [tγ : topological_space γ] [polish_space γ] [hγb : borel_space γ] {β : Type u_4} [tβ : topological_space β] [t2_space β] [borel_space β] {s : set γ} {f : γ β} (hs : measurable_set s) (f_meas : measurable f) (f_inj : s) :

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.

theorem continuous.measurable_embedding {γ : Type u_3} [tγ : topological_space γ] [polish_space γ] [hγb : borel_space γ] {β : Type u_4} [tβ : topological_space β] [t2_space β] [borel_space β] {f : γ β} (f_cont : continuous f) (f_inj : function.injective f) :

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

theorem continuous_on.measurable_embedding {γ : Type u_3} [tγ : topological_space γ] [polish_space γ] [hγb : borel_space γ] {β : Type u_4} [tβ : topological_space β] [t2_space β] [borel_space β] {s : set γ} {f : γ β} (hs : measurable_set s) (f_cont : s) (f_inj : s) :

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.

theorem measurable.measurable_embedding {γ : Type u_3} [tγ : topological_space γ] [polish_space γ] [hγb : borel_space γ] {β : Type u_4} [tβ : topological_space β] [t2_space β] [borel_space β] {f : γ β} (f_meas : measurable f) (f_inj : function.injective f) :

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

theorem measure_theory.is_clopenable_iff_measurable_set {γ : Type u_3} [tγ : topological_space γ] [polish_space γ] [hγb : borel_space γ] {s : set γ} :

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

@[measurability]
theorem measure_theory.measurable_set_exists_tendsto {ι : Type u_2} {γ : Type u_3} [tγ : topological_space γ] [polish_space γ] {β : Type u_4} [hγ : opens_measurable_space γ] [countable ι] {l : filter ι} {f : ι β γ} (hf : (i : ι), measurable (f i)) :
measurable_set {x : β | (c : γ), filter.tendsto (λ (n : ι), f n x) l (nhds c)}

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

### The Borel Isomorphism Theorem #

@[protected, instance]
def polish_of_countable {α : Type u_1} [h : countable α]  :
noncomputable def polish_space.borel_schroeder_bernstein {α : Type u_1} {β : Type u_3} [polish_space α] [polish_space β] [borel_space α] [borel_space β] {f : α β} {g : β α} (fmeas : measurable f) (finj : function.injective f) (gmeas : measurable g) (ginj : function.injective g) :
α ≃ᵐ β

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

Equations
• finj gmeas ginj =

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

Equations
noncomputable def polish_space.measurable_equiv_of_not_countable {α : Type u_1} {β : Type u_3} [polish_space α] [polish_space β] [borel_space α] [borel_space β] (hα : ¬) (hβ : ¬) :
α ≃ᵐ β

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

Equations
noncomputable def polish_space.equiv.measurable_equiv {α : Type u_1} {β : Type u_3} [polish_space α] [polish_space β] [borel_space α] [borel_space β] (e : α β) :
α ≃ᵐ β

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

Equations
@[protected, instance]

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

Any Polish Borel space embeds measurably into the reals.