Function sums factor into product of sums

Proved

BookSixth.sum_func_prod_eq_prod_sum

by Tamas Fulop · Sep 16, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatoricsprobabilistic-method

Sums over Boolean-valued functions factor as products of sums. For a finite type $A$ and $F : A \to \\{0,1\\} \to \mathbb{R}$ ,

\sum_{b : A \to \\{0,1\\}} \prod_{e} F_e(b_e) = \prod_e (F_e(0) + F_e(1)).

The proof is induction on the index set, splitting functions by their value at the new point. This is the Fubini step behind every independent-coordinate expectation computation, including the $G(n,p)$ calculations. Formalization Note Lean states both sums over Finset.univ with explicit Finset.sum and Finset.prod.

Preamble

import Mathlib
import Definitions.Def_BookSixthRandomGraph

set_option autoImplicit false

Formal statement

theorem BookSixth.sum_func_prod_eq_prod_sum (A : Type) [DecidableEq A] [Fintype A]
    (F : A -> Bool -> Real) :
    Finset.sum Finset.univ (fun b : A -> Bool => Finset.prod Finset.univ (fun e => F e (b e)))
    = Finset.prod Finset.univ (fun e => (F e true + F e false)) := by sorry

Source

Fubini step for independent-coordinate expectations; cf. Alon--Spencer, The Probabilistic Method, Chapter 1

View graph