Equation (7), proved in Section 5.3: CPTP data processing

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.dataProcessing

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

prove2quantum

Let $\Phi$ be any finite CPTP map, possibly between different dimensions, and let $\rho,\gamma>0$ be normalized states. Then

H(\Phi(\rho),\Phi(\gamma))\le H(\rho,\gamma).

The outputs are faithful on their common support $\operatorname{supp}\Phi(I)$ ; output logarithms are evaluated there. Thus channels with singular ambient outputs, including pure-state replacers, are included. This is quantum data processing.

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]

/-- Equation (7), PDF pp.4,15,17: all finite CPTP maps, including singular-output
and rectangular channels. Common-support calculus evaluates the output entropy. -/
theorem dataProcessing [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 := 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. 4, Equation (7), proved in Section 5.3: CPTP data processing

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)$ admit a finite Kraus representation $\Phi(X)=\sum_iE_iXE_i^\dagger$ with $\sum_iE_i^\dagger E_i=I_A$ . For all positive definite matrices $\rho,\gamma$ on $A$ with $\operatorname{tr}\rho=\operatorname{tr}\gamma=1$ ,

D_{\mathbb R}(\Phi\rho\Vert\Phi\gamma)\le D_{\mathbb R}(\rho\Vert\gamma).

Here $D_{\mathbb R}$ is the real conversion of the extended-real function that equals $\operatorname{Re}\operatorname{tr}[f(X)-X\log Y]$ , where $f(x)=x\ln x$ , when $\ker Y\subseteq\ker X$ , and equals $+\infty$ otherwise. Both matrix functions use continuous functional calculus with the total real logarithm, including $\ln0=0$ ; real conversion sends $+\infty$ to zero. The input states are required to be positive definite, while their outputs are not required to be positive definite.

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