Two-qudit second moment and operator locality

Open

QAlgorithms.Papers.Independent.Intakethird100.P71.twoQudit_secondMoment

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

prove2quantum

In the complete locally scrambled two-qudit toy experiment, let $d\ge2$ , $2d/(d^2+1)\le w\le1$ , and the snapshot features be $(1,w,w,1)$ . Fix a density matrix $\rho$ and a traceless Hermitian observable $O$ . Write $T=\operatorname{Tr}(O^2)$ and

K=\operatorname{Tr}[(\operatorname{Tr}_2O)^2]+\operatorname{Tr}[(\operatorname{Tr}_1O)^2].

The second moment averaged over local Haar conjugations of $\rho$ is

Q_{\mathrm{av}}(O)=\frac{d^2-1}{d^3}\left(\frac{K}{dw-1}+\frac{(d^2-1)(dT-K)}{d^2-2dw+1}\right).

For nonzero $O$ , putting $k_{\rm tot}=K/T$ recovers Eq. (31). The undivided identity also includes $O=0$ , where both sides vanish. This records the exact dependence on observable locality without introducing undefined purity ratios.

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.(29)–(31): undivided two-qudit formula. K is the sum of the
unnormalized partial purities; for O≠0, k_tot=K/Tr(O²). O=0 is included. -/
theorem twoQudit_secondMoment {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 O : Op 2 d) (hrho : IsDensityMatrix rho) (hO : O.IsHermitian) (ht : O.trace = 0) :
    averagedSecondMoment H (prior E) hc rho O =
      ((d : ℝ)^2-1)/(d : ℝ)^3 *
        (localityNumerator O / ((d : ℝ)*w-1) +
          ((d : ℝ)^2-1) * ((d : ℝ)*hsSquare O - localityNumerator O) /
            ((d : ℝ)^2-2*(d : ℝ)*w+1)) := 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.(29)–(31): two-qudit shadow norm

Read-back

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

Let $d\ge2$ , let $\mathcal X=\{0,\ldots,d-1\}^2$ , and let $E$ specify a probability law $\lambda$ on global unitary matrices. Set $\nu=d^{-2}\sum_b(U\mapsto U^\dagger|b\rangle\langle b|U)_*\lambda$ , and assume that $\nu$ is invariant under $S\mapsto L_V^\dagger SL_V$ for every $L_V=V_0\otimes V_1$ with unitary factors. 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 $w$ satisfy $2d/(d^2+1)\le w\le1$ , and suppose that $\int\operatorname{Re}\operatorname{tr}((\operatorname{Tr}_{A^c}S)^2)\,d\nu(S)$ equals $w$ for each singleton $A\subseteq\{0,1\}$ and equals $1$ for the empty and full subsets; here the partial trace sums matching complementary indices. Let $H$ be a probability measure on pairs of local unitary matrices invariant under left multiplication by every fixed pair. Let $\rho$ be positive semidefinite of trace $1$ , and let $O$ be Hermitian of trace $0$ . Define $z(S)=\operatorname{Re}\operatorname{tr}(O\mathcal R(S))$ , $d\nu_\sigma=[d^2\operatorname{Re}\operatorname{tr}(S\sigma)]_+d\nu$ , and

\overline Q=\int\left(\int z(S)^2\,d\nu_{L_V^\dagger\rho L_V}(S)\right)dH(V), \quad L(O)=\operatorname{Re}\operatorname{tr}((\operatorname{Tr}_{\{1\}}O)^2) +\operatorname{Re}\operatorname{tr}((\operatorname{Tr}_{\{0\}}O)^2), \quad K(O)=\operatorname{Re}\operatorname{tr}(O^2).

The theorem asserts the exact equality

\overline Q=\frac{d^2-1}{d^3} \left[ \frac{L(O)}{dw-1} +\frac{(d^2-1)(dK(O)-L(O))}{d^2-2dw+1} \right].

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