Exponential tilting of finite-tree weights

Replacing degree weights p k by a * b ^ k * p k multiplies the weight of a tree with n vertices by a ^ n * b ^ (n - 1). The identity uses only that the sum of the outdegrees is n - 1; no normalization, positivity or finiteness of the weights is needed. The conditioned-law consequence is in BGW.LocallyFinite.Tilting.

theorem BGW.PlaneTree.weight_tilt (p : ℕ → ENNReal) (a b : ENNReal) (t : PlaneTree) : weight (fun (k : ℕ) => a * b ^ k * p k) t = a ^ t.size * b ^ (t.size - 1) * weight p t

Exponential tilting multiplies a tree's weight by a factor depending only on its size. This algebraic identity also allows zero or infinite weights and tilt parameters.