Joint law of the first long label and excursion

Predictable compensation identifies the joint density. The label density is exponential and the excursion factor is the normalized restriction to lifetimes greater than one.

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

theorem BGW.StableTrees.map_firstLongLabel_firstLongMark {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => (firstLongLabel f, firstLongMark f)) ↑(stableLocalLaw θ) = (firstLongLabelLaw θ).prod ↑(tailExcursionLaw θ)

Exponential/product law: the first long label is Exp(r_θ), the first long mark has law tailExcursionLaw θ, and they are independent.

theorem BGW.StableTrees.map_firstLongMark {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.Measure.map firstLongMark ↑(stableLocalLaw θ) = ↑(tailExcursionLaw θ)

Identification of the selected mark with tailExcursionLaw θ (a corollary of the product law; no extraction convergence is assumed).

theorem BGW.StableTrees.map_firstLongLabel {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.Measure.map firstLongLabel ↑(stableLocalLaw θ) = firstLongLabelLaw θ

Marginal of the first label: Exp(r_θ).