Constant one in the logarithmic commutator inequality
For positive definite $A, B \in \mathbb{C}^{n \times n}$ with $\operatorname{tr}(A + B) = 1$, let $a = \operatorname{tr} A$ and $b = \operatorname{tr} B$, so that $a, b > 0$ and $a + b = 1$. Here $\log$ is the natural logarithm, applied to $A + B$ by functional calculus, and $\|\cdot\|_1$ is the trace norm. Bravyi's small incremental mixing conjecture, in Audenaert and Kittaneh's trace-norm form, asks for the inequality below with its right-hand side multiplied by some constant independent of $n$. Audenaert and Kittaneh note that numerical work indicates the constant might be $1$, and Audenaert's proof of the small incremental mixing conjecture gives the inequality with the constant $2$.
Problem. Is $$\|B \log(A + B) - \log(A + B) B\|_1 \le -a \log a - b \log b$$ for every $n \ge 1$ and all such $A$ and $B$?
Source: Audenaert and Kittaneh (2017), Conjecture 4, and the remark after it that the constant might be 1; with an unspecified constant, Bravyi's (2007) small incremental mixing conjecture.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- FA — Functional Analysis
- Secondary
- MP, NA
- Keywords
- commutators, matrix logarithms, OpenProblemsInNLA
References
@article{audenaert2017,
author = {Audenaert, Koenraad M. R. and Kittaneh, Fuad},
title = {Problems and conjectures in matrix and operator inequalities},
journal = {Banach Center Publ.},
volume = {112},
year = {2017},
pages = {15--31},
doi = {10.4064/bc112-0-2},
eprint = {1201.5232},
archivePrefix = {arXiv},
}
@article{bravyi2007,
author = {Bravyi, Sergey},
title = {Upper bounds on entangling rates of bipartite {H}amiltonians},
journal = {Phys. Rev. A},
volume = {76},
number = {5},
year = {2007},
pages = {052319},
doi = {10.1103/PhysRevA.76.052319},
eprint = {0704.0964},
archivePrefix = {arXiv},
}
@article{audenaert2014,
author = {Audenaert, Koenraad M. R.},
title = {Quantum skew divergence},
journal = {J. Math. Phys.},
volume = {55},
number = {11},
year = {2014},
pages = {112202},
doi = {10.1063/1.4901039},
eprint = {1304.5935},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-mi27,
author = {Townsend, Alex},
title = {{MI-27}: Constant one in the logarithmic commutator inequality},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-inequalities-and-norms/MI-27/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00108.
namespace RegistryProblems.OP_00108
noncomputable section
open scoped BigOperators Classical ComplexOrder MatrixOrder Matrix Matrix.Norms.L2Operator
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℂ
/-- Real part of the actual complex matrix trace, including for non-Hermitian products. -/
def trR {n : ℕ} (X : Mat n) : ℝ := (Matrix.trace X).re
/-- Natural spectral logarithm. Final entropy/logarithm applications are on PD matrices. -/
def logM {n : ℕ} (X : Mat n) : Mat n := CFC.log X
/-- The original full trace norm: trace of the positive square root of the Gram matrix. -/
def traceNorm {n : ℕ} (X : Mat n) : ℝ :=
trR (CFC.rpow (Xᴴ * X) (1 / 2 : ℝ))
/-- OP-00108: Constant one in the logarithmic commutator inequality -/
def _root_.RegistryProblems.Problem_OP_00108 : Prop :=
∀ (n : ℕ), 1 ≤ n → ∀ (A B : Mat n), A.PosDef → B.PosDef → Matrix.trace (A + B) = 1 →
traceNorm (B * logM (A + B) - logM (A + B) * B) ≤
-(trR A) * Real.log (trR A) - (trR B) * Real.log (trR B)
end
end RegistryProblems.OP_00108
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_00108 theorem resolution : RegistryProblems.Problem_OP_00108 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00108" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00108 := 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
Full original coefficient-one bound for every complex positive definite pair of trace sum one in every positive dimension. All twenty frozen contracts pass local Lean and actual source-matched non-root Linux Comparator/default-kernel verification; two independent nonauthor final reviews pass.
For every pair of positive definite complex matrices $A,B$ with $\operatorname{tr}(A+B)=1$, we prove $$\|[B,\log(A+B)]\|_1\le-\operatorname{tr}(A)\log\operatorname{tr}(A)-\operatorname{tr}(B)\log\operatorname{tr}(B).$$ The proof uses Frenkel's integral representation of quantum relative entropy, in its positive-part form given by Hirche and Tomamichel. The key estimate is that $\operatorname{tr}(\rho-\gamma e^{itH}\sigma e^{-itH})_+$ is $\|H\|_\infty$-Lipschitz in $t$, uniformly for $\gamma\ge1$ and for all matrix sizes. A positive integral of these estimates has …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MI-27/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00108, "Constant one in the logarithmic commutator inequality", clopen.solutions.