Approximation error of an SRFT rangefinder

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal

namespace RNLAPhaseB.HMT2011SRFT

/-- Discrete measurable structure on the finite type of ordered column selections. -/
instance instMeasurableSpaceFinEmbedding (l n : ℕ) : MeasurableSpace (Fin l ↪ Fin n) := ⊤

/-- Uniform distribution on the complex unit circle: the image of the uniform law on
`[0, 2π)` under `θ ↦ e^{iθ}`. -/
noncomputable def uniformUnitCircle : Measure ℂ :=
  Measure.map (fun θ : ℝ => Complex.exp ((θ : ℂ) * Complex.I))
    ((ENNReal.ofReal (2 * Real.pi))⁻¹ • (volume.restrict (Set.Ico (0 : ℝ) (2 * Real.pi))))

/-- The `n × n` unitary DFT, `f_pq = n^{-1/2} e^{-2πi(p-1)(q-1)/n}` (0-based indices here). -/
noncomputable def dftMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℂ :=
  fun p q => (((Real.sqrt (n : ℝ))⁻¹ : ℝ) : ℂ) *
    Complex.exp (-(2 * (Real.pi : ℂ) * Complex.I * ((p : ℕ) : ℂ) * ((q : ℕ) : ℂ)) / (n : ℂ))

/-- `R`: the `n × ℓ` matrix whose `j`th column is the `s(j)`th column of the identity. -/
def coordinateSampler {n ℓ : ℕ} (s : Fin ℓ ↪ Fin n) : Matrix (Fin n) (Fin ℓ) ℂ :=
  fun i j => if i = s j then 1 else 0

/-- The SRFT `Ω = sqrt(n/ℓ) · D F R` built from the diagonal of `D` and the selection `R`. -/
noncomputable def srftMatrix {n ℓ : ℕ} (d : Fin n → ℂ) (s : Fin ℓ ↪ Fin n) :
    Matrix (Fin n) (Fin ℓ) ℂ :=
  ((Real.sqrt ((n : ℝ) / (ℓ : ℝ)) : ℝ) : ℂ) •
    (Matrix.diagonal d * dftMatrix n * coordinateSampler s)

/-- Law of an SRFT draw: the diagonal entries of `D` are independent and uniform on the
complex unit circle; the `ℓ` columns of `R` are drawn uniformly at random without
replacement from the columns of the identity (uniform ordered injection), independently of `D`. -/
structure SRFTDraw {Ω : Type*} [MeasurableSpace Ω] {n ℓ : ℕ} (P : Measure Ω)
    (d : Ω → Fin n → ℂ) (s : Ω → (Fin ℓ ↪ Fin n)) : Prop where
  isProbabilityMeasure : IsProbabilityMeasure P
  diag_hasLaw : ∀ i, ProbabilityTheory.HasLaw (fun ω => d ω i) uniformUnitCircle P
  diag_iIndep : ProbabilityTheory.iIndepFun (fun i ω => d ω i) P
  sampler_measurable : Measurable s
  sampler_uniform : ∀ e : Fin ℓ ↪ Fin n,
    P {ω | s ω = e} = ((Fintype.card (Fin ℓ ↪ Fin n) : ℝ≥0∞))⁻¹
  diag_indep_sampler : ProbabilityTheory.IndepFun d s P

/-- Singular values of `A`, 1-based, in nonincreasing order, zero-padded: `σ_j` is the square
root of the `j`th largest eigenvalue of `Aᴴ A` (and `0` for `j = 0` or `j > n`). -/
noncomputable def singularValue {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℂ) (j : ℕ) : ℝ :=
  let ev := (Matrix.isHermitian_conjTranspose_mul_self A).eigenvalues
  let l : List ℝ := (((Finset.univ : Finset (Fin n)).val.map ev).toList).mergeSort
    (fun a b => decide (b ≤ a))
  if 1 ≤ j then Real.sqrt (l.getD (j - 1) 0) else 0

/-- Frobenius norm. -/
noncomputable def frobNorm {m n : ℕ} (M : Matrix (Fin m) (Fin n) ℂ) : ℝ :=
  Real.sqrt (∑ i, ∑ j, ‖M i j‖ ^ 2)

/-- HMT Theorem 11.2 (thm:SRFT). `O(k^{-1})` is read as one constant `C`, uniform over all
dimensions, matrices and admissible `ℓ`; `log` is the natural logarithm. -/
theorem srft_rangefinder_bound :
    ∃ C : ℝ, ∀ {Ω : Type} [MeasurableSpace Ω] (P : Measure Ω) (m n k ℓ : ℕ)
      (A : Matrix (Fin m) (Fin n) ℂ) (d : Ω → Fin n → ℂ) (s : Ω → (Fin ℓ ↪ Fin n)),
      SRFTDraw P d s → 1 ≤ k →
      4 * (Real.sqrt (k : ℝ) + Real.sqrt (8 * Real.log ((k : ℝ) * (n : ℝ)))) ^ 2 *
          Real.log (k : ℝ) ≤ (ℓ : ℝ) →
      ℓ ≤ n →
      P {ω | ¬ (
          ‖(1 - orthogonalProjector (A * srftMatrix (d ω) (s ω))) * A‖ ≤
              Real.sqrt (1 + 7 * (n : ℝ) / (ℓ : ℝ)) * singularValue A (k + 1) ∧
          frobNorm ((1 - orthogonalProjector (A * srftMatrix (d ω) (s ω))) * A) ≤
              Real.sqrt (1 + 7 * (n : ℝ) / (ℓ : ℝ)) *
                Real.sqrt (∑ j ∈ Finset.Ioc k n, singularValue A j ^ 2))}
        ≤ ENNReal.ofReal (C / (k : ℝ)) := by
  sorry

end RNLAPhaseB.HMT2011SRFT