Spectral tail bound for 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.HMT2011TailSpecErrorGauss

open RNLAPhaseB

/-- The `j`-th singular value (1-based) of a real `m × n` matrix `A`, i.e. the square root
of the `j`-th largest eigenvalue of `Aᴴ A` (Mathlib's `eigenvalues₀` are listed in
nonincreasing order). It is zero-padded: `singularValue A j = 0` for `j = 0` or `j > n`.
The singular values are therefore `σ₁ ≥ σ₂ ≥ σ₃ ≥ …`, as in the source. -/
noncomputable def singularValue {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (j : ℕ) : ℝ :=
  if h : 1 ≤ j ∧ j ≤ n then
    Real.sqrt ((Matrix.isHermitian_conjTranspose_mul_self A).eigenvalues₀
      ⟨j - 1, by obtain ⟨h1, h2⟩ := h; rw [Fintype.card_fin]; omega⟩)
  else 0

/-- HMT (thm:tail-spec-error-gauss). These are the hypotheses of thm:avg-frob-error-gauss:
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Ω`. In addition
`p ≥ 4`. Then for all `u, t ≥ 1`, the spectral-norm bound
`‖(I - P_Y)A‖ ≤ [(1 + t√(12k/p)) σ_{k+1} + t (e√(k+p)/(p+1)) (∑_{j>k} σ_j²)^{1/2}]
 + u t (e√(k+p)/(p+1)) σ_{k+1}`
fails with probability at most `5 t^{-p} + e^{-u²/2}`. -/
theorem tail_spec_error_gauss
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    {m n k p : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
    (hk : 2 ≤ k) (hp : 2 ≤ p) (hkp : k + p ≤ min m n)
    (Omega : Ω → Matrix (Fin n) (Fin (k + p)) ℝ)
    (hOmega : StandardGaussianTestMatrix P Omega)
    (hp4 : 4 ≤ p) :
    ∀ u t : ℝ, 1 ≤ u → 1 ≤ t →
      P {ω |
          ((1 + t * Real.sqrt (12 * (k : ℝ) / (p : ℝ))) * singularValue A (k + 1)
            + t * (Real.exp 1 * Real.sqrt ((k : ℝ) + (p : ℝ)) / ((p : ℝ) + 1))
                * Real.sqrt (∑ j ∈ Finset.Ioc k n, singularValue A j ^ 2))
            + u * t * (Real.exp 1 * Real.sqrt ((k : ℝ) + (p : ℝ)) / ((p : ℝ) + 1))
                * singularValue A (k + 1)
          < ‖(1 - orthogonalProjector (A * Omega ω)) * A‖}
        ≤ ENNReal.ofReal (5 * t ^ (-(p : ℝ)) + Real.exp (-u ^ 2 / 2)) := by
  sorry

end RNLAPhaseB.HMT2011TailSpecErrorGauss