Local-state averaged second moment from second entanglement features

Open

QAlgorithms.Papers.Independent.Intakethird100.P71.averagedSecondMoment_entanglementFeatures

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

prove2quantum

Let $\nu$ be the locally scrambled prior of a complete projective experiment on $N$ qudits, $d\ge2$ , with reconstruction coefficients $r$ solving Eq. (12). Fix a density matrix $\rho$ and a traceless Hermitian $O$ . Let $H$ be normalized Haar measure on $U(d)^N$ , $W_C=\mathbb E_\nu\operatorname{Tr}[(\operatorname{Tr}_{\bar C}S)^2]$ , and $W_{O,D}=\mathbb E_{V\sim H}\operatorname{Tr}[(\operatorname{Tr}_{\bar D}(V^\dagger OV))^2]$ . The local-state average $Q_{\mathrm{av}}(O)=\mathbb E_{V\sim H}Q_{V^\dagger\rho V}(O)$ equals the prior second moment of the prediction and satisfies

Q_{\mathrm{av}}(O)=\sum_{A,B,C,D}v_{A,B,C,D}W_{A\cap B\cap C}W_{O,D},

v_{A,B,C,D}=r_A r_B\left(\frac{d^2}{d^2-1}\right)^N\frac{d^{|A\cap B\cap C|}}{d^{|C|}}\left(-\frac1d\right)^{|C\triangle D|}.

All indices are arbitrary regions, including empty and full regions. Observable partial traces are unnormalized. This formula removes the input-state dependence by averaging; it gives no pointwise bound for each $\rho$ .

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.(20)–(22), Appendix B pp.18–19: local-state averaged Q in
second EFs. The signed power is multiplicative. This is an average, not a
pointwise-in-rho variance bound. -/
theorem averagedSecondMoment_entanglementFeatures {n d : ℕ} (hd : 2 ≤ d)
    (E : ProjectiveEnsemble n d) (hls : LocallyScrambled (prior E)) (hc : Complete (prior E))
    (H : Measure (Local n d)) [IsProbabilityMeasure H] [H.IsMulLeftInvariant]
    (rho O : Op n d) (hrho : IsDensityMatrix rho) (hO : O.IsHermitian) (ht : O.trace = 0)
    (r : Finset (Fin n) → ℝ) (hr : CoefficientSystem (prior E) r) :
    averagedSecondMoment H (prior E) hc rho O =
      (∫ S, shadowEstimate (prior E) hc O S ^ 2 ∂prior E) ∧
    averagedSecondMoment H (prior E) hc rho O =
      ∑ A : Finset (Fin n), ∑ B : Finset (Fin n), ∑ C : Finset (Fin n), ∑ D : Finset (Fin n),
        varianceCoefficient d r A B C D * feature (prior E) (A ∩ B ∩ C) *
          observableFeature H O D := 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 / Appendix B: state-averaged second moment in entanglement features

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$ supply a probability law $\lambda$ on global unitary matrices and set $\nu=N^{-1}\sum_b(U\mapsto U^\dagger|b\rangle\langle b|U)_*\lambda$ . For local unitary families $V=(V_i)_{i<n}$ , put $L_V=\bigotimes_iV_i$ , assume $(S\mapsto L_V^\dagger SL_V)_*\nu=\nu$ for every $V$ , and let $H$ be a probability measure on these families invariant under multiplication on the left by every fixed family. Define $\mathcal M(X)_{ij}=\sum_{k,l}(\int NS_{ij}S_{lk}\,d\nu(S))X_{kl}$ , assume $\mathcal M$ is injective, and write $\mathcal R=\mathcal M^{-1}$ . Let $\rho$ be positive semidefinite of trace $1$ , and let $O$ be Hermitian of trace $0$ . For any matrix $\sigma$ , set $d\nu_\sigma(S)=[N\operatorname{Re}\operatorname{tr}(S\sigma)]_+d\nu(S)$ , and put $z(S)=\operatorname{Re}\operatorname{tr}(O\mathcal R(S))$ and

\overline Q=\int\left(\int z(S)^2\,d\nu_{L_V^\dagger\rho L_V}(S)\right)dH(V).

For subsets $A$ of the sites, let $\operatorname{Tr}_{A^c}X$ be the matrix with entries $\sum_zX_{(x,z),(y,z)}$ , summing over configurations on the complement, and define

f(A)=\int\operatorname{Re}\operatorname{tr}((\operatorname{Tr}_{A^c}S)^2)\,d\nu(S), \qquad o(A)=\int\operatorname{Re}\operatorname{tr}((\operatorname{Tr}_{A^c}(L_V^\dagger OL_V))^2)\,dH(V).

Let $r$ be any real function on site subsets satisfying, for every $B$ ,

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

Then the theorem asserts both

\overline Q=\int z(S)^2\,d\nu(S)

and

\overline Q= \sum_{A,B,C,D} r(A)r(B)\left(\frac{d^2}{d^2-1}\right)^n \frac{d^{|A\cap B\cap C|}}{d^{|C|}} (-1/d)^{|C\triangle D|} f(A\cap B\cap C)\,o(D).

Every subset sum includes the empty subset; $n=0$ is 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