Remark 6 / Eq.(40): smooth generalized channel robustness

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.smooth_robustness_identity

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 a CPTP channel $\mathcal N:A\to B$ , define independently $R_g(\mathcal N)=\inf\{t\ge0:\exists\mathcal M\text{ CPTP},\ (\mathcal N+t\mathcal M)/(1+t)\in\mathcal G\}$ , where $\mathcal G$ is the set of replacement channels. Smooth this robustness over CPTP alternatives at half-diamond distance at most $\varepsilon\ge0$ , obtaining $R_g^\varepsilon(\mathcal N)$ . Then

I_{\max}^\varepsilon(\mathcal N)=\log_2(1+R_g^\varepsilon(\mathcal N)).

The mixing channel may be any CPTP map. This relates the independently defined channel entropy and generalized robustness.

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.(40), PDF pp.9--10: independent generalized constantChannelRobustness,
with arbitrary CPTP mixing noise. -/
theorem smooth_robustness_identity (N : Superop A B) (hN : IsChannel N)
    (e : ℝ) (he : 0 ≤ e) :
    smoothChannelInfo N e = Real.logb 2 (1 + smoothRobustness N 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.(40): smooth generalized channel robustness

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 every real $e\ge0$ satisfy $I_e(N)=\log_2(1+R_e(N))$ , with the quantities defined as follows. A channel is a map $X\mapsto\sum_iK_iXK_i^\dagger$ for a finite family satisfying $\sum_iK_i^\dagger K_i=I$ , and a density matrix is positive semidefinite with trace $1$ . Let $\|\Delta\|_\diamond=\sup_{\|X\|_1\le1}\|(\mathrm{id}_A\otimes\Delta)(X)\|_1$ , where $X$ ranges over all matrices on $A\times A$ and $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ . Define $D_{\max}(R\|S)=\inf\{\lambda\in\mathbb R:2^\lambda S-R\ge0\}$ in the extended reals and $I_{\max}(R)=\inf_{\sigma\text{ density}}D_{\max}(R\|(\operatorname{Tr}_B R)\otimes\sigma)$ . If $\Phi_A$ has entry $|A|^{-1}$ when both row and column pairs have equal coordinates and $0$ otherwise, set

I(T)=\left(I_{\max}((\mathrm{id}_A\otimes T)(\Phi_A))\right)_{\mathrm{toReal}}, \qquad I_e(N)=\inf_{\substack{T\text{ channel}\\\frac12\|T-N\|_\diamond\le e}}I(T),

where either extended-real infinity converts to $0$ . For a map $T$ , define

R(T)=\inf\left\{t\ge0: \begin{array}{l} \exists M\text{ channel},\ \exists\sigma\text{ density},\\ (1+t)^{-1}\bigl(T(X)+tM(X)\bigr)=\operatorname{tr}(X)\sigma \text{ for every }X \end{array}\right\}, \qquad R_e(N)=\inf_{\substack{T\text{ channel}\\\frac12\|T-N\|_\diamond\le e}}R(T).

All these smoothing and robustness infima, except those explicitly defining $D_{\max}$ and $I_{\max}$ , are real infima. No optimizer is asserted, and the hypothesis includes $e=0$ and $e\ge1$ .

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