Three-copy formula for the state-dependent second moment

Open

QAlgorithms.Papers.Independent.Intakethird100.P71.shadowSecondMoment_threeCopies

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Consider the fixed projective experiment on $N$ qudits, $d\ge2$ , with locally conjugation-invariant prior $\nu$ and invertible channel $\mathcal M$ . Let $\rho$ be a density matrix and $O$ a traceless Hermitian observable. Put $R=\mathcal M^{-1}(O)$ , $\hat o(S)=\operatorname{Tr}(O\mathcal M^{-1}(S))$ , and $Q_\rho(O)=\mathbb E_{S\mid\rho}\hat o(S)^2$ . For $g,h\in(S_3)^N$ , let $\chi_g$ permute the three copies independently at each site and $W_h^{(3)}=\mathbb E_\nu\operatorname{Tr}(S^{\otimes3}\chi_h)$ . Then

\operatorname{Var}\hat o\le Q_\rho(O),\qquad Q_\rho(O)=\sum_{g,h\in(S_3)^N}d^N\operatorname{Tr}[(R\otimes R\otimes\rho)\chi_g]\,\mathrm{Wg}_{g,h}W_h^{(3)}.

The Weingarten coefficient is the product of the local three-copy coefficients. At $d=2$ the usual spectral extension omits the three-row partition instead of inverting a singular Gram matrix. The equality is expressed over $\mathbb C$ to retain the individual permutation traces. This is a state-dependent second moment, not a worst-state supremum.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P71

Formal statement

noncomputable section

open MeasureTheory

open scoped Matrix ComplexConjugate ENNReal Matrix.Norms.Elementwise

namespace QAlgorithms.Papers.Independent.Intakethird100.P71

attribute [local instance] Classical.propDecidable

local notation "Config" n:max d:max =>
  QAlgorithms.Papers.Independent.Information100.P21.Config (P := Fin n) (fun _ => d)

local notation "Op" n:max d:max =>
  QAlgorithms.Papers.Independent.Information100.P21.Op (Config n d)

attribute [local instance] QAlgorithms.Papers.Independent.Intakethird100.P71.matrixContinuousENorm

local notation "Unitary" n:max d:max => Matrix.unitaryGroup (Config n d) ℂ

local notation "Local" n:max d:max => Fin n → Matrix.unitaryGroup (Fin d) ℂ

open QAlgorithms.Papers.Independent.Information100.P63 (tensorPower)

/-- PDF pp.4–5 Eqs.(14)–(17): the state-dependent second moment in (S_3)^N.
For qubits wgThree uses its spectral extension at the singular Gram matrix. -/
theorem shadowSecondMoment_threeCopies {n d : ℕ} (hd : 2 ≤ d) (E : ProjectiveEnsemble n d)
    (hls : LocallyScrambled (prior E)) (hc : Complete (prior E))
    (rho O : Op n d) (hrho : IsDensityMatrix rho) (hO : O.IsHermitian) (ht : O.trace = 0) :
    shotVariance (prior E) hc rho O ≤ secondMoment (prior E) hc rho O ∧
    (secondMoment (prior E) hc rho O : ℂ) =
      ∑ g : Permutations n 3, ∑ h : Permutations n 3,
        observableThree (prior E) hc rho O g * (productWgThree d g h : ℂ) *
          featureThree (prior E) h := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P71

end

Source

Classical Shadow Tomography with Locally Scrambled Quantum Dynamics, arXiv:2107.04817v4, PDF p. 4, §II B, Eqs.(14)–(17): state-dependent shadow second moment

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $n\ge0$ and $d\ge2$ , put $\mathcal X=\{0,\ldots,d-1\}^n$ and $N=d^n$ , and let $E$ supply a probability law $\lambda$ on global unitary matrices. Define $\nu=N^{-1}\sum_b(U\mapsto U^\dagger|b\rangle\langle b|U)_*\lambda$ . Assume that $\nu$ is invariant under $S\mapsto L_V^\dagger SL_V$ for every $L_V=\bigotimes_iV_i$ with all $V_i$ unitary. Define $\mathcal M(X)_{ij}=\sum_{k,l}(\int NS_{ij}S_{lk}\,d\nu(S))X_{kl}$ , assume $\mathcal M$ is injective, and write $\mathcal R=\mathcal M^{-1}$ . Let $\rho$ be positive semidefinite with trace $1$ , and let $O$ be Hermitian with trace exactly $0$ . Define $z(S)=\operatorname{Re}\operatorname{tr}(O\mathcal R(S))$ , $d\nu_\rho=[N\operatorname{Re}\operatorname{tr}(S\rho)]_+d\nu$ ,

Q=\int z(S)^2\,d\nu_\rho(S), \qquad V=Q-\left(\int z(S)\,d\nu_\rho(S)\right)^2.

For $g=(g_i)_{i<n}$ with $g_i$ permutations of $\{0,1,2\}$ , let $C_g$ be the matrix indexed by triples of configurations whose $(x,y)$ -entry is $1$ precisely when $x_k(i)=y_{g_i(k)}(i)$ for every $i,k$ , and is $0$ otherwise. For a permutation $\pi$ of three elements, put $\chi(\pi)=|\{k:\pi(k)=k\}|-1$ and

w_d(\pi)=\frac16\left[ \frac1{d(d+1)(d+2)} +\frac{2\chi(\pi)}{d(d+1)(d-1)} +\begin{cases} \dfrac{\operatorname{sgn}\pi}{d(d-1)(d-2)},&d\ge3,\\ 0,&d=2. \end{cases}\right].

Define $W_d(g,h)=\prod_iw_d(g_i h_i^{-1})$ , $F_3(h)=\int\operatorname{tr}(S^{\otimes3}C_h)\,d\nu(S)$ , and $A_3(g)=N\operatorname{tr}((\mathcal R(O)\otimes\mathcal R(O)\otimes\rho)C_g)$ , where tensor coordinates list the three copies first. The theorem states

V\le Q, \qquad Q=\sum_g\sum_h A_3(g)W_d(g,h)F_3(h),

with the second equality interpreted in $\mathbb C$ by embedding the real number $Q$ . The case $n=0$ is included, with empty products equal to $1$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph