Local and global random-observable comparison, with source correction

Open

QAlgorithms.Papers.Independent.Intakethird100.P71.localGlobal_randomObservableComparison

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

prove2quantum

Consider the complete locally scrambled two-qudit toy experiment with $d\ge2$ , $2d/(d^2+1)\le w\le1$ , snapshot features $(1,w,w,1)$ , and local-state averaged second moment $Q_{\mathrm{av}}$ . Every traceless Hermitian local observable $O_{\rm loc}=A\otimes I$ satisfies

Q_{\mathrm{av}}(O_{\rm loc})=\frac{d^2-1}{d^2(dw-1)}\operatorname{Tr}(O_{\rm loc}^2).

For a trace-removed global GUE observable $G$ , in ensemble expectation,

\mathbb E_G Q_{\mathrm{av}}(G)=\frac{d^2-1}{d^2(d^2+1)}\left(\frac{(d^2-1)^2}{d^2-2dw+1}+\frac{2}{dw-1}\right)\mathbb E_G\operatorname{Tr}(G^2).

The Gaussian integrands are integrable. At $w=2d/(d^2+1)$ every traceless Hermitian $O$ has $Q_{\mathrm{av}}(O)=(1+d^{-2})\operatorname{Tr}(O^2)$ . This compares second moments at a fixed Hilbert–Schmidt scale.

Source correction. The printed global denominator in Eq. (34) is $d^2-2dw-1$ ; it is changed to $d^2-2dw+1$ , as forced by Eq. (31). The printed expression is negative at $d=2,w=4/5$ . The global formula is an ensemble assertion, not an identity for each GUE draw. Independent moderation of this correction is pending.

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.6 Eqs.(32)–(34), corrected consequence of Eq.(31).
Printed: d²−2dw−1 in the global denominator. Changed: d²−2dw+1.
Why: Eq.(31) forces +1; at d=2,w=4/5 the printed expression is negative.
The global GUE statement is an ensemble expectation, not an identity for each
random draw. Traces are removed to obey the section's traceless convention.
This source correction requires independent moderation. -/
theorem localGlobal_randomObservableComparison {d : ℕ} (hd : 2 ≤ d) (E : ProjectiveEnsemble 2 d)
    (hls : LocallyScrambled (prior E)) (hc : Complete (prior E))
    (w : ℝ) (hw : 2*(d : ℝ)/((d : ℝ)^2+1) ≤ w ∧ w ≤ 1) (hf : ToyFeature (prior E) w)
    (H : Measure (Local 2 d)) [IsProbabilityMeasure H] [H.IsMulLeftInvariant]
    (rho : Op 2 d) (hrho : IsDensityMatrix rho) :
    (∀ A : Matrix (Fin d) (Fin d) ℂ, A.IsHermitian → A.trace = 0 →
      averagedSecondMoment H (prior E) hc rho (localObservable A) =
        ((d : ℝ)^2-1)/((d : ℝ)^2*((d : ℝ)*w-1)) * hsSquare (localObservable A)) ∧
    Integrable (fun z => averagedSecondMoment H (prior E) hc rho (gueOperator d z)) (gueCoordinates d) ∧
    Integrable (fun z => hsSquare (gueOperator d z)) (gueCoordinates d) ∧
    (∫ z, averagedSecondMoment H (prior E) hc rho (gueOperator d z) ∂gueCoordinates d) =
      ((d : ℝ)^2-1)/((d : ℝ)^2*((d : ℝ)^2+1)) *
        (((d : ℝ)^2-1)^2/((d : ℝ)^2-2*(d : ℝ)*w+1) + 2/((d : ℝ)*w-1)) *
          (∫ z, hsSquare (gueOperator d z) ∂gueCoordinates d) ∧
    (∀ X : Op 2 d, X.IsHermitian → X.trace = 0 →
      (w = 2*(d : ℝ)/((d : ℝ)^2+1) →
        averagedSecondMoment H (prior E) hc rho X = (1 + ((d : ℝ)^2)⁻¹) * hsSquare X)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P71

end

Source

Classical Shadow Tomography with Locally Scrambled Quantum Dynamics, arXiv:2107.04817v4, PDF p. 6, §II C, Eqs.(32)–(34): local/global random-observable comparison, with correction

Read-back

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

Let $d\ge2$ , $\mathcal X=\{0,\ldots,d-1\}^2$ , and let $E$ give a probability law $\lambda$ on global unitary matrices. Define $\nu=d^{-2}\sum_b(U\mapsto U^\dagger|b\rangle\langle b|U)_*\lambda$ ; assume it is invariant under $S\mapsto L_V^\dagger SL_V$ for every local tensor product $L_V=V_0\otimes V_1$ . Define $\mathcal M(X)_{ij}=\sum_{k,l}(\int d^2S_{ij}S_{lk}\,d\nu(S))X_{kl}$ , assume it is injective, and write $\mathcal R=\mathcal M^{-1}$ . Let $2d/(d^2+1)\le w\le1$ , and assume that $f(A)=\int\operatorname{Re}\operatorname{tr}((\operatorname{Tr}_{A^c}S)^2)\,d\nu(S)$ equals $w$ for singleton $A\subseteq\{0,1\}$ and $1$ otherwise, where the partial trace sums matching complementary indices. Let $H$ be a probability measure on local unitary pairs invariant under left multiplication, and let $\rho$ be positive semidefinite of trace $1$ . For any observable $O$ , define

Q_\rho(O)= \int\left(\int [\operatorname{Re}\operatorname{tr}(O\mathcal R(S))]^2 \,d\nu_{L_V^\dagger\rho L_V}(S)\right)dH(V), \qquad d\nu_\sigma=[d^2\operatorname{Re}\operatorname{tr}(S\sigma)]_+d\nu, \quad K(O)=\operatorname{Re}\operatorname{tr}(O^2).

For every Hermitian $d\times d$ matrix $A$ with $\operatorname{tr}A=0$ , the theorem asserts

Q_\rho(A\otimes I)=\frac{d^2-1}{d^2(dw-1)}K(A\otimes I).

Let $\gamma$ be the product measure under which all real coordinates $z_{ij,0},z_{ij,1}$ , for $i,j\in\mathcal X$ , are independent Gaussian random variables of mean $0$ and variance $1$ . Set $Z_{ij}=z_{ij,0}+iz_{ij,1}$ , $G_0=(Z+Z^\dagger)/2$ , and $G(z)=G_0-\operatorname{tr}(G_0)I/d^2$ . Both $z\mapsto Q_\rho(G(z))$ and $z\mapsto K(G(z))$ are integrable with respect to $\gamma$ , and

\int Q_\rho(G(z))\,d\gamma(z)= \frac{d^2-1}{d^2(d^2+1)} \left[\frac{(d^2-1)^2}{d^2-2dw+1}+\frac2{dw-1}\right] \int K(G(z))\,d\gamma(z).

Finally, every Hermitian matrix $X$ on $\mathbb C^{\mathcal X}$ with trace $0$ satisfies the implication

w=\frac{2d}{d^2+1}\quad\Longrightarrow\quad Q_\rho(X)=(1+d^{-2})K(X).

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