Reversal of the discrete forest walk

Reversal retains weak records, and sends the half-open forest interval to the positive integer times through the endpoint. It preserves the iid sequence law.

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_revSeq (k : ℕ) : Measurable (revSeq k)

Reversal of a finite prefix is measurable.

theorem BGW.StableTrees.DiscreteHeightApprox.map_revSeq_offspringSeqLaw (μ : PMF ℕ) (k : ℕ) : MeasureTheory.Measure.map (revSeq k) ↑(DiscreteForest.offspringSeqLaw μ) = ↑(DiscreteForest.offspringSeqLaw μ)

Exchangeability: reversing the first k coordinates preserves the iid law.

theorem BGW.StableTrees.DiscreteHeightApprox.walk_revSeq (ω : ℕ → ℕ) {k u : ℕ} (hu : u ≤ k) : DiscreteForest.walk (revSeq k ω) u = DiscreteForest.walk ω k - DiscreteForest.walk ω (k - u)

walk (revSeq k ω) u = W_k - W_{k-u} for u ≤ k.

theorem BGW.StableTrees.DiscreteHeightApprox.reflGap_nonneg (ω : ℕ → ℕ) (u : ℕ) : 0 ≤ reflGap ω u

The reflected gap is nonnegative.

theorem BGW.StableTrees.DiscreteHeightApprox.reflGap_zero_iff_record (ω : ℕ → ℕ) (u : ℕ) : reflGap ω u = 0 ↔ ∀ v ≤ u, DiscreteForest.walk ω v ≤ DiscreteForest.walk ω u

A zero gap is precisely a weak ascending record.

theorem BGW.StableTrees.DiscreteHeightApprox.reflGap_lt_iff (ω : ℕ → ℕ) (u : ℕ) (a : ℝ) : ↑(reflGap ω u) < a ↔ ∀ v ≤ u, ↑(DiscreteForest.walk ω v) - ↑(DiscreteForest.walk ω u) < a

A strict band condition can be tested at every preceding walk value.

theorem BGW.StableTrees.DiscreteHeightApprox.forestHeight_eq_weakLadderCount (ω : ℕ → ℕ) (k : ℕ) : DiscreteForest.forestHeight ω k = weakLadderCount (revSeq k ω) k

(Deterministic) the forest height is the weak ladder count of the reversed sequence.

theorem BGW.StableTrees.DiscreteHeightApprox.discreteCount_eq_bandCount (ω : ℕ → ℕ) (k : ℕ) (a : ℝ) : discreteCount ω k a = bandCount (revSeq k ω) k a

(Deterministic) the discrete occupation count is the band count of the reversed sequence.