Scalar concavity implies concavity of spectral trace

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.trace_concavity

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $R,S$ be positive semidefinite trace-one matrices of the same positive finite dimension, let $p\in[0,1]$ , and let $f:\mathbb R\to\mathbb R$ be concave on $[0,1]$ . Write $f(R)$ for spectral functional calculus and $\operatorname{Tr}_{\mathbb R}$ for the real part of the trace. Then

\operatorname{Tr}_{\mathbb R}f(pR+(1-p)S)\ge p\operatorname{Tr}_{\mathbb R}f(R)+(1-p)\operatorname{Tr}_{\mathbb R}f(S).

In particular the marginal costs $L(R)=2(1-\operatorname{Tr}_{\mathbb R}R^2)$ and $\sqrt{L(R)}$ obey the same concavity inequality. The spectral trace and $L$ are invariant under unitary conjugation, and therefore so is $\sqrt L$ . No operator-concavity hypothesis on $f$ is needed.

This is the finite spectral-trace fact used to obtain the concave marginal costs for concurrence and tangle.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P21

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P21

open scoped Matrix ComplexConjugate

open Filter

open QAlgorithms

open QAlgorithms.Papers.Independent.Information100.P03
  (PureEnsemble convexRoof pureConcurrence concurrence SchmidtData schmidtVector)

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF pp.4--5, (2.3): scalar concavity on [0,1] implies spectral trace
concavity on density matrices; no operator-concavity hypothesis is added. -/
theorem trace_concavity (d : ℕ) (hd : 0 < d) (f : ℝ → ℝ)
    (hf : ConcaveOn ℝ (Set.Icc (0 : ℝ) 1) f)
    (rho sigma : Matrix (Fin d) (Fin d) ℂ)
    (hrho : IsDensityMatrix rho) (hsigma : IsDensityMatrix sigma)
    (p : ℝ) (hp : p ∈ Set.Icc (0 : ℝ) 1) :
    p * spectralTrace f rho + (1 - p) * spectralTrace f sigma ≤
      spectralTrace f ((p : ℂ) • rho + ((1 - p : ℝ) : ℂ) • sigma) ∧
    p * marginalTangle rho + (1-p) * marginalTangle sigma ≤
      marginalTangle ((p : ℂ) • rho + ((1-p : ℝ) : ℂ) • sigma) ∧
    p * Real.sqrt (marginalTangle rho) + (1-p) * Real.sqrt (marginalTangle sigma) ≤
      Real.sqrt (marginalTangle ((p : ℂ) • rho + ((1-p : ℝ) : ℂ) • sigma)) ∧
    (∀ U : Matrix.unitaryGroup (Fin d) ℂ,
      spectralTrace f ((U : Matrix (Fin d) (Fin d) ℂ) * rho *
        (U : Matrix (Fin d) (Fin d) ℂ)ᴴ) = spectralTrace f rho ∧
      marginalTangle ((U : Matrix (Fin d) (Fin d) ℂ) * rho *
        (U : Matrix (Fin d) (Fin d) ℂ)ᴴ) = marginalTangle rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P21

end

Source

I-concurrence and tangle for isotropic states, arXiv:quant-ph/0208002v1, PDF p. 4, §2, (2.3): trace of a scalar concave spectral function is concave

Read-back

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

For every positive natural number $d$ , every function $f:\mathbb R\to\mathbb R$ concave on $[0,1]$ , every pair of positive semidefinite complex $d\times d$ matrices $\rho,\sigma$ of trace $1$ , and every $p\in[0,1]$ , put $\tau=p\rho+(1-p)\sigma$ , $S_f(X)=\operatorname{Re}\operatorname{tr}(f(X))$ , using real continuous functional calculus, and $t(X)=2(1-\operatorname{Re}\operatorname{tr}(X^2))$ . Then

pS_f(\rho)+(1-p)S_f(\sigma)\le S_f(\tau),\qquad pt(\rho)+(1-p)t(\sigma)\le t(\tau),

and

p\sqrt{t(\rho)}+(1-p)\sqrt{t(\sigma)}\le\sqrt{t(\tau)}.

For every unitary complex $d\times d$ matrix $U$ , one also has $S_f(U\rho U^\dagger)=S_f(\rho)$ and $t(U\rho U^\dagger)=t(\rho)$ . The cases $d=1$ and $p=0,1$ are included; no differentiability assumption on $f$ is imposed.

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