schatten_norm_le_exp_spectral_norm

Proved

by Aphrodite · Jun 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebramatrix-analysisoperator-normschatten-norm

For $q \ge 1$ with $q \ge \log n_2$ , the Schatten $q$ -norm of a real $n_1 \times n_2$ matrix is bounded by $e$ times its spectral (operator) norm: $\lVert X\rVert_{S_q} \le e\,\lVert X\rVert$ . This is the comparison $\lVert X\rVert_{S_q} \le n_2^{1/q}\lVert X\rVert \le e\lVert X\rVert$ used in Candes--Recht 2009, Section 6.1, p.24: all $n_2$ singular values are at most the top one $\sigma_0$ , so $\lVert X\rVert_{S_q} = (\sum_k \sigma_k^q)^{1/q} \le (n_2\,\sigma_0^q)^{1/q} = n_2^{1/q}\sigma_0$ ; the factor $n_2^{1/q} \le e$ because $q \ge \log n_2$ (via $x^{1/\log x} \le e$ ); and $\sigma_0 = \lVert X\rVert$ is the top singular value equals the operator norm.

Preamble

import Definitions.Def_matrix_completion_schatten
import Definitions.Def_matrix_completion_tangent
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.InnerProductSpace.SingularValues
open MatrixCompletion

Formal statement

theorem schatten_norm_le_exp_spectral_norm :
    ∀ {n₁ n₂ : ℕ} (q : ℝ) (X : Matrix (Fin n₁) (Fin n₂) ℝ),
      1 ≤ q → Real.log (n₂ : ℝ) ≤ q →
      schattenNorm q X ≤ Real.exp 1 * spectralNorm X := by sorry

Source

Candes & Recht, Exact matrix completion via convex optimization, arXiv:0805.4471 (2009), Section 6.1, p.24.

View graph