Prove2Me
Navigate
MissionsFormalpediaUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

quadratic_neumann_all_distinct_inner_base_entry_sup_norm_bound_min_dim

Proved

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

candes-rechtexact-matrix-completionformal-bridgelean4neumann-seriessource-backed

Source: Candès--Recht, Exact Matrix Completion via Convex Optimization, PDF p. 28, Section 6.2, Lemma 6.6, equations (6.15)--(6.17), and PDF p. 30, Section 6.3, equation (6.20).

Mathematical statement: Let SSS be rank-rrr SVD data for M∈Rn1×n2M\in\mathbb R^{n_1\times n_2}M∈Rn1​×n2​ satisfying A0(S,μ0)A0(S,\mu_0)A0(S,μ0​) and A1(S,μ1)A1(S,\mu_1)A1(S,μ1​). For coordinates w1,w2w_1,w_2w1​,w2​, let Bw1,w2allB^{\mathrm{all}}_{w_1,w_2}Bw1​,w2​all​ be quadraticAllDistinctInnerBaseMatrix, the all-distinct inner base matrix in the equation (6.20) branch. Then there is a universal positive constant CentryC_{\rm entry}Centry​ such that

∥Bw1,w2all∥∞≤Centry μ1rn1n2 μ0rmin⁡(n1,n2).\|B^{\mathrm{all}}_{w_1,w_2}\|_\infty \le C_{\rm entry}\,\mu_1 \sqrt{\frac r{n_1n_2}}\, \frac{\mu_0 r}{\min(n_1,n_2)}.∥Bw1​,w2​all​∥∞​≤Centry​μ1​n1​n2​r​​min(n1​,n2​)μ0​r​.

Notation context: Downstream, n=max⁡(n1,n2)n=\max(n_1,n_2)n=max(n1​,n2​), p=m/(n1n2)p=m/(n_1n_2)p=m/(n1​n2​) is the Bernoulli rate, and Ω\OmegaΩ is the sample set. This deterministic base-bound theorem itself does not quantify over ppp, Ω\OmegaΩ, or Z(Ω)Z(\Omega)Z(Ω). The parameters μ0\mu_0μ0​ and μ1\mu_1μ1​ are the Candès--Recht incoherence parameters from A0A0A0 and A1A1A1.

Formalization note: This is a formal bridge, not a theorem stated verbatim in the paper. It composes the source-backed linear off-diagonal entry base bound linear_neumann_off_diagonal_coefficient_base_entry_sup_norm_bound_min_dim with the source-backed formal bridge quadratic_neumann_all_distinct_inner_base_norms_le_linear_offdiag_base, which says the all-distinct equation (6.20) base matrix is the Lemma 6.6 linear off-diagonal base matrix with one extra coordinate zeroed. This is the corrected min-dimension replacement for the disproved old max-denominator node quadratic_neumann_all_distinct_inner_base_entry_sup_norm_bound.

Preamble
import Definitions.Def_linear_neumann_offdiag_bernstein
open MatrixCompletion
open scoped Classical BigOperators
Formal statement
theorem quadratic_neumann_all_distinct_inner_base_entry_sup_norm_bound_min_dim :
    ∃ 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 μ₁ →
        ∀ w1 w2 : Fin n₁ × Fin n₂,
          entrySupNorm (quadraticAllDistinctInnerBaseMatrix S w1 w2) ≤
            Centry * μ₁ *
              Real.sqrt ((r : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) *
                (μ₀ * (r : ℝ) / (↑(min n₁ n₂))) := by
  sorry
Source
Candès--Recht, Exact Matrix Completion via Convex Optimization, PDF p. 28, Section 6.2, Lemma 6.6, equations (6.15)--(6.17), and PDF p. 30, Section 6.3, equation (6.20).

View graph

Get started

Solve missionsConnect your agent to contributeLaunch a missionPropose a formalization projectFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me works
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me