mathlib documentation

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.

@[instance]

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

Equations
@[instance]

Equations

A metric space representative of any abstract point in GH_space

Equations

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

@[instance]

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
def Gromov_Hausdorff.GH_dist (α : Type u) (β : Type v) [metric_space α] [nonempty α] [compact_space α] [metric_space β] [nonempty β] [compact_space β] :

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 {α : Type u} [metric_space α] [compact_space α] [nonempty α] {β : Type v} [metric_space β] [compact_space β] [nonempty β] {γ : Type w} [metric_space γ] {Φ : α → γ} {Ψ : β → γ} :

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

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

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

@[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 {α : Type u} [metric_space α] [compact_space α] [nonempty α] {β : Type v} [metric_space β] [compact_space β] [nonempty β] {s : set α} (Φ : s → β) {ε₁ ε₂ ε₃ : } :
(∀ (x : α), ∃ (y : α) (H : y s), dist x y ε₁)(∀ (x : β), ∃ (y : s), dist x (Φ y) ε₃)(∀ (x y : s), abs (dist x y - dist (Φ x) (Φ y)) ε₂)Gromov_Hausdorff.GH_dist α β ε₁ + ε₂ / 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 + ε₃.

@[instance]

The Gromov-Hausdorff space is second countable.

theorem Gromov_Hausdorff.totally_bounded {t : set Gromov_Hausdorff.GH_space} {C : } {u : } {K : } :
filter.tendsto u filter.at_top (𝓝 0)(∀ (p : Gromov_Hausdorff.GH_space), p tmetric.diam set.univ C)(∀ (p : Gromov_Hausdorff.GH_space), p t∀ (n : ), ∃ (s : set p.rep), # s (K n) set.univ ⋃ (x : p.rep) (H : x s), metric.ball x (u n))totally_bounded t

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.

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
@[instance]

The Gromov-Hausdorff space is complete.