English
A subset t of GHSpace is totally bounded provided all spaces in t have uniformly bounded diameter and there are uniform finite ε-nets at every scale; i.e., a uniform discretization criterion ensures total boundedness.
Русский
Подмножество t пространства GHSpace пока его элементы имеют единственный предел диаметра и существует единство конечных ε-сеток на всех масштабах, так что выполняется условие единообразной дискретизации, обеспечивающее полноту предела.
LaTeX
$$$TotallyBounded\ t$, under hypotheses of uniform diameter bound and uniform finite coverings.$$
Lean4
/-- The Gromov-Hausdorff distance defines a genuine distance on the Gromov-Hausdorff space. -/
instance : MetricSpace GHSpace where
dist := dist
dist_self
x := by
rcases exists_rep x with ⟨y, hy⟩
refine le_antisymm ?_ ?_
· apply csInf_le
· exact ⟨0, by rintro b ⟨⟨u, v⟩, -, rfl⟩; exact hausdorffDist_nonneg⟩
· simp only [mem_image, mem_prod, mem_setOf_eq, Prod.exists]
exists y, y
simpa only [and_self_iff, hausdorffDist_self_zero, eq_self_iff_true, and_true]
· apply le_csInf
· exact Set.Nonempty.image _ <| Set.Nonempty.prod ⟨y, hy⟩ ⟨y, hy⟩
· rintro b ⟨⟨u, v⟩, -, rfl⟩; exact hausdorffDist_nonneg
dist_comm x
y :=
by
have A :
(fun p : NonemptyCompacts ℓ_infty_ℝ × NonemptyCompacts ℓ_infty_ℝ => hausdorffDist (p.1 : Set ℓ_infty_ℝ) p.2) ''
{a | ⟦a⟧ = x} ×ˢ {b | ⟦b⟧ = y} =
(fun p : NonemptyCompacts ℓ_infty_ℝ × NonemptyCompacts ℓ_infty_ℝ => hausdorffDist (p.1 : Set ℓ_infty_ℝ) p.2) ∘
Prod.swap ''
{a | ⟦a⟧ = x} ×ˢ {b | ⟦b⟧ = y} :=
by
funext
simp only [comp_apply, Prod.fst_swap, Prod.snd_swap]
congr
simp only [hausdorffDist_comm]
simp only [dist, A, image_comp, image_swap_prod]
eq_of_dist_eq_zero {x} {y}
hxy := by
/- To show that two spaces at zero distance are isometric,
we argue that the distance is realized by some coupling.
In this coupling, the two spaces are at zero Hausdorff distance,
i.e., they coincide. Therefore, the original spaces are isometric. -/
rcases ghDist_eq_hausdorffDist x.Rep y.Rep with ⟨Φ, Ψ, Φisom, Ψisom, DΦΨ⟩
rw [← dist_ghDist, hxy] at DΦΨ
have : range Φ = range Ψ :=
by
have hΦ : IsCompact (range Φ) := isCompact_range Φisom.continuous
have hΨ : IsCompact (range Ψ) := isCompact_range Ψisom.continuous
apply (IsClosed.hausdorffDist_zero_iff_eq _ _ _).1 DΦΨ.symm
· exact hΦ.isClosed
· exact hΨ.isClosed
·
exact
hausdorffEdist_ne_top_of_nonempty_of_bounded (range_nonempty _) (range_nonempty _) hΦ.isBounded hΨ.isBounded
have T : (range Ψ ≃ᵢ y.Rep) = (range Φ ≃ᵢ y.Rep) := by rw [this]
have eΨ := cast T Ψisom.isometryEquivOnRange.symm
have e := Φisom.isometryEquivOnRange.trans eΨ
rw [← x.toGHSpace_rep, ← y.toGHSpace_rep, toGHSpace_eq_toGHSpace_iff_isometryEquiv]
exact ⟨e⟩
dist_triangle x y
z := by
/- To show the triangular inequality between `X`, `Y` and `Z`,
realize an optimal coupling between `X` and `Y` in a space `γ1`,
and an optimal coupling between `Y` and `Z` in a space `γ2`.
Then, glue these metric spaces along `Y`. We get a new space `γ`
in which `X` and `Y` are optimally coupled, as well as `Y` and `Z`.
Apply the triangle inequality for the Hausdorff distance in `γ`
to conclude. -/
let X := x.Rep
let Y := y.Rep
let Z := z.Rep
let γ1 := OptimalGHCoupling X Y
let γ2 := OptimalGHCoupling Y Z
let Φ : Y → γ1 := optimalGHInjr X Y
have hΦ : Isometry Φ := isometry_optimalGHInjr X Y
let Ψ : Y → γ2 := optimalGHInjl Y Z
have hΨ : Isometry Ψ := isometry_optimalGHInjl Y Z
have Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z := toGlue_commute hΦ hΨ
calc
dist x z = dist (toGHSpace X) (toGHSpace Z) := by rw [x.toGHSpace_rep, z.toGHSpace_rep]
_ ≤ hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y)) (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z)) :=
(ghDist_le_hausdorffDist ((toGlueL_isometry hΦ hΨ).comp (isometry_optimalGHInjl X Y))
((toGlueR_isometry hΦ hΨ).comp (isometry_optimalGHInjr Y Z)))
_ ≤
hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y)) (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) +
hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z)) :=
by
refine
hausdorffDist_triangle <|
hausdorffEdist_ne_top_of_nonempty_of_bounded (range_nonempty _) (range_nonempty _) ?_ ?_
·
exact
(isCompact_range
(Isometry.continuous ((toGlueL_isometry hΦ hΨ).comp (isometry_optimalGHInjl X Y)))).isBounded
·
exact
(isCompact_range
(Isometry.continuous ((toGlueL_isometry hΦ hΨ).comp (isometry_optimalGHInjr X Y)))).isBounded
_ =
hausdorffDist (toGlueL hΦ hΨ '' range (optimalGHInjl X Y)) (toGlueL hΦ hΨ '' range (optimalGHInjr X Y)) +
hausdorffDist (toGlueR hΦ hΨ '' range (optimalGHInjl Y Z)) (toGlueR hΦ hΨ '' range (optimalGHInjr Y Z)) :=
by simp only [← range_comp, Comm]
_ =
hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) +
hausdorffDist (range (optimalGHInjl Y Z)) (range (optimalGHInjr Y Z)) :=
by rw [hausdorffDist_image (toGlueL_isometry hΦ hΨ), hausdorffDist_image (toGlueR_isometry hΦ hΨ)]
_ = dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z) := by
rw [hausdorffDist_optimal, hausdorffDist_optimal, ghDist, ghDist]
_ = dist x y + dist y z := by rw [x.toGHSpace_rep, y.toGHSpace_rep, z.toGHSpace_rep]
