Weak convergence of walk first-passage times

The functional central limit theorem is mapped through the J1-continuous running infimum. Moving levels are handled by CDF convergence and atom-freeness. A real quantile coupling then converts the CDF limit into convergence of all bounded continuous integrals (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII; P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Section 13).

theorem BGW.StableTrees.tendsto_walkPassageLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {x : NNReal} (hx : 0 < x) {ℓ : ℕ → ℕ} (hℓ : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ ℓ n) (hscale : Filter.Tendsto (fun (n : ℕ) => ↑(ℓ n) / B n) Filter.atTop (nhds ↑x)) (f : BoundedContinuousFunction ℝ ℝ) : Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ), f t ∂walkPassageLaw μ (ℓ n) n) Filter.atTop (nhds (∫ (t : ℝ), f t ∂passageLaw θ x))

Walk first passage converges to the stable passage law. For a StableDomain μ θ B witness, integers ℓ n ≥ 1 eventually, and ℓ n / B n → x > 0: walkHitTime (ℓ n) / n ⟹ T_x in law. Stated for bounded continuous test functions on ℝ (all measures involved are probability measures).