quadratic_neumann_section63_summary_bound_min_dim
ProvedSource: Candès–Recht 2008, Section 6.3, PDF pp. 30--34, the five-way split (6.20) and the summary display on PDF p. 34.
The theorem-regime §6.3 summary estimate for the second Neumann correction, stated
at the corrected rectangular five-term scale Φ + t₅ (the sound scale for the
first-index-distinct case; the N-only four-term Φ of
quadratic_neumann_section63_summary_bound_under_general_sample_bound is too tight
for thin matrices because the honest Lemma-6.8 mean cross-term 2(μ₀ r/min)² sends
a spectral contribution proportional to the (N/min)-aware fifth term
t₅ = √(βlogN)·μ₀²·((N R)/M)^{3/2}·√((N R)/min)).
Assembled from the five index-partition case bounds: the corrected
first-index-distinct case at Φ + t₅, and the other four cases (all-equal,
middle/last-index-distinct, all-distinct) at the four-term Φ, lifted to Φ + t₅
by monotonicity (t₅ ≥ 0).
import Definitions.Def_matrix_completion_neumann open MatrixCompletion
theorem quadratic_neumann_section63_summary_bound_min_dim :
∃ Csec csec : ℝ, 0 < Csec ∧ 0 < csec ∧
∀ C' : ℝ, Csec ≤ 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₂))) →
bernoulliEventProb ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
(fun Omega =>
NeumannCertificateTermSpectralBound Omega S
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) 2
(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) +
Real.sqrt (β * logN) * μ₀ ^ 2 *
Real.rpow ((N * R) / Mobs) ((3 : ℝ) / 2) *
Real.sqrt ((N * R) / (↑(min n₁ n₂)))))) ≥
1 - csec * Real.rpow (↑(max n₁ n₂)) (-β) := by sorry