Inclusive forest tails and passage-law convergence

The inclusive forest tail is the tail of the integer first passage time. Weak convergence of the passage laws supplies tail convergence at positive levels.

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

theorem BGW.StableTrees.forestTail_eq_walkPassage_tail {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {ℓ r n : ℕ} (hℓ : 1 ≤ ℓ) (hr : 1 ≤ r) (hn : 1 ≤ n) : forestTail μ ℓ r = (walkPassageLaw μ ℓ n).real (Set.Ioi (↑(r - 1) / ↑n))

An inclusive forest tail is the passage-time tail above the preceding integer.

theorem BGW.StableTrees.forestTail_limit_seq {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q ℓ r : ℕ → ℕ} (hq : StrictMono q) {x κ : ℝ} (hx : 0 < x) (hκ : 0 < κ) (hscale : Filter.Tendsto (fun (k : ℕ) => ↑(ℓ k) / B (q k)) Filter.atTop (nhds x)) (hratio : Filter.Tendsto (fun (k : ℕ) => ↑(r k) / ↑(q k)) Filter.atTop (nhds κ)) : Filter.Tendsto (fun (k : ℕ) => forestTail μ (ℓ k) (r k)) Filter.atTop (nhds (sizeTailKernel θ κ x))

Tail convergence along a strictly increasing time sequence and a convergent level sequence.

theorem BGW.StableTrees.forestTailLimit_uniform {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {a b ε M : ℝ} (ha : 0 < a) (hab : a ≤ b) (hε : 0 < ε) (hεM : ε ≤ M) {η : ℝ} (hη : 0 < η) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (r j : ℕ), a * ↑n ≤ ↑r → ↑r ≤ b * ↑n → ε ≤ ↑j / B n → ↑j / B n ≤ M → |forestTail μ j r - sizeTailKernel θ (↑r / ↑n) (↑j / B n)| ≤ η

Forest tail limit, compact-uniform, NO lattice condition. Uniformly for r/n ∈ [a,b], j/B_n ∈ [ε,M]: G_j(r) - G_{r/n}(j/B_n) → 0 (G = sizeTailKernel θ).