All five properties of informational distance

Open

QAlgorithms.Papers.Independent.Intakethird100.P81.informational_distance_properties

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

prove2quantum

Let $\rho_{ABC}$ be any normalized state on finite-dimensional complex systems. For each indicated marginal define $D(U:V)=\|\rho_{UV}-\rho_U\otimes\rho_V\|_1$ , and use mutual information $S(U:V)$ in bits. All of the following hold:

$D(A:B)=D(B:A)$ , with the two tensor factors exchanged.
$D(AB:C)\ge D(A:C)$ , where $B$ is traced out on the right.
$0\le D(A:B)\le2$ .
For every finite-dimensional CPTP map $F$ on $AB$ , $D(A:B)\ge\|F(\rho_{AB})-F(\rho_A\otimes\rho_B)\|_1$ .
The source's stated estimate is

D(A:B)\le\sqrt{2S(A:B)}.

These properties make informational distance compatible with exchanging subsystems, discarding subsystems and physical processing. Clause 5 keeps the printed weaker constant.

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)

/-- Lemma 2, PDF p.11: all five clauses, with explicit swap, regrouping and marginalization. -/
theorem informational_distance_properties {A B C : Type*}
    [Fintype A] [Fintype B] [Fintype C]
    [DecidableEq A] [DecidableEq B] [DecidableEq C]
    (rho : Matrix ((A × B) × C) ((A × B) × C) ℂ)
    (hrho : IsDensityMatrix rho) :
    let ab := traceRight rho
    informationalDistance ab = informationalDistance (swapState ab) ∧
    informationalDistance rho ≥ informationalDistance (traceRight
      (fun p q : (A × C) × B =>
        rho ((p.1.1, p.2), p.1.2) ((q.1.1, q.2), q.1.2))) ∧
    (0 ≤ informationalDistance ab ∧ informationalDistance ab ≤ 2) ∧
    (∀ (J : Type) [Fintype J] [DecidableEq J] (F : Superop (A × B) J),
      IsChannel F → traceNorm (F ab - F (jointMarginalProduct ab)) ≤ informationalDistance ab) ∧
    informationalDistance ab ≤ Real.sqrt (2 * jointMutualInfoBits ab) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P81

end

Source

On rounds in quantum communication, arXiv:quant-ph/0004100v5, PDF p. 11, Lemma 2

Read-back

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

For all finite types $A,B,C$ with decidable equality and every positive semidefinite trace-one matrix $\rho$ on $(A\times B)\times C$ , let $\rho_{AB}$ be its partial trace over $C$ , and define $(\rho_{AC})_{(a,c),(a',c')}=\sum_b\rho_{((a,b),c),((a',b),c')}$ . For any matrix $\tau$ on a bipartite index set $X\times Y$ , write $\tau_X,\tau_Y$ for the partial traces over $Y,X$ , respectively, and define $\mathcal D(\tau)=\|\tau-\tau_X\otimes\tau_Y\|_1$ , where $\|Z\|_1=\operatorname{Re}\operatorname{tr}\sqrt{Z^\dagger Z}$ uses continuous functional calculus. Also define $H(Z)=-\operatorname{Re}\operatorname{tr}((x\mapsto x\log_2x)[Z])$ . The assertions are

\mathcal D(\rho_{AB})=\mathcal D(\operatorname{swap}(\rho_{AB})), \qquad \mathcal D(\rho)\ge\mathcal D(\rho_{AC}), \qquad 0\le\mathcal D(\rho_{AB})\le2,

where $\operatorname{swap}(\tau)_{(b,a),(b',a')}=\tau_{(a,b),(a',b')}$ , and $\mathcal D(\rho)$ uses the partition $(A\times B):C$ . Moreover, for every finite type $J$ with decidable equality and every function $F$ admitting a finite representation $F(X)=\sum_jE_jXE_j^\dagger$ with $\sum_jE_j^\dagger E_j=1$ ,

\left\|F(\rho_{AB})-F\bigl((\rho_{AB})_A\otimes(\rho_{AB})_B\bigr)\right\|_1 \le\mathcal D(\rho_{AB}), \qquad \mathcal D(\rho_{AB})\le \sqrt{2\bigl(H((\rho_{AB})_A)+H((\rho_{AB})_B)-H(\rho_{AB})\bigr)}.

The density hypothesis excludes empty $A,B,C$ ; the quantification over $J$ includes any empty case compatible with the representation of $F$ .

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