First-passage decomposition of forest bridge words

For ℓ ≥ 1, a word of length N, entries at least -1 and sum -ℓ has a first time q ≤ N at which its prefix sum equals -ℓ. Its prefix of length q is then a forest code, and the remaining suffix is a word of length N - q, entries at least -1 and sum 0. Conversely a forest code followed by such a suffix is a word of length N with sum -ℓ, and q is recovered as the length of the code (the first passage time is unique). Since the walk weight is multiplicative under concatenation, this gives, for arbitrary step masses p and every N,

∑ weight(forestBridgeWords ℓ N) = ∑_{q ≤ N} forestWeight p ℓ q * ∑ weight(forestBridgeWords 0 (N - q))

(tsum_forestBridgeWords_eq_sum). The suffixes are the words of forestBridgeWords 0 (N - q), the bridges back to level 0. No criticality, positivity or lattice hypothesis is used. Adapted from PoissonDeclumping/Bridge/Kemperman.lean (firstPassageAt_take_unique, walkMass_neg_eq_sum); the measure statement is in BGW.LocallyFinite.FirstPassageLaw.

theorem BGW.walkWeight_append (p : ℕ → ENNReal) (a b : List ℤ) : walkWeight p (a ++ b) = walkWeight p a * walkWeight p b

The walk weight is multiplicative under concatenation.

theorem BGW.length_eq_of_isForestCode_take {x : List ℤ} {ℓ q q' : ℕ} (hq : q ≤ x.length) (hq' : q' ≤ x.length) (h : IsForestCode ℓ (List.take q x)) (h' : IsForestCode ℓ (List.take q' x)) : q = q'

The first passage time to -ℓ is unique: two prefixes of a word that are forest codes have the same length.

def BGW.firstPassageWords (ℓ N q : ℕ) : Set (List ℤ)

A word of length N, entries at least -1 and sum -ℓ (ℓ ≥ 0) whose prefix of length q is a forest code: the words cut at the first passage time q.

Equations

• BGW.firstPassageWords ℓ N q = {x : List ℤ | x ∈ BGW.forestBridgeWords ℓ N ∧ q ≤ N ∧ BGW.IsForestCode ℓ (List.take q x)}

theorem BGW.mem_firstPassageWords_iff {ℓ N q : ℕ} (hq : q ≤ N) (x : List ℤ) : x ∈ firstPassageWords ℓ N q ↔ (IsForestCode ℓ (List.take q x) ∧ (List.take q x).length = q) ∧ List.drop q x ∈ forestBridgeWords 0 (N - q)

Cutting a word at q is the same as a forest code of length q followed by a bridge of length N - q at level 0.

theorem BGW.sum_indicator_firstPassageWords {ℓ N : ℕ} (F : List ℤ → ENNReal) (x : List ℤ) : ∑ q ∈ Finset.range (N + 1), (firstPassageWords ℓ N q).indicator F x = (forestBridgeWords ℓ N).indicator F x

The sets firstPassageWords ℓ N q, q ≤ N, partition the words of forestBridgeWords ℓ N (1 ≤ ℓ is not needed: for ℓ = 0 the cut is at q = 0).

theorem BGW.tsum_firstPassageWords_walkWeight (p : ℕ → ENNReal) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) {N q : ℕ} (hq : q ≤ N) : ∑' (x : List ℤ), (firstPassageWords ℓ N q).indicator (walkWeight p) x = forestWeight p ℓ q * ∑' (x : List ℤ), (forestBridgeWords 0 (N - q)).indicator (walkWeight p) x

The total walk weight of the words cut at q factors as forest codes times bridges at level 0.

theorem BGW.tsum_forestBridgeWords_eq_sum (p : ℕ → ENNReal) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (N : ℕ) : ∑' (x : List ℤ), (forestBridgeWords ℓ N).indicator (walkWeight p) x = ∑ q ∈ Finset.range (N + 1), forestWeight p ℓ q * ∑' (x : List ℤ), (forestBridgeWords 0 (N - q)).indicator (walkWeight p) x

First-passage decomposition of the walk weights. For 1 ≤ ℓ, every N and every p : ℕ → ℝ≥0∞, the total weight of the words of length N, entries at least -1 and sum -ℓ is the sum over the first passage time q ≤ N of forestWeight p ℓ q times the total weight of the words of length N - q, entries at least -1 and sum 0.