Relative entropy decreases when a positive trace-nonincreasing map preserves the first input trace

Open

QAlgorithms.Papers.Independent.Intakethird100.P46.relative_entropy_monotonicity_trace_nonincreasing

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

prove2quantum

Let $H,H'$ be complex separable Hilbert spaces, and let $\Phi:\mathcal T(H)\to\mathcal T(H')$ be complex-linear, positive, and trace-nonincreasing on every positive trace-class input. Let $\rho,\sigma\ge0$ be trace-class operators satisfying only the additional local equality $\operatorname{tr}\Phi(\rho)=\operatorname{tr}\rho$ . Then

D(\Phi(\rho)\Vert\Phi(\sigma))\le D(\rho\Vert\sigma).

The divergence $D$ is the unnormalized natural-log Umegaki relative entropy, with extended values and $D(0\Vert\sigma)=0$ . No trace condition is imposed on $\sigma$ , no global trace preservation is required, and no support or entropy-finiteness assumption is made. This identifies the input-dependent trace condition that suffices beyond trace-preserving maps.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P46

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder ENNReal

namespace QAlgorithms.Papers.Independent.Intakethird100.P46

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms

open QAlgorithms.Papers.Independent.Dependency50.P13
  (IsTraceClass TraceClass IsPositive operatorTrace)

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

open QAlgorithms.Papers.Independent.Bridge50.P49 (beigiSandwichedDivergence)

variable {H K : Type*}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]

/-- Müller-Hermes–Reeb, arXiv:1512.06117v3, PDF p.3, Theorem 1', (6).
Global trace nonincrease is supplemented by trace preservation only at rho.
Neither global trace preservation nor preservation at sigma is assumed. -/
theorem relative_entropy_monotonicity_trace_nonincreasing
    {I J : Type*} [Countable I] [Countable J]
    (b : HilbertBasis I ℂ H) (c : HilbertBasis J ℂ K)
    (Phi : (H →L[ℂ] H) → (K →L[ℂ] K))
    (hPhi : PositiveTraceNonincreasingBetween b c Phi)
    (rho sigma : TraceClass H) (hrho : IsPositive rho.val) (hsigma : IsPositive sigma.val)
    (hTrace : operatorTrace c (Phi rho.val) = operatorTrace b rho.val) :
    literalTraceClassRelativeEntropy c
        (traceClassImage Phi hPhi.1 rho) (traceClassImage Phi hPhi.1 sigma) ≤
      literalTraceClassRelativeEntropy b rho sigma := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P46

end

Source

Monotonicity of the Quantum Relative Entropy Under Positive Maps, arXiv:1512.06117v3, PDF p. 3, Theorem 1′: relative-entropy monotonicity for trace-nonincreasing maps preserving tr(ρ)

Read-back

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

Let $H$ and $K$ be complete complex inner product spaces, let $I,J$ be countable index types, and let $b=(b_i)_{i\in I}$ and $c=(c_j)_{j\in J}$ be Hilbert bases of $H$ and $K$ , respectively. Here a bounded complex linear operator $T$ is called trace class if there exist sequences $u_r,v_r$ such that $\sum_r\|u_r\|\|v_r\|$ converges and $Tx=\sum_r\langle v_r,x\rangle u_r$ for every $x$ ; write $\operatorname{Tr}_b(T)=\sum_i\langle b_i,Tb_i\rangle$ , and call $T$ positive when $T^*=T$ and $\operatorname{Re}\langle x,Tx\rangle\ge0$ for every $x$ . Let $\Phi$ map bounded complex linear operators on $H$ to such operators on $K$ . Assume that $\Phi$ maps trace-class operators to trace-class operators, is additive and complex homogeneous on trace-class operators, and, for every positive trace-class $T$ , satisfies $\Phi(T)\ge0$ and $\operatorname{Re}\operatorname{Tr}_c(\Phi(T))\le\operatorname{Re}\operatorname{Tr}_b(T)$ . Let $\rho,\sigma$ be positive trace-class operators, and assume the complex trace equality $\operatorname{Tr}_c(\Phi(\rho))=\operatorname{Tr}_b(\rho)$ . To specify the asserted quantity, for positive semidefinite finite matrices $X,Y$ , put

F(X,Y)= \begin{cases} \max\!\left\{0,\operatorname{Re}\operatorname{tr}\!\left(f(X)-X\log Y-X+Y\right)\right\}, &\ker Y\subseteq\ker X,\\ +\infty,&\text{otherwise}, \end{cases} \qquad f(t)=t\log t,

where the matrix functions use continuous functional calculus and the logarithm is natural, with its total real convention $\log0=0$ . For trace-class $R,S$ on either space, define

\mathcal R(R,S)= \sup_{\substack{n\in\mathbb N\\v_0,\ldots,v_{n-1}\text{ orthonormal}}} F\!\left( [\langle v_i,Rv_j\rangle]_{i,j}, [\langle v_i,Sv_j\rangle]_{i,j} \right), \qquad L_b(R,S)=\mathcal R(R,S) -\left(\operatorname{Re}\operatorname{Tr}_b(S)-\operatorname{Re}\operatorname{Tr}_b(R)\right).

The supremum defining $\mathcal R$ is taken in $[0,+\infty]$ , and $L_b$ is valued in the extended real numbers. Then

L_c(\Phi(\rho),\Phi(\sigma))\le L_b(\rho,\sigma).

Neither input is required to have trace one or to be nonzero; zero-dimensional spaces and the empty orthonormal family $n=0$ are included.

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