Walk weights of Łukasiewicz words

For step masses p : ℕ → ℝ≥0∞, the weight of an integer word x₁, …, xₙ with all xᵢ ≥ -1 is ∏ p (xᵢ + 1): the steps are k - 1 for an offspring count k. The weight of a finite plane tree is the walk weight of its increments (walkWeight_increments), and the total weight of the trees of size n is the total walk weight of the tree excursions of length n (tsum_weight_size_eq_tsum_excursions). No assumption is made on p. Adapted from PoissonDeclumping/Lukasiewicz/Excursion.lean (walkWeight, weight_eq_walkWeight), where p is a probability mass function and the excursions are defined through a first-passage time.

noncomputable def BGW.walkWeight (p : ℕ → ENNReal) (xs : List ℤ) : ENNReal

The product of p (x + 1) over the entries of a word of steps x ≥ -1. An entry below -1 would silently contribute p 0; such words are never used, since excursions have all entries at least -1.

Equations

• BGW.walkWeight p xs = (List.map (fun (a : ℤ) => p (a + 1).toNat) xs).prod

theorem BGW.PlaneTree.walkWeight_increments (p : ℕ → ENNReal) (t : PlaneTree) : walkWeight p t.increments = weight p t

The weight of a tree is the walk weight of its Łukasiewicz increments.

theorem BGW.PlaneTree.tsum_weight_size_eq_tsum_excursions (p : ℕ → ENNReal) (n : ℕ) : (∑' (t : PlaneTree), if t.size = n then weight p t else 0) = ∑' (x : List ℤ), {x : List ℤ | IsTreeExcursion x ∧ x.length = n}.indicator (walkWeight p) x

Total weight of the trees of size n as a total walk weight of the excursions of length n.