Separation for rooted measured GHP distance

Vanishing actual rooted costs give approximate maps of the whole compact carriers. Their uniform isometric limit preserves the probability measure by the ambient Prokhorov bounds. The additional root-distance bounds show that this same limit sends the first root to the second root.

The proof extends BGW.MetricMeasure.GHPSeparation, adapted from Freezing2/Geometry/GHPSeparation.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0). There is no full-support assumption and no assumed root-preserving isometry.

theorem BGW.MetricMeasure.exists_rootedGHPCoupling_cost_lt_of_eq_zero {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) (x : X) (y : Y) (hz : rootedGHPDistance μ ν x y = 0) {ε : ℝ} (hε : 0 < ε) : ∃ (C : GHPCoupling X Y), C.rootedCost μ ν x y < ε

Zero rooted distance supplies actual ambient realizations of arbitrarily small rooted cost.

theorem BGW.MetricMeasure.exists_measured_rooted_isometry_of_rootedGHPDistance_eq_zero {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) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (x : X) (y : Y) (hz : rootedGHPDistance μ ν x y = 0) : ∃ (e : X ≃ᵢ Y), MeasureTheory.Measure.map (⇑e) μ = ν ∧ e x = y

A single surjective isometry preserves both the measure and the distinguished point.

theorem BGW.MetricMeasure.rootedGHPDistance_eq_zero_iff_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) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (x : X) (y : Y) : rootedGHPDistance μ ν x y = 0 ↔ ∃ (e : X ≃ᵢ Y), MeasureTheory.Measure.map (⇑e) μ = ν ∧ e x = y

Zero rooted GHP distance is exactly whole-carrier, root- and measure-preserving isometry.