Remark 6 / Eq.(36): distance to constant channels

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.constantChannel_distance

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.

Let $\mathcal N:A\to B$ be CPTP and $\varepsilon\ge0$ . Let $\mathcal G$ consist of all replacement channels $\mathcal R_\sigma(X)=\operatorname{Tr}(X)\sigma$ , where $\sigma$ is a density matrix on $B$ . Define $D_{\max}^\varepsilon(\mathcal N\|\mathcal M)$ by smoothing only $\mathcal N$ over same-dimensional CPTP channels at half-diamond distance at most $\varepsilon$ , and using the max-relative entropy of unnormalized Choi matrices. Then

I_{\max}^\varepsilon(\mathcal N)=\min_{\mathcal M\in\mathcal G}D_{\max}^\varepsilon(\mathcal N\|\mathcal M).

A minimizing constant channel exists and has value no larger than every other constant reference. Extended-real divergences retain support failures.

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]

/-- Remark 6, Eq.(36), PDF p.9: equality to a MINIMUM, including attainment. -/
theorem constantChannel_distance (N : Superop A B) (hN : IsChannel N) (e : ℝ) (he : 0 ≤ e) :
    ∃ M : Superop A B, Constant M ∧
      smoothChannelDmax N M e = (smoothChannelInfo N e : EReal) ∧
      ∀ T : Superop A B, Constant T → smoothChannelDmax N M e ≤ smoothChannelDmax N T e := 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. 9, Remark 6 / Eq.(36): distance to constant channels

Read-back

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

For finite index types $A,B$ , with decidable equality, every channel $N:A\to B$ and real $e\ge0$ admit a density matrix $\sigma$ on $B$ and the constant map $M(X)=\operatorname{tr}(X)\sigma$ with the following property. Here a density matrix is positive semidefinite with complex trace $1$ , and a channel has a finite Kraus representation with $\sum_iK_i^\dagger K_i=I$ . Write $J_T((a,b),(a',b'))=T(|a\rangle\langle a'|)_{b,b'}$ , and define $D_{\max}(R\|S)=\inf\{\lambda\in\mathbb R:2^\lambda S-R\ge0\}$ in the extended reals. Let

d_e(N,M)= \inf_{\substack{T\text{ channel}\\\frac12\|T-N\|_\diamond\le e}} D_{\max}(J_T\|J_M).

The norm here is $\|\Delta\|_\diamond=\sup_{\|X\|_1\le1}\|(\mathrm{id}_A\otimes\Delta)(X)\|_1$ , over all matrices on $A\times A$ , with $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ . For a matrix $R$ on $A\times B$ , put $I_{\max}(R)=\inf_{\omega\text{ density}}D_{\max}(R\|(\operatorname{Tr}_B R)\otimes\omega)$ , let $\Phi_A$ have entry $|A|^{-1}$ when both row and column pairs have equal coordinates and $0$ otherwise, and set $I(T)=(I_{\max}((\mathrm{id}_A\otimes T)(\Phi_A)))_{\mathrm{toReal}}$ , with infinities converted to $0$ . Finally set $I_e(N)=\inf_{T\text{ channel},\,\frac12\|T-N\|_\diamond\le e}I(T)$ , a real infimum. The asserted property is

d_e(N,M)=(I_e(N):\overline{\mathbb R}), \qquad d_e(N,M)\le d_e(N,T) \quad\text{for every }T(X)=\operatorname{tr}(X)\omega \text{ with }\omega\text{ a density matrix}.

The constant comparator is attained; the declaration does not assert attainment of the inner smoothing infima, and $e$ has no upper bound.

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