second_order_prefactored_centered_sampling_quadratic_prefactor_bound_from_base_entry_scale
ProvedRole. It is a centered-sampling fluctuation estimate, one of the reusable concentration interfaces used repeatedly by the Neumann-term bounds.
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. Raw fixed-matrix event step for the all-equal quadratic centered term with prefactor , leaving the scalar prefactor unabsorbed.
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_tangent open MatrixCompletion
theorem
second_order_prefactored_centered_sampling_quadratic_prefactor_bound_from_base_entry_scale
(Cfixed Cbase : ℝ) :
0 < Cfixed → 0 < Cbase →
∃ Cpref : ℝ, 0 < Cpref ∧
∀ (β lam : ℝ), 2 < β → 1 ≤ lam →
∀ (n₁ n₂ r m : ℕ) (μ₀ : ℝ),
0 < n₁ → 0 < n₂ → 0 < r → m ≤ n₁ * n₂ →
1 ≤ μ₀ →
∀ (Omega : Finset (Fin n₁ × Fin n₂))
(B Y : Matrix (Fin n₁) (Fin n₂) ℝ),
Y =
((((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))⁻¹) ^ 2 *
(1 - 3 * ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) +
3 * ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) ^ 2)) •
centeredSamplingFluctuation Omega
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) B →
entrySupNorm B ≤
Cbase * μ₀ ^ 3 * (((r : ℝ) / (↑(max n₁ n₂))) ^ 3) →
CenteredSamplingSpectralBound Omega
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) B
(Cfixed * Real.sqrt
((β * (↑(max n₁ n₂)) *
Real.log (↑(max n₁ n₂))) /
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))) *
entrySupNorm B) →
spectralNorm Y ≤
Cpref * Cbase *
|(((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))⁻¹) ^ 2 *
(1 - 3 * ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) +
3 * ((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ))) ^ 2)| *
μ₀ ^ 3 * (((r : ℝ) / (↑(max n₁ n₂))) ^ 3) *
Real.sqrt
((β * (↑(max n₁ n₂)) *
Real.log (↑(max n₁ n₂))) /
((m : ℝ) / ((n₁ : ℝ) * (n₂ : ℝ)))) := by
sorry