AcceptedProposition · Statement with omitted proof

Frobenius and spectral estimates for a scaled Gaussian matrix

Fixed left and right factors give complementary Frobenius and spectral estimates for SGT.

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

Download Lean file ↓

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

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Fixed left and right factors give complementary Frobenius and spectral estimates for SGT.

\begin{aligned}(\mathbb E\|SGT\|_F^2)^{1/2}&=\|S\|_F\|T\|_F,\\ \mathbb E\|SGT\|&\le\|S\|\|T\|_F+\|S\|_F\|T\|.\end{aligned}

Assumptions & context

G is standard real Gaussian and S,T are fixed compatible matrices.

Source

Halko, Martinsson & Tropp. Finding structure with randomness.

Source label: prop:scaled-gauss

02 / LEAN REPRESENTATION

Formal statement

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

theorem prop_scaled_gauss {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    {a b c d : ℕ}
    (S : Matrix (Fin a) (Fin b) ℝ) (T : Matrix (Fin c) (Fin d) ℝ)
    (G : Ω → Matrix (Fin b) (Fin c) ℝ)
    (hG : StandardGaussianTestMatrix P G) :
    Real.sqrt (∫ ω, frobeniusNorm (S * G ω * T) ^ 2 ∂P)
        = frobeniusNorm S * frobeniusNorm T ∧
      ∫ ω, ‖S * G ω * T‖ ∂P
        ≤ ‖S‖ * frobeniusNorm T + frobeniusNorm S * ‖T‖ := 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.HMTScaledGauss

/-- The Frobenius norm `‖M‖_F = (∑_{i,j} |m_{ij}|^2)^{1/2}` of a real matrix.
It is defined explicitly because the spectral norm `‖·‖` is the scoped L2-operator
norm opened in the header. -/
noncomputable def frobeniusNorm {m n : ℕ} (M : Matrix (Fin m) (Fin n) ℝ) : ℝ :=
  Real.sqrt (∑ i, ∑ j, M i j ^ 2)

/-- HMT (2011) Proposition (prop:scaled-gauss), scaled Gaussian matrices.
Fix matrices `S` and `T`, and draw a standard Gaussian matrix `G`. Then
`(𝔼‖SGT‖_F^2)^{1/2} = ‖S‖_F ‖T‖_F` and `𝔼‖SGT‖ ≤ ‖S‖ ‖T‖_F + ‖S‖_F ‖T‖`.
Here `‖·‖` is the spectral (ℓ₂ operator) norm and `‖·‖_F` is the Frobenius norm. -/
theorem prop_scaled_gauss {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    {a b c d : ℕ}
    (S : Matrix (Fin a) (Fin b) ℝ) (T : Matrix (Fin c) (Fin d) ℝ)
    (G : Ω → Matrix (Fin b) (Fin c) ℝ)
    (hG : StandardGaussianTestMatrix P G) :
    Real.sqrt (∫ ω, frobeniusNorm (S * G ω * T) ^ 2 ∂P)
        = frobeniusNorm S * frobeniusNorm T ∧
      ∫ ω, ‖S * G ω * T‖ ∂P
        ≤ ‖S‖ * frobeniusNorm T + frobeniusNorm S * ‖T‖ := by
  sorry

end RNLAPhaseB.HMTScaledGauss

How to read the formalization

The first clause is an exact second-moment identity; the second is an upper bound on the expected norm.

← Back to all statements