Machine Learning

Motivation

Provably efficient machine learning for quantum many-body problems establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Fix a finite spatial dimension $d$, bounds on the number and geometric radius of sites in each Hamiltonian term, a local-term density bound $b_d+c_dr^d$, a spectral gap $\gamma>0$, an observable locality bound $q$, and a confidence parameter $\delta\in(0,1)$. Consider $n$-qubit Hamiltonians $H(x)=\sum_j h_j(x)$, smoothly parametrized by $x\in[-1,1]^m$. Each term is Hermitian, obeys $\|h_j(x)\|_\infty\le1$, and has directional derivative of operator norm at most one in every Euclidean unit parameter direction. These properties hold throughout the cube; smoothness at its boundary uses a local smooth extension. Every Hamiltonian has an excited energy and a gap at least $\gamma$ above its entire ground eigenspace. Let $\rho(x)$ be the normalized projector onto that eigenspace, allowing degeneracy.

For a fixed Hermitian observable $O=\sum_{i=1}^L O_i$, each term supported on at most $q$ qubits (not necessarily neighboring), choose a norm budget $B\ge1$ satisfying $\sum_i\|O_i\|_\infty\le B$. A smaller norm budget may be replaced by one. There are uniform positive constants, depending only on the fixed physical bounds, $q$, and $\delta$, such that for every fixed mean-squared error tolerance $\varepsilon\in(0,1]$ and all sufficiently large $m$, public sample counts, cutoffs, and actual classical arithmetic/RAM programs can be selected before the unknown Hamiltonian family, training draw, observable entries, and test parameter. The training set consists of $N$ independent uniform parameter draws, with one fresh-copy randomized Pauli snapshot $S_\ell$ at each point. Pauli axes are independently uniform; the joint measurement outcomes obey the Born law.

The named predictor is

$$\widehat{\sigma}_N(x)=\frac1N\sum_{\ell=1}^N\kappa_\Lambda(x,x_\ell)S_\ell,\qquad \kappa_\Lambda(x,y)=\sum_{\substack{k\in\mathbb Z^m\\\|k\|_2\le\Lambda}} \cos\!\bigl(\pi k\cdot(x-y)\bigr).$$

For each observable fixed before the training draw,

$$\Pr_{\mathcal T}\!\left[ \mathbb E_{x\sim\mathrm{Unif}[-1,1]^m} \left|\operatorname{tr}\!\left(O\widehat{\sigma}_N(x)\right) -\operatorname{tr}\!\left(O\rho(x)\right)\right|^2 \le\varepsilon\right]\ge1-\delta,$$

with $N\le C B^2m^{C B^2/\varepsilon}$ and computed classical training and prediction work $O((n+L)B^2m^{O(B^2/\varepsilon)})$. The compact representation stores $mN$ real parameter words and $nN$ six-valued labels, encodable in $3nN$ bits. The programs read and store those data and compute the observable value; they do not materialize the represented matrix. Ground-state preparation and data generation are excluded from this classical work.

For every fixed subsystem $A$ of at most $q$ qubits, separately with confidence at least $1-\delta$,

$$\mathbb E_x\left\|\operatorname{tr}_{A^{\mathrm c}} \bigl(\widehat{\sigma}_N(x)-\rho(x)\bigr)\right\|_1 \le\sqrt{4^q\varepsilon}.$$

Thus taking $\varepsilon=\eta^2/4^q$ gives the informal constant trace-norm error $\eta$ on a fixed few-body reduced matrix. This conversion uses the finite Pauli expansion and allocates confidence $\delta/4^q$ to its coefficients; it leaves the polynomial-in-$m$, linear-in-$n$ conclusion intact at fixed accuracy and locality.

This result describes generalization in population average for the source's compact shadow predictor. It asserts neither pointwise error nor simultaneous accuracy on all observables or subsystems, and does not require the predicted representation to be positive or trace one.

Formalization Note Theorem 3 on PDF pp.29–30 explicitly identifies itself as the detailed restatement of Theorem 1. Its Eq. (F3) prints exact ground-state labels, whereas its premise and Eqs. (2), (E3), and (F27) specify shadow labels; the latter determine the model above. This discrepancy and the nonperiodic-boundary gap in Lemma 2 are recorded for independent source moderation, without adding periodicity or a gradient bound as hypotheses.

Target

Theorem 1; detailed Theorem 3, PDF pp.29–30

Fix a finite spatial dimension $d$, bounds on the number and geometric radius of sites in each Hamiltonian term, a local-term density bound $b_d+c_dr^d$, a spectral gap $\gamma>0$, an observable locality bound $q$, and a confidence parameter $\delta\in(0,1)$. Consider $n$-qubit Hamiltonians $H(x)=\sum_j h_j(x)$, smoothly parametrized by $x\in[-1,1]^m$. Each term is Hermitian, obeys $\|h_j(x)\|_\infty\le1$, and has directional derivative of operator norm at most one in every Euclidean unit parameter direction. These properties hold throughout the cube; smoothness at its boundary uses a local smooth extension. Every Hamiltonian has an excited energy and a gap at least $\gamma$ above its entire ground eigenspace. Let $\rho(x)$ be the normalized projector onto that eigenspace, allowing degeneracy.

For a fixed Hermitian observable $O=\sum_{i=1}^L O_i$, each term supported on at most $q$ qubits (not necessarily neighboring), choose a norm budget $B\ge1$ satisfying $\sum_i\|O_i\|_\infty\le B$. A smaller norm budget may be replaced by one. There are uniform positive constants, depending only on the fixed physical bounds, $q$, and $\delta$, such that for every fixed mean-squared error tolerance $\varepsilon\in(0,1]$ and all sufficiently large $m$, public sample counts, cutoffs, and actual classical arithmetic/RAM programs can be selected before the unknown Hamiltonian family, training draw, observable entries, and test parameter. The training set consists of $N$ independent uniform parameter draws, with one fresh-copy randomized Pauli snapshot $S_\ell$ at each point. Pauli axes are independently uniform; the joint measurement outcomes obey the Born law.

The named predictor is

$$\widehat{\sigma}_N(x)=\frac1N\sum_{\ell=1}^N\kappa_\Lambda(x,x_\ell)S_\ell,\qquad \kappa_\Lambda(x,y)=\sum_{\substack{k\in\mathbb Z^m\\\|k\|_2\le\Lambda}} \cos\!\bigl(\pi k\cdot(x-y)\bigr).$$

For each observable fixed before the training draw,

$$\Pr_{\mathcal T}\!\left[ \mathbb E_{x\sim\mathrm{Unif}[-1,1]^m} \left|\operatorname{tr}\!\left(O\widehat{\sigma}_N(x)\right) -\operatorname{tr}\!\left(O\rho(x)\right)\right|^2 \le\varepsilon\right]\ge1-\delta,$$

with $N\le C B^2m^{C B^2/\varepsilon}$ and computed classical training and prediction work $O((n+L)B^2m^{O(B^2/\varepsilon)})$. The compact representation stores $mN$ real parameter words and $nN$ six-valued labels, encodable in $3nN$ bits. The programs read and store those data and compute the observable value; they do not materialize the represented matrix. Ground-state preparation and data generation are excluded from this classical work.

For every fixed subsystem $A$ of at most $q$ qubits, separately with confidence at least $1-\delta$,

$$\mathbb E_x\left\|\operatorname{tr}_{A^{\mathrm c}} \bigl(\widehat{\sigma}_N(x)-\rho(x)\bigr)\right\|_1 \le\sqrt{4^q\varepsilon}.$$

Thus taking $\varepsilon=\eta^2/4^q$ gives the informal constant trace-norm error $\eta$ on a fixed few-body reduced matrix. This conversion uses the finite Pauli expansion and allocates confidence $\delta/4^q$ to its coefficients; it leaves the polynomial-in-$m$, linear-in-$n$ conclusion intact at fixed accuracy and locality.

This result describes generalization in population average for the source's compact shadow predictor. It asserts neither pointwise error nor simultaneous accuracy on all observables or subsystems, and does not require the predicted representation to be positive or trace one.

Formalization Note Theorem 3 on PDF pp.29–30 explicitly identifies itself as the detailed restatement of Theorem 1. Its Eq. (F3) prints exact ground-state labels, whereas its premise and Eqs. (2), (E3), and (F27) specify shadow labels; the latter determine the model above. This discrepancy and the nonperiodic-boundary gap in Lemma 2 are recorded for independent source moderation, without adding periodicity or a gradient bound as hypotheses.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Provably efficient machine learning for quantum many-body problems, arXiv:2106.12627v4. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Foundations for learning from noisy quantum experiments establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Fix a positive finite dimension $d$ and finite labelled sets $X,Y,Z,B$ of preparation actions, dynamics actions, measurement actions, and measurement outcomes. Let $\mathcal Q$ be any set of world models $W=(\{\rho_x\}_{x\in X},\{\mathcal E_y\}_{y\in Y},\{M_{zb}\}_{z\in Z,b\in B})$ on $\mathbb C^d$: every preparation is a density matrix, every dynamics action is a CPTP map, and each measurement is a POVM. The model class may be uncountable and may contain equivalent descriptions.

Suppose every $W\in\mathcal Q$ is universal: some preparation is pure; some finite collection of dynamics actions implements exact unitary channels whose representatives generate a dense subgroup of $\mathrm{SU}(d)$; and some measurement effect is not proportional to the identity. These witnessing actions and their physical descriptions are unknown and may vary between worlds. Mathematical inverses enter the generated subgroup; physical access to inverse actions is not assumed.

Then there exists a fixed family $(L_k)_{k\in\mathbb N}$ of finite classical experimental procedures, chosen before the unknown world. Each procedure adaptively chooses experiments that freshly prepare $\rho_x$, apply a finite word of the available dynamics actions, and measure one of the available POVMs. Its description output is denoted $\widehat W^{(k)}=(\{\widehat\rho_x^{(k)}\},\{\widehat{\mathcal E}_y^{(k)}\},\{\widehat M_{zb}^{(k)}\})$. For every $W\in\mathcal Q$, every $\epsilon>0$, and every $0<\delta<1$, there exists $k_0$ such that for all $k\ge k_0$ there is one unitary or anti-unitary gauge $\mathcal G$ satisfying

$$\begin{aligned} \Pr_W\!\left[\|\rho_x-\mathcal G(\widehat\rho_x^{(k)})\|_1\le\epsilon\right]&\ge1-\delta &&(x\in X),\\ \Pr_W\!\left[\|\mathcal E_y-\mathcal G\circ\widehat{\mathcal E}_y^{(k)}\circ\mathcal G^{-1}\|_\diamond\le\epsilon\right]&\ge1-\delta &&(y\in Y),\\ \Pr_W\!\left[\|M_{zb}-\mathcal G(\widehat M_{zb}^{(k)})\|_1\le\epsilon\right]&\ge1-\delta &&(z\in Z,\ b\in B). \end{aligned}$$

Here $\Pr_W$ is computed from the experimental outcome probabilities and internal classical randomization of $L_k$. A unitary gauge has the form $\mathcal G(A)=UAU^\dagger$; an anti-unitary gauge has the form $\mathcal G(A)=U\overline A U^\dagger$. The same gauge is fixed outside all three collections of probability clauses. Both norms are unhalved. The output estimates need not themselves be lawful quantum objects.

The result establishes learnability of all labelled operations from untrusted experiments under universality. It gives eventual accuracy for each world, with no uniform sample bound, polynomial complexity guarantee, or certified accuracy-based stopping rule.

Formalization Note The finite-action scope is explicit in Theorem D.1 (PDF p.21), although the main-text Theorem 2 does not explicitly restrict the action sets. The stage-indexed interpretation follows the precision-halving procedure in D.2 (p.23) and D.7 (p.33).

Target

Theorem 2; formal restatement Theorem D.1 (PDF p.21)

Fix a positive finite dimension $d$ and finite labelled sets $X,Y,Z,B$ of preparation actions, dynamics actions, measurement actions, and measurement outcomes. Let $\mathcal Q$ be any set of world models $W=(\{\rho_x\}_{x\in X},\{\mathcal E_y\}_{y\in Y},\{M_{zb}\}_{z\in Z,b\in B})$ on $\mathbb C^d$: every preparation is a density matrix, every dynamics action is a CPTP map, and each measurement is a POVM. The model class may be uncountable and may contain equivalent descriptions.

Suppose every $W\in\mathcal Q$ is universal: some preparation is pure; some finite collection of dynamics actions implements exact unitary channels whose representatives generate a dense subgroup of $\mathrm{SU}(d)$; and some measurement effect is not proportional to the identity. These witnessing actions and their physical descriptions are unknown and may vary between worlds. Mathematical inverses enter the generated subgroup; physical access to inverse actions is not assumed.

Then there exists a fixed family $(L_k)_{k\in\mathbb N}$ of finite classical experimental procedures, chosen before the unknown world. Each procedure adaptively chooses experiments that freshly prepare $\rho_x$, apply a finite word of the available dynamics actions, and measure one of the available POVMs. Its description output is denoted $\widehat W^{(k)}=(\{\widehat\rho_x^{(k)}\},\{\widehat{\mathcal E}_y^{(k)}\},\{\widehat M_{zb}^{(k)}\})$. For every $W\in\mathcal Q$, every $\epsilon>0$, and every $0<\delta<1$, there exists $k_0$ such that for all $k\ge k_0$ there is one unitary or anti-unitary gauge $\mathcal G$ satisfying

$$\begin{aligned} \Pr_W\!\left[\|\rho_x-\mathcal G(\widehat\rho_x^{(k)})\|_1\le\epsilon\right]&\ge1-\delta &&(x\in X),\\ \Pr_W\!\left[\|\mathcal E_y-\mathcal G\circ\widehat{\mathcal E}_y^{(k)}\circ\mathcal G^{-1}\|_\diamond\le\epsilon\right]&\ge1-\delta &&(y\in Y),\\ \Pr_W\!\left[\|M_{zb}-\mathcal G(\widehat M_{zb}^{(k)})\|_1\le\epsilon\right]&\ge1-\delta &&(z\in Z,\ b\in B). \end{aligned}$$

Here $\Pr_W$ is computed from the experimental outcome probabilities and internal classical randomization of $L_k$. A unitary gauge has the form $\mathcal G(A)=UAU^\dagger$; an anti-unitary gauge has the form $\mathcal G(A)=U\overline A U^\dagger$. The same gauge is fixed outside all three collections of probability clauses. Both norms are unhalved. The output estimates need not themselves be lawful quantum objects.

The result establishes learnability of all labelled operations from untrusted experiments under universality. It gives eventual accuracy for each world, with no uniform sample bound, polynomial complexity guarantee, or certified accuracy-based stopping rule.

Formalization Note The finite-action scope is explicit in Theorem D.1 (PDF p.21), although the main-text Theorem 2 does not explicitly restrict the action sets. The stage-indexed interpretation follows the precision-halving procedure in D.2 (p.23) and D.7 (p.33).

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Foundations for learning from noisy quantum experiments, arXiv:2204.13691v1. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Robust shadow estimation establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Consider Protocol 1 of Chen, Yu, Zeng and Flammia on $n\ge 1$ qubits, with Hilbert space dimension $d=2^n$. The same completely positive, trace-preserving noise channel $\Lambda$ acts after each ideal global Clifford gate; fixed computational-basis measurement noise is absorbed into $\Lambda$. Calibration perfectly prepares $|0\rangle^{\otimes n}$. The full Clifford group modulo global phase is sampled uniformly and calibration shots are independent and identically distributed.

Let $\varepsilon>0$ and $0<\delta\le 1$. Define the Z-basis average fidelity by $F_Z(\Lambda)=d^{-1}\sum_b\langle b|\Lambda(|b\rangle\langle b|)|b\rangle$, and suppose $F_Z(\Lambda)>1/d$. Set

$$A=\frac{(1+\varepsilon^2)(1+1/d)^2}{\varepsilon^2(F_Z(\Lambda)-1/d)^2}.$$

The printed sample scale in Theorem 7 is $R_{\rm printed}=136\ln(2/\delta)A$. Interpret its real-valued batch parameters operationally as positive integers $N\ge\lceil68A\rceil$ and $K\ge\lceil2\ln(2/\delta)\rceil$, with actual calibration count $R=NK$.

For each recorded ideal Clifford $U$ and noisy outcome $b$, compute $\widehat f^{(r)}=(d|\langle b|U(|0\rangle^{\otimes n})|^2-1)/(d-1)$. Let $\widehat f$ be the median of the $K$ means of batches of $N$ such scores. The estimated inverse sends an operator $X$ to $(\operatorname{Tr}X/d)I+\widehat f^{-1}(X-(\operatorname{Tr}X/d)I)$. Let $\widetilde{\mathcal M}(X)=\mathbb E_U[U^\dagger\mathcal M_Z(\Lambda(UXU^\dagger))U]$, where $\mathcal M_Z$ removes off-diagonal computational-basis entries, and let $O_0=O-(\operatorname{Tr}O/d)I$.

With probability at least $1-\delta$ over calibration records, $\widehat f\ne0$ and the subsequent single-shot retrieval expectation satisfies, simultaneously for every Hermitian observable $O$ and every density matrix $\rho$,

$$\left|\mathbb E_{U,b\mid\rho}[\operatorname{Tr}(O\widehat{\mathcal M}^{-1}(U^\dagger|b\rangle\langle b|U))]-\operatorname{Tr}(O\rho)\right| =\left|\operatorname{Tr}(O\widehat{\mathcal M}^{-1}\widetilde{\mathcal M}(\rho))-\operatorname{Tr}(O\rho)\right| \le\varepsilon\|O_0\|_\infty.$$

Here $\|\cdot\|_\infty$ is the operator norm, and the expectation is conditional on the calibration result. This guarantee controls the systematic, asymptotic bias of robust shadow retrieval; it applies to all observables and states on the same successful calibration event.

Formalization Note The statement retains the printed $1+\varepsilon^2$ factor. The source proof's substitution instead gives $(1+\varepsilon)^2$ from the stated variance bound; this discrepancy and the integer rounding interpretation remain subject to independent source moderation. The product of rounded batch parameters is not asserted to equal, or be bounded above by the ceiling of, the printed total scale. The frozen calibration probability law, overlap scores, median and retrieval expectation compute the named protocol directly.

Target

Theorem 7, Eqs. (B24)-(B25), Protocol 1

Consider Protocol 1 of Chen, Yu, Zeng and Flammia on $n\ge 1$ qubits, with Hilbert space dimension $d=2^n$. The same completely positive, trace-preserving noise channel $\Lambda$ acts after each ideal global Clifford gate; fixed computational-basis measurement noise is absorbed into $\Lambda$. Calibration perfectly prepares $|0\rangle^{\otimes n}$. The full Clifford group modulo global phase is sampled uniformly and calibration shots are independent and identically distributed.

Let $\varepsilon>0$ and $0<\delta\le 1$. Define the Z-basis average fidelity by $F_Z(\Lambda)=d^{-1}\sum_b\langle b|\Lambda(|b\rangle\langle b|)|b\rangle$, and suppose $F_Z(\Lambda)>1/d$. Set

$$A=\frac{(1+\varepsilon^2)(1+1/d)^2}{\varepsilon^2(F_Z(\Lambda)-1/d)^2}.$$

The printed sample scale in Theorem 7 is $R_{\rm printed}=136\ln(2/\delta)A$. Interpret its real-valued batch parameters operationally as positive integers $N\ge\lceil68A\rceil$ and $K\ge\lceil2\ln(2/\delta)\rceil$, with actual calibration count $R=NK$.

For each recorded ideal Clifford $U$ and noisy outcome $b$, compute $\widehat f^{(r)}=(d|\langle b|U(|0\rangle^{\otimes n})|^2-1)/(d-1)$. Let $\widehat f$ be the median of the $K$ means of batches of $N$ such scores. The estimated inverse sends an operator $X$ to $(\operatorname{Tr}X/d)I+\widehat f^{-1}(X-(\operatorname{Tr}X/d)I)$. Let $\widetilde{\mathcal M}(X)=\mathbb E_U[U^\dagger\mathcal M_Z(\Lambda(UXU^\dagger))U]$, where $\mathcal M_Z$ removes off-diagonal computational-basis entries, and let $O_0=O-(\operatorname{Tr}O/d)I$.

With probability at least $1-\delta$ over calibration records, $\widehat f\ne0$ and the subsequent single-shot retrieval expectation satisfies, simultaneously for every Hermitian observable $O$ and every density matrix $\rho$,

$$\left|\mathbb E_{U,b\mid\rho}[\operatorname{Tr}(O\widehat{\mathcal M}^{-1}(U^\dagger|b\rangle\langle b|U))]-\operatorname{Tr}(O\rho)\right| =\left|\operatorname{Tr}(O\widehat{\mathcal M}^{-1}\widetilde{\mathcal M}(\rho))-\operatorname{Tr}(O\rho)\right| \le\varepsilon\|O_0\|_\infty.$$

Here $\|\cdot\|_\infty$ is the operator norm, and the expectation is conditional on the calibration result. This guarantee controls the systematic, asymptotic bias of robust shadow retrieval; it applies to all observables and states on the same successful calibration event.

Formalization Note The statement retains the printed $1+\varepsilon^2$ factor. The source proof's substitution instead gives $(1+\varepsilon)^2$ from the stated variance bound; this discrepancy and the integer rounding interpretation remain subject to independent source moderation. The product of rounded batch parameters is not asserted to equal, or be bounded above by the ceiling of, the printed total scale. The frozen calibration probability law, overlap scores, median and retrieval expectation compute the named protocol directly.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Robust shadow estimation, arXiv:2011.09636v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Predicting Many Properties of a Quantum System from Very Few Measurements establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $n\ge0$, $d=2^n$, and let $\rho$ be any density matrix on an $n$-qubit system. Fix a tomographically complete measurement primitive: a probability ensemble $\mu$ of unitary matrices, whose averaged measurement channel $\mathcal M$ is invertible. A shot samples $U\sim\mu$, measures $U\rho U^\dagger$ in the computational basis with Born outcome $b$, and forms the snapshot $\widehat\rho=\mathcal M^{-1}(U^\dagger|b\rangle\langle b|U)$. The ensemble may be continuous and need not be uniform.

Fix $M\ge1$ Hermitian observables $O_1,\ldots,O_M$, independently of the sampled outcomes, and $0<\varepsilon\le1$, $0<\delta\le1$. For a Hermitian matrix $A$, define

$$\|A\|_{\mathrm{shadow}}^2=\max_{\sigma\text{ a density matrix}}\mathbb E_{U\sim\mu}\sum_{b\in\{0,1\}^n}\langle b|U\sigma U^\dagger|b\rangle\,\langle b|U\mathcal M^{-1}(A)U^\dagger|b\rangle^2.$$

Set $V=\max_{1\le i\le M}\|O_i-\operatorname{tr}(O_i)I/d\|_{\mathrm{shadow}}^2$, $K=\lceil2\log(2M/\delta)\rceil$, and $N=\max\{1,\lceil34V/\varepsilon^2\rceil\}$. Here $\log$ is natural logarithm. Draw exactly $KN$ independent snapshots in $K$ batches of $N$ shots. Let $\widehat o_i$ be the median of the $K$ batch means of $\operatorname{tr}(O_i\widehat\rho)$, using the lower median for even $K$. Then

$$\Pr\!\left[\forall i\in\{1,\ldots,M\},\quad |\widehat o_i-\operatorname{tr}(O_i\rho)|\le\varepsilon\right]\ge1-\delta.$$

This is the paper's simultaneous linear-prediction guarantee, with observable-dependent sample size and no purity, locality, positivity, operator-norm, or computational-cost restriction on the observables.

Formalization Note The printed zero endpoints in (S13) are undefined and are excluded. Integer counts are rounded upward and each batch has at least one sample, including scalar observables with $V=0$. Lean concludes positivity of the constructed counts instead of assuming it. Real parts of traces express the real expectations of Hermitian observables.

Target

Supplementary Information §1.B, Theorem 1, Eqs. (S13)–(S14)

Let $n\ge0$, $d=2^n$, and let $\rho$ be any density matrix on an $n$-qubit system. Fix a tomographically complete measurement primitive: a probability ensemble $\mu$ of unitary matrices, whose averaged measurement channel $\mathcal M$ is invertible. A shot samples $U\sim\mu$, measures $U\rho U^\dagger$ in the computational basis with Born outcome $b$, and forms the snapshot $\widehat\rho=\mathcal M^{-1}(U^\dagger|b\rangle\langle b|U)$. The ensemble may be continuous and need not be uniform.

Fix $M\ge1$ Hermitian observables $O_1,\ldots,O_M$, independently of the sampled outcomes, and $0<\varepsilon\le1$, $0<\delta\le1$. For a Hermitian matrix $A$, define

$$\|A\|_{\mathrm{shadow}}^2=\max_{\sigma\text{ a density matrix}}\mathbb E_{U\sim\mu}\sum_{b\in\{0,1\}^n}\langle b|U\sigma U^\dagger|b\rangle\,\langle b|U\mathcal M^{-1}(A)U^\dagger|b\rangle^2.$$

Set $V=\max_{1\le i\le M}\|O_i-\operatorname{tr}(O_i)I/d\|_{\mathrm{shadow}}^2$, $K=\lceil2\log(2M/\delta)\rceil$, and $N=\max\{1,\lceil34V/\varepsilon^2\rceil\}$. Here $\log$ is natural logarithm. Draw exactly $KN$ independent snapshots in $K$ batches of $N$ shots. Let $\widehat o_i$ be the median of the $K$ batch means of $\operatorname{tr}(O_i\widehat\rho)$, using the lower median for even $K$. Then

$$\Pr\!\left[\forall i\in\{1,\ldots,M\},\quad |\widehat o_i-\operatorname{tr}(O_i\rho)|\le\varepsilon\right]\ge1-\delta.$$

This is the paper's simultaneous linear-prediction guarantee, with observable-dependent sample size and no purity, locality, positivity, operator-norm, or computational-cost restriction on the observables.

Formalization Note The printed zero endpoints in (S13) are undefined and are excluded. Integer counts are rounded upward and each batch has at least one sample, including scalar observables with $V=0$. Lean concludes positivity of the constructed counts instead of assuming it. Real parts of traces express the real expectations of Hermitian observables.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Predicting Many Properties of a Quantum System from Very Few Measurements, arXiv:2002.08953v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Shadow Tomography of Quantum States establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

There are universal constants $C>0$ and $p\in\mathbb N$ and one explicit adaptive measurement constructor with the following property. Let $D,M\ge1$ be integers, let $E_1,\ldots,E_M$ be known two-outcome measurement effects on $\mathbb C^D$ (so $0\preceq E_i\preceq I$), and let $0<\varepsilon,\delta<1$. The constructor depends on these known data and not on the unknown state.

Write $L_D=\max\{1,\log D\}$, $L_M=\max\{1,\log M\}$, $L_\delta=\max\{1,\log(1/\delta)\}$, $L_\varepsilon=\max\{1,\log(1/\varepsilon)\}$, $L_{LM}=\max\{1,\log L_M\}$, and $L_{LD}=\max\{1,\log L_D\}$. The constructed procedure uses $k$ independent copies of the unknown state, with

$$k\le\left\lceil C\varepsilon^{-4}L_\delta L_M^4 L_D(1+L_{LM}+L_{LD}+L_\varepsilon)^p\right\rceil.$$

For every density matrix $\rho$ on $\mathbb C^D$, a run on $\rho^{\otimes k}$ returns numbers $b_1,\ldots,b_M\in[0,1]$ satisfying

$$\Pr\!\left[\forall i\in\{1,\ldots,M\},\ |b_i-\operatorname{Tr}(E_i\rho)|\le\varepsilon\right]\ge1-\delta.$$

Collective measurements, adaptive measurements, temporary ancillas, and unrestricted known-data classical computation are permitted. The procedure composes physical quantum-OR decision programs, the paper's binary gentle search over signed amplified deviation effects, and classical matrix multiplicative weights. This estimates the entire specified list simultaneously without reconstructing the unknown density matrix in trace distance.

Formalization Note The finite adaptive instrument programs carry normalized Kraus families. The constructor supplies actual physical decision programs, not an assumed accuracy contract or a state oracle. The source composition is executed by chunk-local recursive definitions. The logarithm floors extend the asymptotic notation to $D=1$, $M=1$, and other finite boundary regimes; they introduce no additional asymptotic parameter dependence. No computation-time or gate-complexity assertion is made.

Target

Theorem 2 (Shadow Tomography Theorem); Problem 1

There are universal constants $C>0$ and $p\in\mathbb N$ and one explicit adaptive measurement constructor with the following property. Let $D,M\ge1$ be integers, let $E_1,\ldots,E_M$ be known two-outcome measurement effects on $\mathbb C^D$ (so $0\preceq E_i\preceq I$), and let $0<\varepsilon,\delta<1$. The constructor depends on these known data and not on the unknown state.

Write $L_D=\max\{1,\log D\}$, $L_M=\max\{1,\log M\}$, $L_\delta=\max\{1,\log(1/\delta)\}$, $L_\varepsilon=\max\{1,\log(1/\varepsilon)\}$, $L_{LM}=\max\{1,\log L_M\}$, and $L_{LD}=\max\{1,\log L_D\}$. The constructed procedure uses $k$ independent copies of the unknown state, with

$$k\le\left\lceil C\varepsilon^{-4}L_\delta L_M^4 L_D(1+L_{LM}+L_{LD}+L_\varepsilon)^p\right\rceil.$$

For every density matrix $\rho$ on $\mathbb C^D$, a run on $\rho^{\otimes k}$ returns numbers $b_1,\ldots,b_M\in[0,1]$ satisfying

$$\Pr\!\left[\forall i\in\{1,\ldots,M\},\ |b_i-\operatorname{Tr}(E_i\rho)|\le\varepsilon\right]\ge1-\delta.$$

Collective measurements, adaptive measurements, temporary ancillas, and unrestricted known-data classical computation are permitted. The procedure composes physical quantum-OR decision programs, the paper's binary gentle search over signed amplified deviation effects, and classical matrix multiplicative weights. This estimates the entire specified list simultaneously without reconstructing the unknown density matrix in trace distance.

Formalization Note The finite adaptive instrument programs carry normalized Kraus families. The constructor supplies actual physical decision programs, not an assumed accuracy contract or a state oracle. The source composition is executed by chunk-local recursive definitions. The logarithm floors extend the asymptotic notation to $D=1$, $M=1$, and other finite boundary regimes; they introduce no additional asymptotic parameter dependence. No computation-time or gate-complexity assertion is made.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Shadow Tomography of Quantum States, arXiv:1711.01053v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

The Power of Two Bases: Robust and copy-optimal certification of nearly all quantum states with few-qubit measurements establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

There is a single efficient oracle procedure for certifying a pure target state using one copy of an arbitrary mixed lab state. The classical oracle returns the exact amplitudes of the target in the computational basis and in the full-register Hadamard basis, as in Definition 1 of the paper.

More precisely, there exist a polynomial resource bound $p$, a constant $C>0$, a threshold $n_0\ge1$, a nonnegative sequence $\eta_n\to0$, and measurable sets $G_n$ of normalized $n$-qubit target states such that, for all $n\ge n_0$,

$$\Pr_{\psi\sim\mathrm{Haar}_n}[\psi\notin G_n]\le C2^{-n}.$$

For every $\psi\in G_n$ and every density matrix $\rho$ on the same $n$ qubits, write $F(\psi,\rho)=\langle\psi|\rho|\psi\rangle$. The procedure satisfies

$$\Pr[\mathrm{accept}]\ge F(\psi,\rho),\qquad \Pr[\mathrm{reject}]\ge\frac{1-F(\psi,\rho)}{2}-\eta_n.$$

It flips one fair classical bit and measures the first $r=n-k$ qubits either all in the $Z$ basis or all in the $X$ basis, where $k=\min\{n,\lceil2\log_2(\max\{2,n\})\rceil\}$. Given the observed prefix, it reads the $2^k$ oracle amplitudes for that prefix, computes the conditional target, and performs one projector/complement measurement on the fixed suffix of $k$ qubits. In the $X$ branch, the full-Hadamard oracle fiber is transformed by $H^{\otimes k}$ to obtain the physical conditional target. A zero target fiber is always rejected. The executed oracle calls, scalar instructions, and suffix circuit gates are bounded by $p(n)$, uniformly over normalized targets and every branch; the compiled accepting effect is the conditional target projector.

The same good set and error sequence apply simultaneously to all lab density matrices. This provides the paper's constant robustness with only one measurement involving logarithmically many qubits.

Formalization Note The suffix rounding fixes the proof's choice $\gamma=1$. Efficiency is relative to exact complex-answer classical oracle access and ideal scalar operations, with arbitrary one- and two-qubit unitaries for exact synthesis. No finite-precision or oracle-simulation cost is claimed. The Lean statement uses the concrete frozen conditional measurement program and its execution-derived resource counts, and gives the additive soundness of Theorem 1.

Target

Theorem 1

There is a single efficient oracle procedure for certifying a pure target state using one copy of an arbitrary mixed lab state. The classical oracle returns the exact amplitudes of the target in the computational basis and in the full-register Hadamard basis, as in Definition 1 of the paper.

More precisely, there exist a polynomial resource bound $p$, a constant $C>0$, a threshold $n_0\ge1$, a nonnegative sequence $\eta_n\to0$, and measurable sets $G_n$ of normalized $n$-qubit target states such that, for all $n\ge n_0$,

$$\Pr_{\psi\sim\mathrm{Haar}_n}[\psi\notin G_n]\le C2^{-n}.$$

For every $\psi\in G_n$ and every density matrix $\rho$ on the same $n$ qubits, write $F(\psi,\rho)=\langle\psi|\rho|\psi\rangle$. The procedure satisfies

$$\Pr[\mathrm{accept}]\ge F(\psi,\rho),\qquad \Pr[\mathrm{reject}]\ge\frac{1-F(\psi,\rho)}{2}-\eta_n.$$

It flips one fair classical bit and measures the first $r=n-k$ qubits either all in the $Z$ basis or all in the $X$ basis, where $k=\min\{n,\lceil2\log_2(\max\{2,n\})\rceil\}$. Given the observed prefix, it reads the $2^k$ oracle amplitudes for that prefix, computes the conditional target, and performs one projector/complement measurement on the fixed suffix of $k$ qubits. In the $X$ branch, the full-Hadamard oracle fiber is transformed by $H^{\otimes k}$ to obtain the physical conditional target. A zero target fiber is always rejected. The executed oracle calls, scalar instructions, and suffix circuit gates are bounded by $p(n)$, uniformly over normalized targets and every branch; the compiled accepting effect is the conditional target projector.

The same good set and error sequence apply simultaneously to all lab density matrices. This provides the paper's constant robustness with only one measurement involving logarithmically many qubits.

Formalization Note The suffix rounding fixes the proof's choice $\gamma=1$. Efficiency is relative to exact complex-answer classical oracle access and ideal scalar operations, with arbitrary one- and two-qubit unitaries for exact synthesis. No finite-precision or oracle-simulation cost is claimed. The Lean statement uses the concrete frozen conditional measurement program and its execution-derived resource counts, and gives the additive soundness of Theorem 1.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• The Power of Two Bases: Robust and copy-optimal certification of nearly all quantum states with few-qubit measurements, arXiv:2602.11616v1. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum state tomography via compressed sensing establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $n\ge 0$ be the number of qubits, $d=2^n$, and let $\rho\in\mathbb C^{d\times d}$ be a fixed density matrix (positive semidefinite with trace one) of exact rank $r$. There are absolute constants $a,b,c_0>0$, independent of $n,r,\rho$, such that the following holds for every $c\ge c_0$.

Set $m=\lceil cdr(\ln d)^2\rceil$. Independently sample $m$ unphased Pauli strings $w(A_i)$, uniformly with replacement from all $d^2$ tensor products of $I,X,Y,Z$, including the identity. Suppose their exact expectations $y_i=\operatorname{Tr}(w(A_i)\rho)$ are known. Write $\mathcal O(A,y)$ for the set of minimizers of

$$\min_{\sigma=\sigma^\dagger}\|\sigma\|_{\mathrm{tr}} \quad\text{subject to}\quad \operatorname{Tr}\sigma=1,\qquad \operatorname{Tr}(w(A_i)\sigma)=y_i\quad(1\le i\le m).$$

The trace norm is the sum of the singular values; competitors need not be positive semidefinite and have no rank constraint. Then

$$\Pr_A\!\left[\mathcal O(A,y)\ne\{\rho\}\right]\le a e^{-bc}.$$

Thus this specific convex program attains its minimum uniquely at the unknown state with exponentially small failure probability. The probability is over the design for each fixed state, and $m$ counts exact expectation settings, rather than physical copies or computation time.

Formalization Note Natural logarithms and integer rounding pin down the paper's asymptotic notation using its closing proof on PDF p.3. The sampling law and optimizer set are frozen definitions depending only on public $n,m$, and on the design and supplied data, respectively. For $n=0$, $d=r=1$ and $m=0$; trace one alone gives unique recovery.

Target

Theorem 1 (Low-rank tomography), convex program (1)

Let $n\ge 0$ be the number of qubits, $d=2^n$, and let $\rho\in\mathbb C^{d\times d}$ be a fixed density matrix (positive semidefinite with trace one) of exact rank $r$. There are absolute constants $a,b,c_0>0$, independent of $n,r,\rho$, such that the following holds for every $c\ge c_0$.

Set $m=\lceil cdr(\ln d)^2\rceil$. Independently sample $m$ unphased Pauli strings $w(A_i)$, uniformly with replacement from all $d^2$ tensor products of $I,X,Y,Z$, including the identity. Suppose their exact expectations $y_i=\operatorname{Tr}(w(A_i)\rho)$ are known. Write $\mathcal O(A,y)$ for the set of minimizers of

$$\min_{\sigma=\sigma^\dagger}\|\sigma\|_{\mathrm{tr}} \quad\text{subject to}\quad \operatorname{Tr}\sigma=1,\qquad \operatorname{Tr}(w(A_i)\sigma)=y_i\quad(1\le i\le m).$$

The trace norm is the sum of the singular values; competitors need not be positive semidefinite and have no rank constraint. Then

$$\Pr_A\!\left[\mathcal O(A,y)\ne\{\rho\}\right]\le a e^{-bc}.$$

Thus this specific convex program attains its minimum uniquely at the unknown state with exponentially small failure probability. The probability is over the design for each fixed state, and $m$ counts exact expectation settings, rather than physical copies or computation time.

Formalization Note Natural logarithms and integer rounding pin down the paper's asymptotic notation using its closing proof on PDF p.3. The sampling law and optimizer set are frozen definitions depending only on public $n,m$, and on the design and supplied data, respectively. For $n=0$, $d=r=1$ and $m=0$; trace one alone gives unique recovery.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Quantum state tomography via compressed sensing, arXiv:0909.3304v4. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum chi-squared tomography and mutual information testing establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

There are absolute constants $C>0$ and $0<\epsilon_0\le 1/2$ with the following property. For every integer dimension $d\ge 1$, supplied integer rank bound $1\le r\le d$, and accuracy $0<\epsilon\le\epsilon_0$, one can choose a copy count $n\ge 0$ and a lawful collective measurement on $n$ independent identical copies of a state, with a density matrix as its classical outcome, such that

$$n\le C\frac{rd}{\epsilon}\left(\ln\frac{d}{\epsilon}\right)^2,\qquad \Pr_{\widehat\rho\sim\mathcal M(\rho^{\otimes n})}\!\left[S(\rho\Vert\widehat\rho)\le\epsilon\right]\ge 0.99.$$

The probability guarantee holds for every unknown positive semidefinite $d\times d$ matrix $\rho$ of trace one and rank at most $r$. The measurement is chosen using only $d,r,\epsilon$, before $\rho$. Here $S$ is Umegaki quantum relative entropy with natural logarithms: $S(\rho\Vert\sigma)=\operatorname{Tr}(\rho\ln\rho-\rho\ln\sigma)$ when $\operatorname{supp}\rho\subseteq\operatorname{supp}\sigma$, and $+\infty$ otherwise; zero-eigenvalue terms use their continuous limits. The estimate may have any rank.

This gives relative entropy tomography with $\widetilde O(rd/\epsilon)$ copies, including singular input states. Larger positive accuracies follow by running at a fixed smaller accuracy. The explicit squared-logarithm bound is stated on PDF p.12 immediately after Theorem 2.34.

Formalization Note The measurement uses the frozen general operator-valued POVM on the space of density matrices, and its output distribution is the Born law on $\rho^{\otimes n}$. The extended divergence uses the frozen kernel-containment support guard.

Target

Corollary 1.8

There are absolute constants $C>0$ and $0<\epsilon_0\le 1/2$ with the following property. For every integer dimension $d\ge 1$, supplied integer rank bound $1\le r\le d$, and accuracy $0<\epsilon\le\epsilon_0$, one can choose a copy count $n\ge 0$ and a lawful collective measurement on $n$ independent identical copies of a state, with a density matrix as its classical outcome, such that

$$n\le C\frac{rd}{\epsilon}\left(\ln\frac{d}{\epsilon}\right)^2,\qquad \Pr_{\widehat\rho\sim\mathcal M(\rho^{\otimes n})}\!\left[S(\rho\Vert\widehat\rho)\le\epsilon\right]\ge 0.99.$$

The probability guarantee holds for every unknown positive semidefinite $d\times d$ matrix $\rho$ of trace one and rank at most $r$. The measurement is chosen using only $d,r,\epsilon$, before $\rho$. Here $S$ is Umegaki quantum relative entropy with natural logarithms: $S(\rho\Vert\sigma)=\operatorname{Tr}(\rho\ln\rho-\rho\ln\sigma)$ when $\operatorname{supp}\rho\subseteq\operatorname{supp}\sigma$, and $+\infty$ otherwise; zero-eigenvalue terms use their continuous limits. The estimate may have any rank.

This gives relative entropy tomography with $\widetilde O(rd/\epsilon)$ copies, including singular input states. Larger positive accuracies follow by running at a fixed smaller accuracy. The explicit squared-logarithm bound is stated on PDF p.12 immediately after Theorem 2.34.

Formalization Note The measurement uses the frozen general operator-valued POVM on the space of density matrices, and its output distribution is the Born law on $\rho^{\otimes n}$. The extended divergence uses the frozen kernel-containment support guard.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Quantum chi-squared tomography and mutual information testing, arXiv:2305.18519v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Improved quantum data analysis establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

There are a universal constant $C>0$ and a copy-count function $n_{\mathrm{TS}}(m,\varepsilon,\delta)$, depending only on the number of tests $m$ and the accuracy and failure parameters $\varepsilon,\delta$, with the following property. For every integer $m\ge1$ and every $0<\varepsilon,\delta<1/2$, write $L=\log(1/\delta)$. Then

$$n_{\mathrm{TS}}(m,\varepsilon,\delta) \le \left\lceil C\,\frac{((\log m)^2+L)L}{\varepsilon^2}\right\rceil.$$

For every dimension $d\ge1$, there is an online quantum protocol that begins with $n_{\mathrm{TS}}(m,\varepsilon,\delta)$ independent, unentangled copies of an unknown state $\rho\in\mathbb C^{d\times d}$, where $\rho$ is positive semidefinite and $\operatorname{tr}\rho=1$, together with a known ancillary state. Observable/threshold pairs $(A_t,\theta_t)$ are then presented in order, with $0\le A_t\le I$ and $\theta_t\in[0,1]$. The protocol is fixed independently of $\rho$ and the stream, and its decision at stage $t$ depends only on the presented prefix and its retained quantum memory. It either passes or halts and selects the current index $t$. Selection asserts $\operatorname{tr}(\rho A_t)>\theta_t-\varepsilon$; after $m$ passes it asserts $\operatorname{tr}(\rho A_i)\le\theta_i$ for all $i$.

For every such state and stream,

$$\Pr\!\left[ \begin{array}{l} \text{the protocol selects }t\text{ with }\operatorname{tr}(\rho A_t)>\theta_t-\varepsilon,\\ \text{or passes on all }m\text{ pairs with }\operatorname{tr}(\rho A_i)\le\theta_i\text{ for every }i \end{array} \right]\ge1-\delta.$$

The stream may depend on preceding public pass responses. No promise that an expectation exceeds a threshold is required. Both kinds of claim are valid in the overlap $\theta_t-\varepsilon<\operatorname{tr}(\rho A_t)\le\theta_t$.

This theorem bounds the sample cost of online search among quantum observables independently of the state dimension.

Formalization Note Natural logarithms and a ceiling express the source's uniform big-O copy bound. Physical Kraus instruments act on the initial tensor power of $\rho$ and an ancillary state; the model uses only copy access. The selected index is zero-based in Lean.

Target

Theorem 1.1

There are a universal constant $C>0$ and a copy-count function $n_{\mathrm{TS}}(m,\varepsilon,\delta)$, depending only on the number of tests $m$ and the accuracy and failure parameters $\varepsilon,\delta$, with the following property. For every integer $m\ge1$ and every $0<\varepsilon,\delta<1/2$, write $L=\log(1/\delta)$. Then

$$n_{\mathrm{TS}}(m,\varepsilon,\delta) \le \left\lceil C\,\frac{((\log m)^2+L)L}{\varepsilon^2}\right\rceil.$$

For every dimension $d\ge1$, there is an online quantum protocol that begins with $n_{\mathrm{TS}}(m,\varepsilon,\delta)$ independent, unentangled copies of an unknown state $\rho\in\mathbb C^{d\times d}$, where $\rho$ is positive semidefinite and $\operatorname{tr}\rho=1$, together with a known ancillary state. Observable/threshold pairs $(A_t,\theta_t)$ are then presented in order, with $0\le A_t\le I$ and $\theta_t\in[0,1]$. The protocol is fixed independently of $\rho$ and the stream, and its decision at stage $t$ depends only on the presented prefix and its retained quantum memory. It either passes or halts and selects the current index $t$. Selection asserts $\operatorname{tr}(\rho A_t)>\theta_t-\varepsilon$; after $m$ passes it asserts $\operatorname{tr}(\rho A_i)\le\theta_i$ for all $i$.

For every such state and stream,

$$\Pr\!\left[ \begin{array}{l} \text{the protocol selects }t\text{ with }\operatorname{tr}(\rho A_t)>\theta_t-\varepsilon,\\ \text{or passes on all }m\text{ pairs with }\operatorname{tr}(\rho A_i)\le\theta_i\text{ for every }i \end{array} \right]\ge1-\delta.$$

The stream may depend on preceding public pass responses. No promise that an expectation exceeds a threshold is required. Both kinds of claim are valid in the overlap $\theta_t-\varepsilon<\operatorname{tr}(\rho A_t)\le\theta_t$.

This theorem bounds the sample cost of online search among quantum observables independently of the state dimension.

Formalization Note Natural logarithms and a ceiling express the source's uniform big-O copy bound. Physical Kraus instruments act on the initial tensor power of $\rho$ and an ancillary state; the model uses only copy access. The selected index is zero-based in Lean.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Improved quantum data analysis, arXiv:2011.10908v4. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum Tomography via Compressed Sensing: Error Bounds, Sample Complexity, and Efficient Estimators establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

There are positive absolute constants $C,C_0,C_1,C'_0,C'_1$ and a function $\eta:\mathbb N\to[0,1]$ with $\eta(n)\to0$ as $n\to\infty$ such that the following holds. Let $d=2^n$, $1\le r\le d$, and $m\ge1$ satisfy $m\ge Crd(\log d)^6$. Sample $P_1,\ldots,P_m$ independently and uniformly, with replacement, from all $d^2$ unsigned tensor Pauli operators, including the identity. On the real space of Hermitian matrices define $\mathcal A(X)_i=\sqrt{d/m}\,\operatorname{Tr}(P_iX)$ and $\mathcal A^*(v)=\sqrt{d/m}\sum_i v_iP_i$.

With probability at least $1-\eta(n)$ over this sampling, simultaneously for every positive semidefinite matrix $\rho$ (without a trace or rank restriction), every $z\in\mathbb R^m$, and $y=\mathcal A(\rho)+z$, both conclusions below hold. Write $\rho_r$ for the spectral truncation retaining the largest $r$ eigenvalues, and $\rho_c=\rho-\rho_r$. All optimizations range over Hermitian matrices and permit nonunique minimizers.

1. For every $\lambda$ satisfying $\|\mathcal A^*(z)\|\le\lambda$, the problem minimizing $\|X\|_{\mathrm{tr}}$ subject to $\|\mathcal A^*(\mathcal A(X)-y)\|\le\lambda$ has a minimizer. Every such minimizer $\widehat\rho_{\mathrm{DS}}$ satisfies

$$\|\widehat\rho_{\mathrm{DS}}-\rho\|_{\mathrm{tr}}\le C_0r\lambda+C_1\|\rho_c\|_{\mathrm{tr}}.$$

2. For every $\mu>0$ satisfying $\|\mathcal A^*(z)\|\le\mu/2$, the problem minimizing $\frac12\|\mathcal A(X)-y\|_2^2+\mu\|X\|_{\mathrm{tr}}$ has a minimizer. Every such minimizer $\widehat\rho_{\mathrm{Lasso}}$ satisfies

$$\|\widehat\rho_{\mathrm{Lasso}}-\rho\|_{\mathrm{tr}}\le C'_0r\mu+C'_1\|\rho_c\|_{\mathrm{tr}}.$$

Here $\|\cdot\|$ is the operator norm, $\|\cdot\|_2$ is the Euclidean vector norm, and $\|X\|_{\mathrm{tr}}=\operatorname{Tr}\sqrt{X^\dagger X}$ is the full trace norm. The two bounds separate noise from the spectral tail and apply to full-rank inputs as well as exactly low-rank ones.

Formalization Note The paper's qualitative “high probability” is represented by a vanishing failure function uniform in $r,m$. Positive Lasso regularization is an explicit correction of the omitted $\mu=0$ domain; the source's regularized recovery argument requires it. This correction, the interpretation of unnormalized PSD inputs, and the qualitative probability convention require independent moderation.

Target

Theorem 1, §II.C

There are positive absolute constants $C,C_0,C_1,C'_0,C'_1$ and a function $\eta:\mathbb N\to[0,1]$ with $\eta(n)\to0$ as $n\to\infty$ such that the following holds. Let $d=2^n$, $1\le r\le d$, and $m\ge1$ satisfy $m\ge Crd(\log d)^6$. Sample $P_1,\ldots,P_m$ independently and uniformly, with replacement, from all $d^2$ unsigned tensor Pauli operators, including the identity. On the real space of Hermitian matrices define $\mathcal A(X)_i=\sqrt{d/m}\,\operatorname{Tr}(P_iX)$ and $\mathcal A^*(v)=\sqrt{d/m}\sum_i v_iP_i$.

With probability at least $1-\eta(n)$ over this sampling, simultaneously for every positive semidefinite matrix $\rho$ (without a trace or rank restriction), every $z\in\mathbb R^m$, and $y=\mathcal A(\rho)+z$, both conclusions below hold. Write $\rho_r$ for the spectral truncation retaining the largest $r$ eigenvalues, and $\rho_c=\rho-\rho_r$. All optimizations range over Hermitian matrices and permit nonunique minimizers.

1. For every $\lambda$ satisfying $\|\mathcal A^*(z)\|\le\lambda$, the problem minimizing $\|X\|_{\mathrm{tr}}$ subject to $\|\mathcal A^*(\mathcal A(X)-y)\|\le\lambda$ has a minimizer. Every such minimizer $\widehat\rho_{\mathrm{DS}}$ satisfies

$$\|\widehat\rho_{\mathrm{DS}}-\rho\|_{\mathrm{tr}}\le C_0r\lambda+C_1\|\rho_c\|_{\mathrm{tr}}.$$

2. For every $\mu>0$ satisfying $\|\mathcal A^*(z)\|\le\mu/2$, the problem minimizing $\frac12\|\mathcal A(X)-y\|_2^2+\mu\|X\|_{\mathrm{tr}}$ has a minimizer. Every such minimizer $\widehat\rho_{\mathrm{Lasso}}$ satisfies

$$\|\widehat\rho_{\mathrm{Lasso}}-\rho\|_{\mathrm{tr}}\le C'_0r\mu+C'_1\|\rho_c\|_{\mathrm{tr}}.$$

Here $\|\cdot\|$ is the operator norm, $\|\cdot\|_2$ is the Euclidean vector norm, and $\|X\|_{\mathrm{tr}}=\operatorname{Tr}\sqrt{X^\dagger X}$ is the full trace norm. The two bounds separate noise from the spectral tail and apply to full-rank inputs as well as exactly low-rank ones.

Formalization Note The paper's qualitative “high probability” is represented by a vanishing failure function uniform in $r,m$. Positive Lasso regularization is an explicit correction of the omitted $\mu=0$ domain; the source's regularized recovery argument requires it. This correction, the interpretation of unnormalized PSD inputs, and the qualitative probability convention require independent moderation.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Quantum Tomography via Compressed Sensing: Error Bounds, Sample Complexity, and Efficient Estimators, arXiv:1205.2300v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.