GHP bounds from a common probability source

Two measurable surjections from one probability space give a correspondence between the entire target carriers and a coupling of their image measures. If their distortion is at most twice a positive radius, approximate metric gluing bounds both Hausdorff and Lévy–Prokhorov distance by that radius. Paired source points can also serve as roots, with the same bound on their distance in the gluing.

The source needs only a measurable-space structure. Neither target measure is required to have full support. This extracts the common-source argument used in BGW.ContinuumTrees.CodingStability for reuse with spatial scaling.

theorem BGW.MetricMeasure.ghpDistance_map_le_of_distortion {S : Type v} {X Y : Type u} [MeasurableSpace S] [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] (μ : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure μ] (p : S → X) (q : S → Y) (hp : Measurable p) (hq : Measurable q) (hps : Function.Surjective p) (hqs : Function.Surjective q) {ε : ℝ} (hε : 0 < ε) (hdis : ∀ (s t : S), |dist (p s) (p t) - dist (q s) (q t)| ≤ 2 * ε) : ghpDistance (MeasureTheory.Measure.map p μ) (MeasureTheory.Measure.map q μ) ≤ 2 * ε

Surjective common-source maps with distortion at most 2 * ε give GHP at most 2 * ε.

theorem BGW.MetricMeasure.rootedGHPDistance_map_le_of_distortion {S : Type v} {X Y : Type u} [MeasurableSpace S] [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] (μ : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure μ] (p : S → X) (q : S → Y) (hp : Measurable p) (hq : Measurable q) (hps : Function.Surjective p) (hqs : Function.Surjective q) {ε : ℝ} (hε : 0 < ε) (hdis : ∀ (s t : S), |dist (p s) (p t) - dist (q s) (q t)| ≤ 2 * ε) (s₀ : S) : rootedGHPDistance (MeasureTheory.Measure.map p μ) (MeasureTheory.Measure.map q μ) (p s₀) (q s₀) ≤ 3 * ε

Pairing the roots at one source point adds at most one more gluing radius.