Mission

Exact Matrix CompletionResearch Paper

Machine Learning Statistics·Captain: Shuze Chen

Every time a streaming service guesses what you would rate a film you have never seen, it is solving a matrix completion problem: fill in the missing entries of a vast user-by-item table from the few that are observed. The question became famous during the Netflix Prize (2006-2009), and it looks hopeless - infinitely many matrices fit the observed entries - until one assumes the structure that makes recommendation possible: the table is essentially low rank, because tastes are governed by a few latent factors. In their landmark 2009 paper 'Exact Matrix Completion via Convex Optimization' (Foundations of Computational Mathematics), Emmanuel Candes and Benjamin Recht proved that an n-by-n matrix of rank r can be recovered exactly, with high probability, from only about n^1.2 * r * log n randomly observed entries - not by the NP-hard route of minimizing rank, but by minimizing the nuclear norm, a convex surrogate (the sum of the singular values) solvable efficiently. The proof, in the lineage of Candes-Romberg-Tao compressed sensing, turns on two ideas: an incoherence condition ensuring the singular vectors are spread out rather than spiky, and a dual certificate witnessing optimality, whose existence rests on delicate random-matrix concentration. It transformed a practical engineering puzzle into rigorous theory and seeded a decade of work across machine learning, signal processing, computer vision, and sensor localization. This mission formalizes the Candes-Recht exact-recovery theorem in Lean, decomposed into its dual-certificate construction and the probabilistic concentration reductions at its core.

Goal · Candes-Recht Exact Matrix Completion

PROVED

theorem candes_recht_matrix_completion :
    ∃ C c : ℝ, 0 < C ∧ 0 < c ∧
      ∀ (β : ℝ), 2 < β →
      ∀ (n₁ n₂ r m : ℕ) (M : Matrix (Fin n₁) (Fin n₂) ℝ)
        (μ₀ μ₁ : ℝ) (S : SVD M r),
        0 < n₁ → 0 < n₂ → 0 < r → m ≤ n₁ * n₂ →
        1 ≤ μ₀ → 1 ≤ μ₁ →
        A0 S μ₀ → A1 S μ₁ →
        (m : ℝ) ≥
          C * max (max (μ₁ ^ 2) (Real.sqrt μ₀ * μ₁))
                  (μ₀ * Real.rpow (↑(max n₁ n₂)) ((1 : ℝ) / 4))
            * (↑(max n₁ n₂)) * (r : ℝ) * (β * Real.log (↑(max n₁ n₂))) →
        successProb m M ≥ 1 - c * Real.rpow (↑(max n₁ n₂)) (-β) := by
  sorry

Role. It is the root theorem of the mission: the fixed-cardinality exact matrix completion guarantee corresponding to the general coherence branch of Theorem 1.3.

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 $M\in\mathbb R^{n_1\times n_2}$ has rank $r$ , $m$ entries are observed, and $n=\max(n_1,n_2)$ . Recovery means nuclear-norm minimization: minimize $\|X\|_*$ among matrices $X$ agreeing with $M$ on the observed entries. Probability notation. $\operatorname{successProb}(m,M)$ is the fixed-cardinality success probability: $\Omega$ is chosen uniformly among all subsets of $n_1n_2$ entries with $|\Omega|=m$ , and the event is that the convex program uniquely returns $M$ . In Bernoulli nodes, $\mathbb P_p(E)$ or $\operatorname{bernoulliEventProb}(p,E)$ means each entry is sampled independently with probability $p$ , usually $p=m/(n_1n_2)$ . Coherence notation. The object $S$ records SVD/singular-vector data for $M$ . The hypotheses $A0(S,\mu_0)$ and $A1(S,\mu_1)$ are the Candes-Recht incoherence assumptions: $\mu_0$ measures how spread out the singular vector spaces are, and $\mu_1$ measures the largest entry of the sign matrix $UV^\top$ . The parameter $\beta>2$ controls polynomial failure probabilities such as $n^{-\beta}$ .

Claim. Candes-Recht 2008, Theorem 1.3, general coherence-based sample complexity branch. There are universal constants $C, c > 0$ such that any rank- $r$ matrix obeying A0/A1 is recovered by nuclear-norm minimization from a uniformly random set of $m$ observed entries with probability at least $1 - c n^{-\beta}$ , provided $m$ satisfies the displayed general sample lower bound.

Lecture-note formulation:

\begin{gathered} n=\max(n_1,n_2),\qquad m \ge C\,\max\!\left\{\mu_1^2,\sqrt{\mu_0}\mu_1,\mu_0 n^{1/4}\right\} n r\,\beta\log n\\ \Longrightarrow\quad \mathbb P_{\Omega:\ |\Omega|=m} \left( \begin{array}{c} \text{the nuclear-norm minimization problem}\\ \min\|X\|_*\ \text{ subject to }X_{ij}=M_{ij}\text{ for }(i,j)\in\Omega\\ \text{has the unique solution }X=M \end{array} \right) \ge 1-c\,n^{-\beta}. \end{gathered}

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 2 subclaims: Bernoulli exact completion general sample complexity; fixed cardinality completion probability from Bernoulli model.

Frontier · Open leaf nodes

No open leaves. Every sub-goal is proved or awaiting decomposition.

Recent activity

ACCEPTEDShuze ChenJun 21, 2026
ACCEPTEDShuze ChenJun 13, 2026