Prove2Me

Corollary 4 (Wall 2013): tr⁡f(ρ)\operatorname{tr} f(\rho) is nondecreasing for concave ff

Proved
WallGSL.unital_positive_map_trace_concave_nondecreasing

by Lucas · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

entropymatrix-analysisquantum-information

Corollary 4 (appendix). Let ρ\rho be an n×nn\times n density matrix and let TT be a positive, trace-preserving, identity-preserving linear map on n×nn\times n complex matrices. Then for every function ff that is concave on [0,∞)[0,\infty),

tr⁡f(ρ)=∑j=1nf(λj(ρ)) ≤ ∑j=1nf(λj(T(ρ)))=tr⁡f(T(ρ)).\operatorname{tr} f(\rho)=\sum_{j=1}^n f(\lambda_j(\rho))\ \le\ \sum_{j=1}^n f\big(\lambda_j(T(\rho))\big)=\operatorname{tr}f\big(T(\rho)\big).

In particular the von Neumann entropy −tr⁡(ρln⁡ρ)-\operatorname{tr}(\rho\ln\rho) does not decrease.

This expresses that the probability eigenvalues can only evolve towards equalization; the paper uses it with the function f(p)=0f(p)=0 for p≤pip\le p_i and f(p)=pi−pf(p)=p_i-p for p≥pip\ge p_i (eqs. (A.8)–(A.10)).

Formalization Note The paper says "convex"; the statement is formalized for concave ff, because the paper's own example (A.8)–(A.9) is concave and the convex version is false: for f(p)=p2f(p)=p^2 and the completely depolarizing map T(A)=tr⁡AnIT(A)=\frac{\operatorname{tr}A}{n}I, a pure state ρ\rho has tr⁡f(ρ)=1>1n=tr⁡f(T(ρ))\operatorname{tr}f(\rho)=1>\frac1n=\operatorname{tr}f(T(\rho)) when n≥2n\ge2.

Preamble
import Mathlib

open Matrix
open scoped ComplexOrder
Formal statement
namespace WallGSL

/-- Corollary 4 (appendix) of Wall (2013), with the convexity condition read as concavity
(see the formalization note): for every function `f` concave on `[0, ∞)`, the quantity
`tr f(ρ) = ∑ⱼ f(pⱼ)` does not decrease under a trace-preserving, identity-preserving,
positive linear map `T`. -/
theorem unital_positive_map_trace_concave_nondecreasing
    {n : ℕ} (T : Matrix (Fin n) (Fin n) ℂ →ₗ[ℂ] Matrix (Fin n) (Fin n) ℂ)
    (hT_pos : ∀ A : Matrix (Fin n) (Fin n) ℂ, A.PosSemidef → (T A).PosSemidef)
    (hT_trace : ∀ A : Matrix (Fin n) (Fin n) ℂ, (T A).trace = A.trace)
    (hT_one : T 1 = 1)
    (ρ : Matrix (Fin n) (Fin n) ℂ) (hρ : ρ.PosSemidef) (hρ_tr : ρ.trace = 1)
    (f : ℝ → ℝ) (hf : ConcaveOn ℝ (Set.Ici 0) f) :
    ∑ j, f (hρ.isHermitian.eigenvalues j) ≤ ∑ j, f ((hT_pos ρ hρ).isHermitian.eigenvalues j) := by sorry

end WallGSL
Source
A. C. Wall, The generalized second law implies a quantum singularity theorem, Class. Quantum Grav. 30 (2013) 165003, https://doi.org/10.1088/0264-9381/30/16/165003, Appendix, Corollary 4 and eqs. (A.8)–(A.10), p. 32
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent as the drafter; non-blind

Provenance note — this read-back is NOT blind. It was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source paper and of the intended meaning. It is therefore not independent testimony and must not be mistaken for a blind audit; reviewers should treat it as the drafter's own literal reading of the code and compare it against the source themselves.

Data. A natural number nn; a C\mathbb C-linear map TT on n×nn\times n complex matrices; an n×nn\times n complex matrix ρ\rho; and a function f:R→Rf:\mathbb R\to\mathbb R.

Hypotheses.

  1. TT maps positive semidefinite matrices to positive semidefinite matrices;
  2. tr⁡T(A)=tr⁡A\operatorname{tr}T(A)=\operatorname{tr}A for all AA;
  3. T(I)=IT(I)=I;
  4. ρ\rho is positive semidefinite with tr⁡ρ=1\operatorname{tr}\rho=1;
  5. ff is concave on [0,∞)[0,\infty) (no condition on (−∞,0)(-\infty,0)).

Conclusion. With λ1,…,λn\lambda_1,\dots,\lambda_n the eigenvalues of ρ\rho and μ1,…,μn\mu_1,\dots,\mu_n those of T(ρ)T(\rho) (with multiplicity),

∑j=1nf(λj) ≤ ∑j=1nf(μj).\sum_{j=1}^n f(\lambda_j)\ \le\ \sum_{j=1}^n f(\mu_j).

For n=0n=0 the trace of ρ\rho is 0≠10\ne1, so hypothesis 4 cannot hold and the statement is vacuous in that case.

Human review

  • Endorsed by Shuze Chen · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 8, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph