The step-path occupation mesh

Each integer index between the two endpoint floors is attained inside the real time window. Consequently its path infimum is a finite minimum of walk values.

theorem BGW.StableTrees.DiscreteHeightApprox.forestWalkPath_apply_eq_walk (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (ω : ℕ → ℕ) (u : ↑(Set.Icc 0 ↑T)) : (DiscreteForest.forestWalkPath B n T ω) u = ↑(DiscreteForest.walk ω ⌊↑n * ↑u⌋₊) / B n

A floor-step forest path evaluates to its integer walk value divided by the norming.

theorem BGW.StableTrees.DiscreteHeightApprox.exists_time_floor {n l : ℕ} (hn : 0 < n) {s t : NNReal} (hst : s ≤ t) (hl : ⌊↑n * ↑s⌋₊ ≤ l ∧ l ≤ ⌊↑n * ↑t⌋₊) : ∃ (u : NNReal), s ≤ u ∧ u ≤ t ∧ ⌊↑n * ↑u⌋₊ = l

Every index between the endpoint floors is attained inside that real time window.

theorem BGW.StableTrees.DiscreteHeightApprox.futureInf_forestWalkPath (B : ℕ → ℝ) {n : ℕ} (hn : 0 < n) (T : NNReal) (ω : ℕ → ℕ) {s t : NNReal} (hst : s ≤ t) (ht : t ≤ T) : futureInf (extendFinitePath T (DiscreteForest.forestWalkPath B n T ω)) t s = (Finset.Icc ⌊↑n * ↑s⌋₊ ⌊↑n * ↑t⌋₊).inf' ⋯ fun (l : ℕ) => ↑(DiscreteForest.walk ω l) / B n

A step-path future infimum is the finite minimum between the two endpoint floors.

theorem BGW.StableTrees.DiscreteHeightApprox.finiteGap_forestWalkPath_lt_iff (B : ℕ → ℝ) {n : ℕ} (hn : 0 < n) (hB : 0 < B n) (T : NNReal) (ω : ℕ → ℕ) {s t : NNReal} (hst : s ≤ t) (ht : t ≤ T) (ε : ℝ) : finiteGap T t (DiscreteForest.forestWalkPath B n T ω) ↑s < ε ↔ ∀ (l : ℕ), ⌊↑n * ↑s⌋₊ ≤ l → l ≤ ⌊↑n * ↑t⌋₊ → ↑(DiscreteForest.walk ω ⌊↑n * ↑s⌋₊) - ↑(DiscreteForest.walk ω l) < ε * B n

The step-path occupation test is exactly the discrete future-window test.