rademacher_sampled_matrix_moment_from_row_column_energy
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 . For sampled row/column nodes, counts observed entries in row , counts observed entries in column , and the corresponding energies sum over sampled entries. These estimates feed the noncommutative Khintchine and spectral-norm concentration bounds.
Claim. Noncommutative Khintchine step from Section 6.1: conditional on the sampled row/column energies, the Rademacher-signed sampled matrix has the expected spectral moment at scale .
Lecture-note formulation:
The constants in this node are universal existential constants; the theorem asserts that some positive constants with these roles exist.
Decomposition status. A corresponding proof sketch reduces this node to smaller mathematical subclaims. The checked reduction uses 3 subclaims: Rademacher sampled matrix conditional Khintchine bound; Bernoulli Rademacher moment bound by conditional Khintchine scales; conditional Khintchine scale moment from row column energy moment.
import Definitions.Def_matrix_completion_rademacher open MatrixCompletion
theorem rademacher_sampled_matrix_moment_from_row_column_energy
(Cenergy : ℝ) :
0 < Cenergy →
∃ Crad : ℝ, 0 < Crad ∧
∀ (β : ℝ), 2 < β →
∀ (n₁ n₂ m q : ℕ) (X : Matrix (Fin n₁) (Fin n₂) ℝ),
0 < n₁ → 0 < n₂ → m ≤ n₁ * n₂ →
(m : ℝ) ≥ β * (↑(max n₁ n₂)) *
Real.log (↑(max n₁ n₂)) →
1 ≤ q →
(q : ℝ) ≥ β * Real.log (↑(max n₁ n₂)) →
(q : ℝ) ≤ 2 * (β * Real.log (↑(max n₁ n₂))) →
(q : ℝ) ≤
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) *
(↑(max n₁ n₂)) →
bernoulliExpectation ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
(fun Omega =>
(max (sampledRowEnergyMax Omega X)
(sampledColumnEnergyMax Omega X)) ^ q) ≤
(Cenergy * ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) *
(↑(max n₁ n₂)) * entrySupNorm X ^ 2) ^ q →
bernoulliExpectation ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
(fun Omega =>
rademacherExpectation
(fun eps =>
spectralNorm
(rademacherSampledMatrix Omega eps
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) X) ^ q)) ≤
(Crad * Real.sqrt
(((q : ℝ) * (↑(max n₁ n₂))) /
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))) *
entrySupNorm X) ^ q := by
sorry