Lemma 10: quantitative private-capacity expansion from polynomial degradability

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.privateCapacity_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 $P(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

|P(N(p))-I_c(N(p))|\le L_P(e(p),c,r,p)+Kp^{2r}, \qquad L_P(e,c,r,p)=3crp^{r-1}(-p\log_2p)+cp^r\left[-3\log_2c+3+\frac3{\ln2}+\log_2(e-1)+4\log_2e\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 10, PDF p.10: private-capacity analogue, with O(p^(2r)) remainder.
There is no constant-rank or positive-c exclusion of exact-degradable boundaries. -/
theorem privateCapacity_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, fullTracePrivateCapacity (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 fullTracePrivateCapacity (V p) = maximumCoherentInformation (V p)
        else |fullTracePrivateCapacity (V p) - maximumCoherentInformation (V p)| ≤
          privatePolynomialLeading (dilationChoiRank (V p)) c r p + K * p ^ (2 * r)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P50

end

Source

Quantum and private capacities of low-noise channels, arXiv:1705.04335v3, PDF p. 10, Lemma 10: quantitative private-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:B\times E\leftarrow A$ be any family of complex matrices with $V_p^\dagger V_p=I_A$ for every $p\in[0,1]$ . Set $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 real $c\ge0,r>1$ satisfy $d(V_p)\le cp^r$ for every $p\in[0,1]$ . If $c=0$ , then $P(V_p)=I_{\max}(V_p)$ for every $p\in[0,1]$ . Also, if $c>0$ , there exist real $K\ge0$ and $0<\delta\le1$ such that, for every $0<p<\delta$ , with $e_p=\operatorname{rank}J_{N_p}$ and $(J_{N_p})_{(a,b),(a',b')}=N_p(E_{a,a'})_{b,b'}$ , the case $e_p=1$ gives $P(V_p)=I_{\max}(V_p)$ , and otherwise

|P(V_p)-I_{\max}(V_p)| \le3crp^{r-1}(-p\log_2p) +cp^r\left[-3\log_2c+3+\frac3{\ln2} +\log_2(e_p-1)+4\log_2e_p\right]+Kp^{2r}.

Here $E_{a,a'}$ denotes a matrix unit,

I_{\max}(V)=\sup_{\rho\ge0,\ \operatorname{Tr}\rho=1} [H(N(\rho))-H(N^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 satisfying $\sum_jK_j^\dagger K_j=I$ . For an input type $I$ , $\|\Phi\|_\diamond=\sup_{\|X\|_1\le1}\|(\mathrm{id}_I\otimes\Phi)(X)\|_1$ , over all complex matrices on $I\times I$ , where amplification acts on each reference matrix block and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . The number $P(V)$ is the real supremum of nonnegative rates $s$ such that, for every $\eta>0,\xi>0$ , some positive $n_0$ ensures that each $n\ge n_0$ admits $M>0$ density matrices $\rho_m$ on $A^n$ and positive semidefinite measurement matrices $F_j$ on $B^n$ summing to the identity, with $s-\xi\le\log_2M/n$ and $\|\Omega-J_M(\sigma)\|_1<\eta$ , where

(V_n)_{(b,e),a}=\prod_{i=0}^{n-1}V_{(b_i,e_i),a_i}, \quad \Omega_{(m,j,e),(m',j',e')} =\frac{\mathbf1_{m=m'}\mathbf1_{j=j'}}M \sum_{b,c}(F_j)_{c,b}(V_n\rho_mV_n^\dagger)_{(b,e),(c,e')},

\sigma_{e,e'}=\sum_{m,j}\Omega_{(m,j,e),(m,j,e')}, \qquad J_M(\sigma)_{(m,j,e),(m',j',e')} =\frac{\mathbf1_{m=j}\mathbf1_{m'=j'}\mathbf1_{m=m'}}M\,\sigma_{e,e'}.

All displayed real powers use real exponentiation and $\log_2x=\ln x/\ln2$ . No continuity of $V_p$ is required; the positive- $c$ assertion excludes $p=0,\delta$ , and the zero- $c$ assertion 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