Quantitative continuity estimate for moving stopped cuts #
An interior clock preserves every jump. At the two ends only continuity-window estimates enter.
theorem
BGW.StableTrees.dist_translatedStoppedCut_le
{M : ℝ}
(T : NNReal)
(u f : Skorokhod.D M ℝ)
(g d a b : ↑(Set.Icc 0 M))
(hgd : g < d)
(hab : a ≤ b)
(σ : Skorokhod.TimeChange M)
{δ e : ℝ}
(hδ : 0 < δ)
(hsmall : 4 * δ < min (↑g + ↑T) ↑d - ↑g)
(hd : ∀ (t : ↑(Set.Icc 0 M)), |↑(σ t) - ↑t| ≤ δ / 8)
(hp : ∀ (t : ↑(Set.Icc 0 M)), dist (u (σ t)) (f t) ≤ e)
(ha : |↑a - ↑g| ≤ δ / 8)
(hb : |↑b - ↑d| ≤ δ / 8)
(hg : ∀ (s : ↑(Set.Icc 0 M)), |↑s - ↑g| < 5 * δ → dist (f s) (f g) ≤ e)
(hq : ∀ (s : ↑(Set.Icc 0 M)), |↑s - min (↑g + ↑T) ↑d| < 5 * δ → dist (f s) (f ⟨min (↑g + ↑T) ↑d, ⋯⟩) ≤ e)
:
A uniform J1 approximation and continuity windows control moving translated stopped cuts. Reference: Billingsley (1999), Chapter 3.