scalar_centered_sampling_bernstein_tail_from_entry_frobenius_scales

Proved

by Shuze Chen · Jun 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

bernsteincandes-rechtcentered-samplingconvex-optimizationlean4matrix-completionprobabilityscale-absorptiontail-bounds

Role. It is a centered-sampling fluctuation estimate, one of the reusable concentration interfaces used repeatedly by the Neumann-term bounds.

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. Raw scalar Bernstein inequality for the entry-sum of a centered sampling fluctuation. The bound is stated in terms of exposed entry and Frobenius scales, before any Candes-Recht sample-size arithmetic is absorbed.

Lecture-note formulation:

\|a\|_\infty\le a_\infty,\qquad \|a\|_2\le a_2 \Longrightarrow \mathbb P_p\!\left(\left|\sum(\delta_{ij}-p)a_{ij}\right| \le C\bigl(a_2\sqrt{p\beta\log n}+a_\infty\beta\log n\bigr)\right) \ge 1-cn^{-\beta}.

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 scalar_centered_sampling_bernstein_tail_from_entry_frobenius_scales :
    ∃ Cbern cbern : ℝ, 0 < Cbern ∧ 0 < cbern ∧
      ∀ (β : ℝ), 2 < β →
      ∀ (n₁ n₂ m : ℕ), 0 < n₁ → 0 < n₂ → m ≤ n₁ * n₂ →
      ∀ (Coeff : Finset (Fin n₁ × Fin n₂) → ℝ)
        (B : Matrix (Fin n₁) (Fin n₂) ℝ)
        (entryScale frobScale : ℝ),
        (∀ Omega : Finset (Fin n₁ × Fin n₂),
          Coeff Omega =
            matrixEntrySum
              (centeredSamplingFluctuation Omega
                ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) B)) →
        entrySupNorm B ≤ entryScale →
        frobeniusNorm B ≤ frobScale →
        bernoulliEventProb ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
            (fun Omega =>
              |Coeff Omega| ≤
                Cbern *
                  (Real.sqrt
                      ((β * Real.log (↑(max n₁ n₂))) /
                        ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))) *
                    frobScale +
                    ((β * Real.log (↑(max n₁ n₂))) /
                      ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))) *
                    entryScale)) ≥
          1 - cbern * Real.rpow (↑(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