tangent_projection_idempotent

Proved

by Hartmann_Psi · Jun 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

linear-algebramatrix-completion

The orthogonal projection $P_T$ onto the tangent space at $M$ (defined from a rank- $r$ SVD via the left/right singular-space projectors) is idempotent: $P_T(P_T X)=P_T X$ for every matrix $X$ . This follows from orthonormality of the singular vectors and is a reusable building block for operator-norm bounds on tangent-space sampling operators (Candes-Recht 2009, Section 3-4).

Preamble

import Definitions.Def_matrix_completion_tangent
import Mathlib.Analysis.CStarAlgebra.Matrix
import Mathlib.Analysis.InnerProductSpace.PiL2

open MatrixCompletion
open scoped Classical BigOperators Matrix Matrix.Norms.L2Operator

Formal statement

theorem tangent_projection_idempotent
    {n1 n2 r : Nat} {M : RealMatrix n1 n2} (S : SVD M r)
    (X : RealMatrix n1 n2) :
    tangentProjection S (tangentProjection S X) = tangentProjection S X := by sorry

Source

Candes, Recht, Exact Matrix Completion via Convex Optimization (2009), Section 3

View graph