A counterexample to the maximal reverse Pinsker bound

Abstract

A noncommuting qubit pair violates the maximal reverse Pinsker bound.

Lanier, Béguinot and Rioul, arXiv:2501.14340v1, §III-C, p. 5: “We conjecture that (49) is in fact not necessary for (50) to hold.” The same paragraph states: “Our bound holds in general for any f-divergence, in particular for the maximal f-divergence.”

Definition 1.1 (The maximal spectral divergence).

$$\forall (n:\mathbb{N}),\forall (f:\mathbb{R}\to \mathbb{R}),\forall (rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),\forall (sigma:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),\mathrm{maxDivergence}\left(f,rho,sigma\right)=\mathrm{re}\left(\mathrm{trace}\left(\mathrm{sqrt}\left(sigma\right)\cdot \mathrm{cfc}\left(f,(\mathrm{sqrt}\left(sigma\right){)}^{-1}\cdot rho\cdot (\mathrm{sqrt}\left(sigma\right){)}^{-1}\right)\cdot \mathrm{sqrt}\left(sigma\right)\right)\right)$$

Formalization. D5/S3/Divergence/LanierBeguinotRioulReversePinskerRefutation.maxDivergence (✓ std3).

Citation. D. Lanier; J. Béguinot; O. Rioul (2025). From Classical to Quantum: Explicit Classical Distributions Achieving Maximal Quantum f-Divergence. DOI: 10.48550/arXiv.2501.14340. URL: https://arxiv.org/abs/2501.14340v1.

Commentary.

Equation (4), p. 1, is the real part of the trace of the displayed product. The matrix function is Mathlib’s continuous functional calculus. For the operator-convex generator f(x)=(x−1)², its status as a quantum f-divergence satisfying Definition 2 uses the Matsumoto theorem cited in the source. That general data-processing theorem is not proved here.

Definition 1.2 (The proposed right-hand side).

$$\forall (n:\mathbb{N}),\forall (f:\mathbb{R}\to \mathbb{R}),\forall (rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),\forall (sigma:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),\mathrm{reversePinskerBound}\left(f,rho,sigma\right)=\frac{\mathrm{traceNorm}\left(rho-sigma\right)}{2}\cdot (\frac{f\left(\mathrm{sInf}\left(\mathrm{spectrum}\left(\mathbb{R},(\mathrm{sqrt}\left(sigma\right){)}^{-1}\cdot rho\cdot (\mathrm{sqrt}\left(sigma\right){)}^{-1}\right)\right)\right)}{1-\mathrm{sInf}\left(\mathrm{spectrum}\left(\mathbb{R},(\mathrm{sqrt}\left(sigma\right){)}^{-1}\cdot rho\cdot (\mathrm{sqrt}\left(sigma\right){)}^{-1}\right)\right)}+\frac{f\left(\mathrm{sSup}\left(\mathrm{spectrum}\left(\mathbb{R},(\mathrm{sqrt}\left(sigma\right){)}^{-1}\cdot rho\cdot (\mathrm{sqrt}\left(sigma\right){)}^{-1}\right)\right)\right)}{\mathrm{sSup}\left(\mathrm{spectrum}\left(\mathbb{R},(\mathrm{sqrt}\left(sigma\right){)}^{-1}\cdot rho\cdot (\mathrm{sqrt}\left(sigma\right){)}^{-1}\right)\right)-1})$$

Formalization. D5/S3/Divergence/LanierBeguinotRioulReversePinskerRefutation.reversePinskerBound (✓ std3).

Citation. D. Lanier; J. Béguinot; O. Rioul (2025). From Classical to Quantum: Explicit Classical Distributions Achieving Maximal Quantum f-Divergence. DOI: 10.48550/arXiv.2501.14340. URL: https://arxiv.org/abs/2501.14340v1.

Commentary.

Equation (50), p. 4, uses the least and greatest points of the real spectrum of the relative matrix and the trace norm of the state difference. The numerical example below has spectral endpoints 4/5 and 6/5, so both denominators are nonzero.

Definition 1.3 (The conjectured maximal-divergence inequality).

$$(claim)\iff (\forall (n:\mathbb{N}),\forall (f:\mathbb{R}\to \mathbb{R}),(\mathrm{ConvexOn}\left(\mathbb{R},\mathrm{Ici}\left(0\right),f\right))\Rightarrow ((f\left(1\right)=0)\Rightarrow (\forall (rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),\forall (sigma:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),(\mathrm{PosSemidef}\left(rho\right))\Rightarrow ((\mathrm{trace}\left(rho\right)=1)\Rightarrow ((\mathrm{PosDef}\left(sigma\right))\Rightarrow ((\mathrm{trace}\left(sigma\right)=1)\Rightarrow (\mathrm{maxDivergence}\left(f,rho,sigma\right)\le \mathrm{reversePinskerBound}\left(f,rho,sigma\right))))))))$$

Formalization. D5/S3/Divergence/LanierBeguinotRioulReversePinskerRefutation.claim (✓ std3).

Citation. D. Lanier; J. Béguinot; O. Rioul (2025). From Classical to Quantum: Explicit Classical Distributions Achieving Maximal Quantum f-Divergence. DOI: 10.48550/arXiv.2501.14340. URL: https://arxiv.org/abs/2501.14340v1.

Commentary.

“We conjecture that (49) is in fact not necessary for (50) to hold.” (§III-C, p. 5.) The displayed proposition is its maximal-divergence instance: every dimension, every real generator convex on the nonnegative half-line and zero at one, and every pair of positive semidefinite states with the second positive definite. Each state has trace one. No matrix-order condition on the absolute difference is imposed.

Theorem 1.4 (A qubit counterexample).

$$\neg (\forall (n:\mathbb{N}),\forall (f:\mathbb{R}\to \mathbb{R}),(\mathrm{ConvexOn}\left(\mathbb{R},\mathrm{Ici}\left(0\right),f\right))\Rightarrow ((f\left(1\right)=0)\Rightarrow (\forall (rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),\forall (sigma:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),(\mathrm{PosSemidef}\left(rho\right))\Rightarrow ((\mathrm{trace}\left(rho\right)=1)\Rightarrow ((\mathrm{PosDef}\left(sigma\right))\Rightarrow ((\mathrm{trace}\left(sigma\right)=1)\Rightarrow (\mathrm{maxDivergence}\left(f,rho,sigma\right)\le \mathrm{reversePinskerBound}\left(f,rho,sigma\right))))))))$$

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

Resolves. Problems/lanier-beguinot-rioul-2025-reverse-pinsker-condition-refutation (refuted) by D5/S3/Divergence/LanierBeguinotRioulReversePinskerRefutation.result.

Source. Repository-derived.

Acknowledgement. D. Lanier; J. Béguinot; O. Rioul (2025). From Classical to Quantum: Explicit Classical Distributions Achieving Maximal Quantum f-Divergence. DOI: 10.48550/arXiv.2501.14340. URL: https://arxiv.org/abs/2501.14340v1.

Commentary.

Let σ=diag(9/25,16/25) and ρ=((9/25,12/125),(12/125,16/25)). Both matrices have trace one; σ is positive definite and ρ is positive semidefinite. The positive square root of σ is diag(3/5,4/5), and the relative matrix is ((1,1/5),(1/5,1)), with spectrum {4/5,6/5}. For f(x)=(x−1)² its matrix function is I/25, giving maxDivergence=1/25=25/625. The absolute difference is (12/125)I, with trace norm 24/125, so reversePinskerBound=24/625. This contradicts the proposed inequality. The matrix ρ+σ−|ρ−σ|=((78/125,12/125),(12/125,148/125)) is positive definite. Thus the same pair also contradicts the conditional maximal-divergence statement of Theorem 4. The proof checks that stronger failure before deriving the displayed negation. The result concerns the spectral formula (4); the Definition 2 admissibility theorem and the source’s other choices of quantum divergence remain separate.

References

• Truth anchor: D5/S3/Divergence/LanierBeguinotRioulReversePinskerRefutation.claim
• Truth anchor: D5/S3/Divergence/LanierBeguinotRioulReversePinskerRefutation.maxDivergence
• Truth anchor: D5/S3/Divergence/LanierBeguinotRioulReversePinskerRefutation.result
• Truth anchor: D5/S3/Divergence/LanierBeguinotRioulReversePinskerRefutation.reversePinskerBound
• Dependency: D5/S3/Quantum/Foundation/FiniteTraceDistance
• Dependency: D5/S3/Quantum/Matrix/SpectralPower
• Dependency: D5/S3/Resource/LogDet/PathSpectralClassical