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.

source
@[protected, instance]
def Gromov_Hausdorff.isometry_rel.setoid  :
setoid (topological_space.nonempty_compacts ↥(lp (λ (n : ℕ), ℝ) ⊤))

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

Equations
source
def Gromov_Hausdorff.GH_space  :
Type

The Gromov-Hausdorff space

Equations
Instances for Gromov_Hausdorff.GH_space
source
def Gromov_Hausdorff.to_GH_space (X : Type u) [metric_space X] [compact_space X] [nonempty X] :
Gromov_Hausdorff.GH_space

Map any nonempty compact type to GH_space

Equations
source
@[protected, instance]
def Gromov_Hausdorff.GH_space.inhabited  :
inhabited Gromov_Hausdorff.GH_space
Equations
source
@[nolint]
def Gromov_Hausdorff.GH_space.rep (p : Gromov_Hausdorff.GH_space) :
Type

A metric space representative of any abstract point in GH_space

Equations
Instances for Gromov_Hausdorff.GH_space.rep
source
theorem Gromov_Hausdorff.eq_to_GH_space_iff {X : Type u} [metric_space X] [compact_space X] [nonempty X] {p : topological_space.nonempty_compacts ↥(lp (λ (n : ℕ), ℝ) ⊤)} :
⟦p⟧ = Gromov_Hausdorff.to_GH_space X ↔ ∃ (Ψ : X → ↥(lp (λ (n : ℕ), ℝ) ⊤)), isometry Ψ ∧ set.range Ψ = ↑p
source
theorem Gromov_Hausdorff.eq_to_GH_space {p : topological_space.nonempty_compacts ↥(lp (λ (n : ℕ), ℝ) ⊤)} :
⟦p⟧ = Gromov_Hausdorff.to_GH_space ↥p
source
@[protected, instance]
noncomputable def Gromov_Hausdorff.rep_GH_space_metric_space {p : Gromov_Hausdorff.GH_space} :
metric_space p.rep
Equations
source
@[protected, instance]
def Gromov_Hausdorff.rep_GH_space_compact_space {p : Gromov_Hausdorff.GH_space} :
compact_space p.rep
source
@[protected, instance]
def Gromov_Hausdorff.rep_GH_space_nonempty {p : Gromov_Hausdorff.GH_space} :
nonempty p.rep
source
theorem Gromov_Hausdorff.GH_space.to_GH_space_rep (p : Gromov_Hausdorff.GH_space) :
Gromov_Hausdorff.to_GH_space p.rep = p
source
theorem Gromov_Hausdorff.to_GH_space_eq_to_GH_space_iff_isometry_equiv {X : Type u} [metric_space X] [compact_space X] [nonempty X] {Y : Type v} [metric_space Y] [compact_space Y] [nonempty Y] :
Gromov_Hausdorff.to_GH_space X = Gromov_Hausdorff.to_GH_space Y ↔ nonempty (X ≃ᵢ Y)

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

source
@[protected, instance]
noncomputable def Gromov_Hausdorff.GH_space.has_dist  :
has_dist Gromov_Hausdorff.GH_space

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
source
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
source
theorem Gromov_Hausdorff.dist_GH_dist (p q : Gromov_Hausdorff.GH_space) :
has_dist.dist p q = Gromov_Hausdorff.GH_dist p.rep q.rep
source
theorem Gromov_Hausdorff.GH_dist_le_Hausdorff_dist {X : Type u} [metric_space X] [compact_space X] [nonempty X] {Y : Type v} [metric_space Y] [compact_space Y] [nonempty Y] {γ : Type w} [metric_space γ] {Φ : X → γ} {Ψ : Y → γ} (ha : isometry Φ) (hb : isometry Ψ) :
Gromov_Hausdorff.GH_dist X Y ≤ metric.Hausdorff_dist (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.

source
theorem Gromov_Hausdorff.Hausdorff_dist_optimal {X : Type u} [metric_space X] [compact_space X] [nonempty X] {Y : Type v} [metric_space Y] [compact_space Y] [nonempty Y] :
metric.Hausdorff_dist (set.range (Gromov_Hausdorff.optimal_GH_injl X Y)) (set.range (Gromov_Hausdorff.optimal_GH_injr X Y)) = Gromov_Hausdorff.GH_dist X Y

The optimal coupling constructed above realizes exactly the Gromov-Hausdorff distance, essentially by design.

source
theorem Gromov_Hausdorff.GH_dist_eq_Hausdorff_dist (X : Type u) [metric_space X] [compact_space X] [nonempty X] (Y : Type v) [metric_space Y] [compact_space Y] [nonempty Y] :
∃ (Φ : X → ↥(lp (λ (n : ℕ), ℝ) ⊤)) (Ψ : Y → ↥(lp (λ (n : ℕ), ℝ) ⊤)), isometry Φ ∧ isometry Ψ ∧ Gromov_Hausdorff.GH_dist X Y = metric.Hausdorff_dist (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.

source
@[protected, instance]
noncomputable def Gromov_Hausdorff.GH_space.metric_space  :
metric_space Gromov_Hausdorff.GH_space

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

Equations
source
def topological_space.nonempty_compacts.to_GH_space {X : Type u} [metric_space X] (p : topological_space.nonempty_compacts X) :
Gromov_Hausdorff.GH_space

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
source
theorem Gromov_Hausdorff.GH_dist_le_nonempty_compacts_dist {X : Type u} [metric_space X] (p q : topological_space.nonempty_compacts X) :
has_dist.dist p.to_GH_space q.to_GH_space ≤ has_dist.dist p q
source
theorem Gromov_Hausdorff.to_GH_space_lipschitz {X : Type u} [metric_space X] :
lipschitz_with 1 topological_space.nonempty_compacts.to_GH_space
source
theorem Gromov_Hausdorff.to_GH_space_continuous {X : Type u} [metric_space X] :
continuous topological_space.nonempty_compacts.to_GH_space
source
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 + ε₃.

source
@[protected, instance]
def Gromov_Hausdorff.GH_space.topological_space.second_countable_topology  :
topological_space.second_countable_topology Gromov_Hausdorff.GH_space

The Gromov-Hausdorff space is second countable.

source
theorem Gromov_Hausdorff.totally_bounded {t : set Gromov_Hausdorff.GH_space} {C : ℝ} {u : ℕ → ℝ} {K : ℕ → ℕ} (ulim : filter.tendsto u filter.at_top (nhds 0)) (hdiam : ∀ (p : Gromov_Hausdorff.GH_space), p ∈ t → metric.diam set.univ ≤ C) (hcov : ∀ (p : Gromov_Hausdorff.GH_space), p ∈ t → ∀ (n : ℕ), ∃ (s : set p.rep), cardinal.mk ↥s ≤ ↑(K n) ∧ set.univ ⊆ ⋃ (x : p.rep) (H : x ∈ s), metric.ball x (u n)) :
totally_bounded 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.

source
structure Gromov_Hausdorff.aux_gluing_struct (A : Type) [metric_space A] :
Type 1

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
source
@[protected, instance]
def Gromov_Hausdorff.aux_gluing_struct.inhabited (A : Type) [metric_space A] :
inhabited (Gromov_Hausdorff.aux_gluing_struct A)
Equations
source
noncomputable def Gromov_Hausdorff.aux_gluing (X : ℕ → Type) [Π (n : ℕ), metric_space (X n)] [∀ (n : ℕ), compact_space (X n)] [∀ (n : ℕ), nonempty (X n)] (n : ℕ) :
Gromov_Hausdorff.aux_gluing_struct (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
source
@[protected, instance]
def Gromov_Hausdorff.GH_space.complete_space  :
complete_space Gromov_Hausdorff.GH_space

The Gromov-Hausdorff space is complete.