16 Quantum relative entropy and its monotonicity
The multiplicative ergodic machinery of the preceding chapters is built on the continuous functional calculus of self-adjoint matrices. That same finite-dimensional matrix and CFC infrastructure supports a second, logically independent development: a finite-dimensional quantum-information layer. This chapter documents its foundational half — the entropies of a finite quantum system and the master inequality controlling how they behave under quantum channels.
The objects are density matrices: positive semidefinite complex matrices of unit trace, the finite-dimensional states of a quantum system. Attached to a state \(\rho \) is its von Neumann entropy \(S(\rho )\), and to a pair \(\rho ,\sigma \) the Umegaki relative entropy \(S(\rho \| \sigma ) = \operatorname{Tr}\bigl(\rho (\log \rho -\log \sigma )\bigr)\), the finite-dimensional distinguishability functional of quantum information theory. The central theorem, the data-processing inequality, states that no quantum channel can increase relative entropy: distinguishability can only degrade under physical processing. We reach it through Lieb’s 1973 theorem on the joint convexity of relative entropy (Lieb 1973), following the modern route of Carlen’s Trace Inequalities and Quantum Entropy via the Effros operator perspective, and close with the easy half of Petz’s equality theorem (Petz 1986, 2003) — recovery implies saturation — whose hard converse (saturation implies the existence of a Petz recovery map) is treated separately.
Everything in this chapter is formalized sorry-free, on the same matrix/CFC foundations as the multiplicative ergodic theorem, and is verified by the guarded axiom audit to rest only on \(\{ \texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}\} \). Throughout, \(n\) is a finite index type, matrices are complex \(n\times n\) acting on \(\mathbb {C}^n\), and \(\operatorname{Tr}\) is the matrix trace.
16.1 Density matrices and von Neumann entropy
For a finite index type \(n\), a density matrix is a structure bundling a matrix \(\rho \in \operatorname {Matrix}_n(\mathbb {C})\) together with proofs that \(\rho \) is positive semidefinite and has unit trace, \(\operatorname{Tr}\rho = 1\). It is the finite-dimensional state of a quantum system on \(\mathbb {C}^n\).
The real eigenvalues \(\lambda _i\) of a density matrix \(\rho \) are nonnegative, each at most \(1\), and sum to \(1\): \(\sum _i \lambda _i = \operatorname{Tr}\rho = 1\).
Positive semidefiniteness gives \(\lambda _i\ge 0\). The Hermitian spectral theorem identifies \(\operatorname{Tr}\rho \) with \(\sum _i\lambda _i\) as a complex number; casting the hypothesis \(\operatorname{Tr}\rho = 1\) back to \(\mathbb {R}\) yields \(\sum _i\lambda _i = 1\). Each \(\lambda _i\le 1\) is then a single term bounded by the sum of the nonnegative terms.
The von Neumann entropy of a density matrix \(\rho \) with eigenvalues \(\lambda _i\) is
using Mathlib’s \(\operatorname {negMulLog}(x) = -x\log x\), so the convention \(0\log 0 = 0\) is built in.
\(S(\rho )\ge 0\) for every density matrix \(\rho \).
Each eigenvalue satisfies \(0\le \lambda _i\le 1\), and on \([0,1]\) one has \(\operatorname {negMulLog}(x) = -x\log x\ge 0\). The entropy is a sum of these nonnegative terms.
We record the partial trace here, as it is the elementary operation underlying both the reduced states of a bipartite system and the data-processing inequality.
For an operator \(M\) on a bipartite system \(\mathbb {C}^{n_A}\otimes \mathbb {C}^{n_B}\), the partial trace over the \(B\) factor is
an operator on \(\mathbb {C}^{n_A}\). (The left partial trace \(\operatorname{Tr}_A\) is defined symmetrically.)
\(\operatorname{Tr}(\operatorname{Tr}_B M) = \operatorname{Tr}M\).
Both sides expand to the full double sum \(\sum _{i,j} M_{(i,j),(i,j)}\) over the product index set; a reindexing of the finite sum finishes.
If \(M\) is positive semidefinite then so is \(\operatorname{Tr}_B M\).
Write the partial trace in Kraus/compression form \(\operatorname{Tr}_B M = \sum _j E_j^{*} M E_j\), the sum of the conjugations of \(M\) by the block-inclusion isometries \(E_j : i\mapsto (i,j)\). Each compression \(E_j^{*} M E_j\) is positive semidefinite, and a finite sum of positive semidefinite matrices is positive semidefinite.
16.2 Maximum entropy and strict positivity
Beyond nonnegativity, the von Neumann entropy is pinned between two spectral extremes. From above it is bounded by the logarithm of the rank — the finite-dimensional maximum-entropy principle, saturated by the maximally mixed state on the support — and from below it is strictly positive unless the state is pure. Both are consequences of the same eigenvalue analysis, and the upper bound is powered by a single uniform-weight Jensen lemma shared verbatim with the classical entropy layer of Chapter 10.
For a probability vector \(p\) supported on a nonempty finite set \(s\) (\(p_i\ge 0\) and \(\sum _{i\in s}p_i = 1\)), the entropy sum is bounded by the log-cardinality,
with equality at the uniform distribution \(p\equiv 1/\left\lvert s \right\rvert \).
The concave Jensen inequality (\(\texttt{ConcaveOn.le\_ map\_ sum}\)) for \(\operatorname {negMulLog}\) with the uniform weights \(w_i = \left\lvert s \right\rvert ^{-1}\) gives \(\left\lvert s \right\rvert ^{-1}\sum _i\operatorname {negMulLog}(p_i)\le \operatorname {negMulLog}\bigl(\left\lvert s \right\rvert ^{-1}\sum _i p_i\bigr) = \operatorname {negMulLog}(\left\lvert s \right\rvert ^{-1})\); evaluating \(\operatorname {negMulLog}(\left\lvert s \right\rvert ^{-1}) = \left\lvert s \right\rvert ^{-1}\log \left\lvert s \right\rvert \) and cancelling the positive factor \(\left\lvert s \right\rvert ^{-1}\) gives the claim. This is factored out of both entropy layers so the single Jensen argument is not inlined twice.
The rank of a density matrix is strictly positive, \(0 {\lt} \operatorname {rank}\rho \).
The eigenvalues sum to \(1\ne 0\) (Lemma 16.2), so at least one is nonzero; the rank of a Hermitian matrix is the number of nonzero eigenvalues (\(\texttt{IsHermitian.rank\_ eq\_ card\_ non\_ zero\_ eigs}\)), hence at least \(1\).
The von Neumann entropy of a density matrix is at most the logarithm of its rank,
Among all states supported on a \(k\)-dimensional subspace, the maximally mixed state — with entropy \(\log k\) — is the most disordered.
Restrict the entropy sum \(S(\rho ) = \sum _i\operatorname {negMulLog}(\lambda _i)\) to the support \(s = \{ i : \lambda _i\ne 0\} \); the off-support terms vanish because \(\operatorname {negMulLog}(0) = 0\), and the restricted eigenvalues still sum to \(1\). The support cardinality equals the rank (\(\texttt{IsHermitian.rank\_ eq\_ card\_ non\_ zero\_ eigs}\)) and is positive (Lemma 16.9), so the uniform-weight Jensen bound (Lemma 16.8) applied on \(s\) gives \(S(\rho )\le \log \left\lvert s \right\rvert = \log (\operatorname {rank}\rho )\).
\(S(\rho )\le \log (\# n)\), the logarithm of the ambient Hilbert-space dimension.
The rank never exceeds the number of columns, \(\operatorname {rank}\rho \le \# n\); monotonicity of \(\log \) applied to Theorem 16.10 gives the bound.
If a density matrix is not idempotent (\(\rho ^2\ne \rho \)) then its von Neumann entropy is strictly positive, \(0 {\lt} S(\rho )\). Equivalently, a zero-entropy state is a pure state — a rank-one projection.
Entropy is a sum of nonnegative terms (Theorem 16.4), so \(S(\rho ) = 0\) forces every \(\operatorname {negMulLog}(\lambda _i) = 0\); since each \(\lambda _i\in [0,1]\) this drives every eigenvalue to \(\{ 0,1\} \). A diagonal matrix with \(\{ 0,1\} \) entries is idempotent, and idempotency is transported through the spectral unitary (a \(*\)-algebra automorphism, hence multiplicative), yielding \(\rho ^2 = \rho \) — contradicting the hypothesis. Hence \(S(\rho ) {\gt} 0\).
16.3 Explicit block-inclusion Kraus form of the partial trace
The complete positivity of Lemma 16.7 was read off a Kraus decomposition \(\operatorname{Tr}_B M = \sum _j E_j M E_j^{*}\) into block-inclusion isometries. We now record that decomposition as a literal theorem with the Kraus operators named as honest matrices — the Stinespring presentation of the partial trace — together with the two structural identities the block operators satisfy. Naming the operators as concrete \(\operatorname {Matrix}\)-typed \(\texttt{def}\)s (rather than bare lambdas) is the load-bearing point of issue #25: it resolves the \(\texttt{CStarMatrix}/\operatorname {Matrix}\) multiplication-elaboration ambiguity that a bare lambda triggers against \(*\).
For each \(j\in n_B\), the right block-inclusion operator \(E_j\in \operatorname {Matrix}_{n_A,\, n_A\times n_B}(\mathbb {C})\) is the co-isometry onto the \(A\)-factor picking out the \(j\)-th \(B\)-slice,
The left block-inclusion operator \(F_i\in \operatorname {Matrix}_{n_B,\, n_A\times n_B}(\mathbb {C})\), \((F_i)_{b,\, (i',b')} = [\, (i',b') = (i,b)\, ]\), is defined symmetrically for the \(A\)-factor.
The conjugation \(E_j M E_j^{*}\) is exactly the \((j,j)\)-diagonal block of \(M\), the submatrix \(M_{(a,j),(a',j)}\) on the \(A\)-index.
Entrywise: the two \(E_j\)-factors select the row index \((a,j)\) and column index \((a',j)\) through the indicator, leaving \(M_{(a,j),(a',j)}\), which is the asserted \(\texttt{submatrix}\).
Both partial traces are genuine sums of Kraus conjugations:
The left analogue is partialTraceLeft_eq_kraus.
By Lemma 16.14 each summand \(E_j M E_j^{*}\) is the \(j\)-th diagonal block submatrix; summing the diagonal blocks over \(j\) is precisely the block-compression form of the partial trace already established for \(\operatorname{Tr}_B\) (and symmetrically for \(\operatorname{Tr}_A\)).
Each block inclusion is a co-isometry onto its factor: for every \(j\), \(E_j E_j^{*} = 1\) on \(\mathbb {C}^{n_A}\), and symmetrically \(F_i F_i^{*} = 1\) on \(\mathbb {C}^{n_B}\) .
\((E_j E_j^{*})_{a,a'} = \sum _{(a'',j')}[\, (a'',j') = (a,j)\, ][\, (a'',j') = (a',j)\, ] = [\, a = a'\, ]\), the identity on the \(A\)-factor.
The block inclusions satisfy the Kraus completeness / trace-preservation relation on the full \(A\otimes B\) space,
The left analogue is sum_conjTranspose_mul_krausInclusionLeft.
\(\bigl(\sum _j E_j^{*}E_j\bigr)_{(p),(p')} = \sum _{a,j}[\, p = (a,j)\, ][\, p' = (a,j)\, ] = [\, p = p'\, ]\), the identity on \(\mathbb {C}^{n_A\times n_B}\). This is a genuinely different identity from the co-isometry Lemma 16.16: summing that one instead gives \(\sum _j E_j E_j^{*} = \# n_B\cdot 1\), not \(1\).
16.4 Umegaki relative entropy and Klein’s inequality
The Umegaki relative entropy of \(\rho \) with respect to \(\sigma \) is \(S(\rho \| \sigma ) = \operatorname{Tr}\rho (\log \rho - \log \sigma )\). It is defined in the concrete spectral/overlap form
where \((p_k,e_k)\) are the eigenvalues/eigenvectors of \(\rho \) and \((q_m,f_m)\) those of \(\sigma \). The definition is total: with the convention \(\log 0 = 0\) the \(\sigma \)-singular columns contribute \(0\).
For faithful (positive definite) \(\sigma \), the spectral definition agrees with the textbook trace form
where \(\log \rho ,\log \sigma \) are the Hermitian continuous functional calculus of the real logarithm.
Expand both eigendecompositions. The trace–spectral bridge \(\Re \, \operatorname{Tr}(\rho \, f(\tau )) = \sum _{k,m} p_k\left\lvert \langle e_k\mid g_m\rangle \right\rvert ^2 f(q_m)\) (proved once, entrywise, via the spectral theorem and the identity \(z\bar z = \left\lvert z \right\rvert ^2\)) identifies \(\Re \, \operatorname{Tr}(\rho \log \rho )\) with \(\sum _k p_k\log p_k\) (the overlap of \(\rho \) with itself is the identity) and \(\Re \, \operatorname{Tr}(\rho \log \sigma )\) with the cross double sum. Distributing over the difference gives the claim.
For faithful (positive definite) \(\sigma \), \(\; 0\le S(\rho \| \sigma )\).
The overlap matrix \(D_{km} = \left\lvert \langle e_k\mid f_m\rangle \right\rvert ^2\) is doubly stochastic: writing \(Q = \rho .\mathrm{eigVec}^{*}\, \sigma .\mathrm{eigVec}\), both \(QQ^{*} = 1\) and \(Q^{*}Q = 1\) (the eigenvector unitaries cancel), giving unit row and column sums. Faithfulness makes every \(q_m {\gt} 0\), so the support side condition is vacuous. Klein’s scalar inequality (Theorem 16.24) then yields \(\sum _{k,m} D_{km}\, p_k\log q_m \le \sum _k p_k\log p_k\), i.e. \(0\le S(\rho \| \sigma )\).
\(S(\rho \| \rho ) = 0\) for every density matrix \(\rho \).
With \(\sigma = \rho \) the overlap matrix \(Q = \rho .\mathrm{eigVec}^{*}\, \rho .\mathrm{eigVec} = 1\), so \(D_{km} = \delta _{km}\). The cross double sum collapses to \(\sum _k p_k\log p_k\), exactly cancelling the first term.
For any unitary \(W\), \(\; S(W\rho W^{*}\, \| \, W\sigma W^{*}) = S(\rho \| \sigma )\), where \(W\rho W^{*}\) denotes the density matrix obtained by conjugating \(\rho \).
Conjugation by \(W\) is a \(*\)-algebra automorphism, so it commutes with the functional calculus: \(\log (W\rho W^{*}) = W(\log \rho )W^{*}\). Hence each trace \(\operatorname{Tr}\bigl((W\rho W^{*})\log (W\tau W^{*})\bigr) = \operatorname{Tr}\bigl(W(\rho \log \tau )W^{*}\bigr) = \operatorname{Tr}(\rho \log \tau )\) by cyclicity of the trace and \(W^{*}W = 1\). Applying this to the two terms of the trace form leaves \(S(\rho \| \sigma )\) unchanged.
Tensoring both arguments with a common faithful ancilla \(\alpha \) leaves the relative entropy unchanged: for faithful \(\sigma \) and faithful \(\alpha \), \(S(\rho \otimes \alpha \, \| \, \sigma \otimes \alpha ) = S(\rho \| \sigma )\).
Relative entropy is additive over Kronecker products, \(S(\rho \otimes \alpha \, \| \, \sigma \otimes \alpha ) = S(\rho \| \sigma ) + S(\alpha \| \alpha )\), and the self-term vanishes by Theorem 16.21.
The nonnegativity above is the operator form of Klein’s inequality; its scalar core, which we isolate next, is the combinatorial engine behind both nonnegativity and the subadditivity of the von Neumann entropy.
Let \(D = (D_{km})\) be a doubly stochastic \(K\times M\) matrix (\(D_{km}\ge 0\), all row sums and all column sums equal to \(1\)), let \(p\ge 0\) on \(K\) and \(s\ge 0\) on \(M\) have equal total mass \(\sum _k p_k = \sum _m s_m\), and assume the support condition \(s_m = 0\Rightarrow D_{km}p_k = 0\). Writing \(a_m = \sum _k D_{km}p_k\) for the column marginal,
This is the finite scalar core of Klein’s inequality (Carlen, Trace Inequalities and Quantum Entropy, Thm. 2.11; Peierls, Thm. 2.9). The termwise Peierls bound \(p - s\le p\log p - p\log s\) (valid for \(p\ge 0\), \(s {\gt} 0\), from \(\log (s/p)\le s/p - 1\)) is scaled by \(D_{km}\ge 0\) and summed over the double index. Double stochasticity makes the mass-balance term \(\sum _{k,m} D_{km}(p_k - s_m)\) telescope to \(\sum _k p_k - \sum _m s_m = 0\); the columns with \(s_m = 0\) contribute nothing by the support hypothesis (there \(a_m = 0\)). Rearranging the summed inequality yields the claim.
For a bipartite density matrix \(\rho \) on \(n_A\otimes n_B\) with reduced density matrices \(\rho _A = \operatorname{Tr}_B\rho \) and \(\rho _B = \operatorname{Tr}_A\rho \), the von Neumann entropy is subadditive:
An elementary route through the scalar Klein inequality, with no matrix logarithm (Carlen, Trace Inequalities and Quantum Entropy, Thm. 2.11; Nielsen–Chuang §11.3). Diagonalize \(\rho = G\, \mathrm{diag}(p)\, G^{*}\), \(\rho _A = U\, \mathrm{diag}(\lambda )\, U^{*}\), \(\rho _B = V\, \mathrm{diag}(\mu )\, V^{*}\) and set \(Q = G^{*}(U\otimes V)\), a unitary. Then \(D_{km} = \left\lvert Q_{km} \right\rvert ^2\) is doubly stochastic, and the conjugation–partial-trace identity \(\operatorname{Tr}_B\bigl((U\otimes V)^{*}\rho (U\otimes V)\bigr) = U^{*}(\operatorname{Tr}_B\rho )U\) (and its left analogue) identifies the marginals of \(D\) with \(\lambda \) and \(\mu \). Feeding \(D\), the eigenvalue vector \(p\), and the product vector \(s_{(i,j)} = \lambda _i\mu _j\) into Theorem 16.24 gives \(\sum _i\eta (\lambda _i) + \sum _j\eta (\mu _j)\ge \sum _k\eta (p_k)\) (with \(\eta (t) = -t\log t\)), which is the assertion after negation.
16.5 Lieb’s joint-convexity theorem
The deep content of quantum relative entropy is Lieb’s 1973 theorem: the map \((\rho ,\sigma )\mapsto S(\rho \| \sigma )\) is jointly convex. We prove it through the Effros operator perspective, whose joint convexity follows in turn from operator convexity of \(-\log \) and the Hansen–Pedersen–Jensen operator-Jensen inequality, following Carlen’s Trace Inequalities and Quantum Entropy.
The function \(x\mapsto -\log x\) is operator convex on \((0,\infty )\): for every matrix dimension its continuous functional calculus is convex in the Loewner order on the self-adjoint matrices with spectrum in \((0,\infty )\).
Transport the statement along the \(\mathbb {R}\)-linear star-algebra equivalence \(\operatorname {Matrix}\simeq \texttt{CStarMatrix}\) (identity on the shared carrier, order- and cfc-preserving) onto the \(C^{*}\)-algebra where Mathlib’s operator concavity of \(\log \) lives. Negating concavity of \(\log \) there and pulling back the Loewner inequality gives convexity of \(-\log \) on \(\operatorname {Matrix}\).
Let \(f\) be operator convex on an interval \(I\), let \(A,B\) be a contraction pair (\(A^{*}A + B^{*}B = 1\)), and let \(X,Y\) be self-adjoint with spectra in \(I\). Then
The Effros / Hansen–Pedersen unitary-dilation method. Work in the doubled algebra \(\operatorname {Matrix}(\operatorname {Fin}2\times \operatorname {Fin}N)\), form the block diagonal \(D = \mathrm{diag}(X,Y)\), dilate the column isometry \([A;B]\) to a unitary \(U\), and pinch \(M = U^{*}DU\) by the involution \(V = \mathrm{diag}(1,-1)\): \(\tfrac 12 M + \tfrac 12 VMV = \mathrm{diag}(M_{00},M_{11})\). Operator convexity of \(f\) at dimension \(2N\), applied to \(M\) and \(VMV\), yields \(f(\mathrm{diag}(M_{00},M_{11}))\le \mathrm{diag}(f(M)_{00},f(M)_{11})\) blockwise, whose \((0,0)\)-block is exactly the asserted inequality. (This node is stated for a general operator-convex \(f\) and specialized below to \(f = -\log \).)
For \(f:\mathbb {R}\to \mathbb {R}\) and matrices \(L,R\) with \(R\) positive definite, the operator perspective is
with the functional calculus and real powers supplied by the continuous functional calculus.
Let \(f\) be operator convex on \(I\), let \(R_1,R_2\) be positive definite with the sandwiched arguments \(R_i^{-1/2}L_iR_i^{-1/2}\) self-adjoint and with spectra in \(I\), and let \(c\in [0,1]\). Then
The Effros argument, a single application of Theorem 16.27. Writing \(R = cR_1 + (1-c)R_2\), the contraction pair \(A = \sqrt{c}\, R_1^{1/2}R^{-1/2}\), \(B = \sqrt{1-c}\, R_2^{1/2}R^{-1/2}\) satisfies \(A^{*}A + B^{*}B = R^{-1/2}RR^{-1/2} = 1\), and the self-adjoint arguments are \(X = R_1^{-1/2}L_1R_1^{-1/2}\), \(Y = R_2^{-1/2}L_2R_2^{-1/2}\). Applying Hansen–Pedersen–Jensen and conjugating the resulting inequality by \(R^{1/2}\) reproduces exactly the joint-convexity estimate, once the sandwich cancellations \(R^{1/2}R^{-1/2} = 1\) are used on both sides.
The same formula \(P_f(L,R) = R^{1/2}f(R^{-1/2}LR^{-1/2})R^{1/2}\) for matrices indexed by an arbitrary finite type \(m\) (rather than \(\operatorname {Fin}N\)).
Under the same hypotheses as Theorem 16.29, joint convexity of \(\mathrm{opPersp}\, f\) holds over an arbitrary finite index type \(m\).
Transport along the star-algebra equivalence \(\operatorname {Matrix}(m)\simeq \operatorname {Matrix}(\operatorname {Fin}(\left\lvert m \right\rvert ))\) (a reindexing), which preserves positive definiteness, self-adjointness, spectra, the continuous functional calculus, real powers, and the Loewner order. Push the pair through the equivalence, invoke Theorem 16.29 on \(\operatorname {Fin}(\left\lvert m \right\rvert )\), and reflect the resulting Loewner inequality back.
For positive-definite \(A,B\), \(\ \log (A\otimes B) = \log A\otimes 1 + 1\otimes \log B\).
Simultaneously diagonalize by \(U_A\otimes U_B\); the Kronecker of the two eigenvalue diagonals is \(\mathrm{diag}(a_i b_j)\), and \(\log (a_i b_j) = \log a_i + \log b_j\) splits the diagonal cfc additively across the two factors. Conjugating back by \(U_A\otimes U_B\) gives the stated Kronecker splitting of \(\log \).
For positive-definite \(\rho ,\sigma \), the perspective of \(-\log \) at the commuting pair \(L = 1\otimes \sigma ^{\top }\), \(R = \rho \otimes 1\) has the closed form
The sandwiched argument is \(R^{-1/2}LR^{-1/2} = \rho ^{-1}\otimes \sigma ^{\top }\). Apply Lemma 16.32 to \(-\log (\rho ^{-1}\otimes \sigma ^{\top }) = \log \rho \otimes 1 - 1\otimes (\log \sigma )^{\top }\) (using \(\log (\rho ^{-1}) = -\log \rho \) and the transpose-commutes-with-cfc identity \((\log \sigma )^{\top } = \log (\sigma ^{\top })\)), then conjugate by \(R^{1/2} = \rho ^{1/2}\otimes 1\) and cancel with the sandwich to obtain the closed form.
The positive linear functional \(M\mapsto \langle \mathrm{vec}\, 1,\, M\, \mathrm{vec}\, 1\rangle \) recovers the trace-form relative entropy from the perspective:
Apply \(\mathrm{relForm}\) to the closed form of Lemma 16.33. On Kronecker products \(\mathrm{relForm}(A\otimes C) = \operatorname{Tr}(AC^{\top })\), so the two terms become \(\operatorname{Tr}(\rho ^{1/2}(\log \rho )\rho ^{1/2}) = \operatorname{Tr}(\rho \log \rho )\) and \(\operatorname{Tr}(\rho \log \sigma )\); their difference is the trace-form relative entropy.
For matrices \(\rho ,\sigma \), the trace-form relative entropy is \(\mathrm{relEntropyMat}(\rho ,\sigma ) = \Re \, \operatorname{Tr}\bigl(\rho \, (\log \rho - \log \sigma )\bigr)\), the logarithms taken through the continuous functional calculus.
For positive-definite \(\rho _1,\rho _2,\sigma _1,\sigma _2\) and \(c\in [0,1]\),
Lieb’s theorem (Lieb 1973; Carlen, Trace Inequalities and Quantum Entropy, Thm. 2.12), obtained from Effros’ joint convexity of the perspective. The maps \(\rho \mapsto R = \rho \otimes 1\) and \(\sigma \mapsto L = 1\otimes \sigma ^{\top }\) are \(\mathbb {R}\)-linear, so applying Theorem 16.31 to \(f = -\log \) (operator convex on \((0,\infty )\) by Theorem 16.26) gives a Loewner joint-convexity inequality for the perspective. The functional \(\mathrm{relForm}\) is positive and linear; by Lemma 16.34 it turns that operator inequality into the scalar convexity of \((\rho ,\sigma )\mapsto \operatorname{Tr}(\rho (\log \rho - \log \sigma ))\), whose real part is \(\mathrm{relEntropyMat}\).
For a finite convex combination of faithful states — weights \(w_i\ge 0\) with \(\sum _i w_i = 1\) and positive-definite \(\rho _i,\sigma _i\) —,
The two-point joint convexity of Theorem 16.36 says \(\mathrm{relEntropyMat}\) is a convex function on the set of pairs of positive-definite matrices; Jensen’s inequality for a convex function over a finite convex combination upgrades the two-point estimate to the finite-sum form.
For density matrices \(\rho ,\sigma \) with \(\sigma \) faithful (positive definite), \(\mathrm{relEntropyMat}(\rho ,\sigma ) = S(\rho \| \sigma )\), the Umegaki relative entropy.
Both sides expand through the spectral theorem: the trace form \(\Re \, \operatorname{Tr}(\rho (\log \rho - \log \sigma ))\) equals the spectral double sum defining \(S(\rho \| \sigma )\) once the Hermitian cfc is written via eigendecompositions (this is Theorem 16.19 together with the eigenbasis form of the functional calculus). Hence the trace-form joint convexity above transfers to the Umegaki relative entropy on density matrices.
16.6 The data-processing inequality
The Umegaki relative entropy is the finite-dimensional distinguishability functional whose monotonicity under quantum channels is the master inequality of quantum information. We derive it from Lieb’s joint convexity in three moves: a Weyl-twirl reduction of the partial-trace case, a regularization to remove faithfulness, and a Stinespring dilation lifting the partial-trace case to every mixed-ancilla channel. We close with the no-recovery obstruction and the easy (\(\Leftarrow \)) half of Petz’s equality theorem (Petz 1986, 2003).
RelEntropyMonotoneUnderPartialTrace is the proposition that for all finite index types \(n_A, n_E\) and all states \(\rho ,\sigma \) on \(n_A\times n_E\) with \(\sigma \) faithful (positive definite), tracing out the \(E\)-factor does not increase relative entropy,
The index types are quantified over Type (universe \(0\)): finite-dimensional quantum information lives in universe \(0\), and pinning the universe lets this Prop be used as a reusable hypothesis whose subsystems unify with any consumer’s.
For positive-definite states \(\rho ,\sigma \) on \(n_A\times n_E\),
Realize the partial trace as a Weyl twirl: with \(d = \# n_E\) and \(\tau = \tfrac 1d\mathbf1\) the maximally mixed ancilla state, averaging \(\rho \) over the \(d^2\) Heisenberg–Weyl unitaries \(W_{ab}\) on the \(E\)-factor gives \(d^{-2}\sum _{a,b}(\mathbf1\otimes W_{ab})\rho (\mathbf1\otimes W_{ab})^{*} = (\operatorname{Tr}_E\rho )\otimes \tau \), and likewise for \(\sigma \). Each twirled state \(\rho _{ab} := (\mathbf1\otimes W_{ab})\rho (\mathbf1\otimes W_{ab})^{*}\) has \(S(\rho _{ab}\| \sigma _{ab}) = S(\rho \| \sigma )\) by unitary invariance (Theorem 16.22), and the averaged pair has relative entropy \(S\bigl((\operatorname{Tr}_E\rho )\otimes \tau \, \| \, (\operatorname{Tr}_E\sigma )\otimes \tau \bigr) = S(\operatorname{Tr}_E\rho \| \operatorname{Tr}_E\sigma )\) by ancilla additivity (Theorem 16.23). The finite-sum form of Lieb’s joint convexity (Lemma 16.37) applied to the weights \(w_{ab} = d^{-2}\) then yields \(S(\operatorname{Tr}_E\rho \| \operatorname{Tr}_E\sigma )\le \sum _{ab} w_{ab}\, S(\rho _{ab}\| \sigma _{ab}) = S(\rho \| \sigma )\).
The proposition RelEntropyMonotoneUnderPartialTrace holds: the faithfulness hypothesis on \(\rho \) is unnecessary, so \(S(\operatorname{Tr}_E\rho \| \operatorname{Tr}_E\sigma )\le S(\rho \| \sigma )\) for every \(\rho \) and every faithful \(\sigma \).
Regularize the first argument along the affine path \(\rho _\varepsilon = (1-\varepsilon )\rho + \varepsilon \tau \) towards the maximally mixed state \(\tau \). For \(\varepsilon \in (0,1]\) the state \(\rho _\varepsilon \) is positive definite, so the faithful case (Theorem 16.40) gives \(S(\operatorname{Tr}_E\rho _\varepsilon \| \operatorname{Tr}_E\sigma )\le S(\rho _\varepsilon \| \sigma )\). Both sides are continuous in \(\varepsilon \) at \(0\) (continuity of \(M\mapsto S(M\| \sigma )\) on states with \(\sigma \) fixed and faithful, and continuity of the partial trace), and \(\rho _\varepsilon \to \rho \); passing to the limit \(\varepsilon \downarrow 0\) preserves the inequality.
For any state \(\rho \) and any ancilla state \(\alpha \), \(\operatorname{Tr}_E(\rho \otimes \alpha ) = \rho \).
Entrywise, \((\operatorname{Tr}_E(\rho \otimes \alpha ))_{ii'} = \sum _j\rho _{ii'}\alpha _{jj} = \rho _{ii'}\cdot \operatorname{Tr}\alpha = \rho _{ii'}\), using only \(\operatorname{Tr}\alpha = 1\).
For states \(\rho ,\sigma \) on \(n\), a faithful ancilla \(\alpha \) on \(e\), a unitary \(U\) on \(n\times e\), and faithful \(\sigma \),
Unitary conjugation leaves relative entropy invariant (Theorem 16.22), reducing the claim to \(S(\rho \otimes \alpha \| \sigma \otimes \alpha ) = S(\rho \| \sigma )\), which is ancilla additivity (Theorem 16.23) for the faithful ancilla \(\alpha \).
Given the partial-trace DPI (Definition 16.39), every Stinespring-dilated channel \(\Lambda \rho = \operatorname{Tr}_E\bigl(U(\rho \otimes \alpha )U^{*}\bigr)\) — adjoin a faithful ancilla \(\alpha \), conjugate by a unitary dilation \(U\), then trace out the ancilla — is relative-entropy monotone on faithful states: \(S(\Lambda \rho \| \Lambda \sigma )\le S(\rho \| \sigma )\).
Apply the wall (Definition 16.39) to the dilated states \(U(\rho \otimes \alpha )U^{*}\) and \(U(\sigma \otimes \alpha )U^{*}\) (the latter faithful, being a unitary conjugate of a Kronecker product of faithful states): tracing out the ancilla gives \(S(\operatorname{Tr}_E U(\rho \otimes \alpha )U^{*}\| \operatorname{Tr}_E U(\sigma \otimes \alpha )U^{*})\le S(U(\rho \otimes \alpha )U^{*}\| U(\sigma \otimes \alpha )U^{*})\). The right-hand side equals \(S(\rho \| \sigma )\) by isometric-embedding invariance (Theorem 16.43).
Unconditionally, for a faithful ancilla \(\alpha \), a unitary dilation \(U\), and faithful \(\sigma \),
This is the data-processing inequality for the faithful-ancilla mixed-Stinespring family; that family does not contain every CPTP channel (amplitude damping lies outside it, since its exact dilation needs a pure, non-faithful ancilla), so it is not an in-repo DPI for a general Kraus channel.
Feed the now-discharged partial-trace DPI (Theorem 16.41) into the Stinespring reduction (Theorem 16.44), removing its hypothesis.
If a map \(R\) satisfies the faithful data-processing inequality and inverts a coarse-graining \(\Lambda \) on the pair \(\rho ,\sigma \) (\(R(\Lambda \rho ) = \rho \), \(R(\Lambda \sigma ) = \sigma \) with \(\Lambda \sigma \) faithful), then a strict drop \(S(\Lambda \rho \| \Lambda \sigma ) {\lt} S(\rho \| \sigma )\) is impossible.
Monotonicity of \(R\) applied to \(\Lambda \rho ,\Lambda \sigma \) gives \(S(R(\Lambda \rho )\| R(\Lambda \sigma ))\le S(\Lambda \rho \| \Lambda \sigma )\); the section identities rewrite the left side as \(S(\rho \| \sigma )\), so \(S(\rho \| \sigma )\le S(\Lambda \rho \| \Lambda \sigma )\), contradicting the assumed strict drop.
Unconditionally: a strict relative-entropy drop under a coarse-graining \(\Lambda \) (an endomorphism of the input space) rules out any Stinespring recovery channel \(R\, x = \operatorname{Tr}_E(U(x\otimes \alpha )U^{*})\) inverting \(\Lambda \) on \(\rho ,\sigma \).
Specialize Theorem 16.46 to the Stinespring recovery map, whose faithful data-processing monotonicity is exactly Theorem 16.45.
The equality case of the data-processing inequality — that saturation \(S(\Lambda \rho \| \Lambda \sigma ) = S(\rho \| \sigma )\) is equivalent to the existence of a Petz recovery map inverting \(\Lambda \) on \(\rho ,\sigma \) — is Petz’s equality theorem. Its elementary direction (recovery \(\Rightarrow \) saturation) rests only on the monotonicity established above; the converse (saturation \(\Rightarrow \) recovery) is the analytic heart of the next chapter. Both are treated in full in Chapter 17.