Corollary 10: exponential trace inequality resolving the Ruskai question

Open

QAlgorithms.Papers.Independent.Intakethird100.P52.exponential_trace_bound

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

prove2quantum

All Hilbert spaces below are finite dimensional and nonzero over $\mathbb C$ . A density operator is positive semidefinite with trace one. Every spectral power is zero on the kernel, including zero and negative powers. Information quantities use base-two logarithms, with $\log_2 0=-\infty$ ; the operator logarithms in exponential formulas are natural logarithms.

Let $\rho>0$ be a density operator, let $\sigma>0$ be arbitrary, and let $\mathcal N:\mathcal B(H)\to\mathcal B(K)$ be a strict CPTP map. Then

\operatorname{Tr}\exp\!\left(\log\sigma+\mathcal N^\dagger(\log\mathcal N(\rho)-\log\mathcal N(\sigma))\right)\le1.

Here the exponential is the ordinary exponential of a Hermitian operator and satisfies $\exp(0)=I$ .

This gives the exponential trace inequality posed by Ruskai.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P52

Formal statement

noncomputable section

open scoped Matrix ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P52

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Information100.P63 (Mat)

open QAlgorithms.Papers.Independent.Dependency50.P21 (channelAdjoint petz marginalAB)

open QAlgorithms.Papers.Independent.Dependency50.P35 (tr elog maxRelative)

open QAlgorithms.Papers.Independent.Information100.P71 (supportPower)

open QAlgorithms.Papers.Independent.Renew46.P35 (HasMarkovBlocks)

/-- Corollary 10, PDF p.13, equation (3.50). Natural logarithms and ordinary
exponential of the Hermitian exponent; exp(0)=I even on its zero eigenspace. -/
theorem exponential_trace_bound {H K : Type} [Fintype H] [Fintype K]
    [DecidableEq H] [DecidableEq K] [Nonempty H] [Nonempty K]
    (rho sigma : Mat H) (hrho : IsDensityMatrix rho)
    (hrhoPD : rho.PosDef) (hsigmaPD : sigma.PosDef)
    (N : Superop H K) (hN : IsStrictChannel N) :
    tr (cfc Real.exp (cfc Real.log sigma +
      channelAdjoint N (cfc Real.log (N rho) - cfc Real.log (N sigma)))) ≤ 1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P52

end

Source

Quantum Markov chains, sufficiency of quantum channels, and Renyi information measures, arXiv:1501.05636v4, PDF p. 13, Corollary 10: exponential trace inequality resolving the Ruskai question

Read-back

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

For finite nonempty types $H,K$ , each with decidable equality, let $\rho,\sigma$ be complex matrices on $H$ , assume that $\rho$ is positive semidefinite with trace $1$ and is positive definite, and assume that $\sigma$ is positive definite without requiring trace $1$ . Let $N$ admit a finite Kraus representation $N(X)=\sum_jE_jXE_j^\dagger$ with $\sum_jE_j^\dagger E_j=I_H$ , and assume additionally that $N(X)$ is positive definite whenever $X$ is positive definite. With $(N^\dagger Z)_{ij}=\sum_{k,l}\overline{N(E_{ij})_{kl}}Z_{kl}$ , the assertion is

\operatorname{Re}\operatorname{Tr} \exp_{\mathrm{fc}}\!\left( \log_{\mathrm{fc}}\sigma+ N^\dagger\!\left(\log_{\mathrm{fc}}(N\rho)-\log_{\mathrm{fc}}(N\sigma)\right) \right)\le1,

where $\log_{\mathrm{fc}}$ and $\exp_{\mathrm{fc}}$ mean continuous functional calculus for the real natural logarithm and real exponential, respectively.

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