Singular values of an SRFT embedding

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

/-- The `i`-th singular value (1-based) of a complex matrix, computed from the matrix
as the spectral-norm distance to the matrices of rank `< i` (Eckart--Young). For
`i = 1` this is the spectral norm, and it is `0` for `i > min(m,p)` (zero padding). -/
noncomputable def singularValue {m p : ℕ} (A : Matrix (Fin m) (Fin p) ℂ) (i : ℕ) : ℝ :=
  ⨅ B : {B : Matrix (Fin m) (Fin p) ℂ // B.rank < i}, ‖A - B‖

/-- The `n × n` unitary discrete Fourier transform,
`F_{pq} = n^{-1/2} exp(-2πi (p-1)(q-1)/n)`, written with 0-based indices. -/
noncomputable def dftMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℂ :=
  fun p q => ((Real.sqrt n)⁻¹ : ℂ) *
    Complex.exp (-(2 * (Real.pi : ℂ) * Complex.I * ((p.val : ℂ) * (q.val : ℂ))) / (n : ℂ))

/-- The diagonal matrix `D` whose entries are the unit-modulus numbers `e^{iθ_j}`. -/
noncomputable def phaseDiagonal {n : ℕ} (θ : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℂ :=
  Matrix.diagonal fun j => Complex.exp ((θ j : ℂ) * Complex.I)

/-- The `n × ℓ` matrix `R` whose `j`-th column is the coordinate vector `e_{τ j}`. -/
def coordinateSampler {n ℓ : ℕ} (τ : Fin ℓ → Fin n) : Matrix (Fin n) (Fin ℓ) ℂ :=
  fun i j => if τ j = i then 1 else 0

/-- The SRFT matrix `Ω = sqrt(n/ℓ) · D F R`. -/
noncomputable def srftMatrix {n ℓ : ℕ} (θ : Fin n → ℝ) (τ : Fin ℓ → Fin n) :
    Matrix (Fin n) (Fin ℓ) ℂ :=
  ((Real.sqrt ((n : ℝ) / (ℓ : ℝ)) : ℝ) : ℂ) •
    (phaseDiagonal θ * dftMatrix n * coordinateSampler τ)

/-- The law of an `n × ℓ` SRFT draw: independent phases uniform on `[0, 2π)` (so each
`D_jj` is uniform on the complex unit circle), an ordered choice of `ℓ` distinct
coordinates drawn uniformly without replacement, independent of the phases. -/
structure SRFTLaw {Ω : Type*} [MeasurableSpace Ω] {n ℓ : ℕ} (P : Measure Ω)
    (θ : Ω → Fin n → ℝ) (τ : Ω → Fin ℓ → Fin n) : Prop where
  isProbabilityMeasure : IsProbabilityMeasure P
  phase_measurable : ∀ j, Measurable (fun ω => θ ω j)
  phase_uniform : ∀ j,
    MeasureTheory.pdf.IsUniform (fun ω => θ ω j) (Set.Ico (0 : ℝ) (2 * Real.pi)) P
  phases_iIndep : ProbabilityTheory.iIndepFun (fun j ω => θ ω j) P
  sampler_measurable : Measurable τ
  sampler_uniform : ∀ f : Fin ℓ → Fin n,
    P {ω | τ ω = f} =
      if Function.Injective f then ((n.descFactorial ℓ : ℝ≥0∞))⁻¹ else 0
  sampler_indep : ProbabilityTheory.IndepFun θ τ P

/-- HMT Theorem 11.1 (thm:srft-spec-bd). `O(k^{-1})` is read as one constant `C`
uniform over all admissible `n, k, ℓ, V` and draws. `log` is the natural logarithm.
`1 ≤ k` is the implicit range of the 1-based index in `σ_k`. -/
theorem srft_spectral_bounds :
    ∃ C : ℝ, 0 < C ∧
      ∀ (n k ℓ : ℕ), 1 ≤ k →
        4 * (Real.sqrt (k : ℝ) + Real.sqrt (8 * Real.log ((k : ℝ) * (n : ℝ)))) ^ 2
            * Real.log (k : ℝ) ≤ (ℓ : ℝ) →
        ℓ ≤ n →
        ∀ V : Matrix (Fin n) (Fin k) ℂ, Vᴴ * V = 1 →
        ∀ (Ω : Type) [MeasurableSpace Ω] (P : Measure Ω)
          (θ : Ω → Fin n → ℝ) (τ : Ω → Fin ℓ → Fin n),
          SRFTLaw P θ τ →
          P {ω | ¬ ((0.40 : ℝ) ≤ singularValue (Vᴴ * srftMatrix (θ ω) (τ ω)) k ∧
                    singularValue (Vᴴ * srftMatrix (θ ω) (τ ω)) 1 ≤ (1.48 : ℝ))}
            ≤ ENNReal.ofReal (C / (k : ℝ)) := by
  sorry

end RNLAPhaseB.HMT2011.SRFTSpecBd