Lemos–Soares singular-value log-majorization
For positive definite $A, B$ and $t \in [0, 1]$ let $A \#_t B = A^{1/2}(A^{-1/2} B A^{-1/2})^t A^{1/2}$, with real powers by functional calculus. Let $s(X) = (s_1(X), \dots, s_n(X))$ be the singular values of $X \in \mathbb{C}^{n \times n}$ in decreasing order, and let $\prec_{\log}$ be 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$. The relation below holds for $t = 1/2$ (Zou), and Lemos and Soares asked for a generalisation of that case; with eigenvalues in place of singular values it holds for every $t \in [0, 1]$ (Ghabries, Abbas, Mourad and Assi).
Problem. Is $s\bigl(A^t (A \#_t B) B^{1-t}\bigr) \prec_{\log} s(AB)$ for every $n \ge 1$, all positive definite $A, B \in \mathbb{C}^{n \times n}$ and every $t \in [0, 1]$?
Source: Ghabries, Abbas, Mourad and Assi (2023), Conjecture 1.1 in arXiv:2105.13356, formulating a question of Lemos and Soares (2018).
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- FA — Functional Analysis
- Secondary
- NA
- Keywords
- log-majorization, matrix geometric means, OpenProblemsInNLA, singular values
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},
}
@article{zou2017,
author = {Zou, Limin},
title = {An arithmetic--geometric mean inequality for singular values and its applications},
journal = {Linear Algebra Appl.},
volume = {528},
year = {2017},
pages = {25--32},
doi = {10.1016/j.laa.2016.01.016},
}
@misc{openproblemsinnla-mi22,
author = {Townsend, Alex},
title = {{MI-22}: Lemos–Soares singular-value log-majorization},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-inequalities-and-norms/MI-22/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00105.
namespace RegistryProblems.OP_00105
noncomputable section
open scoped BigOperators Classical ComplexOrder MatrixOrder
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℂ
/-- The genuine real power from continuous functional calculus. It is never
replaced by entrywise powers or an assumed rational matrix certificate. -/
def spectralPower {n : ℕ} (A : Mat n) (t : ℝ) : Mat n := CFC.rpow A t
/-- The exact weighted mean, with the original noncommuting order of factors. -/
def weightedMean {n : ℕ} (A B : Mat n) (t : ℝ) : Mat n :=
spectralPower A (1 / 2) *
spectralPower (spectralPower A (-1 / 2) * B * spectralPower A (-1 / 2)) t *
spectralPower A (1 / 2)
def leftProduct {n : ℕ} (A B : Mat n) (t : ℝ) : Mat n :=
spectralPower A t * weightedMean A B t * spectralPower B (1 - t)
/-- Mathlib's actual singular values of the linear map on complex Euclidean
space: descending, repeated with multiplicity, and zero beyond dimension n.
The index zero is the first singular value. No user-supplied list is involved. -/
def singularValue {n : ℕ} (A : Mat n) (j : ℕ) : ℝ :=
(Matrix.toEuclideanLin A).singularValues j
/-- The first k actual singular values, with the original one-based range
1,...,k represented as the zero-based range 0,...,k-1. -/
def singularPrefix {n : ℕ} (A : Mat n) (k : ℕ) : ℝ :=
∏ j ∈ Finset.range k, singularValue A j
/-- Full log-majorization, including equality at n rather than weak
log-majorization. Both matrices have the same actual dimension n. -/
def SingularLogMajorized {n : ℕ} (X Y : Mat n) : Prop :=
(∀ k : ℕ, 1 ≤ k → k < n → singularPrefix X k ≤ singularPrefix Y k) ∧
singularPrefix X n = singularPrefix Y n
/-- OP-00105: Lemos–Soares singular-value log-majorization -/
def _root_.RegistryProblems.Problem_OP_00105 : Prop :=
∀ n : ℕ, 1 ≤ n → ∀ A B : Mat n, A.PosDef → B.PosDef →
∀ t : ℝ, 0 ≤ t → t ≤ 1 → SingularLogMajorized (leftProduct A B t) (A * B)
end
end RegistryProblems.OP_00105
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_00105 theorem resolution : RegistryProblems.Problem_OP_00105 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00105" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00105 := 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 negative resolution of the canonical complex positive-definite weighted singular-value log-majorization statement, using an exact rational adaptation and proved genuine CFC, singular-value and Euclidean-norm semantics.
For positive definite $A,B$ and $0\le t\le1$, the conjecture asserts the log-majorization $s(A^t(A\#_tB)B^{1-t})\prec_{\log}s(AB)$ of singular values, where $\#_t$ is the weighted geometric mean. The note disproves even the largest-singular-value inequality: for $A=\operatorname{diag}(256,1/256,1)$, an explicit integer positive definite $3\times3$ matrix $B$ and $t=1/8$, the operator norm of $A^{1/8}(A\#_{1/8}B)B^{7/8}$ exceeds $10900$, while $\|AB\|_2<10200$. The proof replaces the eighth roots of $A^{-1/2}BA^{-1/2}$ and …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MI-22/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00105, "Lemos–Soares singular-value log-majorization", clopen.solutions.