Exact skip-free ladder blocks

Finite weak hits of integer barriers are exact. Consecutive hits delimit nonnegative blocks.

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

Before a finite weak hit, the walk is strictly above its barrier. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.ladderTime_mono_of_finite {ω : ℕ → ℝ} {r s : ℕ} (hrs : r ≤ s) (hs : walkHitTime s ω ≠ ⊤) : walkHitTime r ω ≠ ⊤ ∧ ladderTime ω r ≤ ladderTime ω s

A finite higher hit makes every lower hit finite and orders the finite readings. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.partialSum_ladderTime_eq {ω : ℕ → ℝ} (hω : ∀ (i : ℕ), IsSkipFreeIncrement (ω i)) {r : ℕ} (hfin : walkHitTime r ω ≠ ⊤) : Probability.RealWalk.partialSum ω (ladderTime ω r) = -↑r

A finite hit of an integer barrier by a skip-free walk attains the barrier exactly. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.ladderTime_lt_succ {ω : ℕ → ℝ} (hω : ∀ (i : ℕ), IsSkipFreeIncrement (ω i)) {r : ℕ} (hfin : walkHitTime (r + 1) ω ≠ ⊤) : ladderTime ω r < ladderTime ω (r + 1)

Consecutive finite skip-free ladder times are strictly increasing. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.partialSum_blockIncrements (ω : ℕ → ℝ) (r i : ℕ) : Probability.RealWalk.partialSum (blockIncrements ω r) i = Probability.RealWalk.partialSum ω (ladderTime ω r + min i (ladderTime ω (r + 1) - ladderTime ω r - 1)) - Probability.RealWalk.partialSum ω (ladderTime ω r)

Partial sums of the modified block stop just before the final downward step. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.partialSum_blockIncrements_eq_zero {ω : ℕ → ℝ} (hω : ∀ (i : ℕ), IsSkipFreeIncrement (ω i)) {r : ℕ} (hfin : walkHitTime (r + 1) ω ≠ ⊤) {i : ℕ} (hi : ladderTime ω (r + 1) - ladderTime ω r - 1 ≤ i) : Probability.RealWalk.partialSum (blockIncrements ω r) i = 0

The extracted block is identically zero after its final step has been removed. Reference: Billingsley (1999), Chapter 3.