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

@[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

@[simp]

theorem Matrix.traceNorm_eq_neg_self {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.

theorem Matrix.cfc_sqrt_isometry_conj {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [RCLike R] {A : Matrix n n R} (hA : 0 ≤ A) {u : Matrix m n R} (hu₁ : u.Isometry) : CFC.sqrt (u * A * u.conjTranspose) = u * CFC.sqrt A * u.conjTranspose

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

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

theorem Matrix.traceNorm_isometry_conj {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [RCLike R] {A : Matrix n n R} {u : Matrix m n R} (hu : u.Isometry) {v : Matrix m n R} (hv : v.Isometry) : (u * A * v.conjTranspose).traceNorm = A.traceNorm

The trace norm is invariant under isometries u and v, Property 9.1.4 in Wilde

@[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

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|

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

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.

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

Trace norm is linear under scalar multiplication. Property 9.1.2 in Wilde

theorem Matrix.traceNorm_eq_max_tr_U {n : Type u_2} {R : Type u_3} [Fintype n] [RCLike R] (A : Matrix n n R) : IsGreatest {x : R | ∃ (U : ↥(unitaryGroup n R)), (↑U * A).trace = x} ↑A.traceNorm

For square matrices, the trace norm is max Tr[U * A] over unitaries U.

theorem Matrix.traceNorm_triangleIneq {n : Type u_2} {R : Type u_3} [Fintype n] [RCLike R] (A B : Matrix n n R) : (A + B).traceNorm ≤ A.traceNorm + B.traceNorm

the trace norm satisfies the triangle inequality (for square matrices). TODO: Prove in general.

theorem Matrix.traceNorm_triangleIneq' {n : Type u_2} {R : Type u_3} [Fintype n] [RCLike R] (A B : Matrix n n R) : (A - B).traceNorm ≤ A.traceNorm + B.traceNorm

theorem Matrix.PosSemidef.traceNorm_PSD_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

theorem Matrix.traceNorm_convex {n : Type u_2} {R : Type u_3} [Fintype n] [RCLike R] (M N : Matrix n n R) (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