Metadata
slug: gan-kim-2024-wasserstein-weak-log-majorization
bibkey: gankim2024wasserstein
doi: 10.48550/arXiv.2301.07934
url: https://arxiv.org/abs/2301.07934
triage: theorem
motivation_gids:
- D5/S3/Quantum/Matrix/GanKimConjectureRefutation.result
Gan–Kim: weak log-majorization monotonicity of Wasserstein power means
Problem
Luyining Gan and Sejong Kim, Weak log-majorization between the geometric and Wasserstein means, arXiv:2301.07934v4, §5, Conjecture 5.7. See gankim2024wasserstein.
Conjecture 5.7. Let A, B ∈ Pm and t ∈ (0, 1). Then (A^p ⋄t B^p)^{1/p} ց≺w log exp((1 − t) log A + t log B) as p ց 0.
A ⋄t B := (1 − t)² A + t² B + t(1 − t)[A(A^{−1} #B) + (A^{−1} #B)A]
Here and is the cone of complex Hermitian positive definite matrices. Weak log-majorization compares every initial product of decreasingly sorted eigenvalues, including the product of all eigenvalues.
For , the decreasing arrow is the conjunction of the comparisons for all real and the right-hand limit as . The formal statement includes both assertions, every finite dimension, all complex positive definite inputs and every real .
Motivation
The conjecture removes the extra hypothesis (5.15) from the paper’s Theorem 5.6 and proposes an unconditional power-parameter monotonicity law for the Wasserstein mean. The assertion and proposed counterexample are identified in issue #19050.
Gap
The full eigenvalue product can increase when the power parameter decreases. Equal spectra of the two input matrices do not prevent this determinant obstruction.
Route
Take
Then , , and the positive definite solutions of and are
Riccati uniqueness identifies them with the required inverse geometric means. With , and , the determinant identities are
Exact squared comparisons give and . For , , so
Squaring the positive sides proves .
Falsifier
The same two positive definite integer matrices violate the conjectured comparison at and for every . The determinant is the product at the full prefix , so a strict reverse determinant inequality refutes weak log-majorization itself.
Evidence
D5/S3/Quantum/Matrix/GanKimConjectureRefutation.result : ¬ conjecture targets the full quantified conjecture, including its limit conjunct. The certificate belongs to that module. D5/S3/Quantum/Matrix/WassersteinMean.weakLogMajorization_det_le supplies the implication from the eigenvalue-product comparison to the determinant inequality. The counterexample refutes the monotonicity conjunct; the proof does not use a failure of the limit conjunct.
Triage
PROVED — Refutation of Conjecture 5.7, for every . For and , the comparison from to fails at the product of both eigenvalues.
OPEN — formal non-implication for Theorem 5.6 under (5.15). The unconditional conjecture and the conditional theorem are distinct assertions. Direct violation of the literal hypothesis (5.15) by these matrices is ASSUMED-UNVERIFIED here: its primary-source text is unavailable locally, and no Lean theorem about that condition is asserted.
OPEN — convergence without monotonicity. The determinant counterexample does not decide the limit of as . No global claim that this convergence is unresolved in the literature is made.
ASSUMED-UNVERIFIED
The exact condition (5.15), its failure for the displayed pair, and the journal DOI have not been confirmed against primary text. Absence of subsequent settlements and worldwide priority are not established. Convergence alone is not proved or refuted by this module.