Finite-sample Chebyshev guarantee

Open

QAlgorithms.Papers.Independent.Intakethird100.P71.finiteSample_chebyshev

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

prove2quantum

Fix a locally scrambled, tomographically complete projective experiment on $N$ qudits, $d\ge2$ , a density matrix $\rho$ , and a traceless Hermitian observable $O$ . Let $\hat o$ be its unbiased single-shot shadow prediction, $Q_\rho(O)=\mathbb E\hat o^2$ , and $\bar o$ the arithmetic mean of $M\ge1$ independent snapshots of identical copies. For $\epsilon>0$ and $0<\delta<1$ ,

\Pr\bigl(|\bar o-\operatorname{Tr}(O\rho)|\ge\epsilon\bigr)\le\frac{\operatorname{Var}\hat o}{\epsilon^2 M}\le\frac{Q_\rho(O)}{\epsilon^2 M}.

In particular,

M\ge\frac{Q_\rho(O)}{\epsilon^2\delta}\quad\Longrightarrow\quad\Pr\bigl(|\bar o-\operatorname{Tr}(O\rho)|\ge\epsilon\bigr)\le\delta.

This is a sufficient copy count for the specified state and observable.

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 p.5 Eqs.(18)–(19): Chebyshev and its sufficient copy count for each
specified rho and O. No necessary bound or simultaneous-observable claim. -/
theorem finiteSample_chebyshev {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)
    (m : ℕ) (hm : 0 < m) (eps delta : ℝ) (heps : 0 < eps)
    (hdelta : 0 < delta ∧ delta < 1) :
    let failure := (snapshotSampleLaw (prior E) rho m)
      {s | eps ≤ |shadowSampleMean (prior E) hc O s - (O*rho).trace.re|}
    failure ≤ ENNReal.ofReal (shotVariance (prior E) hc rho O / (eps^2 * m)) ∧
    shotVariance (prior E) hc rho O / (eps^2 * m) ≤
      secondMoment (prior E) hc rho O / (eps^2 * m) ∧
    (secondMoment (prior E) hc rho O / (eps^2 * delta) ≤ m →
      failure ≤ ENNReal.ofReal delta) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P71

end

Source

Classical Shadow Tomography with Locally Scrambled Quantum Dynamics, arXiv:2107.04817v4, PDF p. 5, §II B, Eqs.(18)–(19): finite-sample Chebyshev guarantee

Read-back

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

Let $n\ge0$ , $d\ge2$ , $\mathcal X=\{0,\ldots,d-1\}^n$ , and $N=d^n$ . Let $E$ specify a probability law $\lambda$ on global unitary matrices, and define $\nu=N^{-1}\sum_b(U\mapsto U^\dagger|b\rangle\langle b|U)_*\lambda$ . Assume that $\nu$ is invariant under conjugation $S\mapsto L_V^\dagger SL_V$ by every tensor product $L_V=\bigotimes_iV_i$ of local unitary matrices. Define $\mathcal M(X)_{ij}=\sum_{k,l}(\int NS_{ij}S_{lk}\,d\nu(S))X_{kl}$ , assume it is injective, and let $\mathcal R=\mathcal M^{-1}$ . Let $\rho$ be positive semidefinite of trace $1$ , let $O$ be Hermitian of trace $0$ , let $m$ be a strictly positive natural number, and let $\varepsilon,\delta\in\mathbb R$ satisfy $\varepsilon>0$ and $0<\delta<1$ . Set $z(S)=\operatorname{Re}\operatorname{tr}(O\mathcal R(S))$ , define $d\nu_\rho=[N\operatorname{Re}\operatorname{tr}(S\rho)]_+d\nu$ , and put

Q=\int z^2\,d\nu_\rho,\qquad V=Q-\left(\int z\,d\nu_\rho\right)^2,\qquad \overline z(S_0,\ldots,S_{m-1})=\frac1m\sum_{a=0}^{m-1}z(S_a).

Writing $F$ for the $\nu_\rho^{\otimes m}$ -measure of the event $\{\varepsilon\le|\overline z-\operatorname{Re}\operatorname{tr}(O\rho)|\}$ , including equality at the threshold, the theorem asserts

F\le\left[\frac{V}{\varepsilon^2m}\right]_+,\qquad \frac{V}{\varepsilon^2m}\le\frac{Q}{\varepsilon^2m}, \qquad \left(\frac{Q}{\varepsilon^2\delta}\le m\right)\Longrightarrow F\le\delta.

The first bound is in the extended nonnegative reals, where $[x]_+$ denotes the embedding of $\max(x,0)$ ; the middle inequality is a real inequality. The case $n=0$ is permitted, while $m=0$ is excluded.

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