The walk bridge invariance principle

Strict-prefix convergence and terminal-window smallness give full weak convergence on D[0,1] by the prefix-extension criterion.

theorem BGW.StableTrees.DiscreteBridge.tendsto_walkBridgeLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) : Filter.Tendsto (fun (k : ℕ) => walkBridgeLaw μ B (q k) ⋯) Filter.atTop (nhds (stableBridgeLaw θ))

Walk bridge invariance principle (K06 main theorem). Along an unbounded sequence of admissible sizes, the walk conditioned to end at -1 at time q k, scaled by B (q k), converges weakly in D[0,1] to the stable bridge stableBridgeLaw θ.