Support and lifetime of marked excursions

The simultaneous support theorem identifies the marked cuts with the reflected path.

(J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.)

theorem BGW.StableTrees.ae_jumpExcursion_spec {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, cutValid (passageTimeMinus x f) (passageTime x f) f ∧ (jumpExcursion x f).lifetime = passageTime x f - passageTimeMinus x f ∧ ∀ (t : NNReal), ↑(jumpExcursion x f).path t = ↑(reflectedFrom 0 f) (min (passageTimeMinus x f + t) (passageTime x f))

Lifetime identity and cut validity (a.s., all jump levels at once; uses the excursion support theorem): the cut of (T_{x-}, T_x) is valid, its tag is the true lifetime T_x - T_{x-}, and its path is the reflected path run from T_{x-} and stopped at T_x.

theorem BGW.StableTrees.ae_jumpExcursion_support {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, (∀ (t : NNReal), 0 < t → t < (jumpExcursion x f).lifetime → 0 < ↑(jumpExcursion x f).path t) ∧ (jumpExcursion x f).lifetime = sSup {t : NNReal | 0 < ↑(jumpExcursion x f).path t} ∧ ↑(jumpExcursion x f).path 0 = 0 ∧ ContinuousAt (↑(reflectedFrom 0 f)) (passageTimeMinus x f) ∧ Filter.Tendsto (↑(jumpExcursion x f).path) (nhdsWithin (jumpExcursion x f).lifetime (Set.Iio (jumpExcursion x f).lifetime)) (nhds 0)

Support properties of the excursions: a.s., for every jump level x, the excursion is positive on (0, ζ), its tag is the actual lifetime sup {t | 0 < e t}, it starts at 0 with the reflected path continuous at T_{x-} (no jump start), and its left limit at ζ is 0.