Trace distance $\|M - N\|_1$

Definition

WildeQIT_traceDist

by aadarwal · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

matrix-analysisquantum-informationtrace-distancetrace-normwilde-qit

Definition 9.1.2 (Trace Distance). Given any two operators $M, N \in \mathcal{L}(\mathcal{H}, \mathcal{H}')$ , the trace distance between them is

\|M - N\|_1 .

For density operators $\rho, \sigma$ the trace distance $\|\rho - \sigma\|_1$ is the operational measure of distinguishability of the two states (Chapter 9); every later result of §9.1 (probability-difference characterization, triangle inequality, monotonicity under partial trace and channels, strong convexity, the diamond norm) is phrased with it.

Formalization Note. WildeQIT.traceDist M N := WildeQIT.traceNorm (M - N) for (possibly rectangular) matrices M N : Matrix m n ℂ, where WildeQIT.traceNorm is Definition 9.1.1 (Definitions.Def_WildeQIT_traceNorm). It is not normalized: the book's normalized trace distance is $\tfrac12 \|\rho-\sigma\|_1$ .

Definition code

import Definitions.Def_WildeQIT_traceNorm

/-!
Wilde, *Quantum Information Theory* (2nd ed.), §9.1.2, Definition 9.1.2 (Trace Distance).

Given any two operators `M, N ∈ L(H, H')`, the trace distance between them is `‖M − N‖₁`.
-/

namespace WildeQIT

/-- **Definition 9.1.2 (Trace Distance).** The trace distance between two
(possibly rectangular) matrices `M N : Matrix m n ℂ` is the trace norm of their difference,
`‖M − N‖₁`. -/
noncomputable def traceDist {m n : Type} [Fintype m] [Fintype n] [DecidableEq n]
    (M N : Matrix m n ℂ) : ℝ :=
  traceNorm (M - N)

end WildeQIT

Source

Wilde, *Quantum Information Theory*, 2nd ed. (Cambridge University Press, 2017; arXiv:1106.1445v8), §9.1.2 "Trace Distance from the Trace Norm", Definition 9.1.2 (Trace Distance).

View graph

Trace distance ∥M−N∥1\|M - N\|_1∥M−N∥1​

Trace distance $\|M - N\|_1$