Classical capacity / Theorem
Hayashi-Nagaoka operator inequality (c = 1)
Theorem statement
Let $A$ and $B$ be positive semidefinite operators with $A \le 1$. The Hayashi-Nagaoka operator inequality (parameter 1) gives $1 - (A+B)^{-1/2}\, A\, (A+B)^{-1/2} \;\le\; 2\,(1 - A) + 4\,B$.
Sources
- From Classical to Quantum Shannon Theory
Mark M. Wilde, 2011
Lean context
- Lean declaration
QIT.hayashi_nagaoka_one
Copy a short prompt with the import, Lean declaration, citations, and public source link.