Theorem 8: adjoint logarithm characterization of equality

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.dataProcessingEquality

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

prove2quantum

Let $\Phi$ be a finite CPTP map and let $\rho,\gamma>0$ be normalized input states. Define $L=\log\Phi(\rho)-\log\Phi(\gamma)$ on their common output support and extend $L$ by zero to its orthogonal complement. Let $\widehat\Phi$ be the actual Hilbert–Schmidt adjoint. Then

H(\Phi(\rho),\Phi(\gamma))=H(\rho,\gamma)\iff\log\rho-\log\gamma=\widehat\Phi(L).

This is the adjoint-logarithm characterization of equality, preserving all finite channels and using compressed output calculus.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P51

Formal statement

noncomputable section

open scoped Matrix ComplexOrder ComplexConjugate Matrix.Norms.L2Operator

open MeasureTheory

namespace QAlgorithms.Papers.Independent.Intakethird100.P51

attribute [local instance] Classical.propDecidable Classical.decEq

-- Exact interfaces from the frozen accepted library; no local redeclarations.

open QAlgorithms.Papers.Independent.Information100.P63 (Mat)

open QAlgorithms.Papers.Independent.Information100.P56 (entropy holevo IsLaw)

open QAlgorithms.Papers.Independent.Information100.P27 (average)

open QAlgorithms.Papers.Independent.Dependency50.P21 (relativeEntropy marginalAB channelAdjoint)

open QAlgorithms.Papers.Independent.Dependency50.P35 (marginalAC)

open QAlgorithms.Papers.Independent.Gap48.P19 (shannonNats)

open QAlgorithms.Papers.Independent.Gap48.P33 (measurementInformation)

section Statements

variable {A B C D J K O : Type}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D] [Fintype J] [Fintype K] [Fintype O]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

variable [DecidableEq J] [DecidableEq K] [DecidableEq O]

/-- Theorem 8, equation (40), PDF pp.15–17: actual adjoint and supported output
logarithms. For faithful inputs the two outputs have common support supp(Phi I),
so the cfc log difference is the unique zero extension from this support. -/
theorem dataProcessingEquality [Nonempty A] [Nonempty B] (Phi : Superop A B) (hPhi : IsChannel Phi) (rho gamma : Mat A)
    (hr : FaithfulDensity rho) (hg : FaithfulDensity gamma) :
    (relativeEntropy (Phi rho) (Phi gamma)).toReal = (relativeEntropy rho gamma).toReal ↔
      logMatrix rho - logMatrix gamma =
        channelAdjoint Phi (logMatrix (Phi rho) - logMatrix (Phi gamma)) := by sorry

end Statements

end QAlgorithms.Papers.Independent.Intakethird100.P51

end

Source

Inequalities for Quantum Entropy: A Review with Conditions for Equality, arXiv:quant-ph/0205064v2, PDF p. 15, Theorem 8: adjoint logarithm characterization of equality

Read-back

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

For finite nonempty index types $A,B$ , with decidable equality as used in the matrix definitions, let $\Phi:\operatorname{Mat}_A(\mathbb C)\to\operatorname{Mat}_B(\mathbb C)$ have a finite Kraus representation $\Phi(X)=\sum_iE_iXE_i^\dagger$ satisfying $\sum_iE_i^\dagger E_i=I_A$ , and let $\rho,\gamma$ be positive definite matrices of trace one on $A$ . Then

D_{\mathbb R}(\Phi\rho\Vert\Phi\gamma)=D_{\mathbb R}(\rho\Vert\gamma) \quad\Longleftrightarrow\quad \log\rho-\log\gamma =\Phi^\sharp\!\left(\log(\Phi\rho)-\log(\Phi\gamma)\right).

The logarithms are continuous-functional-calculus logarithms using $\ln0=0$ , so they are defined even when an output is singular. For a matrix $Y$ on $B$ , the map on the right is explicitly

[\Phi^\sharp(Y)]_{ij} =\sum_{k,l\in B}\overline{[\Phi(E_{ij})]_{kl}}\,Y_{kl},

where $E_{ij}$ is the matrix unit on $A$ . The extended-real $D(X\Vert Y)$ equals $\operatorname{Re}\operatorname{tr}[f(X)-X\log Y]$ , with $f(x)=x\ln x$ , if $\ker Y\subseteq\ker X$ , and equals $+\infty$ otherwise; $D_{\mathbb R}$ denotes its real conversion, which sends $+\infty$ to zero.

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