Sharp additive triangle constant for an odd number of contractions
For $A \in \mathbb{C}^{n \times n}$ let $|A| = (A^*A)^{1/2}$, let $\|\cdot\|_2$ be the operator norm, and write $X \preceq Y$ when $Y - X$ is positive semidefinite. For $k \ge 2$ let $c_k$ be the infimum of the $c \ge 0$ such that $$\Bigl|\sum_{j=1}^k A_j\Bigr| \preceq c\,I_n + \sum_{j=1}^k |A_j|$$ for every $n \ge 1$ and all $A_1, \dots, A_k \in \mathbb{C}^{n \times n}$ with $\|A_j\|_2 \le 1$. The triangle inequality $|A + B| \preceq |A| + |B|$ fails for matrices, and so does $|A + B| \preceq \kappa\,(|A| + |B|)$ for every constant $\kappa$ (Lee). Bourin and Lee proved $c_k \le k/4$ for every $k \ge 2$, with equality for even $k$.
Problem. Is $c_k = k/4$ for every odd integer $k \ge 3$?
Source: Bourin and Lee (2024), the conjecture after Remark 4.5.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- FA — Functional Analysis
- Secondary
- NA
- Keywords
- contractions, OpenProblemsInNLA, triangle inequalities
References
@article{bourin2024,
author = {Bourin, Jean-Christophe and Lee, Eun-Young},
title = {Diagonal and off-diagonal blocks of positive definite partitioned matrices},
journal = {Linear Algebra Appl.},
volume = {684},
year = {2024},
pages = {87--100},
doi = {10.1016/j.laa.2023.12.012},
eprint = {2307.02034},
archivePrefix = {arXiv},
}
@article{lee2012,
author = {Lee, Eun-Young},
title = {How to compare the absolute values of operator sums and the sums of absolute values?},
journal = {Oper. Matrices},
volume = {6},
number = {3},
year = {2012},
pages = {613--619},
doi = {10.7153/oam-06-42},
}
@misc{openproblemsinnla-mi03,
author = {Townsend, Alex},
title = {{MI-03}: Sharp additive triangle constant for an odd number of contractions},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-inequalities-and-norms/MI-03/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00098.
namespace RegistryProblems.OP_00098
noncomputable section
open scoped BigOperators Classical ComplexOrder MatrixOrder
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℂ
/-- The actual principal positive square root of the actual Gram matrix. -/
def matrixModulus {n : ℕ} (A : Mat n) : Mat n :=
CFC.sqrt (A.conjTranspose * A)
/-- The genuine induced Euclidean operator norm, not an entrywise matrix norm. -/
def operatorNorm {n : ℕ} (A : Mat n) : ℝ :=
‖Matrix.toEuclideanCLM (n := Fin n) (𝕜 := ℂ) A‖
def summandSum {n k : ℕ} (A : Fin k → Mat n) : Mat n := ∑ j, A j
def modulusSum {n k : ℕ} (A : Fin k → Mat n) : Mat n :=
∑ j, matrixModulus (A j)
/-- Positivity of this actual difference is the original matrix-order bound. -/
def errorGap {n k : ℕ} (A : Fin k → Mat n) (c : ℝ) : Mat n :=
(c : ℂ) • (1 : Mat n) + modulusSum A - matrixModulus (summandSum A)
/-- Every positive dimension and every complex contraction tuple are retained. -/
def AdmissibleConstant (k : ℕ) (c : ℝ) : Prop :=
0 ≤ c ∧ ∀ n : ℕ, 1 ≤ n → ∀ A : Fin k → Mat n,
(∀ j, operatorNorm (A j) ≤ 1) → (errorGap A c).PosSemidef
def admissibleConstants (k : ℕ) : Set ℝ := {c | AdmissibleConstant k c}
/-- The original infimum. Nonemptiness and a least element are proof obligations. -/
def sharpConstant (k : ℕ) : ℝ := sInf (admissibleConstants k)
/-- OP-00098: Sharp additive triangle constant for an odd number of contractions -/
def _root_.RegistryProblems.Problem_OP_00098 : Prop :=
∀ k : ℕ, 3 ≤ k → Odd k → sharpConstant k = (k : ℝ) / 4
end
end RegistryProblems.OP_00098
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_00098 theorem resolution : RegistryProblems.Problem_OP_00098 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00098" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00098 := 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
We solve a problem posed by Audenaert and Kittaneh in 2012 by proving that the Aujla--Bourin subadditivity inequality can be strengthened to an optimal form. We also answer questions posed by Bourin and the second author: (1) we significantly extend both the reciprocal Lie--Trotter theorem of Audenaert and Hiai and Kato's limit theorem; (2) we determine the best constants in …
Complete proof of the canonical odd-summand conjecture, via the stronger exact least admissible constant k/4 for every k≥2 in every positive dimension.
For complex square contractions $A_1,\ldots,A_k$, with $|X|=(X^*X)^{1/2}$, the least constant $c_k$ such that $\left|\sum_{j=1}^kA_j\right|\le c_kI+\sum_{j=1}^k|A_j|$ holds in every dimension is $c_k=k/4$, for every integer $k\ge2$. For the upper bound, put $R=|\sum_jA_j|$ and $T=\sum_j|A_j|$; the vector Cauchy–Schwarz inequality gives $R^2\le k\sum_j|A_j|^2\le kT$, and then $T+\frac k4I-R\ge\frac1k\left(R-\frac k2I\right)^2\ge0$, without assuming the summands Hermitian. An explicit positive decomposition gives the same bound. Sharpness …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MI-03/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00098, "Sharp additive triangle constant for an odd number of contractions", clopen.solutions.