linear_neumann_off_diagonal_pair_decoupling_tail_bound
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. Threshold-form two-variable decoupling inequality for the off-diagonal first Neumann chaos. A tail estimate for the two-copy model transfers to the diagonal coupling with universal losses.
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_neumann open MatrixCompletion
theorem linear_neumann_off_diagonal_pair_decoupling_tail_bound :
∃ K L : ℝ, 0 < K ∧ 0 < L ∧
∀ {n₁ n₂ r : ℕ} {M : Matrix (Fin n₁) (Fin n₂) ℝ}
(S : SVD M r)
(p Cdec cdec failureScale thresholdScale : ℝ),
0 ≤ p → p ≤ 1 → 0 < Cdec → 0 < cdec →
bernoulliPairEventProb p
(fun Omega1 Omega2 =>
spectralNorm
(linearNeumannOffDiagonalDecoupledContribution
Omega1 Omega2 S p) ≤
Cdec * thresholdScale) ≥
1 - cdec * failureScale →
bernoulliEventProb p
(fun Omega =>
spectralNorm
(linearNeumannOffDiagonalDecoupledContribution
Omega Omega S p) ≤
(K * Cdec) * thresholdScale) ≥
1 - (L * cdec) * failureScale := by
sorry