Entropy and asymptotics / Bound

Alicki-Fannes-Winter continuity bound

Bound statement

For bipartite quantum states $\rho$ and $\sigma$ on a finite-dimensional system $AB$ with $\frac{1}{2}\|\rho - \sigma\|_1 \le \varepsilon \le 1$, the conditional von Neumann entropy satisfies $|H(A \mid B)_\rho - H(A \mid B)_\sigma| \le 2\varepsilon \log |A| + (1+\varepsilon)h\left(\frac{\varepsilon}{1+\varepsilon}\right)$.

Sources

Tight uniform continuity bounds for quantum entropies: conditional entropy, relative entropy distance and energy constraints
Andreas Winter, 2015

Lean context

Import: QIT.Information.AlickiFannesWinter
Lean declaration: QIT.State.alickiFannesWinter_conditionalEntropy

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

Open Lean source