A universal block-norm characterization of essentially Hermitian matrices
Let $\|\cdot\|_2$ be the operator norm, and for $A, B, X \in \mathbb{C}^{n \times n}$ let $$H = \begin{bmatrix} A & X \\ X^* & B \end{bmatrix}.$$ A matrix $X$ is essentially Hermitian if $X = \alpha K + \beta I_n$ for a Hermitian $K$ and scalars $\alpha, \beta \in \mathbb{C}$; equivalently, its numerical range lies in a line. If $X$ is essentially Hermitian, then $\|H\| \le \|A + B\|$ for every positive semidefinite $H$ and every unitarily invariant norm (Mhanna). Conversely, Hayashi showed that an invertible $X$ with $n$ distinct singular values such that $\|H\|_2 \le \|A + B\|_2$ for every positive semidefinite $H$ is normal, and with the Frobenius norm in place of $\|\cdot\|_2$ that property characterises the normal $X$ (Bourin and Lee).
Problem. Let $n \ge 1$ and $X \in \mathbb{C}^{n \times n}$, and suppose that $\|H\|_2 \le \|A + B\|_2$ for every pair of Hermitian $A, B \in \mathbb{C}^{n \times n}$ for which $H$ is positive semidefinite. Must $X$ be essentially Hermitian?
Source: Bourin and Lee (2022), Conjecture 3.3 in arXiv:2111.15180.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- FA — Functional Analysis
- Secondary
- NA
- Keywords
- block matrices, numerical ranges, OpenProblemsInNLA
References
@article{bourin2022,
author = {Bourin, Jean-Christophe and Lee, Eun-Young},
title = {Eigenvalue inequalities for positive block matrices with the inradius of the numerical range},
journal = {Internat. J. Math.},
volume = {33},
number = {1},
year = {2022},
pages = {2250009},
doi = {10.1142/S0129167X22500094},
eprint = {2111.15180},
archivePrefix = {arXiv},
}
@article{mhanna2018,
author = {Mhanna, Antoine},
title = {On symmetric norm inequalities and positive definite block-matrices},
journal = {Math. Inequal. Appl.},
volume = {21},
number = {1},
year = {2018},
pages = {133--138},
doi = {10.7153/mia-2018-21-11},
}
@article{hayashi2019,
author = {Hayashi, Tomohiro},
title = {On a norm inequality for a positive block-matrix},
journal = {Linear Algebra Appl.},
volume = {566},
year = {2019},
pages = {86--97},
doi = {10.1016/j.laa.2018.12.027},
eprint = {1808.00181},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-mi04,
author = {Townsend, Alex},
title = {{MI-04}: A universal block-norm characterization of essentially Hermitian matrices},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-inequalities-and-norms/MI-04/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00099.
namespace RegistryProblems.OP_00099
noncomputable section
open scoped BigOperators ComplexOrder
abbrev CMatrix (ι : Type*) := Matrix ι ι ℂ
abbrev Square (n : ℕ) := CMatrix (Fin n)
section
variable {ι : Type*} [Fintype ι] [DecidableEq ι]
/-- The actual complex Euclidean operator norm, never the default Pi matrix norm. -/
def spectralNorm (M : CMatrix ι) : ℝ :=
‖Matrix.toEuclideanCLM (n := ι) (𝕜 := ℂ) M‖
end
/-- OP-00099: A universal block-norm characterization of essentially Hermitian matrices -/
def _root_.RegistryProblems.Problem_OP_00099 : Prop :=
∀ (n : ℕ), 1 ≤ n → ∀ (X : Square n),
(∀ A B : Square n, A.IsHermitian → B.IsHermitian →
(Matrix.fromBlocks A X X.conjTranspose B).PosSemidef →
spectralNorm (Matrix.fromBlocks A X X.conjTranspose B) ≤ spectralNorm (A + B)) →
∃ K : Square n, K.IsHermitian ∧ ∃ α β : ℂ,
X = α • K + β • (1 : Square n)
end
end RegistryProblems.OP_00099
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_00099 theorem resolution : RegistryProblems.Problem_OP_00099 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00099" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00099 := 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
Complete Lean verification of the full original MI-04 necessity implication. All21 exports passed actual canonical Linux default-kernel, Comparator, axiom and control checks at the immutable proof revision.
For $X\in\mathbb{C}^{n\times n}$ the following are equivalent: (1) $\|P\|\le\|A+B\|$ in the operator norm for every positive semidefinite completion $P=\begin{pmatrix}A&X\\X^*&B\end{pmatrix}$; (2) the same holds whenever $A+B$ is a scalar multiple of $I$; (3) for every Hermitian $T$ the largest and smallest eigenvalues of $\begin{pmatrix}T&X\\X^*&-T\end{pmatrix}$ are negatives of each other; (4) $X=\alpha H+\beta I$ with $H$ Hermitian and $\alpha,\beta\in\mathbb{C}$. No invertibility or …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MI-04/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00099, "A universal block-norm characterization of essentially Hermitian matrices", clopen.solutions.