The Fréchet–Kuratowski embedding of a pseudometric space

Every pseudometric space X embeds isometrically into the bounded continuous real functions on X, by the Fréchet–Kuratowski embedding x ↦ (y ↦ dist x y - dist x₀ y) based at a point x₀. Unlike Mathlib's KuratowskiEmbedding.embeddingOfSubset, which lands in ℓ^∞(ℕ) and needs a separable space, this embedding exists for every pseudometric space. It transfers metric statements proved for normed targets to arbitrary pseudometric targets.

A separable metric space moreover embeds isometrically into a separable Banach space: the closed linear span of the image of Mathlib's Kuratowski embedding into ℓ^∞(ℕ). This transfers statements proved for separable Banach spaces, such as those resting on Polish path spaces, to separable metric spaces.

Main definitions

• TauCeti.kuratowskiEmbedding x₀: the Fréchet–Kuratowski embedding X → X →ᵇ ℝ based at x₀.

Main results

• TauCeti.isometry_kuratowskiEmbedding: the Fréchet–Kuratowski embedding is an isometry.
• TauCeti.exists_isometry_separableSpace_completeSpace: a separable metric space embeds isometrically into a separable Banach space.

noncomputable def TauCeti.kuratowskiEmbedding {X : Type u_1} [PseudoMetricSpace X] (x₀ x : X) : BoundedContinuousFunction X ℝ

The Fréchet–Kuratowski embedding of a pseudometric space into the bounded continuous real functions on it, based at x₀: it sends x to y ↦ dist x y - dist x₀ y.

Equations

• TauCeti.kuratowskiEmbedding x₀ x = BoundedContinuousFunction.mkOfBound { toFun := fun (y : X) => dist x y - dist x₀ y, continuous_toFun := ⋯ } (2 * dist x x₀) ⋯

@[simp]

theorem TauCeti.kuratowskiEmbedding_apply {X : Type u_1} [PseudoMetricSpace X] (x₀ x y : X) : (kuratowskiEmbedding x₀ x) y = dist x y - dist x₀ y

The Fréchet–Kuratowski embedding of x evaluated at y.

theorem TauCeti.isometry_kuratowskiEmbedding {X : Type u_1} [PseudoMetricSpace X] (x₀ : X) : Isometry (kuratowskiEmbedding x₀)

The Fréchet–Kuratowski embedding is an isometry.

theorem TauCeti.exists_isometry_separableSpace_completeSpace (Y : Type u_2) [MetricSpace Y] [TopologicalSpace.SeparableSpace Y] : ∃ (E : Type) (x : NormedAddCommGroup E) (x_1 : NormedSpace ℝ E), CompleteSpace E ∧ TopologicalSpace.SeparableSpace E ∧ ∃ (f : Y → E), Isometry f

A separable metric space embeds isometrically into a separable real Banach space, namely the closed linear span of its image under Mathlib's Kuratowski embedding into ℓ^∞(ℕ, ℝ).