Two-limit control of centered cycle maxima

Centering the iid cycle counts gives independent square-integrable increments, with variances bounded by the uncentered first-cycle second moment. The number of cycles is of order n/B_n. The finite-cutoff maximal bound and the scale-uniform second moment therefore give an error tending to zero as the band shrinks.

theorem BGW.StableTrees.DiscreteHeightApprox.integral_clusterVisits_sq_eq_zero (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (a : ℝ) (i : ℕ) : ∫ (ω : ℕ → ℕ), ↑(clusterVisits ω a i) ^ 2 ∂↑(DiscreteForest.offspringSeqLaw μ) = ∫ (ω : ℕ → ℕ), ↑(clusterVisits ω a 0) ^ 2 ∂↑(DiscreteForest.offspringSeqLaw μ)

All cycles have the same second moment.

theorem BGW.StableTrees.DiscreteHeightApprox.measure_cluster_partialSum_maximal_le (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (m : ℕ) : ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | ∃ N ∈ Finset.range (m + 1), r < |∑ i ∈ Finset.range N, ↑(clusterVisits ω a i) - ↑N * ↑⌈a⌉₊|} ≤ ENNReal.ofReal ((4 * ↑(m + 1) * ∫ (ω : ℕ → ℕ), ↑(clusterVisits ω a 0) ^ 2 ∂↑(DiscreteForest.offspringSeqLaw μ)) / r ^ 2)

The centered cycle-sum maximum has a second-moment upper bound with one extra cycle.

theorem BGW.StableTrees.DiscreteHeightApprox.cluster_partialSum_maximal {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {x δ : ℝ} (hx : 0 < x) (hδ : 0 < δ) : Filter.Tendsto (fun (ε : ℝ) => Filter.limsup (fun (n : ℕ) => ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | ∃ N ∈ Finset.range (⌈x * ↑n / B n⌉₊ + 1), δ * (↑n * ε) < |∑ i ∈ Finset.range N, ↑(clusterVisits ω (ε * B n) i) - ↑N * ↑⌈ε * B n⌉₊|}) Filter.atTop) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Stopped error, uniform over the cutoff (Kolmogorov maximal inequality from the three suppliers above): over N ≤ x n/B_n cycles the centered cycle sums stay o(n ε) as n → ∞, then ε → 0.