Theorem 14: depolarizing quantum and private capacities through the leading quadratic-log correction

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.depolarizing_capacities_expansion

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 $D_p(\rho)=(1-p)\rho+\frac p3(X\rho X+Y\rho Y+Z\rho Z)$ and set $b(p)=1-h(p)-p\log_2 3$ , where $h$ is binary entropy in bits. There exist $K_Q,K_P\ge0$ and $0<\delta\le1$ such that for every $0<p<\delta$ ,

b(p)\le Q(D_p)\le b(p)-\frac{16}{9}(6+\sqrt2)p^2\log_2p+K_Qp^2,

b(p)\le P(D_p)\le b(p)-\frac{16}{3}(6+\sqrt2)p^2\log_2p+K_Pp^2.

Both lower and upper bounds are retained. The displayed hashing expression is used only in the low-noise regime.

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)

/-- Theorem 14, PDF p.15: both lower and upper bounds for both operational
capacities, with the factor-three private/quantum leading correction. -/
theorem depolarizing_capacities_expansion :
    ∃ Kq Kp : ℝ, 0 ≤ Kq ∧ 0 ≤ Kp ∧ ∃ delta : ℝ, 0 < delta ∧ delta ≤ 1 ∧
      ∀ p ∈ Set.Ioo 0 delta,
        (depolarizingHashing p ≤ dilationQuantumCapacity (depolarizingDilation p) ∧
          dilationQuantumCapacity (depolarizingDilation p) ≤ depolarizingHashing p -
            (16 / 9 : ℝ) * (6 + Real.sqrt 2) * p ^ 2 * log2 p + Kq * p ^ 2) ∧
        (depolarizingHashing p ≤ fullTracePrivateCapacity (depolarizingDilation p) ∧
          fullTracePrivateCapacity (depolarizingDilation p) ≤ depolarizingHashing p -
            (16 / 3 : ℝ) * (6 + Real.sqrt 2) * p ^ 2 * log2 p + Kp * 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. 15, Theorem 14: depolarizing quantum and private capacities through the leading quadratic-log correction

Read-back

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

For $0<p<1$ , let $V_p:\mathbb C^2\to\mathbb C^2\otimes\mathbb C^4$ have entries $(V_p)_{b,j;a}=\sqrt{w_j(p)}(\sigma_j)_{ba}$ , where $w(p)=(1-p,p/3,p/3,p/3)$ and $(\sigma_0,\sigma_1,\sigma_2,\sigma_3)$ are respectively the identity and the usual Pauli $X,Y,Z$ matrices. Write $N_p(X)=\operatorname{Tr}_{E}(V_pXV_p^\dagger)$ , $\log_2x=\log x/\log2$ , $h_2(p)=[-p\log p-(1-p)\log(1-p)]/\log2$ , and $H(p)=1-h_2(p)-p\log_2 3$ . Define $Q(V_p)$ as the supremum of nonnegative rates $r$ for which there is, for every integer $n\ge0$ , a positive integer $M_n$ and encoding and decoding channels through $N_p^{\otimes n}$ , such that their entanglement transmission fidelities tend to $1$ and, for every $s>0$ , eventually $r-s\le\log_2M_n/n$ . The fidelity is

\operatorname{Re}\operatorname{Tr}\!\left[ |\Phi_{M_n}\rangle\langle\Phi_{M_n}| (\operatorname{id}\otimes\mathrm{Dec}_n\circ N_p^{\otimes n}\circ\mathrm{Enc}_n) (|\Phi_{M_n}\rangle\langle\Phi_{M_n}|)\right], \quad |\Phi_M\rangle=M^{-1/2}\sum_{m=0}^{M-1}|m,m\rangle.

Here and below a channel is a finite Kraus sum with $\sum_jK_j^\dagger K_j=I$ . Define $P(V_p)$ as the supremum of nonnegative rates $r$ such that, for every $\epsilon,s>0$ , all sufficiently large positive $n$ admit $M>0$ , input density matrices $\rho_m$ , and positive semidefinite decoding matrices $F_j$ summing to $I$ , with $r-s\le\log_2M/n$ and

\left\|\Omega-\frac1M\sum_m|m,m\rangle\langle m,m|\otimes\Omega_E\right\|_1<\epsilon, \quad \Omega=\frac1M\sum_{m,j}|m,j\rangle\langle m,j| \otimes\operatorname{Tr}_{B^n}\!\left[(F_j\otimes I)V_p^{\otimes n}\rho_m(V_p^{\otimes n})^\dagger\right], \quad \Omega_E=\operatorname{Tr}_{m,j}\Omega .

A density matrix is positive semidefinite with trace $1$ , and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ ; the private error uses this full trace norm. There exist real $K_q,K_p\ge0$ and $0<\delta\le1$ such that every $0<p<\delta$ satisfies

H(p)\le Q(V_p)\le H(p)-\frac{16}{9}(6+\sqrt2)p^2\log_2p+K_qp^2, \qquad H(p)\le P(V_p)\le H(p)-\frac{16}{3}(6+\sqrt2)p^2\log_2p+K_pp^2.

The quantum code sequence includes a zeroth block, although its limiting rate condition concerns large $n$ ; real division by zero at that block is interpreted as $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