Expected norms 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.GaussInvExpect

/-- The Moore–Penrose conditions: `X` is the pseudoinverse `A^†` of the real matrix `A`.
Over ℝ, self-adjointness is symmetry (`Mᵀ = M`). These four conditions determine `X`
uniquely, so a binder constrained by them denotes the source's `A^†`. -/
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 of a real matrix: the sum of squares of its entries. -/
noncomputable def frobeniusNormSq {m n : ℕ} (M : Matrix (Fin m) (Fin n) ℝ) : ℝ :=
  ∑ i, ∑ j, (M i j) ^ 2

/-- HMT 2011, Proposition (prop:gauss-inv-expect).
Let `G` be a `k × (k+p)` standard Gaussian matrix with `k ≥ 2`, `p ≥ 2`, and let `Gdag ω`
be its pseudoinverse `G(ω)^†` for every sample point. Then
`(E ‖G^†‖_F^2)^{1/2} = √(k/(p-1))` and `E ‖G^†‖ ≤ e √(k+p) / p`, where `‖·‖` is the
spectral (ℓ₂ operator) norm and `e = exp 1`. The expectation `E ‖G^†‖` being bounded by a
finite number is stated together with its integrability (otherwise Lean's Bochner integral
would make the inequality vacuous). -/
theorem gauss_inv_expect
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (k p : ℕ) (hk : 2 ≤ k) (hp : 2 ≤ p)
    (G : Ω → Matrix (Fin k) (Fin (k + p)) ℝ)
    (hG : RNLAPhaseB.StandardGaussianTestMatrix P G)
    (Gdag : Ω → Matrix (Fin (k + p)) (Fin k) ℝ)
    (hGdag : ∀ ω, IsMoorePenroseInverse (G ω) (Gdag ω)) :
    Real.sqrt (∫ ω, frobeniusNormSq (Gdag ω) ∂P) = Real.sqrt ((k : ℝ) / ((p : ℝ) - 1)) ∧
    (Integrable (fun ω => ‖Gdag ω‖) P ∧
      ∫ ω, ‖Gdag ω‖ ∂P ≤ Real.exp 1 * Real.sqrt ((k : ℝ) + (p : ℝ)) / (p : ℝ)) := by
  sorry

end RNLAPhaseB.HMT2011.GaussInvExpect