Theorem 8 / Eq.(48): channel asymptotic equipartition property

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.channel_aep

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

prove2quantum

All systems have finite positive dimension and fixed computational bases. Matrix order is Loewner order and logarithms are base two.

For every CPTP channel $\mathcal N:A'\to B$ , let $I(\mathcal N)$ be the maximum state mutual information over all purified input density matrices, including singular ones. Then

\lim_{\varepsilon\downarrow0}\lim_{n\to\infty}\frac1n I_{\max}^{\varepsilon}(\mathcal N^{\otimes n})=I(\mathcal N).

The inner limits exist for every $0<\varepsilon<1$ , and the outer limit approaches zero from above. A maximizing input density for $I(\mathcal N)$ exists. This is the channel asymptotic equipartition property.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P65

Formal statement

noncomputable section

open Filter QAlgorithms

open scoped BigOperators Matrix ComplexConjugate ComplexOrder Topology

namespace QAlgorithms.Papers.Independent.Intakethird100.P65

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Dependency50.P09 (transposeBob)

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

open QAlgorithms.Papers.Independent.Independent2.P01 (dampingKraus damping)

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

open QAlgorithms.Papers.Independent.Information100.P06 (Below)

open QAlgorithms.Papers.Independent.Information100.P34 (choi)

open QAlgorithms.Papers.Independent.Information100.P62 (Stochastic)

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

open QAlgorithms.Papers.Independent.Information100.P67 (IsSubnormalized purifiedDistance)

open QAlgorithms.Papers.Independent.Information100.P69 (replacer permute)

open QAlgorithms.Papers.Independent.Information100.P71 (diamond channelPower channelRelative)

open QAlgorithms.Papers.Independent.Support50.P39 (quantumMutualInformation)

variable {A B C D R : Type} [Fintype A] [DecidableEq A]
  [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C]
  [Fintype D] [DecidableEq D] [Fintype R] [DecidableEq R]

variable [Nonempty A] [Nonempty B] [Nonempty C] [Nonempty D] [Nonempty R]

/-- Theorem 8, Eq.(48), PDF pp.11--12: successive limits in the printed order,
with existence of the inner limits. No full-rank restriction on the optimizer. -/
theorem channel_aep (N : Superop A B) (hN : IsChannel N) :
    IteratedLimit (fun e n => smoothChannelInfo (channelPower N n) e / n)
      (channelMutualInfo N) ∧
    (∃ rho : Mat A, IsDensityMatrix rho ∧
      quantumMutualInformation (idTensorSuperop N (purify rho)) = channelMutualInfo N) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P65

end

Source

Quantum Channel Simulation and the Channel's Smooth Max-Information, arXiv:1807.05354v2, PDF p. 11, Theorem 8 / Eq.(48): channel asymptotic equipartition property

Read-back

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

For finite index types $A,B$ , with decidable equality, let $N:A\to B$ be a channel, meaning a finite Kraus sum with $\sum_iK_i^\dagger K_i=I_A$ . Write $S(R)=-\operatorname{Re}\operatorname{tr}(f(R))$ , where $f(x)=x\log_2x$ is applied by continuous functional calculus, and define $I(R)=S(\operatorname{Tr}_B R)+S(\operatorname{Tr}_A R)-S(R)$ . For a density matrix $\rho$ on $A$ , let $v_\rho(a,a')=(\sqrt\rho)_{a,a'}$ , let $P_\rho=|v_\rho\rangle\langle v_\rho|$ , and put $C(N)=\sup_{\rho\text{ density}}I((\mathrm{id}_A\otimes N)(P_\rho))$ . A density matrix means a positive semidefinite matrix of trace $1$ , and $((\mathrm{id}_A\otimes N)(X))_{(r,b),(s,b')}=N((X_{(r,a),(s,a')})_{a,a'})_{b,b'}$ . To define the smoothed quantity, set $D_{\max}(R\|T)=\inf\{\lambda\in\mathbb R:2^\lambda T-R\ge0\}$ in the extended reals, $I_{\max}(R)=\inf_{\sigma\text{ density}}D_{\max}(R\|(\operatorname{Tr}_B R)\otimes\sigma)$ , and $I_{\mathrm{ch}}(T)=(I_{\max}((\mathrm{id}_A\otimes T)(\Phi_A)))_{\mathrm{toReal}}$ , where $\Phi_A$ has entry $|A|^{-1}$ when both index pairs have equal coordinates and $0$ otherwise, and infinities convert to $0$ . Let

I_e(T)=\inf_{\substack{M\text{ channel}\\\frac12\|M-T\|_\diamond\le e}} I_{\mathrm{ch}}(M), \quad \|\Delta\|_\diamond=\sup_{\|X\|_1\le1} \|(\mathrm{id}\otimes\Delta)(X)\|_1, \quad \|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X},

using all matrices on an input-sized reference tensor the input. Tensor powers act by

(T^{\otimes n}(X))_{y,z} =\sum_{x,x'}X_{x,x'}\prod_{i=0}^{n-1} T(|x_i\rangle\langle x'_i|)_{y_i,z_i}.

There exists a real function $L$ such that, for every $0<e<1$ ,

\lim_{j\to\infty}\frac{I_e(N^{\otimes(j+1)})}{j+1}=L(e), \qquad \lim_{e\downarrow0}L(e)=C(N),

and there exists a density matrix $\rho$ on $A$ with $I((\mathrm{id}_A\otimes N)(P_\rho))=C(N)$ . The optimizing $\rho$ is 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