quadratic_neumann_last_index_distinct_centered_decoupling_transfer_general_sample
Provedcandes-rechtmatrix-completionquadratic-neumannsection-63
General-sample (constant/Φ-scale) two-variable decoupling transfer for the
centered ω₁ = ω₂ ≠ ω₃ quadratic contribution.
This is the §6.3 summary-scale analogue of
quadratic_neumann_last_index_distinct_centered_decoupling_transfer: a
high-probability two-copy (pair) Bernoulli estimate for the decoupled
contribution at an arbitrary nonnegative scale implies the corresponding
one-copy estimate, with only universal constant loss. Unlike the lam-form
node, the threshold scale is a free parameter (so it can be instantiated at
the four-term Section 6.3 summary scale Φ), and there is no weak μ₀^{4/3}
sample lower bound baked in.
Preamble
import Definitions.Def_matrix_completion_neumann open MatrixCompletion
Formal statement
theorem quadratic_neumann_last_index_distinct_centered_decoupling_transfer_general_sample :
∃ Cdecouple cdecouple : ℝ, 0 < Cdecouple ∧ 0 < cdecouple ∧
∀ {n₁ n₂ r : ℕ} {M : Matrix (Fin n₁) (Fin n₂) ℝ}
(S : SVD M r) (p Cdec cdec β scale : ℝ),
0 ≤ p → p ≤ 1 → 0 < Cdec → 0 < cdec → 0 ≤ scale →
bernoulliPairEventProb p
(fun Omega1 Omega3 =>
spectralNorm
(quadraticNeumannLastIndexDistinctCenteredDecoupledContribution
Omega1 Omega3 S p) ≤
Cdec * scale) ≥
1 - cdec * Real.rpow (↑(max n₁ n₂)) (-β) →
bernoulliEventProb p
(fun Omega =>
spectralNorm
(quadraticNeumannLastIndexDistinctCenteredContribution Omega S p) ≤
(Cdecouple * Cdec) * scale) ≥
1 - (cdecouple * cdec) * Real.rpow (↑(max n₁ n₂)) (-β) := by sorry
Source
Candes, Emmanuel, and Benjamin Recht. "Exact matrix completion via convex optimization." Communications of the ACM 55.6 (2012): 111-119.