QuantumInfo.ForMathlib.MatrixNorm.TraceNorm

source

noncomputable def Matrix.traceNorm {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [RCLike R] (A : Matrix m n R) :

ℝ

The trace norm of a matrix: Tr[√(A† A)].

Equations

A.traceNorm = RCLike.re (CFC.sqrt (A.conjTranspose * A)).trace

Instances For

source

@[simp]

theorem Matrix.traceNorm_zero {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [RCLike R] :

traceNorm 0 = 0

source

@[simp]

theorem Matrix.traceNorm_neg {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [RCLike R] (A : Matrix m n R) :

(-A).traceNorm = A.traceNorm

The trace norm of the negative is equal to the trace norm.

source

theorem Matrix.traceNorm_isometry_left {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [RCLike R] {k : Type u_4} [Fintype k] {A : Matrix n m R} {u : Matrix k n R} (hu₁ : u.Isometry) :

(u * A).traceNorm = A.traceNorm

The trace norm is invariant under left multiplication by an isometry.

source

theorem Matrix.traceNorm_isometry_right {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [RCLike R] {k : Type u_4} [Fintype k] {A : Matrix n m R} {u : Matrix k m R} (hu₁ : u.Isometry) :

(A * u.conjTranspose).traceNorm = A.traceNorm

The trace norm is invariant under right multiplication by the adjoint of an isometry.

source

@[simp]

theorem Matrix.traceNorm_unitary_conj {n : Type u_2} {R : Type u_3} [Fintype n] [RCLike R] {A : Matrix n n R} {U : ↥(unitaryGroup n R)} :

(↑U * A * (↑U).conjTranspose).traceNorm = A.traceNorm

The trace norm is invariant under unitary conjugation.

source

theorem Matrix.traceNorm_Hermitian_eq_sum_abs_eigenvalues {n : Type u_2} {R : Type u_3} [Fintype n] [RCLike R] {A : Matrix n n R} (hA : A.IsHermitian) :

A.traceNorm = ∑ i : n, |hA.eigenvalues i|

For Hermitian matrices, the trace norm is the sum of absolute eigenvalues.

This is Proposition 9.1.1 in Wilde.

source

theorem Matrix.traceNorm_nonneg {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [RCLike R] (A : Matrix m n R) :

0 ≤ A.traceNorm

The trace norm is nonnegative. Property 9.1.1 in Wilde.

source

theorem Matrix.traceNorm_zero_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [RCLike R] (A : Matrix m n R) :

A.traceNorm = 0 ↔ A = 0

The trace norm is zero iff the matrix is zero.

source

theorem Matrix.traceNorm_smul {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [RCLike R] (A : Matrix m n R) (c : R) :

(c • A).traceNorm = ‖c‖ * A.traceNorm

The trace norm is homogeneous under scalar multiplication. Property 9.1.2 in Wilde.

source

theorem Matrix.exists_svd_sqrt_eigenvalues {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) :

have hH := ⋯; ∃ (V : ↥𝐔[n]) (W : ↥𝐔[n]), A = (↑V * diagonal fun (i : n) => ↑√(hH.eigenvalues i)) * (↑W).conjTranspose

Singular value decomposition for square complex matrices, with singular values expressed as square roots of the eigenvalues of Aᴴ * A.

source

theorem Matrix.traceNorm_eq_sum_singularValues {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) :

A.traceNorm = ∑ i : n, singularValues A i

The trace norm of a square complex matrix is the sum of its singular values.

source

theorem Matrix.traceNorm_eq_sum_singularValuesSorted {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) :

A.traceNorm = ∑ i : Fin (Fintype.card n), singularValuesSorted A i

The trace norm of a square complex matrix is the sum of its sorted singular values.

source

theorem Matrix.singularValues_le_opNorm {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) (i : n) :

singularValues A i ≤ ‖A‖

Every singular value is bounded by the operator norm.

source

theorem Matrix.traceNorm_mul_le_opNorm_traceNorm {n : Type u_2} [Fintype n] [DecidableEq n] (A B : Matrix n n ℂ) :

(A * B).traceNorm ≤ ‖A‖ * B.traceNorm

The trace norm is bounded by the operator norm on the left times the trace norm on the right.

source

theorem Matrix.traceNorm_conjTranspose {n : Type u_2} [Fintype n] (A : Matrix n n ℂ) :

A.conjTranspose.traceNorm = A.traceNorm

The trace norm is invariant under conjugate transpose.

source

theorem Matrix.traceNorm_mul_le_traceNorm_opNorm {n : Type u_2} [Fintype n] [DecidableEq n] (A B : Matrix n n ℂ) :

(A * B).traceNorm ≤ A.traceNorm * ‖B‖

The trace norm is bounded by trace norm on the left times operator norm on the right.

source

theorem Matrix.traceNorm_sandwich_le {n : Type u_2} [Fintype n] [DecidableEq n] {S M T : Matrix n n ℂ} (hS : ‖S‖ ≤ 1) (hT : ‖T‖ ≤ 1) :

(S * M * T).traceNorm ≤ M.traceNorm

Multiplication on both sides by contractions does not increase trace norm.

source

theorem Matrix.abs_trace_le_traceNorm {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) :

‖A.trace‖ ≤ A.traceNorm

The absolute value of the trace is bounded by the trace norm.

source

theorem Matrix.traceNorm_eq_max_re_tr_U {n : Type u_2} [Fintype n] (A : Matrix n n ℂ) :

IsGreatest {x : ℝ | ∃ (U : ↥𝐔[n]), (↑U * A).trace.re = x} A.traceNorm

For square complex matrices, the trace norm is the maximum of re (Tr[U * A]) over unitaries U.

source

theorem Matrix.traceNorm_add_le {n : Type u_2} [Fintype n] (A B : Matrix n n ℂ) :

(A + B).traceNorm ≤ A.traceNorm + B.traceNorm

The trace norm satisfies the triangle inequality for square complex matrices.

source

theorem Matrix.PosSemidef.traceNorm_eq_trace {m : Type u_1} {R : Type u_3} [Fintype m] [RCLike R] {A : Matrix m m R} (hA : A.PosSemidef) :

↑A.traceNorm = A.trace

A positive semidefinite matrix has trace norm equal to its trace.

source

theorem Matrix.traceNorm_convex {n : Type u_2} [Fintype n] (M N : Matrix n n ℂ) (l : ℝ) (hl : 0 ≤ l ∧ l ≤ 1) :

(↑l • M + (1 - ↑l) • N).traceNorm ≤ l * M.traceNorm + (1 - l) * N.traceNorm

The trace norm is convex. Property 9.1.5 in Wilde.