Exponential tails and transforms for the drawdown clock

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VI.

theorem BGW.StableTrees.expMeasure_Ioi_nonneg {r : ℝ} (hr : 0 < r) {y : ℝ} (hy : 0 ≤ y) : (ProbabilityTheory.expMeasure r) (Set.Ioi y) = ENNReal.ofReal (Real.exp (-(r * y)))

The strict upper tail of a positive-rate exponential law.

theorem BGW.StableTrees.lintegral_exp_mul_expMeasure {r c : ℝ} (hr : 0 < r) (hc : c < r) : ∫⁻ (t : ℝ), ENNReal.ofReal (Real.exp (c * t)) ∂ProbabilityTheory.expMeasure r = ENNReal.ofReal (r / (r - c))

The exponential moment on its finite domain, in nonnegative integral form.

theorem BGW.StableTrees.integral_exp_mul_expMeasure {r c : ℝ} (hr : 0 < r) (hc : c < r) : MeasureTheory.Integrable (fun (t : ℝ) => Real.exp (c * t)) (ProbabilityTheory.expMeasure r) ∧ ∫ (t : ℝ), Real.exp (c * t) ∂ProbabilityTheory.expMeasure r = r / (r - c)

Exponential moments are integrable on their finite domain, with the usual value.