Degree-product weights of finite plane trees

For p : ℕ → ℝ≥0∞ (in applications, the point masses of an offspring law), the weight of a tree is the product of p over the outdegrees of all its vertices, each occurrence counted. Nothing is assumed about p; in particular it need not be summable to one. For the point masses of an offspring law the total weight of all finite trees is at most one (tsum_weight_le_one), and equality is not claimed here. This follows PoissonDeclumping/Bienayme/Basic.lean.

noncomputable def BGW.PlaneTree.weight (p : ℕ → ENNReal) (t : PlaneTree) : ENNReal

The product of p over the outdegrees of all vertices, with multiplicity.

Equations

• BGW.PlaneTree.weight p t = (List.map p t.degrees).prod

theorem BGW.PlaneTree.weight_node (p : ℕ → ENNReal) (ts : List PlaneTree) : weight p (node ts) = p ts.length * (List.map (weight p) ts).prod

theorem BGW.PlaneTree.weight_node_ofFn (p : ℕ → ENNReal) {k : ℕ} (f : Fin k → PlaneTree) : weight p (node (List.ofFn f)) = p k * ∏ i : Fin k, weight p (f i)

@[simp]

theorem BGW.PlaneTree.weight_leaf (p : ℕ → ENNReal) : weight p leaf = p 0

theorem BGW.PlaneTree.weight_eq_zero_iff (p : ℕ → ENNReal) (t : PlaneTree) : weight p t = 0 ↔ ∃ d ∈ t.degrees, p d = 0

The weight vanishes exactly when some vertex has an outdegree of zero p-mass.

theorem BGW.PlaneTree.weight_ne_zero_iff (p : ℕ → ENNReal) (t : PlaneTree) : weight p t ≠ 0 ↔ ∀ d ∈ t.degrees, p d ≠ 0