Appendix A: joint trace concavity extended to positive semidefinite pairs

Open

QAlgorithms.Papers.Independent.Intakethird100.P52.joint_trace_concavity

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 $1<a<2$ , let $X$ be a nonempty finite set, and let $p_x\ge0$ satisfy $\sum_xp_x=1$ . Let $P_x,Q_x$ be positive semidefinite operators on the same space $H$ , and set $\overline P=\sum_xp_xP_x$ and $\overline Q=\sum_xp_xQ_x$ . Then

\sum_xp_x\operatorname{Tr}\left[(Q_x^{(a-1)/2}P_xQ_x^{(a-1)/2})^{1/a}\right] \le\operatorname{Tr}\left[(\overline Q^{(a-1)/2}\overline P\overline Q^{(a-1)/2})^{1/a}\right].

Zero weights and zero or singular operators are allowed.

This extends the joint trace concavity from positive definite to positive semidefinite pairs.

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)

/-- Appendix A, PDF p.20, equation (A.12): joint concavity extended
to all positive semidefinite pairs, including zero matrices and zero weights. -/
theorem joint_trace_concavity {H X : Type} [Fintype H] [DecidableEq H] [Nonempty H]
    [Fintype X] [Nonempty X] (a : ℝ) (ha : 1 < a ∧ a < 2)
    (p : X → ℝ) (hp : ∀ x, 0 ≤ p x) (hsum : ∑ x, p x = 1)
    (P Q : X → Mat H) (hP : ∀ x, (P x).PosSemidef) (hQ : ∀ x, (Q x).PosSemidef) :
    (∑ x, p x * jointTrace a (P x) (Q x)) ≤
      jointTrace a (∑ x, (p x : ℂ) • P x) (∑ x, (p x : ℂ) • Q x) := 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. 20, Appendix A: joint trace concavity extended to positive semidefinite pairs

Read-back

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

Let $H$ be a finite, nonempty index type with decidable equality, let $X$ be a finite, nonempty index type, and let $a\in\mathbb R$ satisfy $1<a<2$ . Let $p:X\to\mathbb R$ satisfy $p_x\ge0$ for every $x$ and $\sum_xp_x=1$ , and let $P_x,Q_x$ be positive semidefinite complex matrices on $H$ for every $x$ . For a positive semidefinite matrix $M$ , write $M^{[t]}$ for spectral functional calculus that assigns $u^t$ to each nonzero eigenvalue $u$ and $0$ to a zero eigenvalue, and define

J_a(P,Q)=\operatorname{Re}\operatorname{Tr} \left(Q^{[(a-1)/2]}P Q^{[(a-1)/2]}\right)^{[1/a]}.

Then

\sum_{x\in X}p_xJ_a(P_x,Q_x) \le J_a\!\left(\sum_{x\in X}p_xP_x,\, \sum_{x\in X}p_xQ_x\right).

Zero weights and singular or zero matrices are included; the matrices need not have trace $1$ .

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