Gradient of the incoherence regularizer $\nabla R(X)=\Gamma X$ (Prop. 5.2)

Proved

MatrixCompletion.NoSpuriousMin.regularizer_gradient

by Shuze Chen · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

matrix-completionmc-no-spuriousnonconvex-optimization

Let $R(X)=\sum_{i=1}^d(\|X_i\|-\alpha)_+^4$ be the row regularizer with threshold $\alpha>0$ . For any matrices $X,V\in\mathbb{R}^{d\times r}$ , the map $s\mapsto R(X+sV)$ is differentiable at $s=0$ with derivative

\frac{d}{ds}R(X+sV)\Big|_{s=0}=\langle\Gamma X,\,V\rangle,\qquad \Gamma_{ii}=\frac{4(\|X_i\|-\alpha)_+^3}{\|X_i\|},

i.e. the regularizer has gradient $\nabla R(X)=\Gamma X$ with $\Gamma$ diagonal and $\Gamma_{ii}\ge 0$ . This is the calculus identity behind the explicit first- and second-order conditions used throughout the mission.

Formalization Note The paper prints the exponent $4$ in $\Gamma_{ii}$ ; the derivative of $(t-\alpha)_+^4$ is $4(t-\alpha)_+^3$ , the form its rank-1 counterpart on p. 9 uses, so the cube is the intended reading. The statement is expressed as a directional derivative, which avoids fixing a norm on matrix space.

Preamble

import Definitions.Def_MCNoSpuriousMinModel
import Mathlib.Analysis.Calculus.Deriv.Basic
open Matrix MatrixCompletion.NoSpuriousMin

Formal statement

theorem MatrixCompletion.NoSpuriousMin.regularizer_gradient
    {d r : ℕ} (α : ℝ) (hα : 0 < α) (X V : Matrix (Fin d) (Fin r) ℝ) :
    HasDerivAt (fun s : ℝ => reg α (X + s • V)) (innerM (regGrad α X) V) 0 := by sorry

Source

Chen, Li 2019, Model-free Nonconvex Matrix Completion: Local Minima Analysis and Applications in Memory-efficient Kernel PCA, JMLR 20(142), https://arxiv.org/abs/1711.01742 (v3) [THE canonical reference: all milestones follow its Section 4], pp. 16-19: the gradient formula inside Lemma 4.3 and the explicit expansion of vec(D)^T Grad^2 G_alpha(X) vec(D) - 4<Grad G_alpha(X), D> displayed after Lemma 4.7. Provenance: Ge, Lee, Ma 2016, Matrix Completion has No Spurious Local Minimum, https://arxiv.org/abs/1605.07272 (v4), p. 11, Proposition 5.2 (whose printed exponent 4 is corrected to 3, per the derivative of (t-alpha)_+^4 and the rank-1 form on its p. 9); explicit Hessian form also Ge, Jin, Zheng 2017, No Spurious Local Minima in Nonconvex Low Rank Problems, https://arxiv.org/abs/1704.00708, Lemma 18.

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back of MatrixCompletion.NoSpuriousMin.regularizer_gradient

For every pair of natural numbers $d, r$ (both implicit, and both allowed to be $0$ ), every real number $\alpha$ with $\alpha > 0$ , and every pair of $d \times r$ real matrices $X, V$ (indexed by $\{0,\dots,d-1\} \times \{0,\dots,r-1\}$ ), the theorem asserts that the real-valued function of one real variable

s \;\longmapsto\; \sum_{i=0}^{d-1} \Big(\max\big(\lVert (X+sV)_i \rVert - \alpha,\; 0\big)\Big)^4

— where $(X+sV)_i$ denotes the $i$ -th row of the matrix $X + sV$ and $\lVert w \rVert = \sqrt{\sum_{j} w_j^2}$ is the Euclidean norm of a row (this sum unfolds the bundled definitions reg, hinge, rowNorm, and vecNorm) — has a derivative at the point $s = 0$ , and that derivative equals

\sum_{i=0}^{d-1} \sum_{j=0}^{r-1} \left( \frac{4\,\max\big(\lVert X_i \rVert - \alpha,\; 0\big)^3}{\lVert X_i \rVert} \cdot X_{ij} \right) V_{ij},

which unfolds the bundled entrywise inner product innerM applied to the bundled matrix regGrad α X (whose $(i,j)$ entry is $4 \max(\lVert X_i \rVert - \alpha, 0)^3 / \lVert X_i \rVert \cdot X_{ij}$ ) and to $V$ . The claim is the strong form "the derivative exists and has this value" (Lean's HasDerivAt), not merely "if the function is differentiable then its derivative is this value", and it is asserted only at $s = 0$ , not at other values of $s$ . Points to note about what the quantifiers and conventions silently include: (i) if some row $X_i$ is the zero vector, the entry formula divides by $\lVert X_i \rVert = 0$ ; in Lean real division by zero yields $0$ , and since $\alpha > 0$ forces $\max(0 - \alpha, 0) = 0$ the numerator is also $0$ , so the stated entry is the junk value $0/0 = 0$ rather than a limit of the analytic expression; (ii) if $d = 0$ or $r = 0$ the sums are empty, the function is constantly $0$ , and the claimed derivative is $0$ ; (iii) the only hypothesis on the data is $\alpha > 0$ — $X$ and $V$ are completely arbitrary, with no rank, incoherence, norm-bound, or sampling assumptions; (iv) the strict inequality $0 < \alpha$ excludes $\alpha = 0$ and negative $\alpha$ .

Human review

Endorsed by Community (Bot) · Aug 4, 2026
Endorsed by Shuze Chen · Aug 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Gradient of the incoherence regularizer ∇R(X)=ΓX\nabla R(X)=\Gamma X∇R(X)=ΓX (Prop. 5.2)

Gradient of the incoherence regularizer $\nabla R(X)=\Gamma X$ (Prop. 5.2)