Theorem 17: min/max entropy differences and channel sufficiency

Open

QAlgorithms.Papers.Independent.Intakethird100.P52.sufficiency_min_max

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, $\sigma>0$ arbitrary, and $\mathcal N$ strict CPTP. Sufficiency means existence of a common CPTP recovery of both $\rho$ and $\sigma$ .

The Petz map and min/max divergences are

\mathcal P_{\sigma,\mathcal N}(X)=\sigma^{1/2}\mathcal N^\dagger\!\left(\mathcal N(\sigma)^{-1/2}X\mathcal N(\sigma)^{-1/2}\right)\sigma^{1/2},\quad D_{\min}(\omega\Vert\tau)=-\log_2 F(\omega,\tau),\quad D_{\max}(\omega\Vert\tau)=\inf\{\lambda\in\mathbb R:\omega\le2^\lambda\tau\},

where $F(\omega,\tau)=\|\sqrt\omega\sqrt\tau\|_1^2$ is squared fidelity. The max-divergence infimum is extended real, so an empty set gives $+\infty$ . Set $\Delta_{\min}=D_{\min}(\rho\Vert\mathcal P_{\sigma,\mathcal N}(\mathcal N(\rho)))$ and define $\Delta_{\max}$ by the same reference with $D_{\max}$ .

Then

\Delta_{\min}\ge0,\qquad\Delta_{\max}\ge0,\qquad (\Delta_{\min}=0\iff\mathcal N\text{ is sufficient}),\qquad (\Delta_{\max}=0\iff\mathcal N\text{ is sufficient}).

Each min/max entropy difference separately detects sufficiency.

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)

/-- Theorem 17, PDF p.17, equation (5.3): both nonnegativities and each
individual iff-zero condition. Recovery of rho is not assumed. -/
theorem sufficiency_min_max {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) :
    0 ≤ deltaMin rho sigma N ∧ 0 ≤ deltaMax rho sigma N ∧
    (deltaMin rho sigma N = 0 ↔ IsSufficient rho sigma N) ∧
    (deltaMax rho sigma N = 0 ↔ IsSufficient rho sigma N) := 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. 17, Theorem 17: min/max entropy differences and channel sufficiency

Read-back

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

Let $H,K$ be finite, nonempty index types with decidable equality. Let $\rho,\sigma$ be positive definite complex matrices on $H$ , with $\rho$ positive semidefinite and of trace $1$ ; no trace normalization is assumed for $\sigma$ . Let $N$ be a map from matrices on $H$ to matrices on $K$ that has a finite Kraus representation $N(X)=\sum_jE_jXE_j^\dagger$ with $\sum_jE_j^\dagger E_j=I_H$ , and assume that $N(X)$ is positive definite whenever $X$ is positive definite. Define

(N^*Y)_{ab} =\sum_{u,v\in K}\overline{N(E_{ab})_{uv}}\,Y_{uv}, \qquad \tau=\sigma^{[1/2]}N^*\!\left( (N\sigma)^{[-1/2]}(N\rho)(N\sigma)^{[-1/2]} \right)\sigma^{[1/2]},

where $E_{ab}$ is the matrix unit and $X^{[t]}$ denotes spectral functional calculus using $x^t$ at nonzero eigenvalues and $0$ at zero eigenvalues, even for $t=0$ . Put

F=\operatorname{Re}\operatorname{Tr} \sqrt{\sqrt{\rho}\,\tau\,\sqrt{\rho}}, \qquad d_{\min}=-\ell(F^2), \qquad d_{\max}=\inf\{\lambda\in\mathbb R:2^\lambda\tau-\rho \text{ is positive semidefinite}\},

where $\ell(x)=\log_2x$ for $x>0$ and $-\infty$ otherwise, and the infimum is taken in the extended real numbers, so an empty feasible set gives $+\infty$ . Then $d_{\min}\ge0$ and $d_{\max}\ge0$ , and each of the equalities $d_{\min}=0$ and $d_{\max}=0$ is separately equivalent to the existence of a map $R$ from matrices on $K$ to matrices on $H$ , having a finite Kraus representation $R(Y)=\sum_jF_jYF_j^\dagger$ with $\sum_jF_j^\dagger F_j=I_K$ , such that $R(N\rho)=\rho$ and $R(N\sigma)=\sigma$ .

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