The global contour and height comparison

First-visit times recover all DFS heights from the contour. Compact sets of contours control their suprema and oscillations, making the first-visit clock displacement vanish.

theorem BGW.StableTrees.ExactContour.eventually_globalError_le_of_compact {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (K : Set C(↑unitInterval, ℝ)) (hK : IsCompact K) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : PlaneTree), t.size = n → treeContourPath B n 1 t.toLocallyFinite ∈ K → contourHeightError B n 1 t.toLocallyFinite ≤ ε

On compact sets of normalized contours, the global height/contour error vanishes.

theorem BGW.StableTrees.ExactContour.contourHeightError_eq_dist (B : ℕ → ℝ) (n : ℕ) (a : NNReal) (τ : LocallyFinite.Tree) : contourHeightError B n a τ = dist (treeContourPath B n a τ) (TailPair.treeHeightPath B n a τ)

The uniform contour/height error is exactly the distance between the continuous paths.

theorem BGW.StableTrees.ExactContour.tendsto_contourHeightError {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (k : ℕ) => (↑(DiscreteForest.exactTreeLaw μ (q k))).real {τ : LocallyFinite.Tree | ε < contourHeightError B (q k) 1 τ}) Filter.atTop (nhds 0)

Global contour/height error on [0,1] (first visits H_i = C(2i - H_i), sup H ≤ sup C, contour equicontinuity): it tends to 0 in probability.