Gromov--Hausdorff stability of coded trees

The identity correspondence on the coding interval has distortion at most four times the uniform distance between two coding functions. Approximate metric gluing turns this into a Gromov--Hausdorff bound with constant two. Forgetting both the root and measure is the composition of the existing nonexpansive quotient maps.

theorem BGW.ContinuumTrees.Coding.ghDist_le_two_mul_norm (g h : C(↑unitInterval, ℝ)) : GromovHausdorff.ghDist (Space g) (Space h) ≤ 2 * ‖g - h‖

The Gromov--Hausdorff distance between the trees coded by g and h is at most 2 ‖g - h‖ (Le Gall 2005, Lemma 2.4; Duquesne--Le Gall 2005, Lemma 2.3) (C37.4).

theorem BGW.ContinuumTrees.Coding.lipschitzWith_two_toGHSpace : LipschitzWith 2 fun (g : C(↑unitInterval, ℝ)) => GromovHausdorff.toGHSpace (Space g)

The Gromov--Hausdorff class of the coded tree is a 2-Lipschitz function of the coding function (C37.4).

theorem BGW.MetricMeasure.RootedMeasuredGHSpace.lipschitzWith_underlyingGH_forgetRoot : LipschitzWith 1 (MeasuredGHSpace.underlyingGH ∘ forgetRoot)

Forgetting the root and the measure is 1-Lipschitz from rooted measured GHP to GH (C37.5).