Fourier coefficients of (1 − β|z|/m)^T are nonnegative and small

Proved

QAlgorithms.Arunachalam.fourier_weightPow_bound

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

arunachalamlecture-notesquantum-information

Let $m\ge10$ , $\beta\in(0,1]$ and let $T$ be an integer with $1\le T\le m/(e^3\beta)$ (the setting of Theorem 7.5.1). Let $f:\{0,1\}^m\to\mathbb R$ , $f(z)=(1-\beta|z|/m)^T$ , with Fourier coefficients $\hat f(S)=\mathbb E_z[f(z)(-1)^{S\cdot z}]$ . Then for every $S\in\{0,1\}^m$ of Hamming weight $|S|=q$ ,

0\ \le\ \hat f(S)\ \le\ 4e\left(1-\frac\beta2\right)^T\left(\frac{T\beta}{m}\right)^q e^{22T^2\beta^2/m}.

Combined with Claim 7.5.3 this bounds the diagonal of $\sqrt A$ in Theorem 7.5.1.

Formalization Note The conditions $m\ge10$ and $1\le T\le m/(e^3\beta)$ are those of Theorem 7.5.1, which the proof of the lemma uses.

Preamble

import Definitions.Def_QAlgorithms_Defs_LearningHardInstances
set_option autoImplicit false

Formal statement

namespace QAlgorithms.Arunachalam

open QAlgorithms.Learning





/-- Arunachalam p.172–175, Lemma 7.5.4, in the setting of Theorem 7.5.1 (`m ≥ 10`,
`T ∈ [1, m/(e³β)]` a natural number, which the proof uses): for `β ∈ (0, 1]`, the Fourier
coefficients of `f(z) = (1 − β|z|/m)^T` on `{0,1}^m` satisfy
`0 ≤ f̂(S) ≤ 4e (1 − β/2)^T (Tβ/m)^q e^{22T²β²/m}` for all `S` with `|S| = q`. -/
theorem fourier_weightPow_bound {m T : ℕ} {β : ℝ} (hm : 10 ≤ m) (hβ : 0 < β) (hβ1 : β ≤ 1)
    (hT : 1 ≤ T) (hTm : (T : ℝ) ≤ (m : ℝ) / (Real.exp 3 * β)) (S : Fin m → ZMod 2) :
    0 ≤ boolFourier (weightPowFun m β T) S ∧
      boolFourier (weightPowFun m β T) S ≤
        4 * Real.exp 1 * (1 - β / 2) ^ T * ((T : ℝ) * β / (m : ℝ)) ^ hammingNorm S *
          Real.exp (22 * (T : ℝ) ^ 2 * β ^ 2 / (m : ℝ)) := by
  sorry


end QAlgorithms.Arunachalam

Source

Srinivasan Arunachalam, Quantum Algorithms and Learning Theory — Part II, 2018 thesis, ILLC DS-2018-08, PDF p. 172, Lemma 7.5.4. 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, 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)$ .

Let $S \in \mathbb{F}_2^m$ be arbitrary. Define $w(u) = (1 - \beta|u|/m)^T$ on $\mathbb{F}_2^m$ , where $|u|$ is the Hamming weight. Let $\hat w(S) = 2^{-m}\sum_{u \in \mathbb{F}_2^m} w(u)(-1)^{S\cdot u}$ be its Boolean Fourier transform.

The theorem asserts

0 \le \hat w(S) \le 4e\,\Big(1 - \frac{\beta}{2}\Big)^T \Big(\frac{T\beta}{m}\Big)^{|S|} \exp\!\Big(\frac{22\,T^2\beta^2}{m}\Big),

where $|S|$ is the Hamming weight of $S$ .

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