Full-filter stopped occupation convergence

Uniform second moments follow from the inverse-time energy and exact mean. The energy bound vanishes along the full positive filter; Markov's inequality gives maximal convergence.

References

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

theorem BGW.StableTrees.supOccupation_stopped_L2_bound_aux {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ε : ℝ), 0 < ε → ε ≤ 1 → MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => supOccupation ε f (supAuxLadderTime θ z f) ^ 2) ↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), supOccupation ε f (supAuxLadderTime θ z f) ^ 2 ∂↑(stableLocalLaw θ) ≤ C

Auxiliary form of supOccupation_stopped_L2_bound (A^*, same shape).

theorem BGW.StableTrees.supOccupation_stopped_L2_tendsto_aux {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) : (∀ (ε : ℝ), 0 < ε → ε ≤ 1 → MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => (supOccupation ε f (supAuxLadderTime θ z f) - ↑z) ^ 2) ↑(stableLocalLaw θ)) ∧ Filter.Tendsto (fun (ε : ℝ) => ∫ (f : Skorokhod.DLoc), (supOccupation ε f (supAuxLadderTime θ z f) - ↑z) ^ 2 ∂↑(stableLocalLaw θ)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Auxiliary form of supOccupation_stopped_L2_tendsto.

theorem BGW.StableTrees.supOccupation_stopped_uniform_tendstoInMeasure_aux {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) (δ : ℝ) (hδ : 0 < δ) : Filter.Tendsto (fun (ε : ℝ) => ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | δ ≤ ⨆ (t : ↑(Set.Iic (supAuxLadderTime θ z f))), |supOccupation ε f ↑t - supAuxLocalTime θ f ↑t|}) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Auxiliary form of supOccupation_stopped_uniform_tendstoInMeasure (Markov on the stopped maximal estimate; z = 0 is the same bound).