The weak ladder-height Laplace scale

At parameter 1/B_n, the first-height transform has defect asymptotic to B_n/n. This gives an exponential tail for the number of weak epochs below a bounded height.

theorem BGW.StableTrees.DiscreteHeightApprox.tendsto_scaled_ladderPGF_defect {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) : Filter.Tendsto (fun (n : ℕ) => ↑n / B n * (1 - (weakLadderPGF μ (ENNReal.ofReal (Real.exp (-1 / B n)))).toReal)) Filter.atTop (nhds 1)

The weak ladder transform has its critical stable normalization, with constant one.

theorem BGW.StableTrees.DiscreteHeightApprox.measure_epochHeight_le (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (N : ℕ) {b : ℝ} (hb : 0 < b) (K : ℝ) : ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | ↑(weakEpochHeight ω N) ≤ K * b} ≤ ENNReal.ofReal (Real.exp K) * weakLadderPGF μ (ENNReal.ofReal (Real.exp (-1 / b))) ^ N

Exponential Markov bounds the mass of attained epoch heights below a fixed real level.

theorem BGW.StableTrees.DiscreteHeightApprox.eventual_epochHeight_bound {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {x : ℝ} (hx : 0 < x) (K : ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | ↑(weakEpochHeight ω ⌈x * ↑n / B n⌉₊) ≤ K * B n} ≤ ENNReal.ofReal (Real.exp (K - x / 2))

At x*n/B_n weak epochs, a bounded attained height has an exponentially small tail in x.