Weighted Bottcher-Wenzel, case (ii)

Abstract

The squared weighted Bottcher-Wenzel conjecture holds for every positive definite weight.

Definition 1.1 (Squared weighted Frobenius norm).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),W\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\mathrm{weightedSq}\left(A,W\right)=Complex.re(Matrix.trace(Matrix.conjTranspose(A)\cdot A\cdot W))$$

Formalization. D5/S3/Quantum/Matrix/WeightedBotcherWenzel.weightedSq (✓ std3).

Citation. Aina Mayumi; Gen Kimura; Hiromichi Ohno; Dariusz Chruściński (2024). Böttcher-Wenzel inequality for weighted Frobenius norms and its application to quantum physics. DOI: 10.1016/j.laa.2024.07.013. URL: https://arxiv.org/abs/2403.04199v2.

Commentary.

The source defines: “In what follows we call ω-weighted Frobenius norm” followed by “‖A‖ω := √tr(A∗Aω)” (equation (2), page 2). This is its literal squared trace expression, using the real part for the real-valued result.

Theorem 1.2 (Additive weight dependence).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),W\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),V\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\mathrm{weightedSq}\left(A,W+V\right)=\mathrm{weightedSq}\left(A,W\right)+\mathrm{weightedSq}\left(A,V\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/WeightedBotcherWenzel.weighted_add (✓ std3). ∎

Source. Repository-derived.

Commentary.

Trace and right matrix multiplication are additive in the weight.

Theorem 1.3 (Real scaling of the weight).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),W\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),t\in \mathbb{R},\mathrm{weightedSq}\left(A,t\cdot (W)\right)=t\cdot \mathrm{weightedSq}\left(A,W\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/WeightedBotcherWenzel.weighted_smul (✓ std3). ∎

Source. Repository-derived.

Commentary.

The real part of the trace respects real scalar multiplication.

Theorem 1.4 (Identity weight).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\mathrm{weightedSq}\left(A,1\right)=RHLinalg.frobSq(A)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/WeightedBotcherWenzel.weighted_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

The identity weight gives the ordinary Frobenius square.

Theorem 1.5 (Projection weight equals projected norm).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),P\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\left(Matrix.IsHermitian(P)\wedge P\cdot P=P\right)\Rightarrow \mathrm{weightedSq}\left(A,P\right)=RHLinalg.frobSq(A\cdot P)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/WeightedBotcherWenzel.projected_trace (✓ std3). ∎

Source. Repository-derived.

Commentary.

Hermiticity and idempotence permit trace cycling to the Gram matrix of AP.

Theorem 1.6 (Projection commutator channel bound).

$$\forall n\in \mathbb{N},A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),B\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),P\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\left(Matrix.IsHermitian(P)\wedge P\cdot P=P\right)\Rightarrow RHLinalg.frobSq(\mathrm{commutator}\left(A,B\right)\cdot P)\le \left(RHLinalg.frobSq(A)+2\cdot RHLinalg.frobSq(A\cdot P)+2\cdot Real.sqrt(RHLinalg.frobSq(A\cdot P)\cdot \mathrm{gap}\left(A\right))\right)\cdot RHLinalg.frobSq(B)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/WeightedBotcherWenzel.projection_gap (✓ std3). ∎

Source. Repository-derived.

Commentary.

The SVD expresses a contraction as an average of two actual unitaries. A common-radius bound for scalar pencils transfers to the projected adjoint channel, for every projection rank and including zero input matrices.

Definition 1.7 (Attained spectral endpoints).

$$\forall n\in \mathbb{N},W\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),lo\in \mathbb{R},hi\in \mathbb{R},\mathrm{SpectralExtrema}\left(W,lo,hi\right)\iff \left(\exists h\in Matrix.IsHermitian(W),\left(\forall i\in \mathrm{Fin}\left(n\right),lo\le \mathrm{eigenvalues}\left(h\right)(i)\wedge \mathrm{eigenvalues}\left(h\right)(i)\le hi\right)\wedge \left(\left(\exists i\in \mathrm{Fin}\left(n\right),\mathrm{eigenvalues}\left(h\right)(i)=lo\right)\wedge \left(\exists i\in \mathrm{Fin}\left(n\right),\mathrm{eigenvalues}\left(h\right)(i)=hi\right)\right)\right)$$

Formalization. D5/S3/Quantum/Matrix/WeightedBotcherWenzel.SpectralExtrema (✓ std3).

Source. Repository-derived.

Commentary.

Every eigenvalue lies between lo and hi, and each endpoint is attained. Thus these parameters are exactly the smallest and largest eigenvalues, including repeated eigenvalues.

Definition 1.8 (Conjecture 1, equation (15)).

$$claim\iff (\forall n\in \mathbb{N},0<n\Rightarrow \left(\forall W\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),lo\in \mathbb{R},hi\in \mathbb{R},Matrix.PosDef(W)\Rightarrow \left(0<lo\Rightarrow \left(\mathrm{SpectralExtrema}\left(W,lo,hi\right)\Rightarrow \left(\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),B\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\mathrm{weightedSq}\left(\mathrm{commutator}\left(A,B\right),W\right)\le \left(1+\frac{hi}{lo}\right)\cdot \mathrm{weightedSq}\left(A,W\right)\cdot RHLinalg.frobSq(B)\right)\right)\right)\right))$$

Formalization. D5/S3/Quantum/Matrix/WeightedBotcherWenzel.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. Aina Mayumi; Gen Kimura; Hiromichi Ohno; Dariusz Chruściński (2024). Böttcher-Wenzel inequality for weighted Frobenius norms and its application to quantum physics. DOI: 10.1016/j.laa.2024.07.013. URL: https://arxiv.org/abs/2403.04199v2.

Commentary.

“Conjecture 1. For any matrices A, B ∈ Mₙ(ℂ),” followed by equation (15), “‖[A, B]‖ω ≤ √((λm + λM)/λm) ‖A‖ω ‖B‖” (arXiv:2403.04199v2, page 6). The encoding uses Matrix (Fin n) (Fin n) ℂ for n greater than zero, PosDef for the positive definite weight, and SpectralExtrema for the attained endpoints lo = λm and hi = λM. Squaring the nonnegative norms gives constant 1 + hi/lo. The weighted and ordinary squares are the real trace formulas; commutator means AB minus BA.

Theorem 1.9 (The weighted inequality).

$$claim$$

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

Resolves. Problems/mayumi-kimura-ohno-chruscinski-2024-weighted-bottcher-wenzel-ii (proved) by D5/S3/Quantum/Matrix/WeightedBotcherWenzel.result.

Source. Repository-derived.

Acknowledgement. Aina Mayumi; Gen Kimura; Hiromichi Ohno; Dariusz Chruściński (2024). Böttcher-Wenzel inequality for weighted Frobenius norms and its application to quantum physics. DOI: 10.1016/j.laa.2024.07.013. URL: https://arxiv.org/abs/2403.04199v2.

Commentary.

The projection channel bound and nonnegative commutator gap give a square-completion lower bound for every two-level weight. A spectral convex decomposition transfers the inequality to an arbitrary positive definite weight. This statement is case (ii). Cases (i) and (iv) are separate questions.

References

• Truth anchor: D5/S3/Quantum/Matrix/WeightedBotcherWenzel.SpectralExtrema
• Truth anchor: D5/S3/Quantum/Matrix/WeightedBotcherWenzel.claim
• Truth anchor: D5/S3/Quantum/Matrix/WeightedBotcherWenzel.projected_trace
• Truth anchor: D5/S3/Quantum/Matrix/WeightedBotcherWenzel.projection_gap
• Truth anchor: D5/S3/Quantum/Matrix/WeightedBotcherWenzel.result
• Truth anchor: D5/S3/Quantum/Matrix/WeightedBotcherWenzel.weightedSq
• Truth anchor: D5/S3/Quantum/Matrix/WeightedBotcherWenzel.weighted_add
• Truth anchor: D5/S3/Quantum/Matrix/WeightedBotcherWenzel.weighted_one
• Truth anchor: D5/S3/Quantum/Matrix/WeightedBotcherWenzel.weighted_smul
• Dependency: D5/S3/Quantum/Foundation/FiniteTraceDistance
• Dependency: D5/S3/Quantum/Matrix/CommutatorGap