Potential measure of stable passage times

The passage potential has Laplace transform q^(-1/θ). Exponential tilting reduces its identification to uniqueness of Laplace transforms for probability measures.

References

J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

noncomputable def BGW.StableTrees.straddleAgeDensity (θ s : ℝ) : ENNReal

Potential density s^{1/θ-1}/Γ(1/θ) of the passage subordinator, on s > 0.

Equations

• BGW.StableTrees.straddleAgeDensity θ s = (Set.Ioi 0).indicator (fun (s : ℝ) => ENNReal.ofReal (s ^ (1 / θ - 1) / Real.Gamma (1 / θ))) s

theorem BGW.StableTrees.passage_potential_measure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {B : Set ℝ} (hB : MeasurableSet B) : ∫⁻ (x : ℝ) in Set.Ioi 0, ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | ↑(passageTime x.toNNReal f) ∈ B} = ∫⁻ (s : ℝ) in B, straddleAgeDensity θ s

Potential measure of the passage subordinator: for measurable B ⊆ ℝ, ∫_0^∞ P(T_x ∈ B) dx = ∫_B s^{1/θ-1}/Γ(1/θ) ds (Laplace transform q^{-1/θ}).

theorem BGW.StableTrees.lintegral_passage_potential {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {F : ℝ → ENNReal} (hF : Measurable F) : ∫⁻ (x : ℝ) in Set.Ioi 0, ∫⁻ (f : Skorokhod.DLoc), F ↑(passageTime x.toNNReal f) ∂↑(stableLocalLaw θ) = ∫⁻ (s : ℝ), straddleAgeDensity θ s * F s

Integral form of the passage potential identity for nonnegative measurable functions.