Documentation

Mathlib.Topology.MetricSpace.Kuratowski

The Kuratowski embedding #

Any separable metric space can be embedded isometrically in ℓ^∞(ℕ, ℝ). Any partially defined Lipschitz map into ℓ^∞ can be extended to the whole space.

Any separable metric space can be embedded isometrically in ℓ^∞(ℕ, ℝ) #

source
def KuratowskiEmbedding.embeddingOfSubset {α : Type u} [MetricSpace α] (x : ℕ → α) (a : α) :
↥(lp (fun (i : ℕ) => ℝ) ⊤)

A metric space can be embedded in l^∞(ℝ) via the distances to points in a fixed countable set, if this set is dense. This map is given in kuratowskiEmbedding, without density assumptions.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem KuratowskiEmbedding.embeddingOfSubset_coe {α : Type u} {n : ℕ} [MetricSpace α] (x : ℕ → α) (a : α) :
    ↑(KuratowskiEmbedding.embeddingOfSubset x a) n = dist a (x n) - dist (x 0) (x n)
    source
    theorem KuratowskiEmbedding.embeddingOfSubset_dist_le {α : Type u} [MetricSpace α] (x : ℕ → α) (a : α) (b : α) :
    dist (KuratowskiEmbedding.embeddingOfSubset x a) (KuratowskiEmbedding.embeddingOfSubset x b) ≤ dist a b

    The embedding map is always a semi-contraction.

    source
    theorem KuratowskiEmbedding.embeddingOfSubset_isometry {α : Type u} [MetricSpace α] (x : ℕ → α) (H : DenseRange x) :
    Isometry (KuratowskiEmbedding.embeddingOfSubset x)

    When the reference set is dense, the embedding map is an isometry on its image.

    source
    theorem KuratowskiEmbedding.exists_isometric_embedding (α : Type u) [MetricSpace α] [TopologicalSpace.SeparableSpace α] :
    ∃ (f : α → ↥(lp (fun (i : ℕ) => ℝ) ⊤)), Isometry f

    Every separable metric space embeds isometrically in ℓ^∞(ℕ).

    source
    def kuratowskiEmbedding (α : Type u) [MetricSpace α] [TopologicalSpace.SeparableSpace α] :
    α → ↥(lp (fun (i : ℕ) => ℝ) ⊤)

    The Kuratowski embedding is an isometric embedding of a separable metric space in ℓ^∞(ℕ, ℝ).

    Equations
    Instances For
      source
      theorem kuratowskiEmbedding.isometry (α : Type u) [MetricSpace α] [TopologicalSpace.SeparableSpace α] :
      Isometry (kuratowskiEmbedding α)

      The Kuratowski embedding is an isometry. Theorem 2.1 of [Assaf Naor, Metric Embeddings and Lipschitz Extensions][Naor-2015].

      source
      def NonemptyCompacts.kuratowskiEmbedding (α : Type u) [MetricSpace α] [CompactSpace α] [Nonempty α] :
      TopologicalSpace.NonemptyCompacts ↥(lp (fun (i : ℕ) => ℝ) ⊤)

      Version of the Kuratowski embedding for nonempty compacts

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem LipschitzOnWith.extend_lp_infty {α : Type u} [PseudoMetricSpace α] {s : Set α} {ι : Type u_1} {f : α → ↥(lp (fun (i : ι) => ℝ) ⊤)} {K : NNReal} (hfl : LipschitzOnWith K f s) :
        ∃ (g : α → ↥(lp (fun (i : ι) => ℝ) ⊤)), LipschitzWith K g ∧ Set.EqOn f g s

        A function f : α → ℓ^∞(ι, ℝ) which is K-Lipschitz on a subset s admits a K-Lipschitz extension to the whole space.

        Theorem 2.2 of [Assaf Naor, Metric Embeddings and Lipschitz Extensions][Naor-2015]

        The same result for the case of a finite type ι is implemented in LipschitzOnWith.extend_pi.