Fine-grid increments of continuous càdlàg paths

Uniform continuity on a compact interval controls all sufficiently fine regular grids.

theorem BGW.StableTrees.eventually_grid_increments_le {f : Skorokhod.DLoc} {a b : NNReal} (hab : a < b) (hf : ∀ s ∈ Set.Ioc a b, Function.leftLim (↑f) s = ↑f s) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ k < n, ↑f (a + (↑k + 1) * ((b - a) / ↑n)) - ↑f (a + ↑k * ((b - a) / ↑n)) ≤ δ

Deterministic: a càdlàg path with no jump in (a, b] has uniformly small increments on fine regular grids of [a, b].