Robertson-Schrodinger Identity

Abstract

Centered vectors satisfy an exact Robertson-Schrodinger identity with a nonnegative Gram remainder.

Theorem 1.1 (Centered vectors satisfy the Robertson-Schrodinger identity).

$$\begin{array}{c}\forall E:{\mathrm{Type}}^{\ast },[\mathrm{NormedAddCommGroup}(E)],[\mathrm{InnerProductSpace}(\mathbb{C},E)],\\ \forall A,B:E{\to }_{\mathbb{C}}E,\forall \psi \in E,\mathrm{IsSymmetric}(A)\wedge \mathrm{IsSymmetric}(B)\wedge \Vert \psi \Vert =1\Rightarrow \\ (u:=A\psi -⟨\psi ,A\psi {⟩}_{\mathbb{C}}\cdot \psi )\wedge (v:=B\psi -⟨\psi ,B\psi {⟩}_{\mathbb{C}}\cdot \psi )\wedge \\ (\mathrm{Cov}:=\frac{1}{2}\cdot \mathrm{re}(⟨\psi ,(AB+BA)\psi {⟩}_{\mathbb{C}})-\mathrm{re}(⟨\psi ,A\psi {⟩}_{\mathbb{C}})\cdot \mathrm{re}(⟨\psi ,B\psi {⟩}_{\mathbb{C}}))\wedge \\ (c:=\frac{1}{2i}⟨\psi ,(AB-BA)\psi {⟩}_{\mathbb{C}})\wedge \\ (G:=\Vert u{\Vert }^2\cdot \Vert v{\Vert }^2-\Vert ⟨u,v{⟩}_{\mathbb{C}}{\Vert }^2)\Rightarrow \\ \Vert u{\Vert }^2\cdot \Vert v{\Vert }^2={\mathrm{Cov}}^2+\Vert c{\Vert }^2+G\wedge G\ge 0\wedge \\ \mathrm{re}(⟨u,v{⟩}_{\mathbb{C}})=\mathrm{Cov}\wedge \mathrm{ofReal}(\mathrm{im}(⟨u,v{⟩}_{\mathbb{C}}))=c.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/QuantumBounds/RobertsonSchrodinger.robertson_schrodinger (✓ std3). ∎

Citation. H. P. Robertson (1929). The Uncertainty Principle. DOI: 10.1103/PhysRev.34.163.

Commentary.

The parent declaration gram_wedge_identity applies to arbitrary vectors u and v in any normed additive commutative group with a complex inner-product-space structure. It defines G as the product of the squared norms minus the squared norm of the inner product, states the defining equality, and proves G nonnegative from mathlib’s Cauchy-Schwarz theorem. It assumes no operators, symmetricity, distinguished vector, or normalization.

The adapter takes complex-linear symmetric operators A and B and a unit vector psi. Its centered vectors u and v have squared norms equal to the two variances. The real part of their inner product is the symmetric covariance Cov, while the complex coercion of the imaginary part is one over two i times the expectation of AB minus BA. Substitution into the parent identity gives the displayed equality with the same nonnegative G.

Robertson’s 1929 relation retains the commutator lower bound, and Schrodinger’s 1930 refinement additionally retains the symmetric covariance term. The exact equality here also retains the Gram remainder: discarding G recovers the strengthened lower bound, and discarding both G and the covariance contribution recovers the weaker bound. No finite-dimensional, completeness, spectral, or unbounded-operator domain theory is asserted.

References

• Truth anchor: D5/S3/QuantumBounds/RobertsonSchrodinger.robertson_schrodinger