Compatibility of the logarithmic-slope metric

Finite interpolation of a small-oscillation partition replaces J1 time changes by ones whose logarithmic slopes tend to zero.

theorem BGW.Skorokhod.continuous_toDComplete_fun {T : ℝ} {E : Type u_1} [MetricSpace E] : Continuous fun (f : D T E) => f

The identity from J1 paths to logarithmic-slope paths is continuous.

theorem BGW.Skorokhod.continuous_fromDComplete_fun {T : ℝ} {E : Type u_1} [MetricSpace E] : Continuous fun (f : DComplete T E) => f

The identity from logarithmic-slope paths to J1 paths is continuous.

noncomputable def BGW.Skorokhod.toDComplete {T : ℝ} {E : Type u_1} [MetricSpace E] : D T E ≃ₜ DComplete T E

The identity map D T E → DComplete T E: d° and the J1 metric induce the same topology (Billingsley 1999, Theorem 12.1).

Equations

• BGW.Skorokhod.toDComplete = { toEquiv := Equiv.refl (BGW.Skorokhod.D T E), continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem BGW.Skorokhod.dist_toDComplete {T : ℝ} {E : Type u_1} [MetricSpace E] (f g : D T E) : dist (toDComplete f) (toDComplete g) = j1CompleteDist f g

The distance of DComplete is d°.