Limits of discrete ladder blocks give running-infimum plateaus

The change in the prefix infimum across one skip-free block is precisely one downward mesh.

theorem BGW.StableTrees.runningInf_eq_of_tendsto_ladderBlocks {M : NNReal} {N : ℕ → ℕ} (hN : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < N n) {B : ℕ → ℝ} (hB : Filter.Tendsto B Filter.atTop Filter.atTop) (ω : ℕ → ℕ → ℝ) (hω : ∀ (n i : ℕ), IsSkipFreeIncrement (ω n i)) {f : Skorokhod.DLoc} (hI : Continuous (runningInfLoc f)) (hu : Filter.Tendsto (fun (n : ℕ) => Skorokhod.realStepPath (↑M) (N n) (B n) (ω n)) Filter.atTop (nhds (Skorokhod.DLoc.restrict M f))) (r : ℕ → ℕ) (hfin : ∀ᶠ (n : ℕ) in Filter.atTop, walkHitTime (r n + 1) (ω n) ≠ ⊤) (s t : ℕ → ↑(Set.Icc 0 ↑M)) (hs : ∀ (n : ℕ), ↑(s n) = ↑(ladderTime (ω n) (r n)) / ↑(N n)) (ht : ∀ (n : ℕ), ↑(t n) = ↑(ladderTime (ω n) (r n + 1)) / ↑(N n)) {a b : NNReal} (hsa : Filter.Tendsto (fun (n : ℕ) => ↑(s n)) Filter.atTop (nhds ↑a)) (htb : Filter.Tendsto (fun (n : ℕ) => ↑(t n)) Filter.atTop (nhds ↑b)) : runningInfLoc f a = runningInfLoc f b

Limits of finite ladder-block endpoints have the same running infimum. Reference: Billingsley (1999), Chapter 3.