Comparison with logarithmic negativity and equality criterion

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.comparisonWithNegativity

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

prove2quantum

Let $\rho$ be any normalized finite-dimensional bipartite state, and write $E_N(\rho)=\log_2\|T_B(\rho)\|_1$ . With $W$ defined by SDP (7) and $E_W=\log_2W$ , one has

E_W(\rho)\le E_N(\rho).

There exists a normalized finite-dimensional state for which the inequality is strict. For each $\rho$ , equality holds exactly when there is a Hermitian matrix $R$ satisfying

\|R\|_\infty\le1,\quad \operatorname{Re}\operatorname{Tr}(T_B(\rho)R)=\|T_B(\rho)\|_1,\quad T_B(R)\ge0.

Thus equality is characterized by a partial-transpose-positive optimizer of (10). Positivity of $R$ itself is not required.

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 4, PDF p.4: universal comparison, possible strict improvement,
and equality exactly when (10) has a Hermitian optimizer whose partial transpose
is positive. Positivity of the optimizer itself is not required. -/
theorem comparisonWithNegativity [Nonempty A] [Nonempty B]
    (rho : Matrix (A × B) (A × B) ℂ) (hrho : IsDensityMatrix rho) :
    entanglementW rho ≤ entanglementN rho ∧
    (∃ a b : ℕ, ∃ sigma : Matrix (Fin (a+1) × Fin (b+1)) (Fin (a+1) × Fin (b+1)) ℂ,
      IsDensityMatrix sigma ∧ entanglementW sigma < entanglementN sigma) ∧
    (entanglementW rho = entanglementN rho ↔
      ∃ R : Matrix (A × B) (A × B) ℂ,
        R.IsHermitian ∧ complexSpectralNorm R ≤ 1 ∧
        effectProb (partialTranspose rho) R = traceNorm (partialTranspose rho) ∧
        (partialTranspose R).PosSemidef) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P83

end

Source

Improved Semidefinite Programming Upper Bound on Distillable Entanglement, arXiv:1601.07940v4, PDF p. 4, Theorem 4: comparison with logarithmic negativity and equality criterion

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\ge0$ be a complex matrix on $A\times B$ with trace $1$ . For a matrix $X$ on any finite bipartite coordinate space, define $X^\Gamma_{(i,j),(i',j')}=X_{(i,j'),(i',j)}$ , $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , and

w(X)=\sup\{\operatorname{Re}\operatorname{tr}(X^\Gamma R): R=R^\dagger,\ \|R\|_{\mathrm{op}}\le1,\ R^\Gamma\ge0\}, \qquad W(X)=\log_2w(X),\qquad N(X)=\log_2\|X^\Gamma\|_1,

where $\|\cdot\|_{\mathrm{op}}$ is the Euclidean operator norm and the supremum uses matrices $R$ on the same space as $X$ . The theorem asserts $W(\rho)\le N(\rho)$ ; it also asserts that there exist natural $a,b$ and a positive semidefinite trace-one matrix $\sigma$ on $\{0,\ldots,a\}\times\{0,\ldots,b\}$ for which $W(\sigma)<N(\sigma)$ . Finally, it asserts the equivalence

W(\rho)=N(\rho) \quad\Longleftrightarrow\quad \exists R,\quad R=R^\dagger,\quad \|R\|_{\mathrm{op}}\le1,\quad \operatorname{Re}\operatorname{tr}(\rho^\Gamma R)=\|\rho^\Gamma\|_1,\quad R^\Gamma\ge0,

where $R$ is a complex matrix indexed by $A\times B$ .

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