Audenaert’s binary Holevo bound

Abstract

Binary Holevo information in bits is at most half the trace norm of the difference.

Theorem 1.1 (The binary ensemble inequality).

$$\forall (n:\mathbb{N}),\forall (sigma:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),\forall (tau:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),((\mathrm{PosSemidef}\left(sigma\right))\wedge (\mathrm{trace}\left(sigma\right)=1))\Rightarrow (((\mathrm{PosSemidef}\left(tau\right))\wedge (\mathrm{trace}\left(tau\right)=1))\Rightarrow (-\mathrm{re}\left(\mathrm{trace}\left(\mathrm{cfc}\left(((x:\mathbb{R})\mapsto x\cdot \mathrm{Real}.\mathrm{logb}(2,x)),(\frac{1}{2}:\mathbb{C})\cdot (sigma+tau)\right)\right)\right)-\frac{-\mathrm{re}\left(\mathrm{trace}\left(\mathrm{cfc}\left(((x:\mathbb{R})\mapsto x\cdot \mathrm{Real}.\mathrm{logb}(2,x)),sigma\right)\right)\right)+-\mathrm{re}\left(\mathrm{trace}\left(\mathrm{cfc}\left(((x:\mathbb{R})\mapsto x\cdot \mathrm{Real}.\mathrm{logb}(2,x)),tau\right)\right)\right)}{2}\le \frac{\mathrm{traceNorm}\left(sigma-tau\right)}{2}))$$

Proof. Machine-checked in Lean as D5/S3/Divergence/AudenaertBinaryHolevoBound.binaryHolevoBound (✓ std3). ∎

Citation. Koenraad M. R. Audenaert (2014). Quantum Skew Divergence. DOI: 10.1063/1.4901039. URL: https://arxiv.org/abs/1304.5935v2.

Commentary.

Audenaert, Quantum Skew Divergence, Theorem 14, bounds Holevo information by the classical mixing entropy times the maximal trace distance. For an equiprobable binary ensemble the mixing entropy is one bit. The matrices may be singular. The matrix-log resolvent integral gives the derivative along a positive affine path. Positivity of that derivative and its trace pairing bound the skew divergence by trace distance times the negative logarithm of the mixing weight. Specializing the weight to one half gives the binary inequality for strictly positive states. Adding epsilon times the identity and dividing by one plus n epsilon preserves trace one, and continuity of x log x extends the estimate to singular states.

References

• Truth anchor: D5/S3/Divergence/AudenaertBinaryHolevoBound.binaryHolevoBound
• Dependency: D5/S3/ArithSums/TwoPointSlabSupport
• Dependency: D5/S3/Divergence/LogDerivTrace
• Dependency: D5/S3/Quantum/Entanglement/ConicalDesignConcurrenceComparability
• Dependency: D5/S3/Quantum/Subentropy/UniformIntegrals