English
The Gromov–Hausdorff space is complete.
Русский
Пространство Громова–Хаусдорфа полно.
LaTeX
$$CompleteSpace(GHSpace).$$
Lean4
/-- If there are subsets which are `ε₁`-dense and `ε₃`-dense in two spaces, and
isometric up to `ε₂`, then the Gromov-Hausdorff distance between the spaces is bounded by
`ε₁ + ε₂/2 + ε₃`. -/
theorem ghDist_le_of_approx_subsets {s : Set X} (Φ : s → Y) {ε₁ ε₂ ε₃ : ℝ} (hs : ∀ x : X, ∃ y ∈ s, dist x y ≤ ε₁)
(hs' : ∀ x : Y, ∃ y : s, dist x (Φ y) ≤ ε₃) (H : ∀ x y : s, |dist x y - dist (Φ x) (Φ y)| ≤ ε₂) :
ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ := by
refine le_of_forall_pos_le_add fun δ δ0 => ?_
rcases exists_mem_of_nonempty X with ⟨xX, _⟩
rcases hs xX with ⟨xs, hxs, Dxs⟩
have sne : s.Nonempty := ⟨xs, hxs⟩
let _ : Nonempty s := sne.to_subtype
have : 0 ≤ ε₂ := le_trans (abs_nonneg _) (H ⟨xs, hxs⟩ ⟨xs, hxs⟩)
have : ∀ p q : s, |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ) := fun p q =>
calc
|dist p q - dist (Φ p) (Φ q)| ≤ ε₂ := H p q
_ ≤ 2 * (ε₂ / 2 + δ) := by
linarith
-- glue `X` and `Y` along the almost matching subsets
let _ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x : s => (x : X)) (fun x => Φ x) (ε₂ / 2 + δ) (by linarith) this
let Fl := @Sum.inl X Y
let Fr := @Sum.inr X Y
have Il : Isometry Fl := Isometry.of_dist_eq fun x y => rfl
have Ir : Isometry Fr := Isometry.of_dist_eq fun x y => rfl
have : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr) := ghDist_le_hausdorffDist Il Ir
have :
hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr) :=
have B : IsBounded (range Fl) := (isCompact_range Il.continuous).isBounded
hausdorffDist_triangle
(hausdorffEdist_ne_top_of_nonempty_of_bounded (range_nonempty _) (sne.image _) B
(B.subset (image_subset_range _ _)))
have :
hausdorffDist (Fl '' s) (range Fr) ≤
hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr) :=
have B : IsBounded (range Fr) := (isCompact_range Ir.continuous).isBounded
hausdorffDist_triangle'
(hausdorffEdist_ne_top_of_nonempty_of_bounded ((range_nonempty _).image _) (range_nonempty _)
(B.subset (image_subset_range _ _)) B)
have : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁ :=
by
rw [← image_univ, hausdorffDist_image Il]
have : 0 ≤ ε₁ := le_trans dist_nonneg Dxs
refine hausdorffDist_le_of_mem_dist this (fun x _ => hs x) fun x _ => ⟨x, mem_univ _, by simpa only [dist_self]⟩
have : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ :=
by
refine hausdorffDist_le_of_mem_dist (by linarith) ?_ ?_
· intro x' hx'
rcases (Set.mem_image _ _ _).1 hx' with ⟨x, ⟨x_in_s, xx'⟩⟩
rw [← xx']
use Fr (Φ ⟨x, x_in_s⟩), mem_image_of_mem Fr (mem_range_self _)
exact le_of_eq (glueDist_glued_points (fun x : s => (x : X)) Φ (ε₂ / 2 + δ) ⟨x, x_in_s⟩)
· intro x' hx'
rcases (Set.mem_image _ _ _).1 hx' with ⟨y, ⟨y_in_s', yx'⟩⟩
rcases mem_range.1 y_in_s' with ⟨x, xy⟩
use Fl x, mem_image_of_mem _ x.2
rw [← yx', ← xy, dist_comm]
exact le_of_eq (glueDist_glued_points (Z := s) (@Subtype.val X s) Φ (ε₂ / 2 + δ) x)
have : hausdorffDist (Fr '' range Φ) (range Fr) ≤ ε₃ :=
by
rw [← @image_univ _ _ Fr, hausdorffDist_image Ir]
rcases exists_mem_of_nonempty Y with ⟨xY, _⟩
rcases hs' xY with ⟨xs', Dxs'⟩
have : 0 ≤ ε₃ := le_trans dist_nonneg Dxs'
refine hausdorffDist_le_of_mem_dist this (fun x _ => ⟨x, mem_univ _, by simpa only [dist_self]⟩) fun x _ => ?_
rcases hs' x with ⟨y, Dy⟩
exact ⟨Φ y, mem_range_self _, Dy⟩
linarith
