For every \(n : \mathbb {N}\), the Boolean hypercube satisfies \(|\{ 0,1\} ^n| = 2^n\).

The average of the two values of the \(\pm 1\) embedding is zero:

For every \(b : \mathrm{Bool}\), \(\mathrm{BoolToPM1}(b)^2 = 1\).

For every \(b : \mathrm{Bool}\), \(\mathrm{BoolToPM1}(\lnot b) = -\mathrm{BoolToPM1}(b)\).

For all \(a, b : \mathrm{Bool}\), \(\mathrm{BoolToPM1}(a \oplus b) = \mathrm{BoolToPM1}(a) \cdot \mathrm{BoolToPM1}(b)\); that is, XOR corresponds to multiplication in \(\{ \pm 1\} \subset \mathbb {R}\).

If \(g : \mathrm{Fin}\, n \to \mathrm{Bool} \to \mathbb {R}\) and \(f(x) = \prod _{i} g_i(x_i)\), then

For every \(S \subseteq [n]\), \(\chi _S(\mathbf{0}) = 1\).

For every \(S \subseteq [n]\) and \(x \in \{ 0,1\} ^n\), \(\chi _S(x)^2 = 1\).

\(\chi _\emptyset = \mathbf{1}\), the constant function equal to \(1\).

For all \(S, T \subseteq [n]\) and \(x \in \{ 0,1\} ^n\),

where \(S \mathbin {\triangle } T\) denotes the symmetric difference.

For every \(x \in \{ 0,1\} ^n\) with \(x \ne \mathbf{0}\),

\(\mathbb {E}[\chi _\emptyset ] = 1\).

If \(S \ne \emptyset \), then \(\mathbb {E}[\chi _S] = 0\).

For every \(S \subseteq [n]\), \(\langle \chi _S, \chi _S \rangle = 1\).

If \(S \ne T\), then \(\langle \chi _S, \chi _T \rangle = 0\).

For every \(S \subseteq [n]\), \(\widehat{\chi _S}(S) = 1\).

If \(S \ne T\), then \(\widehat{\chi _S}(T) = 0\).

The locally-defined expectation BoolFourier.expectation agrees with BooleanAnalysis.expect: for every \(f\), \(\mathbb {E}[f] = \mathrm{expect}(f)\).

For every \(f\) and \(S\), \(\mathrm{fourier\_ coeff}(f, S) = \mathrm{fourierCoeff}(f, S)\), bridging the local and upstream definitions.

Every Boolean function \(f : \{ 0,1\} ^n \to \mathbb {R}\) expands in the Walsh–Fourier basis:

For every \(f : \{ 0,1\} ^n \to \mathbb {R}\),

For all \(f, g : \{ 0,1\} ^n \to \mathbb {R}\) and \(S \subseteq [n]\),

For every \(S \subseteq [n]\) and every \(x \in \{ 0,1\} ^n\), \(\chi _S(x)^2 = 1\). This is the squaring form (with exponent \(2\) rather than an explicit product) of the fact that Walsh characters take values in \(\{ \pm 1\} \).

As functions of \(S\), the evaluation of characters at the all-zeros vector is constant:

Let \(x \in \{ 0,1\} ^n\) with \(x \ne \mathbf{0}\) and let \(i\) be a coordinate with \(x_i = \mathtt{true}\). Then the sum of all characters at \(x\) equals the sum of their negations:

For a non-empty \(S \subseteq [n]\), the uniform expectation of the character \(\chi _S\) factorises over the coordinates of \(S\):

For every \(f : \{ 0,1\} ^n \to \mathbb {R}\), the locally-defined squared \(L^2\) norm agrees with the upstream inner product of \(f\) with itself:

For all \(f, g : \{ 0,1\} ^n \to \mathbb {R}\) and \(S \subseteq [n]\), the double sum defining the unnormalised convolution coefficient may be reordered:

For all \(x, y \in \{ 0,1\} ^n\) and \(S \subseteq [n]\),

expressing that \(\chi _S\) is a character of the group \((\mathbb {F}_2)^n\). The statement also carries the (unused) Fubini hypothesis of the enclosing proof.

Let \(f, g : \{ 0,1\} ^n \to \mathbb {R}\), let \(S \subseteq [n]\), assume the Fubini interchange for the convolution coefficient, and let \(y \in \{ 0,1\} ^n\). Then translating the argument of \(g\) by \(y\) only multiplies the character-weighted sum by \(\chi _S(y)\):