Entanglement features determine unbiased reconstruction

Open

QAlgorithms.Papers.Independent.Intakethird100.P71.entanglementFeature_reconstruction

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

prove2quantum

Let a fixed Borel probability ensemble of unitaries measure $N$ qudits of dimension $d\ge2$ , with $D=d^N$ . A raw snapshot is $S=U^\dagger|b\rangle\langle b|U$ . The prior chooses $b$ uniformly; the posterior weights the prior by $D\operatorname{Tr}(S\rho)$ . Assume the prior law is invariant under every local conjugation and its measurement channel $\mathcal M(X)=D\mathbb E[S\operatorname{Tr}(SX)]$ is injective. For every region $A$ , let $X_A$ denote the partial trace over its complement, tensored with normalized identity in the original site order, and let $W_C=\mathbb E\operatorname{Tr}[(\operatorname{Tr}_{\bar C}S)^2]$ . Then

\mathcal M(X)=\sum_{B,C}d^{2N-|B|}X_B\,\mathrm{Wg}_{B,C}W_C,\qquad \mathrm{Wg}_{B,C}=(d^2-1)^{-N}(-1/d)^{|B\triangle C|}.

There is a unique real coefficient vector $r$ solving $\sum_{A,C}r_A f_{A,B,C}W_C=\delta_{B,\Omega}$ , where $f$ is the explicit fusion coefficient of Eq. (11). For every operator $X$ and every density matrix $\rho$ ,

\mathcal R(X)=d^N\sum_A r_A X_A=\mathcal M^{-1}(X),\qquad \mathbb E_{S\mid\rho}\mathcal R(S)=\rho.

Consequently every Hermitian observable has an unbiased linear prediction. The same coefficients work for all input states; their computation is not claimed efficient.

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.3–4 Eqs.(7),(9),(11),(12), Appendix A p.18: EF channel formula,
unique reconstruction coefficients under completeness, and unbiased shadows.
The coefficients are chosen once from the ensemble, before rho. -/
theorem entanglementFeature_reconstruction {n d : ℕ} (hd : 2 ≤ d) (E : ProjectiveEnsemble n d)
    (hls : LocallyScrambled (prior E)) (hc : Complete (prior E)) :
    (∀ X : Op n d, snapshotMeasurementMap (prior E) X =
      ∑ B : Finset (Fin n), ∑ C : Finset (Fin n),
        ((((d : ℝ)^(2*n) / (d : ℝ)^B.card) * regionalWg n d B C *
          feature (prior E) C : ℝ) : ℂ) • reducedSnapshot B X) ∧
    ∃! r : Finset (Fin n) → ℝ,
      CoefficientSystem (prior E) r ∧
      (∀ X : Op n d, efReconstruct r X = snapshotInverse (prior E) hc X) ∧
      (∀ rho : Op n d, IsDensityMatrix rho →
        Integrable (fun S => efReconstruct r S) (posteriorOf (prior E) rho) ∧
        (∫ S, efReconstruct r S ∂posteriorOf (prior E) rho) = rho ∧
        ∀ O : Op n d, O.IsHermitian →
          (∫ S, shadowEstimate (prior E) hc O S ∂posteriorOf (prior E) rho) = (O*rho).trace.re) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P71

end

Source

Classical Shadow Tomography with Locally Scrambled Quantum Dynamics, arXiv:2107.04817v4, PDF p. 1, Abstract / §II A: entanglement-feature reconstruction and unbiased classical shadows

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$ , and let $E$ give a probability law $\lambda$ on global unitary matrices. Set $S_b(U)=U^\dagger|b\rangle\langle b|U$ and $\nu=N^{-1}\sum_{b\in\mathcal X}(S_b)_*\lambda$ . For each family $V=(V_i)_{i<n}$ of $d\times d$ unitary matrices, write $L_V=\bigotimes_iV_i$ ; assume that pushing $\nu$ forward by $S\mapsto L_V^\dagger SL_V$ leaves $\nu$ unchanged for every $V$ . Define

\mathcal M(X)_{ij} =\sum_{k,l}\left(\int N S_{ij}S_{lk}\,d\nu(S)\right)X_{kl},

and assume that $\mathcal M$ is injective; write $\mathcal R=\mathcal M^{-1}$ . For a subset $A\subseteq\{0,\ldots,n-1\}$ , define $(\operatorname{Tr}_{A^c}X)_{xy}=\sum_zX_{(x,z),(y,z)}$ , where $z$ ranges over configurations on $A^c$ , and let $R_A(X)$ have entry $d^{-(n-|A|)}(\operatorname{Tr}_{A^c}X)_{x|_A,y|_A}$ when $x,y$ agree on $A^c$ , and entry $0$ otherwise. Put

f(A)=\int\operatorname{Re}\operatorname{tr}\bigl((\operatorname{Tr}_{A^c}S)^2\bigr)\,d\nu(S), \quad G(B,C)=(d^2-1)^{-n}(-1/d)^{|B\triangle C|},

F(A,B,C)= \left(\frac{d^3}{d^2-1}\right)^n \sum_{\substack{D\subseteq\{0,\ldots,n-1\}\\B=A\cap D}} d^{-|D|}(-1/d)^{|C\triangle D|}.

The theorem asserts that, for every complex matrix $X$ ,

\mathcal M(X)=\sum_{B,C}d^{2n-|B|}G(B,C)f(C)R_B(X).

It also asserts that there exists exactly one real function $r$ on the subsets satisfying all the following conditions together: for every subset $B$ , $\sum_{A,C}r(A)F(A,B,C)f(C)=1$ if $B$ is the full set and $0$ otherwise; the map $\mathcal E_r(X)=N\sum_A r(A)R_A(X)$ equals $\mathcal R(X)$ for every $X$ ; and, for every positive semidefinite matrix $\rho$ of trace $1$ , with $d\nu_\rho(S)=[N\operatorname{Re}\operatorname{tr}(S\rho)]_+d\nu(S)$ , the function $S\mapsto\mathcal E_r(S)$ is integrable and has integral $\rho$ , and every Hermitian matrix $O$ satisfies

\int\operatorname{Re}\operatorname{tr}(O\mathcal R(S))\,d\nu_\rho(S) =\operatorname{Re}\operatorname{tr}(O\rho).

All subset sums include the empty subset, and $n=0$ is allowed.

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