Data-processing inequality for the trace distance (K3)

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

The CPTP data-processing inequality for the trace distance: a quantum channel cannot increase distinguishability,

traceDist (Φ ρ) (Φ σ) ≤ traceDist ρ σ (channel_traceDist_le),

for Hermitian, equal-trace ρ, σ (in particular any two density operators). This is the final K3 metric property after non-negativity, the distinguishability headline, symmetry, and the triangle inequality (TraceDistance.lean).

Route — the variational characterisation

For a traceless Hermitian difference D = ρ − σ the trace distance collapses to a single trace,

traceDist D = Re Tr(D₊) (traceDist_eq_re_trace_posPart),

since Tr|D| = Tr(D₊) + Tr(D₋) while Tr(D₊) − Tr(D₋) = Tr D = 0 forces the two parts to have equal trace. The positive part is realised as D₊ = D · P₊ at the positive-eigenspace projector P₊ (mul_posProj_eq_posPart), giving the variational reading Re Tr(D₊) = Re Tr(P₊ · D) = max₀≤P≤I Re Tr(P · D) — the maximum is attained at P = P₊, so no sSup is needed.

The headline then chains: the optimal projector on the channel side, P := P₊(Φ ρ − Φ σ), is pulled back through the channel adjoint (Channel.adjoint, Φ†(P) = ∑ᵢ Kᵢᴴ P Kᵢ) using the trace duality Tr(P · Φ D) = Tr(Φ† P · D) (adjoint_trace_mul). Unitality and positivity of the adjoint give 0 ≤ Φ† P ≤ I (adjoint_le_one), so Φ† P is an admissible projector candidate on the input side, and the operator bound Re Tr(D · Q) ≤ Re Tr(D₊) (re_trace_mul_le_re_trace_posPart, the L6 key bound from TraceDistance.lean) closes the inequality. The whole argument consumes the channel adjoint (unital + positive ⟹ 0 ≤ Φ† P ≤ I) and the posPart/posProj Jordan machinery.

theorem QuantumInfo.traceDist_eq_re_trace_posPart {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (h : (ρ - σ).IsHermitian) (htr : (ρ - σ).trace = 0) : traceDist h = RCLike.re (posPart h).trace

Variational collapse for a traceless Hermitian difference: traceDist D = Re Tr(D₊). From traceNorm D = Re Tr(D₊) + Re Tr(D₋) (Jordan split) and Re Tr(D₊) = Re Tr(D₋), which holds because Tr(D₊) − Tr(D₋) = Tr D = 0.

theorem QuantumInfo.channel_traceDist_le {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_2} {ι : Type u_3} [Fintype m] [Fintype ι] [DecidableEq m] (Φ : Channel n m ι) {ρ σ : Matrix n n ℂ} (hρ : ρ.IsHermitian) (hσ : σ.IsHermitian) (htr : ρ.trace = σ.trace) : traceDist ⋯ ≤ traceDist ⋯

Data-processing inequality for the trace distance. A quantum channel cannot increase distinguishability: traceDist (Φ ρ) (Φ σ) ≤ traceDist ρ σ, for Hermitian, equal-trace ρ, σ (so in particular for any two density operators). Via the variational characterisation traceDist D = Re Tr(D₊), the channel adjoint pull-back Tr(P · Φ D) = Tr(Φ† P · D), and the operator bound Re Tr(D · Q) ≤ Re Tr(D₊) at the admissible Q = Φ† P₊ with 0 ≤ Q ≤ I.

theorem QuantumInfo.traceDist_le_one {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (hσ : σ.PosSemidef) (htrρ : ρ.trace = 1) (htrσ : σ.trace = 1) : traceDist ⋯ ≤ 1

The trace distance of two states is at most one (boundedness of the metric on the density-operator set). For PSD unit-trace ρ, σ, traceDist ρ σ ≤ 1. Via the variational form traceDist D = Re Tr(D₊) = Re Tr((ρ−σ)·P₊), dropping the σ term (Tr(σ·P₊) ≥ 0) and bounding Re Tr(ρ·P₊) ≤ Re Tr ρ = 1 (from Tr(ρ·(1−P₊)) ≥ 0), both by tr_psd_mul_nonneg.

theorem QuantumInfo.traceDist_conj_unitary {n : Type u_1} [Fintype n] [DecidableEq n] {U : Matrix n n ℂ} (hU : U.conjTranspose * U = 1) {ρ σ : Matrix n n ℂ} (hρ : ρ.IsHermitian) (hσ : σ.IsHermitian) (htr : ρ.trace = σ.trace) (hUconj : (U * ρ * U.conjTranspose - U * σ * U.conjTranspose).IsHermitian) : traceDist hUconj = traceDist ⋯

Unitary invariance of the trace distance (the equality case of data processing): for a unitary U (Uᴴ U = 1) and Hermitian, equal-trace ρ, σ, traceDist (UρUᴴ − UσUᴴ) = traceDist (ρ − σ). Proved via channel_traceDist_le applied to the unitaryChannel in both directions (the reverse using the channel of Uᴴ, which is unitary since U Uᴴ = 1 by Matrix.mul_eq_one_comm), then le_antisymm after collapsing Uᴴ(UρUᴴ)U = ρ.