Row norms are invariant across factorizations $UU^\top=ZZ^\top$ (Claim C.2)

Proved

MatrixCompletion.NoSpuriousMin.row_norms_of_factorization

by Shuze Chen · Aug 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

matrix-completionmc-no-spuriousnonconvex-optimization

If $U,Z\in\mathbb{R}^{d\times r}$ satisfy $UU^\top=ZZ^\top$ , then every row satisfies $\|U_i\|=\|Z_i\|$ ; consequently $\|U\|_F=\|Z\|_F$ . In particular all exact factors of $M=ZZ^\top$ are equally incoherent — the symmetric-case substitute for the row-norm bounds on both factors in the asymmetric analysis of Sun–Luo. (Immediate from $\|U_i\|^2=(UU^\top)_{ii}$ .)

Preamble

import Definitions.Def_MCNoSpuriousMinModel
open Matrix MatrixCompletion.NoSpuriousMin

Formal statement

theorem MatrixCompletion.NoSpuriousMin.row_norms_of_factorization
    {d r : ℕ} (U Z : Matrix (Fin d) (Fin r) ℝ)
    (hU : U * Uᵀ = Z * Zᵀ) (i : Fin d) :
    rowNorm U i = rowNorm Z i := 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], Section 4.3 (auxiliary fact used to transfer incoherence to the aligned factor U; immediate from ||U_i||^2 = (UU^T)_ii). Explicitly stated as Ge, Lee, Ma 2016, Matrix Completion has No Spurious Local Minimum, https://arxiv.org/abs/1605.07272 (v4), p. 21, Claim C.2.

View graph

Row norms are invariant across factorizations UU⊤=ZZ⊤UU^\top=ZZ^\topUU⊤=ZZ⊤ (Claim C.2)

Row norms are invariant across factorizations $UU^\top=ZZ^\top$ (Claim C.2)