Multiplication of paths by a convergent spatial factor

Uniform bounds on the fixed limiting path suffice for multiplication at factor one.

def BGW.Skorokhod.mulPath {T : ℝ} {E : Type u_1} [NormedRing E] (k : E) (f : D T E) : D T E

Left multiplication of a càdlàg path by a constant.

Equations

• BGW.Skorokhod.mulPath k f = { toFun := fun (t : ↑(Set.Icc 0 T)) => k * f t, isCadlag' := ⋯ }

theorem BGW.Skorokhod.tendsto_mulPath_one {T : ℝ} {E : Type u_1} [NormedRing E] {ι : Type u_2} {l : Filter ι} (hT : 0 ≤ T) {u : ι → D T E} {f : D T E} {k : ι → E} (hu : Filter.Tendsto u l (nhds f)) (hk : Filter.Tendsto k l (nhds 1)) : Filter.Tendsto (fun (i : ι) => mulPath (k i) (u i)) l (nhds f)

Multiplication by spatial factors tending to one preserves J1 convergence.