AcceptedProposition · Statement with omitted proof

Frobenius second moment of a Gaussian matrix product

The root mean square Frobenius norm of SGT factors into the Frobenius norms of S and T.

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

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 root mean square Frobenius norm of SGT factors into the Frobenius norms of S and T.

(\mathbb E\|SGT\|_F^2)^{1/2}=\|S\|_F\|T\|_F

Assumptions & context

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

Source

Halko, Martinsson & Tropp. Finding structure with randomness.

Source label: prop:gauss-frob-expect

02 / LEAN REPRESENTATION

Formal statement

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

theorem gauss_frob_expect
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    {p k l q : ℕ}
    (S : Matrix (Fin p) (Fin k) ℝ) (T : Matrix (Fin l) (Fin q) ℝ)
    (G : Ω → Matrix (Fin k) (Fin l) ℝ)
    (hG : RNLAPhaseB.StandardGaussianTestMatrix P G) :
    (∫ ω, frobNorm (S * G ω * T) ^ 2 ∂P) ^ ((1 : ℝ) / 2) =
      frobNorm S * frobNorm 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.HMT2011GaussFrobExpect

/-- The Frobenius norm of a real matrix, `‖M‖_F = (∑_{i,j} M_{ij}^2)^{1/2}`.
It is written out explicitly because the header's scoped norm `‖·‖` is the
L2 operator (spectral) norm, not the Frobenius norm. -/
noncomputable def frobNorm {m n : ℕ} (M : Matrix (Fin m) (Fin n) ℝ) : ℝ :=
  Real.sqrt (∑ i, ∑ j, M i j ^ 2)

/-- HMT 2011, Proposition (prop:gauss-frob-expect): fix real matrices `S`, `T`
and draw a standard Gaussian matrix `G`. Then
`(𝔼 ‖S G T‖_F^2)^{1/2} = ‖S‖_F ‖T‖_F`. -/
theorem gauss_frob_expect
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    {p k l q : ℕ}
    (S : Matrix (Fin p) (Fin k) ℝ) (T : Matrix (Fin l) (Fin q) ℝ)
    (G : Ω → Matrix (Fin k) (Fin l) ℝ)
    (hG : RNLAPhaseB.StandardGaussianTestMatrix P G) :
    (∫ ω, frobNorm (S * G ω * T) ^ 2 ∂P) ^ ((1 : ℝ) / 2) =
      frobNorm S * frobNorm T := by
  sorry

end RNLAPhaseB.HMT2011GaussFrobExpect

How to read the formalization

The expectation applies to the squared Frobenius norm, not to the norm itself.

← Back to all statements