Matching a compact excursion interior to a discrete block #
Absence of ladder hits in an interval forces that interval into one consecutive ladder block.
The level-zero ladder time is always zero. Reference: Billingsley (1999), Chapter 3.
theorem
BGW.StableTrees.exists_ladderBlock_spanning
{ω : ℕ → ℝ}
{n R : ℕ}
{a b : ℝ}
(ha : 0 < a)
(hab : a ≤ b)
(hfin : walkHitTime R ω ≠ ⊤)
(hR : b < ↑(ladderTime ω R) / ↑n)
(havoid : ∀ s ≤ R, ¬(a ≤ ↑(ladderTime ω s) / ↑n ∧ ↑(ladderTime ω s) / ↑n ≤ b))
:
∃ r < R,
walkHitTime (r + 1) ω ≠ ⊤ ∧ ↑(ladderTime ω r) / ↑n < a ∧ b < ↑(ladderTime ω (r + 1)) / ↑n ∧ ∀ s ≤ R, ↑(ladderTime ω s) / ↑n < a → s ≤ r
An interval avoiding all ladder hits lies in one finite consecutive ladder block. Reference: Billingsley (1999), Chapter 3.
theorem
BGW.StableTrees.eventually_longBlockSet_nonempty
{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)))
:
∀ᶠ (n : ℕ) in Filter.atTop, (longBlockSet n (ω n)).Nonempty
A good long excursion forces the discrete walk to have a long block eventually. Reference: Billingsley (1999), Chapter 3.