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 #

source

@[irreducible]

def measure_theory.analytic_set {α : Type u_1} [topological_space α] (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

measure_theory.analytic_set s = (s = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), continuous f ∧ set.range f = s)

source

theorem measure_theory.analytic_set_empty {α : Type u_1} [topological_space α] :

measure_theory.analytic_set ∅

source

theorem measure_theory.analytic_set_range_of_polish_space {α : Type u_1} [topological_space α] {β : Type u_2} [topological_space β] [polish_space β] {f : β → α} (f_cont : continuous f) :

measure_theory.analytic_set (set.range f)

source

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

measure_theory.analytic_set (f '' s)

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

source

theorem measure_theory.analytic_set_iff_exists_polish_space_range {α : Type u_1} [topological_space α] {s : set α} :

measure_theory.analytic_set s ↔ ∃ (β : Type) (h : topological_space β) (h' : polish_space β) (f : β → α), continuous f ∧ set.range f = s

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

source

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

measure_theory.analytic_set (f '' s)

The continuous image of an analytic set is analytic

source

theorem measure_theory.analytic_set.image_of_continuous {α : Type u_1} [topological_space α] {β : Type u_2} [topological_space β] {s : set α} (hs : measure_theory.analytic_set s) {f : α → β} (hf : continuous f) :

measure_theory.analytic_set (f '' s)

source

theorem measure_theory.analytic_set.Inter {α : Type u_1} [topological_space α] {ι : Type u_2} [hι : nonempty ι] [countable ι] [t2_space α] {s : ι → set α} (hs : ∀ (n : ι), measure_theory.analytic_set (s n)) :

measure_theory.analytic_set (⋂ (n : ι), s n)

A countable intersection of analytic sets is analytic.

source

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

measure_theory.analytic_set (⋃ (n : ι), s n)

A countable union of analytic sets is analytic.

source

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

measure_theory.analytic_set s

source

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

polish_space.is_clopenable 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.

source

theorem measurable_set.analytic_set {α : Type u_1} [t : topological_space α] [polish_space α] [measurable_space α] [borel_space α] {s : set α} (hs : measurable_set s) :

measure_theory.analytic_set s

source

theorem measurable.exists_continuous {α : Type u_1} {β : Type u_2} [t : topological_space α] [polish_space α] [measurable_space α] [borel_space α] [tβ : topological_space β] [measurable_space β] [opens_measurable_space β] {f : α → β} [topological_space.second_countable_topology ↥(set.range f)] (hf : measurable f) :

∃ (t' : topological_space α), t' ≤ t ∧ continuous f ∧ polish_space α

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.

source

theorem measurable_set.analytic_set_image {X : Type u_1} {Y : Type u_2} [topological_space X] [polish_space X] [measurable_space X] [borel_space X] [topological_space Y] [measurable_space Y] [opens_measurable_space Y] {f : X → Y} [topological_space.second_countable_topology ↥(set.range f)] {s : set X} (hs : measurable_set s) (hf : measurable f) :

measure_theory.analytic_set (f '' s)

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

Separating sets with measurable sets #

source

def measure_theory.measurably_separable {α : Type u_1} [measurable_space α] (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

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

source

theorem measure_theory.measurably_separable.Union {ι : Type u_2} [countable ι] {α : Type u_1} [measurable_space α] {s t : ι → set α} (h : ∀ (m n : ι), measure_theory.measurably_separable (s m) (t n)) :

measure_theory.measurably_separable (⋃ (n : ι), s n) (⋃ (m : ι), t m)

source

theorem measure_theory.measurably_separable_range_of_disjoint {α : Type u_1} [topological_space α] [t2_space α] [measurable_space α] [opens_measurable_space α] {f g : (ℕ → ℕ) → α} (hf : continuous f) (hg : continuous g) (h : disjoint (set.range f) (set.range g)) :

measure_theory.measurably_separable (set.range f) (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 ℕ → ℕ.

source

theorem measure_theory.analytic_set.measurably_separable {α : Type u_1} [topological_space α] [t2_space α] [measurable_space α] [opens_measurable_space α] {s t : set α} (hs : measure_theory.analytic_set s) (ht : measure_theory.analytic_set t) (h : disjoint s t) :

measure_theory.measurably_separable s t

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

source

theorem measure_theory.analytic_set.measurable_set_of_compl {α : Type u_1} [topological_space α] [t2_space α] [measurable_space α] [opens_measurable_space α] {s : set α} (hs : measure_theory.analytic_set s) (hsc : measure_theory.analytic_set sᶜ) :

measurable_set s

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

Measurability of preimages under measurable maps #

source

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

measurable_set (f ⁻¹' s) ↔ measurable_set s

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.

source

theorem measurable.map_measurable_space_eq {X : Type u_3} {Y : Type u_4} [topological_space X] [polish_space X] [measurable_space X] [borel_space X] [topological_space Y] [t2_space Y] [measurable_space Y] [opens_measurable_space Y] [topological_space.second_countable_topology Y] {f : X → Y} (hf : measurable f) (hsurj : function.surjective f) :

measurable_space.map f _inst_4 = _inst_8

source

theorem measurable.map_measurable_space_eq_borel {X : Type u_3} {Y : Type u_4} [topological_space X] [polish_space X] [measurable_space X] [borel_space X] [topological_space Y] [t2_space Y] [measurable_space Y] [opens_measurable_space Y] [topological_space.second_countable_topology Y] {f : X → Y} (hf : measurable f) (hsurj : function.surjective f) :

measurable_space.map f _inst_4 = borel Y

source

theorem measurable.borel_space_codomain {X : Type u_3} {Y : Type u_4} [topological_space X] [polish_space X] [measurable_space X] [borel_space X] [topological_space Y] [t2_space Y] [measurable_space Y] [opens_measurable_space Y] [topological_space.second_countable_topology Y] {f : X → Y} (hf : measurable f) (hsurj : function.surjective f) :

borel_space Y

source

theorem measurable.measurable_set_preimage_iff_preimage_coe {X : Type u_3} {Y : Type u_4} [topological_space X] [polish_space X] [measurable_space X] [borel_space X] [topological_space Y] [t2_space Y] [measurable_space Y] [opens_measurable_space Y] {f : X → Y} [topological_space.second_countable_topology ↥(set.range f)] (hf : measurable f) {s : set Y} :

measurable_set (f ⁻¹' s) ↔ measurable_set (coe ⁻¹' s)

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.

source

theorem measurable.measurable_set_preimage_iff_inter_range {X : Type u_3} {Y : Type u_4} [topological_space X] [polish_space X] [measurable_space X] [borel_space X] [topological_space Y] [t2_space Y] [measurable_space Y] [opens_measurable_space Y] {f : X → Y} [topological_space.second_countable_topology ↥(set.range f)] (hf : measurable f) (hr : measurable_set (set.range f)) {s : set Y} :

measurable_set (f ⁻¹' s) ↔ measurable_set (s ∩ 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.

source

theorem measurable.measurable_comp_iff_restrict {X : Type u_3} {Y : Type u_4} {β : Type u_5} [topological_space X] [polish_space X] [measurable_space X] [borel_space X] [topological_space Y] [t2_space Y] [measurable_space Y] [opens_measurable_space Y] [measurable_space β] {f : X → Y} [topological_space.second_countable_topology ↥(set.range f)] (hf : measurable f) {g : Y → β} :

measurable (g ∘ f) ↔ measurable ((set.range f).restrict g)

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.

source

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

measurable (g ∘ f) ↔ measurable g

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.

source

theorem continuous.map_eq_borel {X : Type u_1} {Y : Type u_2} [topological_space X] [polish_space X] [measurable_space X] [borel_space X] [topological_space Y] [t2_space Y] [topological_space.second_countable_topology Y] {f : X → Y} (hf : continuous f) (hsurj : function.surjective f) :

measurable_space.map f _inst_4 = borel Y

source

theorem continuous.map_borel_eq {X : Type u_1} {Y : Type u_2} [topological_space X] [polish_space X] [topological_space Y] [t2_space Y] [topological_space.second_countable_topology Y] {f : X → Y} (hf : continuous f) (hsurj : function.surjective f) :

measurable_space.map f (borel X) = borel Y

source

@[protected, instance]

def quotient.borel_space {X : Type u_1} [topological_space X] [polish_space X] [measurable_space X] [borel_space X] {s : setoid X} [t2_space (quotient s)] [topological_space.second_countable_topology (quotient s)] :

borel_space (quotient s)

source

@[protected, instance]

def quotient_group.borel_space {G : Type u_1} [topological_space G] [polish_space G] [group G] [topological_group G] [measurable_space G] [borel_space G] {N : subgroup G} [N.normal] [is_closed ↑N] :

borel_space (G ⧸ N)

source

@[protected, instance]

def quotient_add_group.borel_space {G : Type u_1} [topological_space G] [polish_space G] [add_group G] [topological_add_group G] [measurable_space G] [borel_space G] {N : add_subgroup G} [N.normal] [is_closed ↑N] :

borel_space (G ⧸ N)

Injective images of Borel sets #

source

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

measurable_set (set.range f)

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

source

theorem is_closed.measurable_set_image_of_continuous_on_inj_on {γ : Type u_3} [tγ : topological_space γ] [polish_space γ] {β : Type u_1} [topological_space β] [t2_space β] [measurable_space β] [borel_space β] {s : set γ} (hs : is_closed s) {f : γ → β} (f_cont : continuous_on f s) (f_inj : set.inj_on f s) :

measurable_set (f '' s)

source

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

measurable_set (f '' 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.

source

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

measurable_set (f '' 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.

source

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

measurable_embedding f

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

source

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

measurable_embedding (s.restrict f)

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.

source

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

measurable_embedding f

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

source

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

polish_space.is_clopenable s ↔ measurable_set s

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

source

@[measurability]

theorem measure_theory.measurable_set_exists_tendsto {ι : Type u_2} {γ : Type u_3} [tγ : topological_space γ] [polish_space γ] [measurable_space γ] {β : Type u_4} [measurable_space β] [hγ : opens_measurable_space γ] [countable ι] {l : filter ι} [l.is_countably_generated] {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 #

source

@[protected, instance]

def polish_of_countable {α : Type u_1} [topological_space α] [h : countable α] [discrete_topology α] :

polish_space α

source

noncomputable def polish_space.borel_schroeder_bernstein {α : Type u_1} [topological_space α] {β : Type u_3} [topological_space β] [polish_space α] [polish_space β] [measurable_space α] [measurable_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

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

source

noncomputable def polish_space.measurable_equiv_nat_bool_of_not_countable {α : Type u_1} [topological_space α] [polish_space α] [measurable_space α] [borel_space α] (h : ¬countable α) :

α ≃ᵐ (ℕ → bool)

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

Equations

polish_space.measurable_equiv_nat_bool_of_not_countable h = nonempty.some _

source

noncomputable def polish_space.measurable_equiv_of_not_countable {α : Type u_1} [topological_space α] {β : Type u_3} [topological_space β] [polish_space α] [polish_space β] [measurable_space α] [measurable_space β] [borel_space α] [borel_space β] (hα : ¬countable α) (hβ : ¬countable β) :

α ≃ᵐ β

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

Equations

polish_space.measurable_equiv_of_not_countable hα hβ = (polish_space.measurable_equiv_nat_bool_of_not_countable hα).trans (polish_space.measurable_equiv_nat_bool_of_not_countable hβ).symm

source

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

α ≃ᵐ β

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

source

@[protected, instance]

def measure_theory.set.univ.polish_space {α : Type u_1} [topological_space α] [polish_space α] :

polish_space ↥set.univ

source

theorem measure_theory.exists_nat_measurable_equiv_range_coe_fin_of_finite (α : Type u_1) [topological_space α] [measurable_space α] [polish_space α] [borel_space α] [finite α] :

∃ (n : ℕ), nonempty (α ≃ᵐ ↥(set.range coe))

source

theorem measure_theory.measurable_equiv_range_coe_nat_of_infinite_of_countable (α : Type u_1) [topological_space α] [measurable_space α] [polish_space α] [borel_space α] [infinite α] [countable α] :

nonempty (α ≃ᵐ ↥(set.range coe))

source

theorem measure_theory.exists_subset_real_measurable_equiv (α : Type u_1) [topological_space α] [measurable_space α] [polish_space α] [borel_space α] :

∃ (s : set ℝ), measurable_set s ∧ nonempty (α ≃ᵐ ↥s)

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

source

theorem measure_theory.exists_measurable_embedding_real (α : Type u_1) [topological_space α] [measurable_space α] [polish_space α] [borel_space α] :

∃ (f : α → ℝ), measurable_embedding f

Any Polish Borel space embeds measurably into the reals.