Time and space scaling of càdlàg paths

Positive linear time scaling followed by clipping at the terminal time preserves càdlàg paths.

def BGW.Skorokhod.timeSpaceScale {T : ℝ} {E : Type u_1} [NormedRing E] (a : ℝ) (hT : 0 ≤ T) (p : D T E × E × ↑(Set.Ioi 0)) : D a E

Time–space scaling restricted to [0,a]: t ↦ k * g (min (s * t) T) for a spatial factor k (coordinatewise for E = Fin d → ℝ) and a time factor s > 0 (C6.4).

Equations

• BGW.Skorokhod.timeSpaceScale a hT p = { toFun := fun (t : ↑(Set.Icc 0 a)) => p.2.1 * p.1 ⟨min (↑p.2.2 * ↑t) T, ⋯⟩, isCadlag' := ⋯ }

theorem BGW.Skorokhod.continuousAt_timeSpaceScale {T : ℝ} {E : Type u_1} [NormedRing E] {a : ℝ} (ha : 0 < a) (haT : a < T) {f : D T E} (hf : ContinuousAt ⇑f ⟨a, ⋯⟩) : ContinuousAt (timeSpaceScale a ⋯) (f, 1, ⟨1, ⋯⟩)

Time–space scaling is continuous at (f, 1, 1) when f is continuous at a < T (C6.4, the core of the source's Lemma 5.7).