Vertex and leaf measures on coded trees #
Uniform time is sent to empirical vertex and leaf measures by an explicit quantile map. A coupling on time pairs controls the Lévy–Prokhorov distance after projection into a coded tree. The quantile coupling gives discrete bounds, convergence under asymptotic equicontinuity, and a common-source comparison for finite plane trees. The coded-tree bound is the deterministic core of comparisons between vertex and leaf measures of large trees (J.-F. Le Gall, Random trees and applications, Probab. Surveys 2 (2005), Lemma 2.4 for the coding distance; P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Section 6, for the Prokhorov distance).
Time i / n of the index i among n points, as a point of [0,1] (clamped).
Equations
Instances For
Quantile rank: the index in {0, …, n-1} selected by the uniform time s
(⌊n s⌋, with s = 1 sent to n - 1).
Instances For
Uniform measure on the times i/n, i < n (vertex-time measure).
Equations
Instances For
Uniform measure on the times ℓ k / n, k < N (leaf-time measure).
Equations
- BGW.ContinuumTrees.LeafMeasure.leafTimeMeasure n N ℓ = (↑N)⁻¹ • ∑ k ∈ Finset.range N, MeasureTheory.Measure.dirac (BGW.ContinuumTrees.LeafMeasure.idxTime n (ℓ k))
Instances For
The quantile rank is measurable.
Quantile ranks of n points lie below n.
Pushing uniform time through rank n gives the empirical measure on Fin n.
The vertex-time measure is the pushforward of Lebesgue measure under the quantile map.
The leaf-time measure is the pushforward of Lebesgue measure under the leaf quantile map.
Quantile coupling bound: the leaf and vertex quantile times differ by at most
D + 1/N + 1/n.
Deterministic coupling estimate. If π is a coupling of μ and ν on [0,1]²
giving mass ≤ δ' to the set {|s - t| > δ}, and g oscillates by at most ω at time scale
δ, then the Prokhorov distance of the images in the coded tree is at most max δ' (2 ω).
Discrete estimate: for every continuous coding function g, the vertex-time and leaf-time
measures on the coded tree are within 2 ω in Prokhorov distance, where ω bounds the
oscillation
of g at time scale D + 1/N + 1/n.
Convergence consequence under asymptotic equicontinuity of the coding functions, explicit
leaf-index discrepancy D j → 0, and N j → ∞.
The case of uniform convergence of the coding functions g j → g₀ in C([0,1]).
Leaf addresses, in the DFS order of t.vertices.
Equations
- BGW.ContinuumTrees.LeafMeasure.leafAddrs t = List.filter (fun (u : List ℕ) => decide (BGW.ContinuumTrees.LeafMeasure.IsLeafAddr t u)) t.vertices
Instances For
Number of leaves (vertices without children).
Equations
Instances For
DFS index (position in t.vertices) of the k-th leaf; junk value 0 (the root's index)
for k ≥ numLeaves t.
Equations
Instances For
Uniform probability on the leaves (0 if there were no leaf; see numLeaves_pos).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every finite plane tree has a leaf.
A valid leaf index selects an address with no first child.
Valid leaf indices are strictly increasing in DFS order.
Quantile sampling pushes uniform time to the uniform leaf measure.
Transfer to a plane tree. The metric of Vertex t is the graph metric, for which
vertexEmbedding t is an isometry into Coding.Space t.contourFunction. The time scale is
D + 1/N + 2A + 3/n with A = ‖c‖ / (2 (n-1)) (c the contour function, n = t.size,
N = numLeaves t), hence at most the threshold in hω.