Quantum Pinsker inequality in bits

Open

QAlgorithms.Papers.Independent.Intakethird100.P81.quantum_pinsker

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $\rho$ and $\sigma$ be normalized density matrices on the same finite-dimensional complex Hilbert space. Write $S_2(\rho\Vert\sigma)$ for Umegaki relative entropy with binary logarithms, taking value $+\infty$ when the support of $\rho$ is not contained in the support of $\sigma$ . Let $\|M\|_1=\operatorname{Tr}\sqrt{M^\dagger M}$ be the full trace norm. Then

S_2(\rho\Vert\sigma)\ge\frac{\|\rho-\sigma\|_1^2}{2\ln 2}.

This bounds statistical distinguishability by relative entropy. Singular density matrices are included; no positive-definiteness assumption is imposed.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P81

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ENNReal

attribute [local instance] Classical.propDecidable

namespace QAlgorithms.Papers.Independent.Intakethird100.P81

open QAlgorithms.Papers.Independent.Information100.P54 (relativeEntropyBits)

open QAlgorithms.Papers.Independent.Bridge50.P44 (ClassicalFirst)

/-- Theorem 1, PDF p.9 (proof pp.9–11): quantum Pinsker with base-two entropy,
including singular states and support violations. -/
theorem quantum_pinsker {I : Type*} [Fintype I] [DecidableEq I]
    (rho sigma : Matrix I I ℂ) (hrho : IsDensityMatrix rho)
    (hsigma : IsDensityMatrix sigma) :
    ENNReal.ofReal ((traceNorm (rho - sigma)) ^ 2 / (2 * Real.log 2)) ≤
      relativeEntropyBits rho sigma := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P81

end

Source

On rounds in quantum communication, arXiv:quant-ph/0004100v5, PDF p. 9, Theorem 1

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every finite type $I$ with decidable equality and every pair of positive semidefinite complex matrices $\rho,\sigma$ on $I$ , each having trace $1$ , define $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , using continuous functional calculus for the square root. Let $[r]_+=\max(r,0)$ , regarded as an extended nonnegative real, and define

D_{\mathrm{bits}}(\rho\|\sigma)= \begin{cases} \displaystyle \frac{\left[\operatorname{Re}\operatorname{tr}\bigl((x\mapsto x\ln x)[\rho]-\rho\,(\ln)[\sigma]\bigr)\right]_+}{\ln 2}, &\ker\sigma\subseteq\ker\rho,\\[6pt] +\infty,&\text{otherwise}, \end{cases}

where $f[X]$ denotes continuous functional calculus and the real logarithm has value $0$ at $0$ . The assertion is

\left[\frac{\|\rho-\sigma\|_1^2}{2\ln 2}\right]_+ \le D_{\mathrm{bits}}(\rho\|\sigma).

If the kernel inclusion fails, the right side is $+\infty$ . The density hypotheses cannot hold when $I$ is empty.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph