linear_neumann_off_diagonal_coefficient_base_entry_sup_norm_bound

Disproved

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

bernsteincandes-rechtdual-certificatelemma-66matrix-completionneumann-series

This node supplies the pointwise kernel bound needed for the scalar Bernstein proof of Candes--Recht Lemma 6.6.

Fix a coordinate $w=(a,b)$ and form the base matrix

B^{(w)}_{a'b'}=\mathbf 1_{(a',b')\ne (a,b)}E_{a'b'} \,\langle P_T(e_{a'}e_{b'}^{\mathsf T}),e_a e_b^{\mathsf T}\rangle,

where $E=UV^{\mathsf T}$ is the sign matrix and $P_T$ is the tangent-space projector at the rank- $r$ matrix. Under the incoherence hypotheses $A0(S,\mu_0)$ and $A1(S,\mu_1)$ , every entry of $B^{(w)}$ is bounded by a universal constant times

\mu_1\sqrt{\frac r{n_1n_2}}\,\frac{\mu_0 r}{n},\qquad n=\max(n_1,n_2).

This is the range bound for the summands in the Bernstein estimate of equation (6.15). Source location: Candes--Recht, Section 6.2, Lemma 6.6, especially equations (6.2), (6.3), and (6.17).

Preamble

import Definitions.Def_linear_neumann_offdiag_bernstein
open MatrixCompletion

Formal statement

theorem linear_neumann_off_diagonal_coefficient_base_entry_sup_norm_bound :
    ∃ Centry : ℝ, 0 < Centry ∧
      ∀ (n₁ n₂ r : ℕ) (M : Matrix (Fin n₁) (Fin n₂) ℝ)
        (μ₀ μ₁ : ℝ) (S : SVD M r),
        0 < n₁ → 0 < n₂ → 0 < r →
        1 ≤ μ₀ → 1 ≤ μ₁ →
        A0 S μ₀ → A1 S μ₁ →
        ∀ w : Fin n₁ × Fin n₂,
          entrySupNorm
              (linearNeumannOffDiagonalCoefficientBaseMatrix S w) ≤
            Centry * μ₁ *
              Real.sqrt ((r : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) *
                (μ₀ * (r : ℝ) / (↑(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