Sandwiched Rényi divergence decreases under positive trace-nonincreasing maps

Open

QAlgorithms.Papers.Independent.Intakethird100.P46.sandwiched_renyi_monotonicity

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

prove2quantum

Let $d,d'$ be finite dimensions and let $\Phi:M_d(\mathbb C)\to M_{d'}(\mathbb C)$ be complex-linear, with $\Phi(A)\ge0$ and $\operatorname{tr}\Phi(A)\le\operatorname{tr}A$ for every $A\ge0$ . For every finite real $\alpha>1$ and arbitrary positive semidefinite $\rho,\sigma$ ,

D_\alpha(\Phi(\rho)\Vert\Phi(\sigma))\le D_\alpha(\rho\Vert\sigma).

On support inclusion, $D_\alpha(\rho\Vert\sigma)=\frac{1}{\alpha-1}\log\operatorname{tr}[(\sigma^{(1-\alpha)/(2\alpha)}\rho\sigma^{(1-\alpha)/(2\alpha)})^\alpha]$ ; otherwise it is $+\infty$ . Negative powers use the inverse on the support. The natural logarithm is extended by $\log0=-\infty$ , so zero inputs and the zero map are included, without division by $\operatorname{tr}\rho$ . This extends data processing to maps with positivity alone, even when trace can decrease.

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 2, (5).
The accepted sandwiched divergence is unnormalized and has extended log(0)=-infinity.
The map may be merely positive; the input operators may be zero or singular. -/
theorem sandwiched_renyi_monotonicity (d e : ℕ)
    (Phi : Matrix (Fin d) (Fin d) ℂ →ₗ[ℂ] Matrix (Fin e) (Fin e) ℂ)
    (hPhi : PositiveMatrixTraceNonincreasing Phi)
    (alpha : ℝ) (hAlpha : 1 < alpha)
    (rho sigma : Matrix (Fin d) (Fin d) ℂ)
    (hrho : rho.PosSemidef) (hsigma : sigma.PosSemidef) :
    beigiSandwichedDivergence alpha (Phi rho) (Phi sigma) ≤
      beigiSandwichedDivergence alpha 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 2: sandwiched Rényi monotonicity under positive trace-nonincreasing maps

Read-back

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

For every pair of natural numbers $d,e$ , a complex-linear map $\Phi:M_d(\mathbb C)\to M_e(\mathbb C)$ such that every positive semidefinite $A$ has positive semidefinite image and $\operatorname{Re}\operatorname{Tr}\Phi(A)\le\operatorname{Re}\operatorname{Tr}A$ , every real $\alpha>1$ , and every positive semidefinite $\rho,\sigma\in M_d(\mathbb C)$ , the assertion is

D_\alpha\bigl(\Phi(\rho),\Phi(\sigma)\bigr)\le D_\alpha(\rho,\sigma).

For matrices $X,Y$ of the same size, the extended-real quantity used here is

D_\alpha(X,Y)= \begin{cases} \displaystyle\frac{1}{\alpha-1} \log_{\mathrm{ext}}\!\left( \max\!\left\{0,\operatorname{Re}\operatorname{Tr} P_\alpha\!\left(P_{\frac{1-\alpha}{2\alpha}}(Y)\,X\, P_{\frac{1-\alpha}{2\alpha}}(Y)\right)\right\}\right), &\ker Y\subseteq\ker X,\\ +\infty,&\text{otherwise}. \end{cases}

Here $P_0(Z)$ is the identity matrix, while for $t\ne0$ , $P_t(Z)$ is the continuous-functional-calculus value of the real function that is $0$ at $0$ and $x^t$ elsewhere; $\log_{\mathrm{ext}}$ is the natural logarithm on nonnegative extended reals, with value $-\infty$ at $0$ and $+\infty$ at $+\infty$ . No normalization by $\operatorname{Tr}X$ occurs. Zero matrices and zero dimensions are included, and neither input is required to be nonzero or have trace one; in particular, $D_\alpha(0,Y)=-\infty$ for positive semidefinite $Y$ .

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