Freewan–Hayajneh inequality for sums of weighted geometric means
For positive definite $A, B$ and $t \in [0, 1]$ let $$A \#_t B = A^{1/2}\bigl(A^{-1/2} B A^{-1/2}\bigr)^t A^{1/2}$$ be the weighted geometric mean; real powers of positive definite matrices are defined by functional calculus. The case $s = 2$, $t = 1/2$, $r = p = 1$ of the inequality below is a conjecture of Dinh, Ahsani and Tam, and Freewan and Hayajneh showed the case $t = 1/2$, $s \ge 2$, $r \ge 1$, $rp \ge 1$.
Problem. Is $$\Bigl\|\sum_{i=1}^m \bigl(A_i^s \#_t B_i^s\bigr)^r\Bigr\| \le \Bigl\|\bigl(A^{(1-t)srp/2}\, B^{tsrp}\, A^{(1-t)srp/2}\bigr)^{1/p}\Bigr\|, \qquad A = \sum_{i=1}^m A_i,\quad B = \sum_{i=1}^m B_i,$$ for all integers $m, n \ge 1$, all positive definite $A_1, \dots, A_m, B_1, \dots, B_m \in \mathbb{C}^{n \times n}$, every $t \in [0, 1]$, all real $s, r, p > 0$ with $sr \ge 1$, and every unitarily invariant norm $\|\cdot\|$ on $\mathbb{C}^{n \times n}$?
Source: Freewan and Hayajneh (2024), Conjecture 3.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- FA — Functional Analysis
- Secondary
- NA
- Keywords
- matrix geometric means, OpenProblemsInNLA, unitarily invariant norms
References
@article{freewan2024,
author = {Freewan, Shaima'a and Hayajneh, Mostafa},
title = {On a conjecture related to the geometric mean and norm inequalities},
journal = {Math. Inequal. Appl.},
volume = {27},
number = {1},
year = {2024},
pages = {193--200},
doi = {10.7153/mia-2024-27-15},
}
@misc{freewan2023,
author = {Freewan, Shaima'a and Hayajneh, Mostafa},
title = {Norm inequalities involving geometric means},
year = {2023},
eprint = {2401.00337},
archivePrefix = {arXiv},
}
@article{dinh2016,
author = {Dinh, Trung Hoa and Ahsani, Sima and Tam, Tin-Yau},
title = {Geometry and inequalities of geometric mean},
journal = {Czechoslovak Math. J.},
volume = {66},
number = {3},
year = {2016},
pages = {777--792},
doi = {10.1007/s10587-016-0292-8},
}
@misc{openproblemsinnla-mi21,
author = {Townsend, Alex},
title = {{MI-21}: Freewan–Hayajneh inequality for sums of weighted geometric means},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-inequalities-and-norms/MI-21/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00104.
namespace RegistryProblems.OP_00104
noncomputable section
open scoped BigOperators Classical ComplexOrder MatrixOrder
open Matrix
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℂ
/-- Real powers from the actual continuous functional calculus. On the positive
definite inputs of the conjecture this is spectral matrix exponentiation. -/
def spectralPower {n : ℕ} (A : Mat n) (r : ℝ) : Mat n := CFC.rpow A r
/-- The weighted geometric mean in the exact order written in the canonical target.
The exponents `1/2`, `-1/2` and `t` are real spectral powers. -/
def geometricMean {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)
/-- A complex norm on the full matrix vector space, with independent left and
right unitary invariance. These are the usual norm axioms, not an operator-norm
restriction. Both unitary inverse identities are stated explicitly. -/
def IsUnitaryInvariantNorm {n : ℕ} (ν : Mat n → ℝ) : Prop :=
(∀ X, 0 ≤ ν X) ∧
(∀ X, ν X = 0 ↔ X = 0) ∧
(∀ X Y, ν (X + Y) ≤ ν X + ν Y) ∧
(∀ (z : ℂ) X, ν (z • X) = ‖z‖ * ν X) ∧
(∀ U V X : Mat n, Uᴴ * U = 1 → U * Uᴴ = 1 →
Vᴴ * V = 1 → V * Vᴴ = 1 → ν (U * X * V) = ν X)
/-- The sum of the powered weighted means on the left of MI-21. -/
def leftMatrix {m n : ℕ} (A B : Fin m → Mat n) (s t r : ℝ) : Mat n :=
∑ i, spectralPower (geometricMean (spectralPower (A i) s)
(spectralPower (B i) s) t) r
/-- The right side uses the actual aggregate sums and the original order of
the three noncommuting factors before its final real power. -/
def rightMatrix {m n : ℕ} (A B : Fin m → Mat n) (s t r p : ℝ) : Mat n :=
spectralPower
(spectralPower (∑ i, A i) ((1 - t) * s * r * p / 2) *
spectralPower (∑ i, B i) (t * s * r * p) *
spectralPower (∑ i, A i) ((1 - t) * s * r * p / 2)) (1 / p)
/-- OP-00104: Freewan–Hayajneh inequality for sums of weighted geometric means -/
def _root_.RegistryProblems.Problem_OP_00104 : Prop :=
∀ m n : ℕ, 1 ≤ m → 1 ≤ n → ∀ A B : Fin m → Mat n,
(∀ i, (A i).PosDef) → (∀ i, (B i).PosDef) →
∀ t s r p : ℝ, 0 ≤ t → t ≤ 1 → 0 < s → 0 < r → 0 < p → 1 ≤ s * r →
∀ ν : Mat n → ℝ, IsUnitaryInvariantNorm ν →
ν (leftMatrix A B s t r) ≤ ν (rightMatrix A B s t r p)
end
end RegistryProblems.OP_00104
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_00104 theorem resolution : RegistryProblems.Problem_OP_00104 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00104" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00104 := 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 admissibility of the genuine Euclidean operator norm, exact CFC geometric-mean identities at positive definite complex matrices, a strict counterexample for every positive outer parameter, and the full original universal conjecture's negation.
For positive definite matrices let $A\#_tB=A^{1/2}(A^{-1/2}BA^{-1/2})^tA^{1/2}$. The note disproves the norm inequality $\|\sum_i(A_i^s\#_tB_i^s)^r\|\le\|(A^{(1-t)srp/2}B^{tsrp}A^{(1-t)srp/2})^{1/p}\|$, with $A=\sum_iA_i$ and $B=\sum_iB_i$, conjectured for every unitarily invariant norm, $0\le t\le1$ and $p,r,s>0$ with $sr\ge1$. It fails for two rational positive definite $2\times2$ summands, the operator norm, $s=t=1/2$ and $r=2$, for every $p>0$. The inputs are $A_1=C^2$, $A_2=E^2$, $B_1=SE^2S$ and $B_2=SC^2S$, with diagonal $C,E>0$ satisfying $C^2+E^2=I_2$ …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MI-21/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00104, "Freewan–Hayajneh inequality for sums of weighted geometric means", clopen.solutions.