One-shot entropy tools / Theorem

Smooth min/max entropy duality

Theorem statement

Let $\rho_{ABC}$ be a pure subnormalized state and let $0 \le \varepsilon < \sqrt{\operatorname{Tr}\rho}$. Then $H_{\max}^{\varepsilon}(A|B)_{\rho} = -H_{\min}^{\varepsilon}(A|C)_{\rho}$.

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

Open Lean source