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.
setoid instance identifying two isometric nonempty compact subspaces of ℓ^∞(ℝ)
Equations
- Gromov_Hausdorff.isometry_rel.setoid = {r := isometry_rel, iseqv := is_equivalence_isometry_rel}
The Gromov-Hausdorff space
Map any nonempty compact type to GH_space
A metric space representative of any abstract point in GH_space
Two nonempty compact spaces have the same image in GH_space if and only if they are isometric
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
- Gromov_Hausdorff.has_dist = {dist := λ (x y : Gromov_Hausdorff.GH_space), has_Inf.Inf ((λ (p : topological_space.nonempty_compacts ℓ_infty_ℝ × topological_space.nonempty_compacts ℓ_infty_ℝ), metric.Hausdorff_dist p.fst.val p.snd.val) '' {a : topological_space.nonempty_compacts ℓ_infty_ℝ | ⟦a⟧ = x}.prod {b : topological_space.nonempty_compacts ℓ_infty_ℝ | ⟦b⟧ = 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.
The Gromov-Hausdorff distance defines a genuine distance on the Gromov-Hausdorff space.
Equations
- Gromov_Hausdorff.GH_space_metric_space = {to_has_dist := Gromov_Hausdorff.has_dist, dist_self := Gromov_Hausdorff.GH_space_metric_space._proof_1, eq_of_dist_eq_zero := Gromov_Hausdorff.GH_space_metric_space._proof_2, dist_comm := Gromov_Hausdorff.GH_space_metric_space._proof_3, dist_triangle := Gromov_Hausdorff.GH_space_metric_space._proof_4, edist := λ (x y : Gromov_Hausdorff.GH_space), ennreal.of_real ((λ (x y : Gromov_Hausdorff.GH_space), has_Inf.Inf ((λ (p : topological_space.nonempty_compacts ℓ_infty_ℝ × topological_space.nonempty_compacts ℓ_infty_ℝ), metric.Hausdorff_dist p.fst.val p.snd.val) '' {a : topological_space.nonempty_compacts ℓ_infty_ℝ | ⟦a⟧ = x}.prod {b : topological_space.nonempty_compacts ℓ_infty_ℝ | ⟦b⟧ = y})) x y), edist_dist := Gromov_Hausdorff.GH_space_metric_space._proof_5, to_uniform_space := uniform_space_of_dist (λ (x y : Gromov_Hausdorff.GH_space), has_Inf.Inf ((λ (p : topological_space.nonempty_compacts ℓ_infty_ℝ × topological_space.nonempty_compacts ℓ_infty_ℝ), metric.Hausdorff_dist p.fst.val p.snd.val) '' {a : topological_space.nonempty_compacts ℓ_infty_ℝ | ⟦a⟧ = x}.prod {b : topological_space.nonempty_compacts ℓ_infty_ℝ | ⟦b⟧ = y})) Gromov_Hausdorff.GH_space_metric_space._proof_6 Gromov_Hausdorff.GH_space_metric_space._proof_7 Gromov_Hausdorff.GH_space_metric_space._proof_8, uniformity_dist := Gromov_Hausdorff.GH_space_metric_space._proof_9}
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
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 + ε₃.
The Gromov-Hausdorff space is second countable.
Equations
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.
- space : Type
- metric : metric_space c.space
- embed : A → c.space
- isom : isometry c.embed
Auxiliary structure used to glue metric spaces below, recording an isometric embedding
of a type A in another metric space.
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
- Gromov_Hausdorff.aux_gluing X n = n.rec_on {space := X 0, metric := _inst_1 0, embed := id (X 0), isom := _} (λ (n : ℕ) (a : Gromov_Hausdorff.aux_gluing_struct (X n)), let _inst : metric_space a.space := a.metric in {space := metric.glue_space _ _, metric := metric.metric_space_glue_space _ _, embed := metric.to_glue_r _ _ ∘ Gromov_Hausdorff.optimal_GH_injr (X n) (X n.succ), isom := _})
The Gromov-Hausdorff space is complete.