Forest codes

For ℓ ≥ 1, a forest code is an integer word with all entries at least -1, sum -ℓ, and all proper prefix sums (the empty prefix included) strictly above -ℓ: the first passage to -ℓ happens at the terminal time. Prepending the artificial-root increment ℓ - 1 turns such a word into a tree excursion, so forest codes are exactly the increments of the ordered forests with ℓ components, each forest being determined by its code. The weight of a forest, the product of the weights of its components, is the walk weight of its code.

The rotation of a word of sum -ℓ is a forest code exactly when its starting index is a strict running minimum of the prefix sums that later prefix sums do not undercut by ℓ or more. The generalized cycle lemma follows: a word of length n, entries at least -1 and sum -ℓ has exactly ℓ good rotation indices (indices are counted, not distinct rotated words, so periodic words are covered). Counting the pairs of a bridge word and a good index in two ways gives Kemperman's formula for forests in weight form, n * forestWeight p ℓ n = ℓ * (total walk weight of the words of length n and sum -ℓ), for arbitrary step masses p. Adapted from PoissonDeclumping/Bridge/Kemperman.lean (card_filter_rotate_firstPassageAt, forestMap_bijective, natCast_mul_forestSizeWeight); the forest coding goes through the artificial root and the tree excursion bijection instead of a second parser, and the first-passage convolution is not part of this module.

def BGW.IsForestCode (ℓ : ℕ) (xs : List ℤ) : Prop

Words of steps at least -1 whose first passage to -ℓ is at the terminal time.

Equations

• BGW.IsForestCode ℓ xs = ((∀ x ∈ xs, -1 ≤ x) ∧ xs.sum = -↑ℓ ∧ ∀ i < xs.length, -↑ℓ < (List.take i xs).sum)

theorem BGW.isForestCode_iff_isTreeExcursion_cons {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (xs : List ℤ) : IsForestCode ℓ xs ↔ IsTreeExcursion ((↑ℓ - 1) :: xs)

The artificial root: a forest code with ℓ components is a tree excursion once the increment ℓ - 1 of a root with ℓ children is prepended.

theorem BGW.PlaneForest.increments_injective : Function.Injective increments

A forest is determined by its code.

theorem BGW.PlaneForest.isForestCode_iff_existsUnique {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (xs : List ℤ) : IsForestCode ℓ xs ↔ ∃! ts : PlaneForest, List.length ts = ℓ ∧ ts.increments = xs

Forest codes with ℓ ≥ 1 components are exactly the codes of the unique ordered forests with ℓ components.

theorem BGW.PlaneForest.walkWeight_increments (p : ℕ → ENNReal) (ts : PlaneForest) : walkWeight p ts.increments = (List.map (PlaneTree.weight p) ts).prod

The weight of a forest is the walk weight of its code.

def BGW.forestBridgeWords (ℓ n : ℕ) : Set (List ℤ)

Words of length n with entries at least -1 and sum -ℓ; ℓ = 1 gives bridgeWords n.

Equations

• BGW.forestBridgeWords ℓ n = {x : List ℤ | x.length = n ∧ (∀ a ∈ x, -1 ≤ a) ∧ x.sum = -↑ℓ}

theorem BGW.forestBridgeWords_one (n : ℕ) : forestBridgeWords 1 n = bridgeWords n

theorem BGW.exists_first_sum_take_eq {x : List ℤ} (hx : ∀ a ∈ x, -1 ≤ a) {v : ℤ} (hv : v ≤ 0) {b : ℕ} (hb : (List.take b x).sum ≤ v) : ∃ l ≤ b, (List.take l x).sum = v ∧ ∀ l' < l, v < (List.take l' x).sum

Discrete intermediate value property: if the steps are at least -1, v ≤ 0 and some prefix sum is at most v, then v is attained at a first time, all earlier prefix sums being above v. Adapted from PoissonDeclumping/Bridge/Kemperman.lean.

theorem BGW.isForestCode_rotate_iff {x : List ℤ} {ℓ : ℕ} (hge : ∀ a ∈ x, -1 ≤ a) (hs : x.sum = -↑ℓ) {i : ℕ} (hi : i < x.length) : IsForestCode ℓ (x.rotate i) ↔ (∀ (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 rotation of a word of sum -ℓ by i < n is a forest code iff i is a strict running minimum of the prefix sums that later prefix sums (before time n) do not undercut by ℓ.

theorem BGW.ncard_rotate_isForestCode {x : List ℤ} (hx : ∀ a ∈ x, -1 ≤ a) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (hs : x.sum = -↑ℓ) : {i : ℕ | i < x.length ∧ IsForestCode ℓ (x.rotate i)}.ncard = ℓ

Generalized cycle lemma. A word of length n, entries at least -1 and sum -ℓ with ℓ ≥ 1 has exactly ℓ indices i < n whose left rotation is a forest code. Indices are counted, not distinct rotated words, so periodic words are covered: [-1, -1] has two good indices.

noncomputable def BGW.forestWeight (p : ℕ → ENNReal) (ℓ n : ℕ) : ENNReal

Total weight of the ordered forests of ℓ trees with n vertices in total.

Equations

• BGW.forestWeight p ℓ n = ∑' (ts : BGW.PlaneForest), if List.length ts = ℓ ∧ ts.size = n then (List.map (BGW.PlaneTree.weight p) ts).prod else 0

theorem BGW.forestWeight_eq_tsum_codes (p : ℕ → ENNReal) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (n : ℕ) : forestWeight p ℓ n = ∑' (x : List ℤ), {x : List ℤ | IsForestCode ℓ x ∧ x.length = n}.indicator (walkWeight p) x

The weights of forests reindexed by their codes.

theorem BGW.natCast_mul_forestWeight (p : ℕ → ENNReal) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (n : ℕ) : ↑n * forestWeight p ℓ n = ↑ℓ * ∑' (x : List ℤ), (forestBridgeWords ℓ n).indicator (walkWeight p) x

Kemperman's formula for forests, in weight form. For every p : ℕ → ℝ≥0∞, ℓ ≥ 1 and n: n times the total weight of the ordered forests of ℓ trees with n vertices is ℓ times the total walk weight of the words of length n, entries at least -1 and sum -ℓ.

theorem BGW.PlaneForest.length_le_size (ts : PlaneForest) : List.length ts ≤ ts.size

theorem BGW.forestWeight_eq_zero_of_lt (p : ℕ → ENNReal) {ℓ n : ℕ} (h : n < ℓ) : forestWeight p ℓ n = 0

Fewer vertices than components: no forest.