Auxiliary lemmas for real step paths

The rescaled step path of a real walk is càdlàg; first-exit and last-exit facts used by the exit-partition bound on Billingsley's modulus.

theorem BGW.Skorokhod.isCadlag_stepPath {T : ℝ} (n : ℕ) (b : ℝ) (ω : ℕ → ℝ) : IsCadlag fun (t : ↑(Set.Icc 0 T)) => Probability.RealWalk.partialSum ω ⌊↑n * ↑t⌋₊ / b

The floor-step path on a compact interval is càdlàg.