Integral identities for the supremum potential

The identified probability density is integrable without an exponential tilt. Its tail integral gives the potential and its boundary difference.

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

theorem BGW.StableTrees.integrableOn_supremum_density {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : MeasureTheory.IntegrableOn (fun (x : ℝ) => stableSeriesDeriv θ q x - q ^ (1 / θ) * stableSeries θ q x) (Set.Ioi 0) MeasureTheory.volume

The unscaled supremum density is integrable without an exponential weight.

theorem BGW.StableTrees.supExpTail_eq_integral {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {x : ℝ} (hx : 0 ≤ x) : supExpTail θ q x = q / q ^ (1 / θ) * ∫ (y : ℝ) in Set.Ioi x, stableSeriesDeriv θ q y - q ^ (1 / θ) * stableSeries θ q y

H_q(x) = (q/Φ) ∫_x^∞ (W_q'-ΦW_q) for x ≥ 0.

theorem BGW.StableTrees.supPotential_eq_integral {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {x : ℝ} (hx : 0 ≤ x) : supPotential θ q x = ∫ (y : ℝ) in Set.Ioi x, stableSeriesDeriv θ q y - q ^ (1 / θ) * stableSeries θ q y

The potential is the tail integral of the unscaled supremum density.

theorem BGW.StableTrees.supPotential_zero_sub {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {x : ℝ} (hx : 0 ≤ x) : supPotential θ q 0 - supPotential θ q x = stableSeries θ q x - q ^ (1 / θ) * ∫ (y : ℝ) in Set.Ioc 0 x, stableSeries θ q y

h_q(0) - h_q(x) = W_q(x) - Φ ∫_0^x W_q(y)dy for x ≥ 0.