Matching small-oscillation partitions

Matching partition nodes controls the complete Skorokhod distance without constructing auxiliary step paths.

theorem BGW.Skorokhod.exists_halfOpen_partition_block {n : ℕ} (t : Fin (n + 1) → ℝ) {u : ℝ} (h₀ : t 0 ≤ u) (hT : u < t (Fin.last n)) : ∃ (i : Fin n), t i.castSucc ≤ u ∧ u < t i.succ

Every time strictly before the last node lies in a half-open partition block.

theorem BGW.Skorokhod.partition_gap_lt {n : ℕ} (p : Fin (n + 1) → ℝ) (hp : StrictMono p) {δ : ℝ} (hgap : ∀ (i : Fin n), δ < p i.succ - p i.castSucc) {i j : Fin (n + 1)} (hij : i < j) : δ < p j - p i

A lower bound on adjacent partition gaps also bounds every nonzero node gap.

theorem BGW.Skorokhod.partition_length_le {T : ℝ} {n : ℕ} (p : Fin (n + 1) → ℝ) (hp0 : p 0 = 0) (hpT : p (Fin.last n) = T) {δ : ℝ} (hδ : 0 < δ) (hgap : ∀ (i : Fin n), δ < p i.succ - p i.castSucc) : n ≤ ⌈T / δ⌉₊

Positive minimum spacing bounds the number of blocks.

theorem BGW.Skorokhod.j1CompleteDist_le_of_partition_match {T : ℝ} {E : Type u_1} [MetricSpace E] (f g : D T E) {n : ℕ} (x y : Fin (n + 1) → ↑(Set.Icc 0 T)) (hx0 : ↑(x 0) = 0) (hxT : ↑(x (Fin.last n)) = T) (hx : StrictMono x) (hy : StrictMono y) {a b r : ℝ} (ha : 0 ≤ a) (hr : 0 ≤ r) (hf : ∀ (i : Fin n) (s t : ↑(Set.Icc 0 T)), x i.castSucc ≤ s → s < x i.succ → x i.castSucc ≤ t → t < x i.succ → dist (f s) (f t) ≤ a) (hg : ∀ (i : Fin n) (s t : ↑(Set.Icc 0 T)), y i.castSucc ≤ s → s < y i.succ → y i.castSucc ≤ t → t < y i.succ → dist (g s) (g t) ≤ a) (hnode : ∀ (i : Fin (n + 1)), dist (f (x i)) (g (y i)) ≤ b) (σ : TimeChange T) (hσ : ∀ (i : Fin (n + 1)), σ (x i) = y i) (hlog : σ.logSlope ≤ ENNReal.ofReal r) : j1CompleteDist f g ≤ max r (2 * a + b)

Matching all partition nodes, together with bounds on node values and block oscillations, controls Billingsley's complete distance.

theorem BGW.Skorokhod.j1CompleteDist_lt_of_close_partition_nodes {T : ℝ} {E : Type u_1} [MetricSpace E] (f g : D T E) {n : ℕ} (x y : Fin (n + 1) → ↑(Set.Icc 0 T)) (hx0 : ↑(x 0) = 0) (hxT : ↑(x (Fin.last n)) = T) (hy0 : ↑(y 0) = 0) (hyT : ↑(y (Fin.last n)) = T) (hx : StrictMono x) (hy : StrictMono y) {ε δ κ : ℝ} (hε : 0 < ε) (hκ : κ ≤ ε / 16) (hκlow : 8 * κ ≤ (1 - Real.exp (-(ε / 2))) * δ) (hκupp : 8 * κ ≤ (Real.exp (ε / 2) - 1) * δ) (hgap : ∀ (i : Fin n), δ < ↑(x i.succ) - ↑(x i.castSucc)) (hf : ∀ (i : Fin n) (s t : ↑(Set.Icc 0 T)), x i.castSucc ≤ s → s < x i.succ → x i.castSucc ≤ t → t < x i.succ → dist (f s) (f t) ≤ ε / 8) (hg : ∀ (i : Fin n) (s t : ↑(Set.Icc 0 T)), y i.castSucc ≤ s → s < y i.succ → y i.castSucc ≤ t → t < y i.succ → dist (g s) (g t) ≤ ε / 8) (hnode : ∀ (i : Fin (n + 1)), dist (↑(x i), f (x i)) (↑(y i), g (y i)) < 2 * κ) : j1CompleteDist f g < ε

Close node times and values of two small-oscillation partitions give a small complete distance. The time tolerance is chosen relative to the minimum partition spacing.