Lemma 3: biorthogonal mutual-information mixing

Open

QAlgorithms.Papers.Independent.Intakethird100.P63.lemma3_biorthogonalMixing

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

prove2quantum

Let $(w_k,\rho^k)$ be a finite or countable ensemble of normalized positive trace-class bipartite states, written with nonnegative weights of sum one and arbitrary zero padding. Let $\rho=\sum_k w_k\rho^k$ be its computed mixture. Suppose its two marginal entropies are finite, and that for every distinct pair of positive-weight labels $k,l$ , both $\rho_A^k\rho_A^l=0$ and $\rho_B^k\rho_B^l=0$ . With natural logarithms, $H(w)=-\sum_k w_k\log w_k$ and $I(A:B)=S(\rho_A)+S(\rho_B)-S(\rho_{AB})$ , one has

I(A:B)_\rho=H(w)+\sum_k w_k I(A:B)_{\rho^k}.

The formula is written using nonnegative extended sums; on this finite-entropy domain both terms on the right are finite. All reductions are actual partial traces. Active component entropy finiteness follows from finite mixture marginal entropies. Zero labels contribute zero and impose no component condition.

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 3, PDF p.6, cited there as Herbut [8], Lemma 9: biorthogonal
mutual-information mixing. The Shannon term uses the same natural logarithm as the
state entropy. Finite mixture subsystem entropies implement the source's entropy
cancellation domain and imply finite entropies of every positive-weight component. -/
theorem lemma3_biorthogonalMixing (e : DiscreteDensityEnsemble (Fin 2 → ℕ))
    (hbio : Biorthogonal e {0} {1})
    (hfinite : FiniteSubsystemEntropies (herbutMixture e)) :
    ENNReal.ofReal (clusterMutualInformation (herbutMixture e) {0} {1}) =
      QAlgorithms.Papers.Independent.Renew46.P08.countableShannonNats
        (fun k => ENNReal.ofReal (e.weight k)) +
      ∑' k, ENNReal.ofReal (e.weight k) *
        ENNReal.ofReal (clusterMutualInformation (e.component k) {0} {1}) := 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. 6, Lemma 3 (cited from Herbut [8], Lemma 9)

Read-back

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

Let $e$ consist of real weights $w_k$ and complex coefficient matrices $X_k$ indexed by $\mathbb N^2$ , for $k\in\mathbb N$ , with $w_k\ge0$ , $\sum_k w_k$ summable and equal to $1$ , and with each $X_k$ of positive weight a density matrix in the following sense: there exist sequences $u_r,v_r\in\ell^2(\mathbb N^2;\mathbb C)$ such that $\sum_r\|u_r\|\|v_r\|<\infty$ and $X_k(x,y)=\sum_r u_r(x)\overline{v_r(y)}$ ; every finite quadratic form $\sum_{x,y\in s}\overline{z(x)}X_k(x,y)z(y)$ is real and nonnegative; and the real diagonal entries are summable with sum $1$ . Components of zero weight have no density requirement. Define the mixture coefficientwise by $X(x,y)=\sum_k w_kX_k(x,y)$ . For any coefficient matrix $Y$ and any subset $C\subseteq\{0,1\}$ , define its reduction $Y_C$ , indexed by assignments of natural numbers to the coordinates in $C$ , by

Y_C(a,b)=\sum_{z:C^{\mathrm c}\to\mathbb N} Y(a\mathbin{\sqcup}z,b\mathbin{\sqcup}z),

where $a\mathbin{\sqcup}z$ uses $a$ on $C$ and $z$ on its complement. Define $H(Y)\in[0,\infty]$ as the infimum of $\sum_r[-p_r\log p_r]_+$ over all representations $Y(i,j)=\sum_r p_r f_r(i)\overline{f_r(j)}$ , where $p_r\ge0$ is summable with sum $1$ , $f_r\in\ell^2$ , and the vectors corresponding to positive weights are unit vectors and pairwise orthogonal; here $[a]_+=\max(a,0)$ , regarded as an extended nonnegative real, and an empty infimum is $+\infty$ . Put $h_C(Y)=H(Y_C)^{\mathrm{real}}$ and $I(Y)=h_{\{0\}}(Y)+h_{\{1\}}(Y)-h_{\{0,1\}}(Y)$ , where conversion to a real number sends $+\infty$ to $0$ . Suppose that for every pair $k\ne l$ with $w_k,w_l>0$ , both reduced matrix products vanish coefficientwise:

\sum_z (X_k)_{\{0\}}(a,z)(X_l)_{\{0\}}(z,b)=0, \qquad \sum_z (X_k)_{\{1\}}(a,z)(X_l)_{\{1\}}(z,b)=0 \quad\text{for all }a,b\in\mathbb N.

Suppose also that $H(X_C)\ne+\infty$ for every $C\subseteq\{0,1\}$ , including the empty subset and the whole set. Then the following equality holds in the extended nonnegative reals:

[I(X)]_+ = \sum_{k=0}^{\infty}[-w_k\log w_k]_+ + \sum_{k=0}^{\infty}w_k[I(X_k)]_+.

All coefficient sums above use the total infinite-sum convention, which assigns $0$ to a nonsummable complex series; $\log0=0$ . The component expressions $I(X_k)$ use the specified real conversion even when a component reduction has infinite entropy.

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