Compensation at the first long excursion

The predictable no-earlier-mark indicator leaves exactly one term in the marked sum.

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

theorem BGW.StableTrees.lintegral_firstLong_pair {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {F : NNReal × Excursion → ENNReal} (hF : Measurable F) : ∫⁻ (f : Skorokhod.DLoc), F (firstLongLabel f, firstLongMark f) ∂↑(stableLocalLaw θ) = ∫⁻ (x : NNReal), ENNReal.ofReal (Real.exp (-(↑x * longRate θ))) * ∫⁻ (e : Excursion) in {e : Excursion | 1 < e.lifetime}, F (x, e) ∂excursionMeasure θ ∂lebNN

Nonnegative tests of the first label and mark, evaluated by predictable compensation.