quadratic_neumann_middle_index_distinct_mean_coefficient_bound_small_with_lambda
ProvedRole. 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 has rank , entries are observed, and . Recovery means nuclear-norm minimization: minimize among matrices agreeing with on the observed entries. Probability notation. is the fixed-cardinality success probability: is chosen uniformly among all subsets of entries with , and the event is that the convex program uniquely returns . In Bernoulli nodes, or means each entry is sampled independently with probability , usually . Coherence notation. The object records SVD/singular-vector data for . The hypotheses and are the Candes-Recht incoherence assumptions: measures how spread out the singular vector spaces are, and measures the largest entry of the sign matrix . The parameter controls polynomial failure probabilities such as . For certificate nodes, is the tangent space at , and are the tangent and normal projections, and keeps only observed entries. The Neumann-series estimates control the dual certificate used to prove uniqueness of nuclear-norm recovery.
Claim. Bernstein control of the random coefficients appearing in the mean part of the quadratic term. This is the estimate following the decoupled display for the third term in Section 6.3.
Lecture-note formulation:
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 4 subclaims: quadratic Neumann middle index distinct mean coefficient as centered scalar fluctuation; quadratic Neumann middle index distinct kernel square base entry sup norm bound; quadratic Neumann middle index distinct kernel square base Frobenius norm bound; quadratic Neumann middle index distinct mean coefficients from kernel square base bounds.
import Definitions.Def_matrix_completion_neumann open MatrixCompletion
theorem quadratic_neumann_middle_index_distinct_mean_coefficient_bound_small_with_lambda :
∃ Ccoef ccoef : ℝ, 0 < Ccoef ∧ 0 < ccoef ∧
∀ (β 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₂))) →
bernoulliEventProb ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
(fun Omega =>
QuadraticMiddleIndexDistinctMeanCoefficientBound Omega S
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
(Ccoef *
Real.sqrt (β * Real.log (↑(max n₁ n₂))) *
Real.rpow
((μ₀ * (↑(max n₁ n₂)) * (r : ℝ)) / (m : ℝ))
((3 : ℝ) / 2))) ≥
1 - ccoef * Real.rpow (↑(max n₁ n₂)) (-β) := by
sorry