The Brownian specialization and the non-exponentiality guard

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VI.

theorem BGW.StableTrees.law_supRunning_expTime_two {q : ℝ} (hq : 0 < q) : MeasureTheory.Measure.map (fun (p : Skorokhod.DLoc × ℝ) => supRunning p.1 p.2.toNNReal) (expClockLaw 2 q) = ProbabilityTheory.expMeasure (q ^ (1 / 2))

Brownian case: for θ = 2, S_{e_q} ~ Exp(√q) (Φ = q^{1/2}).

theorem BGW.StableTrees.law_supRunning_expTime_ne_exp {θ : ℝ} (hθ : 1 < θ ∧ θ < 2) {q : ℝ} (hq : 0 < q) : MeasureTheory.Measure.map (fun (p : Skorokhod.DLoc × ℝ) => supRunning p.1 p.2.toNNReal) (expClockLaw θ q) ≠ ProbabilityTheory.expMeasure (q ^ (1 / θ))

Guard: for θ < 2, the supremum is not exponential with rate q^{1/θ}.