Tensor-product additivity

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.tensorAdditivity

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

prove2quantum

Let $\rho$ on $A\otimes B$ and $\sigma$ on $A'\otimes B'$ be independent positive semidefinite, trace-one states on arbitrary nonzero finite-dimensional local spaces. Regard their tensor product as bipartite across $AA':BB'$ . Let $W$ be the primal SDP (7) value and $E_W=\log_2W$ . Then

W(\rho\otimes\sigma)=W(\rho)W(\sigma),\qquad E_W(\rho\otimes\sigma)=E_W(\rho)+E_W(\sigma).

The identities hold without requiring equal local dimensions and allow the bound to be evaluated on tensor powers.

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]

/-- Property i), PDF pp.2–3: multiplicativity of W and additivity of E_W,
with independent input states and independent local dimensions. -/
theorem tensorAdditivity [Nonempty A] [Nonempty B] [Nonempty C] [Nonempty D]
    (rho : Matrix (A × B) (A × B) ℂ) (sigma : Matrix (C × D) (C × D) ℂ)
    (hrho : IsDensityMatrix rho) (hsigma : IsDensityMatrix sigma) :
    wValue (regroupedTensor rho sigma) = wValue rho * wValue sigma ∧
    entanglementW (regroupedTensor rho sigma) = entanglementW rho + entanglementW sigma := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P83

end

Source

Improved Semidefinite Programming Upper Bound on Distillable Entanglement, arXiv:1601.07940v4, PDF p. 2, Unnumbered property i): tensor-product additivity

Read-back

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

Let $A,B,C,D$ be finite nonempty types with decidable equality, and let $\rho$ on $A\times B$ and $\sigma$ on $C\times D$ be positive semidefinite complex matrices, each of trace $1$ . For any bipartite matrix $X$ , let $X^\Gamma_{(i,j),(i',j')}=X_{(i,j'),(i',j)}$ , and define

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

where the supremum ranges over matrices on the same bipartite space as $X$ , and the norm is the Euclidean operator norm. Define $T$ , indexed by $(A\times C)\times(B\times D)$ , by

T_{((a,c),(b,d)),((a',c'),(b',d'))} =\rho_{(a,b),(a',b')}\,\sigma_{(c,d),(c',d')}.

The theorem asserts both $w(T)=w(\rho)w(\sigma)$ and $W(T)=W(\rho)+W(\sigma)$ ; in computing the quantities for $T$ , partial transpose acts on the grouped second component $B\times D$ .

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