Measurement-channel and inverse properties

Open

QAlgorithms.Papers.Independent.Intakethird100.P71.measurementChannel_properties

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

prove2quantum

Fix a Borel probability ensemble of unitaries on $N$ qudits of dimension $d\ge2$ . Write $\nu$ for the prior law of $S=U^\dagger|b\rangle\langle b|U$ , with $b$ uniform independently of $U$ , and $\mathcal M(X)=d^N\mathbb E_\nu[S\operatorname{Tr}(SX)]$ . The prior is a probability measure, each Born-weighted posterior for a density matrix is a probability measure, and the polynomial moment integrands are integrable. The snapshot map is continuous. The channel is completely positive, trace-preserving and self-adjoint:

\operatorname{Tr}\mathcal M(X)=\operatorname{Tr}X,\qquad \operatorname{Tr}(X^\dagger\mathcal M(Y))=\operatorname{Tr}(\mathcal M(X)^\dagger Y).

If $\mathcal M$ is injective, its inverse is also trace-preserving and self-adjoint. Local scrambling and completeness are unnecessary for the forward-channel assertions. This separates the measurement experiment's validity from the assumptions needed for inversion.

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 pp.3–4 Eq.(3): the forward measurement channel is CPTP and self-adjoint,
without local scrambling or completeness. Its inverse, when complete, is
trace-preserving and self-adjoint. Polynomial integrability and Born-law
normalization are conclusions from the projective construction. -/
theorem measurementChannel_properties {n d : ℕ} (hd : 2 ≤ d) (E : ProjectiveEnsemble n d) :
    IsProbabilityMeasure (prior E) ∧ SnapshotPolynomialIntegrable (prior E) ∧
    (∀ b, Continuous (fun U : Unitary n d => raw U b)) ∧
    (∀ rho : Op n d, IsDensityMatrix rho → IsProbabilityMeasure (posteriorOf (prior E) rho)) ∧
    QAlgorithms.IsChannel (snapshotMeasurementMap (prior E)) ∧
    (∀ X : Op n d, (snapshotMeasurementMap (prior E) X).trace = X.trace) ∧
    (∀ X Y : Op n d, (Xᴴ * snapshotMeasurementMap (prior E) Y).trace =
      ((snapshotMeasurementMap (prior E) X)ᴴ * Y).trace) ∧
    (∀ hc : Complete (prior E),
      (∀ X : Op n d, (snapshotInverse (prior E) hc X).trace = X.trace) ∧
      (∀ X Y : Op n d, (Xᴴ * snapshotInverse (prior E) hc Y).trace =
        ((snapshotInverse (prior E) hc X)ᴴ * Y).trace)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P71

end

Source

Classical Shadow Tomography with Locally Scrambled Quantum Dynamics, arXiv:2107.04817v4, PDF p. 3, §II A, Eq.(3): measurement-channel properties

Read-back

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

Let $n\ge0$ and $d\ge2$ be natural numbers, let $\mathcal X=\{0,\ldots,d-1\}^{n}$ , let $N=d^n$ , and let $E$ specify a probability measure $\lambda$ on the unitary matrices on $\mathbb C^{\mathcal X}$ . For $b\in\mathcal X$ , define $S_b(U)=U^\dagger|b\rangle\langle b|U$ , where $|b\rangle$ is the coordinate unit vector, and define the measure $\nu=N^{-1}\sum_b(S_b)_*\lambda$ . For any matrix $\rho$ , let $\nu_\rho$ be the measure having density $[N\operatorname{Re}\operatorname{tr}(S\rho)]_+$ with respect to $\nu$ , where $[x]_+=\max(x,0)$ . Define the complex-linear map $\mathcal M$ by

\mathcal M(X)_{ij} =\sum_{k,l\in\mathcal X} \left(\int N S_{ij}S_{lk}\,d\nu(S)\right)X_{kl}, \qquad (S^{\otimes t})_{xy}=\prod_{a=0}^{t-1}S_{x_a y_a}.

The theorem asserts that $\nu$ is a probability measure; that $S\mapsto S^{\otimes t}$ is integrable for every natural $t$ , including $t=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 of complex matrices $X,Y$ ; and that $U\mapsto S_b(U)$ is continuous for every $b$ . For every positive semidefinite $\rho$ with $\operatorname{tr}\rho=1$ , the measure $\nu_\rho$ is a probability measure. Moreover, $\mathcal M$ has a finite Kraus representation: there are a natural number $q$ and matrices $K_0,\ldots,K_{q-1}$ satisfying $\sum_aK_a^\dagger K_a=I$ and $\mathcal M(X)=\sum_aK_aXK_a^\dagger$ for every $X$ . For all complex matrices $X,Y$ ,

\operatorname{tr}\mathcal M(X)=\operatorname{tr}X, \qquad \operatorname{tr}(X^\dagger\mathcal M(Y)) =\operatorname{tr}(\mathcal M(X)^\dagger Y).

Finally, for every assumption that $\mathcal M$ is injective, let $\mathcal R=\mathcal M^{-1}$ be its complex-linear inverse, which exists because its domain and codomain have the same finite dimension. Then, for all $X,Y$ , $\operatorname{tr}\mathcal R(X)=\operatorname{tr}X$ and $\operatorname{tr}(X^\dagger\mathcal R(Y))=\operatorname{tr}(\mathcal R(X)^\dagger Y)$ . The case $n=0$ , with a single configuration, 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