Equality of attained ordinary and conditional channel-information maxima

Open

QAlgorithms.Papers.Independent.Intakethird100.P27.channel_information_maxima

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

prove2quantum

Let $\mathcal N:A\to B'$ be a fixed CPTP channel between finite nonempty registers. Both optimizations below range over normalized pure states, and all entropies are in bits. On the left, the purifying reference may be chosen isomorphic to $A$ . On the right, the reference $R$ and side register $B$ may be arbitrary finite nonempty systems. The channel acts only on $A$ . Then both maxima are attained and

\max_{\psi_{RA}}I(R;B')_{(\mathrm{id}\otimes\mathcal N)(\psi)}=\max_{\phi_{RAB}}I(R;B'\mid B)_{(\mathrm{id}\otimes\mathcal N\otimes\mathrm{id})(\phi)}.

The common value is achieved on the right with a product pure one-dimensional side register. The upper bound still covers every side register and every pure input.

This identifies channel information quantities; it does not assert the conjectured general-input operational simulation theorem (40).

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P27

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P27

open Filter

open scoped Matrix ComplexConjugate ComplexOrder ENNReal

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Dependency50.P19
  (first marginalRB mutualInformation bipartiteBlock epr)

open QAlgorithms.Papers.Independent.Information100.P08 (formation)

open QAlgorithms.Papers.Independent.Gap48.P20 (redistributionMarginal)

open QAlgorithms.Papers.Independent.Bridge50.P37 (isotropicState normalizedEntangledProjection)

/-- PDF pp.14--15, Theorem 15: the ordinary and conditional channel-information
maxima have a common attained value. The ordinary reference is isomorphic to A;
the conditional upper bound ranges over arbitrary nonempty finite reference and
side-register types. A product pure one-dimensional side register attains it.
The conjectured general-input simulation theorem (40) is not asserted. -/
theorem channel_information_maxima {A C : Type} [Fintype A] [Fintype C]
    [Nonempty A] [Nonempty C] (N : Superop A C) (hN : IsChannel N) :
    ∃ v : EuclideanSpace ℂ (A × A), ‖v‖ = 1 ∧
      (∀ w : EuclideanSpace ℂ (A × A), ‖w‖ = 1 →
        mutualInformation (idTensorSuperop N (pureDensity w)) ≤
          mutualInformation (idTensorSuperop N (pureDensity v))) ∧
      (∃ phi : EuclideanSpace ℂ (A × (A × Fin 1)), ‖phi‖ = 1 ∧
        conditionalOutputInformation N phi =
          mutualInformation (idTensorSuperop N (pureDensity v))) ∧
      (∀ (R B : Type) [Fintype R] [Fintype B] [Nonempty R] [Nonempty B],
        ∀ phi : EuclideanSpace ℂ (R × (A × B)), ‖phi‖ = 1 →
          conditionalOutputInformation N phi ≤
            mutualInformation (idTensorSuperop N (pureDensity v))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P27

end

Source

Quantum rate distortion coding with auxiliary resources, arXiv:1212.5316v3, PDF p. 14, Theorem 15, proof continues p.15

Read-back

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

Let $A,C$ be finite, nonempty types, and let $N$ be a channel from matrices on $A$ to matrices on $C$ , meaning that some finite family of matrices $K_j$ satisfies $N(X)=\sum_jK_jXK_j^\dagger$ for every $X$ and $\sum_jK_j^\dagger K_j=I$ . For a vector $\phi$ on $R\times(A\times B)$ , define $X^\phi$ on $R\times(C\times B)$ by

X^\phi_{(r,(c,b)),(r',(c',b'))} = N\!\left( \left[\phi_{(r,(a,b))}\, \overline{\phi_{(r',(a',b'))}}\right]_{a,a'\in A} \right)_{c,c'}, \qquad J_N(\phi)=H(X^\phi_{RB})+H(X^\phi_{CB})-H(X^\phi_B)-H(X^\phi),

where subscripts denote partial traces over the omitted registers. Here $H(Y)=-\operatorname{Re}\operatorname{tr}(f(Y))$ , with $f(x)=x\log_2x$ applied by continuous functional calculus. For $w\in\mathbb C^{A\times A}$ , let $Y^w=(\operatorname{id}_A\otimes N)(|w\rangle\langle w|)$ , explicitly $Y^w_{(r,c),(r',c')}=N([w_{(r,a)}\overline{w_{(r',a')}}]_{a,a'})_{c,c'}$ , and put $I(Y)=H(\operatorname{Tr}_C Y)+H(\operatorname{Tr}_A Y)-H(Y)$ . The declaration asserts that there exists a unit vector $v\in\mathbb C^{A\times A}$ such that $I(Y^w)\le I(Y^v)$ for every unit vector $w\in\mathbb C^{A\times A}$ ; there exists a unit vector $\phi\in\mathbb C^{A\times(A\times\{*\})}$ , with a one-element last register, satisfying $J_N(\phi)=I(Y^v)$ ; and, for every pair of finite, nonempty types $R,B$ and every unit vector $\phi\in\mathbb C^{R\times(A\times B)}$ , one has $J_N(\phi)\le I(Y^v)$ . No uniqueness of $v$ or of the attaining $\phi$ is asserted.

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