Bracketing a matching long block #
Absence of ladder hits in an interval forces that interval into one consecutive ladder block.
theorem
BGW.StableTrees.eventually_exists_longBlock_near_firstLong
{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)))
{ε : ℝ}
(hε : 0 < ε)
:
∀ᶠ (n : ℕ) in Filter.atTop, ∃ r ∈ longBlockSet n (ω n),
(firstLongEnds f).1 - ε < ↑(ladderTime (ω n) r) / ↑n ∧ ↑(ladderTime (ω n) r) / ↑n < (firstLongEnds f).1 + ε ∧ (firstLongEnds f).2 - ε < ↑(ladderTime (ω n) (r + 1)) / ↑n ∧ ↑(ladderTime (ω n) (r + 1)) / ↑n < (firstLongEnds f).2 + ε
A discrete long block has endpoints arbitrarily close to the selected continuum interval. Reference: Billingsley (1999), Chapter 3.