The Gurvits–Barnum separable ball

Abstract

Block positivity bounds the Frobenius sum by the real trace and gives a separable ball about a scalar identity.

All matrices act on the product index set Fin m times Fin n. SeparableCone consists of finite sums of Kronecker products of positive semidefinite factors. BlockPositive means that the real quadratic form is nonnegative on every product vector. The Frobenius sum below is the sum of squared entry norms, independently of any default norm on matrices. Empty index sets and a ball of radius zero are included.

Definition 1.1 (Interchanging the two tensor factors).

$$\forall (m:\mathbb{N}),(\forall (n:\mathbb{N}),(\forall (H:Matrix\left((Fin\left(m\right)\times Fin\left(n\right)),(Fin\left(m\right)\times Fin\left(n\right)),\mathbb{C}\right)),((flip\left(H\right):Matrix\left((Fin\left(n\right)\times Fin\left(m\right)),(Fin\left(n\right)\times Fin\left(m\right)),\mathbb{C}\right))=\mathrm{Matrix}.\mathrm{submatrix}\left(H,\mathrm{Prod}.\mathrm{swap},\mathrm{Prod}.\mathrm{swap}\right))))$$

Formalization. D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.flip (✓ std3).

Source. Repository-derived.

Acknowledgement. Leonid Gurvits and Howard Barnum (2002). Largest separable balls around the maximally mixed bipartite quantum state. DOI: 10.1103/PhysRevA.66.062311. URL: https://doi.org/10.1103/PhysRevA.66.062311.

Commentary.

The flip of a matrix is its submatrix along the product-index swap in both arguments. It acts on Fin n times Fin m when the original matrix acts on Fin m times Fin n, and is defined for all natural dimensions, including zero.

Theorem 1.2 (Tensor-factor interchange preserves the trace).

$$\forall (m:\mathbb{N}),(\forall (n:\mathbb{N}),(\forall (H:Matrix\left((Fin\left(m\right)\times Fin\left(n\right)),(Fin\left(m\right)\times Fin\left(n\right)),\mathbb{C}\right)),(\mathrm{Matrix}.\mathrm{trace}\left(flip\left(H\right)\right)=\mathrm{Matrix}.\mathrm{trace}\left(H\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.trace_flip (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Leonid Gurvits and Howard Barnum (2002). Largest separable balls around the maximally mixed bipartite quantum state. DOI: 10.1103/PhysRevA.66.062311. URL: https://doi.org/10.1103/PhysRevA.66.062311.

Commentary.

Interchanging both product indices only reorders the diagonal entries. Expanding the trace as the two finite coordinate sums and interchanging those sums proves equality of the complex traces.

Theorem 1.3 (Positive semidefinite trace-square bound).

$$\forall (I:Type),[Fintype\left(I\right)],\forall (C:Matrix\left(I,I,\mathbb{C}\right)),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(C\right))\Rightarrow \mathrm{Complex}.\mathrm{re}\left((\mathrm{Matrix}.\mathrm{trace}\left((C\cdot C)\right))\right)\le (\mathrm{Complex}.\mathrm{re}\left((\mathrm{Matrix}.\mathrm{trace}\left(C\right))\right){)}^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.psd_trace_sq (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a positive semidefinite complex matrix on any finite index type, the real trace of its square is at most the square of its real trace. Its eigenvalues are nonnegative, so the sum of their squares is at most the square of their sum. The empty index type gives equality at zero.

Theorem 1.4 (Block-positive Frobenius bound).

$$\forall (m:\mathbb{N}),\forall (n:\mathbb{N}),\forall (H:Fin\left(m\right)\times Fin\left(n\right)\to Fin\left(m\right)\times Fin\left(n\right)\to \mathbb{C}),((Hermitian\left(H\right))\wedge (BlockPositive\left(H\right)))\Rightarrow (0\le Re\left(tr\left(H\right)\right))\wedge (\sum _{u:Fin\left(m\right)\times Fin\left(n\right)}\sum _{v:Fin\left(m\right)\times Fin\left(n\right)}{\Vert H\left(u,v\right)\Vert }^2\le (Re\left(tr\left(H\right)\right){)}^2)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.frobSq_le_trace_sq_of_blockPositive (✓ std3). ∎

Citation. Leonid Gurvits and Howard Barnum (2002). Largest separable balls around the maximally mixed bipartite quantum state. DOI: 10.1103/PhysRevA.66.062311. URL: https://doi.org/10.1103/PhysRevA.66.062311.

Commentary.

Szarek–Werner–Zyczkowski, J. Math. Phys. 49, 032113 (2008), printed page 18, states Tr(H squared) ≤ (Tr H) squared for block-positive H, as quoted in the Gurvits–Barnum note. For Hermitian H, the entrywise Frobenius sum equals Tr(H squared), so the formal inequality is the same statement, with the nonnegative real trace also made explicit. Compressing H against a vector in either factor gives a positive semidefinite matrix. Its trace square bounds its Frobenius sum. Applying the corrected finite fourth-moment identity in each factor gives two inequalities whose partial-trace terms cancel. Product basis vectors give the nonnegative trace.

Theorem 1.5 (Separable ball criterion).

$$\forall (m:\mathbb{N}),\forall (n:\mathbb{N}),\forall (A:Fin\left(m\right)\times Fin\left(n\right)\to Fin\left(m\right)\times Fin\left(n\right)\to \mathbb{C}),\forall (c:\mathbb{R}),((PSD\left(A\right))\wedge ((0\le c)\wedge (\sum _{u:Fin\left(m\right)\times Fin\left(n\right)}\sum _{v:Fin\left(m\right)\times Fin\left(n\right)}{\Vert (A-c\cdot I)\left(u,v\right)\Vert }^2\le c^2)))\Rightarrow SeparableCone\left(A\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.separableCone_of_frob_ball (✓ std3). ∎

Citation. Leonid Gurvits and Howard Barnum (2002). Largest separable balls around the maximally mixed bipartite quantum state. DOI: 10.1103/PhysRevA.66.062311. URL: https://doi.org/10.1103/PhysRevA.66.062311.

Commentary.

Gurvits–Barnum Theorem 1, printed page 4, states that I + Delta is separable when Delta is Hermitian and its Frobenius norm is at most one. The formal statement is its scalar form A = c(I + Delta), using the scaling in Corollary 2, printed page 5; c = 0 gives the zero matrix. If the PSD matrix were outside the separable cone, the separation theorem would give a block-positive matrix with negative Hilbert–Schmidt pairing. Its Hermitian part preserves both product quadratic forms and pairing with the given PSD matrix. The Frobenius bound and Cauchy–Schwarz force that pairing to be nonnegative throughout the stated ball, a contradiction.

Theorem 1.6 (Unit rank-one complement).

$$\forall (m:\mathbb{N}),\forall (n:\mathbb{N}),\forall (psi:Fin\left(m\right)\times Fin\left(n\right)\to \mathbb{C}),(\sum _{u:Fin\left(m\right)\times Fin\left(n\right)}{\Vert psi\left(u\right)\Vert }^2=1)\Rightarrow SeparableCone\left((I-vecMulVec\left(psi,star\left(psi\right)\right))\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.separableCone_one_sub_rankOne (✓ std3). ∎

Source. Repository-derived.

Commentary.

A unit vector gives an orthogonal rank-one projection of trace one and Frobenius sum one. Its complement is PSD and lies in the radius-one ball about the identity. This supplies the codimension-one ray in a spectral decomposition.

Theorem 1.7 (Projection ray).

$$\forall (m:\mathbb{N}),\forall (n:\mathbb{N}),\forall (Q:Fin\left(m\right)\times Fin\left(n\right)\to Fin\left(m\right)\times Fin\left(n\right)\to \mathbb{C}),\forall (ell:\mathbb{R}),((Hermitian\left(Q\right))\wedge ((Q\cdot Q=Q)\wedge ((tr\left(Q\right)=ell)\wedge (1\le ell))))\Rightarrow SeparableCone\left(((ell+1)\cdot I-2\cdot Q)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.separableCone_scaled_one_sub_two_projection (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a Hermitian idempotent Q of real trace ell at least one, the matrix is PSD: it is the sum of ell minus one times the identity and twice the complement of Q. Its squared distance from ell plus one times the identity is 4 ell, which is at most the square of ell plus one. The real trace parameter includes integer ranks by coercion. This supplies the complementary high-rank rays in a spectral decomposition.

References

• Truth anchor: D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.flip
• Truth anchor: D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.frobSq_le_trace_sq_of_blockPositive
• Truth anchor: D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.psd_trace_sq
• Truth anchor: D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.separableCone_of_frob_ball
• Truth anchor: D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.separableCone_one_sub_rankOne
• Truth anchor: D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.separableCone_scaled_one_sub_two_projection
• Truth anchor: D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumBall.trace_flip
• Dependency: D5/S3/Quantum/Entanglement/AbsoluteSeparability/GurvitsBarnumMoments
• Dependency: D5/S3/Quantum/GNSMatrix
• Dependency: D5/S3/Quantum/Information/PartialTraceMutualInformation
• Dependency: D5/S3/Resource/SeparableConeResidualWitness