Quantitative continuity of relative entropy of entanglement

Open

QAlgorithms.Papers.Independent.Intakethird100.P100.relativeEntanglement_continuity

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

prove2quantum

Let $H_A,H_B$ be fixed complex Hilbert spaces of positive finite dimensions, and let $N=\dim(H_A\otimes H_B)$ . For a bipartite state $\omega$ , define $E_r(\omega)=\inf_{\tau\in\mathrm{SEP}}S(\omega\Vert\tau)$ , where $\mathrm{SEP}$ consists exactly of finite convex combinations of product density matrices and $S$ is Umegaki relative entropy, infinite when support inclusion fails.

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 any states $\sigma,\rho$ with $t\leq 1/3$ , both entanglement values are finite and

|E_r(\sigma)-E_r(\rho)|\leq 2\bigl(t\log N+\eta(t)\bigr)+4t.

This is the precise separable-state specialization of the paper's Fannes-type continuity requirement. No separability assumption is imposed on either input.

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)

/-- Introduction (2), PDF p.1, specialized via Remark (i), PDF p.2:
relative entropy of entanglement obeys the exact quantitative bound (3).
The local domain t <= 1/3 is retained. No separability of the inputs is assumed. -/
theorem relativeEntanglement_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) :
    relativeEntanglement sigma < ⊤ ∧ relativeEntanglement rho < ⊤ ∧
    Real.log 2 * |(relativeEntanglement sigma).toReal -
      (relativeEntanglement 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. 1, Introduction (2); specialization of (3) through Remark (i), p.2

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 any positive semidefinite complex matrices $\sigma,\rho$ on $A\times B$ having 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{sep}}(\sigma)<+\infty$ , $E_{\mathrm{sep}}(\rho)<+\infty$ , and

(\ln2)\left|E_{\mathrm{sep}}(\sigma)_{\mathbb R} -E_{\mathrm{sep}}(\rho)_{\mathbb R}\right| \le 2\bigl(t\ln d-t\ln t\bigr)+4t.

Here $E_{\mathrm{sep}}(X)$ is the infimum, in the extended nonnegative reals, of $R(X\Vert Y)$ over all finite mixtures $Y=\sum_{j<q}w_j(R_j\otimes S_j)$ , where $q\in\mathbb N$ , $w_j\ge0$ , $\sum_jw_j=1$ , and each $R_j,S_j$ is positive semidefinite with trace $1$ on $A,B$ , respectively. For density matrices $X,Y$ , $R(X\Vert Y)$ equals $\max\{\operatorname{Re}\operatorname{tr}(f(X)-X\log Y),0\}/\ln2$ when $\ker Y\subseteq\ker X$ , and equals $+\infty$ otherwise, where $f(x)=x\ln x$ ; outside density matrices it is also $+\infty$ . Matrix functions use functional calculus with $\ln0=0$ . The subscript $\mathbb R$ denotes conversion from extended nonnegative reals to reals, which sends $+\infty$ to $0$ , although finiteness is asserted here. The case $t=0$ is included, with $t\ln t=0$ , and $d=1$ is allowed.

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