Fixed-evolution sandwich has the required local moments

Open

QAlgorithms.Papers.Independent.Intakethird100.P71.fixedEvolution_sandwichMoments

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

prove2quantum

Fix $N$ qudits, $d\ge2$ , and an arbitrary unitary $U_0$ independently of the unknown input state. Let $L$ and $R$ be independent random local unitaries whose twirling superoperators equal those of normalized product Haar measure at orders two and three. For the sandwich $U=L U_0 R$ , choose the prior basis outcome $b$ uniformly and set $S=U^\dagger|b\rangle\langle b|U$ . Its prior law $\nu$ is a probability measure with integrable polynomial moments. If $\nu^{\rm LS}$ is its local Haar twirl, then

\mathbb E_\nu S^{\otimes t}=\mathbb E_{\nu^{\rm LS}}S^{\otimes t},\qquad t\in\{2,3\}.

When its measurement channel is injective, Eq. (12) has unique real coefficients defining its inverse, and the resulting shadows reconstruct every density matrix without bias. This formulation includes the moment property used for Clifford end factors without asserting continuous Haar invariance of their discrete probability laws.

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.11 §III C: fixed evolution sandwiched between independent local
2/3-designs has the required snapshot moments. Finite Clifford factors are not
asserted Haar-invariant as laws. Completeness is needed only for reconstruction. -/
theorem fixedEvolution_sandwichMoments {n d : ℕ} (hd : 2 ≤ d) (U0 : Unitary n d)
    (H muL muR : Measure (Local n d)) [IsProbabilityMeasure H] [H.IsMulLeftInvariant]
    [IsProbabilityMeasure muL] [IsProbabilityMeasure muR]
    (hL : ∀ t ∈ ({2,3} : Finset ℕ), IsLocalDesign muL H t)
    (hR : ∀ t ∈ ({2,3} : Finset ℕ), IsLocalDesign muR H t) :
    let nu := sandwichPrior U0 muL muR
    IsProbabilityMeasure nu ∧ SnapshotPolynomialIntegrable nu ∧
    (∀ t ∈ ({2,3} : Finset ℕ), snapshotMoment nu t = snapshotMoment (twirled H nu) t) ∧
    (∀ hc : Complete nu, ∃! r : Finset (Fin n) → ℝ,
      CoefficientSystem nu r ∧ (∀ X : Op n d, efReconstruct r X = snapshotInverse nu hc X) ∧
      (∀ rho : Op n d, IsDensityMatrix rho →
        (∫ S, efReconstruct r S ∂posteriorOf nu rho) = rho)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P71

end

Source

Classical Shadow Tomography with Locally Scrambled Quantum Dynamics, arXiv:2107.04817v4, PDF p. 11, §III C: fixed evolution sandwiched by local random unitaries

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$ , $N=d^n$ , and let $U_0$ be any unitary matrix on $\mathbb C^{\mathcal X}$ . For a family $V=(V_i)_{i<n}$ of local $d\times d$ unitary matrices, write $L_V=\bigotimes_iV_i$ . Let $H,\mu_L,\mu_R$ be probability measures on these families, with $H$ invariant under left multiplication by every fixed family. Assume that, for each $t\in\{2,3\}$ , each $\mu\in\{\mu_L,\mu_R\}$ , and every complex matrix $X$ indexed by $t$ copies of $\mathcal X$ ,

\int (L_V^{\otimes t})^\dagger X L_V^{\otimes t}\,d\mu(V) = \int (L_V^{\otimes t})^\dagger X L_V^{\otimes t}\,dH(V), \qquad (S^{\otimes t})_{xy}=\prod_{a=0}^{t-1}S_{x_a y_a}.

Define

\nu=N^{-1}\sum_{b\in\mathcal X} \bigl((L,R)\mapsto (L_LU_0L_R)^\dagger|b\rangle\langle b|(L_LU_0L_R)\bigr)_*(\mu_L\otimes\mu_R), \quad \widetilde\nu=((V,S)\mapsto L_V^\dagger SL_V)_*(H\otimes\nu).

The theorem states that $\nu$ is a probability measure; that $S\mapsto S^{\otimes t}$ is integrable for every natural $t$ , including $0$ , that $S\mapsto\operatorname{tr}(SX)S$ is integrable for every complex matrix $X$ , and that $S\mapsto(\operatorname{Re}\operatorname{tr}(XS))^2\operatorname{Re}\operatorname{tr}(SY)$ is integrable for every pair $X,Y$ ; and that $\int S^{\otimes t}\,d\nu=\int S^{\otimes t}\,d\widetilde\nu$ for $t=2,3$ . Define $\mathcal M(X)_{ij}=\sum_{k,l}(\int NS_{ij}S_{lk}\,d\nu(S))X_{kl}$ . For every assumption that $\mathcal M$ is injective, writing $\mathcal R=\mathcal M^{-1}$ , there exists exactly one real function $r$ on the site subsets satisfying all of the following together. First, with

f(C)=\int\operatorname{Re}\operatorname{tr}((\operatorname{Tr}_{C^c}S)^2)\,d\nu(S), \quad F(A,B,C)=\left(\frac{d^3}{d^2-1}\right)^n \sum_{\substack{D\\B=A\cap D}}d^{-|D|}(-1/d)^{|C\triangle D|},

it satisfies $\sum_{A,C}r(A)F(A,B,C)f(C)=\mathbf1_{\{B=\{0,\ldots,n-1\}\}}$ for every $B$ . Second, $N\sum_A r(A)R_A(X)=\mathcal R(X)$ for every $X$ , where $R_A(X)$ has entry $d^{-(n-|A|)}(\operatorname{Tr}_{A^c}X)_{x|_A,y|_A}$ when $x,y$ agree outside $A$ , and $0$ otherwise; the partial trace sums matching complementary indices. Third, for every positive semidefinite $\rho$ of trace $1$ ,

\int N\sum_A r(A)R_A(S)\,d\nu_\rho(S)=\rho, \qquad d\nu_\rho=[N\operatorname{Re}\operatorname{tr}(S\rho)]_+d\nu.

The case $n=0$ and all empty products and subsets are included.

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