Hypothesis testing / Theorem

Audenaert positive-operator trace inequality

Theorem statement

For finite-dimensional positive semidefinite operators $A$ and $B$ and any real parameter $s$ with $0\le s\le1$, one has $\operatorname{Tr}(A^sB^{1-s})\ge\frac12\operatorname{Tr}(A+B-|A-B|)$, where $|A-B|$ denotes the operator absolute value.

Sources

  1. The Quantum Chernoff Bound

    K. M. R. Audenaert, J. Calsamiglia, Ll. Masanes, R. Munoz-Tapia, A. Acin, E. Bagan, F. Verstraete, 2006

Lean context

Copy a short prompt with the import, Lean declaration, citations, and public source link.

Open Lean source