spectral_norm_le_schatten_norm
Provedlinear-algebramatrix-completionschatten-norm
For an exponent , the spectral (operator) norm of a real matrix is at most its Schatten -norm: . With singular values , — the Schatten norms decrease to the operator norm as .
Preamble
import Definitions.Def_matrix_completion_schatten open MatrixCompletion
Formal statement
theorem spectral_norm_le_schatten_norm :
∀ {n₁ n₂ : ℕ} (q : ℕ) (Y : Matrix (Fin n₁) (Fin n₂) ℝ),
1 ≤ q →
spectralNorm Y ≤ schattenNorm (q : ℝ) Y := by sorrySource
Candes & Recht, Exact matrix completion via convex optimization, CACM 55.6 (2012).