Example 1 and Appendix A / LP (72): depolarizing finite-blocklength cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.depolarizing_block_lp

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

prove2quantum

All systems have finite positive dimension and fixed computational bases. Matrix order is Loewner order and logarithms are base two.

Let $d\ge1$ , $0\le p\le1$ , $\varepsilon\ge0$ , and $n\ge0$ . For $k=0,\ldots,n$ put $q_1=d(1-p)+p/d$ , $q_2=p/d$ , $p_k=q_1^kq_2^{n-k}$ , and $w_k=\binom nk(1/d)^k(d-1/d)^{n-k}$ . Minimize $d^ns$ over real $s,y_k,r_k$ subject to $y_k-r_k+p_k\ge0$ , $y_k\ge0$ , $0\le r_k\le s$ , $\sum_kw_kr_k=1$ , and $\sum_kw_ky_k\le\varepsilon$ ; denote its infimum by $t$ . Then

S_{\rm NS,\varepsilon}^{(1)}(\mathcal D_p^{\otimes n})=\log_2\lceil\sqrt t\rceil.

An optimal solution of the channel SDP exists with $J=\sum_kr_kP_k^n$ , $Y=\sum_ky_kP_k^n$ , and $V=sI_{d^n}$ , attaining the trace objective $d^ns$ . Here $P_k^n$ sums all products with exactly $k$ normalized maximally entangled projectors and $n-k$ orthogonal complements. Empty products and $0^0$ equal one, retaining the scalar boundaries.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P65

Formal statement

noncomputable section

open Filter QAlgorithms

open scoped BigOperators Matrix ComplexConjugate ComplexOrder Topology

namespace QAlgorithms.Papers.Independent.Intakethird100.P65

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Dependency50.P09 (transposeBob)

open QAlgorithms.Papers.Independent.Dependency50.P35 (maxRelative)

open QAlgorithms.Papers.Independent.Independent2.P01 (dampingKraus damping)

open QAlgorithms.Papers.Independent.Gap48.P33 (phaseFlipChannel)

open QAlgorithms.Papers.Independent.Information100.P06 (Below)

open QAlgorithms.Papers.Independent.Information100.P34 (choi)

open QAlgorithms.Papers.Independent.Information100.P62 (Stochastic)

open QAlgorithms.Papers.Independent.Information100.P63 (Mat)

open QAlgorithms.Papers.Independent.Information100.P67 (IsSubnormalized purifiedDistance)

open QAlgorithms.Papers.Independent.Information100.P69 (replacer permute)

open QAlgorithms.Papers.Independent.Information100.P71 (diamond channelPower channelRelative)

open QAlgorithms.Papers.Independent.Support50.P39 (quantumMutualInformation)

variable {A B C D R : Type} [Fintype A] [DecidableEq A]
  [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C]
  [Fintype D] [DecidableEq D] [Fintype R] [DecidableEq R]

variable [Nonempty A] [Nonempty B] [Nonempty C] [Nonempty D] [Nonempty R]

/-- Example 1 and Appendix A, Eqs.(71)--(72), PDF pp.13,18: finite-blocklength
LP and an attained SDP optimum of the symmetric form. n=0 and d=1 are meaningful
with the usual empty-product and 0^0=1 conventions. -/
theorem depolarizing_block_lp (p e : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) (he : 0 ≤ e) (n : ℕ) :
    oneUseSimulationCost .ns (channelPower (basisDepolarizing A p) n) e =
      roundedTraceCost (depolarizingValue (Fintype.card A) n p e) ∧
    ∃ s : ℝ, ∃ y r : Fin (n+1) → ℝ,
      depolarizingFeasible (Fintype.card A) n p e s y r ∧
      traceFeasible (channelPower (basisDepolarizing A p) n) e
        (sectorMatrix A n y) (sectorMatrix A n r) ((s : ℂ) • (1 : Mat (Fin n → A))) ∧
      (Fintype.card A : ℝ)^n * s = traceValue (channelPower (basisDepolarizing A p) n) e := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P65

end

Source

Quantum Channel Simulation and the Channel's Smooth Max-Information, arXiv:1807.05354v2, PDF p. 18, Example 1 and Appendix A / LP (72): depolarizing finite-blocklength cost

Read-back

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

For a finite type $A$ with decidable equality, real numbers $0\le p\le1$ and $e\ge0$ , and every natural $n$ , put $d=|A|$ , $\mathcal D_p(X)=(1-p)X+(p/d)\operatorname{tr}(X)I_A$ , and $H=\mathcal D_p^{\otimes n}$ , where tensor powers are defined by products of matrix-unit entries. Define

w_k=\binom nk d^{-k}(d-d^{-1})^{n-k},\qquad a_k=\bigl(d(1-p)+p/d\bigr)^k(p/d)^{n-k}.

Let $v$ be the real infimum of $d^ns$ over real $s$ and vectors $y,r\in\mathbb R^{n+1}$ satisfying, for every $0\le k\le n$ ,

0\le y_k-r_k+a_k,\quad y_k\ge0,\quad 0\le r_k\le s,\qquad \sum_{k=0}^nw_kr_k=1,\quad \sum_{k=0}^nw_ky_k\le e.

Then $c_{\mathrm{ns}}(H,e)=\log_2\lceil\sqrt v\rceil$ . Moreover, there exist $s,y,r$ satisfying these constraints for which $Y=\sum_ky_kP_k$ , $J=\sum_kr_kP_k$ , and $V=sI_{A^n}$ satisfy $V=V^\dagger$ , $Y,J\succeq0$ , $\operatorname{Tr}_{B^n}Y\preceq eI_{A^n}$ , $J-J_H\preceq Y$ , $\operatorname{Tr}_{B^n}J=I_{A^n}$ , and $J\preceq I_{A^n}\otimes V$ , and $d^ns$ equals the real infimum of $\operatorname{Re}\operatorname{tr}V'$ over all triples $Y',J',V'$ satisfying those same matrix constraints. Here $J_H((a,b),(a',b'))=H(|a\rangle\langle a'|)_{b,b'}$ ; $P_k$ is the sum over all $k$ -element subsets $S\subseteq\{0,\ldots,n-1\}$ of $\bigotimes_i Q_i$ , with $Q_i=\Phi_A$ for $i\in S$ and $Q_i=I-\Phi_A$ otherwise, where $\Phi_A((a,b),(a',b'))=d^{-1}$ if $a=b$ and $a'=b'$ , and is $0$ otherwise. The cost $c_{\mathrm{ns}}(H,e)$ is the infimum of $\log_2m$ over positive integers $m$ whose infimum error using the $m$ -dimensional identity channel is at most $e$ : the error is $\inf_P\|\mathcal W_m(P)-H\|_\diamond/2$ , where $P$ is a channel with each output marginal determined only by its corresponding input marginal and $\mathcal W_m(P)(X)_{b,d}=\sum_{a,c<m}P(X\otimes|a\rangle\langle c|)_{(a,b),(c,d)}$ . Channels are finite normalized Kraus maps, and $\|F\|_\diamond=\sup_{\|X\|_1\le1}\|(\mathrm{id}_{A^n}\otimes F)(X)\|_1$ , over arbitrary matrices on $A^n\times A^n$ , with $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ . The assertion includes $n=0$ , where the string register is a singleton, empty tensor products equal $1$ , and the scalar constraints force $r_0=1$ and $s\ge1$ . No upper bound on $e$ or displayed nonemptiness condition on $A$ is imposed; division by zero is $0$ , real infima default to $0$ when empty or unbounded below, and the rounding uses the natural-number ceiling with $\log_2 0=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