Corrected generalized geometric-mean product conjecture
For positive definite $A, B \in \mathbb{C}^{n \times n}$, real $r$ and $t \in [0, 1]$ let $$G_{r,t}(A, B) = A^{r/2}\bigl(A^{-1/2} B A^{-1/2}\bigr)^t A^{r/2},$$ with real powers by functional calculus. The products below have positive eigenvalues; $\lambda(\cdot)$ lists them in decreasing order, and $\prec_{\log}$ is log-majorization: $x \prec_{\log} y$ if $\prod_{j=1}^k x_j \le \prod_{j=1}^k y_j$ for $1 \le k < n$, with equality for $k = n$. For $p = 1$ the relation below holds for all real $r, s$ (Lemos and Soares). Ghabries, Abbas, Mourad and Assi proved it for $1 \le p \le 2$, $r, s \ge 1$ and $\frac{r(p-1)}{(r+s)p} \le t \le \frac{rp+s}{(r+s)p}$, and proposed it after showing that a conjecture of Lemos and Soares, the case $p = 1$ with singular values in place of eigenvalues, fails for some $r, s$.
Problem. Is $$\lambda\bigl(G_{r,t}(A, B)^p\, G_{s,1-t}(A, B)^p\bigr) \prec_{\log} \lambda\bigl(A^{p(r+s-1)} B^p\bigr)$$ for every $n \ge 1$, all positive definite $A, B \in \mathbb{C}^{n \times n}$, every $p \ge 1$ and $t \in [0, 1]$, and all real $r, s$ with either $r, s \ge 1$ or $r, s \le 0$?
Source: Ghabries, Abbas, Mourad and Assi (2023), Conjecture 2.1 in arXiv:2105.13356.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- FA — Functional Analysis
- Secondary
- NA
- Keywords
- eigenvalues, log-majorization, matrix geometric means, OpenProblemsInNLA
References
@article{ghabries2023,
author = {Ghabries, Mohammad M. and Abbas, Hassane and Mourad, Bassam and Assi, Abdallah},
title = {New log-majorization results concerning eigenvalues and singular values and a complement of a norm inequality},
journal = {Linear Multilinear Algebra},
volume = {71},
number = {7},
year = {2023},
pages = {1228--1243},
doi = {10.1080/03081087.2022.2059050},
eprint = {2105.13356},
archivePrefix = {arXiv},
}
@article{lemos2018,
author = {Lemos, Rute and Soares, Gra{\c{c}}a},
title = {Some log-majorizations and an extension of a determinantal inequality},
journal = {Linear Algebra Appl.},
volume = {547},
year = {2018},
pages = {19--31},
doi = {10.1016/j.laa.2018.02.015},
}
@misc{openproblemsinnla-mi23,
author = {Townsend, Alex},
title = {{MI-23}: Corrected generalized geometric-mean product 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-23/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00106.
namespace RegistryProblems.OP_00106
noncomputable section
open scoped BigOperators Classical ComplexOrder MatrixOrder
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℂ
/-- The genuine continuous-functional-calculus real power. This is not
entrywise exponentiation or a rational proxy for spectral exponentiation. -/
def spectralPower {n : ℕ} (A : Mat n) (r : ℝ) : Mat n := CFC.rpow A r
/-- The generalized geometric mean, retaining the exact noncommuting factor order
and the independent real parameters `r` and `t` from the canonical target. -/
def generalizedMean {n : ℕ} (A B : Mat n) (r t : ℝ) : Mat n :=
spectralPower A (r / 2) *
spectralPower (spectralPower A (-1 / 2) * B * spectralPower A (-1 / 2)) t *
spectralPower A (r / 2)
/-- Actual characteristic-polynomial roots with algebraic multiplicity, mapped
to their real parts and sorted decreasingly. On products of positive definite
matrices the required semantic theorem proves every root is real and positive,
the list has exactly `n` entries, and no root or multiplicity is discarded.
No fallback Hermitian matrix or assumed numerical eigenvalue list is used. -/
def orderedEigenvalues {n : ℕ} (A : Mat n) : List ℝ :=
(A.charpoly.roots.map Complex.re).sort (· ≥ ·)
/-- Log-majorization for equal-length lists: all proper nonempty prefix products
are bounded and the complete products are equal. Positivity and decreasing order
of every list arising in the conjecture are separate proved semantic obligations.
In particular, this is not weak log-majorization or only its first inequality. -/
def LogMajorized (a b : List ℝ) : Prop :=
a.length = b.length ∧
(∀ k : ℕ, 1 ≤ k → k < a.length → (a.take k).prod ≤ (b.take k).prod) ∧
a.prod = b.prod
def leftProduct {n : ℕ} (A B : Mat n) (r s p t : ℝ) : Mat n :=
spectralPower (generalizedMean A B r t) p *
spectralPower (generalizedMean A B s (1 - t)) p
def rightProduct {n : ℕ} (A B : Mat n) (r s p : ℝ) : Mat n :=
spectralPower A (p * (r + s - 1)) * spectralPower B p
/-- OP-00106: Corrected generalized geometric-mean product conjecture -/
def _root_.RegistryProblems.Problem_OP_00106 : Prop :=
∀ n : ℕ, 1 ≤ n → ∀ A B : Mat n, A.PosDef → B.PosDef →
∀ r s p t : ℝ, 1 ≤ p → 0 ≤ t → t ≤ 1 →
((1 ≤ r ∧ 1 ≤ s) ∨ (r ≤ 0 ∧ s ≤ 0)) →
LogMajorized (orderedEigenvalues (leftProduct A B r s p t))
(orderedEigenvalues (rightProduct A B r s p))
end
end RegistryProblems.OP_00106
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_00106 theorem resolution : RegistryProblems.Problem_OP_00106 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00106" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00106 := 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
Formalizes the complete negative answer to the corrected canonical conjecture using complex positive-definite matrices, genuine CFC real powers, full characteristic-root lists and exact log-majorization. Proved spectral and Euclidean norm bridges connect a small exact rational certificate to the original target.
For positive definite matrices let $A\#_{r,t}B=A^{r/2}(A^{-1/2}BA^{-1/2})^tA^{r/2}$. The note disproves the conjectured eigenvalue log-majorization $\lambda((A\#_{r,t}B)^p(A\#_{s,1-t}B)^p)\prec_{\log}\lambda(A^{p(r+s-1)}B^p)$ for $0\le t\le1$, $p\ge1$ and either $r,s\ge1$ or $r,s\le0$. It fails for $r=s=1$, $p=2$ and $t=1/8$, with $A=D^2$ and $B=DT^8D$, where $D=\operatorname{diag}(16,1/12,1)$ and $T$ is an explicit integer positive definite $3\times3$ matrix. Since $A^{-1/2}BA^{-1/2}=T^8$, the two means are exactly $G=DTD$ and $H=DT^7D$, so no fractional power …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MI-23/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00106, "Corrected generalized geometric-mean product conjecture", clopen.solutions.