Documentation

BGW.Skorokhod.CompleteMetricCore

Billingsley's distance with logarithmic time-change cost #

The extended cost is finite at the identity, so its infimum has a genuine real value.

source
noncomputable def BGW.Skorokhod.j1CompleteDist {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f g : D T E) :
ℝ

Billingsley's distance d°(f,g) = inf_σ max (‖σ‖°, sup_t dist (f t) (g (σ t))) (C3).

Equations
Instances For
    source
    noncomputable def BGW.Skorokhod.completeCost {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f g : D T E) (σ : TimeChange T) :
    ENNReal

    Extended cost of matching two paths with a given time change.

    Equations
    Instances For
      source
      theorem BGW.Skorokhod.iSup_edist_ne_top {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f g : D T E) (σ : TimeChange T) :
      ⨆ (t : ↑(Set.Icc 0 T)), edist (f t) (g (σ t)) ≠ ⊤

      The path part of a time-change cost is finite.

      source
      @[simp]
      theorem BGW.Skorokhod.completeCost_refl {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f : D T E) :
      completeCost f f (OrderIso.refl ↑(Set.Icc 0 T)) = 0

      Matching a path with itself using the identity costs zero.

      source
      theorem BGW.Skorokhod.iInf_completeCost_ne_top {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f g : D T E) :
      ⨅ (σ : TimeChange T), completeCost f g σ ≠ ⊤

      The infimum of matching costs is finite, because the identity is admissible.

      source
      theorem BGW.Skorokhod.j1CompleteDist_nonneg {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f g : D T E) :
      0 ≤ j1CompleteDist f g

      Billingsley's distance is nonnegative.

      source
      theorem BGW.Skorokhod.exists_completeCost_lt {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f g : D T E) {r : ℝ} (hr : j1CompleteDist f g < r) :
      ∃ (σ : TimeChange T), completeCost f g σ < ENNReal.ofReal r

      Any radius strictly above the distance admits a matching with smaller cost.

      source
      theorem BGW.Skorokhod.completeCost_symm {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f g : D T E) (σ : TimeChange T) :
      completeCost g f (OrderIso.symm σ) = completeCost f g σ

      Inverting a time change exchanges the two paths without changing the cost.

      source
      theorem BGW.Skorokhod.completeCost_trans_le {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f g h : D T E) (σ τ : TimeChange T) :
      completeCost f h (OrderIso.trans σ τ) ≤ completeCost f g σ + completeCost g h τ

      Composing time changes gives the triangle bound for matching costs.

      source
      @[simp]
      theorem BGW.Skorokhod.j1CompleteDist_self {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f : D T E) :
      j1CompleteDist f f = 0

      Billingsley's distance vanishes on the diagonal.

      source
      theorem BGW.Skorokhod.j1CompleteDist_comm {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f g : D T E) :
      j1CompleteDist f g = j1CompleteDist g f

      Billingsley's distance is symmetric.

      source
      theorem BGW.Skorokhod.j1CompleteDist_triangle {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f g h : D T E) :
      j1CompleteDist f h ≤ j1CompleteDist f g + j1CompleteDist g h

      Billingsley's distance satisfies the triangle inequality.

      source
      theorem BGW.Skorokhod.j1CompleteDist_le_of_completeCost_le {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f g : D T E) (σ : TimeChange T) {r : ℝ} (hr : 0 ≤ r) (hc : completeCost f g σ ≤ ENNReal.ofReal r) :
      j1CompleteDist f g ≤ r

      A matching of cost at most a nonnegative radius bounds the distance.