Unnumbered result: subadditivity and existence of the regularized variational limit

Open

QAlgorithms.Papers.Independent.Intakethird100.P42.variationalSubadditivity

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

prove2quantum

Let $\{p(x),\rho_x^B\}$ be a normalized finite memoryless classical–quantum source. Let $d:X\times X\to[0,\infty)$ be a finite distortion measure and $D\ge0$ a distortion target. For each positive integer $n$ , define $V_n(D)$ by minimizing $(I(X^n;Y)-I(Y;B^n))/n$ over every finite nonempty classical auxiliary alphabet, every stochastic channel $W(y\mid x^n)$ , and every $y$ -controlled reconstruction POVM on $B^n$ , subject to expected average per-letter distortion at most $D$ . All states and Born probabilities are computed from these data, and entropies are in bits. Use value $+\infty$ when the feasible set is empty.

Then for all positive $m,n$ ,

(m+n)V_{m+n}(D)\le mV_m(D)+nV_n(D),\qquad \lim_{n\to\infty}V_n(D)\text{ exists in }[0,+\infty].

Whenever $V_n(D)<+\infty$ , its minimum is attained by a feasible channel and reconstruction POVM.

This concerns only the regularized variational sequence. It does not identify the limit with the literal exact-distortion operational quantity in the defective Theorem 4.2.

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.16, paragraph following Theorem 4.2: subadditivity and existence of the
regularized VARIATIONAL limit, with finite minima attained. No equality with the
literal operational rate-distortion definition (which has an endpoint defect) is claimed. -/
theorem variationalSubadditivity {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) :
    (∀ m n : ℕ, 1 ≤ m → 1 ≤ n →
      ((m + n : ℕ) : ℝ≥0∞) * blockRD E d D (m + n) ≤
        (m : ℝ≥0∞) * blockRD E d D m + (n : ℝ≥0∞) * blockRD E d D n) ∧
    (∃ L : ℝ≥0∞, Tendsto (fun n : ℕ => blockRD E d D (n + 1)) atTop (nhds L)) ∧
    (∀ n : ℕ, 1 ≤ n → blockRD E d D n ≠ ⊤ →
      ∃ P : RDDatum X B n, rdExpected E d P ≤ D ∧
        ENNReal.ofReal (auxCost (iidCQ E n) P.auxiliary / n) = blockRD E d D n) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P42

end

Source

Channel simulation with quantum side information, arXiv:quant-ph/0611008v1, PDF p. 16, Unnumbered result: subadditivity and existence of the regularized variational limit

Read-back

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

Let $X$ and $B$ be nonempty finite types. Let $E$ consist of weights $p_x\ge0$ with $\sum_xp_x=1$ and matrices $\rho_x$ that are positive semidefinite with trace $1$ , for every $x\in X$ , including those with $p_x=0$ . Let $d:X\times X\to\mathbb R$ satisfy $d(x,z)\ge0$ , and let $D\ge0$ . The quantities in the assertion are defined as follows. Write $H(p)=-\sum_xp_x\log_2p_x$ and $S(M)=-\operatorname{Re}\operatorname{tr}(f(M))$ , where $f(t)=t\log_2t$ is applied by continuous functional calculus and $0\log_20=0$ . For a positive block length $t$ , put $p_t(x)=\prod_{i=1}^tp_{x_i}$ and $\rho_x^{(t)}=\bigotimes_{i=1}^t\rho_{x_i}$ . A datum $P$ consists of a positive integer $a$ , a conditional law $v(u\mid x)\ge0$ on $u\in\{0,\ldots,a-1\}$ for every $x\in X^t$ , with $\sum_uv(u\mid x)=1$ , and, for each $u$ , positive semidefinite matrices $M_{u,z}$ , indexed by $z\in X^t$ , satisfying $\sum_zM_{u,z}=I$ . Define $j(u,x)=p_t(x)v(u\mid x)$ , $a_u=\sum_xj(u,x)$ , and $\sigma_u=a_u^{-1}\sum_xj(u,x)\rho_x^{(t)}$ , taking $0^{-1}=0$ , so that $\sigma_u=0$ when $a_u=0$ . Its auxiliary cost and expected distortion are

K_t(P)=H(p_t)+H(a)-H(j)-S\!\left(\sum_xp_t(x)\rho_x^{(t)}\right)+\sum_ua_uS(\sigma_u), \qquad \Delta_t(P)=\sum_{x,u,z}p_t(x)v(u\mid x)\operatorname{Re}\operatorname{tr}(M_{u,z}\rho_x^{(t)}) \,\frac{\sum_{i=1}^td(x_i,z_i)}{t}.

Let $b_t$ be the infimum, in $[0,\infty]$ , of $\max\{K_t(P)/t,0\}$ over such data with $\Delta_t(P)\le D$ ; an empty feasible set has infimum $+\infty$ . The theorem asserts all three statements:

(m+n)b_{m+n}\le mb_m+nb_n\quad(m,n\ge1),\qquad \exists L\in[0,\infty]\;\;b_{n+1}\longrightarrow L,

and, for every $n\ge1$ with $b_n\ne+\infty$ , there exists a datum $P$ satisfying $\Delta_n(P)\le D$ and $\max\{K_n(P)/n,0\}=b_n$ . The limit is allowed to be $+\infty$ , and attainment includes the case $b_n=0$ . No zero diagonal condition is imposed on $d$ , so feasibility is not assumed.

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