Mean occupation of a weak ascending cycle

Integer gaps strictly below a are exactly the nonnegative integers below its natural ceiling. The exact level mean and stopped restart give every cycle the mean ⌈a⌉₊, with no extra normalization constant.

theorem BGW.StableTrees.DiscreteHeightApprox.clusterVisits_zero_eq_sum_levels {ω : ℕ → ℕ} (hω : EpochsFinite ω) (a : ℝ) : clusterVisits ω a 0 = ∑ y ∈ Finset.range ⌈a⌉₊, {u ∈ Finset.Ico 0 (weakEpoch ω 1) | reflGap ω u = ↑y}.card

The first-cycle band count is the sum of its integer-level counts.

theorem BGW.StableTrees.DiscreteHeightApprox.integrable_clusterLevel (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (y : ℕ) : MeasureTheory.Integrable (fun (ω : ℕ → ℕ) => ↑{u ∈ Finset.Ico 0 (weakEpoch ω 1) | reflGap ω u = ↑y}.card) ↑(DiscreteForest.offspringSeqLaw μ)

Exact-level first-cycle counts are integrable; their integral is the nonzero value one.

theorem BGW.StableTrees.DiscreteHeightApprox.clusterVisits_mean (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {a : ℝ} (ha : 0 < a) (i : ℕ) : ∫ (ω : ℕ → ℕ), ↑(clusterVisits ω a i) ∂↑(DiscreteForest.offspringSeqLaw μ) = ↑⌈a⌉₊

Cycle mean: E V_i(a) = ⌈a⌉₊ for a > 0.