Local frame-potential inequality and exact gap identity

Open

QAlgorithms.Papers.Independent.Intakethird100.P71.framePotential_gap

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

prove2quantum

Let $\nu$ be the prior of any projective experiment on $N$ qudits, $d\ge2$ , and let $\nu^{\rm LS}$ be its conjugation twirl by normalized local Haar measure. Define $M_2(\nu)=\mathbb E_\nu S^{\otimes2}$ and $F_2(\nu)=\mathbb E_{S,S'\sim\nu}[\operatorname{Tr}(SS')]^2$ , with independent snapshots. If $W_A$ is the second EF and $\mathrm{Wg}_{A,B}=(d^2-1)^{-N}(-1/d)^{|A\triangle B|}$ , then

F_2(\nu)\ge F_2(\nu^{\rm LS})=\sum_{A,B}W_A\mathrm{Wg}_{A,B}W_B,

\Delta_2=F_2(\nu)-F_2(\nu^{\rm LS})=\operatorname{Tr}\bigl[(M_2(\nu)-M_2(\nu^{\rm LS}))^2\bigr].

Thus $\Delta_2=0$ exactly when these second moments agree, and local invariance of the whole prior law implies zero gap. At zero gap, inversion of the complete twirled measurement channel reconstructs every density matrix without bias from the original posterior. The twirled moment averages jointly over the local unitary and the snapshot. Equality of second moments does not assert equality of the full 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.12 Eqs.(42)–(45): frame-potential inequality, EF value of the
locally twirled limit, and the trace of the square gap identity. The second
moment in the difference averages over BOTH V and the snapshot. Zero gap
ensures exact reconstruction when the twirled channel is complete; it does not
imply invariance of the entire probability law. -/
theorem framePotential_gap {n d : ℕ} (hd : 2 ≤ d) (E : ProjectiveEnsemble n d)
    (H : Measure (Local n d)) [IsProbabilityMeasure H] [H.IsMulLeftInvariant] :
    framePotential (twirled H (prior E)) ≤ framePotential (prior E) ∧
    framePotential (twirled H (prior E)) =
      ∑ A : Finset (Fin n), ∑ B : Finset (Fin n),
        feature (prior E) A * regionalWg n d A B * feature (prior E) B ∧
    (frameGap H (prior E) : ℂ) =
      ((snapshotMoment (prior E) 2 - snapshotMoment (twirled H (prior E)) 2) *
        (snapshotMoment (prior E) 2 - snapshotMoment (twirled H (prior E)) 2)).trace ∧
    (frameGap H (prior E) = 0 ↔ snapshotMoment (prior E) 2 = snapshotMoment (twirled H (prior E)) 2) ∧
    (LocallyScrambled (prior E) → frameGap H (prior E) = 0) ∧
    (frameGap H (prior E) = 0 → ∀ hc : Complete (twirled H (prior E)),
      ∀ rho : Op n d, IsDensityMatrix rho →
        (∫ S, snapshotInverse (twirled H (prior E)) hc S ∂posteriorOf (prior E) 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. 12, §III D, Eqs.(42)–(45): local frame-potential inequality and gap identity

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, set $\nu=N^{-1}\sum_b(U\mapsto U^\dagger|b\rangle\langle b|U)_*\lambda$ , and let $H$ be a probability measure on local unitary families invariant under left multiplication. Write $L_V=\bigotimes_iV_i$ , and define

\widetilde\nu=((V,S)\mapsto L_V^\dagger SL_V)_*(H\otimes\nu), \quad P(\mu)=\int(\operatorname{Re}\operatorname{tr}(ST))^2\,d(\mu\otimes\mu)(S,T), \quad g=P(\nu)-P(\widetilde\nu),

M_2(\mu)=\int S^{\otimes2}\,d\mu(S), \qquad (S^{\otimes2})_{(x_0,x_1),(y_0,y_1)} =S_{x_0y_0}S_{x_1y_1}.

For each site subset $A$ , put $f(A)=\int\operatorname{Re}\operatorname{tr}((\operatorname{Tr}_{A^c}S)^2)\,d\nu(S)$ , where the partial trace sums matching complementary indices, and put $G(A,B)=(d^2-1)^{-n}(-1/d)^{|A\triangle B|}$ . The theorem asserts

P(\widetilde\nu)\le P(\nu),\qquad P(\widetilde\nu)=\sum_{A,B}f(A)G(A,B)f(B),\qquad g=\operatorname{tr}\bigl((M_2(\nu)-M_2(\widetilde\nu))^2\bigr),

where the last equality embeds the real number $g$ in $\mathbb C$ and uses the matrix square. It also asserts $g=0$ if and only if $M_2(\nu)=M_2(\widetilde\nu)$ , and asserts that invariance $(S\mapsto L_V^\dagger SL_V)_*\nu=\nu$ for every local $V$ implies $g=0$ . Finally, if $g=0$ , then for every assumption that the map

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

is injective, its complex-linear inverse $\mathcal R_{\widetilde\nu}$ satisfies

\int\mathcal R_{\widetilde\nu}(S)\,d\nu_\rho(S)=\rho

for every positive semidefinite matrix $\rho$ of trace $1$ , where $d\nu_\rho=[N\operatorname{Re}\operatorname{tr}(S\rho)]_+d\nu$ uses the original measure $\nu$ . 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