Almost sure compact convergence of the fast occupation sequence

Chebyshev and Borel–Cantelli give summable adjacent errors on growing integer horizons. Completeness of continuous functions on each compact then identifies the raw real limsup.

References

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

theorem BGW.StableTrees.abs_sub_supOccupation_le_compactError {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) (T : NNReal) (f : Skorokhod.DLoc) (t : ↑(Set.Iic T)) : |supOccupation ε f ↑t - supOccupation η f ↑t| ≤ compactError ε η T f

Each pointwise error is bounded by its compact supremum.

theorem BGW.StableTrees.ae_eventually_compactError_supAuxEps_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ᶠ (k : ℕ) in Filter.atTop, compactError (supAuxEps θ k) (supAuxEps θ (k + 1)) (↑k) f ≤ (1 / 2) ^ k

Chebyshev and Borel–Cantelli give eventual geometric adjacent compact errors.

theorem BGW.StableTrees.ae_tendsto_supOccupation_supAuxEps_uniform {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (T : NNReal), Filter.Tendsto (fun (k : ℕ) => ⨆ (t : ↑(Set.Iic T)), |supOccupation (supAuxEps θ k) f ↑t - supAuxLimit θ f ↑t|) Filter.atTop (nhds 0)

A.s. locally uniform convergence along the fast subsequence, for all T simultaneously (Borel–Cantelli on integer horizons).

theorem BGW.StableTrees.ae_supAuxLimit_spec {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), supAuxLimit θ f 0 = 0 ∧ Monotone (supAuxLimit θ f) ∧ Continuous (supAuxLimit θ f)

M^*_0 = 0, nondecreasing and continuous, almost surely (uniform limit of continuous nondecreasing occupations).