Endpoints of the first long block

A matching long block is the first long block: any preceding long block would end too early.

theorem BGW.StableTrees.tendsto_firstLongBlock_endpoints {B : ℕ → ℝ} (hB : Filter.Tendsto B Filter.atTop Filter.atTop) {M : NNReal} (ω : ℕ → ℕ → ℝ) (hω : ∀ (n i : ℕ), IsSkipFreeIncrement (ω n i)) {f : Skorokhod.DLoc} (hf : GoodLongExtractionPath M 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 : ℕ) => extractionEndpoints n (ω n)) Filter.atTop (nhds (firstLongEnds f))

Endpoint matching (finding 1): the first long block's endpoints converge to the selected excursion interval (T_{L-}, T_L). No convergence of extraction is assumed.