Three attained SDP characterizations of W

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.sdpDuality

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

prove2quantum

Let $\rho$ be any normalized bipartite state on nonzero finite-dimensional spaces, and let $T_B$ denote ordinary partial transpose on Bob. All operator inequalities are Loewner inequalities, $\|\cdot\|_\infty$ is the largest singular value, and $\|\cdot\|_1$ is the trace norm. The following three optimization problems have the same value and each attains its optimum:

\begin{aligned}W(\rho)&=\max_{R=R^\dagger}\{\operatorname{Re}\operatorname{Tr}(T_B(\rho)R):\|R\|_\infty\le1,\ T_B(R)\ge0\}\\&=\min_{U,V\ge0}\{\operatorname{Re}\operatorname{Tr}(U+V):T_B(U-V)\ge\rho\}\\&=\min_{X\ge\rho}\|T_B(X)\|_1.\end{aligned}

These are explicit finite-dimensional SDPs. The first witness need not be positive, and the last variable is not constrained to have trace one.

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]

/-- Strong duality and attained equivalent SDPs (7)–(9), PDF p.2.
R need not be positive and X need not have trace one. -/
theorem sdpDuality [Nonempty A] [Nonempty B]
    (rho : Matrix (A × B) (A × B) ℂ) (hrho : IsDensityMatrix rho) :
    wValue rho = dualUVValue rho ∧ wValue rho = dualXValue rho ∧
    (∃ R, WFeasible R ∧ effectProb (partialTranspose rho) R = wValue rho) ∧
    (∃ U V, DualUVFeasible rho U V ∧ (U + V).trace.re = dualUVValue rho) ∧
    (∃ X, Loewner rho X ∧ traceNorm (partialTranspose X) = dualXValue rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P83

end

Source

Improved Semidefinite Programming Upper Bound on Distillable Entanglement, arXiv:1601.07940v4, PDF p. 2, Unnumbered result: equivalent attained SDPs (7)–(9)

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 positive semidefinite complex matrix indexed by $A\times B$ , with trace $1$ . Write $X^\Gamma_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , $X\le Y$ for positive semidefiniteness of $Y-X$ , $\|X\|_{\mathrm{op}}$ for the Euclidean operator norm, and $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ . Define the following real optimization values:

\begin{aligned} w(\rho)&=\sup\{\operatorname{Re}\operatorname{tr}(\rho^\Gamma R): R=R^\dagger,\ \|R\|_{\mathrm{op}}\le1,\ R^\Gamma\ge0\},\\ d_{UV}(\rho)&=\inf\{\operatorname{Re}\operatorname{tr}(U+V): U\ge0,\ V\ge0,\ \rho\le(U-V)^\Gamma\},\\ d_X(\rho)&=\inf\{\|X^\Gamma\|_1:\rho\le X\}. \end{aligned}

All optimization matrices have the same indices as $\rho$ . The theorem asserts $w(\rho)=d_{UV}(\rho)=d_X(\rho)$ , and asserts attainment in all three problems: there exists a feasible $R$ with $\operatorname{Re}\operatorname{tr}(\rho^\Gamma R)=w(\rho)$ , there exist feasible $U,V$ with $\operatorname{Re}\operatorname{tr}(U+V)=d_{UV}(\rho)$ , and there exists $X$ with $X-\rho\ge0$ and $\|X^\Gamma\|_1=d_X(\rho)$ .

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