A positive map reflecting positive contractions

Abstract

Bourin’s Question 1 has a negative answer for the Frobenius norm and the square-root function.

Definition 1.1 (Question 1).

$$\mathrm{claim}=(\forall (n:\mathbb{N}),(\forall (k:\mathbb{N}),(\forall (Phi:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right){\to }_l[\mathbb{C}]\mathrm{Matrix}\left(\mathrm{Fin}\left(k\right),\mathrm{Fin}\left(k\right),\mathbb{C}\right)),((\forall (X:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),((0\le X)\Rightarrow (0\le Phi\left(X\right))))\Rightarrow ((Ph{i}^{-1}(\{X:\mathrm{Matrix}\left(\mathrm{Fin}\left(k\right),\mathrm{Fin}\left(k\right),\mathbb{C}\right)|((0\le X)\wedge (X\le 1))\})\subseteq \{X:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)|((0\le X)\wedge (X\le 1))\})\Rightarrow (\forall (M:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),((0\le M)\Rightarrow (\forall (N:D5.S3.Quantum.Schatten.\mathrm{UINorm}\left(k\right)),(\forall (f:\mathbb{R}\to \mathbb{R}),((\mathrm{ConcaveOn}\left(\mathbb{R},\mathrm{Set}.\mathrm{Ici}\left(0\right),f\right))\Rightarrow ((\forall (x:\mathbb{R}),((0\le x)\Rightarrow (0\le f\left(x\right))))\Rightarrow (N.N\left(\mathrm{cfc}\left(f,Phi\left(M\right)\right)\right)\le N.N\left(Phi\left(\mathrm{cfc}\left(f,M\right)\right)\right)))))))))))))$$

Formalization. D5/S3/Quantum/Schatten/BourinQuestionOneRefutation.claim (✓ std3).

Citation. Jean-Christophe Bourin (2008). Matrix subadditivity inequalities and block-matrices. DOI: 10.1142/S0129167X09005509. URL: https://arxiv.org/abs/0805.1954v1.

Commentary.

Bourin, arXiv:0805.1954v1, p. 3, Question 1: “Let Φ : M_n → M_k be a positive linear map between the algebras of matrices of size n and k and let F_n and F_k be the sets of non-expansive, positive operators in M_n and M_k respectively. Does Φ⁻¹(F_k) ⊂ F_n imply ‖f ∘ Φ(M)‖ ≤ ‖Φ ∘ f(M)‖ for all M ≥ 0, all symmetric norms and all non-negative concave functions on the positive half line?”

The matrices are complex, and 1 is the identity matrix. The order is the Loewner order. Non-expansive positive matrices are exactly the matrices X with 0 ≤ X and X ≤ 1; the preimage is taken in the entire matrix algebra. The type D5.S3.Quantum.Schatten.UINorm contains the norm laws and invariance under left and right multiplication by unitary matrices. Its field N evaluates the norm. The real function f is concave and nonnegative on [0,∞); cfc applies it by continuous functional calculus.

Theorem 1.2 (The Frobenius inequality fails).

$$\neg (\forall (n:\mathbb{N}),(\forall (k:\mathbb{N}),(\forall (Phi:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right){\to }_l[\mathbb{C}]\mathrm{Matrix}\left(\mathrm{Fin}\left(k\right),\mathrm{Fin}\left(k\right),\mathbb{C}\right)),((\forall (X:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),((0\le X)\Rightarrow (0\le Phi\left(X\right))))\Rightarrow ((Ph{i}^{-1}(\{X:\mathrm{Matrix}\left(\mathrm{Fin}\left(k\right),\mathrm{Fin}\left(k\right),\mathbb{C}\right)|((0\le X)\wedge (X\le 1))\})\subseteq \{X:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)|((0\le X)\wedge (X\le 1))\})\Rightarrow (\forall (M:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),((0\le M)\Rightarrow (\forall (N:D5.S3.Quantum.Schatten.\mathrm{UINorm}\left(k\right)),(\forall (f:\mathbb{R}\to \mathbb{R}),((\mathrm{ConcaveOn}\left(\mathbb{R},\mathrm{Set}.\mathrm{Ici}\left(0\right),f\right))\Rightarrow ((\forall (x:\mathbb{R}),((0\le x)\Rightarrow (0\le f\left(x\right))))\Rightarrow (N.N\left(\mathrm{cfc}\left(f,Phi\left(M\right)\right)\right)\le N.N\left(Phi\left(\mathrm{cfc}\left(f,M\right)\right)\right)))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Schatten/BourinQuestionOneRefutation.result (✓ std3). ∎

Resolves. Problems/bourin-2008-matrix-subadditivity-question-1 (refuted) by D5/S3/Quantum/Schatten/BourinQuestionOneRefutation.result.

Source. Repository-derived.

Acknowledgement. Jean-Christophe Bourin (2008). Matrix subadditivity inequalities and block-matrices. DOI: 10.1142/S0129167X09005509. URL: https://arxiv.org/abs/0805.1954v1.

Commentary.

Take n = 1, k = 2, Φ(X) = Matrix.diagonal ![X 0 0, X 0 0 / 4], M = 1 and f = Real.sqrt. Positivity of the first diagonal entry reflects positivity, and the upper bound on that entry reflects the upper bound by 1. The functional-calculus values are Matrix.diagonal ![1, 1/2] and Matrix.diagonal ![1, 1/4]. Their Frobenius norm squares are 5/4 and 17/16, respectively, contradicting the proposed inequality.

The Frobenius norm laws come from Matrix’s Frobenius norm. Its two-sided unitary invariance follows from invariance of RHLinalg.frobSq and its equality with the squared Frobenius norm. The first block suffices to reflect positive contractions, whereas the square root increases the second weight from 1/4 to 1/2. This argument concerns Question 1; it makes no assertion about Question 2 or a restriction to the operator norm.

References

• Truth anchor: D5/S3/Quantum/Schatten/BourinQuestionOneRefutation.claim
• Truth anchor: D5/S3/Quantum/Schatten/BourinQuestionOneRefutation.result
• Dependency: D5/S3/Quantum/Dynamics/EntropyProductionCoherenceDeletionIdentity
• Dependency: D5/S3/Quantum/GNSMatrix
• Dependency: D5/S3/Quantum/Matrix/CommutatorGap
• Dependency: D5/S3/Quantum/Schatten/UnitarilyInvariantNorm