Eigenvalues of an XOR-convolution matrix are scaled Fourier coefficients

Proved

QAlgorithms.Arunachalam.xorConv_eigenvalues

by Goku · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

arunachalamlecture-notesquantum-information

Let $g:\{0,1\}^k\to\mathbb R$ and let $P\in\mathbb R^{2^k\times2^k}$ be defined by $P(x,y)=g(x+y)$ , where addition is over $\mathbb F_2$ . Write $\hat g(Q)=\mathbb E_{z\in\{0,1\}^k}[g(z)(-1)^{Q\cdot z}]$ for the Fourier coefficients of $g$ . Then the eigenvalues of $P$ , counted with multiplicity, are $2^k\hat g(Q)$ for $Q\in\{0,1\}^k$ :

\chi_P(X)=\prod_{Q\in\{0,1\}^k}\bigl(X-2^k\hat g(Q)\bigr),\qquad \operatorname{spec}(P)=\{2^k\hat g(Q):Q\in\{0,1\}^k\}.

The Hadamard matrix diagonalizes every such matrix; this is the basic tool for computing the square root of the Gram matrix in Theorem 7.5.1.

Preamble

import Definitions.Def_QAlgorithms_Defs_LearningHardInstances
set_option autoImplicit false

Formal statement

namespace QAlgorithms.Arunachalam

open QAlgorithms.Learning



/-- Arunachalam p.171, Claim 7.5.2: for `g : {0,1}^k → ℝ` and `P ∈ ℝ^{2^k × 2^k}` defined by
`P(x, y) = g(x + y)` (addition over `F₂`), the eigenvalues of `P` are
`{2^k ĝ(Q) : Q ∈ {0,1}^k}`, with `ĝ(Q) = E_z[g(z)(−1)^{Q·z}]`.

Stated with multiplicities, as the proof gives it (`H P H⁻¹ = diag(2^k ĝ(Q))`): the
characteristic polynomial of `P` is `∏_Q (X − 2^k ĝ(Q))`; and, as a set, the spectrum of `P` is
`{2^k ĝ(Q)}`. -/
theorem xorConv_eigenvalues {k : ℕ} (g : (Fin k → ZMod 2) → ℝ) :
    (xorConvMatrix g).charpoly =
        ∏ Q : Fin k → ZMod 2, (Polynomial.X - Polynomial.C ((2 : ℝ) ^ k * boolFourier g Q)) ∧
      spectrum ℝ (xorConvMatrix g) = Set.range fun Q => (2 : ℝ) ^ k * boolFourier g Q := by
  sorry




end QAlgorithms.Arunachalam

Source

Srinivasan Arunachalam, Quantum Algorithms and Learning Theory — Part II, 2018 thesis, ILLC DS-2018-08, PDF p. 171, Claim 7.5.2. https://ir.cwi.nl/pub/27536/Thesis_S_Arunachalam

Read-back

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

Let $k \in \mathbb{N}$ (including $k = 0$ ), and let $g : \mathbb{F}_2^k \to \mathbb{R}$ be an arbitrary function. Let $A_g$ be the real $2^k \times 2^k$ matrix indexed by $\mathbb{F}_2^k$ with entries

(A_g)_{x,y} = g(x+y),

where the addition is in $\mathbb{F}_2^k$ (bitwise XOR). Let $\hat g$ be the Boolean Fourier transform

\hat g(Q) = 2^{-k} \sum_{x \in \mathbb{F}_2^k} g(x)\,(-1)^{Q\cdot x}, \qquad Q \in \mathbb{F}_2^k,

where $Q \cdot x \in \mathbb{F}_2$ is the dot product, read as $0$ or $1$ in the exponent.

The theorem asserts two things:

The characteristic polynomial of $A_g$ is

\prod_{Q \in \mathbb{F}_2^k} \big(X - 2^k\,\hat g(Q)\big).

The real spectrum of $A_g$ is exactly the set $\{\,2^k\,\hat g(Q) : Q \in \mathbb{F}_2^k\,\}$ .

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Goku · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph