Tightness of the running maximum of the forest height

The first-upcrossing survival bound splits the event into survival among finitely many blocks and early passage beyond those blocks. Walk-maximum tightness controls the latter term, and the stable survival asymptotics control the former.

theorem BGW.StableTrees.HeightTightness.scaled_height_max_probability_le {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {n : ℕ} (hn : 1 ≤ n) (T δ : ℝ) (l : ℕ) : (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | δ < B n / ↑n * ↑((Finset.range (⌊↑n * T⌋₊ + 1)).sup fun (k : ℕ) => DiscreteForest.forestHeight ω k)} ≤ ↑l * Survival.survivalProb μ ⌊δ * ↑n / B n⌋₊ + (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | DiscreteForest.ladderTime ω l ≤ ⌊↑n * T⌋₊}

A scaled finite-height maximum is controlled by the first-upcrossing event.

theorem BGW.StableTrees.HeightTightness.forestHeight_sup_tight {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : ℝ} (hT : 0 < T) {ε : ℝ} (hε : 0 < ε) : ∃ (M : ℝ), Filter.limsup (fun (n : ℕ) => (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | M < B n / ↑n * ↑((Finset.range (⌊↑n * T⌋₊ + 1)).sup fun (k : ℕ) => DiscreteForest.forestHeight ω k)}) Filter.atTop ≤ ε

Running maximum of the normalized height is tight (sup H / n = O_P(1/B_n), used by K12/K13).