First passage of the spectrally positive local stable process

This file proves downward creeping, finiteness and the Laplace transform of the strict first passage below a positive level. Bounded stopping is obtained by dyadic approximation from above (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII, Theorem 1; D. Revuz and M. Yor, Continuous Martingales and Brownian Motion, 3rd ed., Springer, 1999, Chapter II, for optional stopping).

theorem BGW.StableTrees.ae_strictPassageBelow_ne_top {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x : ℝ), 0 < x → Skorokhod.DLoc.strictPassageBelow (-x) f ≠ ⊤

Finite first passage. Almost surely, simultaneously for every level x > 0, T_x = inf{t | X_t < -x} is finite.

theorem BGW.StableTrees.ae_creeping_down_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x : ℝ), 0 < x → ∃ (t : NNReal), Skorokhod.DLoc.strictPassageBelow (-x) f = ↑t ∧ ↑f t = -x

Downward creeping. Almost surely, for every level x > 0 the first passage below -x occurs continuously: X_{T_x} = -x.

theorem BGW.StableTrees.ae_runningInf_continuous_antitone_tendsto {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Continuous (runningInfLoc f) ∧ Antitone (runningInfLoc f) ∧ Filter.Tendsto (runningInfLoc f) Filter.atTop Filter.atBot

Running infimum. Almost surely I is continuous, nonincreasing and tends to -∞.

theorem BGW.StableTrees.integral_exp_neg_strictPassageBelow {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {x q : ℝ} (hx : 0 < x) (hq : 0 ≤ q) : ∫ (f : Skorokhod.DLoc), Real.exp (-q * ↑(WithTop.untopD 0 (Skorokhod.DLoc.strictPassageBelow (-x) f))) ∂↑(stableLocalLaw θ) = Real.exp (-x * q ^ (1 / θ))

Laplace transform of the passage time. For x > 0, q ≥ 0: E[e^{-q T_x}] = e^{-x q^{1/θ}} (with T_x finite a.s., read via untopD 0).

theorem BGW.StableTrees.ae_firstPassageBelow_spec {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ↑f 0 = 0 ∧ ∀ (x : NNReal), 0 < x → firstPassageBelow x f < ⊤ ∧ 0 < firstPassageBelow x f ∧ ↑f (WithTop.untopD 0 (firstPassageBelow x f)) = -↑x

Joint almost-sure event. Almost surely, the path starts at 0 and, simultaneously for every level x > 0, the first passage below -x is finite, positive, and the path takes the value -x there.

theorem BGW.StableTrees.lintegral_exp_neg_firstPassageBelow {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {x : NNReal} (hx : 0 < x) {q : ℝ} (hq : 0 ≤ q) : ∫⁻ (f : Skorokhod.DLoc), ENNReal.ofReal (Real.exp (-q * ↑(WithTop.untopD 0 (firstPassageBelow x f)))) ∂↑(stableLocalLaw θ) = ENNReal.ofReal (Real.exp (-↑x * q ^ (1 / θ)))

Laplace transform, nonnegative form. For x > 0, q ≥ 0.