Halko–Martinsson–Tropp tail bound for $\|G^{\dagger}\|_F$ : $\mathbb P\{\|G^{\dagger}\|_F^2>\frac{12r}{k-r}\,t\}\le 4t^{-(k-r)/2}$

Proved

GaussianMatrix.pinv_frobenius_tail

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

gaussian-matrixprobabilityrandom-matrix-theoryrandomized-numerical-linear-algebra

Let $G\in\mathbb R^{r\times k}$ be a standard Gaussian matrix with $k-r\ge4$ , and let $G^{\dagger}=G^{\mathsf T}(GG^{\mathsf T})^{-1}$ . For every $t\ge1$ ,

\mathbb P\Bigl\{\|G^{\dagger}\|_F^2>\frac{12\,r}{k-r}\cdot t\Bigr\}\ \le\ 4\,t^{-(k-r)/2}.

This is the large-deviation bound for the Frobenius norm of a pseudo-inverted Gaussian matrix, which Halko–Martinsson–Tropp introduced (Theorem A.6; stated as Proposition 10.4 eq. (10.5) in the form $\mathbb P\{\|G^{\dagger}\|_F\ge\sqrt{12k/p}\,t\}\le4t^{-p}$ ) to prove deviation bounds for the Frobenius error of the randomized SVD. Unlike the spectral-norm tail, it is proved through the bidiagonal (Householder) model of a Gaussian matrix and chi-square moment estimates.

Formalization Note. The event is $\{\tfrac{12r}{k-r}t<\|G^{\dagger}\|_F^2\}$ with pinvR as $G^{\dagger}$ ; the exponent $-(k-r)/2$ is a real power (rpow) of $t\ge1$ .

Preamble

import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix

Formal statement

namespace GaussianMatrix
theorem pinv_frobenius_tail {r k : ℕ} (hrk : r + 4 ≤ k) (t : ℝ) (ht : 1 ≤ t) :
    (gaussianMatrix r k) {G | 12 * (r : ℝ) / ((k : ℝ) - r) * t < frobSq (pinvR (Matrix.of G))}
      ≤ ENNReal.ofReal (4 * t ^ (-(((k : ℝ) - r) / 2))) := by sorry
end GaussianMatrix

Source

N. Halko, P.-G. Martinsson, J. A. Tropp, *Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions*, SIAM Review 53(2), 2011, https://arxiv.org/abs/0909.4061 (v2), Appendix A.3 p. 65, Theorem A.6: for an

m\times n

standard Gaussian

G

with

n-m\ge4

and

t\ge1

\mathbb P\{\|G^\dagger\|_F^2>\frac{12m}{n-m}\cdot t\}\le4t^{-(n-m)/2}

(equivalently §10.1 p. 56, Proposition 10.4 eq. (10.5)).

Read-back

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

Throughout, $\mu_{r,k}$ denotes the measure called gaussianMatrix r k: the product measure on the function space $\{0,\dots,r-1\}\times\{0,\dots,k-1\}\to\mathbb{R}$ in which every one of the $rk$ coordinates is an independent standard normal $\mathcal N(0,1)$ ; it is a probability measure, and a sample $G$ is viewed as the real $r\times k$ matrix with entries $G_{ij}$ . Matrix inversion $(\cdot)^{-1}$ is Mathlib's total inverse on square real matrices: it is the usual inverse when the determinant is nonzero and is the zero matrix otherwise. For an $r\times k$ matrix $G$ , write $G^{\dagger} := G^{\top}(GG^{\top})^{-1}$ , a $k\times r$ real matrix (the bundle's pinvR; it is the zero matrix when $GG^{\top}$ is singular), and $\|A\|_F^2 := \sum_i\sum_j A_{ij}^2$ (the bundle's frobSq).

Statement. Let $r,k$ be natural numbers with $r+4\le k$ , and let $t$ be a real number with $1\le t$ . The theorem asserts the single inequality of extended non-negative reals

\mu_{r,k}\Big(\big\{\,G \;:\; \tfrac{12\,r}{k-r}\cdot t \;<\; \big\|G^{\top}(GG^{\top})^{-1}\big\|_F^{2}\,\big\}\Big)\;\le\;\operatorname{ofReal}\!\Big(4\cdot t^{-\frac{k-r}{2}}\Big),

where $r,k$ are cast to $\mathbb{R}$ , the threshold is $\big(12r/(k-r)\big)\cdot t$ (the product is left-associated: $12 r$ divided by $k-r$ , then multiplied by $t$ ), the exponent $-\tfrac{k-r}{2}$ is a real exponent (real power of $t$ ), and $\operatorname{ofReal}$ maps a real to $[0,\infty]$ (negative inputs map to $0$ ). The set on the left consists of samples whose $G^{\dagger}$ has squared Frobenius norm strictly greater than the threshold, and $\mu_{r,k}$ is applied as an outer measure.

Edge cases. Since $k\ge r+4$ , $k-r\ge4>0$ , so the division is ordinary and the exponent satisfies $-\tfrac{k-r}{2}\le -2$ ; since $t\ge1>0$ , $t^{-(k-r)/2} = 1/t^{(k-r)/2}$ is a positive real and $4t^{-(k-r)/2}\in(0,4]$ , so no clipping by $\operatorname{ofReal}$ occurs. Because $\mu_{r,k}$ is a probability measure the left side is at most $1$ , so the claim is automatic whenever $4t^{-(k-r)/2}\ge1$ , i.e. for $1\le t\le 4^{2/(k-r)}$ . When $r=0$ the threshold is $0$ and $\|G^{\dagger}\|_F^2$ is an empty sum equal to $0$ , so the set is empty and the left side is $0$ . Nothing is claimed for $t<1$ .

Human review

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

View graph

Halko–Martinsson–Tropp tail bound for ∥G†∥F\|G^{\dagger}\|_F∥G†∥F​: P{∥G†∥F2>12rk−r t}≤4t−(k−r)/2\mathbb P\{\|G^{\dagger}\|_F^2>\frac{12r}{k-r}\,t\}\le 4t^{-(k-r)/2}P{∥G†∥F2​>k−r12r​t}≤4t−(k−r)/2

Halko–Martinsson–Tropp tail bound for $\|G^{\dagger}\|_F$ : $\mathbb P\{\|G^{\dagger}\|_F^2>\frac{12r}{k-r}\,t\}\le 4t^{-(k-r)/2}$