Tail of the squared Frobenius norm 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.InvGaussFrobTail

/-- The Moore–Penrose relations: `X` is the pseudoinverse `A^†` of the real matrix `A`.
These four equations determine `X` uniquely. 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

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

/-- HMT 2011, thm:inv-gauss-frob-tail. Let `G` be an `m × n` standard Gaussian matrix
with `n - m ≥ 4`. For each `t ≥ 1`,
`P{‖G^†‖_F^2 > (12 m / (n - m)) t} ≤ 4 t^{-(n-m)/2}`.
The pseudoinverse `G^†` is the random matrix `Gdag ω`, pinned down pointwise by the
Moore–Penrose relations. -/
theorem inv_gauss_frob_tail
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    {m n : ℕ} (hmn : m + 4 ≤ n)
    (G : Ω → Matrix (Fin m) (Fin n) ℝ)
    (hG : RNLAPhaseB.StandardGaussianTestMatrix P G)
    (Gdag : Ω → Matrix (Fin n) (Fin m) ℝ)
    (hGdag : ∀ ω, IsMoorePenroseInverse (G ω) (Gdag ω))
    (t : ℝ) (ht : 1 ≤ t) :
    P {ω | 12 * (m : ℝ) / ((n : ℝ) - (m : ℝ)) * t < frobeniusNormSq (Gdag ω)}
      ≤ ENNReal.ofReal (4 * t ^ (-(((n : ℝ) - (m : ℝ)) / 2))) := by
  sorry

end RNLAPhaseB.HMT2011.InvGaussFrobTail