Corollary 9: intertwining and Kraus-range commutation

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.equalityIntertwining

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

prove2quantum

Under equality in data processing for a finite CPTP map $\Phi$ and faithful normalized states $\rho,\gamma$ , put $D=\log\rho-\log\gamma$ and let $L$ be the supported output log difference. Then

\Phi(D)=\Phi(I)L=L\Phi(I).

For every normalized Kraus representation $\Phi(X)=\sum_kF_kXF_k^{\dagger}$ , form the computed isometry $V_{(a',k),a}=(F_k)_{a',a}$ . Its range projection satisfies

[VV^{\dagger},L\otimes I_K]=0.

This records the intertwining and dilation-range commutation forced by equality.

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]

/-- Corollary 9, equations (45)–(46), PDF pp.16–17: the second operator is lifted
by I_K before commutation with the actual Kraus-range projection. -/
theorem equalityIntertwining [Nonempty A] [Nonempty B] [Nonempty K] (Phi : Superop A B) (hPhi : IsChannel Phi) (rho gamma : Mat A)
    (hr : FaithfulDensity rho) (hg : FaithfulDensity gamma)
    (he : (relativeEntropy (Phi rho) (Phi gamma)).toReal = (relativeEntropy rho gamma).toReal) :
    let D := logMatrix rho - logMatrix gamma
    let L := logMatrix (Phi rho) - logMatrix (Phi gamma)
    Phi D = Phi 1 * L ∧ Phi D = L * Phi 1 ∧
    ∀ F : K → Matrix B A ℂ, IsKrausFamily F → (∀ X, Phi X = krausApply F X) →
      (krausV F * (krausV F)ᴴ) * Matrix.kronecker L (1 : Mat K) =
        Matrix.kronecker L (1 : Mat K) * (krausV F * (krausV F)ᴴ) := 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. 16, Corollary 9: intertwining and Kraus-range commutation

Read-back

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

For finite nonempty index types $A,B,K$ , with the decidable equality structures used in the matrix definitions, let $\Phi:\operatorname{Mat}_A(\mathbb C)\to\operatorname{Mat}_B(\mathbb C)$ admit a finite Kraus representation with completeness relation $\sum_iE_i^\dagger E_i=I_A$ , and let $\rho,\gamma$ be positive definite trace-one matrices. Suppose $D_{\mathbb R}(\Phi\rho\Vert\Phi\gamma)=D_{\mathbb R}(\rho\Vert\gamma)$ , where $D(X\Vert Y)=\operatorname{Re}\operatorname{tr}[f(X)-X\log Y]$ , $f(x)=x\ln x$ , when $\ker Y\subseteq\ker X$ , and $D(X\Vert Y)=+\infty$ otherwise, and real conversion sends $+\infty$ to zero. Set $D_0=\log\rho-\log\gamma$ and $L=\log(\Phi\rho)-\log(\Phi\gamma)$ , with matrix logarithms defined by continuous functional calculus and $\ln0=0$ . Then

\Phi(D_0)=\Phi(I_A)L,\qquad \Phi(D_0)=L\Phi(I_A).

Furthermore, for every family $F_k\in\mathbb C^{B\times A}$ , indexed by $k\in K$ , satisfying $\sum_kF_k^\dagger F_k=I_A$ and $\Phi(X)=\sum_kF_kXF_k^\dagger$ for every matrix $X$ , the matrix $V:\mathbb C^A\to\mathbb C^{B\times K}$ defined by $V_{(b,k),a}=(F_k)_{ba}$ satisfies

VV^\dagger(L\otimes I_K)=(L\otimes I_K)VV^\dagger.

This last assertion quantifies only over representations indexed by the specified $K$ ; if none exist, that universally quantified assertion is vacuous.

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