linear_neumann_diagonal_centered_spectral_bound_from_centered_sampling_event

Proved

by Minghui · Jun 30, 2026 · Mathlib c5ea003 (Lean v4.30.0)

candes-rechtformal-bridgelinear-neumannmatrix-completionsection-6-2spectral-norm

Formal bridge from the centered diagonal representation in the proof of Lemma 4.5 to a spectral-norm threshold.

Primary reference: Candes--Recht, Exact Matrix Completion via Convex Optimization, PDF p. 27, Section 6.2, proof of Lemma 4.5, equation (6.9).

Mathematical statement and notation: let $M$ be an $n_1\times n_2$ real matrix with rank- $r$ SVD data $S$ . Let $p$ be the Bernoulli sampling rate and let $\Omega$ be a realized sample set. Equation (6.9) rewrites the centered diagonal part of the first Neumann term as

D_{\rm cent}(\Omega)=p^{-1}(1-2p)\,p^{-1}(P_\Omega-pI)B, \qquad B=\operatorname{linearNeumannDiagonalBaseMatrix}(S).

In Lean this representation is the hypothesis

\operatorname{linearNeumannDiagonalCenteredContribution}(\Omega,S,p) =(p^{-1}(1-2p))\,\operatorname{centeredSamplingFluctuation}(\Omega,p,B).

If the fixed-matrix event gives

\|\operatorname{centeredSamplingFluctuation}(\Omega,p,B)\|\le R

and the scalar prefactor satisfies $|p^{-1}(1-2p)|R\le T$ , then

\|D_{\rm cent}(\Omega)\|\le T.

Here $p,n_1,n_2,\Omega,S$ and the fixed matrix $B$ are explicit. The incoherence parameters $\mu_0,\mu_1$ , $Z(\Omega)$ , probability model bounds, and fixed-cardinality successProb do not appear in this deterministic norm bridge.

Formalization note: this is a formal bridge, not a theorem stated verbatim in the paper. It is the deterministic operator-norm bookkeeping child for the source-backed parent linear_neumann_diagonal_centered_general_sample_threshold_from_min_dim_base_bound (e8be9b95), whose source is Candes--Recht PDF p. 27, Section 6.2, Lemma 4.5, equation (6.9), together with the fixed-matrix sampling event imported by that parent.

Preamble

import Definitions.Def_matrix_completion_neumann
open MatrixCompletion

Formal statement

theorem linear_neumann_diagonal_centered_spectral_bound_from_centered_sampling_event
    {n₁ n₂ r : ℕ} {M : Matrix (Fin n₁) (Fin n₂) ℝ}
    (Omega : Finset (Fin n₁ × Fin n₂)) (S : SVD M r)
    (p R T : ℝ) :
    linearNeumannDiagonalCenteredContribution Omega S p =
      (p⁻¹ * (1 - 2 * p)) •
        centeredSamplingFluctuation Omega p (linearNeumannDiagonalBaseMatrix S) →
    CenteredSamplingSpectralBound Omega p (linearNeumannDiagonalBaseMatrix S) R →
    |p⁻¹ * (1 - 2 * p)| * R ≤ T →
    spectralNorm (linearNeumannDiagonalCenteredContribution Omega S p) ≤ T := by
  sorry

Source

Formal bridge for Candes--Recht, *Exact Matrix Completion via Convex Optimization*, PDF p. 27, Section 6.2, proof of Lemma 4.5, equation (6.9). Source-backed parent: `linear_neumann_diagonal_centered_general_sample_threshold_from_min_dim_base_bound`.

View graph