Irreducible product-source rate-sum converse

Open

QAlgorithms.Papers.Independent.Intakethird100.P11.irreducibleProduct_converse

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

prove2quantum

Let $I$ be a finite label set, $p_i\ge0$ with $\sum_i p_i=1$ , and let $|\phi_i\rangle\in\mathcal H_A$ , $|\psi_i\rangle\in\mathcal H_B$ be unit vectors in finite-dimensional complex Hilbert spaces. Set $\mathcal E_{AB}=\{p_i,|\phi_i\rangle\otimes|\psi_i\rangle\}$ . Assume that its positive-probability support admits no partition into two nonempty mutually orthogonal classes. Write $S(\mathcal E)$ for the base-two von Neumann entropy of its average density operator, and $\mathcal E_A,\mathcal E_B$ for its marginal ensembles. Every achievable real pair $(R_A,R_B)$ satisfies

R_A+R_B\ge\frac{S(\mathcal E_A)+S(\mathcal E_B)+S(\mathcal E_{AB})}{2}.

An achievable pair uses independent blind local CPTP encoders, one noiseless quantum link from each sender, and a joint CPTP decoder, without supplied shared entanglement or side messages. For every $\delta,\epsilon>0$ , every sufficiently large positive integer blocklength $n$ admits positive compressed dimensions $d_A,d_B$ with $\log_2(d_A)/n\le R_A+\delta$ , $\log_2(d_B)/n\le R_B+\delta$ , and ensemble-average pure-input overlap with the reconstructed density operator at least $1-\epsilon$ . Draws are independent and identically distributed; this is squared fidelity, without a purifying reference.

This is a necessary sum-rate constraint for globally irreducible product sources; it does not by itself characterize a complete rate region.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P11

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P11

open MeasureTheory Filter

open scoped BigOperators ComplexConjugate Matrix

open QAlgorithms.Papers.Independent.Dependency50.P19 (both)

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

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.6, Theorem III.3, (10): the rate-sum converse for globally irreducible
product sources. Irreducibility of the separate marginal ensembles is insufficient. -/
theorem irreducibleProduct_converse {I A B : Type*}
    [Fintype I] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
    (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) (htotal : ∑ i, p i = 1)
    (phi : I → EuclideanSpace ℂ A) (psi : I → EuclideanSpace ℂ B)
    (hphi : ∀ i, IsState (phi i)) (hpsi : ∀ i, IsState (psi i))
    (hirr : EnsembleIrreducible p (fun i => tensorVec (phi i) (psi i)))
    (ra rb : ℝ) (hach : FiniteAchievable p (fun i => tensorVec (phi i) (psi i)) ra rb) :
    (vnEntropy (sourceMean p phi) + vnEntropy (sourceMean p psi) +
      vnEntropy (sourceMean p (fun i => tensorVec (phi i) (psi i)))) / 2 ≤ ra + rb := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P11

end

Source

On the distributed compression of quantum information, arXiv:quant-ph/0403042v3, PDF p. 6, Theorem III.3: irreducible product-source rate-sum converse

Read-back

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

Let $I,A,B$ be finite types, with decidable equality on $A,B$ , let $p_i\ge0$ satisfy $\sum_{i\in I}p_i=1$ , and let $\phi_i\in\mathbb C^A$ and $\psi_i\in\mathbb C^B$ have norm $1$ for every $i$ , including labels of weight zero. Put $v_i(a,b)=\phi_i(a)\psi_i(b)$ . Assume that some $p_i>0$ , and that every subset of labels containing and excluding positive-weight labels has labels $i$ inside and $j$ outside with $p_i,p_j>0$ and $\langle v_i,v_j\rangle\ne0$ . Let $r_A,r_B\in\mathbb R$ , and assume that for every $\delta,\varepsilon>0$ , all sufficiently large positive lengths $n$ admit positive dimensions $d_A,d_B$ and separate encoders and a joint decoder, each of the form $\Phi(X)=\sum_jK_jXK_j^\dagger$ with finitely many $K_j$ and $\sum_jK_j^\dagger K_j=I$ , such that their composite $\mathcal C=\mathcal D\circ(\mathcal E_A\otimes\mathcal E_B)$ satisfies

\sum_{w\in I^n}\left(\prod_{t=0}^{n-1}p_{w(t)}\right) \operatorname{Re}\operatorname{tr}\!\left(\rho_w\mathcal C(\rho_w)\right) \ge1-\varepsilon, \qquad \frac{\log_2d_A}{n}\le r_A+\delta, \qquad \frac{\log_2d_B}{n}\le r_B+\delta,

where $V_w(a,b)=\prod_t v_{w(t)}(a(t),b(t))$ and $\rho_w=V_wV_w^\dagger$ . Then

\frac{ S\!\left(\sum_i p_i\phi_i\phi_i^\dagger\right) + S\!\left(\sum_i p_i\psi_i\psi_i^\dagger\right) + S\!\left(\sum_i p_iv_iv_i^\dagger\right) }{2} \le r_A+r_B,

where $S(M)=-\operatorname{Re}\operatorname{tr}(f(M))$ , with $f(x)=x\log_2x$ applied by continuous functional calculus. No separate nonnegativity assumptions on $r_A,r_B$ are present. Although empty finite types are permitted by the type parameters, the probability and unit-norm hypotheses exclude them here.

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