Finite-dimensional continuity of the scaled unit law

At a good time, càdlàg paths are continuous. Exact excursion scaling and bounded convergence give continuity of bounded continuous cylinder tests at lifetime one.

References

• L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.

theorem BGW.StableTrees.excursionAt_finiteDim_continuousAt_one {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {n : ℕ} (t : Fin n → NNReal) (ht : ∀ (i : Fin n), t i ≤ 1) (hgood : ∀ (i : Fin n), NoFixedJumpUnit θ (t i)) (φ : (Fin n → ℝ) → ℝ) (hφ : Continuous φ) (hφb : ∃ (C : ℝ), ∀ (x : Fin n → ℝ), |φ x| ≤ C) : ContinuousAt (fun (u : ↑(Set.Ioi 0)) => ∫ (e : Excursion), φ fun (i : Fin n) => ↑e.path (t i) ∂excursionAt θ u) ⟨1, ⋯⟩

Continuity of finite-dimensional tests under scaling at lifetime one.