Documentation

Mathlib.Topology.MetricSpace.GromovHausdorff

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.

In this section, we define the Gromov-Hausdorff space, denoted GHSpace as the quotient of nonempty compact subsets of ℓ^∞(ℝ) by identifying isometric sets. Using the Kuratwoski embedding, we get a canonical map toGHSpace mapping any nonempty compact type to GHSpace.

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

Equations
Equations
  • One or more equations did not get rendered due to their size.

A metric space representative of any abstract point in GHSpace

Equations
Instances For
    theorem GromovHausdorff.eq_toGHSpace_iff {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X] {p : TopologicalSpace.NonemptyCompacts (lp (fun (n : ) => ) )} :
    p = GromovHausdorff.toGHSpace X ∃ (Ψ : X(lp (fun (n : ) => ) )), Isometry Ψ Set.range Ψ = p
    Equations

    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.

    Equations
    • One or more equations did not get rendered due to their size.

    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
    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.

      theorem GromovHausdorff.ghDist_eq_hausdorffDist (X : Type u) [MetricSpace X] [CompactSpace X] [Nonempty X] (Y : Type v) [MetricSpace Y] [CompactSpace Y] [Nonempty Y] :
      ∃ (Φ : X(lp (fun (n : ) => ) )) (Ψ : Y(lp (fun (n : ) => ) )), Isometry Φ Isometry Ψ GromovHausdorff.ghDist X Y = Metric.hausdorffDist (Set.range Φ) (Set.range Ψ)

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

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

      Equations
      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), ys, dist x y ε₁) (hs' : ∀ (x : Y), ∃ (y : s), 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 : pt, Metric.diam Set.univ C) (hcov : pt, ∀ (n : ), ∃ (s : Set p.Rep), Cardinal.mk s (K n) Set.univ xs, 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
          Equations
          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.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For