Schatten norms

noncomputable def schattenNorm {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) (p : ℝ) : ℝ

The Schatten p-norm of a matrix A is (Tr[(A*A)^(p/2)])^(1/p).

Equations

• schattenNorm A p = RCLike.re (⋯.cfc fun (x : ℝ) => x ^ (p / 2)).trace ^ (1 / p)

theorem schattenNorm_hermitian_pow {d : Type u_1} [Fintype d] [DecidableEq d] {A : HermitianMat d ℂ} (hA : 0 ≤ A) {p : ℝ} (hp : 0 < p) : schattenNorm (↑A) p = (A ^ p).trace ^ (1 / p)

theorem schattenNorm_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) (p : ℝ) : 0 ≤ schattenNorm A p

theorem schattenNorm_pow_eq {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (hA : 0 ≤ A) (p k : ℝ) (hp : 0 < p) (hk : 0 < k) : schattenNorm (↑(A ^ k)) p = schattenNorm (↑A) (k * p) ^ k

theorem trace_eq_schattenNorm_rpow {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (hA : 0 ≤ A) (r : ℝ) (hr : 0 < r) : (A ^ r).trace = schattenNorm (↑A) r ^ r

Relating schattenNorm to singular values

theorem schattenNorm_trace_as_eigenvalue_sum {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) (p : ℝ) : RCLike.re (⋯.cfc fun (x : ℝ) => x ^ (p / 2)).trace = ∑ i : d, ⋯.eigenvalues i ^ (p / 2)

theorem schattenNorm_rpow_eq_sum_singularValues {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) {p : ℝ} (hp : 0 < p) : schattenNorm A p ^ p = ∑ i : d, singularValues A i ^ p

theorem schattenNorm_eq_sum_singularValues_rpow {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) {p : ℝ} (hp : 0 < p) : schattenNorm A p = (∑ i : d, singularValues A i ^ p) ^ (1 / p)

theorem schattenNorm_rpow_eq_sum_sorted {d : Type u_1} [Fintype d] [DecidableEq d] (A : Matrix d d ℂ) {p : ℝ} (hp : 0 < p) : schattenNorm A p ^ p = ∑ i : Fin (Fintype.card d), singularValuesSorted A i ^ p

‖A‖_p^p equals the same sum over sorted singular values.

theorem HermitianMat.trace_young {d : Type u_1} [Fintype d] [DecidableEq d] (A B : HermitianMat d ℂ) (hA : 0 ≤ A) (hB : 0 ≤ B) (p q : ℝ) (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) : inner ℝ A B ≤ (A ^ p).trace / p + (B ^ q).trace / q

Scalar trace Young inequality for PSD matrices: ⟪A, B⟫ ≤ Tr[A^p]/p + Tr[B^q]/q for PSD A, B and conjugate p, q > 1.

theorem conjTranspose_half_mul_eq_conj {d : Type u_1} [Fintype d] [DecidableEq d] {A B : HermitianMat d ℂ} (hA : 0 ≤ A) : (↑(A ^ (1 / 2)) * ↑B).conjTranspose * (↑(A ^ (1 / 2)) * ↑B) = ↑((HermitianMat.conj ↑B) A)

For PSD A and Hermitian B, the product C = A^{1/2} * B satisfies C^* C = (A.conj B.mat).mat = B * A * B.

theorem schattenNorm_half_mul_rpow_eq_trace_conj {d : Type u_1} [Fintype d] [DecidableEq d] {A B : HermitianMat d ℂ} (hA : 0 ≤ A) {α : ℝ} (hα : 0 < α) : schattenNorm (↑(A ^ (1 / 2)) * ↑B) (2 * α) ^ (2 * α) = ((HermitianMat.conj ↑B) A ^ α).trace

Schatten–Hölder inequality

The Schatten–Hölder inequality for matrix products: For matrices A, B and exponents r, p, q > 0 with 1/r = 1/p + 1/q, the Schatten r-norm of the product satisfies ‖A * B‖_{S^r} ≤ ‖A‖_{S^p} * ‖B‖_{S^q}. This version includes the quasi-norm case (r, p, q < 1).

Proof sketch

The proof proceeds in three steps:

1. Express Schatten norms in terms of singular values: ‖A‖_p = (∑ σᵢ(A)^p)^{1/p}.
2. Use the weak log-majorization of singular values of products (weakLogMaj_singularValues_mul + sum_rpow_le_of_weakLogMaj) to obtain ∑ σᵢ(AB)^r ≤ ∑ σ↓ᵢ(A)^r · σ↓ᵢ(B)^r.
3. Apply the classical Hölder inequality for finite sums (NNReal.inner_le_Lp_mul_Lq from Mathlib, with conjugate exponents p/r and q/r) to bound ∑ σ↓ᵢ(A)^r · σ↓ᵢ(B)^r ≤ (∑ σᵢ(A)^p)^{r/p} · (∑ σᵢ(B)^q)^{r/q}.
4. Take 1/r-th powers and combine.

theorem schattenNorm_mul_le {d : Type u_1} [Fintype d] [DecidableEq d] (A B : Matrix d d ℂ) {r p q : ℝ} (hr : 0 < r) (hp : 0 < p) (hq : 0 < q) (hpqr : 1 / r = 1 / p + 1 / q) : schattenNorm (A * B) r ≤ schattenNorm A p * schattenNorm B q

theorem HermitianMat.trace_rpow_conj_le {d : Type u_1} [Fintype d] [DecidableEq d] {A B : HermitianMat d ℂ} (hA : 0 ≤ A) (hB : 0 ≤ B) {α p q : ℝ} (hα : 0 < α) (hp : 0 < p) (hq : 0 < q) (hpq : 1 / (2 * α) = 1 / p + 1 / q) : ((conj ↑B) A ^ α).trace ≤ ((A ^ (p / 2)).trace ^ (1 / p) * (B ^ q).trace ^ (1 / q)) ^ (2 * α)