tangent_coordinate_kernel_symm

Proved

by Minghui · Jun 24, 2026 · Mathlib c5ea003 (Lean v4.30.0)

candes-rechtmatrix-completiontangent-kernel

The tangent-coordinate kernel is symmetric in its two coordinate arguments. This follows from self-adjointness of the tangent projection for the Frobenius inner product: <P_T e_ij, e_ab> = <e_ij, P_T e_ab> = <P_T e_ab, e_ij>. This reusable lemma lets later Frobenius and kernel-square estimates freely swap the fixed and summed coordinate positions.

Preamble

import Definitions.Def_matrix_completion_neumann
open MatrixCompletion

Formal statement

theorem tangent_coordinate_kernel_symm
    {n₁ n₂ r : ℕ} {M : Matrix (Fin n₁) (Fin n₂) ℝ}
    (S : SVD M r) (i a : Fin n₁) (j b : Fin n₂) :
    tangentCoordinateKernel S i j a b =
      tangentCoordinateKernel S a b i j := by
  sorry

Source

Candes-Recht tangent-space projection algebra; follows from the platform theorem tangent_projection_self_adjoint.

View graph