The scalar supremum transform, including the removable diagonal

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

theorem BGW.StableTrees.supremumLaplace_identity_below {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) (hlt : lam < q ^ (1 / θ)) : q ^ (1 / θ) * (q - lam ^ θ) * supremumLaplace θ q lam = q * (q ^ (1 / θ) - lam)

Independence and the process transform give the supremum transform identity below its first singular parameter.

theorem BGW.StableTrees.supremumLaplace_identity {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 < lam) : q ^ (1 / θ) * (q - lam ^ θ) * supremumLaplace θ q lam = q * (q ^ (1 / θ) - lam)

The denominator-free supremum identity holds at every positive parameter.

theorem BGW.StableTrees.integral_exp_neg_supRunning_expTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) (hne : lam ≠ q ^ (1 / θ)) : ∫ (p : Skorokhod.DLoc × ℝ), Real.exp (-lam * supRunning p.1 p.2.toNNReal) ∂expClockLaw θ q = q * (q ^ (1 / θ) - lam) / (q ^ (1 / θ) * (q - lam ^ θ))

Scalar supremum transform, off the diagonal. For every λ ≥ 0, λ ≠ q^{1/θ}: E e^{-λ S_{e_q}} = q (Φ-λ) / (Φ (q-λ^θ)), Φ = q^{1/θ}.

theorem BGW.StableTrees.integral_exp_neg_supRunning_expTime_diag {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : ∫ (p : Skorokhod.DLoc × ℝ), Real.exp (-q ^ (1 / θ) * supRunning p.1 p.2.toNNReal) ∂expClockLaw θ q = 1 / θ

Diagonal value F_q(Φ) = 1/θ (removable singularity of the formula above).