Comparing uniform vertex mass with contour mass

The uniform DFS sampler and the contour projection have the same probability source: Lebesgue measure on the unit interval. A sampled vertex is represented by its first contour visit. The time discrepancy is bounded by the contour height divided by twice the number of edges, plus twice the inverse number of vertices.

An oscillation bound on the spatially scaled contour controls the coding distance between these paired times. The resulting common-source correspondence has distortion at most four oscillation errors, so its rooted GHP distance is at most six errors. The finite measure is uniform on all vertices, including the root and leaves; the contour measure is the actual Lebesgue pushforward. This is a deterministic comparison, not an invariance principle or a convergence assertion.

theorem BGW.ContinuumTrees.Coding.codingDist_le_of_oscillation (g : C(↑unitInterval, ℝ)) {s t : ↑unitInterval} {δ ε : ℝ} (hst : |↑s - ↑t| ≤ δ) (hosc : ∀ (a b : ↑unitInterval), |↑a - ↑b| ≤ δ → |g a - g b| ≤ ε) : codingDist g s t ≤ 2 * ε

A modulus of oscillation controls coding distance between nearby times.

theorem BGW.ContinuumTrees.FiniteTree.rooted_distance_scale_contour_le (t : PlaneTree) (hn : 2 ≤ t.size) (factor : ℝ) (hfactor : 0 < factor) {ε : ℝ} (hε : 0 < ε) (hosc : ∀ (s r : ↑unitInterval), |↑s - ↑r| ≤ ‖t.contourFunction‖ / (2 * ↑(t.size - 1)) + 2 / ↑t.size → |(factor • t.contourFunction) s - (factor • t.contourFunction) r| ≤ ε) : (MetricMeasure.RootedCompactMeasuredSpace.scale factor hfactor (rootedCompactMeasuredSpace t)).distance (Coding.rootedCompactMeasuredSpace (factor • t.contourFunction)) ≤ 6 * ε

Uniform vertex mass and contour mass are close when the scaled contour has small oscillation on the deterministic first-visit time discrepancy.