Convergence in mean of discounted occupation tails

Half-rate growth dominates the expected absolute cumulative errors. The ordinary cumulative formula then transfers this convergence to discounted occupation tails.

References

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

theorem BGW.StableTrees.tendsto_integral_discounted_supAuxError {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (s : NNReal) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in Set.Ioi ↑s, Real.exp (-q * t) * ∫ (f : Skorokhod.DLoc), |supOccupation ε f t.toNNReal - supAuxLocalTime θ f t.toNNReal| ∂↑(stableLocalLaw θ)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Discounted absolute cumulative errors tend to zero in mean over time.

theorem BGW.StableTrees.discounted_cumulative_eq_primitive {m : ℝ → ℝ} {q : ℝ} (hq : 0 < q) (s a : ℝ) (hi : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-q * t) * m t) (Set.Ioi s) MeasureTheory.volume) : q * ∫ (t : ℝ) in Set.Ioi s, Real.exp (-q * t) * (m t - a) = (q * ∫ (t : ℝ) in Set.Ioi s, Real.exp (-q * t) * m t) - Real.exp (-q * s) * a

The discounted cumulative formula separates the endpoint term explicitly.

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

The discounted difference of occupation and clock cumulatives is product integrable.

theorem BGW.StableTrees.integral_abs_supAuxOccupationTail_sub_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q ε : ℝ} (hq : 0 < q) (hε : 0 < ε) (s : NNReal) : ∫ (f : Skorokhod.DLoc), |supAuxOccupationTail q ε s f - supAuxDiscountedTail θ q s f| ∂↑(stableLocalLaw θ) ≤ (q * ∫ (t : ℝ) in Set.Ioi ↑s, Real.exp (-q * t) * ∫ (f : Skorokhod.DLoc), |supOccupation ε f t.toNNReal - supAuxLocalTime θ f t.toNNReal| ∂↑(stableLocalLaw θ)) + Real.exp (-q * ↑s) * ∫ (f : Skorokhod.DLoc), |supOccupation ε f s - supAuxLocalTime θ f s| ∂↑(stableLocalLaw θ)

The cumulative error controls the difference of discounted clock tails in mean.

theorem BGW.StableTrees.tendsto_integral_abs_supAuxOccupationTail_sub {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (s : NNReal) : Filter.Tendsto (fun (ε : ℝ) => ∫ (f : Skorokhod.DLoc), |supAuxOccupationTail q ε s f - supAuxDiscountedTail θ q s f| ∂↑(stableLocalLaw θ)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Discounted occupation tails converge to the constructed Stieltjes tail in mean.