Sums of products of affine forms over the Boolean cube

Let R be a commutative 𝔽₂-algebra. For affine forms Lₚ(c) = aₚ + ∑ᵥ cᵥ • bₚᵥ in Boolean variables c : κ → 𝔽₂, the sum of ∏ₚ Lₚ(c) over the whole cube is the |κ|-th mixed finite difference of the product. Expanding the product, a monomial survives the summation exactly when it involves every variable, since a missing variable doubles its contribution. Hence the sum is a sum over the assignments ℓ : P → Option κ of factors to variables (or to their constant term) that cover every variable.

Two consequences are used for affine dispersers. If every covering assignment meets a vanishing coefficient, the sum is zero. If there are as many factors as variables, the covering assignments are the bijections, and the sum is the permanent of the coefficient matrix.

Main results

• Cslib.sum_cube_prod_affine: the expansion over covering assignments.
• Cslib.sum_cube_prod_affine_eq_zero: vanishing when every covering assignment meets a zero coefficient.
• Cslib.sum_cube_prod_affine_eq_permanent: with as many factors as variables, the sum is the permanent of the coefficient matrix.

References

• E. Ben-Sasson, S. Kopparty, Affine dispersers from subspace polynomials

theorem Cslib.sum_cube_prod_affine {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] {κ : Type u_2} {P : Type u_3} [Fintype κ] [DecidableEq κ] [Fintype P] [DecidableEq P] (a : P → R) (b : P → κ → R) : ∑ c : κ → ZMod 2, ∏ p : P, (a p + ∑ v : κ, c v • b p v) = ∑ ℓ : P → Option κ with ∀ (v : κ), ∃ (p : P), ℓ p = some v, ∏ p : P, (ℓ p).elim (a p) (b p)

Cube sum of a product of affine forms: summing ∏ₚ (aₚ + ∑ᵥ cᵥ • bₚᵥ) over the Boolean cube leaves the assignments ℓ of factors to variables, or to the constant term (none), that cover every variable; each contributes the product of the chosen coefficients.

theorem Cslib.sum_cube_prod_affine_eq_zero {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] {κ : Type u_2} {P : Type u_3} [Fintype κ] [DecidableEq κ] [Fintype P] (a : P → R) (b : P → κ → R) (h : ∀ (ℓ : P → Option κ), (∀ (v : κ), ∃ (p : P), ℓ p = some v) → ∃ (p : P) (v : κ), ℓ p = some v ∧ b p v = 0) : ∑ c : κ → ZMod 2, ∏ p : P, (a p + ∑ v : κ, c v • b p v) = 0

If every assignment covering all variables uses a vanishing coefficient, the cube sum of the product of affine forms is zero.

theorem Cslib.sum_cube_prod_affine_eq_permanent {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] {κ : Type u_2} [Fintype κ] [DecidableEq κ] (a : κ → R) (b : κ → κ → R) : ∑ c : κ → ZMod 2, ∏ p : κ, (a p + ∑ v : κ, c v • b p v) = (Matrix.of b).permanent

With as many affine factors as Boolean variables, the cube sum of their product is the permanent of the matrix of linear coefficients: the constant terms do not contribute.