Identification for arbitrary simultaneous occupation sequences

A subsequence of any admissible sequence can be paired with the fast auxiliary sequence. The uniform second-moment bounds and Borel–Cantelli identify all finite-time limits on one common event, using the sequence's simultaneous convergence hypothesis.

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

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

Every simultaneous occupation sequence has the same all-time limit as the auxiliary clock.

theorem BGW.StableTrees.ae_supLocalTime_eq_aux {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), supLocalTime θ f t = supAuxLocalTime θ f t

The public and auxiliary clocks agree at every time on one full-measure event.

theorem BGW.StableTrees.ae_supLocalTimeENN_eq_aux {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), supLocalTimeENN θ f t = ENNReal.ofReal (supAuxLocalTime θ f t)

The extended public clock agrees with the finite auxiliary clock simultaneously.