§3.3, proof of Prop. 3.4, p. 10 — ‖X − Y‖² = ‖X‖² + m − 2 trace(YᵀX) for Y ∈ V_{n,m}

Proved

ProjLikeRetr.Stiefel.dist_sq_stiefel

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

frobenius-normlinear-algebrap2o-batch-pfp1ap2o-gran-per-chapterp2o-plan-paperp2o-v1stiefel-manifold

Let $X\in\mathbb R^{n\times m}$ and let $\|\cdot\|$ be the Frobenius norm, $\|X\|^2=\sum_{i,j}X_{ij}^2=\operatorname{trace}(X^\top X)$ . For every $Y$ in the Stiefel manifold $V_{n,m}=\{Y: Y^\top Y=I_m\}$ ,

\|X-Y\|^2=\|X\|^2+m-2\operatorname{trace}(Y^\top X).

The identity reduces the projection of $X$ onto $V_{n,m}$ to the maximization of the linear function $Y\mapsto\operatorname{trace}(Y^\top X)$ over $V_{n,m}$ , which is the first step of the proof of Proposition 3.4.

Formalization Note The page prints the constant as $m^2$ . Since $\|Y\|^2=\operatorname{trace}(Y^\top Y)=\operatorname{trace}(I_m)=m$ , the correct constant is $m$ ; with $m^2$ the identity is false for every $m\ge2$ (take $X=Y$ ). The statement uses $m$ .

Preamble

import Mathlib
import Definitions.Def_ProjLikeRetr_Stiefel_stiefel

open scoped Matrix Matrix.Norms.Frobenius

Formal statement

namespace ProjLikeRetr.Stiefel

/-- §3.3, proof of Proposition 3.4, p. 10: for every real `n × m` matrix `X` and every
`Y ∈ V_{n,m}`, `‖X − Y‖² = ‖X‖² + m − 2 trace(YᵀX)` in the Frobenius norm. The page prints
`m²`; since `‖Y‖² = trace(YᵀY) = trace(I_m) = m`, the correct constant is `m` (with `m²` the
identity fails for `m ≥ 2`). -/
theorem dist_sq_stiefel {n m : ℕ} (X Y : Matrix (Fin n) (Fin m) ℝ) (hY : Y ∈ stiefel n m) :
    ‖X - Y‖ ^ 2 = ‖X‖ ^ 2 + (m : ℝ) - 2 * (Yᵀ * X).trace := by sorry

end ProjLikeRetr.Stiefel

Source

Absil & Malick, Projection-like retractions on matrix manifolds, HAL hal-00651608v2, p. 10, §3.3, proof of Proposition 3.4 (first sentence; the page's m² is a misprint for m)

Human review

Endorsed by Shuze Chen · Oct 4, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph