Documentation

Mathlib.Topology.MetricSpace.Polish

Polish spaces #

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 #

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

Basic properties of Polish spaces #

class PolishSpace (α : Type u_3) [h : TopologicalSpace α] extends SecondCountableTopology :

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 := upgradePolishSpace α.

Instances
    theorem PolishSpace.complete {α : Type u_3} [h : TopologicalSpace α] [self : PolishSpace α] :
    ∃ (m : MetricSpace α), UniformSpace.toTopologicalSpace = h CompleteSpace α

    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 := upgradePolishSpace α to endow a Polish space with a complete metric.

      Instances
        @[instance 100]
        Equations
        • =

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

        Equations
        Instances For

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

          Equations
          Instances For
            @[instance 100]
            Equations
            • =
            @[deprecated]
            instance PolishSpace.pi_countable {ι : Type u_3} [Countable ι] {E : ιType u_4} [(i : ι) → TopologicalSpace (E i)] [∀ (i : ι), PolishSpace (E i)] :
            PolishSpace ((i : ι) → E i)

            A countable product of Polish spaces is Polish.

            Equations
            • =
            instance PolishSpace.sigma {ι : Type u_3} [Countable ι] {E : ιType u_4} [(n : ι) → TopologicalSpace (E n)] [∀ (n : ι), PolishSpace (E n)] :
            PolishSpace ((n : ι) × E n)

            A countable disjoint union of Polish spaces is Polish.

            Equations
            • =
            instance PolishSpace.prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PolishSpace α] [TopologicalSpace β] [PolishSpace β] :
            PolishSpace (α × β)

            The product of two Polish spaces is Polish.

            Equations
            • =
            instance PolishSpace.sum {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PolishSpace α] [TopologicalSpace β] [PolishSpace β] :

            The disjoint union of two Polish spaces is Polish.

            Equations
            • =

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

            theorem ClosedEmbedding.polishSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [PolishSpace β] {f : αβ} (hf : ClosedEmbedding f) :

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

            @[instance 50]

            Any countable discrete space is Polish.

            Equations
            • =
            theorem Equiv.polishSpace_induced {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] [PolishSpace β] (f : α β) :

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

            theorem IsClosed.polishSpace {α : Type u_1} [TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : IsClosed s) :

            A closed subset of a Polish space is also Polish.

            Equations
            • =
            theorem CompletePseudometrizable.iInf {α : Type u_1} {ι : Type u_3} [Countable ι] {t : ιTopologicalSpace α} (ht₀ : ∃ (t₀ : TopologicalSpace α), T2Space α ∀ (i : ι), t i t₀) (ht : ∀ (i : ι), ∃ (u : UniformSpace α), CompleteSpace α (uniformity α).IsCountablyGenerated UniformSpace.toTopologicalSpace = t i) :
            ∃ (u : UniformSpace α), CompleteSpace α (uniformity α).IsCountablyGenerated UniformSpace.toTopologicalSpace = ⨅ (i : ι), t i
            theorem PolishSpace.iInf {α : Type u_1} {ι : Type u_3} [Countable ι] {t : ιTopologicalSpace α} (ht₀ : ∃ (i₀ : ι), ∀ (i : ι), t i t i₀) (ht : ∀ (i : ι), PolishSpace α) :
            theorem PolishSpace.exists_polishSpace_forall_le {α : Type u_1} {ι : Type u_3} [Countable ι] [t : TopologicalSpace α] [p : PolishSpace α] (m : ιTopologicalSpace α) (hm : ∀ (n : ι), m n t) (h'm : ∀ (n : ι), PolishSpace α) :
            ∃ (t' : TopologicalSpace α), (∀ (n : ι), t' m n) t' t PolishSpace α

            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.

            Porting note: definitions and lemmas in this section now take (s : Opens α) instead of {s : Set α} (hs : IsOpen s) so that we can turn various definitions and lemmas into instances. Also, some lemmas used to assume Set.Nonempty sᶜ in Lean 3. In fact, this assumption is not needed, so it was dropped.

            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
            • s.CompleteCopy = s
            Instances For

              A distance on an open subset s of a metric space, designed to make it complete. 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
              theorem TopologicalSpace.Opens.CompleteCopy.dist_eq {α : Type u_1} [MetricSpace α] {s : TopologicalSpace.Opens α} (x : s.CompleteCopy) (y : s.CompleteCopy) :
              dist x y = dist x y + |1 / Metric.infDist (x) (s) - 1 / Metric.infDist (y) (s)|
              theorem TopologicalSpace.Opens.CompleteCopy.dist_val_le_dist {α : Type u_1} [MetricSpace α] {s : TopologicalSpace.Opens α} (x : s.CompleteCopy) (y : s.CompleteCopy) :
              dist x y dist x y
              Equations
              Equations
              • =

              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.

              Porting note: the definition changed to ensure that the TopologicalSpace structure on TopologicalSpace.Opens.CompleteCopy s is definitionally equal to the original one.

              Equations
              theorem IsOpen.polishSpace {α : Type u_3} [TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : IsOpen s) :

              An open subset of a Polish space is also Polish.

              Clopenable sets in Polish spaces #

              def PolishSpace.IsClopenable {α : Type u_1} [t : TopologicalSpace α] (s : Set α) :

              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 isClopenable_iff_measurableSet).

              Equations
              Instances For

                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 PolishSpace.IsClopenable.iUnion {α : Type u_1} [t : TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : ∀ (n : ), PolishSpace.IsClopenable (s n)) :
                PolishSpace.IsClopenable (⋃ (n : ), s n)