The first long excursion under the stable law

Lifetime atomlessness, existence and measurability, the exponential/product law of the selected label and mark, regular geometry at passage jumps, and the localized good-path suppliers.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.tendsto_measure_firstLongEnd_lt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : Filter.Tendsto (fun (M : NNReal) => ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | passageTime (firstLongLabel f) f < M}) Filter.atTop (nhds 1)

Finite end: the selected end T_L is finite a.s. and P(T_L < M) → 1 as M → ∞.

theorem BGW.StableTrees.ae_goodLongExtractionPath {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (M : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), passageTime (firstLongLabel f) f < M → GoodLongExtractionPath M f

ae_goodLongExtractionPath, localized by d < M: a.s., if the first long excursion ends before M, the path is good on [0, M].

theorem BGW.StableTrees.ae_goodLongExtractionCutPath {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (M T : NNReal) (hT : 0 < T) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), passageTime (firstLongLabel f) f < M → GoodLongExtractionCutPath M T f

The cut version, for every positive cutoff T (continuity of the selected cut at T).