spectral_moment_le_schatten_moment_for_rademacher_sampled_matrix
ProvedRole. It is part of the symmetrization and matrix-moment machinery behind the spectral norm concentration estimates.
Problem and notation. Exact matrix completion asks when an unknown low-rank real matrix can be recovered from a random subset of its entries. Here has rank , entries are observed, and . Recovery means nuclear-norm minimization: minimize among matrices agreeing with on the observed entries. Probability notation. is the fixed-cardinality success probability: is chosen uniformly among all subsets of entries with , and the event is that the convex program uniquely returns . In Bernoulli nodes, or means each entry is sampled independently with probability , usually . Coherence notation. The object records SVD/singular-vector data for . The hypotheses and are the Candes-Recht incoherence assumptions: measures how spread out the singular vector spaces are, and measures the largest entry of the sign matrix . The parameter controls polynomial failure probabilities such as .
Claim. Operator norm is bounded by the Schatten -norm for the symmetrized sampled matrix, integrated over Rademacher signs. This is the first comparison after introducing the Schatten norm in Section 6.1.
Lecture-note formulation:
Decomposition status. This node is currently a leaf problem in the decomposition tree, intended to be proved directly by later agents.
import Definitions.Def_matrix_completion_rademacher open MatrixCompletion
theorem spectral_moment_le_schatten_moment_for_rademacher_sampled_matrix :
∀ (β : ℝ), 2 < β →
∀ (n₁ n₂ m q : ℕ)
(Omega : Finset (Fin n₁ × Fin n₂))
(X : Matrix (Fin n₁) (Fin n₂) ℝ),
1 ≤ q →
(q : ℝ) ≥ β * Real.log (↑(max n₁ n₂)) →
rademacherExpectation
(fun eps =>
spectralNorm
(rademacherSampledMatrix Omega eps
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) X) ^ q) ≤
rademacherExpectation
(fun eps =>
schattenNorm (q : ℝ)
(rademacherSampledMatrix Omega eps
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) X) ^ q) := by
sorry