Largest jumps of real càdlàg paths

The largest positive and absolute jumps are invariant under time changes and are 2-Lipschitz for the Skorokhod J1 metric.

noncomputable def BGW.Skorokhod.maxJump {T : ℝ} (f : D T ℝ) : ℝ

The largest positive jump sup_t (f t - f (t-)) ∨ 0 of a real càdlàg path (C36).

Equations

• BGW.Skorokhod.maxJump f = ⨆ (t : ↑(Set.Icc 0 T)), max (f t - Function.leftLim (⇑f) t) 0

noncomputable def BGW.Skorokhod.maxAbsJump {T : ℝ} (f : D T ℝ) : ℝ

The largest absolute jump sup_t |f t - f (t-)| of a real càdlàg path (C36).

Equations

• BGW.Skorokhod.maxAbsJump f = ⨆ (t : ↑(Set.Icc 0 T)), |f t - Function.leftLim (⇑f) t|

theorem BGW.Skorokhod.bddAbove_absJump {T : ℝ} (f : D T ℝ) : BddAbove (Set.range fun (t : ↑(Set.Icc 0 T)) => |f t - Function.leftLim (⇑f) t|)

Absolute jump sizes of a bounded-horizon càdlàg path are bounded above.

theorem BGW.Skorokhod.bddAbove_maxJump {T : ℝ} (f : D T ℝ) : BddAbove (Set.range fun (t : ↑(Set.Icc 0 T)) => max (f t - Function.leftLim (⇑f) t) 0)

Positive jump sizes of a bounded-horizon càdlàg path are bounded above.

theorem BGW.Skorokhod.lipschitzWith_two_maxJump {T : ℝ} : LipschitzWith 2 maxJump

The largest positive jump is 2-Lipschitz for J1 (C36).

theorem BGW.Skorokhod.lipschitzWith_two_maxAbsJump {T : ℝ} : LipschitzWith 2 maxAbsJump

The largest absolute jump is 2-Lipschitz for J1 (C36).

theorem BGW.Skorokhod.maxJump_eq_zero_of_continuous {T : ℝ} {f : D T ℝ} (hf : Continuous ⇑f) : maxJump f = 0

C36, continuous paths. A continuous path has zero largest upward jump.

theorem BGW.Skorokhod.maxJump_eq_zero_iff_continuous_of_leftLim_le {T : ℝ} (f : D T ℝ) (hf : ∀ (t : ↑(Set.Icc 0 T)), Function.leftLim (⇑f) t ≤ f t) : maxJump f = 0 ↔ Continuous ⇑f

C36 with nonnegative jumps. If every jump is nonnegative, vanishing of maxJump is equivalent to continuity.