Exact-prefix forest weights

Compactness combines the periodic local limit, the inclusive tail limit and the admissible tree tail-to-mass ratio. The two lattice factors cancel.

Reference: J.-F. Le Gall, Random trees and applications, Probab. Surveys 2 (2005), Section 1.

theorem BGW.StableTrees.exactPrefixWeight_uniform {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {a ε M η : ℝ} (ha : a ∈ Set.Ioo 0 1) (hε : 0 < ε) (hεM : ε ≤ M) (hη : 0 < η) : ∀ᶠ (n : ℕ) in Filter.atTop, Admissible μ n → ∀ (j : ℕ), ε ≤ ↑j / B n → ↑j / B n ≤ M → ↑(Scalar.latticeSpan μ) ∣ ↑n - ↑⌊a * ↑n⌋₊ - ↑j → |exactPrefixWeight μ n ⌊a * ↑n⌋₊ j - gammaA θ a (↑j / B n)| ≤ η

Exact-prefix RN weights, uniform on accessible prefixes (d ∣ (n-m) - j, where m = ⌊a n⌋, j = W_m + 1, ε ≤ j/B_n ≤ M): R_n(m,j) - gammaA θ a (j/B_n) → 0 uniformly, along admissible n.