One-shot entropy tools / Definition

Smooth min/max entropy characterizations

Definition statement

Let $\rho_{AB} \in \mathcal{S}_{\le}(AB)$ be a subnormalized bipartite state and let $0 \le \varepsilon < \sqrt{\operatorname{Tr}\rho_{AB}}$. Define $\mathcal{B}^\varepsilon(\rho_{AB}) := \{\widetilde\rho_{AB} \in \mathcal{S}_{\le}(AB) : P(\widetilde\rho_{AB},\rho_{AB}) \le \varepsilon\}$. Then $$H_{\min}^{\varepsilon}(A|B)_\rho = \max_{\widetilde\rho_{AB} \in \mathcal{B}^\varepsilon(\rho_{AB})} H_{\min}(A|B)_{\widetilde\rho}, \qquad H_{\max}^{\varepsilon}(A|B)_\rho = \min_{\widetilde\rho_{AB} \in \mathcal{B}^\varepsilon(\rho_{AB})} H_{\max}(A|B)_{\widetilde\rho}.$$

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

Open Lean source