mathlibdocumentation

topology.metric_space.gromov_hausdorff

Gromov-Hausdorff distance #

This file defines the Gromov-Hausdorff distance on the space of nonempty compact metric spaces up to isometry.

We introduce the space of all nonempty compact metric spaces, up to isometry, called GH_space, and endow it with a metric space structure. The distance, known as the Gromov-Hausdorff distance, is defined as follows: given two nonempty compact spaces X and Y, their distance is the minimum Hausdorff distance between all possible isometric embeddings of X and Y in all metric spaces. To define properly the Gromov-Hausdorff space, we consider the non-empty compact subsets of ℓ^∞(ℝ) up to isometry, which is a well-defined type, and define the distance as the infimum of the Hausdorff distance over all embeddings in ℓ^∞(ℝ). We prove that this coincides with the previous description, as all separable metric spaces embed isometrically into ℓ^∞(ℝ), through an embedding called the Kuratowski embedding. To prove that we have a distance, we should show that if spaces can be coupled to be arbitrarily close, then they are isometric. More generally, the Gromov-Hausdorff distance is realized, i.e., there is a coupling for which the Hausdorff distance is exactly the Gromov-Hausdorff distance. This follows from a compactness argument, essentially following from Arzela-Ascoli.

Main results #

We prove the most important properties of the Gromov-Hausdorff space: it is a polish space, i.e., it is complete and second countable. We also prove the Gromov compactness criterion.

@[protected, instance]

setoid instance identifying two isometric nonempty compact subspaces of ℓ^∞(ℝ)

Equations

The Gromov-Hausdorff space

Equations

Map any nonempty compact type to GH_space

Equations
@[protected, instance]
Equations
@[nolint]

A metric space representative of any abstract point in GH_space

Equations
theorem Gromov_Hausdorff.eq_to_GH_space_iff {X : Type u} [metric_space X] [nonempty X] {p : topological_space.nonempty_compacts (lp (λ (n : ), ) )} :
∃ (Ψ : X → (lp (λ (n : ), ) )), = p.val
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]

Two nonempty compact spaces have the same image in GH_space if and only if they are isometric.

@[protected, instance]
noncomputable def Gromov_Hausdorff.GH_space.has_dist  :

Distance on GH_space: the distance between two nonempty compact spaces is the infimum Hausdorff distance between isometric copies of the two spaces in a metric space. For the definition, we only consider embeddings in ℓ^∞(ℝ), but we will prove below that it works for all spaces.

Equations
noncomputable def Gromov_Hausdorff.GH_dist (X : Type u) (Y : Type v) [metric_space X] [nonempty X] [metric_space Y] [nonempty Y]  :

The Gromov-Hausdorff distance between two nonempty compact metric spaces, equal by definition to the distance of the equivalence classes of these spaces in the Gromov-Hausdorff space.

Equations
theorem Gromov_Hausdorff.GH_dist_le_Hausdorff_dist {X : Type u} [metric_space X] [nonempty X] {Y : Type v} [metric_space Y] [nonempty Y] {γ : Type w} [metric_space γ] {Φ : X → γ} {Ψ : Y → γ} (ha : isometry Φ) (hb : isometry Ψ) :

The Gromov-Hausdorff distance between two spaces is bounded by the Hausdorff distance of isometric copies of the spaces, in any metric space.

theorem Gromov_Hausdorff.Hausdorff_dist_optimal {X : Type u} [metric_space X] [nonempty X] {Y : Type v} [metric_space Y] [nonempty Y] :

The optimal coupling constructed above realizes exactly the Gromov-Hausdorff distance, essentially by design.

theorem Gromov_Hausdorff.GH_dist_eq_Hausdorff_dist (X : Type u) [metric_space X] [nonempty X] (Y : Type v) [metric_space Y] [nonempty Y] :
∃ (Φ : X → (lp (λ (n : ), ) )) (Ψ : Y → (lp (λ (n : ), ) )),

The Gromov-Hausdorff distance can also be realized by a coupling in ℓ^∞(ℝ), by embedding the optimal coupling through its Kuratowski embedding.

@[protected, instance]

The Gromov-Hausdorff distance defines a genuine distance on the Gromov-Hausdorff space.

Equations

In particular, nonempty compacts of a metric space map to GH_space. We register this in the topological_space namespace to take advantage of the notation p.to_GH_space.

Equations
theorem Gromov_Hausdorff.GH_dist_le_of_approx_subsets {X : Type u} [metric_space X] [nonempty X] {Y : Type v} [metric_space Y] [nonempty Y] {s : set X} (Φ : s → Y) {ε₁ ε₂ ε₃ : } (hs : ∀ (x : X), ∃ (y : X) (H : y s), dist x y ε₁) (hs' : ∀ (x : Y), ∃ (y : s), dist x (Φ y) ε₃) (H : ∀ (x y : s), |dist x y - dist (Φ x) (Φ y)| ε₂) :
ε₁ + ε₂ / 2 + ε₃

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 + ε₃.

@[protected, instance]

The Gromov-Hausdorff space is second countable.

theorem Gromov_Hausdorff.totally_bounded {C : } {u : } {K : } (ulim : (𝓝 0)) (hdiam : ∀ (p : Gromov_Hausdorff.GH_space), p t) (hcov : ∀ (p : Gromov_Hausdorff.GH_space), p t∀ (n : ), ∃ (s : set p.rep), # s (K n) set.univ ⋃ (x : p.rep) (H : x s), (u n)) :

Compactness criterion: a closed set of compact metric spaces is compact if the spaces have a uniformly bounded diameter, and for all ε the number of balls of radius ε required to cover the spaces is uniformly bounded. This is an equivalence, but we only prove the interesting direction that these conditions imply compactness.

structure Gromov_Hausdorff.aux_gluing_struct (A : Type) [metric_space A] :
Type 1

Auxiliary structure used to glue metric spaces below, recording an isometric embedding of a type A in another metric space.

@[protected, instance]
Equations
noncomputable def Gromov_Hausdorff.aux_gluing (X : → Type) [Π (n : ), metric_space (X n)] [∀ (n : ), compact_space (X n)] [∀ (n : ), nonempty (X n)] (n : ) :

Auxiliary sequence of metric spaces, containing copies of X 0, ..., X n, where each X i is glued to X (i+1) in an optimal way. The space at step n+1 is obtained from the space at step n by adding X (n+1), glued in an optimal way to the X n already sitting there.

Equations
@[protected, instance]

The Gromov-Hausdorff space is complete.