Exact weighted fringe identities

Summing an observable over all fringe occurrences in trees of size n gives the convolution of its tree weight with the mass of a zero-sum walk of the remaining length. The identity is unnormalized, holds for arbitrary nonnegative extended weights, and includes n = 0.

This adapts PoissonDeclumping/Lukasiewicz/Excursion.lean, tsum_sum_weight_mul_fringe (lines 202–215), the weighted form of Corollary cor:cyclicshift in Kortchemski–Vetter (manuscript lines 778–824). The first-tree/suffix decomposition is proved directly on words; no stopping-time framework or measure on finite trees is added.

noncomputable def BGW.PlaneTree.fringeSum (G : PlaneTree → ENNReal) (t : PlaneTree) : ENNReal

Sum an observable over every fringe occurrence, including the root.

Equations

• BGW.PlaneTree.fringeSum G t = (List.map (fun (u : List ℕ) => (t.fringe? u).elim 0 G) t.vertices).sum

theorem BGW.PlaneTree.tsum_weight_fringeSum (p : ℕ → ENNReal) (G : PlaneTree → ENNReal) (n : ℕ) : ∑' (t : { t : PlaneTree // t.size = n }), weight p ↑t * fringeSum G ↑t = ∑' (s : PlaneTree), if s.size ≤ n then weight p s * G s * ∑' (x : List ℤ), (forestBridgeWords 0 (n - s.size)).indicator (walkWeight p) x else 0

Exact weighted fringe convolution. The remainder is a bridge to level zero, and trees larger than n contribute zero. No normalization, criticality or moment hypothesis is used.