The SDP measure bounds PPT distillable entanglement

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.upperBound

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

prove2quantum

Let $\rho$ be a positive semidefinite, trace-one operator on arbitrary nonzero finite-dimensional complex spaces $A\otimes B$ . Partial transpose $T_B$ is taken in a fixed product basis. For $k>0$ , let $F_\Gamma(\rho,k)$ be the maximum of $\operatorname{Re}\operatorname{Tr}(\rho Q)$ subject to $0\le Q\le I$ and $-I/k\le T_B(Q)\le I/k$ . Define $E_\Gamma(\rho)$ as the supremum of real rates $r$ for which $F_\Gamma(\rho^{\otimes n},2^{nr})\to1$ . Define $W(\rho)$ by SDP (7), maximizing $\operatorname{Re}\operatorname{Tr}(T_B(\rho)R)$ over Hermitian $R$ with $\|R\|_\infty\le1$ and $T_B(R)\ge0$ , and put $E_W(\rho)=\log_2W(\rho)$ . Then every achievable rate $r$ satisfies $r\le E_W(\rho)$ , and

E_\Gamma(\rho)\le E_W(\rho).

This gives an upper bound on vanishing-error PPT distillation without assuming that its supremum rate is achieved.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P83

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P83

open QAlgorithms.Papers.Independent.Support50.P11 (Loewner)

open QAlgorithms.Papers.Independent.Dependency50.P32 (partialTranspose)

open QAlgorithms.Papers.Independent.Information100.P34 (supportProjector)

variable {A B C D : Type*}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

/-- Theorem 1, PDF p.3: every achievable rate, hence its supremum, is bounded
by E_W. There is no assumption that E_Gamma itself is achievable. -/
theorem upperBound [Nonempty A] [Nonempty B]
    (rho : Matrix (A × B) (A × B) ℂ) (hrho : IsDensityMatrix rho) :
    (∀ r : ℝ, PPTAchievableRate rho r → r ≤ entanglementW rho) ∧
      entanglementGamma rho ≤ entanglementW rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P83

end

Source

Improved Semidefinite Programming Upper Bound on Distillable Entanglement, arXiv:1601.07940v4, PDF p. 3, Theorem 1; abstract seed: the new upper bound

Read-back

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

Let $A,B$ be finite nonempty types with decidable equality, and let $\rho$ be a complex matrix indexed by $A\times B$ that is positive semidefinite and has trace $1$ . For a matrix $X$ on this space, write $X^\Gamma_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , let $\|\cdot\|_{\mathrm{op}}$ be the operator norm induced by the Euclidean norm, and write $X\le Y$ when $Y-X$ is positive semidefinite. Define

w(\rho)=\sup_{\substack{R=R^\dagger,\ \|R\|_{\mathrm{op}}\le1\\R^\Gamma\ge0}} \operatorname{Re}\operatorname{tr}(\rho^\Gamma R), \qquad W(\rho)=\log_2 w(\rho),

and, for real $k$ , define

F(\rho,k)= \sup_{\substack{k>0,\ 0\le Q\le I\\-k^{-1}I\le Q^\Gamma\le k^{-1}I}} \operatorname{Re}\operatorname{tr}(\rho Q).

Here the supremum defining $F$ is over matrices $Q$ , with the displayed condition $k>0$ part of feasibility. For each natural $n$ , let $\rho^{[n]}$ have entries $\rho^{[n]}_{(x,y),(x',y')}=\prod_{i=0}^{n-1}\rho_{(x_i,y_i),(x'_i,y'_i)}$ , indexed by $A^n\times B^n$ . A real rate $r$ is called achievable here precisely when $F(\rho^{[n]},2^{nr})\to1$ as $n\to\infty$ , and put $\Gamma(\rho)=\sup\{r\in\mathbb R:r\text{ is achievable}\}$ . The theorem asserts both that every such real $r$ satisfies $r\le W(\rho)$ and that $\Gamma(\rho)\le W(\rho)$ . Achievability imposes no separate condition $r\ge0$ , and the sequence includes $n=0$ , whose matrix is the one-dimensional matrix with entry $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