Mutual information as relative entropy and its sharp bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P81.mutual_information_relative_entropy

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

prove2quantum

Let $\rho_{AB}$ be a normalized density matrix of a finite bipartite complex system. Compute both marginals from this same state: $\rho_A=\operatorname{Tr}_B\rho_{AB}$ and $\rho_B=\operatorname{Tr}_A\rho_{AB}$ . Define $S(A:B)=S(\rho_A)+S(\rho_B)-S(\rho_{AB})$ , with entropy measured in bits. Then the product of the marginals is a density matrix and

S(A:B)=S_2(\rho_{AB}\Vert\rho_A\otimes\rho_B) \ge\frac{\|\rho_{AB}-\rho_A\otimes\rho_B\|_1^2}{2\ln 2}.

The identity and bound relate correlations to the full trace-norm distance from independence. The product state is constructed from the joint state, including when marginals are singular.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P81

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ENNReal

attribute [local instance] Classical.propDecidable

namespace QAlgorithms.Papers.Independent.Intakethird100.P81

open QAlgorithms.Papers.Independent.Information100.P54 (relativeEntropyBits)

open QAlgorithms.Papers.Independent.Bridge50.P44 (ClassicalFirst)

/-- Unnumbered display, PDF p.11: both the relative-entropy identity and its sharp lower bound.
The product matrix and its normalization are conclusions constructed from rho. -/
theorem mutual_information_relative_entropy {A B : Type*}
    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
    (rho : Matrix (A × B) (A × B) ℂ) (hrho : IsDensityMatrix rho) :
    ∃ hprod : IsDensityMatrix (jointMarginalProduct rho),
      relativeEntropyBits rho (jointMarginalProduct rho) =
        ENNReal.ofReal (jointMutualInfoBits rho) ∧
      (traceNorm (rho - jointMarginalProduct rho)) ^ 2 / (2 * Real.log 2) ≤
        jointMutualInfoBits rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P81

end

Source

On rounds in quantum communication, arXiv:quant-ph/0004100v5, PDF p. 11, Unnumbered display following Theorem 1

Read-back

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

For all finite types $A,B$ with decidable equality and every positive semidefinite complex matrix $\rho$ on $A\times B$ with trace $1$ , define $(\rho_A)_{a,a'}=\sum_b\rho_{(a,b),(a',b)}$ , $(\rho_B)_{b,b'}=\sum_a\rho_{(a,b),(a,b')}$ , and $\pi=\rho_A\otimes\rho_B$ . Set $H(X)=-\operatorname{Re}\operatorname{tr}((x\mapsto x\log_2x)[X])$ , where brackets denote continuous functional calculus, and set $I_\rho=H(\rho_A)+H(\rho_B)-H(\rho)$ . The assertion is that $\pi$ is positive semidefinite with trace $1$ , and

D_{\mathrm{bits}}(\rho\|\pi)=[I_\rho]_+, \qquad \frac{\|\rho-\pi\|_1^2}{2\ln 2}\le I_\rho.

Here $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , $[r]_+=\max(r,0)$ is embedded into the extended nonnegative reals, and $D_{\mathrm{bits}}(\rho\|\pi)$ is $+\infty$ if $\ker\pi\not\subseteq\ker\rho$ , and otherwise equals $\left[\operatorname{Re}\operatorname{tr}((x\mapsto x\ln x)[\rho]-\rho(\ln)[\pi])\right]_+/\ln2$ , with the real logarithm assigned value zero at zero. Neither $A$ nor $B$ can be empty under the density hypothesis.

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