Continuity of the exponential supremum tail

Atomlessness gives continuity by dominated convergence. The tail tends to zero at infinity and is constant on the negative half-line, hence is uniformly continuous.

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

theorem BGW.StableTrees.supExpTail_eq_measureReal {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (x : ℝ) : supExpTail θ q x = (MeasureTheory.Measure.map (fun (p : Skorokhod.DLoc × ℝ) => supRunning p.1 p.2.toNNReal) (expClockLaw θ q)).real (Set.Ici x)

The negative extension of the tail agrees with the actual exponential-clock probability.

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

Continuity on all of ℝ, including the negative extension at zero.

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

Uniform continuity of the exponential supremum tail over the whole real line.