Unnumbered corollary: channel simulation with classical side information

Open

QAlgorithms.Papers.Independent.Intakethird100.P42.classicalSideInformation

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

prove2quantum

Let $X,Y,Z$ be finite nonempty alphabets, $p(x)$ a probability distribution, and $W(y\mid x),V(z\mid x)$ stochastic channels. The source law is $p(x)V(z\mid x)$ and the desired joint law is $p(x)W(y\mid x)V(z\mid x)$ , so $Y\to X\to Z$ ; $X$ and $Z$ need not be independent. Alice initially holds $X^n$ , Bob holds $Z^n$ , and both retain a simulated copy of $Y^n$ .

For nonnegative rates $R,C$ , a fully classical simulation is achievable exactly when

R\ge I(X;Y)-I(Y;Z),\qquad R+C\ge H(Y\mid Z).

For every positive error and rate slack and every sufficiently large positive $n$ , codes use at most $n(R+\delta)$ forward classical bits and $n(C+\delta)$ independent uniform shared bits. The full $\ell^1$ error includes the original $X^n,Z^n$ and both output copies. Bob's diagonal POVM represents stochastic classical decoding and preserves $Z^n$ .

This is the immediate classical specialization of the channel simulation theorem. In Lean, conditional states are the computed diagonal matrices $\rho_x=\sum_zV(z\mid x)|z\rangle\langle z|$ , and their Holevo terms equal the displayed classical information quantities.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P42

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P42

open scoped BigOperators ComplexConjugate ENNReal

open Filter

open QAlgorithms.Papers.Independent.Dependency50.P07

open QAlgorithms.Papers.Independent.Gap48.P20

open QAlgorithms.Papers.Independent.Information100.P27 (IsProbability shannon)

attribute [local instance] Classical.decEq Classical.propDecidable

/-- PDF p.19, immediate corollary: classical side information, allowing arbitrary
correlation XZ and the Markov law Y--X--Z, with the same two exact rate inequalities. -/
theorem classicalSideInformation {X : Type} [Fintype X] [Nonempty X]
    (p : X → ℝ) (hp : IsProbability p) (Z V : Auxiliary X)
    (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) :
    ClassicalSimulationAchievable p Z V R C ↔
      auxCost (diagonalCQSource p Z) V ≤ R ∧
        shannon (auxProb (diagonalCQSource p Z) V) - auxIQ (diagonalCQSource p Z) V ≤ R + C := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P42

end

Source

Channel simulation with quantum side information, arXiv:quant-ph/0611008v1, PDF p. 19, Unnumbered corollary: channel simulation with classical side information

Read-back

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

Let $X$ be any finite nonempty set, let $p:X\to\mathbb R$ satisfy $p(x)\ge0$ and $\sum_xp(x)=1$ , and let $Z$ and $V$ be stochastic maps from $X$ to finite alphabets $\mathcal Z=\{0,\ldots,z_0-1\}$ and $\mathcal U=\{0,\ldots,u_0-1\}$ , respectively, where $z_0,u_0>0$ : every $Z(z\mid x)$ and $V(u\mid x)$ is nonnegative, and each map sums to $1$ for every $x$ . Let $R,C\in\mathbb R$ satisfy $R,C\ge0$ . Define the joint probability law

q(x,u,z)=p(x)V(u\mid x)Z(z\mid x),

and write $H$ for Shannon entropy in bits, $H(a)=-\sum_i a_i\log_2a_i$ , with $0\log_2 0=0$ . Set

I(U;X)=H(p)+H(q_U)-H(q_{XU}),\qquad I(U;Z)=H(q_Z)-\sum_u q_U(u)\, H\!\left(\frac{q_{UZ}(u,\cdot)}{q_U(u)}\right),

where a conditional vector with $q_U(u)=0$ is defined to be the zero vector, so its summand is zero. The declaration asserts that

I(U;X)-I(U;Z)\le R \quad\text{and}\quad H(q_U)-I(U;Z)\le R+C

hold if and only if the following simulation property holds. For every $\varepsilon>0$ and $\delta>0$ , there is a natural number $N$ such that, for every natural $n\ge N$ with $n\ge1$ , there exist natural numbers $a,b,h$ , encoding probabilities $e(w,\ell,m,s)\ge0$ , measurement probabilities $f_{\ell,m,t}(z)\ge0$ , and a decoding function $d(\ell,m,s)\in\mathcal U^n$ , where $w\in X^n$ , $\ell\in\{0,1\}^a$ , $m\in\{0,1\}^b$ , $s,t\in\{0,1\}^h$ , and $z\in\mathcal Z^n$ , satisfying

\sum_{m,s}e(w,\ell,m,s)=1,\qquad \sum_t f_{\ell,m,t}(z)=1,\qquad b\le n(R+\delta),\qquad a\le n(C+\delta).

Here the $f_{\ell,m,t}$ are precisely the diagonal entries of the decoding measurement effects; all off-diagonal entries of those effects are required to vanish. With

p_n(w)=\prod_{i=0}^{n-1}p(w_i),\qquad Z_n(z\mid w)=\prod_{i=0}^{n-1}Z(z_i\mid w_i),

define, for $u,v\in\mathcal U^n$ ,

T(w,u,v,z)= \mathbf1_{\{u=v\}}\,p_n(w)Z_n(z\mid w) \prod_{i=0}^{n-1}V(u_i\mid w_i)

and

O(w,u,v,z)=p_n(w)Z_n(z\mid w)\,2^{-a} \sum_{\ell,m,s,t} \mathbf1_{\{d(\ell,m,s)=u,\ d(\ell,m,t)=v\}} e(w,\ell,m,s)f_{\ell,m,t}(z).

The required error bound is

\sum_{w,u,v,z}|T(w,u,v,z)-O(w,u,v,z)|\le\varepsilon,

which is the specified trace norm error for these diagonal matrices, without a factor of $1/2$ . Zero probabilities are permitted throughout; the bit counts $a,b,h$ may be zero, and the private bit count $h$ has no rate bound.

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