A sharp finite-band second moment

The zero level contributes exactly one. Cauchy--Schwarz on the positive levels, and the diagonal-corrected Green estimate, give the finite-band bound.

theorem BGW.StableTrees.DiscreteHeightApprox.integral_clusterVisits_sq_le_renewal (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {a : ℝ} (ha : 0 < a) : ∫ (ω : ℕ → ℕ), ↑(clusterVisits ω a 0) ^ 2 ∂↑(DiscreteForest.offspringSeqLaw μ) ≤ ↑⌈a⌉₊ + 2 * ↑(⌈a⌉₊ - 1) ^ 2 * (weakLadderRenewal μ ⌈a⌉₊).toReal

A finite band has second moment at most its mean plus the squared positive-level count times twice the weak ladder renewal function.