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.

instance GromovHausdorff.IsometryRel.setoid : Setoid (TopologicalSpace.NonemptyCompacts ↥(lp (fun (n : ℕ) => ℝ) ⊤))

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

Equations

• GromovHausdorff.IsometryRel.setoid = { r := GromovHausdorff.IsometryRel✝, iseqv := GromovHausdorff.equivalence_isometryRel✝ }

def GromovHausdorff.GHSpace : Type

The Gromov-Hausdorff space

Equations

• GromovHausdorff.GHSpace = Quotient GromovHausdorff.IsometryRel.setoid

def GromovHausdorff.toGHSpace (X : Type u) [MetricSpace X] [CompactSpace X] [Nonempty X] : GromovHausdorff.GHSpace

Map any nonempty compact type to GHSpace

Equations

• GromovHausdorff.toGHSpace X = ⟦NonemptyCompacts.kuratowskiEmbedding X⟧

instance GromovHausdorff.instInhabitedGHSpace : Inhabited GromovHausdorff.GHSpace

Equations

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

def GromovHausdorff.GHSpace.Rep (p : GromovHausdorff.GHSpace) : Type

A metric space representative of any abstract point in GHSpace

Equations

• p.Rep = ↥(Quotient.out p)

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

theorem GromovHausdorff.eq_toGHSpace {p : TopologicalSpace.NonemptyCompacts ↥(lp (fun (n : ℕ) => ℝ) ⊤)} : ⟦p⟧ = GromovHausdorff.toGHSpace ↥p

instance GromovHausdorff.repGHSpaceMetricSpace {p : GromovHausdorff.GHSpace} : MetricSpace p.Rep

Equations

• GromovHausdorff.repGHSpaceMetricSpace = inferInstanceAs (MetricSpace ↥(Quotient.out p))

instance GromovHausdorff.rep_gHSpace_compactSpace {p : GromovHausdorff.GHSpace} : CompactSpace p.Rep

instance GromovHausdorff.rep_gHSpace_nonempty {p : GromovHausdorff.GHSpace} : Nonempty p.Rep

theorem GromovHausdorff.GHSpace.toGHSpace_rep (p : GromovHausdorff.GHSpace) : GromovHausdorff.toGHSpace p.Rep = p

theorem GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquiv {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X] {Y : Type v} [MetricSpace Y] [CompactSpace Y] [Nonempty Y] : GromovHausdorff.toGHSpace X = GromovHausdorff.toGHSpace Y ↔ Nonempty (X ≃ᵢ Y)

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

instance GromovHausdorff.instDistGHSpace : Dist GromovHausdorff.GHSpace

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.

def GromovHausdorff.ghDist (X : Type u) (Y : Type v) [MetricSpace X] [Nonempty X] [CompactSpace X] [MetricSpace Y] [Nonempty Y] [CompactSpace 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

• GromovHausdorff.ghDist X Y = dist (GromovHausdorff.toGHSpace X) (GromovHausdorff.toGHSpace Y)

theorem GromovHausdorff.dist_ghDist (p q : GromovHausdorff.GHSpace) : dist p q = GromovHausdorff.ghDist p.Rep q.Rep

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 Ψ) : GromovHausdorff.ghDist X Y ≤ Metric.hausdorffDist (Set.range Φ) (Set.range Ψ)

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

theorem GromovHausdorff.hausdorffDist_optimal {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X] {Y : Type v} [MetricSpace Y] [CompactSpace Y] [Nonempty Y] : Metric.hausdorffDist (Set.range (GromovHausdorff.optimalGHInjl X Y)) (Set.range (GromovHausdorff.optimalGHInjr X Y)) = GromovHausdorff.ghDist X Y

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.

instance GromovHausdorff.instMetricSpaceGHSpace : MetricSpace GromovHausdorff.GHSpace

The Gromov-Hausdorff distance defines a genuine distance on the Gromov-Hausdorff space.

Equations

• GromovHausdorff.instMetricSpaceGHSpace = MetricSpace.mk @GromovHausdorff.instMetricSpaceGHSpace.proof_24

def TopologicalSpace.NonemptyCompacts.toGHSpace {X : Type u} [MetricSpace X] (p : TopologicalSpace.NonemptyCompacts X) : GromovHausdorff.GHSpace

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

• p.toGHSpace = GromovHausdorff.toGHSpace ↥p

theorem GromovHausdorff.ghDist_le_nonemptyCompacts_dist {X : Type u} [MetricSpace X] (p q : TopologicalSpace.NonemptyCompacts X) : dist p.toGHSpace q.toGHSpace ≤ dist p q

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} (Φ : ↑s → Y) {ε₁ ε₂ ε₃ : ℝ} (hs : ∀ (x : X), ∃ y ∈ s, 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 + ε₃.

instance GromovHausdorff.instSecondCountableTopologyGHSpace : SecondCountableTopology GromovHausdorff.GHSpace

The Gromov-Hausdorff space is second countable.

theorem GromovHausdorff.totallyBounded {t : Set GromovHausdorff.GHSpace} {C : ℝ} {u : ℕ → ℝ} {K : ℕ → ℕ} (ulim : Filter.Tendsto u Filter.atTop (nhds 0)) (hdiam : ∀ p ∈ t, Metric.diam Set.univ ≤ C) (hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ (s : Set p.Rep), Cardinal.mk ↑s ≤ ↑(K n) ∧ Set.univ ⊆ ⋃ x ∈ s, Metric.ball x (u n)) : TotallyBounded 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 GromovHausdorff.AuxGluingStruct (A : Type) [MetricSpace A] : Type 1

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

• Space : Type
• metric : MetricSpace self.Space
• embed : A → self.Space
• isom : Isometry self.embed

instance GromovHausdorff.instInhabitedAuxGluingStruct (A : Type) [MetricSpace A] : Inhabited (GromovHausdorff.AuxGluingStruct A)

Equations

• GromovHausdorff.instInhabitedAuxGluingStruct A = { default := { Space := A, metric := inferInstance, embed := id, isom := ⋯ } }

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

instance GromovHausdorff.instCompleteSpaceGHSpace : CompleteSpace GromovHausdorff.GHSpace

The Gromov-Hausdorff space is complete.