The Gromov-Hausdorff distance is realized

In this file, we construct of a good coupling between nonempty compact metric spaces, minimizing their Hausdorff distance. This construction is instrumental to study the Gromov-Hausdorff distance between nonempty compact metric spaces.

Given two nonempty compact metric spaces X and Y, we define OptimalGHCoupling X Y as a compact metric space, together with two isometric embeddings optimalGHInjl and optimalGHInjr respectively of X and Y into OptimalGHCoupling X Y. The main property of the optimal coupling is that the Hausdorff distance between X and Y in OptimalGHCoupling X Y is smaller than the corresponding distance in any other coupling. We do not prove completely this fact in this file, but we show a good enough approximation of this fact in hausdorffDist_optimal_le_HD, that will suffice to obtain the full statement once the Gromov-Hausdorff distance is properly defined, in hausdorffDist_optimal.

The key point in the construction is that the set of possible distances coming from isometric embeddings of X and Y in metric spaces is a set of equicontinuous functions. By Arzela-Ascoli, it is compact, and one can find such a distance which is minimal. This distance defines a premetric space structure on X ⊕ Y. The corresponding metric quotient is OptimalGHCoupling X Y.

This section shows that the Gromov-Hausdorff distance is realized. For this, we consider candidate distances on the disjoint union X ⊕ Y of two compact nonempty metric spaces, almost realizing the Gromov-Hausdorff distance, and show that they form a compact family by applying Arzela-Ascoli theorem. The existence of a minimizer follows.

def GromovHausdorff.candidates (X : Type u) (Y : Type v) [MetricSpace X] [MetricSpace Y] : Set (GromovHausdorff.ProdSpaceFun✝ X Y)

The set of functions on X ⊕ Y that are candidates distances to realize the minimum of the Hausdorff distances between X and Y in a coupling.

Equations

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

def GromovHausdorff.HD {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] (f : GromovHausdorff.Cb✝ X Y) : ℝ

We will then choose the candidate minimizing the Hausdorff distance. Except that we are not in a metric space setting, so we need to define our custom version of Hausdorff distance, called HD, and prove its basic properties.

Equations

• GromovHausdorff.HD f = (⨆ (x : X), ⨅ (y : Y), f (Sum.inl x, Sum.inr y)) ⊔ ⨆ (y : Y), ⨅ (x : X), f (Sum.inl x, Sum.inr y)

theorem GromovHausdorff.HD_below_aux1 {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] {f : GromovHausdorff.Cb✝ X Y} (C : ℝ) {x : X} : BddBelow (Set.range fun (y : Y) => f (Sum.inl x, Sum.inr y) + C)

theorem GromovHausdorff.HD_below_aux2 {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] {f : GromovHausdorff.Cb✝ X Y} (C : ℝ) {y : Y} : BddBelow (Set.range fun (x : X) => f (Sum.inl x, Sum.inr y) + C)

def GromovHausdorff.candidatesBOfCandidates {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] [CompactSpace X] [CompactSpace Y] (f : GromovHausdorff.ProdSpaceFun✝ X Y) (fA : f ∈ GromovHausdorff.candidates X Y) : GromovHausdorff.Cb✝ X Y

candidates give rise to elements of BoundedContinuousFunctions

Equations

• GromovHausdorff.candidatesBOfCandidates f fA = BoundedContinuousFunction.mkOfCompact { toFun := f, continuous_toFun := ⋯ }

theorem GromovHausdorff.candidatesBOfCandidates_mem {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] [CompactSpace X] [CompactSpace Y] (f : GromovHausdorff.ProdSpaceFun✝ X Y) (fA : f ∈ GromovHausdorff.candidates X Y) : GromovHausdorff.candidatesBOfCandidates f fA ∈ GromovHausdorff.candidatesB✝ X Y

def GromovHausdorff.candidatesBDist (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [CompactSpace Y] [Nonempty Y] : GromovHausdorff.Cb✝ X Y

The distance on X ⊕ Y as a candidate

Equations

• GromovHausdorff.candidatesBDist X Y = GromovHausdorff.candidatesBOfCandidates (fun (p : (X ⊕ Y) × (X ⊕ Y)) => dist p.1 p.2) ⋯

theorem GromovHausdorff.candidatesBDist_mem_candidatesB {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] [CompactSpace X] [CompactSpace Y] [Nonempty X] [Nonempty Y] : GromovHausdorff.candidatesBDist X Y ∈ GromovHausdorff.candidatesB✝ X Y

theorem GromovHausdorff.HD_candidatesBDist_le {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] [CompactSpace X] [CompactSpace Y] [Nonempty X] [Nonempty Y] : GromovHausdorff.HD (GromovHausdorff.candidatesBDist X Y) ≤ Metric.diam Set.univ + 1 + Metric.diam Set.univ

Explicit bound on HD (dist). This means that when looking for minimizers it will be sufficient to look for functions with HD(f) bounded by this bound.

def GromovHausdorff.premetricOptimalGHDist (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [CompactSpace Y] [Nonempty Y] : PseudoMetricSpace (X ⊕ Y)

With the optimal candidate, construct a premetric space structure on X ⊕ Y, on which the predistance is given by the candidate. Then, we will identify points at 0 predistance to obtain a genuine metric space.

Equations

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

def GromovHausdorff.OptimalGHCoupling (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [CompactSpace Y] [Nonempty Y] : Type (max v u)

A metric space which realizes the optimal coupling between X and Y

Equations

• GromovHausdorff.OptimalGHCoupling X Y = SeparationQuotient (X ⊕ Y)

instance GromovHausdorff.instMetricSpaceOptimalGHCoupling (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [CompactSpace Y] [Nonempty Y] : MetricSpace (GromovHausdorff.OptimalGHCoupling X Y)

Equations

• GromovHausdorff.instMetricSpaceOptimalGHCoupling X Y = id inferInstance

def GromovHausdorff.optimalGHInjl (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [CompactSpace Y] [Nonempty Y] (x : X) : GromovHausdorff.OptimalGHCoupling X Y

Injection of X in the optimal coupling between X and Y

Equations

• GromovHausdorff.optimalGHInjl X Y x = Quotient.mk'' (Sum.inl x)

theorem GromovHausdorff.isometry_optimalGHInjl (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [CompactSpace Y] [Nonempty Y] : Isometry (GromovHausdorff.optimalGHInjl X Y)

The injection of X in the optimal coupling between X and Y is an isometry.

def GromovHausdorff.optimalGHInjr (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [CompactSpace Y] [Nonempty Y] (y : Y) : GromovHausdorff.OptimalGHCoupling X Y

Injection of Y in the optimal coupling between X and Y

Equations

• GromovHausdorff.optimalGHInjr X Y y = Quotient.mk'' (Sum.inr y)

theorem GromovHausdorff.isometry_optimalGHInjr (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [CompactSpace Y] [Nonempty Y] : Isometry (GromovHausdorff.optimalGHInjr X Y)

The injection of Y in the optimal coupling between X and Y is an isometry.

instance GromovHausdorff.compactSpace_optimalGHCoupling (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [CompactSpace Y] [Nonempty Y] : CompactSpace (GromovHausdorff.OptimalGHCoupling X Y)

The optimal coupling between two compact spaces X and Y is still a compact space

theorem GromovHausdorff.hausdorffDist_optimal_le_HD (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [CompactSpace Y] [Nonempty Y] {f : GromovHausdorff.Cb✝ X Y} (h : f ∈ GromovHausdorff.candidatesB✝ X Y) : Metric.hausdorffDist (Set.range (GromovHausdorff.optimalGHInjl X Y)) (Set.range (GromovHausdorff.optimalGHInjr X Y)) ≤ GromovHausdorff.HD f

For any candidate f, HD(f) is larger than or equal to the Hausdorff distance in the optimal coupling. This follows from the fact that HD of the optimal candidate is exactly the Hausdorff distance in the optimal coupling, although we only prove here the inequality we need.