13 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.
13.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.
13.2 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 13.14) 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 13.11.
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 13.14 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.
13.3 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 13.17. 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 13.19, 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 13.19 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 13.22 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 13.23. 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 13.21 to \(f = -\log \) (operator convex on \((0,\infty )\) by Theorem 13.16) gives a Loewner joint-convexity inequality for the perspective. The functional \(\mathrm{relForm}\) is positive and linear; by Lemma 13.24 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 13.26 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 13.9 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.
13.4 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 13.12), 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 13.13). The finite-sum form of Lieb’s joint convexity (Lemma 13.27) 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 13.30) 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 13.12), reducing the claim to \(S(\rho \otimes \alpha \| \sigma \otimes \alpha ) = S(\rho \| \sigma )\), which is ancilla additivity (Theorem 13.13) for the faithful ancilla \(\alpha \).
Given the partial-trace DPI (Definition 13.29), 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 13.29) 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 13.33).
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 13.31) into the Stinespring reduction (Theorem 13.34), 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 13.36 to the Stinespring recovery map, whose faithful data-processing monotonicity is exactly Theorem 13.35.
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 14.