Continuity of cutoff prefix densities

Compact endpoint support bounds the Kendall kernel on a compact time/endpoint rectangle. Finite excursion survival measure then gives dominated convergence.

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.excursionTail_density_continuousAt_one {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (b : NNReal) (hb : b ∈ Set.Ioo 0 1) {n : ℕ} (t : Fin n → NNReal) (ht : ∀ (i : Fin n), t i ≤ b) (φ : (Fin n → ℝ) → ℝ) (hφ : Continuous φ) (hφb : ∃ (C : ℝ), ∀ (x : Fin n → ℝ), |φ x| ≤ C) (χ : ℝ → ℝ) (hχ : Continuous χ) (hχc : HasCompactSupport χ) : ContinuousAt (fun (u : ℝ) => ∫ (e : Excursion) in {e : Excursion | ↑b < ↑e.lifetime}, (φ fun (i : Fin n) => ↑e.path (t i)) * χ (↑e.path b) * qKernel θ (u - ↑b) (↑e.path b) ∂excursionMeasure θ) 1

Continuity of cutoff prefix densities at lifetime one.