The measure E_W is not convex

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.nonconvexity

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

prove2quantum

There exist nonzero finite local dimensions, normalized bipartite states $\rho,\sigma$ on the same product space, and a real parameter $0<p<1$ for which

E_W\bigl(p\rho+(1-p)\sigma\bigr)>pE_W(\rho)+(1-p)E_W(\sigma).

Here $E_W$ is the base-two logarithm of SDP (7). This existential violation of convexity is compatible with the monotonicity on average established in Theorem 3.

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]

/-- Unnumbered nonconvexity assertion following Theorem 3, PDF p.3.
The violating pair and mixing parameter exist; no violation is assumed. -/
theorem nonconvexity :
    ∃ a b : ℕ, ∃ rho sigma : Matrix (Fin (a+1) × Fin (b+1)) (Fin (a+1) × Fin (b+1)) ℂ,
    IsDensityMatrix rho ∧ IsDensityMatrix sigma ∧
    ∃ p : ℝ, 0 < p ∧ p < 1 ∧
    p * entanglementW rho + (1-p) * entanglementW sigma <
      entanglementW ((p : ℂ) • rho + ((1-p : ℝ) : ℂ) • sigma) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P83

end

Source

Improved Semidefinite Programming Upper Bound on Distillable Entanglement, arXiv:1601.07940v4, PDF p. 3, Unnumbered result following Theorem 3: nonconvexity

Read-back

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

There exist natural numbers $a,b$ , positive semidefinite complex matrices $\rho,\sigma$ of trace $1$ indexed by $\{0,\ldots,a\}\times\{0,\ldots,b\}$ , and a real number $p$ with $0<p<1$ , such that

pW(\rho)+(1-p)W(\sigma) < W\bigl(p\rho+(1-p)\sigma\bigr).

Here, for every matrix $X$ on this bipartite space,

W(X)=\log_2\sup\{\operatorname{Re}\operatorname{tr}(X^\Gamma R): R=R^\dagger,\ \|R\|_{\mathrm{op}}\le1,\ R^\Gamma\ge0\}, \qquad X^\Gamma_{(i,j),(i',j')}=X_{(i,j'),(i',j)},

and $\|\cdot\|_{\mathrm{op}}$ is the Euclidean operator norm. The local dimensions are $a+1$ and $b+1$ , so dimension $1$ is included among the existentially quantified possibilities.

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