GromovHausdorff.HD_candidatesBDist_le
theorem GromovHausdorff.HD_candidatesBDist_le :
∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
[inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
GromovHausdorff.HD (GromovHausdorff.candidatesBDist X Y) ≤ Metric.diam Set.univ + 1 + Metric.diam Set.univ
The theorem `GromovHausdorff.HD_candidatesBDist_le` states that, for any two types `X` and `Y` where both are Metric Spaces, `X` is compact and nonempty, and `Y` is also compact and nonempty, the Gromov-Hausdorff Hausdorff distance (defined as `GromovHausdorff.HD`) of the candidate distance (`GromovHausdorff.candidatesBDist`) on `X` and `Y` is always less than or equal to the sum of the diameter of the universal set plus one and the diameter of the universal set. This means it is enough to search for functions with `HD(f)` bounded by this bound when looking for minimizers.
More concisely: Given compact and nonempty Metric Spaces X and Y, the Gromov-Hausdorff Hausdorff distance between their candidate distances is bounded above by the sum of the diameters of X and Y plus one.
|
GromovHausdorff.isometry_optimalGHInjr
theorem GromovHausdorff.isometry_optimalGHInjr :
∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
[inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
Isometry (GromovHausdorff.optimalGHInjr X Y)
The theorem `GromovHausdorff.isometry_optimalGHInjr` states that for any two types `X` and `Y` which are both metric spaces, compact spaces, and non-empty, the function `GromovHausdorff.optimalGHInjr X Y` is an isometry. In other words, this function, which represents the optimal Gromov-Hausdorff injection of `Y` into the coupling between `X` and `Y`, preserves the distance between any two points in `Y`, meaning the distance between any two points before the transformation is the same as the distance between these points after the transformation.
More concisely: The optimal Gromov-Hausdorff injection of a compact, non-empty metric space into another is an isometry.
|
GromovHausdorff.isometry_optimalGHInjl
theorem GromovHausdorff.isometry_optimalGHInjl :
∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
[inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
Isometry (GromovHausdorff.optimalGHInjl X Y)
The theorem `GromovHausdorff.isometry_optimalGHInjl` asserts that for any types `X` and `Y` endowed with a metric space structure, along with the properties of being compact and nonempty, the injection of `X` into the optimal Gromov-Hausdorff coupling of `X` and `Y` is an isometry. In other words, this mapping preserves the edistance (a generalization of the concept of distance) between any two points in `X`. This is a critical property in the context of Gromov-Hausdorff theory, which deals with comparing different metric spaces.
More concisely: The injection from a compact and nonempty metric space X into the optimal Gromov-Hausdorff distance between X and Y is an isometry.
|
GromovHausdorff.hausdorffDist_optimal_le_HD
theorem GromovHausdorff.hausdorffDist_optimal_le_HD :
∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
[inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y] {f : GromovHausdorff.Cb X Y},
f ∈ GromovHausdorff.candidatesB X Y →
Metric.hausdorffDist (Set.range (GromovHausdorff.optimalGHInjl X Y))
(Set.range (GromovHausdorff.optimalGHInjr X Y)) ≤
GromovHausdorff.HD f
The theorem `GromovHausdorff.hausdorffDist_optimal_le_HD` states for any two given types `X` and `Y` that are metric spaces, compact spaces, and nonempty, and for any candidate function `f` from the Borel-determined candidates between `X` and `Y`, the Hausdorff distance between the set of points in the optimal coupling of `X` and `Y` mapped by `f` from `X` and the set of points mapped by `f` from `Y` is less than or equal to the Hausdorff distance of `f` (`GromovHausdorff.HD f`). In other words, the Hausdorff distance in the optimal coupling is an lower bound for the Hausdorff distance of any candidate function.
More concisely: For any compact, nonempty metric spaces X and Y, and any Borel-determined function f between them, the Hausdorff distance between the images of the optimal coupling under f is less than or equal to the Hausdorff distance of f.
|