CR-1: perturbing a unitary moves states by at most twice the operator-norm defect

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

The bridge between the two norms a perturbative quantum argument uses: drives are estimated in the L2 operator norm (the C*-norm, where Duhamel and Trotter bounds live), while states are compared in the trace distance (the operational metric, where the data-processing inequality lives). This file connects them:

★★ traceDist_conj_sub_le — D(UρU†, VρV†) ≤ 2‖U − V‖

for unitaries U, V and any density operator ρ. Nothing about the two unitaries is assumed beyond unitarity: the bound is uniform in ρ and free of dimension factors.

Route

The difference D = UρU† − VρV† is Hermitian and traceless, so the variational collapse applies (traceDist_eq_re_trace_posPart) and D₊ = D·P₊ (mul_posProj_eq_posPart) turns the distance into a single trace Re Tr(D·P₊). Splitting

UρU† − VρV† = (U−V)ρU† + Vρ(U−V)†

and cycling the trace reduces the bound to two instances of the Hölder-lite

|Re Tr(ρ·M)| ≤ ‖M‖ · Re Tr ρ (abs_re_trace_mul_le, for ρ PSD),

proved by diagonalising ρ (IsHermitian.spectral_theorem), reading the trace as the eigenvalue-weighted diagonal of the unitarily rotated M, and bounding each diagonal entry by the operator norm (norm_entry_le_l2_opNorm). The projector's norm bound comes from norm_cfc_le, the general statement that a Hermitian functional calculus is bounded by the sup of the applied function over the spectrum.

⚠️ Scope: finite dimensions, IsHermitian.cfc (not the general continuous functional calculus). abs_re_trace_mul_le is stated for the real part because that is what the variational characterisation consumes; the modulus version would need |Tr(ρM)| ≤ ‖M‖ Tr ρ through the same spectral route and is not needed here.

Provenance

Named CR-1 and feasibility-checked in specs/channel-rg-scoping.md §6 (CV-25); the first brick of the CV-26 arc. Intended upstream location: beside Mathlib/Analysis/CStarAlgebra/Matrix.lean's unitary bounds, or with the trace-distance material once that is upstreamed.

Tags

trace distance, operator norm, unitary perturbation, functional calculus

Norm bounds from the functional calculus

theorem QuantumInfo.norm_cfc_le {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {A : Matrix n n ℂ} (hA : A.IsHermitian) (f : ℝ → ℝ) {C : ℝ} (hC : 0 ≤ C) (hf : ∀ (i : n), |f (hA.eigenvalues i)| ≤ C) : ‖hA.cfc f‖ ≤ C

The functional calculus is bounded by the function on the spectrum: ‖cfc f‖ ≤ C whenever |f(λᵢ)| ≤ C at every eigenvalue. The conjugating factors are unitary, so the bound is the diagonal one.

theorem QuantumInfo.norm_posProj_le_one {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {A : Matrix n n ℂ} (hA : A.IsHermitian) : ‖posProj hA‖ ≤ 1

The positive-eigenspace projector has norm at most one — its spectrum is {0, 1}.

The Hölder-lite bound

theorem QuantumInfo.abs_re_trace_mul_le {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {ρ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (M : Matrix n n ℂ) : |RCLike.re (ρ * M).trace| ≤ ‖M‖ * RCLike.re ρ.trace

★ Hölder-lite: |Re Tr(ρ·M)| ≤ ‖M‖ · Re Tr ρ for positive semidefinite ρ. Diagonalising ρ reads the trace as the eigenvalue-weighted diagonal of the rotated M, and every diagonal entry is bounded by the operator norm.

The bridge

theorem QuantumInfo.traceDist_conj_sub_le {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {U V ρ : Matrix n n ℂ} (hU : U ∈ Matrix.unitaryGroup n ℂ) (hV : V ∈ Matrix.unitaryGroup n ℂ) (hρ : ρ.PosSemidef) (htr : ρ.trace = 1) (h : (U * ρ * U.conjTranspose - V * ρ * V.conjTranspose).IsHermitian) : traceDist h ≤ 2 * ‖U - V‖

★★ CR-1: the unitary-perturbation bridge. Conjugating a state by two nearby unitaries moves it by at most twice their operator-norm distance:

D(UρU†, VρV†) ≤ 2‖U − V‖.

Uniform in the state and free of dimension factors — the interface that turns a Duhamel or Trotter estimate on drives into a statement about distinguishability of the states they produce.