Continuity of the normalized PPT relative-entropy infimum

Open

QAlgorithms.Papers.Independent.Intakethird100.P100.pptEntanglement_continuity

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

prove2quantum

Let $H_A,H_B$ have positive finite dimensions and set $N=\dim(H_A\otimes H_B)$ . Let $\mathrm{PPT}$ be exactly the trace-one positive semidefinite bipartite matrices whose partial transpose is positive semidefinite. Define $E_{\mathrm{PPT}}(\omega)=\inf_{\tau\in\mathrm{PPT}}S(\omega\Vert\tau)$ , retaining infinity at a support violation.

All logarithms are natural. States are positive semidefinite matrices of trace one, and the distance $t=\|\sigma-\rho\|_1$ uses the full trace norm, without a factor of one half. Set $\eta(t)=-t\log t$ , with $\eta(0)=0$ .

For arbitrary bipartite density matrices $\sigma,\rho$ with $t\leq 1/3$ , both infima are finite and

|E_{\mathrm{PPT}}(\sigma)-E_{\mathrm{PPT}}(\rho)|\leq 2\bigl(t\log N+\eta(t)\bigr)+4t.

This is the paper's normalized PPT variation. Neither input is required to be PPT.

Formalization Note The accepted entropy infimum is stored in bits. The Lean bound multiplies its absolute real difference by $\log 2$ , which gives exactly the natural-logarithm quantity displayed above.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P100

Formal statement

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)

/-- Remark (i), PDF p.2, and introduction, PDF p.1: the identical bound (3)
for minimization over normalized PPT states, with arbitrary density inputs. -/
theorem pptEntanglement_continuity
    {A B : Type*} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
    [Nonempty A] [Nonempty B]
    (sigma rho : Matrix (A × B) (A × B) ℂ)
    (hsigma : IsDensityMatrix sigma) (hrho : IsDensityMatrix rho)
    (hclose : traceNorm (sigma - rho) ≤ 1 / 3) :
    pptEntanglement sigma < ⊤ ∧ pptEntanglement rho < ⊤ ∧
    Real.log 2 * |(pptEntanglement sigma).toReal -
      (pptEntanglement rho).toReal| ≤
      2 * (traceNorm (sigma - rho) * Real.log (Fintype.card (A × B)) +
        Real.negMulLog (traceNorm (sigma - rho))) + 4 * traceNorm (sigma - rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P100

end

Source

Continuity of Relative Entropy of Entanglement, arXiv:quant-ph/9910002v1, PDF p. 2, Remark (i), with the introductory variation on p.1

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 density matrices $\sigma,\rho$ on $A\times B$ , meaning positive semidefinite matrices with trace $1$ , put $d=|A\times B|$ and $t=\operatorname{Re}\operatorname{tr}\sqrt{(\sigma-\rho)^\dagger(\sigma-\rho)}$ . If $t\le1/3$ , then

E_{\mathrm{PPT}}(\sigma)<+\infty,\qquad E_{\mathrm{PPT}}(\rho)<+\infty,\qquad (\ln2)\left|E_{\mathrm{PPT}}(\sigma)_{\mathbb R} -E_{\mathrm{PPT}}(\rho)_{\mathbb R}\right| \le2\bigl(t\ln d-t\ln t\bigr)+4t.

Here $E_{\mathrm{PPT}}(X)=\inf_{Y\in\mathcal P}R(X\Vert Y)$ in the extended nonnegative reals, where $\mathcal P$ consists of density matrices $Y$ for which the matrix with entries $Y^{T_A}_{(a,b),(a',b')}=Y_{(a',b),(a,b')}$ is positive semidefinite. For density matrices $X,Y$ , the minimized quantity is $\max\{\operatorname{Re}\operatorname{tr}(f(X)-X\log Y),0\}/\ln2$ if $\ker Y\subseteq\ker X$ , and $+\infty$ otherwise; it is also $+\infty$ if either argument is not a density matrix. Here $f(x)=x\ln x$ , and matrix functions use functional calculus with $\ln0=0$ . The subscript $\mathbb R$ denotes conversion to a real number, sending $+\infty$ to $0$ , though the conclusion asserts finiteness. The cases $t=0$ and $d=1$ are included, with $t\ln t=0$ at 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