Trace-norm contraction on Hermitian inputs

Open

QAlgorithms.Papers.Independent.Intakethird100.P81.hermitian_trace_norm_contraction

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

prove2quantum

Let $\rho$ be any Hermitian matrix on a finite-dimensional complex Hilbert space, and let $F$ be a complex-linear, completely positive, trace-preserving map to another finite-dimensional complex matrix space. Then

\|F(\rho)\|_1\le\|\rho\|_1.

Here the trace norm is $\operatorname{Tr}\sqrt{M^\dagger M}$ , without a factor of one half. The input need not be positive or have trace one, so the statement controls signed Hermitian perturbations as well as states.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P81

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ENNReal

attribute [local instance] Classical.propDecidable

namespace QAlgorithms.Papers.Independent.Intakethird100.P81

open QAlgorithms.Papers.Independent.Information100.P54 (relativeEntropyBits)

open QAlgorithms.Papers.Independent.Bridge50.P44 (ClassicalFirst)

/-- Lemma 1, PDF p.9: contraction for arbitrary Hermitian inputs, not merely states. -/
theorem hermitian_trace_norm_contraction {I J : Type*}
    [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
    (rho : Matrix I I ℂ) (hrho : rho.IsHermitian) (F : Superop I J)
    (hF : IsChannel F) : traceNorm (F rho) ≤ traceNorm rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P81

end

Source

On rounds in quantum communication, arXiv:quant-ph/0004100v5, PDF p. 9, Lemma 1

Read-back

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

For all finite types $I,J$ with decidable equality, every Hermitian complex matrix $\rho$ on $I$ , and every function $F$ from complex matrices on $I$ to complex matrices on $J$ , suppose there exist a natural number $m$ and matrices $E_0,\ldots,E_{m-1}$ from $\mathbb C^I$ to $\mathbb C^J$ such that

\sum_{j=0}^{m-1}E_j^\dagger E_j=1, \qquad F(X)=\sum_{j=0}^{m-1}E_jXE_j^\dagger \quad\text{for every matrix }X.

Then $\|F(\rho)\|_1\le\|\rho\|_1$ , where $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , with the square root defined by continuous functional calculus. The matrix $\rho$ need not be positive or normalized. Empty index types and $m=0$ are included whenever the stated completeness equation can hold.

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