English
There exist Φ, Ψ as above realizing ghDist through the Hausdorff distance of their ranges, using the Kuratowski embedding of the optimal coupling.
Русский
Существуют Φ, Ψ как выше, реализующие ghDist через хаусдорфову дистанцию между диапазонами их образов, используя вложение Куротовского оптимального связывания.
LaTeX
$$$\exists Φ, Ψ : X, Y \to ℓ_\infty(\mathbb{R}), Isometry(Φ) ∧ Isometry(Ψ) ∧ ghDist X Y = hausdorffDist( range Φ, range Ψ ).$$$
Lean4
/-- The Gromov-Hausdorff distance can also be realized by a coupling in `ℓ^∞(ℝ)`, by embedding
the optimal coupling through its Kuratowski embedding. -/
theorem ghDist_eq_hausdorffDist (X : Type u) [MetricSpace X] [CompactSpace X] [Nonempty X] (Y : Type v) [MetricSpace Y]
[CompactSpace Y] [Nonempty Y] :
∃ Φ : X → ℓ_infty_ℝ,
∃ Ψ : Y → ℓ_infty_ℝ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ) :=
by
let F := kuratowskiEmbedding (OptimalGHCoupling X Y)
let Φ := F ∘ optimalGHInjl X Y
let Ψ := F ∘ optimalGHInjr X Y
refine ⟨Φ, Ψ, ?_, ?_, ?_⟩
· exact (kuratowskiEmbedding.isometry _).comp (isometry_optimalGHInjl X Y)
· exact (kuratowskiEmbedding.isometry _).comp (isometry_optimalGHInjr X Y)
· rw [← image_univ, ← image_univ, image_comp F, image_univ, image_comp F (optimalGHInjr X Y), image_univ, ←
hausdorffDist_optimal]
exact (hausdorffDist_image (kuratowskiEmbedding.isometry _)).symm
