Deterministic ladder-time estimates for long-block extraction

Strict barriers transfer to weak walk hits under J1 time changes.

theorem BGW.StableTrees.ladderTime_le_of_stepPath_le {M b : ℝ} {n r : ℕ} {ω : ℕ → ℝ} (hn : 0 < n) (hb : 0 < b) (t : ↑(Set.Icc 0 M)) (ht : (Skorokhod.realStepPath M n b ω) t ≤ -↑r / b) : walkHitTime r ω ≠ ⊤ ∧ ↑(ladderTime ω r) / ↑n ≤ ↑t

A walk value below the barrier bounds the finite ladder time. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.partialSum_ladderTime_le {r : ℕ} {ω : ℕ → ℝ} (hfin : walkHitTime r ω ≠ ⊤) : Probability.RealWalk.partialSum ω (ladderTime ω r) ≤ -↑r

A finite ladder time attains its weak barrier. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.exists_lower_passage_barrier {M : NNReal} {f : Skorokhod.DLoc} (hf : GoodLongExtractionPath M f) {x t : NNReal} (hx : x ∉ passageJumpSet f) (ht : t < passageTime x f) : ∃ y < x, t < passageTime y f

Before passage at a non-jump positive level, a smaller barrier still has not been hit. Reference: Billingsley (1999), Chapter 3.