Stopped-cut convergence for the first long block

Endpoint convergence and joint continuity of moving stopped cuts identify the extracted path. The modification of the last step costs at most one spatial mesh.

theorem BGW.StableTrees.tendsto_firstLongBlock_cut {B : ℕ → ℝ} (hB : Filter.Tendsto B Filter.atTop Filter.atTop) {M T : NNReal} (ω : ℕ → ℕ → ℝ) (hω : ∀ (n i : ℕ), IsSkipFreeIncrement (ω n i)) {f : Skorokhod.DLoc} (hf : GoodLongExtractionCutPath M T f) (hu : Filter.Tendsto (fun (n : ℕ) => Skorokhod.realStepPath (↑M) n (B n) (ω n)) Filter.atTop (nhds (Skorokhod.DLoc.restrict M f))) : Filter.Tendsto (fun (n : ℕ) => extractionTriple (B n) n T (ω n)) Filter.atTop (nhds (longCutTriple T f))

Stopped-cut convergence: the whole triple (g_n, d_n, cut_n) converges, in ℝ × ℝ × D T ℝ, for every cutoff T at which the limit cut is continuous. The cut is the translated block path, extended by zero.