Documentation

Mathlib.Topology.MetricSpace.PiNat

Topological study of spaces Π (n : ℕ), E n #

When E n are topological spaces, the space Π (n : ℕ), E n is naturally a topological space (with the product topology). When E n are uniform spaces, it also inherits a uniform structure. However, it does not inherit a canonical metric space structure of the E n. Nevertheless, one can put a noncanonical metric space structure (or rather, several of them). This is done in this file.

Main definitions and results #

One can define a combinatorial distance on Π (n : ℕ), E n, as follows:

These results are used to construct continuous functions on Π n, E n:

One can also put distances on Π (i : ι), E i when the spaces E i are metric spaces (not discrete in general), and ι is countable.

The firstDiff function #

@[irreducible]
def PiNat.firstDiff {E : Type u_2} (x : (n : ) → E n) (y : (n : ) → E n) :

In a product space Π n, E n, then firstDiff x y is the first index at which x and y differ. If x = y, then by convention we set firstDiff x x = 0.

Equations
Instances For
    theorem PiNat.firstDiff_def {E : Type u_2} (x : (n : ) → E n) (y : (n : ) → E n) :
    PiNat.firstDiff x y = if h : x y then Nat.find else 0
    theorem PiNat.apply_firstDiff_ne {E : Type u_1} {x : (n : ) → E n} {y : (n : ) → E n} (h : x y) :
    theorem PiNat.apply_eq_of_lt_firstDiff {E : Type u_1} {x : (n : ) → E n} {y : (n : ) → E n} {n : } (hn : n < PiNat.firstDiff x y) :
    x n = y n
    theorem PiNat.firstDiff_comm {E : Type u_1} (x : (n : ) → E n) (y : (n : ) → E n) :
    theorem PiNat.min_firstDiff_le {E : Type u_1} (x : (n : ) → E n) (y : (n : ) → E n) (z : (n : ) → E n) (h : x z) :

    Cylinders #

    def PiNat.cylinder {E : Type u_1} (x : (n : ) → E n) (n : ) :
    Set ((n : ) → E n)

    In a product space Π n, E n, the cylinder set of length n around x, denoted cylinder x n, is the set of sequences y that coincide with x on the first n symbols, i.e., such that y i = x i for all i < n.

    Equations
    Instances For
      theorem PiNat.cylinder_eq_pi {E : Type u_1} (x : (n : ) → E n) (n : ) :
      PiNat.cylinder x n = (↑(Finset.range n)).pi fun (i : ) => {x i}
      @[simp]
      theorem PiNat.cylinder_zero {E : Type u_1} (x : (n : ) → E n) :
      PiNat.cylinder x 0 = Set.univ
      theorem PiNat.cylinder_anti {E : Type u_1} (x : (n : ) → E n) {m : } {n : } (h : m n) :
      @[simp]
      theorem PiNat.mem_cylinder_iff {E : Type u_1} {x : (n : ) → E n} {y : (n : ) → E n} {n : } :
      y PiNat.cylinder x n i < n, y i = x i
      theorem PiNat.self_mem_cylinder {E : Type u_1} (x : (n : ) → E n) (n : ) :
      theorem PiNat.mem_cylinder_iff_eq {E : Type u_1} {x : (n : ) → E n} {y : (n : ) → E n} {n : } :
      theorem PiNat.mem_cylinder_comm {E : Type u_1} (x : (n : ) → E n) (y : (n : ) → E n) (n : ) :
      theorem PiNat.mem_cylinder_iff_le_firstDiff {E : Type u_1} {x : (n : ) → E n} {y : (n : ) → E n} (hne : x y) (i : ) :
      theorem PiNat.mem_cylinder_firstDiff {E : Type u_1} (x : (n : ) → E n) (y : (n : ) → E n) :
      theorem PiNat.cylinder_eq_cylinder_of_le_firstDiff {E : Type u_1} (x : (n : ) → E n) (y : (n : ) → E n) {n : } (hn : n PiNat.firstDiff x y) :
      theorem PiNat.iUnion_cylinder_update {E : Type u_1} (x : (n : ) → E n) (n : ) :
      ⋃ (k : E n), PiNat.cylinder (Function.update x n k) (n + 1) = PiNat.cylinder x n
      theorem PiNat.update_mem_cylinder {E : Type u_1} (x : (n : ) → E n) (n : ) (y : E n) :
      def PiNat.res {α : Type u_2} (x : α) :
      List α

      In the case where E has constant value α, the cylinder cylinder x n can be identified with the element of List α consisting of the first n entries of x. See cylinder_eq_res. We call this list res x n, the restriction of x to n.

      Equations
      Instances For
        @[simp]
        theorem PiNat.res_zero {α : Type u_2} (x : α) :
        PiNat.res x 0 = []
        @[simp]
        theorem PiNat.res_succ {α : Type u_2} (x : α) (n : ) :
        PiNat.res x n.succ = x n :: PiNat.res x n
        @[simp]
        theorem PiNat.res_length {α : Type u_2} (x : α) (n : ) :
        (PiNat.res x n).length = n
        theorem PiNat.res_eq_res {α : Type u_2} {x : α} {y : α} {n : } :
        PiNat.res x n = PiNat.res y n ∀ ⦃m : ⦄, m < nx m = y m

        The restrictions of x and y to n are equal if and only if x m = y m for all m < n.

        theorem PiNat.res_injective {α : Type u_2} :
        theorem PiNat.cylinder_eq_res {α : Type u_2} (x : α) (n : ) :
        PiNat.cylinder x n = {y : α | PiNat.res y n = PiNat.res x n}

        cylinder x n is equal to the set of sequences y with the same restriction to n as x.

        A distance function on Π n, E n #

        We define a distance function on Π n, E n, given by dist x y = (1/2)^n where n is the first index at which x and y differ. When each E n has the discrete topology, this distance will define the right topology on the product space. We do not record a global Dist instance nor a MetricSpace instance, as other distances may be used on these spaces, but we register them as local instances in this section.

        def PiNat.dist {E : Type u_1} :
        Dist ((n : ) → E n)

        The distance function on a product space Π n, E n, given by dist x y = (1/2)^n where n is the first index at which x and y differ.

        Equations
        Instances For
          theorem PiNat.dist_eq_of_ne {E : Type u_1} {x : (n : ) → E n} {y : (n : ) → E n} (h : x y) :
          dist x y = (1 / 2) ^ PiNat.firstDiff x y
          theorem PiNat.dist_self {E : Type u_1} (x : (n : ) → E n) :
          dist x x = 0
          theorem PiNat.dist_comm {E : Type u_1} (x : (n : ) → E n) (y : (n : ) → E n) :
          dist x y = dist y x
          theorem PiNat.dist_nonneg {E : Type u_1} (x : (n : ) → E n) (y : (n : ) → E n) :
          0 dist x y
          theorem PiNat.dist_triangle_nonarch {E : Type u_1} (x : (n : ) → E n) (y : (n : ) → E n) (z : (n : ) → E n) :
          dist x z max (dist x y) (dist y z)
          theorem PiNat.dist_triangle {E : Type u_1} (x : (n : ) → E n) (y : (n : ) → E n) (z : (n : ) → E n) :
          dist x z dist x y + dist y z
          theorem PiNat.eq_of_dist_eq_zero {E : Type u_1} (x : (n : ) → E n) (y : (n : ) → E n) (hxy : dist x y = 0) :
          x = y
          theorem PiNat.mem_cylinder_iff_dist_le {E : Type u_1} {x : (n : ) → E n} {y : (n : ) → E n} {n : } :
          y PiNat.cylinder x n dist y x (1 / 2) ^ n
          theorem PiNat.apply_eq_of_dist_lt {E : Type u_1} {x : (n : ) → E n} {y : (n : ) → E n} {n : } (h : dist x y < (1 / 2) ^ n) {i : } (hi : i n) :
          x i = y i
          theorem PiNat.lipschitz_with_one_iff_forall_dist_image_le_of_mem_cylinder {E : Type u_1} {α : Type u_2} [PseudoMetricSpace α] {f : ((n : ) → E n)α} :
          (∀ (x y : (n : ) → E n), dist (f x) (f y) dist x y) ∀ (x y : (n : ) → E n) (n : ), y PiNat.cylinder x ndist (f x) (f y) (1 / 2) ^ n

          A function to a pseudo-metric-space is 1-Lipschitz if and only if points in the same cylinder of length n are sent to points within distance (1/2)^n. Not expressed using LipschitzWith as we don't have a metric space structure

          theorem PiNat.isOpen_cylinder (E : Type u_1) [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] (x : (n : ) → E n) (n : ) :
          theorem PiNat.isTopologicalBasis_cylinders (E : Type u_1) [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] :
          TopologicalSpace.IsTopologicalBasis {s : Set ((n : ) → E n) | ∃ (x : (n : ) → E n) (n : ), s = PiNat.cylinder x n}
          theorem PiNat.isOpen_iff_dist {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] (s : Set ((n : ) → E n)) :
          IsOpen s xs, ε > 0, ∀ (y : (n : ) → E n), dist x y < εy s
          def PiNat.metricSpace {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] :
          MetricSpace ((n : ) → E n)

          Metric space structure on Π (n : ℕ), E n when the spaces E n have the discrete topology, where the distance is given by dist x y = (1/2)^n, where n is the smallest index where x and y differ. Not registered as a global instance by default. Warning: this definition makes sure that the topology is defeq to the original product topology, but it does not take care of a possible uniformity. If the E n have a uniform structure, then there will be two non-defeq uniform structures on Π n, E n, the product one and the one coming from the metric structure. In this case, use metricSpaceOfDiscreteUniformity instead.

          Equations
          Instances For
            def PiNat.metricSpaceOfDiscreteUniformity {E : Type u_2} [(n : ) → UniformSpace (E n)] (h : ∀ (n : ), uniformity (E n) = Filter.principal idRel) :
            MetricSpace ((n : ) → E n)

            Metric space structure on Π (n : ℕ), E n when the spaces E n have the discrete uniformity, where the distance is given by dist x y = (1/2)^n, where n is the smallest index where x and y differ. Not registered as a global instance by default.

            Equations
            Instances For

              Metric space structure on ℕ → ℕ where the distance is given by dist x y = (1/2)^n, where n is the smallest index where x and y differ. Not registered as a global instance by default.

              Equations
              Instances For
                theorem PiNat.completeSpace {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] :
                CompleteSpace ((n : ) → E n)

                Retractions inside product spaces #

                We show that, in a space Π (n : ℕ), E n where each E n is discrete, there is a retraction on any closed nonempty subset s, i.e., a continuous map f from the whole space to s restricting to the identity on s. The map f is defined as follows. For x ∈ s, let f x = x. Otherwise, consider the longest prefix w that x shares with an element of s, and let f x = z_w where z_w is an element of s starting with w.

                theorem PiNat.exists_disjoint_cylinder {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] {s : Set ((n : ) → E n)} (hs : IsClosed s) {x : (n : ) → E n} (hx : xs) :
                ∃ (n : ), Disjoint s (PiNat.cylinder x n)
                def PiNat.shortestPrefixDiff {E : Type u_2} (x : (n : ) → E n) (s : Set ((n : ) → E n)) :

                Given a point x in a product space Π (n : ℕ), E n, and s a subset of this space, then shortestPrefixDiff x s if the smallest n for which there is no element of s having the same prefix of length n as x. If there is no such n, then use 0 by convention.

                Equations
                Instances For
                  theorem PiNat.firstDiff_lt_shortestPrefixDiff {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] {s : Set ((n : ) → E n)} (hs : IsClosed s) {x : (n : ) → E n} {y : (n : ) → E n} (hx : xs) (hy : y s) :
                  theorem PiNat.shortestPrefixDiff_pos {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] {s : Set ((n : ) → E n)} (hs : IsClosed s) (hne : s.Nonempty) {x : (n : ) → E n} (hx : xs) :
                  def PiNat.longestPrefix {E : Type u_2} (x : (n : ) → E n) (s : Set ((n : ) → E n)) :

                  Given a point x in a product space Π (n : ℕ), E n, and s a subset of this space, then longestPrefix x s if the largest n for which there is an element of s having the same prefix of length n as x. If there is no such n, use 0 by convention.

                  Equations
                  Instances For
                    theorem PiNat.firstDiff_le_longestPrefix {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] {s : Set ((n : ) → E n)} (hs : IsClosed s) {x : (n : ) → E n} {y : (n : ) → E n} (hx : xs) (hy : y s) :
                    theorem PiNat.inter_cylinder_longestPrefix_nonempty {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] {s : Set ((n : ) → E n)} (hs : IsClosed s) (hne : s.Nonempty) (x : (n : ) → E n) :
                    theorem PiNat.disjoint_cylinder_of_longestPrefix_lt {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] {s : Set ((n : ) → E n)} (hs : IsClosed s) {x : (n : ) → E n} (hx : xs) {n : } (hn : PiNat.longestPrefix x s < n) :
                    theorem PiNat.cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] {x : (n : ) → E n} {y : (n : ) → E n} {s : Set ((n : ) → E n)} (hs : IsClosed s) (hne : s.Nonempty) (H : PiNat.longestPrefix x s < PiNat.firstDiff x y) (xs : xs) (ys : ys) :

                    If two points x, y coincide up to length n, and the longest common prefix of x with s is strictly shorter than n, then the longest common prefix of y with s is the same, and both cylinders of this length based at x and y coincide.

                    theorem PiNat.exists_lipschitz_retraction_of_isClosed {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] {s : Set ((n : ) → E n)} (hs : IsClosed s) (hne : s.Nonempty) :
                    ∃ (f : ((n : ) → E n)(n : ) → E n), (∀ xs, f x = x) Set.range f = s LipschitzWith 1 f

                    Given a closed nonempty subset s of Π (n : ℕ), E n, there exists a Lipschitz retraction onto this set, i.e., a Lipschitz map with range equal to s, equal to the identity on s.

                    theorem PiNat.exists_retraction_of_isClosed {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] {s : Set ((n : ) → E n)} (hs : IsClosed s) (hne : s.Nonempty) :
                    ∃ (f : ((n : ) → E n)(n : ) → E n), (∀ xs, f x = x) Set.range f = s Continuous f

                    Given a closed nonempty subset s of Π (n : ℕ), E n, there exists a retraction onto this set, i.e., a continuous map with range equal to s, equal to the identity on s.

                    theorem PiNat.exists_retraction_subtype_of_isClosed {E : Type u_1} [(n : ) → TopologicalSpace (E n)] [∀ (n : ), DiscreteTopology (E n)] {s : Set ((n : ) → E n)} (hs : IsClosed s) (hne : s.Nonempty) :
                    ∃ (f : ((n : ) → E n)s), (∀ (x : s), f x = x) Function.Surjective f Continuous f

                    Any nonempty complete second countable metric space is the continuous image of the fundamental space ℕ → ℕ. For a version of this theorem in the context of Polish spaces, see exists_nat_nat_continuous_surjective_of_polishSpace.

                    Products of (possibly non-discrete) metric spaces #

                    def PiCountable.dist {ι : Type u_2} [Encodable ι] {F : ιType u_3} [(i : ι) → MetricSpace (F i)] :
                    Dist ((i : ι) → F i)

                    Given a countable family of metric spaces, one may put a distance on their product Π i, E i. It is highly non-canonical, though, and therefore not registered as a global instance. The distance we use here is dist x y = ∑' i, min (1/2)^(encode i) (dist (x i) (y i)).

                    Equations
                    • PiCountable.dist = { dist := fun (x y : (i : ι) → F i) => ∑' (i : ι), min ((1 / 2) ^ Encodable.encode i) (dist (x i) (y i)) }
                    Instances For
                      theorem PiCountable.dist_eq_tsum {ι : Type u_2} [Encodable ι] {F : ιType u_3} [(i : ι) → MetricSpace (F i)] (x : (i : ι) → F i) (y : (i : ι) → F i) :
                      dist x y = ∑' (i : ι), min ((1 / 2) ^ Encodable.encode i) (dist (x i) (y i))
                      theorem PiCountable.dist_summable {ι : Type u_2} [Encodable ι] {F : ιType u_3} [(i : ι) → MetricSpace (F i)] (x : (i : ι) → F i) (y : (i : ι) → F i) :
                      Summable fun (i : ι) => min ((1 / 2) ^ Encodable.encode i) (dist (x i) (y i))
                      theorem PiCountable.min_dist_le_dist_pi {ι : Type u_2} [Encodable ι] {F : ιType u_3} [(i : ι) → MetricSpace (F i)] (x : (i : ι) → F i) (y : (i : ι) → F i) (i : ι) :
                      min ((1 / 2) ^ Encodable.encode i) (dist (x i) (y i)) dist x y
                      theorem PiCountable.dist_le_dist_pi_of_dist_lt {ι : Type u_2} [Encodable ι] {F : ιType u_3} [(i : ι) → MetricSpace (F i)] {x : (i : ι) → F i} {y : (i : ι) → F i} {i : ι} (h : dist x y < (1 / 2) ^ Encodable.encode i) :
                      dist (x i) (y i) dist x y
                      def PiCountable.metricSpace {ι : Type u_2} [Encodable ι] {F : ιType u_3} [(i : ι) → MetricSpace (F i)] :
                      MetricSpace ((i : ι) → F i)

                      Given a countable family of metric spaces, one may put a distance on their product Π i, E i, defining the right topology and uniform structure. It is highly non-canonical, though, and therefore not registered as a global instance. The distance we use here is dist x y = ∑' n, min (1/2)^(encode i) (dist (x n) (y n)).

                      Equations
                      Instances For