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 GHSpace, 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 ℓ^∞(ℝ)

The Gromov-Hausdorff space

Instances For

    Map any nonempty compact type to GHSpace

    Instances For

      A metric space representative of any abstract point in GHSpace

      Instances For

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

        Distance on GHSpace: 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.

        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.

        Instances For
          theorem GromovHausdorff.ghDist_le_hausdorffDist {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X] {Y : Type v} [MetricSpace Y] [CompactSpace Y] [Nonempty Y] {γ : Type w} [MetricSpace γ] {Φ : 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.

          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.

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

          Instances For
            theorem GromovHausdorff.toGHSpace_lipschitz {X : Type u} [MetricSpace X] :
            LipschitzWith 1 TopologicalSpace.NonemptyCompacts.toGHSpace
            theorem GromovHausdorff.toGHSpace_continuous {X : Type u} [MetricSpace X] :
            Continuous TopologicalSpace.NonemptyCompacts.toGHSpace
            theorem GromovHausdorff.ghDist_le_of_approx_subsets {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X] {Y : Type v} [MetricSpace Y] [CompactSpace Y] [Nonempty Y] {s : Set X} (Φ : sY) {ε₁ : } {ε₂ : } {ε₃ : } (hs : ∀ (x : X), y, y s dist x y ε₁) (hs' : ∀ (x : Y), y, dist x (Φ y) ε₃) (H : ∀ (x y : s), |dist x y - dist (Φ x) (Φ y)| ε₂) :
            GromovHausdorff.ghDist 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 + ε₃.

            theorem GromovHausdorff.totallyBounded {t : Set GromovHausdorff.GHSpace} {C : } {u : } {K : } (ulim : Filter.Tendsto u Filter.atTop (nhds 0)) (hdiam : ∀ (p : GromovHausdorff.GHSpace), p tMetric.diam Set.univ C) (hcov : ∀ (p : GromovHausdorff.GHSpace), p t∀ (n : ), s, s ↑(K n) Set.univ ⋃ (x : GromovHausdorff.GHSpace.Rep p) (_ : x s), Metric.ball x (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.

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

            Instances For
              def GromovHausdorff.auxGluing (X : Type) [(n : ) → MetricSpace (X n)] [∀ (n : ), CompactSpace (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.

              Instances For