PGM success bound for the PAC hard ensemble

Proved

QAlgorithms.Arunachalam.pgm_pac_hard_ensemble

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

arunachalamlecture-notesquantum-information

Fix integers $d\ge 10$ , $k$ and $T\ge 1$ and a real $\varepsilon\in(0,1/20)$ . Let $M\in\mathbb F_2^{d\times k}$ be a matrix of rank $k$ with $k\ge d/4$ whose codewords satisfy $d_H(Mx,My)\ge d/8$ for $x\neq y$ (the generator matrix of a $[d,k,r]_2$ code with $r\ge d/8$ ). On the points $s_0,\dots,s_d$ let $D(s_0)=1-20\varepsilon$ and $D(s_i)=20\varepsilon/d$ for $i\in[d]$ , and for $x\in\{0,1\}^k$ let $c^x(s_0)=0$ and $c^x(s_i)=(Mx)_i$ . Assume $T\le d/(20e^3\varepsilon)$ . Put

|\psi_x\rangle=\sum_{i=0}^{d}\sqrt{D(s_i)}\,|s_i,c^x(s_i)\rangle,\qquad \mathcal E=\{(2^{-k},|\psi_x\rangle^{\otimes T}):x\in\{0,1\}^k\}.

Then the success probability of the pretty good measurement for $\mathcal E$ satisfies

P^{\mathrm{PGM}}(\mathcal E)\ \le\ \frac{4e}{2^{d/4+T\varepsilon}}\;e^{8800T^2\varepsilon^2/d+4\sqrt{5Td\varepsilon}}.

Since the PGM is optimal for this ensemble, the bound shows that $T=\Omega(d/\varepsilon)$ copies are needed to identify $x$ with constant probability; it is the core of Theorem 7.5.6.

Formalization Note The points $s_i$ enter only as orthonormal labels, so $|s_i,b\rangle$ is the basis vector of $(i,b)\in\{0,\dots,d\}\times\{0,1\}$ . $P^{\mathrm{PGM}}(\mathcal E)=\sum_x p_x|\langle\psi_x'|\rho^{-1/2}|\psi_x\rangle|^2$ with $\rho=\sum_x|\psi_x'\rangle\langle\psi_x'|$ , $\psi_x'=\sqrt{p_x}\psi_x$ (pseudo-inverse square root). The hypotheses $d\ge 10$ , $T\ge1$ , $T\le d/(20e^3\varepsilon)$ and the code parameters are those of the surrounding proof (Theorem 7.5.1 with $m=d$ , $\beta=20\varepsilon$ ).

Preamble

import Definitions.Def_QAlgorithms_Defs_LearningHardInstances
set_option autoImplicit false

Formal statement

namespace QAlgorithms.Arunachalam

open QAlgorithms.Learning


/-- Arunachalam p.176–177, Lemma 7.5.7, in the setting of the proof of Theorem 7.5.6:
`ε ∈ (0, 1/20)`; `D(s₀) = 1 − 20ε`, `D(s_i) = 20ε/d` for `i ∈ [d]`; `M ∈ F₂^{d×k}` is the rank-`k`
generator matrix of a `[d, k, r]₂` code with `k ≥ d/4` and distance `r ≥ d/8`; `c^x(s₀) = 0`,
`c^x(s_i) = (Mx)_i`; `1 ≤ T ≤ d/(20e³ε)` and `d ≥ 10` (the hypotheses of Theorem 7.5.1 with
`m = d`, `β = 20ε`). For every `x ∈ {0,1}^k` let `|ψ_x⟩ = ∑_{i ∈ {0,…,d}} √D(s_i) |s_i, c^x(s_i)⟩`
and `E = {(2^{−k}, |ψ_x⟩^{⊗T}) : x ∈ {0,1}^k}`. Then
`P^PGM(E) ≤ (4e / 2^{d/4 + Tε}) e^{8800T²ε²/d + 4√(5Tdε)}`. -/
theorem pgm_pac_hard_ensemble {d k T : ℕ} {ε : ℝ} (hd : 10 ≤ d) (hε : 0 < ε) (hε' : ε < 1 / 20)
    (M : Matrix (Fin d) (Fin k) (ZMod 2)) (hM : M.rank = k) (hkd : k ≤ d) (hdk : d ≤ 4 * k)
    (hdist : ∀ x y : Fin k → ZMod 2, x ≠ y →
      (d : ℝ) / 8 ≤ (hammingDist (M.mulVec x) (M.mulVec y) : ℝ))
    (hT : 1 ≤ T) (hTd : (T : ℝ) ≤ (d : ℝ) / (20 * Real.exp 3 * ε)) :
    pgmSuccess (fun _ : Fin k → ZMod 2 => ((2 : ℝ) ^ k)⁻¹)
        (fun x => tensorPow T (exampleState (pacHardConcept M x) (pacHardDist d ε))) ≤
      4 * Real.exp 1 / (2 : ℝ) ^ ((d : ℝ) / 4 + (T : ℝ) * ε) *
        Real.exp (8800 * (T : ℝ) ^ 2 * ε ^ 2 / (d : ℝ) +
          4 * Real.sqrt (5 * (T : ℝ) * (d : ℝ) * ε)) := by
  sorry





end QAlgorithms.Arunachalam

Source

Srinivasan Arunachalam, Quantum Algorithms and Learning Theory — Part II, 2018 thesis, ILLC DS-2018-08, PDF p. 176, Lemma 7.5.7. 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 $d, k, T \in \mathbb{N}$ and $\varepsilon \in \mathbb{R}$ , and let $M$ be a $d \times k$ matrix over $\mathbb{F}_2$ . Assume:

$d \ge 10$ and $0 < \varepsilon < 1/20$ ;
$M$ has rank $k$ over $\mathbb{F}_2$ , and $k \le d \le 4k$ ;
for all distinct $x \ne y$ in $\mathbb{F}_2^k$ , the Hamming distance between the codewords $Mx$ and $My$ is at least $d/8$ ;
$1 \le T$ and $T \le \dfrac{d}{20\, e^3\, \varepsilon}$ .

For $x \in \mathbb{F}_2^k$ , define the following objects on the index set $\{0,1,\dots,d\}$ :

the concept $c_x$ has $c_x(0) = 0$ and $c_x(i) = 1$ iff $(Mx)_i = 1$ , for $i = 1,\dots,d$ ;
the distribution $D$ has $D(0) = 1 - 20\varepsilon$ and $D(i) = 20\varepsilon/d$ for $i = 1,\dots,d$ ;
$\psi_x$ is the vector on $\{0,\dots,d\} \times \{0,1\}$ with amplitude $\sqrt{D(j)}$ at $(j, c_x(j))$ and $0$ at $(j, 1 - c_x(j))$ ;
$\Psi_x = \psi_x^{\otimes T}$ , with amplitude $\prod_i \psi_x(z_i)$ at $(z_1,\dots,z_T)$ .

The conclusion bounds the "pretty good measurement" success quantity for the ensemble $\{\Psi_x\}$ with uniform prior $p_x = 2^{-k}$ . Set $\Psi'_x = \sqrt{p_x}\,\Psi_x$ and $\rho = \sum_x |\Psi'_x\rangle\langle\Psi'_x|$ . Let $\rho^{-1/2}$ be obtained by applying $t \mapsto 1/\sqrt{t}$ to the eigenvalues of $\rho$ ; zero eigenvalues are sent to $0$ , by the convention $1/0 = 0$ . The success quantity is

P_{\mathrm{PGM}} = \sum_{x} 2^{-k}\,\big|\langle \rho^{-1/2}\Psi'_x, \Psi_x\rangle\big|^2.

The theorem states

P_{\mathrm{PGM}} \;\le\; \frac{4e}{2^{\,d/4 + T\varepsilon}}\cdot \exp\!\left(\frac{8800\, T^2\varepsilon^2}{d} + 4\sqrt{5\,T d\,\varepsilon}\right),

where $2^{(\cdot)}$ is a real power.

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