Stable-scale comparison for the offspring generating function

This file finishes the expansion below index two and in the infinite-variance Gaussian case.

theorem BGW.StableTrees.Survival.tendsto_realGF_expansion {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {lam : ℝ} (hlam : 0 < lam) : Filter.Tendsto (fun (n : ℕ) => ↑n * (realGF μ (1 - lam / B n) - (1 - lam / B n))) Filter.atTop (nhds (lam ^ θ))

n (g(1 - λ/B_n) - (1 - λ/B_n)) → λ^θ for every λ > 0.