Adapters between finite stopped cuts and excursion blocks

The continuum cut agrees with the sealed local cut. Removing the last discrete step changes its stopped cut by at most one spatial mesh.

theorem BGW.StableTrees.cutPath_min_apply {g d : NNReal} (hgd : g ≤ d) (f : Skorokhod.DLoc) (t : NNReal) : ↑(cutPath g d f) t = ↑f (min (g + t) d) - ↑f g

The sealed local cut evaluates by clipping the translated time at its right endpoint. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.translatedStoppedCut_restrict {M T g d : NNReal} (f : Skorokhod.DLoc) (hgd : g ≤ d) (hdM : d ≤ M) : translatedStoppedCut T (Skorokhod.DLoc.restrict M f) ⟨↑g, ⋯⟩ ⟨↑d, ⋯⟩ ⋯ = Skorokhod.DLoc.restrict T (cutPath g d f)

Finite stopped cuts of a local restriction agree with the sealed local cut. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.dist_blockIncrements_translatedStoppedCut_le {M : ℝ} (T : NNReal) {ω : ℕ → ℝ} (hω : ∀ (i : ℕ), IsSkipFreeIncrement (ω i)) {r n : ℕ} (hfin : walkHitTime (r + 1) ω ≠ ⊤) (hn : 0 < n) {B : ℝ} (hB : 0 < B) (g d : ↑(Set.Icc 0 M)) (hgd : g ≤ d) (hg : ↑g = ↑(ladderTime ω r) / ↑n) (hd : ↑d = ↑(ladderTime ω (r + 1)) / ↑n) : dist (Skorokhod.realStepPath (↑T) n B (blockIncrements ω r)) (translatedStoppedCut T (Skorokhod.realStepPath M n B ω) g d hgd) ≤ 1 / B

Removing the last skip-free step changes the finite stopped cut by at most 1/B. Reference: Billingsley (1999), Chapter 3.