Corollary 2: entrywise quadratic Choi errors imply quadratic diamond error

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.entrywiseQuadratic_implies_diamondQuadratic

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

prove2quantum

Fix nonzero finite-dimensional complex Hilbert spaces $A,B$ and bases. Let $\Theta(p):\mathcal B(A)\to\mathcal B(B)$ be complex-linear for every real $p$ . Suppose that, for each pair of indices $u,v$ of the unnormalized reference-first Choi matrix, there exist $C_{uv}\ge0$ and $\delta_{uv}>0$ such that $|J(\Theta(p))_{uv}|\le C_{uv}p^2$ whenever $0<|p|<\delta_{uv}$ . Then there exist $C\ge0$ and $\delta>0$ such that

\|\Theta(p)\|_\diamond\le Cp^2\qquad(0<|p|<\delta).

This is a two-sided local statement; finite fixed dimensions allow common constants for the entries.

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)

/-- Corollary 2, PDF p.6: a two-sided punctured neighborhood of zero; dimensions
and bases are fixed. Each entry may initially have its own big-O constants. -/
theorem entrywiseQuadratic_implies_diamondQuadratic [Nonempty A] [Nonempty B]
    (Theta : ℝ → (Matrix A A ℂ →ₗ[ℂ] Matrix B B ℂ))
    (h : ∀ i j : A × B, ∃ C : ℝ, 0 ≤ C ∧ ∃ delta : ℝ, 0 < delta ∧
      ∀ p : ℝ, 0 < |p| → |p| < delta → ‖choi (Theta p) i j‖ ≤ C * p ^ 2) :
    ∃ C : ℝ, 0 ≤ C ∧ ∃ delta : ℝ, 0 < delta ∧
      ∀ p : ℝ, 0 < |p| → |p| < delta → diamond (Theta p) ≤ C * p ^ 2 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P50

end

Source

Quantum and private capacities of low-noise channels, arXiv:1705.04335v3, PDF p. 6, Corollary 2: entrywise quadratic Choi errors imply quadratic diamond error

Read-back

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

For finite nonempty types $A,B$ equipped with decidable equality, let $p\mapsto\Theta_p$ be any real-indexed family of complex-linear maps from complex matrices on $A$ to complex matrices on $B$ , and define

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

Suppose that for every pair $i,j\in A\times B$ there exist real constants $C_{i,j}\ge0$ and $\delta_{i,j}>0$ such that $|(J_{\Theta_p})_{i,j}|\le C_{i,j}p^2$ whenever $0<|p|<\delta_{i,j}$ . Then there exist common real constants $C\ge0,\delta>0$ such that

0<|p|<\delta\quad\Longrightarrow\quad \sup_{\|X\|_1\le1}\|(\mathrm{id}_A\otimes\Theta_p)(X)\|_1\le Cp^2.

Here $E_{a,a'}$ is the matrix unit, the supremum ranges over all complex matrices on $A\times A$ , $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ , and amplification applies the map to each reference matrix block. Both positive and negative nonzero $p$ are covered. There is no continuity assumption on the family and no hypothesis or conclusion concerning its value at $p=0$ .

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