Continuity of distance to a compact convex state set

Open

QAlgorithms.Papers.Independent.Intakethird100.P100.compactConvex_relativeDistance_continuity

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

prove2quantum

Let $H$ be a complex Hilbert space of arbitrary positive finite dimension $N$ . Let $D$ be a compact, real-convex set of density matrices containing $I/N$ . Define $E_D(\omega)=\inf_{\tau\in D}S(\omega\Vert\tau)$ , where the relative entropy is infinite if $\operatorname{supp}\omega\not\subseteq\operatorname{supp}\tau$ .

All logarithms are natural. States are positive semidefinite matrices of trace one, and the distance $t=\|\sigma-\rho\|_1$ uses the full trace norm, without a factor of one half. Set $\eta(t)=-t\log t$ , with $\eta(0)=0$ .

For any density matrices $\sigma,\rho$ with $t\leq 1/3$ , the values $E_D(\sigma),E_D(\rho)$ are finite and

|E_D(\sigma)-E_D(\rho)|\leq 2\bigl(t\log N+\eta(t)\bigr)+4t.

This bound applies to a general compact convex state set, without requiring a bipartite system.

Formalization Note The accepted entropy infimum is stored in bits. The Lean bound multiplies its absolute real difference by $\log 2$ , which gives exactly the natural-logarithm quantity displayed above.

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)

/-- Theorem (3), PDF pp.2–3: continuity for every compact real-convex
set of normalized states containing I/N, in arbitrary positive finite dimension.
Finiteness is asserted, rather than assumed before taking real differences. -/
theorem compactConvex_relativeDistance_continuity
    {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)
    (sigmaOne sigmaTwo : Matrix I I ℂ)
    (hOne : IsDensityMatrix sigmaOne) (hTwo : IsDensityMatrix sigmaTwo)
    (hclose : traceNorm (sigmaOne - sigmaTwo) ≤ 1 / 3) :
    0 ≤ relativeDistance D sigmaOne ∧ relativeDistance D sigmaOne < ⊤ ∧
    0 ≤ relativeDistance D sigmaTwo ∧ relativeDistance D sigmaTwo < ⊤ ∧
    Real.log 2 * |relativeDistanceValue D sigmaOne - relativeDistanceValue D sigmaTwo| ≤
      2 * (traceNorm (sigmaOne - sigmaTwo) * Real.log (Fintype.card I) +
        Real.negMulLog (traceNorm (sigmaOne - sigmaTwo))) +
      4 * traceNorm (sigmaOne - sigmaTwo) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P100

end

Source

Continuity of Relative Entropy of Entanglement, arXiv:quant-ph/9910002v1, PDF p. 2, Theorem, equation (3)

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|$ . For any density matrices $\sigma_1,\sigma_2$ on $I$ , put $t=\operatorname{Re}\operatorname{tr}\sqrt{(\sigma_1-\sigma_2)^\dagger(\sigma_1-\sigma_2)}$ . If $t\le1/3$ , then

0\le F_D(\sigma_1)<+\infty,\qquad 0\le F_D(\sigma_2)<+\infty,\qquad (\ln2)\left|F_D(\sigma_1)_{\mathbb R}-F_D(\sigma_2)_{\mathbb R}\right| \le2\bigl(t\ln d-t\ln t\bigr)+4t.

Here $F_D(X)=\inf_{Y\in D}J(X\Vert Y)$ is an infimum in the extended reals, where

J(X\Vert Y)= \begin{cases} \operatorname{Re}\operatorname{tr}\bigl(f_2(X)-X L_2(Y)\bigr), &\ker Y\subseteq\ker X,\\ +\infty,&\text{otherwise}, \end{cases} \quad f_2(x)=x\log_2x,\quad L_2(x)=\log_2x.

These matrix functions are defined by functional calculus, taking $\log_2 0=0$ . The subscript $\mathbb R$ denotes the real conversion of an extended real, which sends both infinities to $0$ ; the displayed bounds exclude infinities for these two arguments. The hypothesis includes $t=0$ , with $t\ln t=0$ , and allows $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