Lemma 1: diamond norm bounded by Choi entrywise norm

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.diamond_le_choi_maxEntry

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

prove2quantum

Let $A,B$ be nonzero finite-dimensional complex Hilbert spaces with fixed orthonormal bases and let $\Theta:\mathcal B(A)\to\mathcal B(B)$ be any complex-linear map. Define its unnormalized reference-first Choi matrix by $J(\Theta)_{(i,b),(j,c)}=\Theta(|i\rangle\langle j|)_{b,c}$ and write $\|J\|_{\max}=\max_{u,v}|J_{u,v}|$ . Then

\|\Theta\|_\diamond\le (\dim A)(\dim B)^2\|J(\Theta)\|_{\max}.

Here the diamond norm is the stabilized induced trace norm on all operators; positivity and trace preservation are not assumed. This converts entrywise Choi estimates into channel-norm estimates.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P50

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P50

variable {A B E F : Type}

variable [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B]

variable [Fintype E] [DecidableEq E] [Fintype F] [DecidableEq F]

open QAlgorithms.Papers.Independent.Information100.P67
  (IsIsometry receiverChannel complementaryChannel maximumCoherentInformation
    dilationPower idealJoint)

open QAlgorithms.Papers.Independent.Information100.P80 (log2)

open QAlgorithms.Papers.Independent.Information100.P69 (diamond choi)

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

open QAlgorithms.Papers.Independent.Frontier18.P17 (clock)

/-- Lemma 1, PDF p.5: arbitrary complex-linear maps, without CP, TP or Hermiticity
assumptions. The Choi matrix is unnormalized and reference-first. -/
theorem diamond_le_choi_maxEntry [Nonempty A] [Nonempty B]
    (Theta : Matrix A A ℂ →ₗ[ℂ] Matrix B B ℂ) :
    diamond Theta ≤ (Fintype.card A : ℝ) * (Fintype.card B : ℝ) ^ 2 *
      maxEntry (choi Theta) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P50

end

Source

Quantum and private capacities of low-noise channels, arXiv:1705.04335v3, PDF p. 5, Lemma 1: diamond norm bounded by Choi entrywise norm

Read-back

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

For every pair of finite nonempty types $A,B$ , each equipped with decidable equality, and every complex-linear map $\Theta$ from complex matrices on $A$ to complex matrices on $B$ , define the matrix $J_\Theta$ on $A\times B$ by

(J_\Theta)_{(a,b),(a',b')}=\Theta(E_{a,a'})_{b,b'},

where $E_{a,a'}$ has its sole nonzero entry $1$ at $(a,a')$ . Then

\sup_{\|X\|_1\le1} \|(\mathrm{id}_A\otimes\Theta)(X)\|_1 \le |A|\,|B|^2 \max_{i,j\in A\times B}|(J_\Theta)_{i,j}|.

The supremum ranges over all complex matrices $X$ on $A\times A$ , not only positive or Hermitian ones; $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ , and the amplified map applies $\Theta$ to each reference matrix block. The maximum on the right is the real supremum of the entry magnitudes, which is a maximum here because the index sets are finite and nonempty. No positivity or trace-preservation assumption is imposed on $\Theta$ .

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