mathlib3 documentation

topology.metric_space.gromov_hausdorff

Gromov-Hausdorff distance #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[protected, instance]
Equations
@[nolint]

A metric space representative of any abstract point in GH_space

Equations
Instances for Gromov_Hausdorff.GH_space.rep

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

@[protected, 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
noncomputable def Gromov_Hausdorff.GH_dist (X : Type u) (Y : Type v) [metric_space X] [nonempty X] [compact_space X] [metric_space Y] [nonempty Y] [compact_space 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

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.

@[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] [compact_space X] [nonempty X] {Y : Type v} [metric_space Y] [compact_space Y] [nonempty Y] {s : set X} (Φ : s Y) {ε₁ ε₂ ε₃ : } (hs : (x : X), (y : X) (H : y s), has_dist.dist x y ε₁) (hs' : (x : Y), (y : s), has_dist.dist x (Φ y) ε₃) (H : (x y : s), |has_dist.dist x y - has_dist.dist (Φ x) (Φ y)| ε₂) :
Gromov_Hausdorff.GH_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 + ε₃.

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.

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

Instances for Gromov_Hausdorff.aux_gluing_struct
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.