linear_neumann_offdiag_base_frobenius_from_a1_and_kernel_row

Proved

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

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

This is the formal sign-weighted Frobenius transfer for the fixed base matrices in the scalar Bernstein proof of the first off-diagonal Neumann coefficient bound.

Assume the kernel-row estimate

\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}}

for every coordinate $w$ , and assume A1, namely

|E_{ij}|\le \mu_1\sqrt{\frac r{n_1n_2}}

for the sign matrix $E=\operatorname{sgn}(M)$ . Then the sign-weighted base matrix

B^{(w)}_{ij}=\mathbf 1_{(i,j)\ne w}\,E_{ij}\langle P_T(e_{ij}),e_w\rangle

satisfies

\|B^{(w)}\|_F\le C_{\mathrm{fro}}\,\mu_1\sqrt{\frac r{n_1n_2}}\sqrt{\frac{\mu_0 r}{n}}.

The content is mainly formal: multiply the kernel Frobenius row by the uniform A1 sign-entry bound.

Source: Candes-Recht, Section 6.2, Lemma 6.6, equations (6.15)--(6.17).

Preamble

import Definitions.Def_linear_neumann_offdiag_bernstein
open MatrixCompletion

Formal statement

theorem linear_neumann_offdiag_base_frobenius_from_a1_and_kernel_row
    (Cker : ℝ) :
    0 < Cker →
    ∃ Cfro : ℝ, 0 < Cfro ∧
      ∀ (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₂,
          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₂))))) →
        ∀ w : Fin n₁ × Fin n₂,
          frobeniusNorm
              (linearNeumannOffDiagonalCoefficientBaseMatrix S w) ≤
            Cfro * μ₁ *
              Real.sqrt ((r : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) *
                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