AcceptedProposition · Statement with omitted proof

Two tail bounds for a Gaussian pseudoinverse

Polynomial tail estimates control large Frobenius and spectral norms of a Gaussian pseudoinverse.

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

Download Lean file ↓

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

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Polynomial tail estimates control large Frobenius and spectral norms of a Gaussian pseudoinverse.

\begin{aligned}\Pr\{\|G^\dagger\|_F\ge\sqrt{12k/p}\,t\}&\le4t^{-p},\\ \Pr\{\|G^\dagger\|\ge e\sqrt{k+p}\,t/(p+1)\}&\le t^{-(p+1)}.\end{aligned}

Assumptions & context

G is k × (k+p), k ≥ 1, p ≥ 4, with independent standard normal entries; t ≥ 1.

Source

Halko, Martinsson & Tropp. Finding structure with randomness.

Source label: prop:gauss-inv-tails

02 / LEAN REPRESENTATION

Formal statement

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

theorem gauss_inv_tails
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (k p : ℕ) (hk : 1 ≤ k) (hp : 4 ≤ p)
    (G : Ω → Matrix (Fin k) (Fin (k + p)) ℝ)
    (hG : RNLAPhaseB.StandardGaussianTestMatrix P G)
    (Gdag : Ω → Matrix (Fin (k + p)) (Fin k) ℝ)
    (hGdag : ∀ ω, IsMoorePenroseInverse (G ω) (Gdag ω)) :
    ∀ t : ℝ, 1 ≤ t →
      P {ω | Real.sqrt (12 * (k : ℝ) / (p : ℝ)) * t ≤ frobeniusNorm (Gdag ω)}
          ≤ ENNReal.ofReal (4 * (t ^ p)⁻¹) ∧
      P {ω | Real.exp 1 * Real.sqrt ((k : ℝ) + (p : ℝ)) / ((p : ℝ) + 1) * t ≤ ‖Gdag ω‖}
          ≤ ENNReal.ofReal ((t ^ (p + 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.HMT2011.GaussInvTails

/-- `X` is the Moore–Penrose pseudoinverse (the source's dagger `A^†`) of the real matrix `A`.
These are the four Penrose conditions, which determine `X` uniquely. -/
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

/-- The Frobenius norm `‖M‖_F = (∑_{i,j} M_{ij}^2)^{1/2}` of a real matrix. -/
noncomputable def frobeniusNorm {m n : ℕ} (M : Matrix (Fin m) (Fin n) ℝ) : ℝ :=
  Real.sqrt (∑ i, ∑ j, M i j ^ 2)

/-- HMT 2011, Proposition (prop:gauss-inv-tails).  Let `G` be a `k × (k+p)` standard
Gaussian matrix with `p ≥ 4`, and let `G^†` be its pseudoinverse.  For all `t ≥ 1`,
`P{‖G^†‖_F ≥ √(12k/p) · t} ≤ 4 t^{-p}` and
`P{‖G^†‖ ≥ e√(k+p)/(p+1) · t} ≤ t^{-(p+1)}`, where `‖·‖` is the spectral norm. -/
theorem gauss_inv_tails
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (k p : ℕ) (hk : 1 ≤ k) (hp : 4 ≤ p)
    (G : Ω → Matrix (Fin k) (Fin (k + p)) ℝ)
    (hG : RNLAPhaseB.StandardGaussianTestMatrix P G)
    (Gdag : Ω → Matrix (Fin (k + p)) (Fin k) ℝ)
    (hGdag : ∀ ω, IsMoorePenroseInverse (G ω) (Gdag ω)) :
    ∀ t : ℝ, 1 ≤ t →
      P {ω | Real.sqrt (12 * (k : ℝ) / (p : ℝ)) * t ≤ frobeniusNorm (Gdag ω)}
          ≤ ENNReal.ofReal (4 * (t ^ p)⁻¹) ∧
      P {ω | Real.exp 1 * Real.sqrt ((k : ℝ) + (p : ℝ)) / ((p : ℝ) + 1) * t ≤ ‖Gdag ω‖}
          ≤ ENNReal.ofReal ((t ^ (p + 1))⁻¹) := by
  sorry

end RNLAPhaseB.HMT2011.GaussInvTails

How to read the formalization

The two events use different norm-dependent thresholds and different tail exponents.

← Back to all statements