bernoulli_uniform_bound_over_matrix_indices_from_pointwise_tails
DisprovedRole. It is a reusable node in the Candes-Recht decomposition, phrased as a standalone theorem so that downstream sketches can import it directly.
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 .
Claim. Finite union bound over matrix coordinates. If every coordinate event fails with probability at most , then the event that all coordinates satisfy the same bound holds with the same polynomial tail after enlarging the absolute constant.
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. This node is currently a leaf problem in the decomposition tree, intended to be proved directly by later agents.
import Definitions.Def_matrix_completion_bernoulli open MatrixCompletion
theorem bernoulli_uniform_bound_over_matrix_indices_from_pointwise_tails
(Cpoint cpoint : ℝ) :
0 < Cpoint → 0 < cpoint →
∃ Cuniform cuniform : ℝ, 0 < Cuniform ∧ 0 < cuniform ∧
∀ (β p scale : ℝ), 2 < β →
∀ (n₁ n₂ : ℕ),
0 < n₁ → 0 < n₂ →
∀ Coeff : (Fin n₁ × Fin n₂) →
Finset (Fin n₁ × Fin n₂) → ℝ,
(∀ w : Fin n₁ × Fin n₂,
bernoulliEventProb p
(fun Omega => |Coeff w Omega| ≤ Cpoint * scale) ≥
1 - cpoint * Real.rpow (↑(max n₁ n₂)) (-β)) →
bernoulliEventProb p
(fun Omega =>
∀ w : Fin n₁ × Fin n₂,
|Coeff w Omega| ≤ Cuniform * scale) ≥
1 - cuniform * Real.rpow (↑(max n₁ n₂)) (-β) := by
sorry