Modulus-order determinant comparison with an arbitrary base power
For $X \in \mathbb{C}^{n \times n}$ let $|X| = (X^*X)^{1/2}$; real powers of positive definite matrices are taken by functional calculus, with $X^0 = I$. For $k = 2$ the inequality below is a question of Lin, who asked it for positive semidefinite $A$ and $B$, and Ghabries, Abbas and Mourad proved that case for Hermitian $A$ and $B$ and every $p \ge 0$.
Problem. Is $$\det(A^k + |AB|^p) \ge \det(A^k + |BA|^p)$$ for every $n \ge 1$, every positive definite $A \in \mathbb{C}^{n \times n}$, every invertible Hermitian $B \in \mathbb{C}^{n \times n}$ and all real $k, p \ge 0$?
Source: Ghabries (2022), PhD thesis, Open Problems, Problem 2, for positive semidefinite A and Hermitian B, as OpenProblemsInNLA records it; stated for positive definite A and invertible Hermitian B by OpenProblemsInNLA. The case k = 2 is Lin's (2017) question.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- FA — Functional Analysis
- Secondary
- NA
- Keywords
- determinantal inequalities, OpenProblemsInNLA, positive definite matrices
References
@phdthesis{ghabries2022,
author = {Ghabries, Mohammad Mahdi},
title = {Contributions to Matrix Inequalities and Some Applications},
school = {Universit{\'e} d'Angers and Lebanese University},
year = {2022},
doi = {10.70675/32bff73dzcb5az430ezbda8ze209c4b1c319},
note = {HAL tel-03936351},
url = {https://theses.hal.science/tel-03936351},
}
@article{lin2017,
author = {Lin, Minghua},
title = {On a determinantal inequality arising from diffusion tensor imaging},
journal = {Commun. Contemp. Math.},
volume = {19},
number = {5},
year = {2017},
pages = {1650044},
doi = {10.1142/S0219199716500449},
eprint = {1604.04141},
archivePrefix = {arXiv},
}
@article{ghabries2020,
author = {Ghabries, Mohammad M. and Abbas, Hassane and Mourad, Bassam},
title = {On some open questions concerning determinantal inequalities},
journal = {Linear Algebra Appl.},
volume = {596},
year = {2020},
pages = {169--183},
doi = {10.1016/j.laa.2020.03.009},
}
@misc{ghabries2026,
author = {Ghabries, Mohammad M.},
title = {A log-majorization inequality for normal matrices with applications to determinantal inequalities and geometric means},
year = {2026},
eprint = {2607.21163},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-mi29,
author = {Townsend, Alex},
title = {{MI-29}: Modulus-order determinant comparison with an arbitrary base power},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-inequalities-and-norms/MI-29/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00109.
namespace RegistryProblems.OP_00109
noncomputable section
open scoped BigOperators Classical ComplexOrder MatrixOrder
/-- The actual unital continuous-functional-calculus power.
The explicit `CFC.rpow` avoids any pointwise function-power instance on matrices.
For a positive semidefinite matrix, exponent zero gives the identity matrix. -/
def spectralPower {n : ℕ} (A : Matrix (Fin n) (Fin n) ℂ) (r : ℝ) :
Matrix (Fin n) (Fin n) ℂ := CFC.rpow A r
/-- The actual matrix modulus, `CFC.sqrt (Xᴴ * X)`.
Mathlib's `CFC.abs` uses the positive square root from functional calculus. -/
def matrixModulus {n : ℕ} (X : Matrix (Fin n) (Fin n) ℂ) :
Matrix (Fin n) (Fin n) ℂ := CFC.abs X
def leftMatrix {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℂ) (k p : ℝ) :
Matrix (Fin n) (Fin n) ℂ :=
spectralPower A k + spectralPower (matrixModulus (A * B)) p
def rightMatrix {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℂ) (k p : ℝ) :
Matrix (Fin n) (Fin n) ℂ :=
spectralPower A k + spectralPower (matrixModulus (B * A)) p
def leftDet {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℂ) (k p : ℝ) : ℂ :=
(leftMatrix A B k p).det
def rightDet {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℂ) (k p : ℝ) : ℂ :=
(rightMatrix A B k p).det
/-- OP-00109: Modulus-order determinant comparison with an arbitrary base power -/
def _root_.RegistryProblems.Problem_OP_00109 : Prop :=
∀ n : ℕ, 1 ≤ n → ∀ A B : Matrix (Fin n) (Fin n) ℂ,
A.PosDef → B.IsHermitian → IsUnit B →
∀ k p : ℝ, 0 ≤ k → 0 ≤ p → rightDet A B k p ≤ leftDet A B k p
end
end RegistryProblems.OP_00109
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_00109 theorem resolution : RegistryProblems.Problem_OP_00109 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00109" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00109 := 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 genuine continuous-functional-calculus bridges, positive-real determinant semantics, an admissible exact complex-matrix witness, and the negation of the full original conjecture with arbitrary nonnegative real exponents.
The determinant comparison $\det(A^k+|AB|^p)\ge\det(A^k+|BA|^p)$, for positive definite $A$, invertible Hermitian $B$ and $k,p\ge0$, fails for real matrices of order three with $k=6$ and $p=8$. One may take $A=\operatorname{diag}(2,1,1/2)$ and $B=\frac15\begin{pmatrix}-1&2&0\\2&1&2\\0&2&1\end{pmatrix}$, which is symmetric with $\det B=-1/125$. Since $|AB|^2=BA^2B$ and $|BA|^2=AB^2A$, both sides are determinants of $A^6+5^{-8}K$ with $K=(MA^2M)^4$ or $(AM^2A)^4$, $M=5B$. Expanding $\det(D+zK)$ by multilinearity in dimension three gives an …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MI-29/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00109, "Modulus-order determinant comparison with an arbitrary base power", clopen.solutions.