Corollary 11: tripartite trace inequalities

Open

QAlgorithms.Papers.Independent.Intakethird100.P52.tripartite_trace_bounds

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.

Define

\begin{aligned} R_a^{ABC}&=\left(\rho_{AC}^{(1-a)/2}\rho_C^{(a-1)/2}\rho_{BC}^{1-a}\rho_C^{(a-1)/2}\rho_{AC}^{(1-a)/2}\right)^{1/(1-a)},\\ S_a^{ABC}&=\left(\rho_{AC}^{(1-a)/(2a)}\rho_C^{(a-1)/(2a)}\rho_{BC}^{(1-a)/a}\rho_C^{(a-1)/(2a)}\rho_{AC}^{(1-a)/(2a)}\right)^{a/(1-a)}. \end{aligned}

Then $\operatorname{Tr}R_a^{ABC}\le1$ for $0<a<1$ and $\operatorname{Tr}S_a^{ABC}\le1$ for $1/2<a<1$ . If $\rho_{ABC}>0$ , the respective bounds extend to $1<a<2$ and every $a>1$ .

These are the tripartite versions of the channel reference trace bounds.

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 11, PDF p.13, equations (3.52)–(3.53). The displayed products
are the computed R_alpha/S_alpha for sigma=rho_AC tensor I_B, N=Tr_A,
by (1.21); all marginals come from the same rho in order A x (C x B). -/
theorem tripartite_trace_bounds {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) :
    (∀ a : ℝ, 0 < a ∧ a < 1 →
      tr (renyiReference a rho (conditionalSigma rho) traceLeft) ≤ 1) ∧
    (∀ a : ℝ, 1 / 2 < a ∧ a < 1 →
      tr (sandwichedReference a rho (conditionalSigma rho) traceLeft) ≤ 1) ∧
    (rho.PosDef →
      (∀ a : ℝ, 1 < a ∧ a < 2 →
        tr (renyiReference a rho (conditionalSigma rho) traceLeft) ≤ 1) ∧
      (∀ a : ℝ, 1 < a →
        tr (sandwichedReference a rho (conditionalSigma rho) traceLeft) ≤ 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 11: tripartite trace inequalities

Read-back

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

For finite nonempty types $A,C,B$ , each with decidable equality, let $\rho$ be a positive semidefinite complex matrix on $A\times(C\times B)$ with trace $1$ . Define $\Sigma=\rho_{AC}\otimes I_B$ , where $(\rho_{AC})_{(i,c),(j,d)}=\sum_b\rho_{(i,c,b),(j,d,b)}$ , and put $\rho_{CB}=\operatorname{Tr}_A\rho$ , $\Sigma_{CB}=\operatorname{Tr}_A\Sigma$ , with partial trace summing equal $A$ -indices. Let $S_t(X)$ be continuous functional calculus for the function zero at zero and $x^t$ otherwise, and set

\begin{aligned} K_a&=S_{(1-a)/2}(\Sigma) \left[I_A\otimes S_{(a-1)/2}(\Sigma_{CB})S_{1-a}(\rho_{CB})S_{(a-1)/2}(\Sigma_{CB})\right] S_{(1-a)/2}(\Sigma),\\ \widetilde K_a&=S_{(1-a)/(2a)}(\Sigma) \left[I_A\otimes S_{(a-1)/(2a)}(\Sigma_{CB})S_{(1-a)/a}(\rho_{CB})S_{(a-1)/(2a)}(\Sigma_{CB})\right] S_{(1-a)/(2a)}(\Sigma),\\ R_a&=S_{1/(1-a)}(K_a),\qquad \widetilde R_a=S_{a/(1-a)}(\widetilde K_a). \end{aligned}

Then $\operatorname{Re}\operatorname{Tr}R_a\le1$ for every $0<a<1$ , and $\operatorname{Re}\operatorname{Tr}\widetilde R_a\le1$ for every $1/2<a<1$ . If $\rho$ is positive definite, these bounds also hold for $1<a<2$ and $a>1$ , respectively. The first two conclusions include singular $\rho$ , with zero spectral values assigned zero by every $S_t$ .

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