Selecting the first long label

Finite counts on bounded label windows give a least long label. The exponential void probabilities exclude the event that all such windows are empty.

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

theorem BGW.StableTrees.longRate_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : 0 < longRate θ

The long-mark intensity is strictly positive in the stable range.

theorem BGW.StableTrees.measure_no_longMarks {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | (excursionPointMeasure f) (Set.Ioc 0 t ×ˢ {e : Excursion | 1 < e.lifetime}) = 0} = ENNReal.ofReal (Real.exp (-(↑t * longRate θ)))

The probability that a bounded initial label window has no long mark.

theorem BGW.StableTrees.ae_exists_longLabel {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∃ (L : NNReal), IsLeast (longLabelSet f) L

A.s. there is a long label and a least one.

theorem BGW.StableTrees.firstLongLabel_eq_of_isLeast {f : Skorokhod.DLoc} {L : NNReal} (hL : IsLeast (longLabelSet f) L) : firstLongLabel f = L

The infimum defining the first label equals any least long label.

theorem BGW.StableTrees.ae_firstLongLabel_mem {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), firstLongLabel f ∈ longLabelSet f

Almost surely, the selected label is a long passage jump.