tangent_coordinate_kernel_offdiagonal_bound_from_a0_min_dim
Provedcandes-rechtmatrix-completionreferencetangent-space
Off-diagonal tangent-kernel magnitude bound (Candes–Recht 2009, §6 eq (6.1)+(6.2), p.32). For a rank- SVD of satisfying the standard incoherence hypothesis A0 S μ₀ (the coherence bound with parameter ), the tangent-space coordinate kernel is uniformly bounded — for all index pairs , not only the diagonal — by
This is the off-diagonal generalization of the diagonal estimate (4.8) . It follows by Cauchy–Schwarz for the Frobenius inner product: (self-adjointness and idempotence of ), hence , and each factor equals by eq (4.7).
Preamble
import Definitions.Def_matrix_completion_neumann open MatrixCompletion
Formal statement
theorem tangent_coordinate_kernel_offdiagonal_bound_from_a0_min_dim :
∃ Cker : ℝ, 0 < Cker ∧
∀ (n₁ n₂ r : ℕ) (M : Matrix (Fin n₁) (Fin n₂) ℝ)
(μ₀ : ℝ) (S : SVD M r),
0 < n₁ → 0 < n₂ → 0 < r → 1 ≤ μ₀ → A0 S μ₀ →
∀ i j a b,
|tangentCoordinateKernel S i j a b| ≤
Cker * μ₀ * ((r : ℝ) / (↑(min n₁ n₂))) := by sorrySource
Candes & Recht, Exact Matrix Completion via Convex Optimization (2009), arXiv:0805.4471, §6 "Proofs of the Critical Lemmas", p.32, eq (6.1)+(6.2).