fixed_cardinality_event_failure_le_twice_bernoulli_event_failure
ProvedRole. It belongs to the sampling-model transfer layer, relating fixed-cardinality probabilities to Bernoulli probabilities.
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 . This node is in the sampling-model transfer layer: it compares the uniform exactly- observation model with the independent Bernoulli model.
Claim. Section 4.1 comparison for arbitrary monotone success events: fixed-size failure is at most twice Bernoulli failure at the same expected sample size.
Lecture-note formulation:
Decomposition status. A corresponding proof sketch reduces this node to smaller mathematical subclaims. The checked reduction uses 4 subclaims: fixed cardinality event failure probability antitone of event mono; binomial lower tail at matrix sample mean ge half; Bernoulli event failure lower bound from cardinality failures; sample ratio between zero and one.
import Definitions.Def_matrix_completion_fixed_cardinality open MatrixCompletion
theorem fixed_cardinality_event_failure_le_twice_bernoulli_event_failure
{n₁ n₂ : ℕ} (m : ℕ)
(Event : Finset (Fin n₁ × Fin n₂) → Prop) :
0 < n₁ → 0 < n₂ → m ≤ n₁ * n₂ →
(∀ Omega Omega' : Finset (Fin n₁ × Fin n₂),
Omega ⊆ Omega' → Event Omega → Event Omega') →
1 - fixedCardinalityEventProb m Event ≤
2 *
(1 - bernoulliEventProb
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) Event) := by
sorry