Exact Frobenius second moment of a 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.InvGaussFrobExpect

/-- `X` is the Moore–Penrose pseudoinverse of the real matrix `A`. The source writes this
as `A^†`. The four Penrose conditions determine it uniquely: `A X A = A`, `X A X = X`,
and `A X` and `X A` are symmetric. Over `ℝ`, self-adjoint means `Mᵀ = M`. -/
def IsMoorePenroseInverse {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

/-- The squared Frobenius norm `‖M‖_F^2`, which is the sum of the squared entries. -/
noncomputable def frobeniusNormSq {p q : ℕ} (M : Matrix (Fin p) (Fin q) ℝ) : ℝ :=
  ∑ i, ∑ j, (M i j) ^ 2

/-- HMT 2011, Proposition (prop:inv-gauss-frob-expect).

Let `G` be an `m × n` standard Gaussian matrix with `n - m ≥ 2`. Then
`𝔼 ‖G^†‖_F^2 = m / (n - m - 1)`.

The pseudoinverse `G^†` is represented by the sample-wise matrix `Gpinv ω`. That matrix
satisfies the Penrose conditions for `G ω` at every sample point. Because the
Moore–Penrose inverse is unique, this pins it down exactly. -/
theorem inv_gauss_frob_expect
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (m n : ℕ) (hnm : 2 ≤ n - m)
    (G : Ω → Matrix (Fin m) (Fin n) ℝ)
    (hG : RNLAPhaseB.StandardGaussianTestMatrix P G)
    (Gpinv : Ω → Matrix (Fin n) (Fin m) ℝ)
    (hGpinv : ∀ ω, IsMoorePenroseInverse (G ω) (Gpinv ω)) :
    ∫ ω, frobeniusNormSq (Gpinv ω) ∂P = (m : ℝ) / ((n : ℝ) - (m : ℝ) - 1) := by
  sorry

end RNLAPhaseB.HMT2011.InvGaussFrobExpect