Discounted occupation bounds before recurrence

The reflected resolvent is an unnormalised time integral. Its uniform bound controls first moments of the cumulative occupations at an arbitrary positive rate.

References

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

noncomputable def BGW.StableTrees.supAuxOccupationTail (q ε : ℝ) (s : NNReal) (f : Skorokhod.DLoc) : ℝ

The ordinary time integral of the discounted reflected occupation kernel.

Equations

• BGW.StableTrees.supAuxOccupationTail q ε s f = ∫ (t : ℝ) in Set.Ioi ↑s, Real.exp (-q * t) * BGW.StableTrees.supOccKernel ε (BGW.StableTrees.supReflectedFrom 0 f t.toNNReal)

theorem BGW.StableTrees.measurable_supAuxKernel (ε : ℝ) : Measurable fun (p : ℝ × Skorokhod.DLoc) => supOccKernel ε (supReflectedFrom 0 p.2 p.1.toNNReal)

The reflected occupation kernel is jointly measurable in real time and path.

theorem BGW.StableTrees.measurable_supAuxOccupationTail (q ε : ℝ) (s : NNReal) : Measurable (supAuxOccupationTail q ε s)

The discounted occupation tail is measurable for every rate and cutoff.

theorem BGW.StableTrees.integrable_supAuxKernel_exp {θ q ε : ℝ} (hq : 0 < q) (hε : 0 < ε) (s : NNReal) : MeasureTheory.Integrable (fun (p : ℝ × Skorokhod.DLoc) => Real.exp (-q * p.1) * supOccKernel ε (supReflectedFrom 0 p.2 p.1.toNNReal)) ((MeasureTheory.volume.restrict (Set.Ioi ↑s)).prod ↑(stableLocalLaw θ))

A positive cutoff has an integrable discounted kernel on the time-path product.

theorem BGW.StableTrees.integrable_supAuxOccupationTail (θ : ℝ) {q ε : ℝ} (hq : 0 < q) (hε : 0 < ε) (s : NNReal) : MeasureTheory.Integrable (supAuxOccupationTail q ε s) ↑(stableLocalLaw θ)

The discounted occupation tail is integrable under the local stable law.

theorem BGW.StableTrees.integral_supAuxOccupationTail_zero (θ q ε : ℝ) : ∫ (f : Skorokhod.DLoc), supAuxOccupationTail q ε 0 f ∂↑(stableLocalLaw θ) = supOccupationResolvent θ q ε 0

At zero the occupation tail has exactly the supOccupationResolvent mean, without a rate factor.

theorem BGW.StableTrees.integrableOn_supAuxKernel_exp {q ε : ℝ} (hq : 0 < q) (hε : 0 < ε) (s : NNReal) (f : Skorokhod.DLoc) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-q * t) * supOccKernel ε (supReflectedFrom 0 f t.toNNReal)) (Set.Ioi ↑s) MeasureTheory.volume

Discounted occupation kernels are integrable on every individual path.

theorem BGW.StableTrees.integrable_supOccupation (θ : ℝ) {ε : ℝ} (hε : 0 < ε) (T : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => supOccupation ε f T) ↑(stableLocalLaw θ)

Every fixed-time occupation is integrable, using its deterministic cutoff bound.

theorem BGW.StableTrees.supOccupation_le_exp_mul_tail {q ε : ℝ} (hq : 0 < q) (hε : 0 < ε) (f : Skorokhod.DLoc) (hf : ↑f 0 = 0) (T : NNReal) : supOccupation ε f T ≤ Real.exp (q * ↑T) * supAuxOccupationTail q ε 0 f

Removing the discount on a finite interval costs at most exp (q T).

theorem BGW.StableTrees.integral_supOccupation_le_exp {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q ε : ℝ} (hq : 0 < q) (hε : 0 < ε) (T : NNReal) : ∫ (f : Skorokhod.DLoc), supOccupation ε f T ∂↑(stableLocalLaw θ) ≤ Real.exp (q * ↑T) * (q ^ (1 / θ) / q)

An arbitrary positive resolvent rate gives a cutoff-uniform first-moment growth bound.