Compact uniform local limits for forest masses #
Kemperman's identity and the lattice local limit theorem give the sequential limit, including levels tending to zero. Compactness then gives the uniform assertion.
Reference: J.-F. Le Gall, Random trees and applications, Probab. Surveys 2 (2005), Section 1.
theorem
BGW.StableTrees.forestMass_local_seq
{μ : PMF ℕ}
{θ : ℝ}
{B : ℕ → ℝ}
(h : StableDomain μ θ B)
{x κ : ℝ}
(hκ : 0 < κ)
{ℓ q k : ℕ → ℕ}
(hscale : Filter.Tendsto (fun (j : ℕ) => ↑(ℓ j) / B (q j)) Filter.atTop (nhds x))
(hq : Filter.Tendsto q Filter.atTop Filter.atTop)
(hk : Filter.Tendsto (fun (j : ℕ) => ↑(k j) / ↑(q j)) Filter.atTop (nhds κ))
(hdiv : ∀ (j : ℕ), ↑(Scalar.latticeSpan μ) ∣ ↑(k j) - ↑(ℓ j))
:
Filter.Tendsto
(fun (j : ℕ) =>
↑(q j) * forestMass μ (ℓ j) (k j) - ↑(Scalar.latticeSpan μ) * qKernel θ (↑(k j) / ↑(q j)) (↑(ℓ j) / B (q j)))
Filter.atTop (nhds 0)
Sequential periodic local limit, allowing the rescaled forest level to tend to zero.
theorem
BGW.StableTrees.forestLocalLimit_uniform
{μ : PMF ℕ}
{θ : ℝ}
{B : ℕ → ℝ}
(h : StableDomain μ θ B)
{a b M : ℝ}
(ha : 0 < a)
(hab : a ≤ b)
(hM : 0 ≤ M)
{η : ℝ}
(hη : 0 < η)
:
Forest local limit, compact-uniform, periodic. With d = latticeSpan μ, uniformly for
r/n ∈ [a,b], j/B_n ∈ [0,M] and ONLY d ∣ r - j:
n f_j(r) - d q_{r/n}(j/B_n) → 0 (absolute error; includes j = 0, where both vanish).