Asymptotic continuity of entanglement per pair

Open

QAlgorithms.Papers.Independent.Intakethird100.P100.entanglement_perPair_asymptotic_continuity

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

prove2quantum

Fix a density matrix $\rho'$ on a positive finite-dimensional bipartite space $H_A\otimes H_B$ . For every integer $n\geq1$ , let $\omega_n$ be any density matrix on $H_A^{\otimes n}\otimes H_B^{\otimes n}$ . Group all Alice factors and all Bob factors when forming the tensor power $(\rho')^{\otimes n}$ . Let $E$ denote either the relative entropy of entanglement or the infimum of relative entropy over normalized PPT states, always across this grouped bipartition and using natural logarithms. If the full trace distance tends to zero, then, for both choices of $E$ ,

\bigl\|(\rho')^{\otimes n}-\omega_n\bigr\|_1\longrightarrow0 \quad\Longrightarrow\quad \frac1n\left|E\bigl((\rho')^{\otimes n}\bigr)-E(\omega_n)\right|\longrightarrow0.

The fixed target may be mixed, and the approximants may have arbitrary correlations. This expresses continuity of entanglement per pair in the many-copy limit.

Formalization Note The sequence is indexed by $n=k+1$ to keep every denominator positive. Both entropic infima are finite in every finite-copy space. The accepted infima are stored in bits; the Lean per-copy expression includes the factor $\log 2$ to express the displayed natural-logarithm convention.

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 (1), PDF p.1, including the PPT variation asserted there:
trace-norm approximation of a fixed tensor-power target gives vanishing
entanglement difference per pair. Positive copy counts k+1 remove division
by zero. The approximants can be correlated and the fixed target can be mixed. -/
theorem entanglement_perPair_asymptotic_continuity
    {A B : Type*} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
    [Nonempty A] [Nonempty B]
    (rhoPrime : Matrix (A × B) (A × B) ℂ)
    (hrhoPrime : IsDensityMatrix rhoPrime)
    (approx : (k : ℕ) →
      Matrix ((Fin (k + 1) → A) × (Fin (k + 1) → B))
        ((Fin (k + 1) → A) × (Fin (k + 1) → B)) ℂ)
    (happrox : ∀ k, IsDensityMatrix (approx k))
    (hclose : Tendsto
      (fun k : ℕ => traceNorm (groupedTensorPower rhoPrime (k + 1) - approx k))
      atTop (nhds 0)) :
    Tendsto (fun k : ℕ => (1 / ((k : ℝ) + 1)) * Real.log 2 *
      |(relativeEntanglement (groupedTensorPower rhoPrime (k + 1))).toReal -
        (relativeEntanglement (approx k)).toReal|) atTop (nhds 0) ∧
    Tendsto (fun k : ℕ => (1 / ((k : ℝ) + 1)) * Real.log 2 *
      |(pptEntanglement (groupedTensorPower rhoPrime (k + 1))).toReal -
        (pptEntanglement (approx k)).toReal|) atTop (nhds 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P100

end

Source

Continuity of Relative Entropy of Entanglement, arXiv:quant-ph/9910002v1, PDF p. 1, Introduction, equation (1), and the PPT variation

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, let $\rho'$ be a positive semidefinite complex matrix of trace $1$ on $A\times B$ , and let $\tau_k$ , for every $k\in\mathbb N$ , be a positive semidefinite matrix of trace $1$ on $A^{k+1}\times B^{k+1}$ , where $A^r$ means functions from $\{0,\ldots,r-1\}$ to $A$ , and similarly for $B$ . Define the matrix $G_r$ on $A^r\times B^r$ by

(G_r)_{(a,b),(a',b')}=\prod_{i=0}^{r-1}\rho'_{(a_i,b_i),(a'_i,b'_i)}, \qquad \|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}.

If $\|G_{k+1}-\tau_k\|_1\to0$ as $k\to\infty$ , then both limits hold:

\frac{\ln2}{k+1} \left|E_{\mathrm{sep}}(G_{k+1})_{\mathbb R} -E_{\mathrm{sep}}(\tau_k)_{\mathbb R}\right|\longrightarrow0, \qquad \frac{\ln2}{k+1} \left|E_{\mathrm{PPT}}(G_{k+1})_{\mathbb R} -E_{\mathrm{PPT}}(\tau_k)_{\mathbb R}\right|\longrightarrow0.

For a bipartite matrix $X$ , these two quantities are infima in the extended nonnegative reals of $R(X\Vert Y)$ : for $E_{\mathrm{sep}}$ , $Y$ ranges over finite sums $\sum_{j<q}w_j(R_j\otimes S_j)$ with nonnegative weights summing to $1$ and local positive semidefinite, trace- $1$ matrices $R_j,S_j$ ; for $E_{\mathrm{PPT}}$ , $Y$ ranges over positive semidefinite, trace- $1$ matrices whose partial transpose $Y^{T_A}_{(a,b),(a',b')}=Y_{(a',b),(a,b')}$ is positive semidefinite. In either case, $R(X\Vert Y)=\max\{\operatorname{Re}\operatorname{tr}(f(X)-X\log Y),0\}/\ln2$ when both arguments are density matrices and $\ker Y\subseteq\ker X$ , and is $+\infty$ otherwise; $f(x)=x\ln x$ , with matrix functions defined by functional calculus and $\ln0=0$ . The real conversion denoted by the subscript $\mathbb R$ sends $+\infty$ to $0$ . The sequence begins at $k=0$ , hence uses one or more copies and never a zero denominator.

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