quadratic_neumann_middle_index_distinct_centered_coefficients_from_kernel_square_base_bounds
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. Scalar Bernstein transfer for the conditional coefficient matrix in the decoupled centered term. The hypotheses isolate the exact signed scalar-fluctuation representation and the deterministic entry/Frobenius bounds for each kernel-square base matrix.
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 2 subclaims: quadratic Neumann middle index distinct centered coefficient pointwise tail from kernel square base bounds; quadratic Neumann middle index distinct centered coefficients uniform from pointwise tails.
import Definitions.Def_matrix_completion_neumann open MatrixCompletion
theorem quadratic_neumann_middle_index_distinct_centered_coefficients_from_kernel_square_base_bounds
(Centry Cfro : ℝ) :
0 < Centry → 0 < Cfro →
∃ 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₂))) →
(∀ (Omega2 : Finset (Fin n₁ × Fin n₂))
(w1 : Fin n₁ × Fin n₂),
quadraticMiddleIndexDistinctCenteredCoefficientMatrix Omega2 S
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) w1.1 w1.2 =
signMatrix S w1.1 w1.2 *
matrixEntrySum
(centeredSamplingFluctuation Omega2
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
(quadraticMiddleIndexDistinctKernelSquareBaseMatrix S w1))) →
(∀ w1 : Fin n₁ × Fin n₂,
entrySupNorm
(quadraticMiddleIndexDistinctKernelSquareBaseMatrix S w1) ≤
Centry * μ₀ ^ 2 *
(((r : ℝ) / (↑(max n₁ n₂))) ^ 2)) →
(∀ w1 : Fin n₁ × Fin n₂,
frobeniusNorm
(quadraticMiddleIndexDistinctKernelSquareBaseMatrix S w1) ≤
Cfro * Real.rpow μ₀ ((3 : ℝ) / 2) *
Real.rpow ((r : ℝ) / (↑(max n₁ n₂))) ((3 : ℝ) / 2)) →
bernoulliEventProb ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
(fun Omega2 =>
QuadraticMiddleIndexDistinctCenteredCoefficientBound Omega2 S
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
(Ccoef * Real.rpow lam (-1))) ≥
1 - ccoef * Real.rpow (↑(max n₁ n₂)) (-β) := by
sorry