mathlib3 documentation

topology.metric_space.polish

Polish spaces #

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

A topological space is Polish if its topology is second-countable and there exists a compatible complete metric. This is the class of spaces that is well-behaved with respect to measure theory. In this file, we establish the basic properties of Polish spaces.

Main definitions and results #

polish_space α is a mixin typeclass on a topological space, requiring that the topology is second-countable and compatible with a complete metric. To endow the space with such a metric, use in a proof letI := upgrade_polish_space α. We register an instance from complete second-countable metric spaces to Polish spaces, not the other way around.
We register that countable products and sums of Polish spaces are Polish.
is_closed.polish_space: a closed subset of a Polish space is Polish.
is_open.polish_space: an open subset of a Polish space is Polish.
exists_nat_nat_continuous_surjective: any nonempty Polish space is the continuous image of the fundamental Polish space ℕ → ℕ.

A fundamental property of Polish spaces is that one can put finer topologies, still Polish, with additional properties:

exists_polish_space_forall_le: on a topological space, consider countably many topologies t n, all Polish and finer than the original topology. Then there exists another Polish topology which is finer than all the t n.
is_clopenable s is a property of a subset s of a topological space, requiring that there exists a finer topology, which is Polish, for which s becomes open and closed. We show that this property is satisfied for open sets, closed sets, for complements, and for countable unions. Once Borel-measurable sets are defined in later files, it will follow that any Borel-measurable set is clopenable. Once the Lusin-Souslin theorem is proved using analytic sets, we will even show that a set is clopenable if and only if it is Borel-measurable, see is_clopenable_iff_measurable_set.

Basic properties of Polish spaces #

@[class]

structure polish_space (α : Type u_3) [h : topological_space α] :

Prop

second_countable : topological_space.second_countable_topology α
complete : ∃ (m : metric_space α), uniform_space.to_topological_space = h ∧ complete_space α

A Polish space is a topological space with second countable topology, that can be endowed with a metric for which it is complete. We register an instance from complete second countable metric space to polish space, and not the other way around as this is the most common use case.

To endow a Polish space with a complete metric space structure, do letI := upgrade_polish_space α.

Instances of this typeclass

@[class]

structure upgraded_polish_space (α : Type u_3) :

Type u_3

to_metric_space : metric_space α
to_second_countable_topology : topological_space.second_countable_topology α
to_complete_space : complete_space α

A convenience class, for a Polish space endowed with a complete metric. No instance of this class should be registered: It should be used as letI := upgrade_polish_space α to endow a Polish space with a complete metric.

Instances for upgraded_polish_space

upgraded_polish_space.has_sizeof_inst

@[protected, instance]

def polish_space_of_complete_second_countable {α : Type u_1} [m : metric_space α] [h : topological_space.second_countable_topology α] [h' : complete_space α] :

polish_space α

noncomputable def polish_space_metric (α : Type u_1) [ht : topological_space α] [h : polish_space α] :

metric_space α

Construct on a Polish space a metric (compatible with the topology) which is complete.

Equations

polish_space_metric α = polish_space.complete.some.replace_topology _

theorem complete_polish_space_metric (α : Type u_1) [ht : topological_space α] [h : polish_space α] :

complete_space α

noncomputable def upgrade_polish_space (α : Type u_1) [ht : topological_space α] [h : polish_space α] :

upgraded_polish_space α

This definition endows a Polish space with a complete metric. Use it as: letI := upgrade_polish_space α.

Equations

upgrade_polish_space α = let _inst : metric_space α := polish_space_metric α in upgraded_polish_space.mk

@[protected, instance]

def polish_space.t2_space (α : Type u_1) [topological_space α] [polish_space α] :

@[protected, instance]

def polish_space.pi_countable {ι : Type u_1} [countable ι] {E : ι → Type u_2} [Π (i : ι), topological_space (E i)] [∀ (i : ι), polish_space (E i)] :

polish_space (Π (i : ι), E i)

A countable product of Polish spaces is Polish.

@[protected, instance]

def polish_space.nat_fun {α : Type u_1} [topological_space α] [polish_space α] :

polish_space (ℕ → α)

Without this instance, polish_space (ℕ → ℕ) is not found by typeclass inference.

@[protected, instance]

def polish_space.sigma {ι : Type u_1} [countable ι] {E : ι → Type u_2} [Π (n : ι), topological_space (E n)] [∀ (n : ι), polish_space (E n)] :

polish_space (Σ (n : ι), E n)

A countable disjoint union of Polish spaces is Polish.

@[protected, instance]

def polish_space.sum {α : Type u_1} {β : Type u_2} [topological_space α] [polish_space α] [topological_space β] [polish_space β] :

polish_space (α ⊕ β)

The disjoint union of two Polish spaces is Polish.

theorem polish_space.exists_nat_nat_continuous_surjective (α : Type u_1) [topological_space α] [polish_space α] [nonempty α] :

∃ (f : (ℕ → ℕ) → α), continuous f ∧ function.surjective f

Any nonempty Polish space is the continuous image of the fundamental space ℕ → ℕ.

theorem closed_embedding.polish_space {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [polish_space β] {f : α → β} (hf : closed_embedding f) :

polish_space α

Given a closed embedding into a Polish space, the source space is also Polish.

theorem equiv.polish_space_induced {α : Type u_1} {β : Type u_2} [t : topological_space β] [polish_space β] (f : α ≃ β) :

polish_space α

Pulling back a Polish topology under an equiv gives again a Polish topology.

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

polish_space ↥s

A closed subset of a Polish space is also Polish.

@[nolint]

def polish_space.aux_copy (α : Type u_1) {ι : Type u_2} (i : ι) :

Type u_1

A sequence of type synonyms of a given type α, useful in the proof of exists_polish_space_forall_le to endow each copy with a different topology.

Equations

polish_space.aux_copy α i = α

theorem polish_space.exists_polish_space_forall_le {α : Type u_1} {ι : Type u_2} [countable ι] [t : topological_space α] [p : polish_space α] (m : ι → topological_space α) (hm : ∀ (n : ι), m n ≤ t) (h'm : ∀ (n : ι), polish_space α) :

∃ (t' : topological_space α), (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ polish_space α

Given a Polish space, and countably many finer Polish topologies, there exists another Polish topology which is finer than all of them.

An open subset of a Polish space is Polish #

To prove this fact, one needs to construct another metric, giving rise to the same topology, for which the open subset is complete. This is not obvious, as for instance (0,1) ⊆ ℝ is not complete for the usual metric of ℝ: one should build a new metric that blows up close to the boundary.

@[nolint]

def polish_space.complete_copy {α : Type u_1} (s : set α) :

Type u_1

A type synonym for a subset s of a metric space, on which we will construct another metric for which it will be complete.

Equations

polish_space.complete_copy s = ↥s

noncomputable def polish_space.has_dist_complete_copy {α : Type u_1} [metric_space α] (s : set α) :

has_dist (polish_space.complete_copy s)

A distance on a subset s of a metric space, designed to make it complete if s is open. It is given by dist' x y = dist x y + |1 / dist x sᶜ - 1 / dist y sᶜ|, where the second term blows up close to the boundary to ensure that Cauchy sequences for dist' remain well inside s.

Equations

polish_space.has_dist_complete_copy s = {dist := λ (x y : polish_space.complete_copy s), has_dist.dist x.val y.val + |1 / metric.inf_dist x.val sᶜ - 1 / metric.inf_dist y.val sᶜ|}

theorem polish_space.dist_complete_copy_eq {α : Type u_1} [metric_space α] {s : set α} (x y : polish_space.complete_copy s) :

has_dist.dist x y = has_dist.dist x.val y.val + |1 / metric.inf_dist x.val sᶜ - 1 / metric.inf_dist y.val sᶜ|

theorem polish_space.dist_le_dist_complete_copy {α : Type u_1} [metric_space α] {s : set α} (x y : polish_space.complete_copy s) :

has_dist.dist x.val y.val ≤ has_dist.dist x y

noncomputable def polish_space.complete_copy_metric_space {α : Type u_1} [metric_space α] (s : set α) :

metric_space (polish_space.complete_copy s)

A metric space structure on a subset s of a metric space, designed to make it complete if s is open. It is given by dist' x y = dist x y + |1 / dist x sᶜ - 1 / dist y sᶜ|, where the second term blows up close to the boundary to ensure that Cauchy sequences for dist' remain well inside s.

Equations

polish_space.complete_copy_metric_space s = {to_pseudo_metric_space := {to_has_dist := polish_space.has_dist_complete_copy s, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : polish_space.complete_copy s), ↑⟨(λ (x y : polish_space.complete_copy s), has_dist.dist x.val y.val + |1 / metric.inf_dist x.val sᶜ - 1 / metric.inf_dist y.val sᶜ|) x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : polish_space.complete_copy s), has_dist.dist x.val y.val + |1 / metric.inf_dist x.val sᶜ - 1 / metric.inf_dist y.val sᶜ|) _ _ _, uniformity_dist := _, to_bornology := bornology.of_dist (λ (x y : polish_space.complete_copy s), has_dist.dist x.val y.val + |1 / metric.inf_dist x.val sᶜ - 1 / metric.inf_dist y.val sᶜ|) _ _ _, cobounded_sets := _}, eq_of_dist_eq_zero := _}

def polish_space.complete_copy_id_homeo {α : Type u_1} [metric_space α] {s : set α} (hs : is_open s) (h's : sᶜ.nonempty) :

polish_space.complete_copy s ≃ₜ ↥s

The identity between the type synonym complete_copy s (with its modified metric) and the original subtype s is a homeomorphism.

Equations

polish_space.complete_copy_id_homeo hs h's = {to_equiv := {to_fun := id (polish_space.complete_copy s), inv_fun := id ↥s, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

theorem polish_space.complete_space_complete_copy {α : Type u_1} [metric_space α] {s : set α} [complete_space α] (hs : is_open s) (h's : sᶜ.nonempty) :

complete_space (polish_space.complete_copy s)

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

polish_space ↥s

An open subset of a Polish space is also Polish.

Clopenable sets in Polish spaces #

def polish_space.is_clopenable {α : Type u_1} [t : topological_space α] (s : set α) :

Prop

A set in a topological space is clopenable if there exists a finer Polish topology for which this set is open and closed. It turns out that this notion is equivalent to being Borel-measurable, but this is nontrivial (see is_clopenable_iff_measurable_set).

Equations

polish_space.is_clopenable s = ∃ (t' : topological_space α), t' ≤ t ∧ polish_space α ∧ is_closed s ∧ is_open s

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

polish_space.is_clopenable s

Given a closed set s in a Polish space, one can construct a finer Polish topology for which s is both open and closed.

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

polish_space.is_clopenable sᶜ

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

polish_space.is_clopenable s

theorem polish_space.is_clopenable.Union {α : Type u_1} [t : topological_space α] [polish_space α] {s : ℕ → set α} (hs : ∀ (n : ℕ), polish_space.is_clopenable (s n)) :

polish_space.is_clopenable (⋃ (n : ℕ), s n)