Càdlàg paths with Billingsley's J1 metric

This file defines the space of càdlàg paths on a compact real interval and proves that Billingsley's J1 distance is a metric when the state space is metric.

Horizon conventions: no sign condition on T is imposed. For T < 0 the time domain is empty, D T E is a singleton and every displayed supremum and distance is 0 (Mathlib's convention for empty real suprema). For T = 0, evaluation at 0 identifies D 0 E isometrically with E. The ordinary J1 metric is not complete; Polishness needs Billingsley's equivalent metric d° and is not provided here.

References: P. Billingsley, Convergence of Probability Measures, 2nd ed., 1999, §12; S. N. Ethier and T. G. Kurtz, Markov Processes, 1986, ch. 3 (general metric state spaces).

structure BGW.Skorokhod.D (T : ℝ) (E : Type u_1) [TopologicalSpace E] : Type u_1

The Skorokhod space D([0,T], E) of càdlàg paths on [0,T]. On the subtype Set.Icc 0 T, IsCadlag is Billingsley's condition: right-continuity at every t < T and a left limit at every t > 0.

• toFun : ↑(Set.Icc 0 T) → E

  The underlying path.

• isCadlag' : IsCadlag self.toFun

  The path is càdlàg.

@[instance_reducible]

instance BGW.Skorokhod.instFunLikeDElemRealIccOfNat {T : ℝ} {E : Type u_1} [TopologicalSpace E] : FunLike (D T E) (↑(Set.Icc 0 T)) E

Equations

• BGW.Skorokhod.instFunLikeDElemRealIccOfNat = { coe := BGW.Skorokhod.D.toFun, coe_injective := ⋯ }

@[simp]

theorem BGW.Skorokhod.coe_mk {T : ℝ} {E : Type u_1} [TopologicalSpace E] (p : ↑(Set.Icc 0 T) → E) (hp : IsCadlag p) : ⇑{ toFun := p, isCadlag' := hp } = p

Coercing a path constructor to a function recovers its underlying path.

theorem BGW.Skorokhod.isCadlag {T : ℝ} {E : Type u_1} [TopologicalSpace E] (f : D T E) : IsCadlag ⇑f

The underlying function of a path is càdlàg.

theorem BGW.Skorokhod.ext {T : ℝ} {E : Type u_1} [TopologicalSpace E] {f g : D T E} (h : ∀ (t : ↑(Set.Icc 0 T)), f t = g t) : f = g

theorem BGW.Skorokhod.ext_iff {T : ℝ} {E : Type u_1} [TopologicalSpace E] {f g : D T E} : f = g ↔ ∀ (t : ↑(Set.Icc 0 T)), f t = g t

theorem BGW.Skorokhod.isBounded_range {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f : D T E) : Bornology.IsBounded (Set.range ⇑f)

The range of a càdlàg path on [0,T] is bounded.

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

Billingsley's Skorokhod J1 distance: d(f,g) = inf_σ max (sup_t |σ t - t|) (sup_t dist (f t) (g (σ t))).

Equations

• BGW.Skorokhod.j1Dist f g = ⨅ (σ : BGW.Skorokhod.TimeChange T), max (⨆ (t : ↑(Set.Icc 0 T)), |↑(σ t) - ↑t|) (⨆ (t : ↑(Set.Icc 0 T)), dist (f t) (g (σ t)))

theorem BGW.Skorokhod.bddAbove_range_dist {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f g : D T E) (σ : TimeChange T) : BddAbove (Set.range fun (t : ↑(Set.Icc 0 T)) => dist (f t) (g (σ t)))

Paths are bounded, so the suprema in j1Dist are genuine.

The following helper extracts a time change from a vanishing infimum.

@[instance_reducible]

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

The J1 metric space structure, with distance j1Dist.

Equations

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

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

The J1 metric has distance exactly j1Dist.

theorem BGW.Skorokhod.tendsto_iff_exists_timeChange {T : ℝ} {E : Type u_1} [MetricSpace E] {ι : Type u_2} {l : Filter ι} {u : ι → D T E} {f : D T E} : Filter.Tendsto u l (nhds f) ↔ ∃ (σ : ι → TimeChange T), Filter.Tendsto (fun (i : ι) => ⨆ (t : ↑(Set.Icc 0 T)), |↑((σ i) t) - ↑t|) l (nhds 0) ∧ Filter.Tendsto (fun (i : ι) => ⨆ (t : ↑(Set.Icc 0 T)), dist ((u i) ((σ i) t)) (f t)) l (nhds 0)

Billingsley's characterization of J1 convergence by time changes.

theorem BGW.Skorokhod.dist_le_iSup_dist {T : ℝ} {E : Type u_1} [MetricSpace E] (f g : D T E) : dist f g ≤ ⨆ (t : ↑(Set.Icc 0 T)), dist (f t) (g t)

The J1 distance is at most the uniform distance (take the identity time change).