Existence and finiteness of a closest feasible state

Open

QAlgorithms.Papers.Independent.Intakethird100.P100.relativeDistance_finite_and_attained

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

prove2quantum

Let $H$ have arbitrary positive finite dimension $N$ , and let $D$ be a compact real-convex set of density matrices containing $I/N$ . Use natural logarithms and define the extended infimum $E_D(\sigma)=\inf_{\rho\in D}S(\sigma\Vert\rho)$ , with infinite relative entropy at a support violation. Then every density matrix $\sigma$ has finite distance and an attaining feasible state:

E_D(\sigma)<\infty, \qquad \exists\,\widehat\rho\in D:\quad S(\sigma\Vert\widehat\rho)=E_D(\sigma).

This makes the notion of a closest feasible state well-defined as a nonempty set of optimizers. It does not assert uniqueness or positive definiteness of an optimizer.

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)

/-- Proof, PDF p.2: every state has a finite distance attained by a state
in D. All assumptions on D from the theorem are carried forward. Minimizers
may be singular and are not required to be unique. -/
theorem relativeDistance_finite_and_attained
    {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 : IsDensityMatrix sigma) :
    0 ≤ relativeDistance D sigma ∧ relativeDistance D sigma < ⊤ ∧
      ∃ rhoHat ∈ D,
        positiveOperatorRelativeEntropyBits sigma rhoHat = relativeDistance D sigma := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P100

end

Source

Continuity of Relative Entropy of Entanglement, arXiv:quant-ph/9910002v1, PDF p. 2, Proof: construction of rho-hat

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$ , all positive semidefinite with trace $1$ , and suppose that $d^{-1}\mathbf1\in D$ , where $d=|I|$ . For every positive semidefinite, trace- $1$ matrix $\sigma$ on $I$ , the extended-real quantity

F_D(\sigma)=\inf_{\rho\in D}J(\sigma\Vert\rho)

satisfies $0\le F_D(\sigma)<+\infty$ , and there exists $\widehat\rho\in D$ such that $J(\sigma\Vert\widehat\rho)=F_D(\sigma)$ . Here $J(X\Vert Y)$ is $+\infty$ if $\ker Y\not\subseteq\ker X$ , and otherwise is

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,

with the matrix functions defined by functional calculus and $\log_2 0=0$ . The inclusion of the maximally mixed matrix makes $D$ nonempty. The assertion is existence of a minimizing matrix, with no uniqueness assertion, and includes $d=1$ .

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