Stopping times and deterministic restart of weak ascending cycles

The first time at which the record count reaches i is a genuine stopping time with value infinity if the record does not exist; on EpochsFinite it agrees with the natural epoch. Shifting to an epoch sends that cycle to the first cycle. Prefix agreement through a completed epoch determines every preceding cycle, even if later epochs fail.

noncomputable def BGW.StableTrees.DiscreteHeightApprox.weakEpochStop (ω : ℕ → ℕ) (i : ℕ) : ℕ∞

The genuine extended stopping time of the ith positive-time weak record.

Equations

• BGW.StableTrees.DiscreteHeightApprox.weakEpochStop ω i = ⨅ (u : { u : ℕ // i ≤ BGW.StableTrees.DiscreteHeightApprox.weakLadderCount ω u }), ↑↑u

theorem BGW.StableTrees.DiscreteHeightApprox.isSeqStoppingTime_weakEpochStop (i : ℕ) : DiscreteForest.IsSeqStoppingTime fun (ω : ℕ → ℕ) => weakEpochStop ω i

The extended epoch is a stopping time for the offspring coordinate filtration.

theorem BGW.StableTrees.DiscreteHeightApprox.weakEpochStop_eq_epoch {ω : ℕ → ℕ} (hω : EpochsFinite ω) (i : ℕ) : weakEpochStop ω i = ↑(weakEpoch ω i)

The extended stopping time agrees with the natural epoch on finite paths.

theorem BGW.StableTrees.DiscreteHeightApprox.ae_weakEpochStop_ne_top (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (i : ℕ) : ∀ᵐ (ω : ℕ → ℕ) ∂↑(DiscreteForest.offspringSeqLaw μ), weakEpochStop ω i ≠ ⊤

Every genuine record stopping time is finite almost surely.

theorem BGW.StableTrees.DiscreteHeightApprox.clusterVisits_shift_zero {ω : ℕ → ℕ} (hω : EpochsFinite ω) (a : ℝ) (i : ℕ) : clusterVisits ω a i = clusterVisits (DiscreteForest.shiftSeq (weakEpoch ω i) ω) a 0

The cycle occupation after shifting to its initial epoch is the first-cycle occupation.

theorem BGW.StableTrees.DiscreteHeightApprox.clusterVisits_eq_of_agree {ω ξ : ℕ → ℕ} (hω : EpochsFinite ω) {n i j : ℕ} (he : ∀ k < n, ω k = ξ k) (hi : weakEpoch ω i ≤ n) (hj : j < i) (a : ℝ) : clusterVisits ω a j = clusterVisits ξ a j

Agreement through a completed epoch determines each preceding cycle occupation.

theorem BGW.StableTrees.DiscreteHeightApprox.weakEpoch_shift_duration {ω : ℕ → ℕ} (hω : EpochsFinite ω) (i : ℕ) : weakEpoch (DiscreteForest.shiftSeq (weakEpoch ω i) ω) 1 = weakEpoch ω (i + 1) - weakEpoch ω i

Shifting to a finite weak epoch sends the next epoch to the cycle duration.