The regularized exact rate is an asymptotic limit

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.deterministicRegularization

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

prove2quantum

Let $\rho$ be any normalized finite-dimensional bipartite state. Define $E_1(\rho)$ independently as the supremum of $\log_2 k$ over real $k>0$ with $F_\Gamma(\rho,k)=1$ , and define $E_{\Gamma,0}(\rho)$ by the supremum of positive-blocklength ratios. Then

\lim_{n\to\infty,\ n\ge1}\frac{E_1(\rho^{\otimes n})}{n}=E_{\Gamma,0}(\rho):=\sup_{n\ge1}\frac{E_1(\rho^{\otimes n})}{n}.

The limit is through positive integers and is finite. This is a regularization statement and does not assert additivity of the one-copy rate.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P83

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P83

open QAlgorithms.Papers.Independent.Support50.P11 (Loewner)

open QAlgorithms.Papers.Independent.Dependency50.P32 (partialTranspose)

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

variable {A B C D : Type*}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

/-- The asymptotic formula on PDF p.4. The printed subscript "lim_{n>=1}"
is interpreted as n tending to infinity through positive blocklengths;
exactRegularized is independently defined by a supremum, not by this limit. -/
theorem deterministicRegularization [Nonempty A] [Nonempty B]
    (rho : Matrix (A × B) (A × B) ℂ) (hrho : IsDensityMatrix rho) :
    Tendsto (fun n : ℕ => oneCopyExact (regroupedPower rho (n+1)) / (n+1 : ℝ))
      atTop (nhds (exactRegularized rho)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P83

end

Source

Improved Semidefinite Programming Upper Bound on Distillable Entanglement, arXiv:1601.07940v4, PDF p. 4, Unnumbered result: regularization equals the asymptotic limit

Read-back

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

For any finite nonempty types $A,B$ with decidable equality and any positive semidefinite complex matrix $\rho$ indexed by $A\times B$ with trace $1$ , define $X^\Gamma_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , and let $F_X(k)$ be the real supremum of $\operatorname{Re}\operatorname{tr}(XQ)$ over matrices $Q$ satisfying $k>0$ , $0\preceq Q\preceq I$ , and $-k^{-1}I\preceq Q^\Gamma\preceq k^{-1}I$ , where $\preceq$ means positive semidefinite difference. Let $D(X)$ be the real supremum of $\log_2 k$ over real $k>0$ for which $F_X(k)=1$ , let $X^{\otimes m}$ have entries $\prod_{i=0}^{m-1}X_{(a_i,b_i),(a'_i,b'_i)}$ , and define $D_{\mathrm{reg}}(\rho)=\sup_{m\ge1}D(\rho^{\otimes m})/m$ , again as a real supremum. Then

\lim_{n\to\infty}\frac{D(\rho^{\otimes(n+1)})}{n+1}=D_{\mathrm{reg}}(\rho).

Here $n$ ranges over all natural numbers, so the sequence begins with the one-copy value and never divides by zero.

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