Entropy and asymptotics / Theorem

Sandwiched Renyi relative entropy data-processing inequality

Theorem statement

Let $\rho$ be a quantum state, $\sigma$ a positive semidefinite operator, and $\mathcal{N}$ a quantum channel. For $\frac{1}{2} \le \alpha < 1$ or $\alpha > 1$, the sandwiched Renyi relative entropy satisfies $\widetilde{D}_\alpha(\rho \| \sigma) \ge \widetilde{D}_\alpha(\mathcal{N}(\rho) \| \mathcal{N}(\sigma))$.

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

Open Lean source