Contour comparison on compact sets of height prefixes #
A larger height prefix controls the contour on a smaller prefix by deterministic bracketing.
theorem
BGW.StableTrees.ExactContour.eventually_contourHeightError_le_of_compact
{μ : PMF ℕ}
{θ : ℝ}
{B : ℕ → ℝ}
(h : StableDomain μ θ B)
{a a' : NNReal}
(haa' : a < a')
(ha' : a' < 1)
(K : Set C(↑(Set.Icc 0 ↑a'), ℝ))
(hK : IsCompact K)
{ε : ℝ}
(hε : 0 < ε)
:
∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : PlaneTree),
t.size = n → TailPair.treeHeightPath B n a' t.toLocallyFinite ∈ K → contourHeightError B n a t.toLocallyFinite ≤ ε
On a compact set of larger height prefixes, the contour/height error vanishes uniformly.