Stable scaling of the weak ladder renewal bound

A fixed positive Laplace parameter controls the moving natural ceiling. The normalized offspring PGF gap supplies the denominator asymptotic.

theorem BGW.StableTrees.DiscreteHeightApprox.tendsto_ceil_scale {B : ℕ → ℝ} (hB : Filter.Tendsto B Filter.atTop Filter.atTop) {ε : ℝ} (hε : 0 ≤ ε) : Filter.Tendsto (fun (n : ℕ) => ↑⌈ε * B n⌉₊ / B n) Filter.atTop (nhds ε)

Dividing a natural ceiling at a diverging scale removes the rounding error.

theorem BGW.StableTrees.DiscreteHeightApprox.tendsto_norming_one_sub_exp {B : ℕ → ℝ} (hB : Filter.Tendsto B Filter.atTop Filter.atTop) {lam : ℝ} (hlam : 0 < lam) : Filter.Tendsto (fun (n : ℕ) => B n * (1 - Real.exp (-lam / B n))) Filter.atTop (nhds lam)

The elementary exponential difference has its normalized first-order limit.

theorem BGW.StableTrees.DiscreteHeightApprox.limsup_scaled_weakLadderRenewal_le {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {ε : ℝ} (hε : 0 < ε) : Filter.limsup (fun (n : ℕ) => ENNReal.ofReal (B n / ↑n * (weakLadderRenewal μ ⌈ε * B n⌉₊).toReal)) Filter.atTop ≤ ENNReal.ofReal (Real.exp 1 * ε ^ (θ - 1))

The exponential renewal majorant has its stable-domain limit at every fixed band.