The cycle lemma for Łukasiewicz bridges

A bridge word of length n has entries at least -1 and sum -1. Writing S j for its prefix sums, the rotation by i < n is a tree excursion exactly when i is the first index in [0, n) at which S attains its minimum. Hence every bridge word has exactly one rotation that is a tree excursion, and (t, i) ↦ (increments t).rotate i is a bijection from the pairs of a tree of size n and an index i < n onto the bridge words of length n. Since rotating a word permutes its entries, the walk weight is rotation invariant, and n times the total weight of the trees of size n is the total walk weight of the bridge words. Adapted from PoissonDeclumping/Lukasiewicz/CyclicShift.lean, with the library's prefix-sum excursions.

def BGW.bridgeWords (n : ℕ) : Set (List ℤ)

Words of length n with all entries at least -1 and total sum -1.

Equations

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

theorem BGW.sum_take_rotate (x : List ℤ) {i k : ℕ} (hi : i ≤ x.length) (hk : k ≤ x.length) : (List.take k (x.rotate i)).sum = if k ≤ x.length - i then (List.take (i + k) x).sum - (List.take i x).sum else x.sum - (List.take i x).sum + (List.take (k - (x.length - i)) x).sum

Prefix sums of a rotation, in terms of prefix sums of the original word.

theorem BGW.exists_unique_rotate_isTreeExcursion {x : List ℤ} {n : ℕ} (hx : x ∈ bridgeWords n) : ∃! i : ℕ, i < n ∧ IsTreeExcursion (x.rotate i)

A bridge word has exactly one rotation, by an index below its length, that is a tree excursion: the cycle lemma.

theorem BGW.walkWeight_rotate (p : ℕ → ENNReal) (x : List ℤ) (i : ℕ) : walkWeight p (x.rotate i) = walkWeight p x

Rotating a word permutes its entries, so the walk weight is unchanged.

theorem BGW.PlaneTree.increments_mem_bridgeWords (t : PlaneTree) : t.increments ∈ bridgeWords t.size

def BGW.PlaneTree.shiftMap (n : ℕ) (q : { t : PlaneTree // t.size = n } × Fin n) : ↑(bridgeWords n)

Cyclic shifts of the codes of trees with n vertices.

Equations

• BGW.PlaneTree.shiftMap n q = ⟨(↑q.1).increments.rotate ↑q.2, ⋯⟩

theorem BGW.PlaneTree.shiftMap_injective (n : ℕ) : Function.Injective (shiftMap n)

theorem BGW.PlaneTree.shiftMap_surjective (n : ℕ) : Function.Surjective (shiftMap n)

noncomputable def BGW.PlaneTree.shiftEquiv (n : ℕ) : { t : PlaneTree // t.size = n } × Fin n ≃ ↑(bridgeWords n)

The cycle lemma as an equivalence.

Equations

• BGW.PlaneTree.shiftEquiv n = Equiv.ofBijective (BGW.PlaneTree.shiftMap n) ⋯

theorem BGW.PlaneTree.natCast_mul_tsum_weight_size (p : ℕ → ENNReal) (n : ℕ) : (↑n * ∑' (t : PlaneTree), if t.size = n then weight p t else 0) = ∑' (x : List ℤ), (bridgeWords n).indicator (walkWeight p) x

Kemperman–Dwass identity in weight form: n times the total weight of the trees of size n is the total walk weight of the bridge words of length n. No hypothesis on p.