Time and space scaling of continuous paths

Time-space scaling is a continuous operation on continuous paths, with the compact-open topology.

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

Time–space scaling of continuous paths (C6.4, continuous coordinates).

Equations

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

theorem BGW.Skorokhod.continuous_timeSpaceScaleC {T : ℝ} {E : Type u_1} [NormedRing E] (a : ℝ) (hT : 0 ≤ T) : Continuous (timeSpaceScaleC a hT)

On continuous paths, time–space scaling is continuous everywhere (C6.4).