Comparing Billingsley's two distances

On [0,T] the comparison has the factor max 1 T; the unit-interval formula is its special case. In particular the logarithmic-slope distance separates paths.

theorem BGW.Skorokhod.dist_le_exp_of_completeCost_le {T : ℝ} {E : Type u_1} [MetricSpace E] (f g : D T E) (σ : TimeChange T) {r : ℝ} (hr : 0 ≤ r) (hc : completeCost f g σ ≤ ENNReal.ofReal r) : dist f g ≤ max 1 T * (Real.exp r - 1)

A logarithmic matching of cost at most r gives the exponential J1 bound.

theorem BGW.Skorokhod.dist_le_exp_j1CompleteDist_sub_one {T : ℝ} {E : Type u_1} [MetricSpace E] (f g : D T E) : dist f g ≤ max 1 T * (Real.exp (j1CompleteDist f g) - 1)

Comparison of the two metrics on [0,T]: d ≤ max 1 T * (exp d° - 1) (Billingsley 1999, (12.17), stated there for T = 1; the factor T comes from |σ t - t| ≤ t (exp ‖σ‖° - 1)).

theorem BGW.Skorokhod.eq_of_j1CompleteDist_eq_zero {T : ℝ} {E : Type u_1} [MetricSpace E] {f g : D T E} (h : j1CompleteDist f g = 0) : f = g

Zero logarithmic-slope distance implies equality of paths.