Concave unitary-orbit subadditivity without monotonicity
For a Hermitian matrix $A$ and a function $f$ on its spectrum, $f(A)$ is defined by the spectral decomposition, and $X \preceq Y$ means that $Y - X$ is positive semidefinite. Aujla and Bourin proved that for every monotone concave function $f$ on $[0, \infty)$ with $f(0) \ge 0$ and all positive semidefinite $A, B$ there are unitaries $U, V$ with $$f(A + B) \preceq U f(A) U^* + V f(B) V^*.$$
Problem. For every $n \ge 1$, all positive semidefinite $A, B \in \mathbb{C}^{n \times n}$ and every concave $f : [0, \infty) \to \mathbb{R}$ with $f(0) \ge 0$, not assumed monotone or nonnegative, are there unitary $U, V \in \mathbb{C}^{n \times n}$ such that $f(A + B) \preceq U f(A) U^* + V f(B) V^*$?
Source: Bourin and Lee (2012), Remark 3.13; restated by Audenaert and Kittaneh (arXiv:1201.5232v3, 2012), Problem 5, and by Bourin, Harada and Lee (2014), Question 1.3.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- FA — Functional Analysis
- Secondary
- NA
- Keywords
- concave functions, matrix subadditivity, OpenProblemsInNLA, unitary orbits
References
@article{bourin2012,
author = {Bourin, Jean-Christophe and Lee, Eun-Young},
title = {Unitary orbits of {H}ermitian operators with convex or concave functions},
journal = {Bull. Lond. Math. Soc.},
volume = {44},
number = {6},
year = {2012},
pages = {1085--1102},
doi = {10.1112/blms/bds080},
eprint = {1109.2384},
archivePrefix = {arXiv},
}
@article{audenaert2017,
author = {Audenaert, Koenraad M. R. and Kittaneh, Fuad},
title = {Problems and conjectures in matrix and operator inequalities},
journal = {Banach Center Publ.},
volume = {112},
year = {2017},
pages = {15--31},
doi = {10.4064/bc112-0-2},
eprint = {1201.5232},
archivePrefix = {arXiv},
}
@article{bourin2014,
author = {Bourin, Jean-Christophe and Harada, Tetsuo and Lee, Eun-Young},
title = {Subadditivity inequalities for compact operators},
journal = {Canad. Math. Bull.},
volume = {57},
number = {1},
year = {2014},
pages = {25--36},
doi = {10.4153/CMB-2012-009-9},
}
@article{aujla2007,
author = {Aujla, Jaspal Singh and Bourin, Jean-Christophe},
title = {Eigenvalue inequalities for convex and log-convex functions},
journal = {Linear Algebra Appl.},
volume = {424},
number = {1},
year = {2007},
pages = {25--35},
doi = {10.1016/j.laa.2006.02.027},
}
@misc{openproblemsinnla-mi26,
author = {Townsend, Alex},
title = {{MI-26}: Concave unitary-orbit subadditivity without monotonicity},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-inequalities-and-norms/MI-26/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00107.
namespace RegistryProblems.OP_00107
noncomputable section
open scoped BigOperators Classical ComplexOrder MatrixOrder
/-- Exactly the canonical real-valued concave function class on the nonnegative
half-line. Values at negative arguments are unrestricted and are irrelevant for
positive semidefinite inputs. No continuity, monotonicity, or global
nonnegativity assumption is added. -/
def AdmissibleFunction (f : ℝ → ℝ) : Prop :=
ConcaveOn ℝ (Set.Ici 0) f ∧ 0 ≤ f 0
/-- Genuine real continuous functional calculus in the complex matrix algebra.
Every function is continuous on a Hermitian matrix's finite spectrum, even
when it is not continuous at an endpoint of the entire half-line. -/
def functionalCalculus {n : ℕ} (f : ℝ → ℝ)
(A : Matrix (Fin n) (Fin n) ℂ) : Matrix (Fin n) (Fin n) ℂ :=
cfc (R := ℝ) f A
/-- Conjugation by an arbitrary complex unitary, with its actual conjugate transpose. -/
def unitaryConjugate {n : ℕ} (U : Matrix.unitaryGroup (Fin n) ℂ)
(H : Matrix (Fin n) (Fin n) ℂ) : Matrix (Fin n) (Fin n) ℂ :=
(U : Matrix (Fin n) (Fin n) ℂ) * H *
(U : Matrix (Fin n) (Fin n) ℂ).conjTranspose
/-- OP-00107: Concave unitary-orbit subadditivity without monotonicity -/
def _root_.RegistryProblems.Problem_OP_00107 : Prop :=
∀ n : ℕ, 1 ≤ n → ∀ A B : Matrix (Fin n) (Fin n) ℂ,
A.PosSemidef → B.PosSemidef → ∀ f : ℝ → ℝ, AdmissibleFunction f →
∃ U V : Matrix.unitaryGroup (Fin n) ℂ,
functionalCalculus f (A + B) ≤
unitaryConjugate U (functionalCalculus f A) +
unitaryConjugate V (functionalCalculus f B)
end
end RegistryProblems.OP_00107
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_00107 theorem resolution : RegistryProblems.Problem_OP_00107 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00107" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00107 := 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
Proves the original function-class equivalence, genuine finite-spectrum CFC and half-line extension bridges, exact polynomial identities for two rational projections, their positive quadratic-form obstruction, and the full negation of the universal complex PSD unitary-orbit assertion.
The question is whether, for every real-valued concave function $f$ on $[0,\infty)$ with $f(0)\ge0$, not assumed monotone, and all positive semidefinite $A,B$, there are unitaries $U,V$ with $f(A+B)\le Uf(A)U^*+Vf(B)V^*$. The note shows that this fails in dimension two. For $f(t)=t-t^2$, let $P=\operatorname{diag}(1,0)$ and let $Q$ be the orthogonal projection onto the line spanned by $(3,4)^T$. Then $f(P)=f(Q)=0$, while $f(P+Q)=-(PQ+QP)$ has …
50 years after Thompson's famous triangle inequality for the operator right modulus, we establish a triangle inequality for the quadratic symmetric modulus. We also discuss the corresponding equality cases as well as the infinite-dimensional setting. In addition, we obtain Clarkson--McCarthy type inequalities for the quadratic symmetric modulus. Moreover, we answer several questions raised by Bourin and Lee in [\emph{Bull. Lond. …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MI-26/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00107, "Concave unitary-orbit subadditivity without monotonicity", clopen.solutions.