Trace norm and trace distance (K3 foundation) #
Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).
The trace norm of a Hermitian matrix and the trace distance of two states, the metric of statistical distinguishability:
traceNorm A = ∑ᵢ |λᵢ(A)| (sum of absolute eigenvalues = Tr|A| for Hermitian A),
traceDist ρ σ = ½ · traceNorm (ρ − σ).
This is the K3 metric-core tranche (K3 of specs/qi-qec-roadmap.md). It delivers the
definitions and the complete metric:
- non-negativity (
traceNorm_nonneg,traceDist_nonneg); - the distinguishability headline
traceDist ρ σ = 0 ↔ ρ = σ(traceDist_eq_zero_iff) — zero trace distance iff the states are identical — viaeigenvalues_eq_zero_iff; - symmetry
traceDist ρ σ = traceDist σ ρ(traceDist_comm), via the functional-calculus bridgetraceNorm A = Re Tr(cfc |·| A)(re_trace_cfc) andcfc_comp_neg(|−x| = |x|); - the triangle inequality
traceDist ρ τ ≤ traceDist ρ σ + traceDist σ τ(traceDist_triangle), completing the metric, reduced to trace-norm subadditivity‖A+B‖₁ ≤ ‖A‖₁ + ‖B‖₁(traceNorm_add_le). Since Mathlib registers no Loewner order on matrices and the signaturesgn/positive projector are discontinuous, this is proved via the Jordan decomposition built fromMatrix.IsHermitian.cfc(defined for anyf, including the discontinuousposProj):posPart/negPart/posProj, the PSD-product trace boundtr_psd_mul_nonneg(0 ≤ Re Tr(S·P)for PSDS,P, via√S = cfc √ S), and the operator boundRe Tr(A·P) ≤ Re Tr(A₊)for0 ≤ P ≤ I; traceNorm_of_posSemidef: the trace norm of a PSD operator is its trace (so a density operator has trace norm1).
The posPart/negPart/posProj Jordan primitives and the IsHermitian.cfc algebra layer
are exposed as named QuantumInfo declarations: they recur in the next K3 tranche.
The CPTP data-processing inequality traceDist (Φρ) (Φσ) ≤ traceDist ρ σ (channels cannot
increase distinguishability) builds on this file's posPart/posProj machinery and the key
bound re_trace_mul_le_re_trace_posPart (the variational half Re Tr((ρ−σ)·P) ≤ Re Tr((ρ−σ)₊),
achieved at P = posProj (ρ−σ)); it is proved in DataProcessing.lean (channel_traceDist_le,
done 2026-06-09) via the channel adjoint. So K3 (metric + data-processing) is complete.
The trace norm of a Hermitian matrix, ‖A‖₁ = ∑ᵢ |λᵢ(A)| = Tr|A|: the sum of the
absolute values of its (real) eigenvalues.
Equations
- QuantumInfo.traceNorm hA = ∑ i : n, |hA.eigenvalues i|
Instances For
The trace distance D(ρ,σ) = ½‖ρ − σ‖₁: the metric of statistical
distinguishability.
Equations
Instances For
The trace norm is non-negative.
The trace distance is non-negative.
The trace norm vanishes iff the matrix is zero. From ∑ᵢ |λᵢ| = 0 ↔ all λᵢ = 0 and
IsHermitian.eigenvalues_eq_zero_iff.
Distinguishability headline: zero trace distance iff the states coincide.
traceDist ρ σ = 0 ↔ ρ = σ.
The trace distance of a state to itself is zero.
Bridge to the functional calculus: traceNorm A = Re Tr(cfc |·| A) = Re Tr|A|.
The Hermitian functional calculus cfc |·| A = U · diag(|λᵢ|) · Uᴴ, whose trace is
∑ᵢ |λᵢ| by cyclicity of the trace and unitarity. This identifies the eigenvalue-sum
definition with the operator absolute value, the form on which cfc_comp_neg acts.
Helper: traceNorm depends only on the underlying matrix (transport along A = B).
Helper: traceDist depends only on the underlying difference matrix (transport along the
equality ρ − σ = ρ' − σ').
The trace norm is invariant under negation: traceNorm (−A) = traceNorm A. Via the
functional-calculus bridge and cfc_comp_neg (|−x| = |x|).
Symmetry of the trace distance: traceDist ρ σ = traceDist σ ρ.
The trace norm of a positive-semidefinite operator is its trace. Since a PSD operator
has non-negative eigenvalues, ∑ᵢ |λᵢ| = ∑ᵢ λᵢ = Tr A. In particular a density operator
(PSD, unit trace) has trace norm 1.
Trace-norm subadditivity (the triangle inequality) #
The route follows specs/trace-distance-triangle-plan.md: a Jordan decomposition of a
Hermitian matrix into positive/negative parts via the Hermitian functional calculus
Matrix.IsHermitian.cfc f = U · diag(↑∘f∘λ) · Uᴴ (defined for any f : ℝ → ℝ, so the
discontinuous positive-eigenspace projector is admissible), plus the linchpin
tr_psd_mul_nonneg : 0 ≤ Re Tr(S·P) for S, P positive-semidefinite.
IsHermitian.cfc f is Hermitian. U · diag(↑∘f∘λ) · Uᴴ is self-adjoint because the
diagonal of real values is.
Multiplicativity of IsHermitian.cfc: (hM.cfc f)·(hM.cfc g) = hM.cfc (f·g). The
two conjugating unitaries collapse via Uᴴ U = 1 and diagonal_mul_diagonal.
Additivity of IsHermitian.cfc: (hM.cfc f) + (hM.cfc g) = hM.cfc (f + g)
(pointwise sum). Same conjugated-diagonal collapse as cfc_mul, with diagonal_add.
IsHermitian.cfc (fun _ => 0) = 0.
IsHermitian.cfc id = A: the functional calculus of the identity recovers the operator
(the spectral theorem).
IsHermitian.cfc of a pointwise non-negative function is positive-semidefinite:
U · diag(↑∘g∘λ) · Uᴴ with g ∘ λ ≥ 0.
The linchpin (TR-PSD): for positive-semidefinite S, P, 0 ≤ Re Tr(S·P). Route:
√S := S.cfc Real.sqrt is Hermitian with √S·√S = S (PSD eigenvalues), so
Tr(S·P) = Tr(√S·P·(√S)ᴴ) by trace cyclicity, and √S·P·(√S)ᴴ is PSD with non-negative
trace.
The positive part of a Hermitian matrix, A₊ = U · diag(λᵢ⁺) · Uᴴ with
λ⁺ = max λ 0. Reusable Jordan-decomposition primitive.
Equations
- QuantumInfo.posPart hA = hA.cfc fun (x : ℝ) => max x 0
Instances For
The negative part of a Hermitian matrix, A₋ = U · diag(λᵢ⁻) · Uᴴ with
λ⁻ = max (−λ) 0, so that A = A₊ − A₋ and |A| = A₊ + A₋.
Instances For
The positive-eigenspace projector P₊ = U · diag(1_{λᵢ>0}) · Uᴴ. Discontinuous, hence
built through IsHermitian.cfc (admissible for any f), never generic cfc.
Instances For
IsHermitian.cfc (fun _ => 1) = 1.
1 − P₊ is positive-semidefinite: it equals hA.cfc (1_{x ≤ 0}), a non-negative cfc.
H · P₊ = H₊ (the positive part as H times its positive-eigenspace projector):
pointwise x · 1_{x>0} = max x 0.
H₊ − H₋ = H (Jordan decomposition): pointwise max x 0 − max (−x) 0 = x.
The trace of H₊ is real and equals ∑ᵢ λᵢ⁺; combined with the matching H₋ fact,
traceNorm = Re Tr(H₊) + Re Tr(H₋).
L5: traceNorm H = Re Tr(H₊) + Re Tr(H₋) — the trace norm as the sum of the traces of
the two Jordan parts (∑ |λᵢ| = ∑ λᵢ⁺ + ∑ λᵢ⁻).
L6 (key bound): for Hermitian A and P with both P and 1 − P positive-
semidefinite, Re Tr(A·P) ≤ Re Tr(A₊). Write A = A₊ − A₋; then
Tr(A·P) = Tr(A₊·P) − Tr(A₋·P) ≤ Tr(A₊·P) ≤ Tr(A₊) by tr_psd_mul_nonneg twice
(Tr(A₋·P) ≥ 0, Tr(A₊·(1−P)) ≥ 0).
L7: for Hermitian A, B and H = A + B, Re Tr(H₊) ≤ Re Tr(A₊) + Re Tr(B₊). Use
Tr(H₊) = Tr(H·P₊) = Tr(A·P₊) + Tr(B·P₊) and the key bound L6 on each summand with
P = P₊(H) (which has P₊, 1 − P₊ both PSD).
L6 (negative-part key bound): for Hermitian A and P with P, 1 − P PSD,
−Re Tr(A₋) ≤ Re Tr(A·P). From Tr(A·P) = Tr(A₊·P) − Tr(A₋·P) ≥ 0 − Tr(A₋) = −Tr(A₋)
(Tr(A₊·P) ≥ 0, Tr(A₋·(1−P)) ≥ 0).
H · P₋ = −H₋ where P₋ = 1 − P₊ is the non-positive-eigenspace projector:
pointwise x · (1 − 1_{x>0}) = x · 1_{x≤0} = −max(−x) 0.
L7 (negative part): Re Tr(H₋) ≤ Re Tr(A₋) + Re Tr(B₋) for H = A + B.
L8: trace-norm subadditivity ‖A + B‖₁ ≤ ‖A‖₁ + ‖B‖₁ for Hermitian A, B. Splits
traceNorm = Re Tr(·₊) + Re Tr(·₋) and bounds each part by L7 (posPart) and its
negative-part counterpart.
L9: the trace-distance triangle inequality D(ρ,τ) ≤ D(ρ,σ) + D(σ,τ) — completing the
metric. From traceNorm subadditivity on ρ − τ = (ρ − σ) + (σ − τ) and D = ½‖·‖₁.