The offspring generating-function expansion at the stable scale #
The stable Laplace asymptotic is transferred from the canonical norming to any attracting
norming, and then from the exponential generating function to its real argument 1 - λ / Bₙ.
theorem
BGW.StableTrees.Survival.centeredLaplace_realGF_difference_bound
(μ : PMF ℕ)
(hc : IsCritical μ)
{u : ℝ}
(hu0 : 0 ≤ u)
(hu1 : u ≤ 1)
:
An O(u²) comparison between the exponential and real generating functions.
theorem
BGW.StableTrees.Survival.tendsto_centeredLaplace_stableDomain
{μ : PMF ℕ}
{θ : ℝ}
{B : ℕ → ℝ}
(h : StableDomain μ θ B)
{lam : ℝ}
(hlam : 0 < lam)
:
Filter.Tendsto (fun (n : ℕ) => ↑n * (Attraction.LaplaceExpansion.centeredLaplace (stepLaw μ) (lam / B n) - 1))
Filter.atTop (nhds (lam ^ θ))
The centered step Laplace expansion along an arbitrary stable norming.
theorem
BGW.StableTrees.Survival.tendsto_realGF_difference_zero_finiteVariance
{μ : PMF ℕ}
{B : ℕ → ℝ}
(h : StableDomain μ 2 B)
(hsq : MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) (stepLaw μ))
{lam : ℝ}
(hlam : 0 < lam)
:
In finite variance, the real and exponential generating-function expansions have the same second-order term.