6 Global variance of the points measurements

Throughout this chapter, \((\psi ,A,B,L)\) is an \((\varepsilon ,\delta ,\gamma )\)-good symmetric strategy for the \((m,q,d)\) low individual degree test.

Lemma 6.1 Replacing a line answer by a fixed polynomial

✓

Let \(G \in \mathrm{PolySub}(m,q,d)\). On the axis-parallel line-test distribution,

\[ B^{\ell }_{[f(u)=g(u)]} \otimes (G_g)^{1/2} \approx _{md/q} B^{\ell }_{g|_{\ell }} \otimes (G_g)^{1/2}. \]

Proof ▶

Expand the \(\approx _{md/q}\) norm on the weighted vector \((I\otimes (G_g)^{1/2})\lvert \psi \rangle \). Because \(B^\ell \) is a projective measurement, only those line polynomials \(f\) with \(f\ne g|_\ell \) and \(f(u)=g(u)\) contribute. Lemma 3.9 is the univariate Schwartz–Zippel wrapper used in Lean for this line-restriction event; it supplies the paper’s \(md/q\) loss, and the remaining operator sum is bounded by the fact that \(G\) is a submeasurement.

Remark 6.2 Conditional variants for the collision-residual estimate

The paper proof of Lemma 6.1 bounds the collision event directly by the Schwartz–Zippel estimate. The following conditional variants instead assume this collision estimate, or one of the reindexing identities that implies it, as an explicit hypothesis. These conditional statements make explicit the intermediate estimates still needed for this route; they are not additional hypotheses in the paper statement of Lemma 6.1.

Lemma 6.3 Local variance of the points measurements

✓

Let \(G \in \mathrm{PolySub}(m,q,d)\). On the hypercube edge distribution \((u,v) \sim C\),

\begin{equation} A^u_{g(u)} \otimes (G_g)^{1/2} \approx _{24\cdot \left(\varepsilon +\delta +\frac{md}{q}\right)} A^v_{g(v)} \otimes (G_g)^{1/2}. \label{eq:local-variance-of-points-equation} \end{equation}

Proof ▶

Fix \(g\) and keep the weight \((G_g)^{1/2}\) on the second tensor factor throughout. On the vector \((I\otimes (G_g)^{1/2})\lvert \psi \rangle \) one has the six-step chain

\[ A^u_{g(u)} \otimes (G_g)^{1/2} \approx _{2\delta } I\otimes (G_g)^{1/2} A^u_{g(u)} \approx _{2\varepsilon } B^\ell _{[f(u)=g(u)]} \otimes (G_g)^{1/2} \approx _{md/q} B^\ell _{g|_\ell } \otimes (G_g)^{1/2} \approx _{md/q} B^\ell _{[f(v)=g(v)]} \otimes (G_g)^{1/2} \approx _{2\varepsilon } I\otimes (G_g)^{1/2} A^v_{g(v)} \approx _{2\delta } A^v_{g(v)} \otimes (G_g)^{1/2}. \]

The first, second, fifth, and sixth comparisons use Lemma 3.21 together with Theorem 3.25 and the good-strategy hypotheses, and the middle pair is Lemma 6.1. Lemma 3.27 sums these six weighted transports.

Lemma 6.4 Equivalent local-variance bound

✓

The local-variance bound for the point measurements is

\begin{equation} \sum _{g \in \mathcal{P}(m,q,d)} \mathbb {E}_{(u,v)\sim C} \langle \psi \rvert (A^u_{g(u)}-A^v_{g(v)})^2 \otimes G_g \lvert \psi \rangle \le 24\left(\varepsilon +\delta +\frac{md}{q}\right). \label{eq:equivalent-local-variance} \end{equation}

Proof ▶

This is the squared-norm expansion of Lemma 6.3 after summing over the polynomial outcome \(g\). The Lean proof expands the weighted operator difference, telescopes the six transports in the local variance proof, sums the resulting bounds over \(g\), and absorbs the transport-chain error into \(24\left(\varepsilon +\delta +\frac{md}{q}\right)\).

Remark 6.5 Polynomial-sum formalization for 2

The three referenced declarations and Lemma 6.4 together provide the full polynomial-sum (cardinality-free) chain proving the equation. The chain assembly lemma localVarianceDeviation_sum_le_localVarianceOfPointsError telescopes the six operator differences via ev_sum_conjTranspose_mul_sum_le, sums over \(g\), and applies the six individual _sum bounds (including the reverse generalizeB sum) to avoid the per-polynomial cardinality blow-up.

Lemma 6.6 Global variance of the points measurements

✓

Let \(G \in \mathrm{PolySub}(m,q,d)\). On the uniform distribution over independent \(u,v \in \mathbb {F}_q^m\),

\begin{equation} A^u_{g(u)} \otimes (G_g)^{1/2} \approx _{24m\left(\varepsilon +\delta +\frac{md}{q}\right)} A^v_{g(v)} \otimes (G_g)^{1/2}. \label{eq:global-variance-of-points-equation} \end{equation}

Proof ▶

We want to bound

\begin{equation} \mathbb {E}_{u,v \sim \mathbb {F}_q^m} \sum _{g \in \mathcal{P}(m,q,d)} \lVert (A^u_{g(u)}-A^v_{g(v)}) \otimes (G_g)^{1/2} \lvert \psi \rangle \rVert ^2 = \mathbb {E}_{u,v \sim \mathbb {F}_q^m} \sum _{g \in \mathcal{P}(m,q,d)} \langle \psi \rvert (A^u_{g(u)}-A^v_{g(v)})^2 \otimes G_g \lvert \psi \rangle . \label{eq:global-variance-target} \end{equation}

For each \(g \in \mathcal{P}(m,q,d)\), define

\[ A(g)^u := A^u_{g(u)}, \qquad \lvert \psi _g \rangle := (I \otimes (G_g)^{1/2})\lvert \psi \rangle . \]

Then

\[ \eqref{eq:global-variance-target} = \sum _{g \in \mathcal{P}(m,q,d)} \mathbb {E}_{u,v \sim \mathbb {F}_q^m} \langle \psi _g \rvert (A(g)^u-A(g)^v)^2 \otimes I \lvert \psi _g \rangle = \sum _{g \in \mathcal{P}(m,q,d)} 2\, \mathbf{Var}_{\mathrm{global}}(A(g),\psi _g). \]

Applying Lemma 5.12 gives

\[ \eqref{eq:global-variance-target} \le \sum _{g \in \mathcal{P}(m,q,d)} 2m\, \mathbf{Var}_{\mathrm{local}}(A(g),\psi _g) = m \cdot \sum _{g \in \mathcal{P}(m,q,d)} \mathbb {E}_{(u,v)\sim C} \langle \psi \rvert (A^u_{g(u)}-A^v_{g(v)})^2 \otimes G_g \lvert \psi \rangle . \]

The last quantity is at most \(m \cdot 24\left(\varepsilon +\delta +\frac{md}{q}\right)\) by Lemma 6.4, which is exactly 3.