Vanishing contour error on exact-size prefixes #
Tightness of a larger height prefix and the local deterministic estimate give convergence in probability under the exact-size conditioned laws themselves.
theorem
BGW.StableTrees.ExactContour.tendsto_contourHeightError_prefix
{μ : PMF ℕ}
{θ : ℝ}
{B : ℕ → ℝ}
(h : StableDomain μ θ B)
{q : ℕ → ℕ}
(hqtop : Filter.Tendsto q Filter.atTop Filter.atTop)
(hq : ∀ (k : ℕ), Admissible μ (q k))
(a : NNReal)
(ha : a ∈ Set.Ioo 0 1)
{ε : ℝ}
(hε : 0 < ε)
:
Filter.Tendsto
(fun (k : ℕ) =>
(↑(DiscreteForest.exactTreeLaw μ (q k))).real {τ : LocallyFinite.Tree | ε < contourHeightError B (q k) a τ})
Filter.atTop (nhds 0)
Prefix contour error (finite-tree K12a bracketing with K15 on a larger prefix a' < 1):
on [0,a], a < 1, the normalized contour at 2nt is uniformly close to the normalized height
at nt, in probability under the exact-size laws.