The stable process transform at an exponential clock

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

noncomputable def BGW.StableTrees.clockEval (p : Skorokhod.DLoc × ℝ) : ℝ

The process value at the independent clock.

Equations

• BGW.StableTrees.clockEval p = ↑p.1 p.2.toNNReal

theorem BGW.StableTrees.measurable_clockEval : Measurable clockEval

Joint evaluation at the independent clock is measurable.

theorem BGW.StableTrees.integral_exp_neg_eval_expTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) (hlt : lam < q ^ (1 / θ)) : MeasureTheory.Integrable (fun (p : Skorokhod.DLoc × ℝ) => Real.exp (-lam * ↑p.1 p.2.toNNReal)) (expClockLaw θ q) ∧ ∫ (p : Skorokhod.DLoc × ℝ), Real.exp (-lam * ↑p.1 p.2.toNNReal) ∂expClockLaw θ q = q / (q - lam ^ θ)

Input for the division step: E e^{-λ X_{e_q}} = q/(q-λ^θ) for 0 ≤ λ < q^{1/θ} (spectrally positive: E e^{-λ X_t} = e^{t λ^θ}), with integrability.