Bounds and regularity of occupation potentials

The occupation convolution is a weighted average of a uniformly continuous tail potential.

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

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

The supremum potential is uniformly continuous on all real arguments.

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

The supremum potential is continuous on all real arguments.

theorem BGW.StableTrees.supOccupationResolvent_eq_max (θ q ε y : ℝ) : supOccupationResolvent θ q ε y = supOccupationResolvent θ q ε (max y 0)

Negative initial arguments are aliases of the zero start.

theorem BGW.StableTrees.supOccupationResolvent_mem_Icc {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {ε : ℝ} (hε : 0 < ε) (y : ℝ) : supOccupationResolvent θ q ε y ∈ Set.Icc 0 (q ^ (1 / θ) / q)

0 ≤ u^q_ε ≤ Φ/q, on all of ℝ.

theorem BGW.StableTrees.antitoneOn_supOccupationResolvent {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {ε : ℝ} (hε : 0 < ε) : AntitoneOn (supOccupationResolvent θ q ε) (Set.Ici 0)

The occupation resolvent is nonincreasing in the nonnegative start.

theorem BGW.StableTrees.continuousOn_supOccupationResolvent {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {ε : ℝ} (hε : 0 < ε) : ContinuousOn (supOccupationResolvent θ q ε) (Set.Ici 0)

Continuity in the nonnegative initial state.