Completeness of Billingsley's logarithmic-slope metric

Geometrically short matchings align a controlled Cauchy sequence. The cumulative time changes converge in the complete space of continuous maps, and their slope bounds prevent degeneration. The aligned paths converge uniformly in the complete state space.

instance BGW.Skorokhod.instCompleteSpaceDComplete {T : ℝ} {E : Type u_1} [MetricSpace E] [CompleteSpace E] : CompleteSpace (DComplete T E)

d° is complete when E is complete (Billingsley 1999, Theorem 12.2).

instance BGW.Skorokhod.instIsCompletelyMetrizableSpace {T : ℝ} {E : Type u_1} [MetricSpace E] [CompleteSpace E] : TopologicalSpace.IsCompletelyMetrizableSpace (D T E)

The Skorokhod space of a complete metric space is completely metrizable (C3).