Stability of continuously coded measured trees

Uniform distance between coding functions bounds the distance between their interval minima and the distortion between the quotient projections. Gluing the two coded spaces along their common time parameter bounds Hausdorff distance, Lévy–Prokhorov distance and root distance simultaneously. With the project's sum convention, the resulting bounds are four times the uniform norm in GHP and six times that norm in rooted GHP.

The map to rooted measured isometry classes is therefore Lipschitz, continuous and measurable. All results hold for arbitrary continuous real coding functions, without sign or endpoint conditions. The common-source GHP bound uses Mathlib's approximate metric gluing; no measurable choice of time representatives is needed.

theorem BGW.ContinuumTrees.Coding.abs_intervalMin_sub_le_norm (g h : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) : |intervalMin g s t - intervalMin h s t| ≤ ‖g - h‖

The interval minimum changes by at most the uniform norm of the change in coding function.

theorem BGW.ContinuumTrees.Coding.abs_codingDist_sub_le_norm (g h : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) : |codingDist g s t - codingDist h s t| ≤ 4 * ‖g - h‖

The correspondence given by common times has distortion at most four uniform norms.

theorem BGW.ContinuumTrees.Coding.compactMeasuredSpace_distance_le (g h : C(↑unitInterval, ℝ)) : (compactMeasuredSpace g).distance (compactMeasuredSpace h) ≤ 4 * ‖g - h‖

Stability in the summed GHP distance, with the entire coded carriers retained.

theorem BGW.ContinuumTrees.Coding.rootedCompactMeasuredSpace_distance_le (g h : C(↑unitInterval, ℝ)) : (rootedCompactMeasuredSpace g).distance (rootedCompactMeasuredSpace h) ≤ 6 * ‖g - h‖

Stability in rooted GHP, using the sum of root, Hausdorff and Lévy–Prokhorov costs.

noncomputable def BGW.ContinuumTrees.Coding.rootedMeasuredGHSpace (g : C(↑unitInterval, ℝ)) : MetricMeasure.RootedMeasuredGHSpace

The rooted measured isometry class of the coded tree.

Equations

• BGW.ContinuumTrees.Coding.rootedMeasuredGHSpace g = BGW.MetricMeasure.toRootedMeasuredGHSpace (BGW.ContinuumTrees.Coding.rootedCompactMeasuredSpace g)

theorem BGW.ContinuumTrees.Coding.lipschitzWith_rootedMeasuredGHSpace : LipschitzWith 6 rootedMeasuredGHSpace

theorem BGW.ContinuumTrees.Coding.continuous_rootedMeasuredGHSpace : Continuous rootedMeasuredGHSpace

theorem BGW.ContinuumTrees.Coding.measurable_rootedMeasuredGHSpace : Measurable rootedMeasuredGHSpace