Limits of time changes with bounded logarithmic slope

A uniform slope bound prevents degeneration of a pointwise limit: its lower secant bound remains strictly positive. Logarithmic slope bounds pass to limits of time changes.

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

A logarithmic slope bound is equivalent to exponential two-sided secant bounds.

theorem BGW.Skorokhod.TimeChange.logSlope_le_of_tendsto {T : ℝ} {κ : Type u_1} {l : Filter κ} [l.NeBot] (σ : κ → TimeChange T) (τ : TimeChange T) (hlim : ∀ (t : ↑(Set.Icc 0 T)), Filter.Tendsto (fun (n : κ) => ↑((σ n) t)) l (nhds ↑(τ t))) {r : ℝ} (hr : 0 ≤ r) (hσ : ∀ᶠ (n : κ) in l, (σ n).logSlope ≤ ENNReal.ofReal r) : τ.logSlope ≤ ENNReal.ofReal r

Logarithmic slope bounds pass to pointwise limits that are time changes.

theorem BGW.Skorokhod.exists_timeChange_of_tendsto_bounded_logSlope {T : ℝ} (hT : 0 ≤ T) (σ : ℕ → TimeChange T) (f : C(↑(Set.Icc 0 T), ↑(Set.Icc 0 T))) (hlim : ∀ (t : ↑(Set.Icc 0 T)), Filter.Tendsto (fun (n : ℕ) => ↑((σ n) t)) Filter.atTop (nhds ↑(f t))) {r : ℝ} (hr : 0 ≤ r) (hσ : ∀ (n : ℕ), (σ n).logSlope ≤ ENNReal.ofReal r) : ∃ (τ : TimeChange T), ∀ (t : ↑(Set.Icc 0 T)), τ t = f t

A continuous pointwise limit of time changes with uniformly bounded logarithmic slope is itself a time change.

theorem BGW.Skorokhod.isCadlag_comp_timeChange {T : ℝ} {E : Type u_1} [TopologicalSpace E] {f : ↑(Set.Icc 0 T) → E} (hf : IsCadlag f) (σ : TimeChange T) : IsCadlag (f ∘ ⇑σ)

Composing a càdlàg path with a time change preserves the càdlàg property.