Extending a linear time scaling

A linear map on a proper initial subinterval extends to an ambient time change with arbitrarily small displacement as its slope tends to one.

def BGW.Skorokhod.reparam {T : ℝ} {E : Type u_1} [TopologicalSpace E] (g : D T E) (σ : TimeChange T) : D T E

Reparametrize a path by an increasing homeomorphism of its time interval.

Equations

• BGW.Skorokhod.reparam g σ = { toFun := ⇑g ∘ ⇑σ, isCadlag' := ⋯ }

theorem BGW.Skorokhod.dist_reparam_le {T : ℝ} {E : Type u_1} [MetricSpace E] (hT : 0 ≤ T) (g : D T E) (σ : TimeChange T) : dist (reparam g σ) g ≤ ⨆ (t : ↑(Set.Icc 0 T)), |↑(σ t) - ↑t|

Reparametrization costs at most the uniform displacement of the time change.

theorem BGW.Skorokhod.eventually_exists_timeChange_scale {T a : ℝ} (ha : 0 < a) (haT : a < T) {ι : Type u_1} {l : Filter ι} {s : ι → ↑(Set.Ioi 0)} (hs : Filter.Tendsto (fun (i : ι) => ↑(s i)) l (nhds 1)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ι) in l, ∃ (γ : TimeChange T), (∀ (t : ↑(Set.Icc 0 T)), ↑t ≤ a → ↑(γ t) = ↑(s i) * ↑t) ∧ ∀ (t : ↑(Set.Icc 0 T)), |↑(γ t) - ↑t| ≤ ε

Linear scalings tending to one have arbitrarily small ambient endpoint corrections.