Excursion interiors contain no discrete ladder times #
A positive lower bound on the reflected limit, together with a uniform aligned path bound, excludes weak record times throughout a compact excursion interior.
theorem
BGW.StableTrees.stepPath_ge_at_ladderTime
{M b : ℝ}
{n r : ℕ}
{ω : ℕ → ℝ}
(hb : 0 < b)
(hfin : walkHitTime r ω ≠ ⊤)
(s : ↑(Set.Icc 0 M))
(hs : ↑n * ↑s ≤ ↑(ladderTime ω r))
:
Every value up to a finite ladder time is at least the value at that time. Reference: Billingsley (1999), Chapter 3.
theorem
BGW.StableTrees.ladderTime_not_mem_aligned_interior
{M : NNReal}
{f : Skorokhod.DLoc}
(hzero : ↑f 0 = 0)
{a b : NNReal}
(haM : a ≤ M)
(hbM : b ≤ M)
{c : ℝ}
(hc : 0 < c)
(hR : ∀ (t : NNReal), a ≤ t → t ≤ b → c ≤ ↑(reflectedFrom 0 f) t)
{n : ℕ}
(hn : 0 < n)
{B : ℝ}
(hB : 0 < B)
{ω : ℕ → ℝ}
(σ : Skorokhod.TimeChange ↑M)
(herr :
∀ (t : ↑(Set.Icc 0 ↑M)), dist ((Skorokhod.realStepPath (↑M) n B ω) (σ t)) ((Skorokhod.DLoc.restrict M f) t) < c / 4)
{r : ℕ}
(hfin : walkHitTime r ω ≠ ⊤)
:
A compact reflected-positive interval has no aligned discrete record times. Reference: Billingsley (1999), Chapter 3.