AcceptedTheorem · Statement with omitted proof

Gaussian a posteriori spectral-norm estimate

A small collection of Gaussian probes gives a probabilistic upper bound on a fixed matrix norm.

Halko, Martinsson & Tropp ↗
Source label: thm:aposteriori

Download Lean file ↓

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

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

A small collection of Gaussian probes gives a probabilistic upper bound on a fixed matrix norm.

\Pr\left\{\|B\|>\alpha\sqrt{\frac2\pi}\max_{1\le i\le r}\|B\omega^{(i)}\|_2\right\}\le\alpha^{-r}

Assumptions & context

B is fixed and real, r > 0 independent standard Gaussian vectors are drawn, and α > 1.

Source

Halko, Martinsson & Tropp. Finding structure with randomness.

Source label: thm:aposteriori

02 / LEAN REPRESENTATION

Formal statement

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

theorem aposteriori_error_estimate
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    {m n : ℕ} (B : Matrix (Fin m) (Fin n) ℝ)
    (r : ℕ) (hr : 0 < r) (α : ℝ) (hα : 1 < α)
    (Omega : Ω → Matrix (Fin n) (Fin r) ℝ)
    (hOmega : StandardGaussianTestMatrix P Omega) :
    P {ω | ¬ (‖B‖ ≤ α * Real.sqrt (2 / Real.pi) *
        Finset.univ.sup' (⟨⟨0, hr⟩, Finset.mem_univ _⟩ : (Finset.univ : Finset (Fin r)).Nonempty)
          (fun i : Fin r => l2Norm (B *ᵥ (fun j => Omega ω j i))))}
      ≤ ENNReal.ofReal ((α ^ r)⁻¹) := 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.APosteriori

/-- HMT (2011), Lemma `thm:aposteriori`.

Let `B` be a real `m × n` matrix. Fix a positive integer `r` and a real `α > 1`.
Draw an independent family `ω^(1), …, ω^(r)` of standard Gaussian vectors in `ℝⁿ`.
These are the columns `fun j => Omega ω j i` of an `n × r` random matrix whose
entries are independent `N(0,1)`, i.e. `StandardGaussianTestMatrix P Omega`.
Then `‖B‖ ≤ α √(2/π) max_{i=1..r} ‖B ω^(i)‖` except with probability `α^{-r}`:
the probability that the bound fails is at most `α^{-r}`.
Here `‖B‖` is the ℓ₂ operator norm (scoped `Matrix.Norms.L2Operator` instance)
and `‖B ω^(i)‖` is the Euclidean norm `l2Norm`. -/
theorem aposteriori_error_estimate
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    {m n : ℕ} (B : Matrix (Fin m) (Fin n) ℝ)
    (r : ℕ) (hr : 0 < r) (α : ℝ) (hα : 1 < α)
    (Omega : Ω → Matrix (Fin n) (Fin r) ℝ)
    (hOmega : StandardGaussianTestMatrix P Omega) :
    P {ω | ¬ (‖B‖ ≤ α * Real.sqrt (2 / Real.pi) *
        Finset.univ.sup' (⟨⟨0, hr⟩, Finset.mem_univ _⟩ : (Finset.univ : Finset (Fin r)).Nonempty)
          (fun i : Fin r => l2Norm (B *ᵥ (fun j => Omega ω j i))))}
      ≤ ENNReal.ofReal ((α ^ r)⁻¹) := by
  sorry

end RNLAPhaseB.HMT2011.APosteriori

How to read the formalization

The finite maximum is taken over a nonempty probe set. The failure probability depends explicitly on r and α.

← Back to all statements