quadratic_neumann_section63_summary_scale_absorbed_under_general_sample_bound

Disproved

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

candes-rechtlemma-46matrix-completionscalar-absorptionsection-63source-faithful

This is the scalar absorption step at the end of the Candes-Recht Section 6.3 proof of Lemma 4.6.

With the same notation as the Section 6.3 summary estimate, let $\Phi$ denote the four-term quantity

\begin{aligned} \Phi={}&(\mu_0^2\mu_1)\sqrt{\frac{nr\,\beta\log n}{m}}\left(\frac{nr}{m}\right)^2 +\mu_0^2\left(\frac{nr}{m}\right)^2 \\ &+\sqrt{\beta\log n}\left(\frac{nr}{m}\right)^{3/2}\mu_0^2 r +\left(\frac{\mu_0\mu_1 nr\,\beta\log n}{m}\right)^{3/2}. \end{aligned}

The theorem says that for every fixed universal coefficient $C_{sec}>0$ , one can choose the universal sample constant in Theorem 1.3 large enough so that the full sample lower bound

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

forces

C_{sec}\Phi\le \frac18.

This node is pure scalar bookkeeping: no new probability estimate is hidden here.

Source location: Candes-Recht 2008, Section 6.3, PDF p. 34, final paragraph after the summary display. The paper writes the scaling as $m=\lambda\mu_0^{4/3}nr^{4/3}\beta\log n$ and concludes that the displayed expression is bounded by a universal constant times $\lambda^{-3/2}$ ; this node is the theorem-regime version obtained by choosing the universal sample constant large enough.

Preamble

import Definitions.Def_matrix_completion_neumann
open MatrixCompletion

Formal statement

theorem quadratic_neumann_section63_summary_scale_absorbed_under_general_sample_bound
    (Csec : ℝ) :
    0 < Csec →
    ∃ C : ℝ, 0 < C ∧
      ∀ C' : ℝ, C ≤ 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₂))) →
        (let N : ℝ := ↑(max n₁ n₂)
         let R : ℝ := (r : ℝ)
         let Mobs : ℝ := (m : ℝ)
         let logN : ℝ := Real.log N
         Csec *
           ((μ₀ ^ 2 * μ₁) *
              Real.sqrt ((N * R * (β * logN)) / Mobs) *
                ((N * R) / Mobs) ^ 2 +
            μ₀ ^ 2 * ((N * R) / Mobs) ^ 2 +
            Real.sqrt (β * logN) *
                Real.rpow ((N * R) / Mobs) ((3 : ℝ) / 2) *
                  (μ₀ ^ 2 * R) +
            Real.rpow
              ((μ₀ * μ₁ * N * R * (β * logN)) / Mobs)
              ((3 : ℝ) / 2))) ≤
          (1 : ℝ) / 8 := 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