Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

quadratic_neumann_all_distinct_outer_sampling_conditional_from_entry_bound

Disproved

by Shuze Chen · Jun 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

candes-rechtconvex-optimizationlean4matrix-completionneumann-seriesprobabilityquadratic-terms

Role. It belongs to the golfing/Neumann-series certificate branch, where the certificate is decomposed into linear and quadratic sampling terms.

Problem and notation. Exact matrix completion asks when an unknown low-rank real matrix can be recovered from a random subset of its entries. Here M∈Rn1×n2M\in\mathbb R^{n_1\times n_2}M∈Rn1​×n2​ has rank rrr, mmm entries are observed, and n=max⁡(n1,n2)n=\max(n_1,n_2)n=max(n1​,n2​). Recovery means nuclear-norm minimization: minimize ∥X∥∗\|X\|_*∥X∥∗​ among matrices XXX agreeing with MMM on the observed entries. Probability notation. successProb⁡(m,M)\operatorname{successProb}(m,M)successProb(m,M) is the fixed-cardinality success probability: Ω\OmegaΩ is chosen uniformly among all subsets of n1n2n_1n_2n1​n2​ entries with ∣Ω∣=m|\Omega|=m∣Ω∣=m, and the event is that the convex program uniquely returns MMM. In Bernoulli nodes, Pp(E)\mathbb P_p(E)Pp​(E) or bernoulliEventProb⁡(p,E)\operatorname{bernoulliEventProb}(p,E)bernoulliEventProb(p,E) means each entry is sampled independently with probability ppp, usually p=m/(n1n2)p=m/(n_1n_2)p=m/(n1​n2​). Coherence notation. The object SSS records SVD/singular-vector data for MMM. The hypotheses A0(S,μ0)A0(S,\mu_0)A0(S,μ0​) and A1(S,μ1)A1(S,\mu_1)A1(S,μ1​) are the Candes-Recht incoherence assumptions: μ0\mu_0μ0​ measures how spread out the singular vector spaces are, and μ1\mu_1μ1​ measures the largest entry of the sign matrix UV⊤UV^\topUV⊤. The parameter β>2\beta>2β>2 controls polynomial failure probabilities such as n−βn^{-\beta}n−β. For certificate nodes, TTT is the tangent space at MMM, PTP_TPT​ and PT⊥P_{T^\perp}PT⊥​ are the tangent and normal projections, and PΩP_\OmegaPΩ​ keeps only observed entries. The Neumann-series estimates control the dual certificate used to prove uniqueness of nuclear-norm recovery.

Claim. Conditional outer sampling step for the all-distinct quadratic term: after fixing Ω2,Ω3Ω_{2}, Ω_{3}Ω2​,Ω3​ and bounding the entry sup norm of the outer coefficient matrix, Theorem 6.3 over the independent Ω₁ sample gives the decoupled spectral estimate.

Lecture-note formulation:

conditional on the inner coefficient event for Gw,Pp ⁣(∥Q1,2,3 distinct∥≤C λ−3/2∣Gw controlled)≥1−cn−β.\begin{gathered} \text{conditional on the inner coefficient event for }G_w,\\ \mathbb P_p\!\left(\|Q_{1,2,3\ \mathrm{distinct}}\|\le C\,\lambda^{-3/2}\mid G_w\text{ controlled}\right) \ge 1-c n^{-\beta}. \end{gathered}conditional on the inner coefficient event for Gw​,Pp​(∥Q1,2,3 distinct​∥≤Cλ−3/2∣Gw​ controlled)≥1−cn−β.​

The constants in this node are universal existential constants; the theorem asserts that some positive constants with these roles exist.

Decomposition status. A corresponding proof sketch reduces this node to smaller mathematical subclaims. The checked reduction uses 3 subclaims: quadratic Neumann all distinct outer decoupled threshold from centered sampling bound; Bernoulli event probability mono; sample ratio between zero and one.

Preamble
import Definitions.Def_matrix_completion_neumann
open MatrixCompletion
Formal statement
theorem quadratic_neumann_all_distinct_outer_sampling_conditional_from_entry_bound
    (Cfixed : ℝ) :
    0 < Cfixed →
    ∃ Ccond ccond : ℝ, 0 < Ccond ∧ 0 < ccond ∧
      ∀ (β lam : ℝ), 2 < β → 1 ≤ lam →
      ∀ (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 : ℝ) ≥
          lam * Real.rpow μ₀ ((4 : ℝ) / 3) *
            (↑(max n₁ n₂)) * Real.rpow (r : ℝ) ((4 : ℝ) / 3) *
              (β * Real.log (↑(max n₁ n₂))) →
        (∀ X : Matrix (Fin n₁) (Fin n₂) ℝ,
          bernoulliEventProb ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
              (fun Omega1 =>
                CenteredSamplingSpectralBound Omega1
                  ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) X
                  (Cfixed * Real.sqrt
                    ((β * (↑(max n₁ n₂)) *
                        Real.log (↑(max n₁ n₂))) /
                      ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))) *
                    entrySupNorm X)) ≥
            1 - (1 : ℝ) * Real.rpow (↑(max n₁ n₂)) (-β)) →
        ∀ Cmid : ℝ, 0 < Cmid →
        ∀ Omega2 Omega3 : Finset (Fin n₁ × Fin n₂),
        (∀ Omega1 : Finset (Fin n₁ × Fin n₂),
          quadraticNeumannAllDistinctDecoupledContribution Omega1 Omega2 Omega3 S
              ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) =
            centeredSamplingFluctuation Omega1
              ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
              (quadraticAllDistinctOuterCoefficientMatrix Omega2 Omega3 S
                ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))))) →
        entrySupNorm
            (quadraticAllDistinctOuterCoefficientMatrix Omega2 Omega3 S
              ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))) ≤
          Cmid * Real.rpow lam (-1) →
        bernoulliEventProb ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
            (fun Omega1 =>
              spectralNorm
                (quadraticNeumannAllDistinctDecoupledContribution
                  Omega1 Omega2 Omega3 S
                  ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))) ≤
                (Ccond * Cmid) * Real.rpow lam (-((3 : ℝ) / 2))) ≥
          1 - ccond * Real.rpow (↑(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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

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 worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me