lemmaroutine

Boolean sum via fixed substitutions

Lemma·lem:boolean-differences·§3.4 Taylor coefficients from fixed Boolean substitutions

Statement (paper)

Let

q\ge0

be an integer and let

\mathcal A

be a commutative ring with identity. For each

x\in\{0,1\}^n

, let

p_x(X_1,\ldots,X_n)

be a polynomial over

\mathcal A

of degree at most

q

. Then

\begin{aligned} \sum_{x\in\{0,1\}^n}p_x(x) &=\sum_{\substack{E\subseteq[n]\\|E|\le q}} \sum_{U\subseteq E}(-1)^{|E|-|U|} \sum_{\substack{x\in\{0,1\}^n\\x_i=1\ (i\in E)}} p_x(\mathbf1_U). \end{aligned}

Here

\mathbf1_U

is the indicator vector of

U

In plain English

For polynomials

p_x

of degree at most

q

over a commutative ring, the sum

\sum_{x\in\{0,1\}^n} p_x(x)

equals a signed sum over sets

E\subseteq[n]

with

|E|\le q

and

U\subseteq E

of the values

p_x(\mathbf1_U)

, with

x

ranging over Boolean vectors that have

x_i=1

E

Why it's here

It rewrites a sum where each polynomial is evaluated at its own index

x

as a sum of evaluations at fixed Boolean points

\mathbf1_U

, with only sets

E

of size at most

q

appearing. This is the Taylor-coefficient (finite-difference) expansion that lets the counting routine in the next proposition replace evaluation at

x

by evaluations at a small family of fixed substitutions. The degree bound

q

is what truncates the sum over

E

Classified routine:

Direct consequence of the Möbius inversion / multilinear (Fourier–Walsh) expansion over the Boolean cube: on {0,1}^n, p_x(x) = sum_{E} x^E sum_{U⊆E} (-1)^{|E|-|U|} p_x(1_U), and the degree bound q truncates the sum over E. This is a standard finite-difference identity applied to an index-dependent family of polynomials.

Uses

Nothing else in the paper

Used by

propGeneral counting routine and its cost

Sources

PaperOpen

Section: §3.4 Taylor coefficients from fixed Boolean substitutions
Page: —
Label: lem:boolean-differences
Line: main_full_version.tex:1933

Leannot aligned

Phase 2 aligns this node to a Lean declaration.