Total influence of a Boolean-valued function is at most its degree

Proved

AaronsonAmbainis.total_influence_le_degree_of_boolean_valued

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

boolean_cube_combinatoricsboolean_function_complexity

Let $p$ be a real polynomial in $N$ variables of degree at most $d$ which takes only the values $0$ and $1$ at points of the cube $\{0,1\}^N$ . Then its influences sum to at most its degree:

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

For Boolean-valued functions the total influence is also the average sensitivity, so the statement says that a function of low degree cannot be sensitive to many coordinates on average. It is the quantitative input to the junta bound for Boolean-valued functions, and it is sharp: the dictator $p(x)=x_1$ has degree $1$ and influence sum $1$ , and the parity of three bits has degree $3$ and influence sum $3$ .

Boundedness in the interval $[0,1]$ is not enough for this inequality -- the hypothesis is the strictly stronger one that $p$ is $\{0,1\}$ -valued on the cube. That gap is precisely what makes the Aaronson--Ambainis conjecture hard.

Formalization Note The source works with $\pm1$ -valued functions on $\{-1,1\}^n$ , whereas the hypothesis here is that $p$ takes only the values $0$ and $1$ at cube points. The two are related by $g=1-2p$ , which is $\pm1$ -valued, has the same degree as $p$ , and satisfies $\operatorname{Inf}_i[g]=4\operatorname{Inf}_i[p]$ in the normalisation used here. O'Donnell's total influence $I[g]=\sum_i\mathbb{E}[(D_ig)^2]$ is one quarter of $\sum_i\operatorname{Inf}_i[g]$ , hence equal to $\sum_i\operatorname{Inf}_i[p]$ ; and $\operatorname{Inf}_i[g]>0$ exactly when $\operatorname{Inf}_i[p]>0$ , so the set of relevant coordinates is the same for both. The degree hypothesis is on totalDegree, the syntactic degree of the representative, which bounds the multilinear degree from above -- the safe direction here.

Preamble

import Definitions.Def_AaronsonAmbainis

Formal statement

namespace AaronsonAmbainis

theorem total_influence_le_degree_of_boolean_valued
    (N d : ℕ) (p : MvPolynomial (Fin N) ℝ)
    (hdeg : p.totalDegree ≤ d)
    (hbool : ∀ x : Fin N → Bool, cubeEval p x = 0 ∨ cubeEval p x = 1) :
    ∑ i : Fin N, cubeInfl p i ≤ (d : ℝ) := by sorry

end AaronsonAmbainis

Source

O'Donnell, Analysis of Boolean Functions, Cambridge Univ. Press 2014; corrected version arXiv:2105.10386, Fact 3.7 (p. 71): "For f : {-1,1}^n -> {-1,1}, I[f] <= deg(f)"; with I[f] as Definition 2.27 and Inf_i as Definition 2.17, D_i as Definition 2.16.

Read-back

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

Read-back — AaronsonAmbainis.total_influence_le_degree_of_boolean_valued

Setting. Fix two natural numbers $N$ and $d$ (both universally quantified, with no positivity assumption), and let $p$ be an element of the polynomial ring $\mathbb{R}[X_0,\dots,X_{N-1}]$ — a multivariate polynomial with real coefficients in $N$ commuting variables.

The bundled definitions, unfolded.

For a Boolean point $x$ , write $\hat{x} \in \mathbb{R}^N$ for its image under $\hat{x}_i = 1$ if $x_i = \text{true}$ , $0$ otherwise, and define the cube evaluation $P(x) := p(\hat{x})$ . The encoding is $\{0,1\}$ , not $\{-1,+1\}$ .
The cube expectation is the unweighted average over all $2^N$ Boolean points, $\mathbb{E}[f] := 2^{-N} \sum_{x} f(x)$ — expectation with respect to the uniform measure on the discrete cube. (The factor is never a division by zero, including at $N = 0$ , where the cube has exactly one point.)
$x^{\oplus i}$ denotes $x$ with coordinate $i$ negated, all others unchanged.
The influence of coordinate $i$ is the expected squared discrete difference,

I_i(p) := \mathbb{E}_x\big[(P(x) - P(x^{\oplus i}))^2\big].

This is the entire normalisation: no additional factor of $\tfrac12$ , $\tfrac14$ , or $\tfrac{1}{2^{N-1}}$ . Each edge $\{x, x^{\oplus i}\}$ contributes its squared difference twice, once from each endpoint, which is exactly what makes this quantity coincide, for $\{0,1\}$ -valued $P$ , with the probability $\Pr_x[P(x) \neq P(x^{\oplus i})]$ rather than half of it. The definition itself imposes no boundedness or Booleanness on $P$ ; it is the raw expected squared derivative.

Hypotheses.

$\deg_{\text{tot}}(p) \le d$ , the total degree of $p$ as a formal polynomial: the maximum over monomials in its support of the sum of exponents ( $0$ for the zero polynomial). This is an inequality, so $d$ is merely an upper bound and may be arbitrarily larger than the actual degree. It is also a property of the chosen representative, not of the induced cube function: $X_i^7$ and $X_i^2 - X_i$ are admitted with total degree $7$ and $2$ respectively, though the functions they compute on $\{0,1\}^N$ have multilinear degree $1$ and $0$ . So the hypothesis is stated in terms of syntactic total degree, which can strictly exceed the degree of the multilinear representation of the same cube function.
For every Boolean point $x$ , $P(x) = 0$ or $P(x) = 1$ . A pointwise, exactly-two-values condition — not the weaker hypothesis that values lie in $[0,1]$ , nor that they are bounded, nor that they are integers. The disjunction is per point, so the branch may differ at each $x$ : the hypothesis says precisely that $p$ computes some Boolean-valued function on the cube. Nothing is assumed about $p$ off the cube, where it may take any values whatsoever.

Conclusion. Under these hypotheses,

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

the sum over all $N$ coordinates, the right-hand side being the natural number $d$ under the canonical embedding $\mathbb{N} \hookrightarrow \mathbb{R}$ . Since $d$ enters as a cast natural number the bound is automatically non-negative; and because $d$ is only an upper bound on the degree, a reader supplying a loose degree bound gets a correspondingly loose conclusion.

Degenerate parameter values silently admitted.

$N = 0$ : the cube is a singleton, the index set empty, the left-hand sum the empty sum $0$ , and the conclusion reads $0 \le d$ , true for every $d$ .
$d = 0$ : the degree hypothesis forces $p$ constant, all influences vanish, and the conclusion reads $0 \le 0$ .
$p = 0$ and $p = 1$ satisfy both hypotheses for every $d$ , so for each $(N,d)$ there is at least one witness and the statement is not vacuous.
The hypotheses are restrictive in one direction only: no upper bound on $N$ relative to $d$ , and no lower bound on $d$ relative to the true degree.

Not used. The imported definitions also provide the cube variance $\operatorname{Var}(p)$ , which does not appear in this statement.

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