Supremum potentials and reflected occupation resolvents

Analytic functions for the scale series, exponential-clock supremum tail, and occupation resolvents of the reflected stable family.

Reference: A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014, Chapter 8.

noncomputable def BGW.StableTrees.stableScale (θ x : ℝ) : ℝ

W(x) = x^{θ-1}/Γ(θ) for x ≥ 0, 0 for x < 0.

Equations

• BGW.StableTrees.stableScale θ x = if 0 ≤ x then x ^ (θ - 1) / Real.Gamma θ else 0

noncomputable def BGW.StableTrees.stableSeriesTerm (θ q : ℝ) (n : ℕ) (x : ℝ) : ℝ

Term q^n x^{θ(n+1)-1}/Γ(θ(n+1)) of W_q.

Equations

• BGW.StableTrees.stableSeriesTerm θ q n x = q ^ n * x ^ (θ * (↑n + 1) - 1) / Real.Gamma (θ * (↑n + 1))

noncomputable def BGW.StableTrees.stableSeriesDerivTerm (θ q : ℝ) (n : ℕ) (x : ℝ) : ℝ

Term q^n x^{θ(n+1)-2}/Γ(θ(n+1)-1) of W_q'.

Equations

• BGW.StableTrees.stableSeriesDerivTerm θ q n x = q ^ n * x ^ (θ * (↑n + 1) - 2) / Real.Gamma (θ * (↑n + 1) - 1)

noncomputable def BGW.StableTrees.stableSeries (θ q x : ℝ) : ℝ

W_q(x) for x ≥ 0, 0 for x < 0.

Equations

• BGW.StableTrees.stableSeries θ q x = if 0 ≤ x then ∑' (n : ℕ), BGW.StableTrees.stableSeriesTerm θ q n x else 0

noncomputable def BGW.StableTrees.stableSeriesDeriv (θ q x : ℝ) : ℝ

Termwise derivative of W_q on (0,∞), 0 elsewhere.

Equations

• BGW.StableTrees.stableSeriesDeriv θ q x = if 0 < x then ∑' (n : ℕ), BGW.StableTrees.stableSeriesDerivTerm θ q n x else 0

noncomputable def BGW.StableTrees.supExpTail (θ q x : ℝ) : ℝ

H_q(x) = P(S_{e_q} ≥ x) for x ≥ 0, extended by 1 for x < 0.

Equations

• BGW.StableTrees.supExpTail θ q x = if x < 0 then 1 else ((BGW.StableTrees.expClockLaw θ q) {p : BGW.Skorokhod.DLoc × ℝ | x ≤ BGW.StableTrees.supRunning p.1 p.2.toNNReal}).toReal

noncomputable def BGW.StableTrees.supPotential (θ q x : ℝ) : ℝ

h_q = (Φ/q) H_q, Φ = q^{1/θ}.

Equations

• BGW.StableTrees.supPotential θ q x = q ^ (1 / θ) / q * BGW.StableTrees.supExpTail θ q x

noncomputable def BGW.StableTrees.supOccKernel (ε r : ℝ) : ℝ

The occupation kernel g_ε(r) = ε⁻¹ 1{r < ε}.

Equations

• BGW.StableTrees.supOccKernel ε r = (Set.Iio ε).indicator (fun (x : ℝ) => ε⁻¹) r

noncomputable def BGW.StableTrees.reflectedResolvent (θ q : ℝ) (k : ℝ → ℝ) (y : ℝ) : ℝ

q-resolvent of the reflected family on a bounded Borel k: y ↦ E ∫_0^∞ e^{-qt} k(R^y_t) dt (start y.toNNReal).

Equations

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

noncomputable def BGW.StableTrees.supOccupationResolvent (θ q ε y : ℝ) : ℝ

u^q_ε = reflectedResolvent θ q g_ε.

Equations

• BGW.StableTrees.supOccupationResolvent θ q ε y = BGW.StableTrees.reflectedResolvent θ q (BGW.StableTrees.supOccKernel ε) y

noncomputable def BGW.StableTrees.supCorrection (θ ε x : ℝ) : ℝ

The zero-resolvent correction v_ε.

Equations

• BGW.StableTrees.supCorrection θ ε x = (BGW.StableTrees.stableScale θ x - ε⁻¹ * ∫ (r : ℝ) in Set.Ioc 0 ε, BGW.StableTrees.stableScale θ (x - r)) - if θ = 2 then ε / 2 else 0

theorem BGW.StableTrees.stableScale_eq_zero {θ x : ℝ} (hθ : 1 < θ) (hx : x ≤ 0) : stableScale θ x = 0

The scale vanishes on the nonpositive half-line for a stable index.

theorem BGW.StableTrees.stableSeries_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q : ℝ) : stableSeries θ q 0 = 0

The scale series vanishes at its left endpoint.

theorem BGW.StableTrees.supExpTail_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : supExpTail θ q 0 = 1

The exponential-clock supremum tail equals one at zero.

theorem BGW.StableTrees.supExpTail_mem_Icc {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (x : ℝ) : supExpTail θ q x ∈ Set.Icc 0 1

The exponential-clock tail takes values in the unit interval.

theorem BGW.StableTrees.antitone_supExpTail {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : Antitone (supExpTail θ q)

The exponential-clock supremum tail is nonincreasing.

theorem BGW.StableTrees.supPotential_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : supPotential θ q 0 = q ^ (1 / θ) / q

The boundary potential has the required normalization.

theorem BGW.StableTrees.supPotential_mem_Icc {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (x : ℝ) : supPotential θ q x ∈ Set.Icc 0 (q ^ (1 / θ) / q)

The potential lies between zero and its boundary value.

theorem BGW.StableTrees.measurable_supOccKernel (ε : ℝ) : Measurable (supOccKernel ε)

The occupation cutoff is a Borel function.

theorem BGW.StableTrees.supOccKernel_mem_Icc {ε : ℝ} (hε : 0 < ε) (r : ℝ) : supOccKernel ε r ∈ Set.Icc 0 ε⁻¹

The positive occupation kernel lies in its sharp constant interval.

theorem BGW.StableTrees.supCorrection_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) : supCorrection θ ε 0 = -if θ = 2 then ε / 2 else 0

The correction at the reflecting boundary.

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

The boundary potential gives the Brownian correction exponent.

theorem BGW.StableTrees.tendsto_rpow_two_div_sub_one {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : Filter.Tendsto (fun (q : ℝ) => q ^ (2 / θ - 1)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (if θ = 2 then 1 else 0))

The scalar correction exponent distinguishes the Brownian endpoint.