Measurability of the first long excursion

Rational label windows detect the first long label. Their countable infimum supplies a measurable version of the raw infimum selector on the almost-sure selection event.

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

theorem BGW.StableTrees.longCount_eq_zero_iff {f : Skorokhod.DLoc} (hc : (passageJumpSet f).Countable) (hs : ∀ x ∈ passageJumpSet f, (jumpExcursion x f).lifetime = passageTime x f - passageTimeMinus x f) (t : NNReal) : (excursionPointMeasure f) (Set.Ioc 0 t ×ˢ {e : Excursion | 1 < e.lifetime}) = 0 ↔ ∀ x ∈ longLabelSet f, t < x

On paths with valid excursion tags, a void long-mark window is equivalent to having all long labels strictly beyond the end of the window.

theorem BGW.StableTrees.ae_longCount_eq_zero_iff {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), (excursionPointMeasure f) (Set.Ioc 0 t ×ˢ {e : Excursion | 1 < e.lifetime}) = 0 ↔ t < firstLongLabel f

On the full-measure selection event, initial void probabilities detect the first label.

theorem BGW.StableTrees.aemeasurable_firstLongLabel {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : AEMeasurable firstLongLabel ↑(stableLocalLaw θ)

The first long label is a.e.-measurable (junk off the a.s. event).

theorem BGW.StableTrees.aemeasurable_firstLongMark {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : AEMeasurable firstLongMark ↑(stableLocalLaw θ)

The first long mark is a.e.-measurable.