Expected spectral norm of a Gaussian matrix product

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

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

namespace RNLAPhaseB.HMT2011GaussSpecExpect

/-- The Frobenius norm `‖A‖_F = (∑_{i,j} |a_{ij}|²)^{1/2}` of a real matrix.
It is written out explicitly so that it does not clash with the scoped spectral
(L2 operator) norm instance used for `‖·‖`. -/
noncomputable def frobeniusNorm {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) : ℝ :=
  Real.sqrt (∑ i, ∑ j, A i j ^ 2)

/-- HMT (2011), Proposition `prop:gauss-spec-expect`.

Fix real matrices `S`, `T`, and draw a standard Gaussian matrix `G`. Then
`E ‖S G T‖ ≤ ‖S‖ ‖T‖_F + ‖S‖_F ‖T‖`.

Here `‖·‖` is the spectral norm (the scoped L2 operator norm on matrices),
`‖·‖_F` is the Frobenius norm, `G` is a matrix-valued random variable on a
probability space `(Ω, P)` with independent standard normal entries, and the
expectation is the Bochner integral against `P`. -/
theorem gauss_spec_expect
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    {m k l n : ℕ}
    (S : Matrix (Fin m) (Fin k) ℝ) (T : Matrix (Fin l) (Fin n) ℝ)
    (G : Ω → Matrix (Fin k) (Fin l) ℝ)
    (hG : StandardGaussianTestMatrix P G) :
    ∫ ω, ‖S * G ω * T‖ ∂P ≤ ‖S‖ * frobeniusNorm T + frobeniusNorm S * ‖T‖ := by
  sorry

end RNLAPhaseB.HMT2011GaussSpecExpect