§II.I, Eqs.(30)–(31): tightened channel-specific bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P49.channel_specific_discrimination_bound

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

prove2quantum

Let $\mathcal E_0,\mathcal E_1:d\to e$ be CPTP, $d\ge2$ , $e\ge1$ , $n\ge1$ , and integer $M\ge2$ . Put $\mathcal E_u^M=\mathcal E_u\circ\Gamma_{d,M}$ and $\overline\Delta_M=(\|\mathcal E_0-\mathcal E_0^M\|_\diamond+\|\mathcal E_1-\mathcal E_1^M\|_\diamond)/2$ , using unhalved diamond norms. Every common adaptive protocol has terminal states satisfying

\|\rho_n(0)-\rho_n(1)\|_1\le2n\overline\Delta_M+\|\rho_{\mathcal E_0}^{\otimes nM}-\rho_{\mathcal E_1}^{\otimes nM}\|_1.

Consequently

p_n\ge\frac{1-n\overline\Delta_M-D(\rho_{\mathcal E_0}^{\otimes nM},\rho_{\mathcal E_1}^{\otimes nM})}{2}.

This improves the universal estimate when the actual channel-specific simulation errors can be computed.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P49

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P49

open QAlgorithms Filter

open scoped Matrix ComplexConjugate ComplexOrder BigOperators

attribute [local instance] Classical.propDecidable Classical.decEq

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

open QAlgorithms.Papers.Independent.Dependency50.P18 (bipartiteTensor)

open QAlgorithms.Papers.Independent.Information100.P71 (diamond AdaptiveTest adaptiveInput adaptiveAccept)

open QAlgorithms.Papers.Independent.Bridge50.P25
  (LOCCOn normalizedChannelChoi TwoWayGenerationCode TwoWayChannelProtocol
   generationCodeError twoWayGenerationCapacity sendChannelRegister StateFunctional
   IsDimensionChangingLOCCMonotone privateStateInPartyOrder)

open QAlgorithms.Papers.Independent.Support50.P07 (amplitudeDampingChannel)

/-- PDF p.6, (30)--(31): channel-specific full diamond errors, with their
arithmetic mean. The same physical test is used under both hypotheses. -/
theorem channel_specific_discrimination_bound (d e n M : ℕ) [NeZero d] [NeZero e]
    (hd : 2 ≤ d) (hn : 1 ≤ n) (hM : 2 ≤ M)
    (E0 E1 : Superop (Fin d) (Fin e)) (h0 : IsChannel E0) (h1 : IsChannel E1) :
    (∀ P : AdaptiveTest (Fin d) (Fin e) n,
      traceNorm (testOutput P E0 - testOutput P E1) ≤
        2*n*meanSimulationError M E0 E1 +
        traceNorm (tensorPower (n*M) (normalizedChannelChoi E0) -
          tensorPower (n*M) (normalizedChannelChoi E1))) ∧
    (1-n*meanSimulationError M E0 E1 - traceDistance
      (tensorPower (n*M) (normalizedChannelChoi E0))
      (tensorPower (n*M) (normalizedChannelChoi E1)))/2 ≤ symmetricAdaptiveError n E0 E1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P49

end

Source

Fundamental limits to quantum channel discrimination, arXiv:1803.02834v4, PDF p. 6, §II.I, Eqs.(30)–(31): tightened channel-specific bound

Read-back

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

For all natural numbers $d,e,n,M$ , equipped with $d,e\ne0$ , with $d\ge2$ , $n\ge1$ , and $M\ge2$ , and all channels $\mathcal E_0,\mathcal E_1:d\to e$ , where channels have finite Kraus representations with $\sum_jK_j^\dagger K_j=I$ , define $\Phi_d=d^{-1}\sum_{x,y}|x,x\rangle\langle y,y|$ and $J_i=(\operatorname{id}_d\otimes\mathcal E_i)(\Phi_d)$ . Define $\mathcal P_{d,M}$ using signal entries $S_i[(x,a),(y,b)]=d^{-1}\mathbf1_{\{x=a_i,\ y=b_i,\ a_j=b_j\ \forall j\ne i\}}$ , $S=\sum_iS_i$ , $R=f(S)$ , $f(t)=(\sqrt t)^{-1}$ , $f(0)=0$ , and effects $Q_i=RS_iR+M^{-1}(I-RSR)$ : contract $X\otimes\Phi_d^{\otimes M}$ against $Q_i$ on the input and first halves, retain second-half port $i$ , and sum over $i$ . Put

\widetilde{\mathcal E}_{i,M}=\mathcal E_i\circ\mathcal P_{d,M}, \qquad \bar\delta_M=\frac{\Delta_d(\mathcal E_0-\widetilde{\mathcal E}_{0,M}) +\Delta_d(\mathcal E_1-\widetilde{\mathcal E}_{1,M})}{2},

where

\Delta_d(\mathcal F)= \sup_{\|X\|_1\le1}\|(\operatorname{id}_d\otimes\mathcal F)(X)\|_1, \qquad \|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X},

and the supremum ranges over all complex matrices on two input registers. For every adaptive test $P$ , consisting of a positive finite memory dimension, an initial density matrix on memory and input, channels from memory-output to memory-input at every natural step index, and an effect $0\le H\le I$ , let $\omega_{P,i}$ be its memory-output state after $n$ uses of $\mathcal E_i$ , with its prescribed channels after the first $n-1$ uses. Then

\|\omega_{P,0}-\omega_{P,1}\|_1 \le2n\bar\delta_M+\|J_0^{\otimes nM}-J_1^{\otimes nM}\|_1.

Also, if $p_n$ denotes the infimum of $(1-\operatorname{Re}\operatorname{tr}(H\omega_{P,0})+\operatorname{Re}\operatorname{tr}(H\omega_{P,1}))/2$ over these tests, then

\frac{1-n\bar\delta_M-\frac12\|J_0^{\otimes nM}-J_1^{\otimes nM}\|_1}{2} \le p_n.

The tensor powers here have entries given by products of the corresponding Choi entries; the first inequality quantifies over the entire test structure even though its final effect does not enter that inequality.

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