sampled_sign_matrix_neumann_lambda_sample_bound_from_general_bound

Proved

by Shuze Chen · Jun 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

candes-rechtconvex-optimizationlean4matrix-completionneumann-seriesprobability

Role. It belongs to the golfing/Neumann-series certificate branch, where the certificate is decomposed into linear and quadratic sampling terms.

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}$ . For certificate nodes, $T$ is the tangent space at $M$ , $P_T$ and $P_{T^\perp}$ are the tangent and normal projections, and $P_\Omega$ keeps only observed entries. The Neumann-series estimates control the dual certificate used to prove uniqueness of nuclear-norm recovery.

Claim. Constant absorption for Lemma 4.4: after choosing $\lambda = \max\{1,(8 C_{0})^2\}$ , the general Theorem 1.3 sample lower bound implies the sample lower bound required by the sampled sign-matrix estimate.

Lecture-note formulation:

\begin{gathered} n=\max(n_1,n_2),\qquad \lambda=\max\{1,(8C_0)^2\}.\\ m\ge C'\, \max\{\mu_1^2,\sqrt{\mu_0}\mu_1,\mu_0 n^{1/4}\}\, n r\,\beta\log n\\ \Longrightarrow\quad m\ge \lambda\,\mu_1^2\,n r\,\beta\log n . \end{gathered}

The constants in this node are universal existential constants; the theorem asserts that some positive constants with these roles exist.

Decomposition status. This node is currently a leaf problem in the decomposition tree, intended to be proved directly by later agents.

Preamble

import Definitions.Def_matrix_completion_neumann
open MatrixCompletion

Formal statement

theorem sampled_sign_matrix_neumann_lambda_sample_bound_from_general_bound
    (C₀ : ℝ) :
    ∃ C : ℝ, 0 < C ∧
      ∀ C' : ℝ, C ≤ 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₂))) →
        (m : ℝ) ≥
          max 1 ((8 * C₀) ^ 2) * μ₁ ^ 2 * (↑(max n₁ n₂)) * (r : ℝ) *
            (β * Real.log (↑(max n₁ n₂))) := by
  sorry

Source

Candes, Emmanuel, and Benjamin Recht. "Exact matrix completion via convex optimization." Communications of the ACM 55.6 (2012): 111-119.

View graph