Papers With

← All papers
First page of Weak Log-Majorization for Negative Lim-Pálfia Power Means

Weak Log-Majorization for Negative Lim-Pálfia Power Means

Marco Tomamichel

math.FA Aug 9, 2026 · v1
formalization mathlib analysis
Read PDF arXiv abstract
TL;DR
The main weak log-majorization theorem and its Schatten quasi-norm corollary are formalized in Lean 4 with Mathlib, released as a GitHub/Zenodo artifact.
Abstract
For $0 \le α\le 1$ and $-1 \le r < 0$, let $\#_{r,α}$ denote the weighted Kubo-Ando power mean of order $r$ and weight $α$. Ando proved that, for every unitarily invariant norm, $\| A \ \#_{r,α}\ B \| \le \| A \|\ \#_{r,α}\ \| B \|$. We show that this inequality remains valid also for the Schatten $q$-quasi-norms with $0 < q < 1$. More generally, our main result resolves a problem recently posed by Hiai and Lim in the stronger form of weak log-majorization for multivariable Lim-Pálfia power means of negative order. It yields analogous Schatten quasi-norm inequalities for every finite family of positive definite matrices.
Problem

Ando proved that weighted Kubo-Ando power means of negative order satisfy a norm inequality for every unitarily invariant norm. Hiai and Lim asked whether this extends further for multivariable Lim-Pálfia power means of negative order.

Approach

The authors prove a weak log-majorization result for multivariable Lim-Pálfia power means of negative order. The proofs of the main theorem and its corollary are formalized in Lean 4 using Mathlib and checked by the Lean kernel. An appendix maps manuscript statements to Lean declarations and gives a dependency graph.

Results

The Hiai-Lim problem is resolved in the stronger weak log-majorization form. As a consequence, Schatten q-quasi-norm inequalities with 0<q<1 hold for every finite family of positive definite matrices. The formalization is archived on GitHub/Zenodo.