Unnumbered result: quantum-auxiliary single-letter lower bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P42.quantumAuxiliaryLowerBound

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

prove2quantum

For a valid finite nonempty classical–quantum source, nonnegative finite distortion d(x,z), and target D>=0, let R_B(D) be the infimum of rates achievable by deterministic finite-block encoders and message-controlled reconstruction POVMs, using every positive rate slack and all sufficiently large positive blocklengths with expected distortion at most D. For every positive finite dimension of C, choose density matrices tau_x and an arbitrary joint CB reconstruction POVM. Compute the distortion on sum_x p(x)|x><x| tensor tau_x tensor rho_x and the bit-valued objective I(X;C)-I(C;B). The minimum R_B^(D) of this objective over the entire feasible domain obeys R_B^(D)<=R_B(D). Whenever finite, the minimum is attained by some such finite-dimensional datum. Empty feasible sets have value +infinity. No dimension bound, achievability claim, or equality with the operational rate is asserted.

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.17, unnumbered quantum-auxiliary lower bound: the printed minimum
is a lower bound on the operational R_B(d). All positive finite C dimensions
are allowed and the finite minimum is ATTAINED, asserted rather than assumed.
The literal p.16 rate definition is sufficient for this converse despite the
separate zero-distortion defect of Theorem 4.2. Empty feasible sets have value infinity. -/
theorem quantumAuxiliaryLowerBound {X B : Type} [Fintype X] [Fintype B]
    [Nonempty X] [Nonempty B] (E : CQData X B) (hE : E.Valid)
    (d : X → X → ℝ) (hd : ∀ x z, 0 ≤ d x z) (D : ℝ) (hD : 0 ≤ D) :
    quantumRDValue E d D ≤ exactDistortionRate E d D ∧
    (quantumRDValue E d D ≠ ⊤ →
      ∃ P : QuantumRDChoice X B, quantumRDExpected E d P ≤ D ∧
        ENNReal.ofReal (quantumRDCost E P) = quantumRDValue E d D) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P42

end

Source

Channel simulation with quantum side information, arXiv:quant-ph/0611008v1, PDF p. 17, Unnumbered result: quantum-auxiliary single-letter lower bound

Read-back

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

For every pair of nonempty finite, finitely enumerated types $X,B$ , data $E=(p,\rho)$ satisfying $p(x)\ge0$ , $\sum_xp(x)=1$ , and $\rho_x\succeq0$ with $\operatorname{tr}\rho_x=1$ for every $x$ , every function $d:X\times X\to\mathbb R$ satisfying $d(x,z)\ge0$ for all $x,z$ , and every real $D\ge0$ , the following inequality and conditional attainment assertion hold. Define $V\in[0,\infty]$ as the infimum of $\max(C,0)$ over every integer $a>0$ , family $\tau_x\succeq0$ of trace-one matrices on $\mathbb C^a$ , and family $M_z\succeq0$ on $\mathbb C^{a\times B}$ summing to $I$ , subject to

\sum_{x,z}p(x)\operatorname{Re}\operatorname{tr}\!\left(M_z(\tau_x\otimes\rho_x)\right)d(x,z)\le D,

where

C=\left[S(\bar\tau)-\sum_xp(x)S(\tau_x)\right] -\left[S(\bar\tau)+S(\bar\rho)-S(\Omega)\right],\quad \bar\tau=\sum_xp(x)\tau_x,\quad \bar\rho=\sum_xp(x)\rho_x,\quad \Omega=\sum_xp(x)(\tau_x\otimes\rho_x),

and $S(A)=-\operatorname{Re}\operatorname{tr}((t\mapsto t\log_2t)(A))$ , evaluated by continuous functional calculus. Define $R_{\mathrm{ex}}\in[0,\infty]$ as the infimum of all $R\ge0$ such that, for every $\delta>0$ , there is $N\in\mathbb N$ for which every integer $n\ge N$ with $n\ge1$ admits some $b\ge0$ , an encoder $e:X^n\to\{0,1\}^b$ , and matrices $F_{m,z}\succeq0$ on $\mathbb C^{B^n}$ , with $\sum_zF_{m,z}=I$ for every message $m$ , satisfying

b\le n(R+\delta),\qquad \sum_{x,z\in X^n}\left(\prod_i p(x_i)\right) \operatorname{Re}\operatorname{tr}\!\left(F_{e(x),z}\rho_x^{(n)}\right) \frac{\sum_i d(x_i,z_i)}n\le D, \quad (\rho_x^{(n)})_{u,v}=\prod_i(\rho_{x_i})_{u_i,v_i}.

Then $V\le R_{\mathrm{ex}}$ , and, if $V\ne+\infty$ , there exists one of the finite-dimensional choices defining $V$ whose distortion is at most $D$ and whose truncated cost $\max(C,0)$ equals $V$ . Both infima use $+\infty$ for an empty feasible set; zero source probabilities, $D=0$ , and zero message bits are included.

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