Prediction of a fair bit and the conditional-state average

Open

QAlgorithms.Papers.Independent.Intakethird100.P81.informational_distance_prediction_and_average

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

prove2quantum

Both statements use the full trace norm and $D(A:B)=\|\rho_{AB}-\rho_A\otimes\rho_B\|_1$ .

Let $\rho_{AB}$ be a normalized bipartite state with $\rho_B=I_2/2$ . Measure any Boolean POVM on $A$ , obtaining $X$ , and measure $B$ in its standard basis. For $0\le\varepsilon\le1$ , suppose $\Pr(X=B)\ge1-\varepsilon$ and $\Pr(X\ne B)\le\varepsilon$ . Applying the same measurement to the product of the marginals gives agreement and disagreement probabilities both equal to $1/2$ , and

D(A:B)\ge1-2\varepsilon.

Only the bit marginal is required to be classical; the joint state can have quantum coherences.

Let $\rho_{AB}$ be normalized and block diagonal in the standard basis of $A$ . Write $p_A(a)$ for the probability of $a$ and $\rho_B^{(a)}$ for the normalized conditional state whenever $p_A(a)>0$ . Then

D(A:B)=\sum_a p_A(a)\,\|\rho_B^{(a)}-\rho_B\|_1.

These formulas connect prediction and classical conditioning to informational distance. Zero-probability outcomes contribute zero; their conditional matrix is assigned zero in the formalization.

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 3, PDF pp.11–12: fair-bit prediction AND the exact classical-quantum average.
Only the bit marginal is classical in clause 1; the joint state need not be classical. -/
theorem informational_distance_prediction_and_average :
    (∀ (A : Type) [Fintype A] [DecidableEq A]
      (rho : Matrix (A × Bool) (A × Bool) ℂ), IsDensityMatrix rho →
      traceLeft rho = (1 / 2 : ℂ) • (1 : Matrix Bool Bool ℂ) →
      ∀ (eps : ℝ), 0 ≤ eps → eps ≤ 1 →
      ∀ M : Bool → Matrix A A ℂ, IsPOVM M →
        agreement M rho ≥ 1 - eps → 1 - agreement M rho ≤ eps →
        agreement M (jointMarginalProduct rho) = 1 / 2 ∧
        1 - agreement M (jointMarginalProduct rho) = 1 / 2 ∧
        informationalDistance rho ≥ 1 - 2 * eps) ∧
    (∀ (A B : Type) [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
      (rho : Matrix (A × B) (A × B) ℂ), IsDensityMatrix rho → ClassicalFirst rho →
        informationalDistance rho = ∑ a, classicalWeight rho a *
          traceNorm (firstRegisterConditionalBlock rho a - traceLeft rho)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P81

end

Source

On rounds in quantum communication, arXiv:quant-ph/0004100v5, PDF p. 11, Lemma 3 (continued on PDF p.12)

Read-back

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

The declaration asserts both of the following universally quantified claims. For any finite type $A$ with decidable equality, any positive semidefinite trace-one matrix $\rho$ on $A\times\{\mathrm{false},\mathrm{true}\}$ whose partial trace over $A$ is $\tfrac12 1$ , any real $0\le\varepsilon\le1$ , and any matrices $M_b$ on $A$ satisfying $M_b\ge0$ and $M_{\mathrm{false}}+M_{\mathrm{true}}=1$ , define

G(M,\tau)=\sum_b\operatorname{Re}\sum_{a,a'}(M_b)_{a,a'}\tau_{(a',b),(a,b)}.

If both $G(M,\rho)\ge1-\varepsilon$ and $1-G(M,\rho)\le\varepsilon$ hold, then, writing $\rho_A,\rho_B$ for the two partial traces and $\pi=\rho_A\otimes\rho_B$ ,

G(M,\pi)=\tfrac12,\qquad 1-G(M,\pi)=\tfrac12, \qquad \|\rho-\pi\|_1\ge1-2\varepsilon.

The second claim is that, for any finite types $A,B$ with decidable equality and any positive semidefinite trace-one matrix $\rho$ on $A\times B$ satisfying $\rho_{(a,b),(a',b')}=0$ whenever $a\ne a'$ , one has

\|\rho-\rho_A\otimes\rho_B\|_1 =\sum_{a\in A}w_a\,\|C_a-\rho_B\|_1, \qquad w_a=\operatorname{Re}\sum_b\rho_{(a,b),(a,b)}, \qquad (C_a)_{b,b'}=(w_a:\mathbb C)^{-1}\rho_{(a,b),(a,b')}.

In both claims, $(\rho_A)_{a,a'}=\sum_b\rho_{(a,b),(a',b)}$ , $(\rho_B)_{b,b'}=\sum_a\rho_{(a,b),(a,b')}$ , and $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , with the square root defined by continuous functional calculus. When $w_a=0$ , the definition gives $C_a=0$ , and its summand is zero. Empty index types are included in the quantifiers, but their corresponding density hypotheses cannot be satisfied.

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