Corollary 19: min/max conditional information and short quantum Markov chains

Open

QAlgorithms.Papers.Independent.Intakethird100.P52.markov_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=\rho_{ABC}$ be a tripartite density operator. Its marginals $\rho_{AC},\rho_{BC},\rho_C$ are computed by partial trace from this same state. Operators on fewer registers are extended by identities. Use tensor order $A\otimes(C\otimes B)$ , and set $\sigma=\rho_{AC}\otimes I_B$ and $\mathcal N=\operatorname{Tr}_A$ . Define $I_a(A;B\mid C)_\rho=\Delta_a(\rho,\sigma,\mathcal N)$ and $\widetilde I_a(A;B\mid C)_\rho=\widetilde\Delta_a(\rho,\sigma,\mathcal N)$ . A short quantum Markov chain $A-C-B$ means that the whole space $H_C$ decomposes as $\bigoplus_j H_{C_{L,j}}\otimes H_{C_{R,j}}$ and $\rho=\bigoplus_j q_j\rho_{AC_{L,j}}\otimes\rho_{C_{R,j}B}$ , where $q_j\ge0$ , $\sum_jq_j=1$ , and both factors in each block are density operators.

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}$ .

Assume $\rho_{ABC}>0$ and define

\tau=\rho_{AC}^{1/2}\rho_C^{-1/2}\rho_{BC}\rho_C^{-1/2}\rho_{AC}^{1/2},\quad I_{\min}=D_{\min}(\rho\Vert\tau),\quad I_{\max}=D_{\max}(\rho\Vert\tau).

Then the two equivalences hold separately:

I_{\max}(A;B\mid C)_\rho=0\iff\rho\text{ is a short quantum Markov chain }A-C-B,

I_{\min}(A;B\mid C)_\rho=0\iff\rho\text{ is a short quantum Markov chain }A-C-B.

Both one-shot information measures have the same exact Markov zero set.

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 19, PDF p.18, equations (5.11)–(5.12), with primary
definitions (5.4),(5.7) and both independent equivalences. -/
theorem markov_min_max {A C B : Type} [Fintype A] [Fintype C] [Fintype B]
    [DecidableEq A] [DecidableEq C] [DecidableEq B]
    [Nonempty A] [Nonempty C] [Nonempty B]
    (rho : Mat (A × (C × B))) (hrho : IsDensityMatrix rho)
    (hrhoPD : rho.PosDef) :
    (conditionalMaxInformation rho = 0 ↔ HasMarkovBlocks rho) ∧
    (conditionalMinInformation rho = 0 ↔ HasMarkovBlocks rho) := 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. 18, Corollary 19: min/max conditional information and short quantum Markov chains

Read-back

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

Let $A,C,B$ be finite, nonempty index types with decidable equality, and let $\rho$ be a positive definite complex matrix on $A\times(C\times B)$ that is positive semidefinite and has trace $1$ . Set $\sigma=(\operatorname{Tr}_B\rho)\otimes I_B$ , $R=\operatorname{Tr}_A\rho$ , $S=\operatorname{Tr}_A\sigma$ , and

\tau=\sigma^{[1/2]} \bigl(I_A\otimes[S^{[-1/2]}RS^{[-1/2]}]\bigr) \sigma^{[1/2]},

where partial traces sum diagonal entries over the indicated register and $X^{[t]}$ applies $x^t$ to nonzero eigenvalues and $0$ to zero eigenvalues. Define the extended-real quantities

\begin{aligned} d_{\max}&=\inf\{\lambda\in\mathbb R: 2^\lambda\tau-\rho\text{ is positive semidefinite}\},\\ d_{\min}&=-\ell\!\left( \left[\operatorname{Re}\operatorname{Tr} \sqrt{\sqrt{\rho}\,\tau\,\sqrt{\rho}}\right]^2\right), \end{aligned}

with $\ell(x)=\log_2x$ for $x>0$ and $-\infty$ otherwise, and with an empty feasible set for the infimum giving $+\infty$ . Each of $d_{\max}=0$ and $d_{\min}=0$ is separately equivalent to the following decomposition: there exist a positive integer $r$ , positive integers $l_j,r_j$ , a unitary identification $C\cong\bigoplus_{j=1}^{r}(\mathbb C^{l_j}\otimes\mathbb C^{r_j})$ with inclusions $V_j$ , nonnegative weights $q_j$ summing to $1$ , and positive semidefinite trace-one matrices $\alpha_j$ on $A\times\{1,\ldots,l_j\}$ and $\beta_j$ on $\{1,\ldots,r_j\}\times B$ , such that

\rho=\sum_{j=1}^{r}q_j (I_A\otimes V_j\otimes I_B)(\alpha_j\otimes\beta_j) (I_A\otimes V_j\otimes I_B)^\dagger.

The weights in this decomposition may be zero.

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