Lemma 9: quantitative quantum-capacity expansion from polynomial degradability

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.quantumCapacity_polynomialDegradability

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

prove2quantum

All systems are nonzero finite-dimensional complex Hilbert spaces. A channel is complex-linear, completely positive and trace preserving. Its receiver and full complementary channel are obtained from the same isometric dilation. Write $Q(N)$ and $P(N)$ for the unassisted operational quantum and private capacities, allowing arbitrary collective codes over independent uses with vanishing reliability error and environmental leakage. Write $I_c(N)=\max_\rho[S(N(\rho))-S(N^c(\rho))]$ , where the maximum includes every density operator. Entropies and logarithms are in bits, with $0\log 0=0$ . The diamond norm has no factor $1/2$ .

Let $N(p):A\to B$ be channels for $p\in[0,1]$ with fixed finite input/output spaces and a common finite dilation space. Let $r>1$ and $c\ge0$ , and suppose $\operatorname{dg}(N(p))\le cp^r$ throughout this interval. Here $\operatorname{dg}$ is the minimum, over all CPTP maps $D:B\to E$ , of $\|N^c-D\circ N\|_\diamond$ . If $c=0$ , then $Q(N(p))=I_c(N(p))$ for every physical $p$ . If $c>0$ , there are $K\ge0$ and $0<\delta\le1$ such that, for every $0<p<\delta$ , writing $e(p)$ for the actual Choi rank, rank-one values have exact equality and rank $e(p)\ge2$ satisfies

|Q(N(p))-I_c(N(p))|\le L_Q(e(p),c,r,p)+Kp^{3r}, \qquad L_Q(e,c,r,p)=crp^{r-1}(-p\log_2p)+cp^r\left[-\log_2c+1+\frac1{\ln2}+\log_2e+\frac12\log_2(e-1)\right].

The Choi rank may vary with $p$ ; no constant-rank assumption is required. This gives the quantitative capacity expansion from polynomial approximate degradability.

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 9, PDF p.9: actual Choi rank may vary. The c=0 and rank-one cases are
exact, and the general branch retains the O(p^(3r)) remainder. -/
theorem quantumCapacity_polynomialDegradability [Nonempty A] [Nonempty B] [Nonempty E]
    (V : ℝ → Matrix (B × E) A ℂ)
    (hV : ∀ p ∈ Set.Icc 0 1, IsIsometry (V p))
    (c r : ℝ) (hc : 0 ≤ c) (hr : 1 < r)
    (hdg : ∀ p ∈ Set.Icc 0 1, degradability (V p) ≤ c * p ^ r) :
    (c = 0 → ∀ p ∈ Set.Icc 0 1, dilationQuantumCapacity (V p) = maximumCoherentInformation (V p)) ∧
    (0 < c → ∃ K : ℝ, 0 ≤ K ∧ ∃ delta : ℝ, 0 < delta ∧ delta ≤ 1 ∧
      ∀ p ∈ Set.Ioo 0 delta,
        if dilationChoiRank (V p) = 1 then dilationQuantumCapacity (V p) = maximumCoherentInformation (V p)
        else |dilationQuantumCapacity (V p) - maximumCoherentInformation (V p)| ≤
          quantumPolynomialLeading (dilationChoiRank (V p)) c r p + K * p ^ (3 * r)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P50

end

Source

Quantum and private capacities of low-noise channels, arXiv:1705.04335v3, PDF p. 9, Lemma 9: quantitative quantum-capacity expansion from polynomial degradability

Read-back

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

Let $A,B,E$ be finite nonempty types equipped with decidable equality, and let $p\mapsto V_p$ be any family of complex matrices $B\times E\leftarrow A$ such that $V_p^\dagger V_p=I_A$ for every $p\in[0,1]$ . Write $N_p(\rho)=\operatorname{Tr}_E(V_p\rho V_p^\dagger)$ , $N_p^c(\rho)=\operatorname{Tr}_B(V_p\rho V_p^\dagger)$ , and

d(V_p)=\inf\left\{\eta\in[0,2]: \exists D\text{ a channel }B\to E,\ \|N_p^c-D\circ N_p\|_\diamond\le\eta\right\}.

Suppose $c\ge0,r>1$ are real and $d(V_p)\le cp^r$ for every $p\in[0,1]$ . Then both of the following implications hold: if $c=0$ , then $Q(N_p)=I_{\max}(V_p)$ for every $p\in[0,1]$ ; if $c>0$ , there exist real constants $K\ge0$ and $0<\delta\le1$ such that for every $0<p<\delta$ , writing

e_p=\operatorname{rank}J_{N_p}, \qquad (J_{N_p})_{(a,b),(a',b')}=N_p(E_{a,a'})_{b,b'},

one has $Q(N_p)=I_{\max}(V_p)$ when $e_p=1$ , and otherwise

|Q(N_p)-I_{\max}(V_p)| \le crp^{r-1}(-p\log_2p) +cp^r\left[-\log_2c+1+\frac1{\ln2} +\log_2e_p+\frac12\log_2(e_p-1)\right]+Kp^{3r}.

Here $E_{a,a'}$ is the matrix unit, a density matrix is positive semidefinite with trace one, and

I_{\max}(V_p)=\sup_{\rho\text{ density}} [H(N_p(\rho))-H(N_p^c(\rho))], \qquad H(\rho)=-\operatorname{Re}\operatorname{Tr}[(x\mapsto x\log_2x)(\rho)].

A channel is a map $X\mapsto\sum_jK_jXK_j^\dagger$ for a finite family with $\sum_jK_j^\dagger K_j=I$ . The number $Q(N)$ is the real supremum of nonnegative $s$ for which there are, for every natural $n$ , positive integers $M_n$ and encoding and decoding channels between $M_n$ dimensions and the input and output spaces of $N^{\otimes n}$ , whose entanglement fidelity tends to one and for which, for every $\xi>0$ , eventually $s-\xi\le\log_2M_n/n$ . That fidelity is the overlap of $|\phi_{M_n}\rangle\langle\phi_{M_n}|$ with its image under the identity on the first factor and the encoded, transmitted, decoded channel on the second, where $\phi_M=M^{-1/2}\sum_j|j,j\rangle$ ; tensor powers send tensor products of matrix units to tensor products of their images. The diamond quantity is $\sup_{\|X\|_1\le1}\|(\mathrm{id}_A\otimes\Phi)(X)\|_1$ , over all complex matrices on $A\times A$ , with amplification acting on reference matrix blocks and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . All real powers use real exponentiation, and $\log_2x=\ln x/\ln2$ . No continuity of $V_p$ is assumed; the positive- $c$ conclusion excludes $p=0,\delta$ , while the zero- $c$ conclusion includes $p=0,1$ .

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