Frobenius 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.HMT2011TailFrobErrorGauss

/-- Frobenius norm of a real rectangular matrix, written out explicitly:
`‖M‖_F = (∑_{i,j} M_{ij}^2)^{1/2}`. -/
noncomputable def frobNorm {a b : ℕ} (M : Matrix (Fin a) (Fin b) ℝ) : ℝ :=
  Real.sqrt (∑ i, ∑ j, M i j ^ 2)

/-- The `j`-th largest value (1-based, counted with multiplicity) of a finite
family `f`: the supremum of the thresholds `x` exceeded-or-met by at least `j`
entries. For `j > d` the set is empty and Lean's `sSup ∅ = 0` gives zero padding. -/
noncomputable def kthLargest {d : ℕ} (f : Fin d → ℝ) (j : ℕ) : ℝ := by
  classical
  exact sSup {x : ℝ | j ≤ (Finset.univ.filter (fun i => x ≤ f i)).card}

/-- The `j`-th singular value `σ_j` (1-based) of a real `m × n` matrix `A`,
derived from `A`: the square root of the `j`-th largest eigenvalue of `Aᴴ A`
(`= Aᵀ A` over ℝ), with `σ_j = 0` for `j > n` (zero padding). -/
noncomputable def singularValue {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (j : ℕ) : ℝ :=
  Real.sqrt (kthLargest (Matrix.isHermitian_conjTranspose_mul_self A).eigenvalues j)

/-- The tail sum `∑_{j>k} σ_j^2`; all singular values with index `> n` vanish,
so the sum over `j ∈ (k, n]` is the full tail. -/
noncomputable def tailSqSum {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (k : ℕ) : ℝ :=
  ∑ j ∈ Finset.Ioc k n, singularValue A j ^ 2

/-- HMT 2011, Theorem thm:tail-frob-error-gauss.

Hypotheses of thm:avg-frob-error-gauss:
* `A` is a real `m × n` matrix with singular values `σ_1 ≥ σ_2 ≥ …`.
* The target rank is `k ≥ 2` and the oversampling is `p ≥ 2`, with `k + p ≤ min {m, n}`.
* `Ω` is an `n × (k+p)` standard Gaussian matrix and `Y = AΩ`.

Additionally `p ≥ 4`.

For all `u, t ≥ 1`, the bound
`‖(I - P_Y)A‖_F ≤ (1 + t√(12k/p)) (∑_{j>k} σ_j²)^{1/2} + u t e√(k+p)/(p+1) σ_{k+1}`
fails with probability at most `5 t^{-p} + 2 e^{-u^2/2}`.

The failure event is the strict reverse inequality. The exponent `-u^2/2` is
written `-(u ^ 2 / 2)`. -/
theorem tail_frob_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) (hp4 : 4 ≤ p)
    (G : Ωs → Matrix (Fin n) (Fin (k + p)) ℝ)
    (hG : RNLAPhaseB.StandardGaussianTestMatrix P G) :
    ∀ u t : ℝ, 1 ≤ u → 1 ≤ t →
      P {ω | (1 + t * Real.sqrt (12 * (k : ℝ) / (p : ℝ))) * Real.sqrt (tailSqSum A k)
                + u * t * (Real.exp 1 * Real.sqrt ((k : ℝ) + (p : ℝ)) / ((p : ℝ) + 1))
                    * singularValue A (k + 1)
              < frobNorm ((1 - orthogonalProjector (A * G ω)) * A)}
        ≤ ENNReal.ofReal (5 * (t ^ p)⁻¹ + 2 * Real.exp (-(u ^ 2 / 2))) := by
  sorry

end RNLAPhaseB.HMT2011TailFrobErrorGauss