English
If Φ, Ψ are isometries from X, Y into γ, then ghDist X Y ≤ hausdorffDist(range Φ, range Ψ).
Русский
Если Φ, Ψ – изометрии от X, Y в γ, то ghDist(X, Y) не превосходит hausdorffDist(range Φ, range Ψ).
LaTeX
$$$\text{If } \Phi: X \to \gamma, \Psi: Y \to \gamma \text{ are isometries, then } ghDist(X,Y) \le hausdorffDist( range(\Phi), range(\Psi) ).$$$
Lean4
/-- The Gromov-Hausdorff distance between two spaces is bounded by the Hausdorff distance
of isometric copies of the spaces, in any metric space. -/
theorem ghDist_le_hausdorffDist {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X] {Y : Type v} [MetricSpace Y]
[CompactSpace Y] [Nonempty Y] {γ : Type w} [MetricSpace γ] {Φ : X → γ} {Ψ : Y → γ} (ha : Isometry Φ)
(hb : Isometry Ψ) : ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ) := by
/- For the proof, we want to embed `γ` in `ℓ^∞(ℝ)`, to say that the Hausdorff distance is realized
in `ℓ^∞(ℝ)` and therefore bounded below by the Gromov-Hausdorff-distance. However, `γ` is not
separable in general. We restrict to the union of the images of `X` and `Y` in `γ`, which is
separable and therefore embeddable in `ℓ^∞(ℝ)`. -/
rcases exists_mem_of_nonempty X with ⟨xX, _⟩
let s : Set γ := range Φ ∪ range Ψ
let Φ' : X → Subtype s := fun y => ⟨Φ y, mem_union_left _ (mem_range_self _)⟩
let Ψ' : Y → Subtype s := fun y => ⟨Ψ y, mem_union_right _ (mem_range_self _)⟩
have IΦ' : Isometry Φ' := fun x y => ha x y
have IΨ' : Isometry Ψ' := fun x y => hb x y
have : IsCompact s := (isCompact_range ha.continuous).union (isCompact_range hb.continuous)
let _ : MetricSpace (Subtype s) := by infer_instance
have : CompactSpace (Subtype s) := ⟨isCompact_iff_isCompact_univ.1 ‹IsCompact s›⟩
have ΦΦ' : Φ = Subtype.val ∘ Φ' := rfl
have ΨΨ' : Ψ = Subtype.val ∘ Ψ' := rfl
have : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ') :=
by
rw [ΦΦ', ΨΨ', range_comp, range_comp]
exact hausdorffDist_image isometry_subtype_coe
rw [this]
-- Embed `s` in `ℓ^∞(ℝ)` through its Kuratowski embedding
let F := kuratowskiEmbedding (Subtype s)
have : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ') :=
hausdorffDist_image (kuratowskiEmbedding.isometry _)
rw [← this]
-- Let `A` and `B` be the images of `X` and `Y` under this embedding. They are in `ℓ^∞(ℝ)`, and
-- their Hausdorff distance is the same as in the original space.
let A : NonemptyCompacts ℓ_infty_ℝ :=
⟨⟨F '' range Φ', (isCompact_range IΦ'.continuous).image (kuratowskiEmbedding.isometry _).continuous⟩,
(range_nonempty _).image _⟩
let B : NonemptyCompacts ℓ_infty_ℝ :=
⟨⟨F '' range Ψ', (isCompact_range IΨ'.continuous).image (kuratowskiEmbedding.isometry _).continuous⟩,
(range_nonempty _).image _⟩
have AX : ⟦A⟧ = toGHSpace X := by
rw [eq_toGHSpace_iff]
exact ⟨fun x => F (Φ' x), (kuratowskiEmbedding.isometry _).comp IΦ', range_comp _ _⟩
have BY : ⟦B⟧ = toGHSpace Y := by
rw [eq_toGHSpace_iff]
exact ⟨fun x => F (Ψ' x), (kuratowskiEmbedding.isometry _).comp IΨ', range_comp _ _⟩
refine csInf_le ⟨0, ?_⟩ ?_
· simp only [lowerBounds, mem_image, mem_prod, mem_setOf_eq, Prod.exists, and_imp, forall_exists_index]
intro t _ _ _ _ ht
rw [← ht]
exact hausdorffDist_nonneg
apply (mem_image _ _ _).2
exists (⟨A, B⟩ : NonemptyCompacts ℓ_infty_ℝ × NonemptyCompacts ℓ_infty_ℝ)
