Billingsley's metric on the Skorokhod space

The type synonym carries the metric defined by logarithmic time-change cost.

def BGW.Skorokhod.DComplete (T : ℝ) (E : Type u_2) [TopologicalSpace E] : Type u_2

The Skorokhod space carrying Billingsley's metric d° (a type synonym of D T E).

Equations

• BGW.Skorokhod.DComplete T E = BGW.Skorokhod.D T E

@[instance_reducible]

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

The metric space structure of d° on DComplete T E.

Equations

• One or more equations did not get rendered due to their size.