Expected spectral error of Gaussian rangefinding

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

/-- The `j`-th (1-based) singular value `σ_j` of a real `m × n` matrix `A`, computed from `A`.
The singular values are the square roots of the eigenvalues of `Aᴴ * A`, counted with
multiplicity. `σ_j` is the `j`-th largest of them: the supremum of all `s ≥ 0` such that at
least `j` of these values are `≥ s`. For `j > n` the set is empty and `sSup ∅ = 0`, which gives
the usual zero padding `σ_j = 0`. -/
noncomputable def singularValue {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (j : ℕ) : ℝ := by
  classical
  exact sSup {s : ℝ | 0 ≤ s ∧
    j ≤ (Finset.univ.filter (fun i : Fin n =>
      s ≤ Real.sqrt ((Matrix.isHermitian_conjTranspose_mul_self A).eigenvalues i))).card}

/-- HMT 2011, Theorem `thm:avg-spec-error-gauss`, under the hypotheses of Theorem
`thm:avg-frob-error-gauss`.

The hypotheses are as follows. `A` is a real `m × n` matrix with singular values
`σ₁ ≥ σ₂ ≥ ⋯`. The target rank satisfies `k ≥ 2` and the oversampling parameter satisfies
`p ≥ 2`, with `k + p ≤ min {m, n}`. `Ω` is an `n × (k+p)` standard Gaussian matrix and
`Y = A Ω`.

The conclusion is
`E ‖(I - P_Y) A‖ ≤ (1 + √(k/(p-1))) σ_{k+1} + (e √(k+p) / p) (∑_{j>k} σ_j²)^{1/2}`.
Here `‖·‖` is the spectral (ℓ₂ operator) norm and `e` is Euler's number. -/
theorem avg_spec_error_gauss
    {S : Type*} [MeasurableSpace S] (P : Measure S)
    (m n k p : ℕ) (A : Matrix (Fin m) (Fin n) ℝ)
    (hk : 2 ≤ k) (hp : 2 ≤ p) (hkp : k + p ≤ min m n)
    (Om : S → Matrix (Fin n) (Fin (k + p)) ℝ)
    (hOm : RNLAPhaseB.StandardGaussianTestMatrix P Om) :
    (∫ ω, ‖(1 - orthogonalProjector (A * Om ω)) * A‖ ∂P)
      ≤ (1 + Real.sqrt ((k : ℝ) / ((p : ℝ) - 1))) * singularValue A (k + 1)
        + Real.exp 1 * Real.sqrt ((k : ℝ) + (p : ℝ)) / (p : ℝ)
          * Real.sqrt (∑ j ∈ Finset.Icc (k + 1) n, singularValue A j ^ 2) := by
  sorry

end RNLAPhaseB.HMT2011.AvgSpecErrorGauss