Definitions for Continuity of Relative Entropy of Entanglement

Definition

QAlgorithms_Papers_Independent_Intakethird100_P100

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

prove2quantum

The objects the formalized statements of Continuity of Relative Entropy of Entanglement (arXiv:quant-ph/9910002) are stated in. Each was checked against the paper by a blind read-back and a moderator.

separableStates: PDF pp.1–2, Remark (i): exactly the normalized separable states, using the accepted finite convex-combination definition.
pptStates: PDF p.2, Remark (i): trace-one positive states with positive partial transpose. This is the normalized PPT optimization specified by the paper.
pptEntanglement: PDF pp.1–2, Remark (i): the infimum over normalized PPT states, in bits to match the frozen relativeEntanglement interface. Bounds convert to nats. The support-aware entropy retains infinity before the infimum is taken.

Definition code

import Mathlib
import Definitions.Def_QAlgorithms_Defs_ExtendedQuantumEntropy
import Definitions.Def_QAlgorithms_Defs_BipartiteSeparability
import Definitions.Def_QAlgorithms_Papers_Independent_Dependency50_P15

/-!
Donald and Horodecki, arXiv:quant-ph/9910002v1, PDF pp.1–3.
Full trace norm throughout. The frozen entropy and distance interfaces below
use bits. Each quantitative real difference is explicitly multiplied by ln 2,
so the displayed bounds use nats exactly as in the chosen source convention.
Frozen relativeDistance is EReal-valued and supports unnormalized operators;
our feasible sets contain only normalized states. Nonnegativity and finiteness
are conclusions, not premises. The frozen normalized relativeEntanglement is
ENNReal-valued. Attainment is invariant under the positive conversion ln 2.
The accepted groupedTensorPower keeps the bipartition A^n:B^n.
-/

noncomputable section

open Filter
open scoped ENNReal Topology ComplexOrder

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P100

open QAlgorithms.Papers.Independent.Dependency50.P15
  (relativeDistance relativeDistanceValue positiveOperatorRelativeEntropyBits groupedTensorPower)
open QAlgorithms.Papers.Independent.Information100.P54
  (relativeEntropyBits relativeEntanglement)

/-- PDF pp.1–2, Remark (i): exactly the normalized separable states,
using the accepted finite convex-combination definition. -/
def separableStates {A B : Type*} [Fintype A] [Fintype B]
    [Nonempty A] [Nonempty B] : Set (Matrix (A × B) (A × B) ℂ) :=
  {rho | QAlgorithms.Entanglement.IsSeparableDensity rho}

/-- PDF p.2, Remark (i): trace-one positive states with positive partial
transpose. This is the normalized PPT optimization specified by the paper. -/
def pptStates {A B : Type*} [Fintype A] [Fintype B] :
    Set (Matrix (A × B) (A × B) ℂ) :=
  {rho | IsDensityMatrix rho ∧
    (QAlgorithms.Entanglement.partialTransposeFirst rho).PosSemidef}

/-- PDF pp.1–2, Remark (i): the infimum over normalized PPT states, in
bits to match the frozen relativeEntanglement interface. Bounds convert to nats.
The support-aware entropy retains infinity before the infimum is taken. -/
def pptEntanglement {A B : Type*} [Fintype A] [Fintype B]
    [DecidableEq A] [DecidableEq B]
    (sigma : Matrix (A × B) (A × B) ℂ) : ℝ≥0∞ :=
  sInf (relativeEntropyBits sigma '' pptStates)

/-- Sanity check, PDF p.1: the reused eta vanishes at zero and one. -/
example : Real.negMulLog 0 = 0 ∧ Real.negMulLog 1 = 0 := by simp

/-- Sanity check, PDF p.2: the frozen extended empty infimum is infinity. -/
example {I : Type*} [Fintype I] [DecidableEq I] (sigma : Matrix I I ℂ) :
    relativeDistance ∅ sigma = ⊤ := by simp [relativeDistance]

/-- Sanity check, PDF pp.1–2: separability membership is the accepted predicate. -/
example {A B : Type*} [Fintype A] [Fintype B] [Nonempty A] [Nonempty B]
    (rho : Matrix (A × B) (A × B) ℂ) :
    rho ∈ separableStates ↔ QAlgorithms.Entanglement.IsSeparableDensity rho := Iff.rfl

/-- Sanity check, PDF p.2: the zero scalar matrix is excluded by normalization. -/
example : (0 : Matrix (Fin 1 × Fin 1) (Fin 1 × Fin 1) ℂ) ∉ pptStates := by
  simp [pptStates, IsDensityMatrix]

/-- Sanity check, PDF p.2: the local PPT infimum uses exactly the PPT feasible image. -/
example {A B : Type*} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
    (sigma : Matrix (A × B) (A × B) ℂ) :
    pptEntanglement sigma = sInf (relativeEntropyBits sigma '' pptStates) := rfl

end QAlgorithms.Papers.Independent.Intakethird100.P100

Source

Continuity of Relative Entropy of Entanglement, arXiv:quant-ph/9910002v1, https://arxiv.org/abs/quant-ph/9910002v1

Read-back

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

`QAlgorithms.Papers.Independent.Intakethird100.P100.pptEntanglement`

For any finite types $A,B$ with decidable equality and any complex matrix $\sigma$ on $A\times B$ , this defines an extended nonnegative real number

E_{\mathrm{PPT}}(\sigma)=\inf_{\tau\in\mathcal P}R(\sigma\Vert\tau),

where $\mathcal P$ consists of matrices $\tau\succeq0$ with $\operatorname{tr}\tau=1$ and $\tau^{T_A}\succeq0$ , with $(\tau^{T_A})_{(a,b),(a',b')}=\tau_{(a',b),(a,b')}$ . The quantity being minimized is

R(X\Vert Y)= \begin{cases} \dfrac{\max\!\left\{\operatorname{Re}\operatorname{tr} \bigl(f(X)-X\log Y\bigr),0\right\}}{\ln2}, & X,Y\succeq0,\ \operatorname{tr}X=\operatorname{tr}Y=1,\ \ker Y\subseteq\ker X,\\[4pt] +\infty,&\text{otherwise}, \end{cases} \qquad f(x)=x\ln x.

The matrix functions use functional calculus, with $\ln0=0$ and $f(0)=0$ . No density or nonemptiness hypothesis is imposed on $\sigma,A,B$ : a $\sigma$ that is not a density matrix gives value $+\infty$ , and an empty comparison set also has infimum $+\infty$ .

`QAlgorithms.Papers.Independent.Intakethird100.P100.pptStates`

For any finite types $A$ and $B$ , this defines the set of complex matrices $\rho$ indexed by $A\times B$ such that $\rho$ is positive semidefinite, $\operatorname{tr}\rho=1$ , and the matrix $\rho^{T_A}$ defined by

(\rho^{T_A})_{(a,b),(a',b')}=\rho_{(a',b),(a,b')}

is positive semidefinite. Nonemptiness of $A$ and $B$ is not assumed; if either is empty, every matrix on $A\times B$ has trace $0$ , so the defined set is empty.

`QAlgorithms.Papers.Independent.Intakethird100.P100.separableStates`

For any finite, nonempty types $A$ and $B$ , this defines the set of complex matrices $\rho$ indexed by $A\times B$ for which there exist a natural number $q$ , real weights $w_j$ , and matrices $R_j$ on $A$ and $S_j$ on $B$ , indexed by $0\le j<q$ , such that

w_j\ge0,\qquad \sum_{j<q}w_j=1,\qquad R_j\succeq0,\quad \operatorname{tr}R_j=1,\qquad S_j\succeq0,\quad \operatorname{tr}S_j=1,\qquad \rho=\sum_{j<q}w_j(R_j\otimes S_j).

Here $\succeq0$ means positive semidefinite, and the tensor product has entries $(R_j\otimes S_j)_{(a,b),(a',b')}=(R_j)_{a,a'}(S_j)_{b,b'}$ . Although $q=0$ is among the quantified natural numbers, it cannot satisfy the requirement that the weights sum to $1$ ; individual weights may be zero.

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