Weak ascending epochs

Deterministic epoch characterizations assume EpochsFinite, which eliminates the empty-set value of sInf. Weak epochs retain ties at the running maximum.

noncomputable def BGW.StableTrees.DiscreteHeightApprox.nextEpoch (ω : ℕ → ℕ) (s : ℕ) : ℕ

The next weak ascending epoch after the epoch s (junk 0 if none).

Equations

• BGW.StableTrees.DiscreteHeightApprox.nextEpoch ω s = sInf {u : ℕ | s < u ∧ BGW.StableTrees.DiscreteForest.walk ω s ≤ BGW.StableTrees.DiscreteForest.walk ω u}

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

The weak epochs τ_0 = 0 < τ_1 < ...: iterates of nextEpoch from 0.

Equations

• BGW.StableTrees.DiscreteHeightApprox.weakEpoch ω i = (BGW.StableTrees.DiscreteHeightApprox.nextEpoch ω)^[i] 0

def BGW.StableTrees.DiscreteHeightApprox.EpochsFinite (ω : ℕ → ℕ) : Prop

All epochs exist (the walk returns to each running-maximum level or above).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGW.StableTrees.DiscreteHeightApprox.clusterVisits (ω : ℕ → ℕ) (a : ℝ) (i : ℕ) : ℕ

The number of times u in the cycle [τ_i, τ_{i+1}) with gap < a below the epoch value: the cycle visit count V_i(a).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGW.StableTrees.DiscreteHeightApprox.weakEpoch_zero (ω : ℕ → ℕ) : weakEpoch ω 0 = 0

The zeroth weak epoch is time zero.

theorem BGW.StableTrees.DiscreteHeightApprox.weakEpoch_succ (ω : ℕ → ℕ) (i : ℕ) : weakEpoch ω (i + 1) = nextEpoch ω (weakEpoch ω i)

Consecutive epochs are related by the next-epoch map.

theorem BGW.StableTrees.DiscreteHeightApprox.weakEpoch_lt_succ {ω : ℕ → ℕ} (hω : EpochsFinite ω) (i : ℕ) : weakEpoch ω i < weakEpoch ω (i + 1)

The epochs are strictly increasing when finite.

theorem BGW.StableTrees.DiscreteHeightApprox.strictMono_weakEpoch {ω : ℕ → ℕ} (hω : EpochsFinite ω) : StrictMono (weakEpoch ω)

Finiteness makes the epoch sequence strictly increasing.

theorem BGW.StableTrees.DiscreteHeightApprox.reflGap_weakEpoch {ω : ℕ → ℕ} (hω : EpochsFinite ω) (i : ℕ) : reflGap ω (weakEpoch ω i) = 0

Every weak epoch attains the running maximum, including time zero.

theorem BGW.StableTrees.DiscreteHeightApprox.exists_weakEpoch_le_lt {ω : ℕ → ℕ} (hω : EpochsFinite ω) (k : ℕ) : ∃ (i : ℕ), weakEpoch ω i ≤ k ∧ k < weakEpoch ω (i + 1)

Every integer time belongs to some finite weak-epoch cycle.

theorem BGW.StableTrees.DiscreteHeightApprox.reflGap_eq_zero_iff {ω : ℕ → ℕ} (hω : EpochsFinite ω) {u : ℕ} : reflGap ω u = 0 ∧ 0 < u ↔ ∃ (i : ℕ), 0 < i ∧ weakEpoch ω i = u

At an epoch the running maximum is attained: reflGap ω (τ_i) = 0 and the epochs are exactly the zeros of reflGap (ties are weak records).

theorem BGW.StableTrees.DiscreteHeightApprox.weakEpoch_bracket {ω : ℕ → ℕ} (hω : EpochsFinite ω) (k : ℕ) : weakEpoch ω (weakLadderCount ω k) ≤ k ∧ k < weakEpoch ω (weakLadderCount ω k + 1)

The number of epochs u ∈ [1,k] is the last cycle index: τ_H ≤ k < τ_{H+1}.

theorem BGW.StableTrees.DiscreteHeightApprox.reflGap_in_cycle {ω : ℕ → ℕ} (hω : EpochsFinite ω) {i u : ℕ} (hi : weakEpoch ω i ≤ u) (hi' : u < weakEpoch ω (i + 1)) : reflGap ω u = DiscreteForest.walk ω (weakEpoch ω i) - DiscreteForest.walk ω u

Inside a cycle the running maximum remains equal to the initial epoch value.

theorem BGW.StableTrees.DiscreteHeightApprox.bandCount_sandwich {ω : ℕ → ℕ} (hω : EpochsFinite ω) (k : ℕ) {a : ℝ} (ha : 0 < a) : ↑(∑ i ∈ Finset.range (weakLadderCount ω k), clusterVisits ω a i) - 1 ≤ ↑(bandCount ω k a) ∧ bandCount ω k a ≤ ∑ i ∈ Finset.range (weakLadderCount ω k + 1), clusterVisits ω a i

(Deterministic stopped decomposition) With H = weakLadderCount ω k and a > 0: Σ_{i<H} V_i(a) - 1 ≤ bandCount ω k a ≤ Σ_{i ≤ H} V_i(a).