Stopped band-count errors

The sandwich uses partial sums at both H and H+1. Doubling the cutoff reserves the extra cycle; the ceiling contribution is negligible at each fixed positive band.

theorem BGW.StableTrees.DiscreteHeightApprox.bandCount_error_le {ω : ℕ → ℕ} (hω : EpochsFinite ω) (k : ℕ) {a r : ℝ} (ha : 0 < a) (hlo : |∑ i ∈ Finset.range (weakLadderCount ω k), ↑(clusterVisits ω a i) - ↑(weakLadderCount ω k) * ↑⌈a⌉₊| ≤ r) (hhi : |∑ i ∈ Finset.range (weakLadderCount ω k + 1), ↑(clusterVisits ω a i) - ↑(weakLadderCount ω k + 1) * ↑⌈a⌉₊| ≤ r) : |↑(bandCount ω k a) - ↑⌈a⌉₊ * ↑(weakLadderCount ω k)| ≤ r + ↑⌈a⌉₊ + 1

A sandwich between the two adjacent cycle sums transfers a uniform centered-sum bound.

theorem BGW.StableTrees.DiscreteHeightApprox.stopped_bandCount_error {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (t : NNReal) {x δ : ℝ} (hx : 0 < x) (hδ : 0 < δ) : Filter.Tendsto (fun (ε : ℝ) => Filter.limsup (fun (n : ℕ) => ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | ↑(weakLadderCount ω ⌊↑n * ↑t⌋₊) ≤ x * ↑n / B n ∧ δ * (↑n * ε) < |↑(bandCount ω ⌊↑n * ↑t⌋₊ (ε * B n)) - ↑⌈ε * B n⌉₊ * ↑(weakLadderCount ω ⌊↑n * ↑t⌋₊)|}) Filter.atTop) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Stopped renewal error for the band count (cutoff event H_k ≤ x n/B_n, k = ⌊nt⌋): bandCount ω k (ε B_n) ≈ ⌈ε B_n⌉ H_k up to δ n ε, two limits.