Discrete forest walks and record counts

The walk is indexed before exploration of a vertex. Heights count weak minima among strictly preceding times, with both endpoints included in each tested interval.

noncomputable def BGW.StableTrees.DiscreteForest.offspringSeqLaw (μ : PMF ℕ) : MeasureTheory.ProbabilityMeasure (ℕ → ℕ)

The law of an iid sequence of offspring numbers with law μ, indexed from 0.

Equations

• BGW.StableTrees.DiscreteForest.offspringSeqLaw μ = ⟨MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ.toMeasure, ⋯⟩

def BGW.StableTrees.DiscreteForest.walk (ω : ℕ → ℕ) (k : ℕ) : ℤ

The walk W ω k = ∑_{i<k} (ω i - 1), with W ω 0 = 0.

Equations

• BGW.StableTrees.DiscreteForest.walk ω k = ∑ i ∈ Finset.range k, (↑(ω i) - 1)

def BGW.StableTrees.DiscreteForest.shiftSeq (m : ℕ) (ω : ℕ → ℕ) : ℕ → ℕ

The shifted offspring sequence i ↦ ω (m + i).

Equations

• BGW.StableTrees.DiscreteForest.shiftSeq m ω i = ω (m + i)

noncomputable def BGW.StableTrees.DiscreteForest.forestHeight (ω : ℕ → ℕ) (k : ℕ) : ℕ

The record-count height of the infinite forest coded by ω at time k: the number of weak running minima j < k of the walk seen from k, namely #{j < k | ∀ l ∈ [j,k], W_j ≤ W_l}.

Equations

• BGW.StableTrees.DiscreteForest.forestHeight ω k = {j ∈ Finset.range k | ∀ (l : ℕ), j ≤ l → l ≤ k → BGW.StableTrees.DiscreteForest.walk ω j ≤ BGW.StableTrees.DiscreteForest.walk ω l}.card

noncomputable def BGW.StableTrees.DiscreteForest.minHeight (ω : ℕ → ℕ) (m k : ℕ) : ℕ

The minimum of the heights H_m, ..., H_{m+k}.

Equations

• BGW.StableTrees.DiscreteForest.minHeight ω m k = (Finset.range (k + 1)).inf' ⋯ fun (i : ℕ) => BGW.StableTrees.DiscreteForest.forestHeight ω (m + i)

noncomputable def BGW.StableTrees.DiscreteForest.shiftedHeight (ω : ℕ → ℕ) (m k : ℕ) : ℤ

The height seen from time m: H_{m+k} - min_{m≤j≤m+k} H_j (an integer).

Equations

• BGW.StableTrees.DiscreteForest.shiftedHeight ω m k = ↑(BGW.StableTrees.DiscreteForest.forestHeight ω (m + k)) - ↑(BGW.StableTrees.DiscreteForest.minHeight ω m k)

theorem BGW.StableTrees.DiscreteForest.walk_shiftSeq (ω : ℕ → ℕ) (m i : ℕ) : walk (shiftSeq m ω) i = walk ω (m + i) - walk ω m

The walk of the shifted sequence is the increment of the walk after time m.

theorem BGW.StableTrees.DiscreteForest.measurable_shiftSeq (m : ℕ) : Measurable (shiftSeq m)

The shifted path process is a measurable function of the shifted sequence.

noncomputable def BGW.StableTrees.DiscreteForest.ladderTime (ω : ℕ → ℕ) (r : ℕ) : ℕ

Ladder times L r = inf {k | W_k = -r} (junk 0 if the set is empty).

Equations

• BGW.StableTrees.DiscreteForest.ladderTime ω r = sInf {k : ℕ | BGW.StableTrees.DiscreteForest.walk ω k = -↑r}

def BGW.StableTrees.DiscreteForest.LadderFinite (ω : ℕ → ℕ) : Prop

All ladder levels are reached.

Equations

• BGW.StableTrees.DiscreteForest.LadderFinite ω = ∀ (r : ℕ), ∃ (k : ℕ), BGW.StableTrees.DiscreteForest.walk ω k = -↑r

theorem BGW.StableTrees.DiscreteForest.ladderTime_zero (ω : ℕ → ℕ) : ladderTime ω 0 = 0

L 0 = 0.

theorem BGW.StableTrees.DiscreteForest.walk_ladderTime {ω : ℕ → ℕ} (hω : LadderFinite ω) (r : ℕ) : walk ω (ladderTime ω r) = -↑r

On LadderFinite, the walk at L r equals -r.

theorem BGW.StableTrees.DiscreteForest.walk_gt_of_lt_ladderTime {ω : ℕ → ℕ} (hω : LadderFinite ω) {r k : ℕ} (hk : k < ladderTime ω r) : -↑r < walk ω k

Before L r, the walk is strictly above -r.

theorem BGW.StableTrees.DiscreteForest.ladderTime_lt_succ {ω : ℕ → ℕ} (hω : LadderFinite ω) (r : ℕ) : ladderTime ω r < ladderTime ω (r + 1)

Ladder times are strictly increasing (skip-free descent).

theorem BGW.StableTrees.DiscreteForest.le_ladderTime {ω : ℕ → ℕ} (hω : LadderFinite ω) (r : ℕ) : r ≤ ladderTime ω r

The r-th ladder time is at least r.

theorem BGW.StableTrees.DiscreteForest.exists_ladderTime_le_lt {ω : ℕ → ℕ} (hω : LadderFinite ω) (k : ℕ) : ∃ (r : ℕ), ladderTime ω r ≤ k ∧ k < ladderTime ω (r + 1)

Block exhaustion: every time lies in exactly one block [L r, L (r+1)).