Discrete occupation and reversal

Finite-time reversal identifies the forest record count and the occupation count with weak ascending records and reflected bands, with both endpoints retained. The height scaling is B n / n, with constant exactly one.

noncomputable def BGW.StableTrees.DiscreteHeightApprox.discreteCount (ω : ℕ → ℕ) (k : ℕ) (a : ℝ) : ℕ

The discrete occupation count at level a: #{j < k | ∀ l ∈ [j,k], W_j - W_l < a}, i.e. W_j - min_{[j,k]} W < a.

Equations

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

noncomputable def BGW.StableTrees.DiscreteHeightApprox.discreteOccupation (B : ℕ → ℝ) (n : ℕ) (ε : ℝ) (ω : ℕ → ℕ) (t : NNReal) : ℝ

The discrete ε-occupation (n ε)⁻¹ #{j < ⌊n t⌋ | W_j - min_{[j,⌊nt⌋]} W < ε B_n}: mesh 1/n, level ε B_n; the discrete analogue of heightApprox ε.

Equations

• BGW.StableTrees.DiscreteHeightApprox.discreteOccupation B n ε ω t = 1 / (↑n * ε) * ↑(BGW.StableTrees.DiscreteHeightApprox.discreteCount ω ⌊↑n * ↑t⌋₊ (ε * B n))

noncomputable def BGW.StableTrees.DiscreteHeightApprox.scaledHeight (B : ℕ → ℝ) (n : ℕ) (ω : ℕ → ℕ) (t : NNReal) : ℝ

The normalized discrete height (B_n / n) · H_{⌊n t⌋} (the constant is 1, see the module docstring; at θ = 2 it converges to X_t - I_t).

Equations

• BGW.StableTrees.DiscreteHeightApprox.scaledHeight B n ω t = B n / ↑n * ↑(BGW.StableTrees.DiscreteForest.forestHeight ω ⌊↑n * ↑t⌋₊)

def BGW.StableTrees.DiscreteHeightApprox.revSeq (k : ℕ) (ω : ℕ → ℕ) : ℕ → ℕ

The sequence reversed at k: i ↦ ω (k-1-i) for i < k, unchanged afterwards.

Equations

• BGW.StableTrees.DiscreteHeightApprox.revSeq k ω i = if i < k then ω (k - 1 - i) else ω i

noncomputable def BGW.StableTrees.DiscreteHeightApprox.reflGap (ω : ℕ → ℕ) (u : ℕ) : ℤ

The reflected gap M_u - W_u of the walk, M_u = max_{v ≤ u} W_v (an integer, ≥ 0).

Equations

• BGW.StableTrees.DiscreteHeightApprox.reflGap ω u = (Finset.range (u + 1)).sup' ⋯ (BGW.StableTrees.DiscreteForest.walk ω) - BGW.StableTrees.DiscreteForest.walk ω u

noncomputable def BGW.StableTrees.DiscreteHeightApprox.weakLadderCount (ω : ℕ → ℕ) (k : ℕ) : ℕ

The number of weak ascending ladder epochs u ∈ [1,k] (W_u ≥ W_v for all v ≤ u).

Equations

• BGW.StableTrees.DiscreteHeightApprox.weakLadderCount ω k = {u ∈ Finset.Icc 1 k | BGW.StableTrees.DiscreteHeightApprox.reflGap ω u = 0}.card

noncomputable def BGW.StableTrees.DiscreteHeightApprox.bandCount (ω : ℕ → ℕ) (k : ℕ) (a : ℝ) : ℕ

The number of times u ∈ [1,k] with reflected gap < a.

Equations

• BGW.StableTrees.DiscreteHeightApprox.bandCount ω k a = {u ∈ Finset.Icc 1 k | ↑(BGW.StableTrees.DiscreteHeightApprox.reflGap ω u) < a}.card

theorem BGW.StableTrees.DiscreteHeightApprox.walk_succ_eq (ω : ℕ → ℕ) (n : ℕ) : DiscreteForest.walk ω (n + 1) = DiscreteForest.walk ω n + ↑(ω n) - 1

One step of the walk: W_{n+1} = W_n + ω_n - 1.

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

Agreement of the first n offspring coordinates determines the walk through time n.

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_scaledHeight (B : ℕ → ℝ) (n : ℕ) (t : NNReal) : Measurable fun (ω : ℕ → ℕ) => scaledHeight B n ω t

Measurability of the discrete height and occupation.

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_discreteCount (k : ℕ) (a : ℝ) : Measurable fun (ω : ℕ → ℕ) => discreteCount ω k a

Each finite discrete occupation count is measurable.

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_discreteOccupation (B : ℕ → ℝ) (n : ℕ) (ε : ℝ) (t : NNReal) : Measurable fun (ω : ℕ → ℕ) => discreteOccupation B n ε ω t

Every fixed-time discrete occupation is measurable.