Simultaneous normalized reduced-process tomography

Open

QAlgorithms.Papers.Independent.Intakethird100.P66.simultaneousReducedInformal

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

prove2quantum

Let $\mathcal E$ be any CPTP map on $n\ge1$ qubits, and let $\rho_{\Lambda}=2^{-n}\Lambda_{\mathcal E}$ be its trace-one reference-first Choi state. For $0\le k\le n$ , let $\rho_{\Lambda,S}$ retain the reference and output copies of a $k$ -element physical subsystem $S$ , tracing out both complements. Fix $0<\epsilon,\delta<1$ .

There is an absolute $C>0$ , uniform over all these data, such that the following independent fresh-shot counts suffice to estimate every $\rho_{\Lambda,S}$ with one simultaneous success event of probability at least $1-\delta$ in the indicated norm:

\begin{array}{ll} \text{global Clifford, Frobenius:}&\left\lceil C4^{n+k}\epsilon^{-2}\log(2(8n)^{2k}/\delta)\right\rceil,\\ \text{Pauli-6, Frobenius:}&\left\lceil C36^k\epsilon^{-2}\log(2(8n)^{2k}/\delta)\right\rceil,\\ \text{Pauli-6, trace:}&\left\lceil C144^k\epsilon^{-2}\log((24n)^{2k}/\delta)\right\rceil. \end{array}

The trace norm has no extra factor $1/2$ . At $k=0$ the scalar marginal $1$ requires no samples. For fixed $k,\epsilon,\delta$ , a Pauli-6 count $N\le D_{k,\epsilon,\delta}\log(2n)$ suffices for either norm, uniformly in $n$ and the process. Each estimator is chosen before the unknown process. The reduced channel has a maximally mixed complementary input.

This is a quantum sample guarantee, including full tomography at $k=n$ , without a unitarity promise or a total classical runtime bound.

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.1 (informal), PDF p.2, with A.3 p.14: all three
norm/ensemble clauses and the fixed-k logarithmic sample consequence.
Constants precede system size, accuracy, confidence, and unknown process. -/
theorem simultaneousReducedInformal [∀ m : ℕ, Fintype (Clifford.ProjectiveGroup m)] :
    (∃ C : ℝ, 0 < C ∧ ∀ (n k : ℕ), 0 < n → k ≤ n →
      ∀ (eps delta : ℝ), 0 < eps → eps < 1 → 0 < delta → delta < 1 →
        ReducedRecovers (globalFrame (n + n)) k
          (sampleCount k (C * (4 : ℝ) ^ (n + k) / eps ^ 2 * reducedLog n k delta))
          .frobenius eps delta ∧
        ReducedRecovers (pauliFrame (n + n)) k
          (sampleCount k (C * (36 : ℝ) ^ k / eps ^ 2 * reducedLog n k delta))
          .frobenius eps delta ∧
        ReducedRecovers (pauliFrame (n + n)) k
          (sampleCount k (C * (144 : ℝ) ^ k / eps ^ 2 * traceSampleLog n k delta))
          .trace eps delta) ∧
    (∀ (k : ℕ) (eps delta : ℝ), 0 < eps → eps < 1 → 0 < delta → delta < 1 →
      ∃ D : ℝ, 0 < D ∧ ∀ n : ℕ, 0 < n → k ≤ n →
        ∃ N : ℕ, (N : ℝ) ≤ D * Real.log (2 * (n : ℝ)) ∧
          ReducedRecovers (pauliFrame (n + n)) k N .frobenius eps delta ∧
          ReducedRecovers (pauliFrame (n + n)) k N .trace eps delta) := 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.1 (informal)

Read-back

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

Assume that, for every natural number $m$ , a finite enumeration is supplied for the following quotient: take the unitary matrices on $m$ qubits that normalize the subgroup generated by all matrices $i^cP_1\otimes\cdots\otimes P_m$ , where $c\in\{0,1,2,3\}$ and each $P_j$ is a Pauli matrix, and identify two normalizing unitaries when their conjugation maps $X\mapsto UXU^\dagger$ agree on every matrix. The theorem asserts both the existence of a single constant $C>0$ and a further statement with constants depending on the requested accuracy and subsystem size. To state these assertions, for a finite basis frame $F$ , write $Q^F_{a,b}$ for its matrix indexed by a basis choice $a$ and a bit string $b$ ; its record weight for a matrix $\rho$ is

p_F(a,b;\rho)=\frac{\operatorname{Re}\operatorname{Tr}(Q^F_{a,b}\rho)} {|\operatorname{Basis}(F)|}, \qquad \Pr_{F,\rho}^{N}(A)= \sum_{r\in(\operatorname{Basis}(F)\times\{0,1\}^{2n})^N} \mathbf1_A(r)\prod_{j<N}p_F(r_j;\rho).

The global frame on $2n$ qubits uses the quotient just described as its basis choices and $Q^F_{a,b}=U_a^\dagger|b\rangle\langle b|U_a$ , for the chosen representative $U_a$ of each quotient class. The Pauli frame has basis choices $a=(A_j,s_j)_{j<2n}$ , with $A_j\in\{X,Y,Z\}$ , $s_j\in\{-1,1\}$ , and

Q^F_{a,b}=\bigotimes_{j<2n}\frac{I+s_j(-1)^{b_j}A_j}{2}.

For any channel $\mathcal E(X)=\sum_jK_jXK_j^\dagger$ with finitely many Kraus matrices satisfying $\sum_jK_j^\dagger K_j=I$ , let

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

For an injection $w:\{0,\ldots,k-1\}\hookrightarrow\{0,\ldots,n-1\}$ , its reduced matrix $C_{\mathcal E,w}$ has entries

(C_{\mathcal E,w})_{(u,v),(u',v')}= \sum_{\substack{a,b\in\{0,1\}^n\\a\circ w=b\circ w=0}} (C_{\mathcal E})_{(a[w\leftarrow u],\,b[w\leftarrow v]), (a[w\leftarrow u'],\,b[w\leftarrow v'])},

where $a[w\leftarrow u]$ overwrites coordinate $w(j)$ of $a$ by $u_j$ . Say that $F$ recovers these reduced matrices with $N$ records in a specified norm if there exists an estimator, independent of $\mathcal E$ , assigning a complex matrix on $2k$ qubits to each record and each injection $w$ , such that for every such channel the record weight of the event $\forall w,\ \|\widehat C(r,w)-C_{\mathcal E,w}\|\le\varepsilon$ is at least $1-\delta$ ; no measurability, positivity, or normalization requirement is imposed on the estimator. The norms used are the Frobenius norm and the trace norm $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . For every $n>0$ , $0\le k\le n$ , and $0<\varepsilon,\delta<1$ , the single constant $C>0$ makes all three recovery assertions hold, with respective record counts

\begin{aligned} N_{\mathrm{global,F}} &=s_k\!\left(\frac{C\,4^{n+k}}{\varepsilon^2} \log\frac{2(8n)^{2k}}{\delta}\right),\\ N_{\mathrm{Pauli,F}} &=s_k\!\left(\frac{C\,36^k}{\varepsilon^2} \log\frac{2(8n)^{2k}}{\delta}\right),\\ N_{\mathrm{Pauli,1}} &=s_k\!\left(\frac{C\,144^k}{\varepsilon^2} \log\frac{(24n)^{2k}}{\delta}\right), \end{aligned} \qquad s_k(B)= \begin{cases} 0,&k=0,\\ \max\{0,\lceil B\rceil\},&k\ne0. \end{cases}

Separately, for every fixed $k\in\mathbb N$ and $0<\varepsilon,\delta<1$ , there exists $D>0$ such that for every $n>0$ with $k\le n$ , there exists one natural number $N\le D\log(2n)$ for which the Pauli frame recovers all these reductions in both norms. Those two recovery assertions may use different estimators. The case $k=0$ is included throughout; the first three counts are then exactly zero.

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