Mixed-State Robertson Uncertainty

Abstract

Mixed-state standard deviations bound the expected commutator magnitude.

Theorem 1.1 (Mixed-state Robertson uncertainty).

$$\begin{array}{r}\forall d:\mathrm{Type},[\mathrm{Fintype}(d)],[\mathrm{DecidableEq}(d)],\\ \forall \rho :\mathrm{DensityState}\left(d\right),A,B:\mathrm{Matrix}\left(d,d,\mathbb{C}\right),\\ \mathrm{Hermitian}(A)\wedge \mathrm{Hermitian}(B)\Rightarrow \\ (rhoMatrix:=\mathrm{toMatrix}\left(\rho \right))\wedge (stateRoot:=\sqrt{rhoMatrix})\wedge \\ (u:=(A-\mathrm{Tr}(rhoMatrix\cdot A)\cdot I)\cdot stateRoot)\wedge (v:=(B-\mathrm{Tr}(rhoMatrix\cdot B)\cdot I)\cdot stateRoot)\Rightarrow \\ \Vert u{\Vert }_{HS}\Vert v{\Vert }_{HS}\ge \frac{1}{2}\Vert \mathrm{Tr}(rhoMatrix\cdot (AB-BA))\Vert .\end{array}$$

Proof. Machine-checked in Lean as D5/S3/QuantumBounds/Designs/MixedStateRobertson.mixed_state_robertson_uncertainty (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let d be a finite index type with decidable equality, rho a canonical density state, and A and B Hermitian complex square matrices. The density-state carrier supplies positivity and trace-one normalization.

The underlying density matrix and its positive continuous-functional-calculus square root construct the centered GNS vectors u and v. Their Frobenius norms are the two standard deviations.

Cauchy-Schwarz bounds the weighted cross pairing, whose imaginary part is one half of the expected commutator. This gives the displayed Robertson inequality for mixed as well as pure density states.

References

• Truth anchor: D5/S3/QuantumBounds/Designs/MixedStateRobertson.mixed_state_robertson_uncertainty
• Dependency: D5/S3/Quantum/Divergence/QuantumRelativeEntropyDefectComposition
• Dependency: D5/S3/Quantum/GNSMatrix