First passage times of integer sequences and the cycle lemma

Section 2.1 of the paper (source lines 685–690) defines, for a sequence 𝐱 = (x_i)_{i ≥ 1} of integers, the first passage time ζ(𝐱) = inf {k ≥ 1 : x_1 + ⋯ + x_k = -1}, with inf ∅ = +∞; for a finite sequence it is defined in the same way (the index k ranging over the available positions). Here a finite sequence is a List ℤ and +∞ is none.

We also prove the cycle lemma (the combinatorial core of eq:shifts, source lines 718–730): a sequence of n ≥ 1 integers that are all ≥ -1 and sum to -1 has exactly one cyclic shift whose first passage time to -1 is n.

noncomputable def PoissonDeclumping.Lukasiewicz.zeta (x : List ℤ) : Option ℕ

The first passage time ζ(𝐱) of a finite integer sequence to -1: the least k ≥ 1 (with k ≤ x.length) such that x_1 + ⋯ + x_k = -1, and none (the paper's +∞) if there is no such k.

Equations

• PoissonDeclumping.Lukasiewicz.zeta x = if h : ∃ (k : ℕ), 1 ≤ k ∧ k ≤ x.length ∧ (List.take k x).sum = -1 then some (Nat.find h) else none

theorem PoissonDeclumping.Lukasiewicz.zeta_eq_some_iff {x : List ℤ} {m : ℕ} : zeta x = some m ↔ 1 ≤ m ∧ m ≤ x.length ∧ (List.take m x).sum = -1 ∧ ∀ (j : ℕ), 1 ≤ j → j < m → (List.take j x).sum ≠ -1

Characterization of ζ(𝐱) = m.

theorem PoissonDeclumping.Lukasiewicz.zeta_eq_none_iff {x : List ℤ} : zeta x = none ↔ ∀ (k : ℕ), 1 ≤ k → k ≤ x.length → (List.take k x).sum ≠ -1

ζ(𝐱) = +∞ exactly when no partial sum x_1 + ⋯ + x_k, 1 ≤ k ≤ length, equals -1.

theorem PoissonDeclumping.Lukasiewicz.sum_take_nonneg_of_ne {x : List ℤ} (hx : ∀ a ∈ x, -1 ≤ a) {m : ℕ} (h : ∀ (j : ℕ), 1 ≤ j → j < m → (List.take j x).sum ≠ -1) (j : ℕ) : j < m → 0 ≤ (List.take j x).sum

Skip-freeness: for a sequence with increments ≥ -1, if the partial sums of indices 1 ≤ j < m avoid -1, then all partial sums of indices j < m are nonnegative.

theorem PoissonDeclumping.Lukasiewicz.zeta_eq_length_iff {y : List ℤ} (hy : ∀ a ∈ y, -1 ≤ a) (hn : 1 ≤ y.length) (hs : y.sum = -1) : zeta y = some y.length ↔ ∀ j < y.length, 0 ≤ (List.take j y).sum

If all proper partial sums are nonnegative, then the first passage to -1 is at the end.

theorem PoissonDeclumping.Lukasiewicz.neg_length_le_sum {l : List ℤ} (hl : ∀ a ∈ l, -1 ≤ a) : -↑l.length ≤ l.sum

A sequence with increments ≥ -1 has partial sums ≥ -length.

theorem PoissonDeclumping.Lukasiewicz.sum_take_rotate_of_le {x : List ℤ} {i j : ℕ} (hi : i ≤ x.length) (hj : j ≤ x.length - i) : (List.take j (x.rotate i)).sum = (List.take (i + j) x).sum - (List.take i x).sum

The partial sums of the cyclic shift x.rotate i before the wrap-around point.

theorem PoissonDeclumping.Lukasiewicz.sum_take_rotate_of_ge {x : List ℤ} {i j : ℕ} (hi : i ≤ x.length) (hj : j ≤ i) : (List.take (x.length - i + j) (x.rotate i)).sum = x.sum - (List.take i x).sum + (List.take j x).sum

The partial sums of the cyclic shift x.rotate i after the wrap-around point.

theorem PoissonDeclumping.Lukasiewicz.rotate_partial_sums_nonneg_iff {x : List ℤ} (hs : x.sum = -1) {i : ℕ} (hi : i < x.length) : (∀ j < x.length, 0 ≤ (List.take j (x.rotate i)).sum) ↔ (∀ (l : ℕ), i ≤ l → l < x.length → (List.take i x).sum ≤ (List.take l x).sum) ∧ ∀ l < i, (List.take i x).sum < (List.take l x).sum

The partial sums of a cyclic shift are nonnegative before time n exactly when the rotation index is the first minimum of the partial sums S_0, …, S_{n-1}.

theorem PoissonDeclumping.Lukasiewicz.existsUnique_zeta_rotate_eq_length {x : List ℤ} (hx : ∀ a ∈ x, -1 ≤ a) (hn : 1 ≤ x.length) (hs : x.sum = -1) : ∃! i : ℕ, i < x.length ∧ zeta (x.rotate i) = some x.length

Cycle lemma. A sequence of n ≥ 1 integers, all ≥ -1, with sum -1, has exactly one cyclic shift x.rotate i (0 ≤ i < n) whose first passage time to -1 is n.