The terminal contour window under exact-size conditioning

Mirror invariance transfers the initial-window control supplied by height-prefix tightness.

theorem BGW.StableTrees.ExactContour.contourHeightError_ge (B : ℕ → ℝ) (n : ℕ) (a : NNReal) (τ : LocallyFinite.Tree) (s : ↑(Set.Icc 0 ↑a)) : |(treeContourPath B n a τ) s - (TailPair.treeHeightPath B n a τ) s| ≤ contourHeightError B n a τ

Every pointwise contour/height difference is bounded by the uniform prefix error.

theorem BGW.StableTrees.ExactContour.exactContour_terminal_small {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) : ∃ δ > 0, δ ≤ 1 / 2 ∧ ∀ᶠ (k : ℕ) in Filter.atTop, (↑(DiscreteForest.exactTreeLaw μ (q k))).real {τ : LocallyFinite.Tree | ∃ (t : ↑(Set.Icc 0 1)), 1 - δ ≤ ↑t ∧ ε < B (q k) / ↑(q k) * treeContourLin τ (2 * ↑(q k) * ↑t)} ≤ η

For any fixed probability tolerance, a sufficiently small terminal contour window is uniformly small for all sufficiently large admissible sizes.

theorem BGW.StableTrees.ExactContour.tendsto_exactContour_terminalWindow {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (δ : ℝ) => Filter.limsup (fun (k : ℕ) => (↑(DiscreteForest.exactTreeLaw μ (q k))).real {τ : LocallyFinite.Tree | ∃ (t : ↑(Set.Icc 0 1)), 1 - δ ≤ ↑t ∧ ε < B (q k) / ↑(q k) * treeContourLin τ (2 * ↑(q k) * ↑t)}) Filter.atTop) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Terminal contour window (mirror symmetry and H^exc(0) = 0): the probability that the normalized contour exceeds ε on [1 - δ, 1] is asymptotically small as δ ↓ 0.