Diagonal of √A in terms of Fourier coefficients of f

Proved

QAlgorithms.Arunachalam.sqrtA_diag

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

arunachalamlecture-notesquantum-information

Work in the setting of Theorem 7.5.1: let $m\ge10$ , $\beta\in(0,1]$ and let $T$ be an integer with $1\le T\le m/(e^3\beta)$ ; let $f:\{0,1\}^m\to\mathbb R$ , $f(z)=(1-\beta|z|/m)^T$ , where $|z|$ is the Hamming weight; let $k\le m$ and let $M\in\mathbb F_2^{m\times k}$ have rank $k$ ; and let $A\in\mathbb R^{2^k\times 2^k}$ be $A(x,y)=(f\circ M)(x+y)=f(M(x+y))$ . Then for every $x\in\{0,1\}^k$ ,

\sqrt A\,(x,x)=\frac1{2^{k/2}}\sum_{Q\in\{0,1\}^k}\sqrt{\sum_{S\in\{0,1\}^m:\,M^{\mathsf T}S=Q}\hat f(S)},

where $\sqrt A$ is the positive semidefinite square root of $A$ and $\hat f$ is the Fourier transform of $f$ .

This expresses the diagonal of $\sqrt A$ , which governs the pretty good measurement success probability, through the Fourier coefficients of $f$ .

Formalization Note $\sqrt A$ is computed by the continuous functional calculus applied to the symmetric matrix $A$ (the square root of each eigenvalue). The hypotheses of Theorem 7.5.1 are carried as hypotheses of the claim.

Preamble

import Definitions.Def_QAlgorithms_Defs_LearningHardInstances
set_option autoImplicit false

Formal statement

namespace QAlgorithms.Arunachalam

open QAlgorithms.Learning




/-- Arunachalam p.170–172, Claim 7.5.3, in the setting of Theorem 7.5.1: `m ≥ 10`,
`f(z) = (1 − β|z|/m)^T` on `{0,1}^m` with `β ∈ (0, 1]` and `T ∈ [1, m/(e³β)]` (a natural number),
`k ≤ m`, `M ∈ F₂^{m×k}` of rank `k`, and `A(x, y) = (f ∘ M)(x + y)` for `x, y ∈ {0,1}^k`. Then for
all `x ∈ {0,1}^k`,
`√A(x, x) = 2^{−k/2} ∑_{Q ∈ {0,1}^k} √(∑_{S ∈ {0,1}^m : Mᵀ S = Q} f̂(S))`,
where `√A` is the positive semidefinite square root of `A`. -/
theorem sqrtA_diag {m k T : ℕ} {β : ℝ} (hm : 10 ≤ m) (hβ : 0 < β) (hβ1 : β ≤ 1) (hT : 1 ≤ T)
    (hTm : (T : ℝ) ≤ (m : ℝ) / (Real.exp 3 * β)) (hk : k ≤ m)
    (M : Matrix (Fin m) (Fin k) (ZMod 2)) (hM : M.rank = k) (x : Fin k → ZMod 2) :
    psdSqrt (xorConvMatrix fun z => weightPowFun m β T (M.mulVec z)) x x =
      (Real.sqrt ((2 : ℝ) ^ k))⁻¹ *
        ∑ Q : Fin k → ZMod 2, Real.sqrt
          (∑ S ∈ Finset.univ.filter (fun S : Fin m → ZMod 2 => M.transpose.mulVec S = Q),
            boolFourier (weightPowFun m β T) S) := 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.3. 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 $m, k, T \in \mathbb{N}$ and $\beta \in \mathbb{R}$ . Assume:

$m \ge 10$ ;
$0 < \beta \le 1$ ;
$T \ge 1$ ;
$T \le m / (e^3 \beta)$ ;
$k \le m$ ;
$M$ is an $m \times k$ matrix over $\mathbb{F}_2$ of rank $k$ ;
$x \in \mathbb{F}_2^k$ .

Define $w : \mathbb{F}_2^m \to \mathbb{R}$ by

w(u) = \left(1 - \frac{\beta\,|u|}{m}\right)^T,

where $|u|$ is the Hamming weight of $u$ . Let $A$ be the real $2^k \times 2^k$ matrix indexed by $\mathbb{F}_2^k$ with entries

A_{y,z} = w\big(M(y+z)\big).

Let $\sqrt{A}$ be the matrix square root given by the real continuous functional calculus. On a symmetric matrix, this applies $t \mapsto \sqrt t$ to the eigenvalues, where $\sqrt t$ is taken to be $0$ for $t < 0$ . On a non-symmetric matrix it gives $0$ ; $A$ is symmetric here.

Let $\hat w(S) = 2^{-m}\sum_{u \in \mathbb{F}_2^m} w(u)(-1)^{S\cdot u}$ be the Fourier transform of $w$ on $\mathbb{F}_2^m$ .

The theorem asserts that the diagonal entry of $\sqrt A$ at $(x,x)$ is

\big(\sqrt A\big)_{x,x} = \frac{1}{\sqrt{2^k}} \sum_{Q \in \mathbb{F}_2^k} \sqrt{\sum_{S \in \mathbb{F}_2^m \,:\, M^{\mathsf T} S = Q} \hat w(S)}.

Here each $\sqrt{\cdot}$ is the real square root, again $0$ on negative arguments. The right-hand side does not depend on $x$ .

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