off_diagonal_tangent_kernel_row_frobenius_bound_from_a0

Disproved

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

candes-rechtexact-matrix-completionfrobenius-normincoherencelemma-6-6linear-neumannoff-diagonal

This theorem isolates the geometric tangent-kernel estimate used in the off-diagonal part of the first Neumann correction.

Let $M$ be an $n_1\times n_2$ rank- $r$ matrix with SVD data $S$ , and put $n=\max(n_1,n_2)$ . Under the A0 incoherence hypothesis with parameter $\mu_0$ , there is a universal constant $C_{\mathrm{ker}}>0$ such that for every output coordinate $w=(a,b)$ ,

\left\|\bigl(\mathbf 1_{(i,j)\ne w}\,\langle P_T(e_{ij}),e_w\rangle\bigr)_{i,j}\right\|_F \le C_{\mathrm{ker}}\sqrt{\frac{\mu_0 r}{n}}.

Here $P_T$ is the tangent-space projection at $M$ , and the left-hand side is the Frobenius norm of one off-diagonal row of the tangent-coordinate kernel.

Source: Candes-Recht, Section 6.2, Lemma 6.6, equations (6.15)--(6.17), using the tangent-coordinate bounds (6.2)--(6.3) on PDF pp. 24--27.

Preamble

import Definitions.Def_linear_neumann_offdiag_bernstein
open MatrixCompletion

Formal statement

theorem off_diagonal_tangent_kernel_row_frobenius_bound_from_a0 :
    ∃ Cker : ℝ, 0 < Cker ∧
      ∀ (n₁ n₂ r : ℕ) (M : Matrix (Fin n₁) (Fin n₂) ℝ)
        (μ₀ : ℝ) (S : SVD M r),
        0 < n₁ → 0 < n₂ → 0 < r →
        1 ≤ μ₀ → A0 S μ₀ →
        ∀ w : Fin n₁ × Fin n₂,
          frobeniusNorm
              (fun i j =>
                if (i, j) = w then 0
                else tangentCoordinateKernel S i j w.1 w.2) ≤
            Cker * Real.sqrt
              (μ₀ * ((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