GromovHausdorff.ghDist_le_of_approx_subsets
theorem GromovHausdorff.ghDist_le_of_approx_subsets :
∀ {X : Type u} [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X] {Y : Type v}
[inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y] {s : Set X} (Φ : ↑s → Y) {ε₁ ε₂ ε₃ : ℝ},
(∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁) →
(∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃) →
(∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂) → GromovHausdorff.ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃
This theorem states that given two types `X` and `Y` that are metric spaces, compact spaces, and nonempty, and given subsets of these spaces, if there are elements in `X` and `Y` such that the distance from any element to the subsets is less than or equal to `ε₁` and `ε₃` respectively, and the absolute difference of the distances between any two elements in the subsets and their images under a certain function `Φ` is less than or equal to `ε₂`, then the Gromov-Hausdorff distance between the two spaces is less than or equal to the sum of `ε₁`, half of `ε₂`, and `ε₃`. This theorem provides a bound on the Gromov-Hausdorff distance in terms of the given epsilon values.
More concisely: Given metric spaces `X` and `Y` that are compact and nonempty, if there exist elements with distances less than `ε₁` to their respective subsets and absolute difference of distances between any pair of elements in the subsets and their images under `Φ` is less than `ε₂`, then their Gromov-Hausdorff distance is less than or equal to `ε₁ + ε₂/2 + ε₃`.
|
GromovHausdorff.ghDist_eq_hausdorffDist
theorem GromovHausdorff.ghDist_eq_hausdorffDist :
∀ (X : Type u) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X] (Y : Type v)
[inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ GromovHausdorff.ghDist X Y = Metric.hausdorffDist (Set.range Φ) (Set.range Ψ)
This theorem states that the Gromov-Hausdorff distance between two nonempty compact metric spaces, given by types 'X' and 'Y', can also be realized by a coupling in the space of bounded sequences of real numbers. Specifically, there exist two isometric embeddings, Φ and Ψ, from 'X' and 'Y' respectively, such that the Gromov-Hausdorff distance between 'X' and 'Y' is equal to the Hausdorff distance between the range of Φ and the range of Ψ. This means that we can effectively measure the "distance" between the two metric spaces by looking at the distance between their isometric images in the space of bounded sequences of real numbers.
More concisely: The Gromov-Hausdorff distance between two compact metric spaces X and Y is equal to the Hausdorff distance between their isometric images in the space of bounded sequences of real numbers, realized by isometric embeddings Φ : X → R^(N) and Ψ : Y → R^(M) for some N and M.
|
GromovHausdorff.ghDist_le_hausdorffDist
theorem GromovHausdorff.ghDist_le_hausdorffDist :
∀ {X : Type u} [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X] {Y : Type v}
[inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y] {γ : Type w} [inst_6 : MetricSpace γ]
{Φ : X → γ} {Ψ : Y → γ},
Isometry Φ → Isometry Ψ → GromovHausdorff.ghDist X Y ≤ Metric.hausdorffDist (Set.range Φ) (Set.range Ψ)
This theorem states that for any two metric spaces X and Y, which are both nonempty and compact, and any other metric space γ, if there exist two isometry functions Φ: X → γ and Ψ: Y → γ, then the Gromov-Hausdorff distance between X and Y is bounded by (less than or equal to) the Hausdorff distance between the images of X and Y under Φ and Ψ respectively in the metric space γ. In simpler terms, this theorem is about comparing the distance between two spaces in terms of how they can be embedded isometrically in a common space.
More concisely: Given any nonempty, compact metric spaces X and Y, and a metric space γ, if there exist isometric embeddings Φ: X → γ and Ψ: Y → γ, then the Gromov-Hausdorff distance between X and Y is less than or equal to the Hausdorff distance between Φ(X) and Ψ(Y) in γ.
|
GromovHausdorff.hausdorffDist_optimal
theorem GromovHausdorff.hausdorffDist_optimal :
∀ {X : Type u} [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X] {Y : Type v}
[inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
Metric.hausdorffDist (Set.range (GromovHausdorff.optimalGHInjl X Y))
(Set.range (GromovHausdorff.optimalGHInjr X Y)) =
GromovHausdorff.ghDist X Y
The theorem `GromovHausdorff.hausdorffDist_optimal` states that for any two nonempty compact metric spaces `X` and `Y`, the Hausdorff distance between the ranges of the optimal Gromov-Hausdorff coupling injections of `X` and `Y` is equal to the Gromov-Hausdorff distance between `X` and `Y`. In other words, the optimal Gromov-Hausdorff coupling precisely realizes the Gromov-Hausdorff distance.
More concisely: The optimal Gromov-Hausdorff coupling injections between two nonempty compact metric spaces realize the Gromov-Hausdorff distance between them in terms of Hausdorff distance between their ranges.
|
GromovHausdorff.totallyBounded
theorem GromovHausdorff.totallyBounded :
∀ {t : Set GromovHausdorff.GHSpace} {C : ℝ} {u : ℕ → ℝ} {K : ℕ → ℕ},
Filter.Tendsto u Filter.atTop (nhds 0) →
(∀ p ∈ t, Metric.diam Set.univ ≤ C) →
(∀ p ∈ t, ∀ (n : ℕ), ∃ s, Cardinal.mk ↑s ≤ ↑(K n) ∧ Set.univ ⊆ ⋃ x ∈ s, Metric.ball x (u n)) →
TotallyBounded t
This theorem, named `GromovHausdorff.totallyBounded`, provides a compactness criterion for a closed set of compact metric spaces in the context of the Gromov-Hausdorff space. Specifically, it states that such a set is totally bounded (and thus compact) if two conditions are met:
1) The diameters of the spaces are uniformly bounded, i.e., for every space in the set, the distance between any two points in the space does not exceed a given constant `C`.
2) For any ε, represented as the limit of a sequence `u` tending to 0, the number of balls of radius ε that are needed to cover each space is uniformly bounded. This is expressed as the existence of a sequence `K` such that for each integer `n`, there exists a set `s` with cardinality not exceeding `K(n)` and covering the entire space using balls of radius `u(n)`.
If these conditions are satisfied, then the theorem concludes that the set of metric spaces is totally bounded.
More concisely: A set of compact metric spaces is totally bounded in the Gromov-Hausdorff topology if and only if the diameters of the spaces are uniformly bounded and the number of balls of arbitrarily small radius required to cover each space is uniformly finite.
|
GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquiv
theorem GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquiv :
∀ {X : Type u} [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X] {Y : Type v}
[inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
GromovHausdorff.toGHSpace X = GromovHausdorff.toGHSpace Y ↔ Nonempty (X ≃ᵢ Y)
This theorem, `GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquiv`, states that for any two non-empty compact spaces `X` and `Y` (both equipped with a metric space structure), they have the same image in the `GHSpace` (Gromov-Hausdorff space) if and only if there exists a nonempty isometry equivalence between `X` and `Y`. In other words, two such spaces are considered identical from the viewpoint of the Gromov-Hausdorff distance if they are isometric.
More concisely: Two compact metric spaces have the same image in the Gromov-Hausdorff space if and only if there exists a nonempty isometry between them.
|