Analyticity of the scalar supremum Laplace transform

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

noncomputable def BGW.StableTrees.supremumLaplace (θ q lam : ℝ) : ℝ

The scalar Laplace transform of the supremum at the exponential clock.

Equations

• BGW.StableTrees.supremumLaplace θ q lam = ∫ (p : BGW.Skorokhod.DLoc × ℝ), Real.exp (-lam * BGW.StableTrees.supRunning p.1 p.2.toNNReal) ∂BGW.StableTrees.expClockLaw θ q

theorem BGW.StableTrees.integrable_exp_neg_supRunning_expTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) : MeasureTheory.Integrable (fun (p : Skorokhod.DLoc × ℝ) => Real.exp (-lam * supRunning p.1 p.2.toNNReal)) (expClockLaw θ q)

Nonnegative Laplace parameters give a bounded, integrable test of the supremum.

theorem BGW.StableTrees.analyticAt_supremumLaplace {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 < lam) : AnalyticAt ℝ (supremumLaplace θ q) lam

The supremum Laplace transform is real analytic at every strictly positive parameter.

theorem BGW.StableTrees.supremumLaplace_identity_of_interval {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (hshort : ∀ (lam : ℝ), 0 < lam → lam < q ^ (1 / θ) → q ^ (1 / θ) * (q - lam ^ θ) * supremumLaplace θ q lam = q * (q ^ (1 / θ) - lam)) (lam : ℝ) : 0 < lam → q ^ (1 / θ) * (q - lam ^ θ) * supremumLaplace θ q lam = q * (q ^ (1 / θ) - lam)

An identity for the supremum transform on the initial interval extends to all positive parameters after multiplication by the removable denominator.