normal_certificate_inner_lt_nuclear_norm_of_nonzero_normal_component
ProvedRole. It is part of the deterministic convex-optimization argument linking injectivity and dual certificates to exact recovery.
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. Nuclear/spectral duality in strict form: a normal certificate with spectral norm < 1 pairs strictly below the nuclear norm of every nonzero normal component.
Lecture-note formulation:
Decomposition status. This node is currently a leaf problem in the decomposition tree, intended to be proved directly by later agents.
import Definitions.Def_matrix_completion_tangent open MatrixCompletion
theorem normal_certificate_inner_lt_nuclear_norm_of_nonzero_normal_component
{n₁ n₂ r : ℕ} {M : Matrix (Fin n₁) (Fin n₂) ℝ}
(S : SVD M r) (Y H : Matrix (Fin n₁) (Fin n₂) ℝ) :
spectralNorm (normalProjection S Y) < 1 →
normalProjection S H ≠ 0 →
matrixInner (normalProjection S Y) (normalProjection S H) <
nuclearNorm (normalProjection S H) := by
sorry