Occupation partition at weak ascending epochs

Finite weak epochs partition all integer times. The killed occupation at zero in each cycle is the restarted occupation at that cycle's attained height.

theorem BGW.StableTrees.DiscreteHeightApprox.epochsFinite_shiftSeq {ω : ℕ → ℕ} (hω : EpochsFinite ω) (m : ℕ) : EpochsFinite (DiscreteForest.shiftSeq m ω)

Weak-epoch finiteness is preserved by every deterministic sequence shift.

theorem BGW.StableTrees.DiscreteHeightApprox.tsum_eq_sum_weakCycles {ω : ℕ → ℕ} (hω : EpochsFinite ω) (f : ℕ → ENNReal) : ∑' (n : ℕ), f n = ∑' (i : ℕ), ∑ n ∈ Finset.Ico (weakEpoch ω i) (weakEpoch ω (i + 1)), f n

Nonnegative sums over time split into finite weak-epoch cycles.

theorem BGW.StableTrees.DiscreteHeightApprox.levelOccupation_epochRestart {ω : ℕ → ℕ} (hω : EpochsFinite ω) (i h : ℕ) : levelOccupation h (epochRestart i ω) = ↑{u ∈ Finset.Ico (weakEpoch ω i) (weakEpoch ω (i + 1)) | DiscreteForest.walk ω (weakEpoch ω i) - DiscreteForest.walk ω u = ↑h}.card

Restarting a cycle identifies its exact-level count with a finite interval count.

theorem BGW.StableTrees.DiscreteHeightApprox.killedOccupation_eq_cycle_rewards {ω : ℕ → ℕ} (hω : EpochsFinite ω) (m : ℕ) : ∑' (n : ℕ), (killedGapEvent m m n).indicator (fun (x : ℕ → ℕ) => 1) ω = ∑' (i : ℕ), ∑ h ∈ Finset.range m, {ξ : ℕ → ℕ | DiscreteForest.walk ξ (weakEpoch ξ i) = ↑h}.indicator (fun (ξ : ℕ → ℕ) => levelOccupation h (epochRestart i ξ)) ω

The killed occupation at zero splits into restarted occupations at epoch heights.