bernoulli_nonnegative_statistic_moment_from_scaled_large_deviation_bound
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. Generic tail-integration/summation step for a nonnegative Bernoulli statistic. If has the scaled large-deviation tail for all , then its th moment is bounded by a universal multiple of in the moment window used in Appendix 9.2.
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_nonnegative_statistic_moment_from_scaled_large_deviation_bound
(Cdev : ℝ) :
0 < Cdev →
∃ Cmoment : ℝ, 0 < Cmoment ∧
∀ (β : ℝ), 2 < β →
∀ (n₁ n₂ m q : ℕ),
0 < n₁ → 0 < n₂ → m ≤ n₁ * n₂ →
1 ≤ q →
(q : ℝ) ≥ β * Real.log (↑(max n₁ n₂)) →
(q : ℝ) ≤
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) * (↑(max n₁ n₂)) →
∀ F : Finset (Fin n₁ × Fin n₂) → ℝ,
(∀ Omega : Finset (Fin n₁ × Fin n₂), 0 ≤ F Omega) →
(∀ lambda : ℝ, 2 ≤ lambda →
bernoulliEventProb ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
(fun Omega : Finset (Fin n₁ × Fin n₂) =>
lambda *
(((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) *
(↑(max n₁ n₂))) <
F Omega) ≤
(↑(max n₁ n₂)) *
Real.exp
(-(lambda *
(((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) *
(↑(max n₁ n₂)))) / Cdev)) →
bernoulliExpectation ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))
(fun Omega : Finset (Fin n₁ × Fin n₂) => F Omega ^ q) ≤
(Cmoment * ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) *
(↑(max n₁ n₂))) ^ q := by
sorry