Poincar\'e inequality on the Boolean cube: $4\operatorname{Var}[p]\le\sum_i\operatorname{Inf}_i[p]$

Proved

AaronsonAmbainis.poincare_four_mul_cubeVar_le_sum_cubeInfl

by Goku · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

boolean_cube_combinatoricsboolean_function_complexity

The Poincare inequality on the Boolean cube, in the influence normalisation used by Aaronson and Ambainis.

Let $p$ be a real polynomial in $N$ variables, regarded as a function on $\{0,1\}^N$ under the uniform distribution, and let $\operatorname{Var}[p]$ and $\operatorname{Inf}_i[p]=\mathbb{E}\big[(p(x)-p(x^{\oplus i}))^2\big]$ be as in the imported definitions. Then

4\operatorname{Var}[p]\;\le\;\sum_{i=1}^{N}\operatorname{Inf}_i[p].

The inequality holds for every function on the cube; no bound on the degree of $p$ is needed. It is the elementary lower bound against which the Aaronson--Ambainis conjecture is measured: it yields a coordinate of influence at least $4\operatorname{Var}[p]/N$ , which degrades with the number of variables, whereas the conjecture asks for a bound depending only on the variance and the degree.

The constant $4$ is sharp. Equality holds for the dictator $p(x)=x_1$ , where $\operatorname{Var}[p]=1/4$ and the influence sum equals $1$ .

Formalization Note The factor $4$ reflects a difference of convention rather than of content. O'Donnell defines the discrete derivative as $D_ip(x)=\tfrac12\big(p(x^{i\mapsto1})-p(x^{i\mapsto-1})\big)$ and the influence as $\mathbb{E}[(D_ip)^2]$ , so his influence is one quarter of the quantity used here; his statement $\operatorname{Var}[p]\le I[p]$ is therefore the inequality above. The source works over $\{-1,1\}^N$ , but both variance and influence as defined here depend only on the values of $p$ at cube points and on the bit-flip involution, so they are unchanged by the affine relabelling between $\{0,1\}^N$ and $\{-1,1\}^N$ .

Preamble

import Definitions.Def_AaronsonAmbainis

Formal statement

namespace AaronsonAmbainis

theorem poincare_four_mul_cubeVar_le_sum_cubeInfl (N : ℕ) (p : MvPolynomial (Fin N) ℝ) :
    4 * cubeVar p ≤ ∑ i : Fin N, cubeInfl p i := by sorry

end AaronsonAmbainis

Source

O'Donnell, Analysis of Boolean Functions, Cambridge Univ. Press 2014; corrected version arXiv:2105.10386, Chapter 2 (Basic concepts and social choice), the "Poincare Inequality" (named, unnumbered display, p. 52 of the arXiv PDF), stated as Var[f] <= I[f]; with Inf_i and I[f] as in Definitions 2.17 and 2.27 and D_i as in Definition 2.16. The factor 4 here converts O'Donnell's normalisation to the influence Inf_i[p] = E[(p(x) - p(x^{+i}))^2] used by Aaronson & Ambainis, arXiv:0911.0996.

Read-back

What the Lean code literally says, in plain math · claude-opus-5

Read-back — AaronsonAmbainis.poincare_four_mul_cubeVar_le_sum_cubeInfl

Fix a natural number $N$ (explicitly quantified, with no positivity assumption, so $N = 0$ is included) and an arbitrary multivariate polynomial $p \in \mathbb{R}[X_0,\dots,X_{N-1}]$ in $N$ real variables indexed by $\{0,\dots,N-1\}$ . No hypothesis whatsoever is placed on $p$ — in particular there is no bound on its degree, no restriction to multilinear polynomials, no normalisation of its coefficients or of its values, and no assumption that $p \neq 0$ .

All quantities below are defined purely through the values of $p$ at the $2^N$ points of the $\{0,1\}$ -cube (not the $\{-1,+1\}$ -cube). Concretely, for a Boolean assignment $x \in \{\text{false},\text{true}\}^N$ let $\tau(x) \in \mathbb{R}^N$ be the real point with $\tau(x)_i = 1$ if $x_i$ is true and $\tau(x)_i = 0$ otherwise, and set

P(x) := p\big(\tau(x)\big) \in \mathbb{R}.

Thus $p$ enters the statement only via the function $P : \{0,1\}^N \to \mathbb{R}$ it induces on the cube's vertices; two different polynomials agreeing on $\{0,1\}^N$ give literally the same statement.

Expectation is the uniform average over all $2^N$ Boolean assignments, with the explicit normalising factor $(2^N)^{-1}$ (the natural number $2^N$ being cast to a real, hence never zero):

\mathbb{E}[f] := \frac{1}{2^N}\sum_{x \in \{0,1\}^N} f(x).

Two derived quantities are used:

the variance

V(p) := \mathbb{E}\Big[\big(P(x) - \mathbb{E}[P]\big)^2\Big] = \frac{1}{2^N}\sum_{x}\Big(P(x) - \frac{1}{2^N}\sum_{y} P(y)\Big)^{2};

for each coordinate $i \in \{0,\dots,N-1\}$ , the coordinate influence

I_i(p) := \mathbb{E}\Big[\big(P(x) - P(x^{\oplus i})\big)^2\Big] = \frac{1}{2^N}\sum_{x}\big(P(x) - P(x^{\oplus i})\big)^{2},

where $x^{\oplus i}$ is $x$ with its $i$ -th bit negated and all other bits unchanged. Note the normalisation: $I_i$ is the plain mean squared discrete difference, with no additional factor of $\tfrac12$ or $\tfrac14$ , and the difference is taken over all $x$ (so each unordered edge of the cube is counted twice, once from each endpoint).

The theorem asserts the single inequality

4\,V(p) \;\le\; \sum_{i=0}^{N-1} I_i(p),

i.e. four times the variance is bounded above (non-strictly, $\le$ ) by the unweighted sum of the $N$ coordinate influences. The numeric constant $4$ multiplies the variance on the left-hand side; there is no constant on the right, and no dependence of the constant on $N$ , on the degree of $p$ , or on anything else.

Degenerate cases silently included: when $N = 0$ the cube $\{0,1\}^0$ has exactly one point, $2^N = 1$ , the variance is $0$ , and the index set $\{0,\dots,N-1\}$ is empty so the right-hand sum is $0$ , giving $0 \le 0$ . When $p$ is a constant polynomial both sides are $0$ . There are no typeclass hypotheses beyond those fixed by the concrete choice of coefficient ring $\mathbb{R}$ and variable type $\{0,\dots,N-1\}$ , and no hypothesis in the statement is unsatisfiable.

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by Goku · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Poincar\'e inequality on the Boolean cube: 4Var⁡[p]≤∑iInf⁡i[p]4\operatorname{Var}[p]\le\sum_i\operatorname{Inf}_i[p]4Var[p]≤∑i​Infi​[p]

Poincar\'e inequality on the Boolean cube: $4\operatorname{Var}[p]\le\sum_i\operatorname{Inf}_i[p]$