Ladder exponent algebra and Laplace functionals

Algebra of the exact ladder exponent and the boundary and ladder Laplace functionals.

noncomputable def BGW.StableTrees.supBoundaryPotential (θ q lam : ℝ) (f : Skorokhod.DLoc) : ENNReal

The boundary potential of the path: ∫_{(0,∞)} e^{-qt-λS_t} dM_t, M = supLocalTime (Stieltjes measure supLocalTimeStieltjes), in ℝ≥0∞ (no junk).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGW.StableTrees.supLadderLaplace (θ q lam : ℝ) (z : NNReal) : ℝ

The ladder Laplace transform φ_{q,λ}(z) = E exp(-q A_z - λ B_z).

Equations

• One or more equations did not get rendered due to their size.

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

κ(q,λ) > 0 for q > 0, λ ≥ 0 (both branches; diagonal θ q^{1-1/θ} > 0).

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

1/κ is the mean potential (Φ/q) F_q(λ), including the diagonal (F_q(Φ) = 1/θ, from BGW.StableTrees.SupremumDrawdown). Pure algebra from integral_exp_neg_supRunning_expTime; no ladder object enters.

Reference: Bertoin, Lévy Processes, Chapter VI.

theorem BGW.StableTrees.inv_supLadderExponent_eq_of_ne {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) (hne : lam ≠ q ^ (1 / θ)) : (supLadderExponent θ q lam)⁻¹ = (q ^ (1 / θ) - lam) / (q - lam ^ θ)

Off the diagonal: 1/κ = (Φ-λ)/(q-λ^θ).

Reference: Bertoin, Lévy Processes, Chapter VI.

theorem BGW.StableTrees.tendsto_supLadderExponent_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {lam : ℝ} (hlam : 0 ≤ lam) : Filter.Tendsto (fun (q : ℝ) => supLadderExponent θ q lam) (nhdsWithin 0 (Set.Ioi 0)) (nhds (supLadderExponent θ 0 lam))

Continuity of κ in q ↓ 0 at fixed λ ≥ 0 (to κ(0,λ) = λ^{θ-1}; at λ = 0 the value is 0), needed to pass from q > 0 to q = 0.