Simultaneous normalized process-overlap prediction

Open

QAlgorithms.Papers.Independent.Intakethird100.P66.simultaneousNormalizedOverlaps

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

prove2quantum

Fix $n\ge1$ , $M\ge1$ , trace-one positive semidefinite input/output matrices $(\rho_i^{\rm in},\sigma_i)_{i=1}^M$ before sampling, and $0<\epsilon,\delta<1$ . Put $O_i=(\rho_i^{\rm in})^T\otimes\sigma_i$ , $O_i^0=O_i-\operatorname{Tr}(O_i)I/4^n$ , and $L=\epsilon^{-2}\log(2M/\delta)$ . For any unknown CPTP channel, write $\rho_{\Lambda}=2^{-n}\Lambda_{\mathcal E}$ .

An absolute $C>0$ , independent of system size, family, primitive, accuracy, confidence and channel, gives the following sufficient total counts. For an arbitrary fixed informationally complete primitive $\mathcal U$ , use $\lceil CL\max_i\|O_i^0\|_{\mathrm{shadow},\mathcal U}^2\rceil$ . For global Clifford measurements, use $\lceil CL\max_i\operatorname{Tr}(O_i^2)\rceil$ . For independent single-qubit Cliffords, if $O_i$ is the identity outside a specified subset of $k_i$ of all $2n$ Choi wires, use $\lceil CL\max_i4^{k_i}\|O_i\|_\infty^2\rceil$ . In each case an estimator chosen independently of the channel, on that many independent fresh-shot records, satisfies

\Pr\!\left[\forall i,\ \left|\widehat o_i-\operatorname{Tr}(O_i\rho_{\Lambda})\right|\le\epsilon\right]\ge1-\delta.

For each pure input/output pair,

\operatorname{Tr}(O_i^2)=1,\qquad \|O_i\|_\infty^2=1.

The shadow norm uses the inverse measurement channel and the worst normalized-state second moment. The physical overlap is $2^n$ times the normalized target, so physical accuracy $\epsilon$ requires normalized accuracy $\epsilon/2^n$ (or $\epsilon/2^k$ for a reduced process). The result permits one data set to predict many fixed normalized queries. For the general Borel measurement primitive, the estimator is measurable, so the simultaneous success event is measurable.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P66

Formal statement

noncomputable section

open MeasureTheory QAlgorithms ClassicalShadows

open scoped Matrix ComplexConjugate ENNReal

namespace QAlgorithms.Papers.Independent.Intakethird100.P66

attribute [local instance] Classical.propDecidable Classical.typeDecidableEq

/-- Theorem II.2 (informal), PDF pp.2-3; proof-defined observable in A.2 p.13.
Printed Tr(O)/2 becomes Tr(O)/4^n; both specialization logarithms retain delta.
The global factor 3 is absorbed only in this order bound. Pure-pair clauses
refer to normalized density matrices. -/
theorem simultaneousNormalizedOverlaps [∀ m : ℕ, Fintype (Clifford.ProjectiveGroup m)] :
    ∃ C : ℝ, 0 < C ∧ ∀ (n M : ℕ), 0 < n → 0 < M →
      ∀ (rho sigma : Fin M → Space n),
        (∀ i, IsDensityMatrix (rho i)) → (∀ i, IsDensityMatrix (sigma i)) →
      ∀ (eps delta : ℝ), 0 < eps → eps < 1 → 0 < delta → delta < 1 →
      let O : Fin M → Space (n + n) := fun i => overlapObservable (rho i) (sigma i)
      let L := Real.log (2 * (M : ℝ) / delta) / eps ^ 2
      (∀ P : MeasurementPrimitive (n + n),
        PrimitiveOverlapsRecover P O
          ⌈C * L * finiteMax (fun i => centeredVariance P (O i))⌉₊ eps delta) ∧
      OverlapsRecover (globalFrame (n + n)) O
        ⌈C * L * finiteMax (fun i => ((O i) ^ 2).trace.re)⌉₊ eps delta ∧
      (∀ s : Fin M → Finset (Fin (n + n)), (∀ i, ActsWithin (s i) (O i)) →
        OverlapsRecover (singleCliffordFrame (n + n)) O
          ⌈C * L * finiteMax (fun i => (4 : ℝ) ^ (s i).card * specNorm (O i) ^ 2)⌉₊
          eps delta) ∧
      (∀ i, (∃ psi : EuclideanSpace ℂ (Qubits n), IsState psi ∧ rho i = pureDensity psi) →
        (∃ psi : EuclideanSpace ℂ (Qubits n), IsState psi ∧ sigma i = pureDensity psi) →
        ((O i) ^ 2).trace.re = 1 ∧ specNorm (O i) ^ 2 = 1) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P66

end

Source

Classical Shadows for Quantum Process Tomography on Near-term Quantum Computers, arXiv:2110.02965v3, PDF p. 2, Theorem II.2 (informal)

Read-back

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

Assume that the quotient of the $m$ -qubit Pauli normalizer by equality of conjugation maps has a supplied finite enumeration for every $m\in\mathbb N$ ; the Pauli subgroup here is generated by all tensor products of Pauli matrices multiplied by $1,i,-1,-i$ . There exists one real constant $C>0$ such that the following holds for every $n>0$ , $M>0$ , every two families $(\rho_i)_{i<M}$ , $(\sigma_i)_{i<M}$ of positive semidefinite $n$ -qubit matrices of trace one, and every $0<\varepsilon,\delta<1$ . Put

O_i=\rho_i^{\mathsf T}\otimes\sigma_i, \qquad L=\frac{\log(2M/\delta)}{\varepsilon^2},

with tensor indices identified with concatenated bit strings. For any channel $\mathcal E(X)=\sum_jK_jXK_j^\dagger$ , where the Kraus family is finite and $\sum_jK_j^\dagger K_j=I$ , write

(C_{\mathcal E})_{(a,b),(a',b')}= 2^{-n}\bigl[\mathcal E(|a\rangle\langle a'|)\bigr]_{b,b'}.

First, for every measurement primitive $P$ on $2n$ qubits, there exists an estimator from $N_P$ unitary/outcome records to $M$ real numbers that, for every such channel, simultaneously estimates all $\operatorname{Re}\operatorname{Tr}(O_iC_{\mathcal E})$ to absolute error at most $\varepsilon$ , on a set of record measure at least $1-\delta$ , where

N_P=\max\!\left\{0,\left\lceil CL\max_{i<M}V_P(O_i)\right\rceil\right\}.

Here $P$ consists of a probability measure $\mu_P$ on unitaries for which

\mathcal M_P(X)= \int\sum_b\operatorname{Tr}(U^\dagger|b\rangle\langle b|U\,X) \,U^\dagger|b\rangle\langle b|U\,d\mu_P(U)

is injective, and its inverse is the inverse complex linear map. The single-record law has density $\max\{\operatorname{Re}(UC_{\mathcal E}U^\dagger)_{bb},0\}$ against $\mu_P$ , summed over $b$ , and records have the product law. For a Hermitian $O$ , define $O^\circ=O-2^{-2n}\operatorname{Tr}(O)I$ and

V_P(O)= \left[ \sqrt{\sup_{\substack{\tau\succeq0\\\operatorname{Tr}\tau=1}} \int\sum_b \operatorname{Re}(U\tau U^\dagger)_{bb} \left(\operatorname{Re}[U\mathcal M_P^{-1}(O^\circ)U^\dagger]_{bb}\right)^2 \,d\mu_P(U)} \right]^2;

the definition sets $V_P(O)=0$ for non-Hermitian $O$ . The supremum is the real-number supremum used in the displayed definition, and the square root is the real square root. Second, the global Clifford frame admits such simultaneous estimators with

N_{\mathrm{global}} =\max\!\left\{0,\left\lceil CL\max_{i<M}\operatorname{Re}\operatorname{Tr}(O_i^2) \right\rceil\right\}.

Its basis choices are the quotient classes above, its matrices are $Q_{a,b}=U_a^\dagger|b\rangle\langle b|U_a$ for chosen representatives, and the weight of a record $r$ is

\prod_{j<N}\frac{\operatorname{Re}\operatorname{Tr}(Q_{r_j}C_{\mathcal E})} {|\operatorname{Basis}|};

the weight of an event is the finite sum of these products over records in that event. Third, for every family of wire sets $s_i\subseteq\{0,\ldots,2n-1\}$ such that $O_i$ acts within $s_i$ , the tensor product of independent single-qubit global Clifford frames admits such simultaneous estimators with

N_{\mathrm{single}} =\max\!\left\{0,\left\lceil CL\max_{i<M}4^{|s_i|}\|O_i\|_{\mathrm{op}}^2 \right\rceil\right\}.

Acting within $s_i$ means that there exist a natural number $q$ , an injection $w:\{0,\ldots,q-1\}\hookrightarrow\{0,\ldots,2n-1\}$ with image contained in $s_i$ , and a $q$ -qubit matrix $A$ , such that

(O_i)_{y,z}= \begin{cases} A_{y\circ w,z\circ w},&y,z\text{ agree outside the image of }w,\\ 0,&\text{otherwise}. \end{cases}

The tensor frame uses the product basis choices and tensor products of their projectors, with the same finite record-weight rule. Each recovery assertion requires one estimator that works for every channel, but imposes no measurability condition on that estimator. Finally, for each $i<M$ , if $\rho_i=\psi\psi^\dagger$ for some unit vector $\psi$ and $\sigma_i=\phi\phi^\dagger$ for some unit vector $\phi$ , then

\operatorname{Re}\operatorname{Tr}(O_i^2)=1 \quad\text{and}\quad \|O_i\|_{\mathrm{op}}^2=1.

The sample counts are natural-number ceilings clipped below at zero and are not required to be positive.

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