Forgetting the measure contracts GHP to GH

Every measured ambient cost contains the ordinary Hausdorff cost of the same isometric embeddings. Thus the exact Gromov--Hausdorff distance is bounded by the exact measured infimum. In particular zero GHP distance forces a whole-space isometry; preservation of the measure is a further obligation.

Adapted from Freezing2/Geometry/GHPUnderlyingGH.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

theorem BGW.MetricMeasure.ghDist_le_ghpDistance {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] [Nonempty Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : GromovHausdorff.ghDist X Y ≤ ghpDistance μ ν

Forgetting the probability measure cannot increase the GHP distance.

theorem BGW.MetricMeasure.nonempty_isometryEquiv_of_ghpDistance_eq_zero {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] [Nonempty Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (h : ghpDistance μ ν = 0) : Nonempty (X ≃ᵢ Y)

Zero measured distance already forces an isometry of the entire compact carriers, including any points outside the measure supports.

theorem BGW.MetricMeasure.ghpDistance_eq_zero_of_measured_isometry {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (e : X ≃ᵢ Y) (he : MeasureTheory.Measure.map (⇑e) μ = ν) : ghpDistance μ ν = 0

A measured isometry always gives zero distance. The converse additionally requires proving that a zero-distance isometry can preserve the measures.