AcceptedProposition · Statement with omitted proof

Spectral tail of a rectangular Gaussian pseudoinverse

The pseudoinverse spectral norm has a polynomial upper-tail bound governed by the dimension gap.

Halko, Martinsson & Tropp ↗
Source label: prop:inv-gauss-spec-tail

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

The pseudoinverse spectral norm has a polynomial upper-tail bound governed by the dimension gap.

\Pr\{\|G^\dagger\|>t\}\le\frac1{\sqrt{2\pi(n-m+1)}}\left(\frac{e\sqrt n}{n-m+1}\right)^{n-m+1}t^{-(n-m+1)}

Assumptions & context

G is standard Gaussian m × n with n ≥ m ≥ 2; t > 0.

Source

Halko, Martinsson & Tropp. Finding structure with randomness.

Source label: prop:inv-gauss-spec-tail

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem inv_gauss_spec_tail {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (m n : ℕ) (hm : 2 ≤ m) (hmn : m ≤ n)
    (G : Ω → Matrix (Fin m) (Fin n) ℝ) (hG : StandardGaussianTestMatrix P G)
    (Gdag : Ω → Matrix (Fin n) (Fin m) ℝ)
    (hGdag : ∀ ω, IsMoorePenroseInverse (G ω) (Gdag ω))
    (t : ℝ) (ht : 0 < t) :
    P {ω | t < ‖Gdag ω‖} ≤
      ENNReal.ofReal
        ((1 / Real.sqrt (2 * Real.pi * ((n - m + 1 : ℕ) : ℝ))) *
          (Real.exp 1 * Real.sqrt (n : ℝ) / ((n - m + 1 : ℕ) : ℝ)) ^ (n - m + 1) *
          t ^ (-((n - m + 1 : ℕ) : ℤ))) := by
  sorry

Complete Lean file and local definitions

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal

namespace RNLAPhaseB.HMT2011InvGaussSpecTail

/-- `X` is the Moore–Penrose pseudoinverse `A^†` of the real matrix `A`, characterised by
the four Penrose equations (over ℝ, self-adjoint means `Mᵀ = M`). These equations determine
`X` uniquely, so constraining a binder by them denotes the pseudoinverse. -/
def IsMoorePenroseInverse {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
    (X : Matrix (Fin n) (Fin m) ℝ) : Prop :=
  A * X * A = A ∧ X * A * X = X ∧ (A * X)ᵀ = A * X ∧ (X * A)ᵀ = X * A

/-- HMT 2011, Proposition (prop:inv-gauss-spec-tail). Let `G` be an `m × n` standard
Gaussian matrix with `n ≥ m ≥ 2`. For each `t > 0`,
`P{‖G^†‖ > t} ≤ (2π(n-m+1))^{-1/2} [e √n / (n-m+1)]^{n-m+1} t^{-(n-m+1)}`,
where `‖·‖` is the spectral (ℓ₂ operator) norm and `G^†` is the pseudoinverse of `G`. -/
theorem inv_gauss_spec_tail {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (m n : ℕ) (hm : 2 ≤ m) (hmn : m ≤ n)
    (G : Ω → Matrix (Fin m) (Fin n) ℝ) (hG : StandardGaussianTestMatrix P G)
    (Gdag : Ω → Matrix (Fin n) (Fin m) ℝ)
    (hGdag : ∀ ω, IsMoorePenroseInverse (G ω) (Gdag ω))
    (t : ℝ) (ht : 0 < t) :
    P {ω | t < ‖Gdag ω‖} ≤
      ENNReal.ofReal
        ((1 / Real.sqrt (2 * Real.pi * ((n - m + 1 : ℕ) : ℝ))) *
          (Real.exp 1 * Real.sqrt (n : ℝ) / ((n - m + 1 : ℕ) : ℝ)) ^ (n - m + 1) *
          t ^ (-((n - m + 1 : ℕ) : ℤ))) := by
  sorry

end RNLAPhaseB.HMT2011InvGaussSpecTail

How to read the formalization

The failure event is a strict exceedance. The exponent n−m+1 also determines the normalizing constant.

← Back to all statements