Explicit assisted lower curves and convexified purification upper bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P27.isotropic_unassisted_bounds

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

prove2quantum

For the memoryless maximally mixed qubit source with Bell purification $\Phi$ and distortion observable $I-\Phi$ , let $R^q(D)$ be the operational unassisted quantum rate in qubits per copy. For $0\le D\le1$ , define the two explicit curves from Theorems 11 and 12 by

L_{\rm ea}(D)=\begin{cases}1-\tfrac12H(1-D,D/3,D/3,D/3),&D\le3/4,\\0,&D>3/4,\end{cases}\qquad L_{\to}(D)=\begin{cases}h_2(1/2+\sqrt{D(1-D)}),&D<1/2,\\0,&D\ge1/2.\end{cases}

Here $H$ is Shannon entropy and $h_2(p)=-p\log_2p-(1-p)\log_2(1-p)$ , with zero logarithmic terms contributing zero. Put $\tau_d=(1-d)\Phi+(d/3)(I-\Phi)$ and $c(d)=E_p(\tau_d)$ for $0\le d\le3/4$ , and $c(d)=0$ for $3/4<d\le1$ . Define

U(D)=\inf\left\{\sum_{i=1}^m p_i c(d_i):m\ge1,\ p_i\ge0,\ \sum_i p_i=1,\ 0\le d_i\le1,\ \sum_i p_id_i\le D\right\}.

Then

\max\{L_{\rm ea}(D),L_{\to}(D)\}\le R^q(D)\le U(D).

$E_p$ is optimized over all finite normalized purifications with exactly the prescribed marginal. The upper bound uses finite time-sharing mixtures, not an assumed numerical evaluation; no exact formula for the unassisted rate is claimed.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P27

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P27

open Filter

open scoped Matrix ComplexConjugate ComplexOrder ENNReal

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Dependency50.P19
  (first marginalRB mutualInformation bipartiteBlock epr)

open QAlgorithms.Papers.Independent.Information100.P08 (formation)

open QAlgorithms.Papers.Independent.Gap48.P20 (redistributionMarginal)

open QAlgorithms.Papers.Independent.Bridge50.P37 (isotropicState normalizedEntangledProjection)

/-- PDF pp.9--10, unnumbered bounds and footnote 2: the explicit curves from
Theorems 11 and 12 lower-bound the unassisted operational rate, which is at most
the convexified exact E_p strategy cost. The Devetak--Berger curve has no factor
1/2 before binary entropy and vanishes for D >= 1/2. This is not an exact formula
for the unassisted rate. -/
theorem isotropic_unassisted_bounds
    (S : DistortionSource (Fin 2) (Fin 2))
    (hsource : pureDensity S.psi = epr 2) (hdelta : S.delta = 1 - epr 2)
    (D : ℝ) (hD0 : 0 ≤ D) (hD1 : D ≤ 1) :
    max (ENNReal.ofReal (if D ≤ 3 / 4 then 1 - isotropicEntropy D / 2 else 0))
      (ENNReal.ofReal (if D < 1 / 2 then
        binEntropy2 (1 / 2 + Real.sqrt (D * (1 - D))) else 0)) ≤
      rateDistortion S .unassisted D ∧
    rateDistortion S .unassisted D ≤ isotropicConvexUpper D := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P27

end

Source

Quantum rate distortion coding with auxiliary resources, arXiv:1212.5316v3, PDF p. 9, §V-A, unnumbered; p.10 and footnote 2

Read-back

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

Let $S$ consist of a normalized vector $\psi\in\mathbb C^{2\times2}$ and a positive semidefinite distortion matrix $\Delta$ , and suppose $|\psi\rangle\langle\psi|=\Omega$ and $\Delta=I-\Omega$ , where $\Omega_{(i,j),(k,l)}=\tfrac12$ if $i=j$ and $k=l$ , and is zero otherwise. For $0\le D\le1$ , define $R(D)\in[0,\infty]$ as the infimum of all real $r\ge0$ such that, for every $\epsilon>0$ and $s>0$ , every sufficiently large integer $n\ge1$ admits channels encoding the $n$ source registers into a positive dimensional quantum register of dimension $q$ and decoding it into $n$ output qubits, with $\log_2q\le n(r+s)$ , and with

\frac1n\sum_{i=1}^n\operatorname{Re}\operatorname{tr}\bigl[(I-\Omega)\,\omega_{A_iB_i}\bigr]\le D+\epsilon.

Here $\omega$ is obtained by applying the encoder and decoder to the second halves of $\Omega^{\otimes n}$ , leaving the first halves untouched; $\omega_{A_iB_i}$ is its $i$ -th reference–output marginal. Channels have finite Kraus representations $X\mapsto\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ ; the code has one dimensional classical and shared registers. Let $h_2(x)=\operatorname{binEntropy}(x)/\ln2$ , so on $[0,1]$ it is binary entropy with zero endpoint terms, and set

H_{\mathrm{iso}}(D)=-(1-D)\log_2(1-D)-3\frac D3\log_2\frac D3.

For a bipartite matrix $\rho$ , let $E_P(\rho)$ be the infimum in $[0,\infty]$ of $\max\{H(\operatorname{Tr}_{BV}|v\rangle\langle v|),0\}$ over all normalized vectors $v$ on $(A\times U)\times(B\times V)$ , with finite positive dimensional $U,V$ , whose marginal on $A\times B$ equals $\rho$ ; here $(|v\rangle\langle v|)_{ij}=v_i\overline{v_j}$ and $H(X)=-\operatorname{Re}\operatorname{tr}[f(X)]$ , where $f(x)=x\log_2x$ is applied by continuous functional calculus. Put

C(d)= \begin{cases} E_P\!\left((1-d)\Omega+\dfrac d3(I-\Omega)\right),&d\le\tfrac34,\\ 0,&d>\tfrac34, \end{cases}

and let $U(D)$ be the infimum of $\sum_{i=1}^m p_iC(d_i)$ over every positive integer $m$ , real weights $p_i\ge0$ with $\sum_i p_i=1$ , and $d_i\in[0,1]$ satisfying $\sum_i p_id_i\le D$ . The assertion is

\max\!\left\{ \max\!\left(0, \begin{cases}1-\tfrac12H_{\mathrm{iso}}(D),&D\le\tfrac34,\\0,&D>\tfrac34,\end{cases}\right), \max\!\left(0, \begin{cases}h_2\!\left(\tfrac12+\sqrt{D(1-D)}\right),&D<\tfrac12,\\0,&D\ge\tfrac12\end{cases}\right) \right\} \le R(D)\le U(D).

The endpoints $D=0,1$ are included; the first lower-bound branch includes $D=\tfrac34$ , while the second excludes $D=\tfrac12$ . All costs, infima, and weighted sums use extended nonnegative arithmetic, including $0\cdot(+\infty)=0$ .

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