Time and real scalar space scaling of càdlàg paths

This is the normed-vector-space analogue of timeSpaceScale. Positive time scaling is clipped at the terminal time, while the spatial coordinate is multiplied by a real scalar. The original ring-multiplication API is unchanged.

def BGW.Skorokhod.timeSpaceScaleSMul {T : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℝ) (hT : 0 ≤ T) (p : D T 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.timeSpaceScaleSMul 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_timeSpaceScaleSMul {T : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} (ha : 0 < a) (haT : a < T) {f : D T E} (hf : ContinuousAt ⇑f ⟨a, ⋯⟩) : ContinuousAt (timeSpaceScaleSMul 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).

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

Time–space scaling of continuous paths with a real spatial factor.

Equations

• BGW.Skorokhod.timeSpaceScaleSMulC 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_timeSpaceScaleSMulC {T : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℝ) (hT : 0 ≤ T) : Continuous (timeSpaceScaleSMulC a hT)

Time–space scaling with real spatial factors is continuous on continuous paths.

@[simp]

theorem BGW.Skorokhod.timeSpaceScaleSMul_real {T : ℝ} (a : ℝ) (hT : 0 ≤ T) (p : D T ℝ × ℝ × ↑(Set.Ioi 0)) : timeSpaceScaleSMul a hT p = timeSpaceScale a hT p

On real-valued paths, real scalar spatial scaling agrees with ring multiplication.