Nobori's spectral-middle-factor commutator conjecture
Let $\|\cdot\|_F$ be the Frobenius norm, $\|\cdot\|_2$ the operator norm, and $\sigma_1(X) \ge \sigma_2(X) \ge \cdots$ the singular values of $X$. For square $X, Y$, Audenaert sharpened the Böttcher–Wenzel inequality $\|XY - YX\|_F^2 \le 2\|X\|_F^2\|Y\|_F^2$ to $$\|XY - YX\|_F^2 \le 2\|X\|_F^2\bigl(\sigma_1(Y)^2 + \sigma_2(Y)^2\bigr),$$ which is the case $m = n$, $B = I_n$ of the inequality below. Nobori proved $\|ABC - CBA\|_F^2 \le 2\|C\|_2^2\bigl(\sigma_1(A)^2 + \sigma_2(A)^2\bigr)\|B\|_F^2$ for all $A, C \in \mathbb{C}^{m \times n}$ and $B \in \mathbb{C}^{n \times m}$.
Problem. Let $m, n \ge 2$. Is $$\|ABC - CBA\|_F^2 \le 2\|B\|_2^2\bigl(\sigma_1(A)^2 + \sigma_2(A)^2\bigr)\|C\|_F^2$$ for all $A, C \in \mathbb{C}^{m \times n}$ and $B \in \mathbb{C}^{n \times m}$?
Source: Nobori (2025), Conjecture 3.1.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- FA — Functional Analysis
- Secondary
- NA
- Keywords
- Böttcher–Wenzel inequality, commutators, norm inequalities, OpenProblemsInNLA
References
@article{nobori2025,
author = {Nobori, Motoyuki},
title = {A generalization of the {B}{\"o}ttcher--{W}enzel inequality for three rectangular matrices},
journal = {Linear Algebra Appl.},
volume = {725},
year = {2025},
pages = {135--144},
doi = {10.1016/j.laa.2025.07.005},
eprint = {2506.17365},
archivePrefix = {arXiv},
}
@article{audenaert2010,
author = {Audenaert, Koenraad M. R.},
title = {Variance bounds, with an application to norm bounds for commutators},
journal = {Linear Algebra Appl.},
volume = {432},
number = {5},
year = {2010},
pages = {1126--1143},
doi = {10.1016/j.laa.2009.10.022},
eprint = {0907.3913},
archivePrefix = {arXiv},
}
@article{bottcher2008,
author = {B{\"o}ttcher, Albrecht and Wenzel, David},
title = {The {F}robenius norm and the commutator},
journal = {Linear Algebra Appl.},
volume = {429},
number = {8--9},
year = {2008},
pages = {1864--1885},
doi = {10.1016/j.laa.2008.05.020},
}
@misc{openproblemsinnla-mi13,
author = {Townsend, Alex},
title = {{MI-13}: Nobori's spectral-middle-factor commutator conjecture},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-inequalities-and-norms/MI-13/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00102.
namespace RegistryProblems.OP_00102
noncomputable section
open scoped BigOperators Matrix
abbrev Rect (m n : ℕ) := Matrix (Fin m) (Fin n) ℂ
abbrev EuclideanVector (n : ℕ) := EuclideanSpace ℂ (Fin n)
abbrev EntrySpace (m n : ℕ) := EuclideanSpace ℂ (Fin m × Fin n)
def euclideanLin {m n : ℕ} (A : Rect m n) :
EuclideanVector n →ₗ[ℂ] EuclideanVector m := Matrix.toEuclideanLin A
def euclideanCLM {m n : ℕ} (A : Rect m n) :
EuclideanVector n →L[ℂ] EuclideanVector m :=
(euclideanLin A).toContinuousLinearMap
def spectralNorm {m n : ℕ} (A : Rect m n) : ℝ := ‖euclideanCLM A‖
def flatten {m n : ℕ} (A : Rect m n) : EntrySpace m n :=
WithLp.toLp 2 (fun ij => A ij.1 ij.2)
def frobeniusNorm {m n : ℕ} (A : Rect m n) : ℝ := ‖flatten A‖
/-- Mathlib's actual decreasing, nonnegative, zero-extended singular values. -/
def singularValue {m n : ℕ} (A : Rect m n) (k : ℕ) : ℝ :=
(euclideanLin A).singularValues k
/-- OP-00102: Nobori's spectral-middle-factor commutator conjecture -/
def _root_.RegistryProblems.Problem_OP_00102 : Prop :=
∀ (m n : ℕ), 2 ≤ m → 2 ≤ n → ∀ (A C : Rect m n) (B : Rect n m),
frobeniusNorm (A * B * C - C * B * A) ^ 2 ≤
2 * spectralNorm B ^ 2 * (singularValue A 0 ^ 2 + singularValue A 1 ^ 2) *
frobeniusNorm C ^ 2
end
end RegistryProblems.OP_00102
Formalised by George Stepaniants (Apache-2.0); reviewed by clemens-admin.
Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.
Resolving this problem in Lean
Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.
In lakefile.toml:
[[require]] name = "RegistryProblems" git = "https://github.com/cthalhammer/registry-problems" rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"
In your proof:
import RegistryProblems.OP_00102 theorem resolution : RegistryProblems.Problem_OP_00102 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00102" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00102 := by sorry
You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.
Resolution claims
Let $m,n\ge 2$. For $m\times n$ complex matrices $A$, $C$ and an $n\times m$ matrix $B$, Nobori (Linear Algebra Appl. 725 (2025) 135--144) proposed the following conjecture on the generalized Böttcher-Wenzel inequality: $$ \|ABC-CBA\|_F^2 \le 2\|B\|_2^2\|A\|_{(2),2}^2\|C\|_F^2, $$ where $\|\cdot\|_F$ is the Frobenius norm, $\|\cdot\|_2$ is the spectral norm, and $\|\cdot\|_{(2),2}$ is the $(2,2)$-norm defined by $\|X\|_{(2),2}=\sqrt{σ_1(X)^2+σ_2(X)^2}$, in which $σ_1(X)$ and …
Full complex rectangular MI-13 inequality with coefficient two, actual Euclidean operator and Frobenius norms and the two largest actual singular values. All ranks, both dimension orderings and every m,n at least two are retained.
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MI-13/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00102, "Nobori's spectral-middle-factor commutator conjecture", clopen.solutions.