Prove2Me

∥A†∥2=∥(AA⊤)−1∥\|A^\dagger\|^2=\|(AA^\top)^{-1}\| for A†=A⊤(AA⊤)−1A^\dagger=A^\top(AA^\top)^{-1}

Proved
GaussianMatrix.specNorm_pinvR_sq

by tc · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

c-identitydeterministiclinear-algebrapseudoinversespectral-norm

Let AA be a real r×kr\times k matrix and let A†=A⊤(AA⊤)−1A^\dagger=A^\top(AA^\top)^{-1} be its right pseudoinverse, where the inverse of a singular matrix is taken to be 00. Then, in the spectral norm,

∥A†∥2=∥(AA⊤)−1∥.\|A^\dagger\|^2=\big\|(AA^\top)^{-1}\big\|.

Write M=AA⊤M=AA^\top, which is symmetric. By the C∗C^*-identity ∥B∥2=∥B⊤B∥\|B\|^2=\|B^\top B\| we get (A†)⊤A†=M−1AA⊤M−1=M−1MM−1=M−1(A^\dagger)^\top A^\dagger=M^{-1}AA^\top M^{-1}=M^{-1}MM^{-1}=M^{-1}. If MM is singular, both sides are 00. Together with ∥(AA⊤)−1∥=1/σmin⁡(A⊤)2\|(AA^\top)^{-1}\|=1/\sigma_{\min}(A^\top)^2 this gives ∥A†∥=1/σmin⁡(A⊤)\|A^\dagger\|=1/\sigma_{\min}(A^\top), which turns tail bounds for λmin⁡(GG⊤)\lambda_{\min}(GG^\top) into tail bounds for ∥G†∥\|G^\dagger\|.

Formalization Note. pinvR A = Aᵀ * (A * Aᵀ)⁻¹ uses Mathlib's total inverse, and specNorm is the ℓ2\ell_2 operator norm. The identity holds unconditionally.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem specNorm_pinvR_sq {r k : ℕ} (A : Matrix (Fin r) (Fin k) ℝ) :
    specNorm (pinvR A) ^ 2 = specNorm (A * Aᵀ)⁻¹ := by sorry

end GaussianMatrix
Source
standard fact: C*-identity ‖B‖² = ‖BᵀB‖ for the spectral norm, applied to B = Aᵀ(AAᵀ)⁻¹, for which BᵀB = (AAᵀ)⁻¹ (e.g. N. Halko, P.-G. Martinsson, J. A. Tropp, SIAM Review 53 (2011), §A.2, ‖G†‖ = σ_min(G)⁻¹).

View graph