Theorem 14: sufficiency characterized by vanishing Renyi relative entropy differences

Open

QAlgorithms.Papers.Independent.Intakethird100.P52.sufficiency_renyi

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$ be a density operator on $H$ , let $\sigma\ge0$ be an operator on $H$ without a trace constraint, and let $\mathcal N:\mathcal B(H)\to\mathcal B(K)$ be CPTP. Its adjoint $\mathcal N^\dagger$ is the Hilbert–Schmidt adjoint. Write

\begin{aligned} K_a&=\sigma^{(1-a)/2}\mathcal N^\dagger\!\left(\mathcal N(\sigma)^{(a-1)/2}\mathcal N(\rho)^{1-a}\mathcal N(\sigma)^{(a-1)/2}\right)\sigma^{(1-a)/2},\\ L_a&=\sigma^{(1-a)/(2a)}\mathcal N^\dagger\!\left(\mathcal N(\sigma)^{(a-1)/(2a)}\mathcal N(\rho)^{(1-a)/a}\mathcal N(\sigma)^{(a-1)/(2a)}\right)\sigma^{(1-a)/(2a)},\\ R_a&=K_a^{1/(1-a)},\qquad S_a=L_a^{a/(1-a)},\\ \Delta_a&=\frac{\log_2\operatorname{Tr}(\rho^aK_a)}{a-1},\qquad \widetilde\Delta_a=\frac{\log_2\operatorname{Tr}[(\rho^{1/2}L_a\rho^{1/2})^a]}{a-1}. \end{aligned}

Assume $\rho>0$ , $\sigma>0$ , and that $\mathcal N$ is strict: $\mathcal N(X)>0$ for every $X>0$ . The channel is sufficient for $(\rho,\sigma)$ when one CPTP map $\mathcal R$ satisfies $\mathcal R(\mathcal N(\rho))=\rho$ and $\mathcal R(\mathcal N(\sigma))=\sigma$ .

Sufficiency implies

\Delta_a=\widetilde\Delta_a=0\quad\text{for every }a\in(0,1)\cup(1,\infty).

Conversely, either $\Delta_a=0$ for some $a\in(0,1)\cup(1,2)$ or $\widetilde\Delta_a=0$ for some $a\in(1/2,1)\cup(1,\infty)$ implies sufficiency.

This characterizes sufficient channels through vanishing Rényi differences, retaining the full forward order range.

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 14, PDF pp.14–17. Correction: the printed final tilde expression
omits “=0”; restored from (4.14), p.16, and the concluding proof on p.17.
The forward range is wider than either converse range. -/
theorem sufficiency_renyi {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) :
    (IsSufficient rho sigma N → ∀ a : ℝ, (0 < a ∧ a < 1) ∨ 1 < a →
      renyiDifference a rho sigma N = 0 ∧ deltaTilde a rho sigma N = 0) ∧
    (((∃ a : ℝ, ((0 < a ∧ a < 1) ∨ (1 < a ∧ a < 2)) ∧ renyiDifference a rho sigma N = 0) ∨
      (∃ a : ℝ, ((1 / 2 < a ∧ a < 1) ∨ 1 < a) ∧ deltaTilde a 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. 14, Theorem 14: sufficiency characterized by vanishing Renyi relative entropy differences

Read-back

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

Let $H,K$ be finite nonempty types with decidable equality, let $\rho,\sigma$ be complex matrices on $H$ , assume that $\rho$ is positive semidefinite with trace $1$ , that both $\rho$ and $\sigma$ are positive definite, and let $N$ be a channel that maps every positive definite matrix to a positive definite matrix. Here a channel means a function admitting a finite Kraus representation $N(X)=\sum_jE_jXE_j^\dagger$ with $\sum_jE_j^\dagger E_j=I_H$ ; no trace-one assumption is made on $\sigma$ . Define

(N^\dagger Z)_{ij}=\sum_{k,l}\overline{N(E_{ij})_{kl}}\,Z_{kl},

where $E_{ij}$ is the matrix unit, and let $S_t(X)$ be continuous functional calculus for $x\mapsto0$ at zero and $x\mapsto x^t$ otherwise. Put

\begin{aligned} K_a&=S_{(1-a)/2}(\sigma)\, N^\dagger\!\left(S_{(a-1)/2}(N\sigma)S_{1-a}(N\rho)S_{(a-1)/2}(N\sigma)\right) S_{(1-a)/2}(\sigma),\\ \widetilde K_a&=S_{(1-a)/(2a)}(\sigma)\, N^\dagger\!\left(S_{(a-1)/(2a)}(N\sigma)S_{(1-a)/a}(N\rho)S_{(a-1)/(2a)}(N\sigma)\right) S_{(1-a)/(2a)}(\sigma),\\ D_a&=\frac{\ell_2(\operatorname{Re}\operatorname{Tr}(S_a(\rho)K_a))}{a-1},\\ \widetilde D_a&=\frac{\ell_2(\operatorname{Re}\operatorname{Tr}S_a(S_{1/2}(\rho)\widetilde K_aS_{1/2}(\rho)))}{a-1}, \end{aligned}

where $\ell_2(x)=\log_2x$ for $x>0$ and $-\infty$ otherwise, and the last two expressions use extended-real arithmetic. The assertion is that if there is a channel $R$ satisfying $R(N\rho)=\rho$ and $R(N\sigma)=\sigma$ , then $D_a=\widetilde D_a=0$ for every $a\in(0,1)\cup(1,\infty)$ ; conversely, such a channel $R$ exists if either $D_a=0$ for at least one $a\in(0,1)\cup(1,2)$ , or $\widetilde D_a=0$ for at least one $a\in(1/2,1)\cup(1,\infty)$ .

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