Lemma 2: biorthogonality lifts from 1|2 to 1|23

Open

QAlgorithms.Papers.Independent.Intakethird100.P63.lemma2_liftBiorthogonality

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$ . A discrete ensemble may have finitely or countably many components: its weights $w_k$ are nonnegative and sum to one, and each component with $w_k>0$ is a normalized density operator. Every mixture below is the computed trace-norm convergent sum $\rho=\sum_k w_k\rho^k$ . All component conditions concern positive-weight labels only.

Let the ensemble be tripartite and suppose for every distinct active pair $k,l$ that $\rho_1^k\rho_1^l=0$ and $\rho_2^k\rho_2^l=0$ . Then

\rho_1^k\rho_1^l=0,\qquad\rho_{23}^k\rho_{23}^l=0\qquad(k\ne l,\ w_kw_l>0).

The products are ordinary operator products and all marginals are partial traces. Thus the same decomposition is biorthogonal for the bipartition $1|23$ . No entropy-finiteness or SSA-equality premise is needed.

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 2, PDF pp.5–6, (13): biorthogonality lifts from 1|2 to 1|23.
No entropy, entropy-finiteness, or component SSA premise is needed. -/
theorem lemma2_liftBiorthogonality (e : DiscreteDensityEnsemble (Fin 3 → ℕ))
    (hbio : Biorthogonal e {0} {1}) : Biorthogonal e {0} {1, 2} := 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. 5, Lemma 2: biorthogonality lifts from 1|2 to 1|23

Read-back

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

Let $e$ consist of nonnegative summable real weights $w_k$ , $k\in\mathbb N$ , of sum $1$ , and complex kernels $K_k$ on $\mathbb N^3$ . Whenever $w_k>0$ , require an entrywise representation $K_k(i,j)=\sum_r a_r(i)\overline{b_r(j)}$ , with square-summable vectors and $\sum_r\|a_r\|\|b_r\|<\infty$ , real nonnegative finite quadratic forms $\sum_{i,j\in F}\overline{z_i}K_k(i,j)z_j$ for every finite $F$ and arbitrary complex $z$ , and summable real diagonal of sum $1$ ; zero-weight components are unrestricted. For $C\subseteq\{0,1,2\}$ , define $R_C^k(x,y)=\sum_{z\in\mathbb N^{C^c}}K_k(x\oplus_C z,y\oplus_C z)$ , where joined configurations agree with the first argument on $C$ and with $z$ on its complement. Assume that for every pair of distinct positive-weight indices $k,l$ , both $\sum_zR_{\{0\}}^k(x,z)R_{\{0\}}^l(z,y)=0$ and $\sum_zR_{\{1\}}^k(x,z)R_{\{1\}}^l(z,y)=0$ for all configurations $x,y$ on the respective singleton sets. Then, for every such pair $k,l$ , both

\sum_{z\in\mathbb N^{\{0\}}}R_{\{0\}}^k(x,z)R_{\{0\}}^l(z,y)=0, \qquad \sum_{z\in\mathbb N^{\{1,2\}}}R_{\{1,2\}}^k(x,z)R_{\{1,2\}}^l(z,y)=0

hold for all configurations $x,y$ on the respective sets. These are total infinite sums, and the conditions on distinct positive-weight indices are vacuous if there is only one such index.

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