linear_neumann_diagonal_centered_general_sample_scalar_threshold_from_min_dim_base_bound

Open

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

candes-rechtconstant-absorptionlinear-neumannmatrix-completionmin-dimensionscalar-thresholdsection-6-2source-backed

Scalar constant-absorption child for the centered diagonal first-Neumann term under the general Candes--Recht sample bound.

Primary reference: Candes--Recht, Exact Matrix Completion via Convex Optimization, PDF p. 6, Section 1.2, Theorem 1.3, equation (1.9), and PDF p. 27, Section 6.2, proof of Lemma 4.5, equation (6.9). The fixed-matrix concentration scale is from PDF p. 25, Section 6.1, Theorem 6.3, equation (6.7).

Mathematical statement and notation: set

n=\max(n_1,n_2),\qquad p={m\over n_1n_2},

and let $B=\operatorname{linearNeumannDiagonalBaseMatrix}(S)$ . In equation (6.9), the centered diagonal term carries the scalar prefactor $p^{-1}(1-2p)$ multiplying a fixed-matrix centered sampling fluctuation. The fixed-matrix event gives the scale

R=C_{\rm fixed}\sqrt{\frac{\beta n\log n}{p}}\,\|B\|_\infty.

Assume the corrected min-dimension base estimate

\|B\|_\infty\le C_{\rm base}\mu_1\sqrt{\frac r{n_1n_2}} {\mu_0r\over\min(n_1,n_2)}

and the root general sample lower bound

m\ge C'\max\{\mu_1^2,\sqrt{\mu_0}\mu_1,\mu_0n^{1/4}\}\,nr\,\beta\log n.

The theorem asserts that a large enough universal threshold $C_{\rm threshold}$ , depending only on $C_{\rm fixed}$ and $C_{\rm base}$ , forces the scalar inequality

|p^{-1}(1-2p)|R\le {1\over32}.

Here $p,n,\mu_0,\mu_1,r,m,S$ are active. The sample set $\Omega$ , $Z(\Omega)$ , Bernoulli probability bounds, and fixed-cardinality successProb do not appear in this deterministic scalar theorem.

Formalization note: this is a source-derived scalar absorption theorem, not a theorem appearing verbatim in the paper and not a purely formal Lean bridge. It is the nontrivial arithmetic child of the source-backed parent linear_neumann_diagonal_centered_general_sample_threshold_from_min_dim_base_bound (e8be9b95). It keeps the fixed-matrix scale and the min-dimension base bound explicit so the route does not repeat the deprecated off-diagonal range-absorption or response-threshold mistakes.

Preamble

import Definitions.Def_matrix_completion_neumann
open MatrixCompletion

Formal statement

theorem linear_neumann_diagonal_centered_general_sample_scalar_threshold_from_min_dim_base_bound
    (Cfixed Cbase : ℝ) :
    0 < Cfixed → 0 < Cbase →
    ∃ Cthreshold : ℝ, 0 < Cthreshold ∧
      ∀ C' : ℝ, Cthreshold ≤ C' →
      ∀ (β : ℝ), 2 < β →
      ∀ (n₁ n₂ r m : ℕ) (M : Matrix (Fin n₁) (Fin n₂) ℝ)
        (μ₀ μ₁ : ℝ) (S : SVD M r),
        0 < n₁ → 0 < n₂ → 0 < r → m ≤ n₁ * n₂ →
        1 ≤ μ₀ → 1 ≤ μ₁ →
        A0 S μ₀ → A1 S μ₁ →
        (m : ℝ) ≥
          C' * max (max (μ₁ ^ 2) (Real.sqrt μ₀ * μ₁))
                  (μ₀ * Real.rpow (↑(max n₁ n₂)) ((1 : ℝ) / 4))
            * (↑(max n₁ n₂)) * (r : ℝ) *
              (β * Real.log (↑(max n₁ n₂))) →
        entrySupNorm (linearNeumannDiagonalBaseMatrix S) ≤
          Cbase * μ₁ *
            Real.sqrt ((r : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) *
              (μ₀ * (r : ℝ) / (↑(min n₁ n₂))) →
        |(((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))⁻¹ *
            (1 - 2 * ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))))| *
          (Cfixed * Real.sqrt
            ((β * (↑(max n₁ n₂)) * Real.log (↑(max n₁ n₂))) /
              ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))) *
            entrySupNorm (linearNeumannDiagonalBaseMatrix S)) ≤
          (1 : ℝ) / 32 := by
  sorry

Source

Candes--Recht, *Exact Matrix Completion via Convex Optimization*, PDF p. 6, Section 1.2, Theorem 1.3, equation (1.9); PDF p. 25, Section 6.1, Theorem 6.3, equation (6.7); PDF p. 27, Section 6.2, proof of Lemma 4.5, equation (6.9).

View graph