Relative entropy decreases under positive trace-preserving maps

Open

QAlgorithms.Papers.Independent.Intakethird100.P46.relative_entropy_monotonicity

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

prove2quantum

Let $H$ and $H'$ be complex separable Hilbert spaces, let $\mathcal T(H)$ denote all trace-class operators, and let $\Phi:\mathcal T(H)\to\mathcal T(H')$ be complex-linear, positive, and trace-preserving on every positive trace-class input. For arbitrary positive trace-class operators $\rho,\sigma$ , with no trace normalization, support, or finite-entropy assumption,

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

Here $D$ is the literal unnormalized Umegaki relative entropy $\operatorname{tr}[\rho(\log\rho-\log\sigma)]$ in natural units, interpreted as $+\infty$ on support failure or a divergent logarithmic expectation, and $D(0\Vert\sigma)=0$ . This gives data processing under positivity alone.

Formalization Note Arbitrary countable Hilbert bases represent the two separable spaces. The accepted corrected extended divergence is embedded in the extended reals and only the finite correction $\operatorname{tr}\sigma-\operatorname{tr}\rho$ is subtracted.

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.2, Theorem 1, (3).
Countable arbitrary Hilbert bases represent exactly the separable Hilbert-space
setting; no eigenbasis, normalization, support, or finite-entropy premise is used. -/
theorem relative_entropy_monotonicity {I J : Type*} [Countable I] [Countable J]
    (b : HilbertBasis I ℂ H) (c : HilbertBasis J ℂ K)
    (Phi : (H →L[ℂ] H) → (K →L[ℂ] K))
    (hPhi : PositiveTracePreservingBetween b c Phi)
    (rho sigma : TraceClass H) (hrho : IsPositive rho.val) (hsigma : IsPositive sigma.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. 2, Theorem 1: monotonicity of quantum relative entropy under positive trace-preserving maps

Read-back

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

For complex Hilbert spaces $H,K$ , countable index types $I,J$ , Hilbert bases $b=(b_i)_{i\in I}$ and $c=(c_j)_{j\in J}$ , and a function $\Phi$ between bounded complex-linear operators, suppose $\Phi$ preserves trace-class operators, is additive and complex homogeneous on them, and maps every positive trace-class operator to a positive operator with the same complex basis trace. Then, for every pair of positive trace-class operators $\rho,\sigma$ on $H$ ,

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

Here trace class means admitting $Tx=\sum_{r\in\mathbb N}\langle v_r,x\rangle u_r$ with $\sum_r\|u_r\|\|v_r\|$ summable; positivity means $T^*=T$ and $\operatorname{Re}\langle x,Tx\rangle\ge0$ for every $x$ ; the basis trace is $\operatorname{Tr}_bT=\sum_i\langle b_i,Tb_i\rangle$ ; and $L_b(X,Y)=R(X,Y)-(\operatorname{Re}\operatorname{Tr}_bY-\operatorname{Re}\operatorname{Tr}_bX)$ . The value $R(X,Y)$ is the supremum in $[0,\infty]$ over all finite orthonormal families, including the empty family, of the compressed-matrix quantity: for compressions $A_{ij}=\langle v_i,Xv_j\rangle$ , $B_{ij}=\langle v_i,Yv_j\rangle$ , take $+\infty$ when $\ker B\nsubseteq\ker A$ , and otherwise take $\max\{0,\operatorname{Re}\operatorname{Tr}(f(A)-A\log B-A+B)\}$ , where $f(x)=x\log x$ and matrix functions use continuous functional calculus. The outputs in the inequality carry the trace-class membership supplied by $\Phi$ . Neither input must have trace one or be nonzero, and infinite entropy values 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