Compact uniform convergence of monotone occupation functions

Monotonicity is in time, rather than in the approximation index. Compactness and squeezing at a moving time give uniform convergence to the continuous auxiliary clock.

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

theorem BGW.StableTrees.tendsto_compact_sup_of_monotone {F : ℕ → NNReal → ℝ} {g : NNReal → ℝ} (hm : ∀ (n : ℕ), Monotone (F n)) (hF : ∀ (n : ℕ), Continuous (F n)) (hc : Continuous g) (hp : ∀ (t : NNReal), Filter.Tendsto (fun (n : ℕ) => F n t) Filter.atTop (nhds (g t))) (T : NNReal) : Filter.Tendsto (fun (n : ℕ) => ⨆ (t : ↑(Set.Iic T)), |F n ↑t - g ↑t|) Filter.atTop (nhds 0)

Continuous nondecreasing functions converging pointwise to a continuous function converge uniformly on every compact initial interval.

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

Locally uniform identification for any simultaneous occupation sequence.

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

Locally uniform convergence to the public clock, simultaneously over horizons.