signed_kernel_square_bernstein_scale_compatibility_from_a0_sample_bound
ProvedRole. It is a scalar Bernstein-type tail estimate or deterministic scale absorption used to control sampled scalar fluctuations.
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. A0/default-sign scalar absorption for the signed kernel-square Bernstein step. Under the Lemma 4.6 sample lower bound, the sign entry times the natural quadratic scalar-Bernstein scale is absorbed into .
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_neumann open MatrixCompletion
theorem signed_kernel_square_bernstein_scale_compatibility_from_a0_sample_bound :
∃ Ccompat : ℝ, 0 < Ccompat ∧
∀ (β lam : ℝ), 2 < β → 1 ≤ lam →
∀ (n₁ n₂ r m : ℕ) (M : Matrix (Fin n₁) (Fin n₂) ℝ)
(μ₀ μ₁ : ℝ) (S : SVD M r),
0 < n₁ → 0 < n₂ → 0 < r → m ≤ n₁ * n₂ →
1 ≤ μ₀ → 1 ≤ μ₁ →
A0 S μ₀ → A1 S μ₁ →
(m : ℝ) ≥
lam * Real.rpow μ₀ ((4 : ℝ) / 3) *
(↑(max n₁ n₂)) * Real.rpow (r : ℝ) ((4 : ℝ) / 3) *
(β * Real.log (↑(max n₁ n₂))) →
∀ w : Fin n₁ × Fin n₂,
|signMatrix S w.1 w.2| *
Real.sqrt (β * Real.log (↑(max n₁ n₂))) *
Real.rpow
((μ₀ * (↑(max n₁ n₂)) * (r : ℝ)) / (m : ℝ))
((3 : ℝ) / 2) ≤
Ccompat * Real.rpow lam (-1) := by
sorry