Expected spectral norm of a rectangular Gaussian pseudoinverse

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.InvGaussSpecExpect

/-- `X` is the (Moore–Penrose) pseudoinverse `A^†` of the real matrix `A`: the four
Penrose equations `A X A = A`, `X A X = X`, `(A X)ᵀ = A X`, `(X A)ᵀ = X A`.
These equations determine `X` uniquely. This is the source's dagger notation. -/
def IsPseudoinverse {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

/-- HMT (2011), Proposition `prop:inv-gauss-spec-expect`:
let `G` be an `m × n` standard Gaussian matrix with `n - m ≥ 1` and `m ≥ 2`. Then
`E ‖G^†‖ < e √n / (n - m)`, where `‖·‖` is the spectral (ℓ₂ operator) norm.
The random pseudoinverse `Gdag ω` is pinned samplewise by the Penrose equations.
The expectation claim is stated as integrability (the expectation is finite) together
with the strict bound on the Bochner integral. -/
theorem expect_norm_pinv_gaussian_lt
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (m n : ℕ) (hnm : 1 ≤ n - m) (hm : 2 ≤ m)
    (G : Ω → Matrix (Fin m) (Fin n) ℝ)
    (hG : RNLAPhaseB.StandardGaussianTestMatrix P G)
    (Gdag : Ω → Matrix (Fin n) (Fin m) ℝ)
    (hGdag : ∀ ω, IsPseudoinverse (G ω) (Gdag ω)) :
    Integrable (fun ω => ‖Gdag ω‖) P ∧
      (∫ ω, ‖Gdag ω‖ ∂P) < Real.exp 1 * Real.sqrt (n : ℝ) / ((n : ℝ) - (m : ℝ)) := by
  sorry

end RNLAPhaseB.HMT2011.InvGaussSpecExpect