Every minimizing sequence converges to the free limit

Open

QAlgorithms.Papers.Independent.Intakethird100.P100.every_minimizer_sequence_converges

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

prove2quantum

Let $H$ have positive finite dimension $N$ , and let $D$ be a compact real-convex set of density matrices containing $I/N$ . Put $E_D(\omega)=\inf_{\rho\in D}S(\omega\Vert\rho)$ , using support-aware relative entropy and natural logarithms. Suppose density matrices $\sigma_n$ converge in full trace norm to a state $\sigma\in D$ . For every selection of attaining states $\widehat\rho_n\in D$ satisfying $S(\sigma_n\Vert\widehat\rho_n)=E_D(\sigma_n)$ , one has

\|\sigma_n-\sigma\|_1\longrightarrow0 \quad\Longrightarrow\quad \|\widehat\rho_n-\sigma\|_1\longrightarrow0.

The conclusion holds for every sequence of minimizers, even when minimizers away from the free limit are nonunique.

Formalization Note The accepted infimum and its attaining comparisons are stored in bits. Multiplication by the positive constant $\log 2$ gives the natural-logarithm values and preserves finiteness and every minimizing equality.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P100

Formal statement

noncomputable section

open Filter

open scoped ENNReal Topology ComplexOrder

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P100

open QAlgorithms.Papers.Independent.Dependency50.P15
  (relativeDistance relativeDistanceValue positiveOperatorRelativeEntropyBits groupedTensorPower)

open QAlgorithms.Papers.Independent.Information100.P54
  (relativeEntropyBits relativeEntanglement)

/-- Corollary, PDF p.3: every selection of attaining states converges to
the free limit. There is no uniqueness hypothesis and no uniform-in-n
small-distance premise; convergence eventually supplies the local threshold. -/
theorem every_minimizer_sequence_converges
    {I : Type*} [Fintype I] [DecidableEq I] [Nonempty I]
    (D : Set (Matrix I I ℂ))
    (hstates : ∀ rho ∈ D, IsDensityMatrix rho)
    (hcompact : IsCompact D) (hconvex : Convex ℝ D)
    (hmixed : (Fintype.card I : ℂ)⁻¹ • (1 : Matrix I I ℂ) ∈ D)
    (sigma : Matrix I I ℂ) (hsigma : sigma ∈ D)
    (sigmaSeq rhoHat : ℕ → Matrix I I ℂ)
    (hseq : ∀ n, IsDensityMatrix (sigmaSeq n))
    (hconverges : Tendsto (fun n => traceNorm (sigmaSeq n - sigma)) atTop (nhds 0))
    (hminimizers : ∀ n, rhoHat n ∈ D ∧
      positiveOperatorRelativeEntropyBits (sigmaSeq n) (rhoHat n) = relativeDistance D (sigmaSeq n)) :
    Tendsto (fun n => traceNorm (rhoHat n - sigma)) atTop (nhds 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P100

end

Source

Continuity of Relative Entropy of Entanglement, arXiv:quant-ph/9910002v1, PDF p. 3, Corollary

Read-back

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

For any finite, nonempty type $I$ with decidable equality, let $D$ be a compact, real-convex set of complex matrices on $I$ , assume every member of $D$ is positive semidefinite with trace $1$ , and assume $d^{-1}\mathbf1\in D$ , where $d=|I|$ . Let $\sigma\in D$ , and let $\sigma_n,\widehat\rho_n$ , for $n\in\mathbb N$ , be sequences of complex matrices on $I$ , with every $\sigma_n$ positive semidefinite of trace $1$ . Define

\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}, \qquad F_D(X)=\inf_{Y\in D}J(X\Vert Y)

as an extended-real infimum, where $J(X\Vert Y)=+\infty$ unless $\ker Y\subseteq\ker X$ , and otherwise

J(X\Vert Y)=\operatorname{Re}\operatorname{tr} \bigl(f_2(X)-X L_2(Y)\bigr), \qquad f_2(x)=x\log_2x,\quad L_2(x)=\log_2x,

using matrix functional calculus with $\log_2 0=0$ . If $\|\sigma_n-\sigma\|_1\to0$ and, for every $n$ , $\widehat\rho_n\in D$ and $J(\sigma_n\Vert\widehat\rho_n)=F_D(\sigma_n)$ , then $\|\widehat\rho_n-\sigma\|_1\to0$ as $n\to\infty$ . The matrices $\sigma_n$ need not belong to $D$ , and no uniqueness assumption is imposed on their chosen minimizers; the limit $\sigma$ itself is required to belong to $D$ .

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