mathlib documentation

measure_theory.constructions.polish

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 the class of analytic sets and establish its basic properties.

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

Finally, we 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.

Analytic sets #

@[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
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) :
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) :

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} [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.

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

The continuous image of an analytic set is analytic

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) :
theorem measure_theory.analytic_set.Inter {α : Type u_1} [topological_space α] {ι : Type u_2} [hι : nonempty ι] [encodable ι] [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.

theorem measure_theory.analytic_set.Union {α : Type u_1} [topological_space α] {ι : Type u_2} [encodable ι] {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.

theorem is_closed.analytic_set {α : Type u_1} [topological_space α] [polish_space α] {s : set α} (hs : is_closed 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.exists_continuous {α : Type u_1} {β : Type u_2} [t : topological_space α] [polish_space α] [measurable_space α] [borel_space α] [tβ : topological_space β] [topological_space.second_countable_topology β] [measurable_space β] [borel_space β] {f : α → β} (hf : measurable f) :

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.

Separating sets with measurable sets #

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
theorem measure_theory.measurably_separable.Union {ι : Type u_2} [encodable ι] {α : 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)

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.

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} [topological_space β] [t2_space β] [measurable_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} [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) :
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) :

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 γ] [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) :

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 γ] [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) :

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 γ] [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) :

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 γ] [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) :

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.

@[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.