Detection of jumps of càdlàg functions

For a càdlàg x : ℝ≥0 → ℝ, firstJumpAbove q ε x is the first time after q at which x jumps by more than ε. There are finitely many jumps larger than ε on a bounded interval, the first such time is attained, and {σ_{q,ε} < t} has a description through rational times only. Every jump time is such a first-passage time for some rational q ≥ 0 and ε > 0. This is the deterministic input to the enumeration of jumps by stopping times (P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Section 12; J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter I).

noncomputable def BGW.Skorokhod.jumpSize (x : NNReal → ℝ) (t : NNReal) : ℝ

The absolute jump of x at t.

Equations

• BGW.Skorokhod.jumpSize x t = |x t - Function.leftLim x t|

noncomputable def BGW.Skorokhod.firstJumpAbove (q : NNReal) (ε : ℝ) (x : NNReal → ℝ) : ENNReal

The first time after q at which x jumps by more than ε (⊤ if there is none).

Equations

• BGW.Skorokhod.firstJumpAbove q ε x = ⨅ t ∈ {t : NNReal | q < t ∧ ε < BGW.Skorokhod.jumpSize x t}, ↑t

theorem BGW.Skorokhod.finite_setOf_jump_gt_cadlag {x : NNReal → ℝ} (hx : IsCadlag x) {ε : ℝ} (hε : 0 < ε) (T : NNReal) : {t : NNReal | t ≤ T ∧ ε < jumpSize x t}.Finite

Finiteness: a càdlàg function has finitely many jumps larger than ε > 0 on [0, T].

theorem BGW.Skorokhod.firstJumpAbove_eq_top_iff (x : NNReal → ℝ) (q : NNReal) (ε : ℝ) : firstJumpAbove q ε x = ⊤ ↔ ∀ (t : NNReal), q < t → jumpSize x t ≤ ε

The first jump time is ⊤ iff no jump after q is larger than ε.

theorem BGW.Skorokhod.firstJumpAbove_attained {x : NNReal → ℝ} (hx : IsCadlag x) (q : NNReal) {ε : ℝ} (hε : 0 < ε) {s : NNReal} (hs : firstJumpAbove q ε x = ↑s) : q < s ∧ ε < jumpSize x s ∧ ∀ (t : NNReal), q < t → ε < jumpSize x t → s ≤ t

If the first jump above ε is finite, it is attained and is minimal.

theorem BGW.Skorokhod.firstJumpAbove_lt_iff {x : NNReal → ℝ} (hx : IsCadlag x) (q : ℚ≥0) {ε : ℚ} (hε : 0 < ε) (t : NNReal) : firstJumpAbove (↑q) (↑ε) x < ↑t ↔ ∃ (ε' : ℚ), ε < ε' ∧ ∀ (n : ℕ), ∃ (a : ℚ≥0) (b : ℚ≥0), q < a ∧ a < b ∧ ↑b < t ∧ ↑b - ↑a < 1 / (↑n + 1) ∧ ↑ε' ≤ |x ↑b - x ↑a|

Countable characterization of {σ_{q,ε} < t} for a fixed càdlàg path.

theorem BGW.Skorokhod.exists_rat_firstJumpAbove_eq {x : NNReal → ℝ} (hx : IsCadlag x) {s : NNReal} (hs : 0 < s) (hj : x s ≠ Function.leftLim x s) : ∃ (q : ℚ≥0) (ε : ℚ), 0 < ε ∧ firstJumpAbove (↑q) (↑ε) x = ↑s

Every jump time s > 0 is σ_{q,ε} for rational q ≥ 0, ε > 0.