Lemma 6: attained maximum separable overlap

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.separableOverlap_maximum

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

prove2quantum

All Hilbert spaces are finite-dimensional complex spaces with fixed product bases and positive local dimensions. States are positive semidefinite operators of trace one; pure kets have norm one. Let $\psi$ be bipartite pure, with largest squared Schmidt coefficient $\lambda_1$ . Let $\mathcal S$ be the separable density matrices on the same register. Then

\operatorname{Tr}(\psi\sigma)\le\lambda_1\quad(\sigma\in\mathcal S),\qquad \exists\sigma_*\in\mathcal S:\operatorname{Tr}(\psi\sigma_*)=\lambda_1.

This records the maximum with attainment, not only a supremum bound.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P19

Formal statement

noncomputable section

open QAlgorithms QAlgorithms.Entanglement Filter

open scoped Matrix ComplexOrder ComplexConjugate ENNReal

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P19

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

open QAlgorithms.Papers.Independent.Information100.P19 (Bip)

open QAlgorithms.Papers.Independent.Information100.P69 (CP)

open QAlgorithms.Papers.Independent.Information100.P71 (supportPower SupportIncluded)

open QAlgorithms.Papers.Independent.Dependency50.P19 (epr)

/-- Lemma 6, PDF pp.10-11, credited to Shimony [28]: the maximum
separable overlap is the largest squared Schmidt coefficient, and is attained. -/
theorem separableOverlap_maximum {a b : ℕ} (ha : 0 < a) (hb : 0 < b)
    (psi : UnitBipartiteKet a b) :
    (∀ sigma : Bip a b, SeparableState sigma →
      (psi.rho * sigma).trace.re ≤ schmidtAt psi.ket 0) ∧
    ∃ sigma : Bip a b, SeparableState sigma ∧
      (psi.rho * sigma).trace.re = schmidtAt psi.ket 0 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 10, Lemma 6

Read-back

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

For every pair of positive natural numbers $a,b$ and every unit vector $\psi\in\mathbb C^a\otimes\mathbb C^b$ , write $P_\psi=|\psi\rangle\langle\psi|$ , and let $\lambda_0$ be the largest eigenvalue of its first marginal, whose entries are $\sum_{j=0}^{b-1}\psi_{ij}\overline{\psi_{i'j}}$ . Every separable density matrix $\sigma$ satisfies $\operatorname{Re}\operatorname{Tr}(P_\psi\sigma)\le\lambda_0$ , and there exists such a $\sigma$ for which equality holds. Here a separable density matrix is a positive semidefinite matrix of trace $1$ that can be expressed as a finite sum $\sum_jw_jA_j\otimes B_j$ , where every $w_j\ge0$ and every $A_j,B_j$ is positive semidefinite of trace $1$ ; the sum of the weights is not separately stipulated in this definition. The assertion includes one-dimensional factors and vectors whose marginal has zero eigenvalues.

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