Expected Frobenius 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.AvgFrobErrorGauss

/-- Eigenvalues of the Gram matrix `Aᴴ A` (= `Aᵀ A` over ℝ), in Mathlib's unspecified order.
These are the squared singular values of `A`, padded with zeros up to length `n`. -/
noncomputable def gramEigenvalues {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) : Fin n → ℝ :=
  (Matrix.isHermitian_conjTranspose_mul_self A).eigenvalues

/-- The Gram eigenvalues rearranged in nondecreasing order (via `Tuple.sort`). -/
noncomputable def sortedGramEigenvalues {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) :
    Fin n → ℝ :=
  gramEigenvalues A ∘ Tuple.sort (gramEigenvalues A)

/-- The `j`th singular value `σ_j` of `A` (1-based, nonincreasing order
`σ_1 ≥ σ_2 ≥ ⋯`), computed from `A`; zero for indices outside `1..n`. -/
noncomputable def singularValue {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (j : ℕ) : ℝ :=
  if h : 1 ≤ j ∧ j ≤ n then
    Real.sqrt (sortedGramEigenvalues A ⟨n - j, by obtain ⟨h1, h2⟩ := h; omega⟩)
  else 0

/-- The tail `∑_{j>k} σ_j²` (all singular values beyond index `n` vanish). -/
noncomputable def singularValueTailSq {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (k : ℕ) : ℝ :=
  ∑ j ∈ Finset.Icc (k + 1) n, singularValue A j ^ 2

/-- The Frobenius norm of a real matrix. -/
noncomputable def frobeniusNorm {m n : ℕ} (M : Matrix (Fin m) (Fin n) ℝ) : ℝ :=
  Real.sqrt (∑ i, ∑ j, M i j ^ 2)

/-- HMT 2011, Theorem (thm:avg-frob-error-gauss): average Frobenius error of the
Gaussian randomized range finder. For a real `m × n` matrix `A`, target rank `k ≥ 2`,
oversampling `p ≥ 2` with `k + p ≤ min m n`, an `n × (k+p)` standard Gaussian `Ω`
and `Y = AΩ`,
`E ‖(I - P_Y) A‖_F ≤ (1 + k/(p-1))^{1/2} (∑_{j>k} σ_j²)^{1/2}`. -/
theorem avg_frob_error_gauss
    {Ωs : Type*} [MeasurableSpace Ωs] (P : Measure Ωs)
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (k p : ℕ)
    (hk : 2 ≤ k) (hp : 2 ≤ p) (hkp : k + p ≤ min m n)
    (Omega : Ωs → Matrix (Fin n) (Fin (k + p)) ℝ)
    (hOmega : RNLAPhaseB.StandardGaussianTestMatrix P Omega) :
    (∫ ω, frobeniusNorm ((1 - orthogonalProjector (A * Omega ω)) * A) ∂P)
      ≤ Real.sqrt (1 + (k : ℝ) / ((p : ℝ) - 1)) * Real.sqrt (singularValueTailSq A k) := by
  sorry

end RNLAPhaseB.HMT2011.AvgFrobErrorGauss