bernoulli_event_failure_lower_bound_from_cardinality_failures
ProvedRole. 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. If fixed-cardinality failure at level is bounded by every lower cardinality failure probability and the binomial lower tail has mass at least 1/2, then Bernoulli failure dominates half of fixed-cardinality failure.
Lecture-note formulation:
Decomposition status. A corresponding proof sketch reduces this node to smaller mathematical subclaims. The checked reduction uses 2 subclaims: Bernoulli event failure probability decomposes by cardinality; binomial lower tail weighted sum lower bound.
import Definitions.Def_matrix_completion_fixed_cardinality open MatrixCompletion
theorem bernoulli_event_failure_lower_bound_from_cardinality_failures
{n₁ n₂ : ℕ} (p : ℝ) (m : ℕ)
(Event : Finset (Fin n₁ × Fin n₂) → Prop) :
0 ≤ p → p ≤ 1 → m ≤ n₁ * n₂ →
(∀ k : ℕ, k ≤ m →
1 - fixedCardinalityEventProb m Event ≤
1 - fixedCardinalityEventProb k Event) →
(1 / 2 : ℝ) ≤ binomialLowerTailProb (n₁ * n₂) m p →
(1 / 2) * (1 - fixedCardinalityEventProb m Event) ≤
1 - bernoulliEventProb p Event := by
sorry