even2n_schatten_moment_bound
Provedcandes-rechtkhintchinelinear-algebramatrix-completionreferencerudelson
Even-order () Schatten moment bound for the Rademacher-sampled matrix. For the Rademacher-sampled matrix rademacherSampledMatrix Ω ε p X and with , the expected even Schatten moment is dominated by the sampled variance scale: , where rademacherSampledVarianceScale Ω p X . Proof (reduction): the Schatten even moment is routed through the Hermitian dilation trace (); the signed sum of per-coordinate rank-one dilations matches the symmetric Rademacher trace-moment engine, whose variance matrix is block-diagonal with (block-diagonal quadratic-form bound); the engine then yields , and the constant+window step (, ) collapses it to .
Preamble
import Definitions.Def_matrix_completion_gram_schatten open Matrix MatrixCompletion open scoped BigOperators
Formal statement
theorem even2n_schatten_moment_bound {n1 n2 : Nat} (n : Nat) (hn : 1 ≤ n) (Omega : Finset (Fin n1 × Fin n2)) (p : ℝ) (X : MatrixCompletion.RealMatrix n1 n2) (hd1 : 1 ≤ (n1 + n2)) (hlog : Real.log ((n1 + n2 : ℕ)) ≤ (2 * n : ℕ)) : rademacherExpectation (fun eps => schattenNorm (2 * n : ℝ) (rademacherSampledMatrix Omega eps p X) ^ (2 * n)) ≤ (Real.sqrt (2 * n : ℕ) * Real.exp 1 * rademacherSampledVarianceScale Omega p X) ^ (2 * n) := by sorrySource
Candes-Recht 2009 (arXiv:0805.4471) Sec 6.1, Thm 6.3. The EVEN-order (q=2n) Schatten moment of the Rademacher-sampled matrix, bounded directly by the (sampled variance scale) via the Hermitian-dilation trace-moment engine. The variance matrix V = ∑_c H_c² is block-diagonal blockdiag(diag(p⁻²rowEnergy), diag(p⁻²colEnergy)) with λmax(V) ≤ (rademacherSampledVarianceScale)², discharged through the block-diagonal quadratic-form bound.