Jumps of the normalized stable excursion

At stability index below two, positive jumps of the host inside a valid excursion window give a positive jump of the normalized excursion. The straddling-excursion identity transfers this to the normalized Itô excursion. At index two, the Brownian identification gives a continuous path, whose largest jump is zero.

Transfer to the normalized excursion

theorem BGW.StableTrees.maxJump_excursionRestrict_normalizeExc_pos (θ : ℝ) {g d u : NNReal} {f : Skorokhod.DLoc} (hcut : cutValid g d f) (hu : u ∈ Set.Ioo g d) (hjump : Function.leftLim (↑f) u < ↑f u) : 0 < Skorokhod.maxJump (excursionRestrict 1 (normalizeExc θ (excursionCut g d f)))

Deterministic transfer: a positive jump of the host strictly inside a valid cut (g, d) is a positive jump of the normalized cut excursion restricted to [0,1].

theorem BGW.StableTrees.ae_maxJump_straddling_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hθ2 : θ < 2) {t : NNReal} (ht : 0 < t) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), 0 < Skorokhod.maxJump (excursionRestrict 1 (normalizeExc θ (straddlingExcursion t f)))

For 1 < θ < 2, the normalized excursion straddling t > 0 has a positive jump on [0,1], almost surely.

C22 (E3)

theorem BGW.StableTrees.ae_maxJump_pos_levyExcLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hθ2 : θ < 2) : ∀ᵐ (x : Skorokhod.D 1 ℝ) ∂↑(levyExcLaw θ), 0 < Skorokhod.maxJump x

C22 (E3), θ < 2. The normalized excursion has a positive jump: Δ̄(X^exc) > 0 a.s.

theorem BGW.StableTrees.ae_maxJump_eq_zero_levyExcLaw_two : ∀ᵐ (x : Skorokhod.D 1 ℝ) ∂↑(levyExcLaw 2), Skorokhod.maxJump x = 0 ∧ Continuous ⇑x

C22 (E3), θ = 2. The normalized excursion √2 e is continuous, so Δ̄(X^exc) = 0 a.s.

theorem BGW.StableTrees.ae_maxJump_pos_iff_levyExcLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (x : Skorokhod.D 1 ℝ) ∂↑(levyExcLaw θ), 0 < Skorokhod.maxJump x ↔ θ < 2

C22 (E3), combined form: for 1 < θ ≤ 2, almost surely Δ̄(X^exc) > 0 iff θ < 2.