Joint continuity of moving translated stopped cuts #
J1 clocks are preserved in the interior. Continuity at the initial and observed terminal source times controls the affine clock corrections.
theorem
BGW.StableTrees.tendsto_translatedStoppedCut
{M : ℝ}
(T : NNReal)
{u : ℕ → Skorokhod.D M ℝ}
{f : Skorokhod.D M ℝ}
(hu : Filter.Tendsto u Filter.atTop (nhds f))
(a b : ℕ → ↑(Set.Icc 0 M))
(hab : ∀ (n : ℕ), a n ≤ b n)
{g d : ↑(Set.Icc 0 M)}
(hgd : g < d)
(ha : Filter.Tendsto (fun (n : ℕ) => ↑(a n)) Filter.atTop (nhds ↑g))
(hb : Filter.Tendsto (fun (n : ℕ) => ↑(b n)) Filter.atTop (nhds ↑d))
(hg : ContinuousAt (⇑f) g)
(hd : ContinuousAt (⇑f) d)
(hc : ContinuousAt ⇑(translatedStoppedCut T f g d ⋯) ⟨↑T, ⋯⟩)
:
Filter.Tendsto (fun (n : ℕ) => translatedStoppedCut T (u n) (a n) (b n) ⋯) Filter.atTop
(nhds (translatedStoppedCut T f g d ⋯))
Joint J1 continuity of translated stopped cuts with moving endpoints, at continuous cutoffs. Reference: Billingsley (1999), Chapter 3.