Positive jumps of the spectrally positive stable process

For 1 < θ < 2, independent increments and the stable tail lower bound imply a jump in every fixed nonempty time interval. A countable rational intersection and simultaneous spectral positivity give positive jumps in every open interval almost surely.

theorem BGW.StableTrees.ae_exists_jump_Ioc {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hθ2 : θ < 2) {a b : NNReal} (hab : a < b) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∃ s ∈ Set.Ioc a b, Function.leftLim (↑f) s ≠ ↑f s

For 1 < θ < 2 and a fixed interval (a, b], the stable process jumps in (a, b] almost surely.

theorem BGW.StableTrees.ae_forall_exists_pos_jump {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hθ2 : θ < 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (a b : NNReal), a < b → ∃ s ∈ Set.Ioo a b, Function.leftLim (↑f) s < ↑f s

Host jumps (C22 E3, host level). For 1 < θ < 2, almost surely the stable process has a positive jump in every nonempty open time interval, simultaneously for all intervals.