Attained one-copy deterministic SDP characterizations

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.deterministicSDPs

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

prove2quantum

Let $\rho$ be a normalized state on arbitrary nonzero finite-dimensional local spaces, let $P_\rho$ be its orthogonal support projector, and let $F_\Gamma$ be the positive-real-target SDP (3). Independently define $E_1(\rho)=\sup\{\log_2 k:k>0,\ F_\Gamma(\rho,k)=1\}$ . Define

\begin{aligned}W_0(\rho)&=\max_R\{\operatorname{Re}\operatorname{Tr}(\rho R):0\le R\le (\operatorname{Re}\operatorname{Tr}(\rho R))I,\ -I\le T_B(R)\le I\},\\m(\rho)&=\min_{P_\rho\le R\le I}\|T_B(R)\|_\infty.\end{aligned}

Both extrema are attained, $W_0(\rho)\ge1$ , $m(\rho)>0$ , and

E_1(\rho)=\log_2W_0(\rho)=-\log_2m(\rho).

The defining supremum for $E_1$ is also attained at some positive real $k$ . This is equivalent to (15), maximizing the negative logarithm over the support interval; the norm minimization itself is the SDP.

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]

/-- Eqs. (14)–(15), PDF p.5, using the independent F_Gamma definition of
oneCopyExact on p.4. Both SDP optima and the positive-real target size are attained;
the norm is minimized before applying the negative logarithm. -/
theorem deterministicSDPs [Nonempty A] [Nonempty B]
    (rho : Matrix (A × B) (A × B) ℂ) (hrho : IsDensityMatrix rho) :
    oneCopyExact rho = Real.logb 2 (wZeroValue rho) ∧
    oneCopyExact rho = -Real.logb 2 (supportNormMinimum rho) ∧
    1 ≤ wZeroValue rho ∧ 0 < supportNormMinimum rho ∧
    (∃ R, WZeroFeasible rho R ∧ effectProb rho R = wZeroValue rho) ∧
    (∃ R, Loewner (supportProjector rho) R ∧ Loewner R 1 ∧
      complexSpectralNorm (partialTranspose R) = supportNormMinimum rho) ∧
    (∃ k : ℝ, 0 < k ∧ pptDistillationFidelity rho k = 1 ∧ oneCopyExact rho = Real.logb 2 k) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P83

end

Source

Improved Semidefinite Programming Upper Bound on Distillable Entanglement, arXiv:1601.07940v4, PDF p. 5, Unnumbered main result: one-copy deterministic SDPs (14)–(15)

Read-back

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

For any finite nonempty types $A,B$ , each equipped with decidable equality, and any complex matrix $\rho$ indexed by $A\times B$ that is positive semidefinite with trace $1$ , write $X^\Gamma_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , let $P_\rho$ be the orthogonal projector onto the range of $\rho$ , and let $\|\cdot\|_{\mathrm{op}}$ denote the Euclidean operator norm. Write $X\preceq Y$ when $Y-X$ is positive semidefinite. Define

F_\rho(k)=\sup\{\operatorname{Re}\operatorname{tr}(\rho Q):k>0,\ 0\preceq Q\preceq I,\ -k^{-1}I\preceq Q^\Gamma\preceq k^{-1}I\},\qquad D(\rho)=\sup\{\log_2 k:k>0,\ F_\rho(k)=1\},

where $k$ is real, not required to be an integer. Define $w_0(\rho)$ as the supremum of $\operatorname{Re}\operatorname{tr}(\rho R)$ over matrices $R$ satisfying $R\succeq0$ , $R\preceq\operatorname{Re}\operatorname{tr}(\rho R)\,I$ , and $-I\preceq R^\Gamma\preceq I$ ; define $s(\rho)=\inf\{\|R^\Gamma\|_{\mathrm{op}}:P_\rho\preceq R\preceq I\}$ . All these extrema are real-valued suprema or infima. Then

D(\rho)=\log_2 w_0(\rho)=-\log_2 s(\rho),\qquad 1\le w_0(\rho),\qquad 0<s(\rho).

There exists an $R$ satisfying the displayed constraints defining $w_0(\rho)$ and attaining $\operatorname{Re}\operatorname{tr}(\rho R)=w_0(\rho)$ ; there exists, possibly separately, an $R$ with $P_\rho\preceq R\preceq I$ attaining $\|R^\Gamma\|_{\mathrm{op}}=s(\rho)$ ; and there exists a real $k>0$ such that $F_\rho(k)=1$ and $D(\rho)=\log_2 k$ .

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