Interpolating finite time-change data

A finite infimum of affine wedges extends finite data with prescribed lower and upper secant bounds. This supplies controlled time changes without choosing interval indices.

theorem BGW.Skorokhod.exists_timeChange_of_finite_secant_bounds {T : ℝ} {ι : Type u_1} [Fintype ι] [Nonempty ι] (x y : ι → ↑(Set.Icc 0 T)) (i₀ iT : ι) (hx₀ : ↑(x i₀) = 0) (hxT : ↑(x iT) = T) (hy₀ : ↑(y i₀) = 0) (hyT : ↑(y iT) = T) {c C : ℝ} (hc : 0 < c) (hcC : c ≤ C) (hxy : ∀ (i j : ι), x i ≤ x j → c * (↑(x j) - ↑(x i)) ≤ ↑(y j) - ↑(y i) ∧ ↑(y j) - ↑(y i) ≤ C * (↑(x j) - ↑(x i))) : ∃ (σ : TimeChange T), (∀ (i : ι), σ (x i) = y i) ∧ ∀ (s t : ↑(Set.Icc 0 T)), s ≤ t → c * (↑t - ↑s) ≤ ↑(σ t) - ↑(σ s) ∧ ↑(σ t) - ↑(σ s) ≤ C * (↑t - ↑s)

Finite data satisfying positive lower and upper secant bounds extend to a time change with the same secant bounds. The endpoint indices need not be distinct.

theorem BGW.Skorokhod.TimeChange.logSlope_le_of_secant_bounds {T r : ℝ} (σ : TimeChange T) (h : ∀ (s t : ↑(Set.Icc 0 T)), s < t → Real.exp (-r) * (↑t - ↑s) ≤ ↑(σ t) - ↑(σ s) ∧ ↑(σ t) - ↑(σ s) ≤ Real.exp r * (↑t - ↑s)) : σ.logSlope ≤ ENNReal.ofReal r

Exponential two-sided secant bounds control logarithmic slope.