Diagonal of the square root of an XOR-invariant Gram matrix (corrected: with the factor 2^{-k/2})

Open

QAlgorithms.LearningSurvey.sqrtGram_diag_le

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

learning-surveylecture-notesquantum-information

This is the spectral estimate behind the pretty-good-measurement lower bounds for quantum PAC and agnostic learning, stated with the decay factor that the source's application needs.

Let $m\ge 10$ , $\beta\in(0,1]$ and let $T$ be a natural number with $1\le T\le m/(e^3\beta)$ . Define $f:\{0,1\}^m\to\mathbb R$ by $f(w)=(1-\beta|w|/m)^T$ , where $|w|$ is the Hamming weight. Let $k\le m$ and let $M\in\mathbb F_2^{m\times k}$ have rank $k$ . Let $A$ be the $2^k\times 2^k$ real matrix $A(z,y)=f(M(z\oplus y))$ , where $z\oplus y$ is addition in $\mathbb F_2^k$ and $M(z\oplus y)$ is the matrix-vector product over $\mathbb F_2$ . The matrix $A$ is positive semidefinite; write $\sqrt A$ for its positive semidefinite square root.

There is an absolute constant $K>0$ such that for all such $m,k,\beta,T,M$ and every $z\in\{0,1\}^k$ ,

\sqrt{A}(z,z)\ \le\ 2^{-k/2}\, e^{K\left(T\beta^2/m+\sqrt{Tm\beta}\right)} .

Because the pretty-good-measurement success probability of the ensemble with Gram matrix $G=A/2^k$ is $\sum_z\sqrt G(z,z)^2=\sqrt A(z,z)^2$ , this bound gives the exponentially small success probability used in the proofs of Theorems 4.12 and 4.15.

Formalization Note The source prints the bound without the factor $2^{-k/2}$ . In that form it always holds trivially, since $\sqrt A(z,z)\le 1$ . The factor is the decay that holds for every $k\le m$ , and it cannot be improved (at $T=1$ and $\beta\to 0$ , $\sqrt A(z,z)\to 2^{-k/2}$ ). $\sqrt A(z,z)$ is the $(z,z)$ entry of the square-root matrix, not the square root of the entry.

Preamble

import Definitions.Def_QAlgorithms_Defs_LearningHardInstances
set_option autoImplicit false

Formal statement

namespace QAlgorithms.LearningSurvey

open MeasureTheory QAlgorithms.Learning


/-- Corrected statement. survey p.13, Theorem 4.13 ([AW17, Theorem 17]). Printed: for `m ≥ 10`,
`f(w) = (1 − β|w|/m)^T` with `β ∈ (0, 1]`, `T ∈ [1, m/(e³β)]`, `k ≤ m`, `M ∈ F₂^{m×k}` of rank `k`
and `A(z, y) = (f ∘ M)(z ⊕ y)`, one has `√A(z, z) ≤ e^{O(Tβ²/m + √(Tmβ))}` for all `z`.

Changed: the bound carries the factor `2^{−k/2}`, i.e.
`√A(z, z) ≤ 2^{−k/2} · e^{K(Tβ²/m + √(Tmβ))}` with an absolute `K > 0`.

Why: as printed the bound is contentless. For integer `T`, `f ∘ M` has nonnegative Fourier
coefficients, so `A` is positive semidefinite with `A(z, z) = f(0) = 1`, and `√A(z, z) ≤ 1` always.
The source's own use (p.14, p.15: `P_pgm = Σ_z √G(z,z)² ≤ e^{O(Tε²/d + √(Tdε)) − d − Tε}`, with
`G = A/2^k`, so `P_pgm = √A(z,z)²`) needs a decaying factor that the printed statement drops
(trap 30). The decay that holds for every `k ≤ m` is `2^{−k/2}`. It cannot be `k`-independent
(at `k = 0`, `√A = 1`), and its rate is tight (at `T = 1`, `β → 0`, `√A(z,z) → 2^{−k/2}`). With
the proof's `k ≥ d/4` it gives the source's `e^{−Ω(d)}`.

`T` is a natural number (the number of copies in both applications), so `√A` is the positive
semidefinite square root (`psdSqrt`); `√A(z, z)` is the `(z, z)` entry of that root. -/
theorem sqrtGram_diag_le :
    ∃ K : ℝ, 0 < K ∧ ∀ (m k : ℕ) (β : ℝ) (T : ℕ) (M : Matrix (Fin m) (Fin k) (ZMod 2))
      (z : Fin k → ZMod 2), 10 ≤ m → k ≤ m → 0 < β → β ≤ 1 → 1 ≤ T →
      (T : ℝ) ≤ (m : ℝ) / (Real.exp 3 * β) → M.rank = k →
      psdSqrt (xorConvMatrix fun x => weightPowFun m β T (M.mulVec x)) z z ≤
        (Real.sqrt 2)⁻¹ ^ k *
          Real.exp (K * ((T : ℝ) * β ^ 2 / (m : ℝ) + Real.sqrt ((T : ℝ) * (m : ℝ) * β))) := by sorry



end QAlgorithms.LearningSurvey

Source

Srinivasan Arunachalam and Ronald de Wolf, A Survey of Quantum Learning Theory, 2017, v3, PDF p. 13, Theorem 4.13. https://arxiv.org/pdf/1701.06806v3

Read-back

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

The statement asserts that there is a single real constant $K > 0$ such that the following holds for all natural numbers $m, k, T$ , every real $\beta$ , every matrix $M \in \mathbb{F}_2^{m \times k}$ , and every vector $z \in \mathbb{F}_2^k$ .

Hypotheses. Assume:

$m \ge 10$ and $k \le m$ ;
$0 < \beta \le 1$ ;
$T \ge 1$ and $T \le \dfrac{m}{e^{3}\beta}$ , a real inequality;
$\operatorname{rank}(M) = k$ , computed over $\mathbb{F}_2$ , so $M$ has full column rank.

The case $k = 0$ is not excluded. Here $M$ is the empty $m \times 0$ matrix and the index set $\mathbb{F}_2^0$ is a single point.

The matrix. Define the real $2^k \times 2^k$ matrix $G$ , indexed by $x, y \in \mathbb{F}_2^k$ , by

G_{x,y} = \left(1 - \frac{\beta\, |M(x+y)|}{m}\right)^{T}.

Here $x + y$ is coordinatewise addition mod 2, $M(x+y) \in \mathbb{F}_2^m$ is the matrix–vector product over $\mathbb{F}_2$ , and $|\cdot|$ is Hamming weight, the number of nonzero coordinates. In other words, $G$ is the XOR-convolution matrix of the function

w \mapsto \left(1 - \frac{\beta |Mw|}{m}\right)^T .

The square root. Let $\sqrt{G}$ be the matrix obtained by applying the real function $t \mapsto \sqrt{t}$ to $G$ via the continuous functional calculus. Concretely, $G$ is symmetric because $x + y = y + x$ . Diagonalize it orthogonally and replace each eigenvalue $\lambda$ by $\sqrt{\lambda}$ . The real square root used here sends negative numbers to $0$ , so any negative eigenvalue would be replaced by $0$ .

Conclusion. The diagonal entry of $\sqrt{G}$ at index $z$ satisfies

\big(\sqrt{G}\big)_{z,z} \;\le\; \left(\frac{1}{\sqrt 2}\right)^{k} \exp\!\left( K \left( \frac{T \beta^2}{m} + \sqrt{T\, m\, \beta} \right) \right).

The constant $K$ is chosen once, before all of $m, k, \beta, T, M, z$ , so it does not depend on any of them.

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