Documentation

QuantumInfo.ForMathlib.MatrixNorm.TraceNorm

source
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
Instances For
    source
    @[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.

    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|
    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 only if 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

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

    source
    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.

    source
    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.

    source
    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
    source
    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