Exponential density for the first long label

The nonnegative label law has density r exp(-rx) relative to local-time Lebesgue measure.

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

theorem BGW.StableTrees.lintegral_firstLongLabelLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {F : NNReal → ENNReal} (hF : Measurable F) : ∫⁻ (x : NNReal), F x ∂firstLongLabelLaw θ = ∫⁻ (x : NNReal), ENNReal.ofReal (longRate θ) * ENNReal.ofReal (Real.exp (-(↑x * longRate θ))) * F x ∂lebNN

The first-label exponential law integrates against its usual density on nonnegative labels.

theorem BGW.StableTrees.isProbabilityMeasure_firstLongLabelLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.IsProbabilityMeasure (firstLongLabelLaw θ)

The exponential first-label law has total mass one.

theorem BGW.StableTrees.longRate_mul_gamma {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ENNReal.ofReal (longRate θ) * ENNReal.ofReal (Real.Gamma (1 - 1 / θ)) = 1

The long-mark rate cancels the tail-law normalization.