Unnumbered after Eq. (5): convexity and separable inclusion of D(epsilon)

Open

QAlgorithms.Papers.Independent.Intakethird100.P09.nearSep_convex_and_contains

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

prove2quantum

All states are normalized finite-dimensional bipartite density matrices. Gamma denotes transposition of Bob in the fixed product basis. The trace norm is the full trace norm. For a finite Bell expression S with real coefficients, C(S) and Q(S) are its largest signed classical value and its supremal signed quantum value over arbitrary finite local dimensions; Q_S(rho) optimizes complete local POVMs on the fixed state. Fix a positive local dimension d and epsilon>0. Define

D(\epsilon)=\{\rho:\rho\text{ is a density matrix and }\exists\sigma\in\mathrm{SEP},\ \|\rho^\Gamma-\sigma^\Gamma\|_1\le\epsilon\}.

Then D(epsilon) is convex over the reals and contains SEP. An actual same-dimensional separable witness is required, including on the boundary. These sets organize the single-copy bounds.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P09

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P09

open scoped Matrix ComplexConjugate ComplexOrder ENNReal

open Filter

open QAlgorithms.Entanglement (IsSeparableDensity)

open QAlgorithms.Papers.Independent.Dependency50.P24
  (transposeSecond partyCut xForm swapPrivate hidingOne hidingTwo)

open QAlgorithms.Papers.Independent.Dependency50.P42 (dimensionedPower)

open QAlgorithms.Papers.Independent.Information100.P21 (Op FiniteLOCC)

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Advance50.P47 (Box)

open QAlgorithms.Papers.Independent.Information100.P54 (relativeEntanglement)

attribute [local instance] Classical.propDecidable

attribute [local instance] Classical.decEq

/-- PDF p.2, following Eq.(5): D(epsilon) is convex and contains every separable density. -/
theorem nearSep_convex_and_contains (d : ℕ+) (epsilon : ℝ) (hepsilon : 0 < epsilon) :
    Convex ℝ (nearSep (I := Fin d) (J := Fin d) epsilon) ∧
    {rho : Op (Fin d × Fin d) | IsSeparableDensity rho} ⊆ nearSep epsilon := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P09

end

Source

Bounds on quantum nonlocality via partial transposition, arXiv:1407.6999v3, PDF p. 2, Unnumbered after Eq. (5): convexity and separable inclusion of D(epsilon)

Read-back

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

For every positive integer $d$ and every real $\epsilon>0$ , let $\mathcal N_\epsilon$ consist of all positive semidefinite trace- $1$ matrices $\rho$ on $\mathbb C^d\otimes\mathbb C^d$ for which there exists a matrix $\tau=\sum_jw_jA_j\otimes B_j$ , with finitely many terms, nonnegative real weights summing to $1$ , and positive semidefinite trace- $1$ local matrices $A_j,B_j$ , such that $\|T_2(\rho)-T_2(\tau)\|_1\le\epsilon$ . Here $T_2(Z)_{(i,j),(k,l)}=Z_{(i,l),(k,j)}$ , and $\|Z\|_1=\operatorname{Re}\operatorname{tr}\sqrt{Z^\dagger Z}$ . Then $\mathcal N_\epsilon$ is convex over $\mathbb R$ , meaning that $t\rho+(1-t)\sigma\in\mathcal N_\epsilon$ whenever $\rho,\sigma\in\mathcal N_\epsilon$ and $0\le t\le1$ , and every matrix admitting the stated finite separable decomposition belongs to $\mathcal N_\epsilon$ . This includes $d=1$ ; the hypothesis requires strictly positive $\epsilon$ .

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