Measurability of weak ascending cycles

The totalized natural epochs and finite cycle occupations are measurable on all sequences. Prefix agreement determines every walk coordinate in the prefix.

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_weakEpoch (i : ℕ) : Measurable fun (ω : ℕ → ℕ) => weakEpoch ω i

Every totalized natural weak epoch is measurable.

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_clusterVisits (a : ℝ) (i : ℕ) : Measurable fun (ω : ℕ → ℕ) => clusterVisits ω a i

Every finite cycle occupation is measurable, including its totalized values.

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_weakLadderCount (k : ℕ) : Measurable fun (ω : ℕ → ℕ) => weakLadderCount ω k

Every finite weak ascending record count is measurable.

theorem BGW.StableTrees.DiscreteHeightApprox.weakLadderCount_eq_of_agree {ω ξ : ℕ → ℕ} {n : ℕ} (he : ∀ i < n, ω i = ξ i) {u : ℕ} (hu : u ≤ n) : weakLadderCount ω u = weakLadderCount ξ u

Prefix agreement determines every weak record count within the prefix.