Support of the excursion measure, transferred through measurable compact-window lower bounds.

See Bertoin, Lévy Processes, Chapter IV.

theorem BGW.StableTrees.ae_excursionMeasure_support {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (e : Excursion) ∂excursionMeasure θ, (∀ (t : NNReal), 0 < t → t < e.lifetime → 0 < ↑e.path t) ∧ e.lifetime = sSup {t : NNReal | 0 < ↑e.path t} ∧ ↑e.path 0 = 0 ∧ ContinuousAt (↑e.path) 0 ∧ Filter.Tendsto (↑e.path) (nhdsWithin e.lifetime (Set.Iio e.lifetime)) (nhds 0)

Support of N: N-a.e. excursion is positive on (0, ζ), its tag is sup {t | 0 < e t}, e 0 = 0, e is continuous (right-continuous) at 0, and e t → 0 as t ↑ ζ. (The carrier only supplies a positive tag; this support theorem identifies the tag with the actual lifetime sup {t | 0 < e t}.)