Density of the stable supremum at an exponential clock

The signed tilted density is identified from its Laplace integrals before its nonnegativity is deduced. Continuity then gives pointwise positivity.

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

theorem BGW.StableTrees.map_supRunning_expClockLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : MeasureTheory.Measure.map (fun (p : Skorokhod.DLoc × ℝ) => supRunning p.1 p.2.toNNReal) (expClockLaw θ q) = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (x : ℝ) => ENNReal.ofReal (q / q ^ (1 / θ) * (stableSeriesDeriv θ q x - q ^ (1 / θ) * stableSeries θ q x))

Density of the supremum at an exponential time, with its exact normalization.

theorem BGW.StableTrees.stableSeriesDeriv_sub_nonneg {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {x : ℝ} (hx : 0 < x) : 0 ≤ stableSeriesDeriv θ q x - q ^ (1 / θ) * stableSeries θ q x

Positivity of the density (a consequence, not an input).

theorem BGW.StableTrees.expClockLaw_supRunning_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (x : ℝ) : (expClockLaw θ q) {p : Skorokhod.DLoc × ℝ | supRunning p.1 p.2.toNNReal = x} = 0

The supremum at an exponential time has no atoms.