Time-change bounds for deterministic extraction #
The uniform errors in the J1 convergence criterion control every time, including moving times.
theorem
BGW.StableTrees.tendsto_extraction_clock
{M : ℝ}
(hM : 0 ≤ M)
{σ : ℕ → Skorokhod.TimeChange M}
(hσ : Filter.Tendsto (fun (n : ℕ) => ⨆ (t : ↑(Set.Icc 0 M)), |↑((σ n) t) - ↑t|) Filter.atTop (nhds 0))
(t : ↑(Set.Icc 0 M))
:
Filter.Tendsto (fun (n : ℕ) => ↑((σ n) t)) Filter.atTop (nhds ↑t)
Vanishing clock displacement gives convergence at every fixed time. Reference: Billingsley (1999), Chapter 3.
theorem
BGW.StableTrees.eventually_extraction_error_lt
{M : ℝ}
{u : ℕ → Skorokhod.D M ℝ}
{f : Skorokhod.D M ℝ}
{σ : ℕ → Skorokhod.TimeChange M}
(hu : Filter.Tendsto (fun (n : ℕ) => ⨆ (t : ↑(Set.Icc 0 M)), dist ((u n) ((σ n) t)) (f t)) Filter.atTop (nhds 0))
{ε : ℝ}
(hε : 0 < ε)
:
Vanishing uniform path error bounds the error simultaneously at all times. Reference: Billingsley (1999), Chapter 3.
theorem
BGW.StableTrees.tendsto_extraction_aligned_eval
{M : ℝ}
{u : ℕ → Skorokhod.D M ℝ}
{f : Skorokhod.D M ℝ}
{σ : ℕ → Skorokhod.TimeChange M}
(hu : Filter.Tendsto (fun (n : ℕ) => ⨆ (t : ↑(Set.Icc 0 M)), dist ((u n) ((σ n) t)) (f t)) Filter.atTop (nhds 0))
(t : ↑(Set.Icc 0 M))
:
Filter.Tendsto (fun (n : ℕ) => (u n) ((σ n) t)) Filter.atTop (nhds (f t))
Aligned path evaluations converge even at jumps of the limit. Reference: Billingsley (1999), Chapter 3.