Lemma 1: multipartite subadditivity and its equality case

Open

QAlgorithms.Papers.Independent.Intakethird100.P63.lemma1_subadditivity

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

prove2quantum

All states below are positive trace-class density operators of trace one on completed complex Hilbert tensor products, represented in countable orthonormal coordinates. Finite dimensional systems are included. Entropies use natural logarithms and the convention $0\log 0=0$ . Every subsystem entropy occurring in an entropy difference is finite; this is the proof-supported finite-entropy reading of the source, and imposes no finite Hilbert dimension.

Let $N\ge2$ , let $\rho$ be an $N$ -party state, and let $\rho_n$ be its actual marginal on party $n$ . Then

S(\rho)\le\sum_{n=1}^{N}S(\rho_n),\qquad S(\rho)=\sum_{n=1}^{N}S(\rho_n)\iff\rho=\bigotimes_{n=1}^{N}\rho_n.

Thus equality characterizes complete absence of correlations among the parties.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P63

Formal statement

noncomputable section

open scoped ENNReal BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P63

attribute [local instance] Classical.propDecidable Classical.decEq

-- Reuse the accepted nuclear trace-class, positive, trace-one predicate verbatim.

open QAlgorithms.Papers.Independent.Dependency50.P33 (IsDensity)

open QAlgorithms.Papers.Independent.Dependency50.P13 (finiteRelativeEntropy)

/-- Lemma 1, PDF p.2, (1): multipartite subadditivity and its full equality case.
Finite subsystem entropies make the source's equality characterization meaningful. -/
theorem lemma1_subadditivity {n : ℕ} (hn : 2 ≤ n)
    (rho : (Matrix (Fin n → ℕ) (Fin n → ℕ) ℂ)) (hrho : IsDensity rho)
    (hfinite : FiniteSubsystemEntropies rho) :
    herbutMarginalEntropy rho Finset.univ ≤ ∑ i : Fin n, herbutMarginalEntropy rho {i} ∧
    (herbutMarginalEntropy rho Finset.univ = ∑ i : Fin n, herbutMarginalEntropy rho {i} ↔
      rho = tensorMarginals rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P63

end

Source

On Mutual Information in Multipartite Quantum States and Equality in Strong Subadditivity of Entropy, arXiv:quant-ph/0311193v1, PDF p. 2, Lemma 1: multipartite subadditivity and its equality case

Read-back

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

For every natural number $n\ge2$ and complex kernel $\rho$ on $\mathbb N^n$ , assume that $\rho(i,j)=\sum_r a_r(i)\overline{b_r(j)}$ for some $a_r,b_r\in\ell^2(\mathbb N^n;\mathbb C)$ with $\sum_r\|a_r\|\|b_r\|<\infty$ , that every finite quadratic form $\sum_{i,j\in F}\overline{z_i}\rho(i,j)z_j$ is real and nonnegative for finite $F\subseteq\mathbb N^n$ and arbitrary $z:\mathbb N^n\to\mathbb C$ , and that the real diagonal of $\rho$ is summable with sum $1$ . For each coordinate set $C\subseteq U=\{0,\ldots,n-1\}$ , let $R_C(x,y)=\sum_{z\in\mathbb N^{C^c}}\rho(x\oplus_C z,y\oplus_C z)$ , where joining configurations uses $x,y$ on $C$ and $z$ on $C^c$ . Define $H(K)$ as the infimum, in $[0,\infty]$ , of $\sum_k\max\{-w_k\log w_k,0\}$ over representations $K(i,j)=\sum_k w_k u_k(i)\overline{u_k(j)}$ with nonnegative summable weights of total mass $1$ and square-summable vectors that have norm $1$ and are pairwise orthogonal at distinct positive-weight indices; an empty collection of representations gives $+\infty$ . Assume $H(R_C)\ne+\infty$ for every $C$ , including the empty and full coordinate sets, and write $S(C)=H(R_C).\mathrm{toReal}$ . Then

S(U)\le\sum_{i=0}^{n-1}S(\{i\}), \qquad S(U)=\sum_{i=0}^{n-1}S(\{i\}) \ \Longleftrightarrow\ \forall x,y\in\mathbb N^n,\quad \rho(x,y)=\prod_{i=0}^{n-1}R_{\{i\}}(x_i,y_i).

In the last expression, $x_i,y_i$ denote configurations on the singleton $\{i\}$ ; all infinite kernel sums use the total-sum convention.

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