Finite product averaging

Product-of-sums identities and their first and second moments hold for extended nonnegative coefficients.

theorem LiebThirring.Assembly.sum_product_weights {ι : Type u_1} {β : Type u_2} [Fintype ι] [Fintype β] [DecidableEq ι] (w : ι → β → ENNReal) (hw : ∀ (i : ι), ∑ b : β, w i b = 1) : ∑ v : ι → β, ∏ i : ι, w i (v i) = 1

theorem LiebThirring.Assembly.sum_product_weights_mul_product {ι : Type u_1} {β : Type u_2} [Fintype ι] [Fintype β] [DecidableEq ι] (w c : ι → β → ENNReal) : ∑ v : ι → β, (∏ i : ι, w i (v i)) * ∏ i : ι, c i (v i) = ∏ i : ι, ∑ b : β, w i b * c i b

theorem LiebThirring.Assembly.sum_product_weights_first {ι : Type u_1} {β : Type u_2} [Fintype ι] [Fintype β] [DecidableEq ι] (w c : ι → β → ENNReal) (hw : ∀ (i : ι), ∑ b : β, w i b = 1) (k : ι) : ∑ v : ι → β, (∏ i : ι, w i (v i)) * c k (v k) = ∑ b : β, w k b * c k b

theorem LiebThirring.Assembly.sum_product_weights_second {ι : Type u_1} {β : Type u_2} [Fintype ι] [Fintype β] [DecidableEq ι] (w c : ι → β → ENNReal) (hw : ∀ (i : ι), ∑ b : β, w i b = 1) (k l : ι) (hkl : k ≠ l) : ∑ v : ι → β, (∏ i : ι, w i (v i)) * (c k (v k) * c l (v l)) = (∑ b : β, w k b * c k b) * ∑ b : β, w l b * c l b