An exponential upper bound for weak ladder renewal

A level cutoff is dominated by an exponential weight. The product formula for attained-height transforms reduces the renewal series to a geometric series.

theorem BGW.StableTrees.DiscreteHeightApprox.weakLadderRenewal_le_exp (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (m : ℕ) {u : ℝ} (hu : 0 ≤ u) : weakLadderRenewal μ m ≤ ENNReal.ofReal (Real.exp (u * ↑m)) * (1 - weakLadderPGF μ (ENNReal.ofReal (Real.exp (-u))))⁻¹

A free exponential parameter bounds renewal without changing a moving level to a fixed one.

theorem BGW.StableTrees.DiscreteHeightApprox.weakLadderRenewal_toReal_le_exp (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (m : ℕ) {u : ℝ} (hu : 0 < u) : (weakLadderRenewal μ m).toReal ≤ Real.exp (u * ↑m) * (1 - Real.exp (-u)) / (offspringPGFReal μ (Real.exp (-u)) - Real.exp (-u))

Real renewal bound with an arbitrary positive exponential parameter.