Summing excursion lifetimes

Disjoint passage intervals have total length at most the passage time. The null zero set removes the possible drift term and also proves summability in the nonnegative reals.

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

theorem BGW.StableTrees.ae_passageTime_eq_tsum_lifetime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (K : NNReal), passageTime K f = ∑' (x : ↑{x : NNReal | x ∈ passageJumpSet f ∧ x ≤ K}), (jumpExcursion (↑x) f).lifetime

Pure-jump passage time: a.s., simultaneously for all K, T_K is the sum of the lifetimes of the excursions at jump levels x ≤ K (no drift).

theorem BGW.StableTrees.ae_finite_excursionCount {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (K ε : NNReal), 0 < K → 0 < ε → ↑ε * (excursionPointMeasure f) (Set.Ioc 0 K ×ˢ {e : Excursion | ε < e.lifetime}) ≤ ↑(passageTime K f) ∧ (excursionPointMeasure f) (Set.Ioc 0 K ×ˢ {e : Excursion | ε < e.lifetime}) < ⊤

Finite counts of long excursions and the passage-time bound ε * count ≤ T_K: for all K, ε > 0 simultaneously.