A lower bound from the actual support projector

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.projectorLowerBound

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

prove2quantum

Let $\rho$ be a positive semidefinite, trace-one bipartite operator on arbitrary nonzero finite-dimensional local spaces, and let $P_\rho$ be the orthogonal projector onto its positive spectral support. The one-copy deterministic PPT rate $E_1$ , defined using positive real target sizes, satisfies

E_1(\rho)\ge-\log_2\|T_B(P_\rho)\|_\infty.

The projector is nonzero, so its partial-transpose norm is positive. The displayed lower bound is not truncated at zero and may be negative.

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]

/-- Consequence of (15), PDF p.5. The projector is constructed from rho;
the lower bound can be negative and is not truncated at zero. -/
theorem projectorLowerBound [Nonempty A] [Nonempty B]
    (rho : Matrix (A × B) (A × B) ℂ) (hrho : IsDensityMatrix rho) :
    -Real.logb 2 (complexSpectralNorm (partialTranspose (supportProjector rho))) ≤ oneCopyExact rho := 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 consequence of (15): support-projector lower bound

Read-back

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

For any finite nonempty types $A,B$ with decidable equality and any complex matrix $\rho$ indexed by $A\times B$ that is positive semidefinite with trace $1$ , let $P_\rho$ be the orthogonal projector onto its range, define $X^\Gamma_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , and let $\|\cdot\|_{\mathrm{op}}$ be the Euclidean operator norm. For real $k$ , let $F_\rho(k)$ be the real supremum of $\operatorname{Re}\operatorname{tr}(\rho Q)$ over matrices satisfying $k>0$ , $0\preceq Q\preceq I$ , and $-k^{-1}I\preceq Q^\Gamma\preceq k^{-1}I$ , where $\preceq$ denotes positive semidefinite difference; let $D(\rho)=\sup\{\log_2 k:k\in\mathbb R,\ k>0,\ F_\rho(k)=1\}$ . Then

-\log_2\|P_\rho^\Gamma\|_{\mathrm{op}}\le D(\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