Restricted singular values of Gaussian matrices

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

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

namespace RNLAPhaseB.MT2020RsvGauss

/-- The unit sphere `𝕊^{n-1}(ℝ)` in `ℝ^n`, with the Euclidean norm. -/
def unitSphere (n : ℕ) : Set (Fin n → ℝ) :=
  {x | l2Norm x = 1}

/-- Minimum restricted singular value `σ_min(S; E) := min_{x ∈ E} ‖S x‖`
(eqn:rsv), realized as an infimum over `E`. It is only used for nonempty `E`. -/
noncomputable def sigmaMinRestricted {d n : ℕ} (S : Matrix (Fin d) (Fin n) ℝ)
    (E : Set (Fin n → ℝ)) : ℝ :=
  ⨅ x : E, l2Norm (S *ᵥ (x : Fin n → ℝ))

/-- Maximum restricted singular value `σ_max(S; E) := max_{x ∈ E} ‖S x‖`
(eqn:rsv), realized as a supremum over `E`. It is only used for nonempty `E`. -/
noncomputable def sigmaMaxRestricted {d n : ℕ} (S : Matrix (Fin d) (Fin n) ℝ)
    (E : Set (Fin n → ℝ)) : ℝ :=
  ⨆ x : E, l2Norm (S *ᵥ (x : Fin n → ℝ))

/-- Gaussian width `w(E) := 𝔼 sup_{x ∈ E} ⟨g, x⟩`, where `g ∈ ℝ^n` is standard
normal (iid `N(0,1)` coordinates, i.e. the product of standard real Gaussians). -/
noncomputable def gaussianWidth {n : ℕ} (E : Set (Fin n → ℝ)) : ℝ :=
  ∫ g, (⨆ x : E, ∑ i, g i * (x : Fin n → ℝ) i)
    ∂(Measure.pi (fun _ : Fin n => ProbabilityTheory.gaussianReal 0 1))

/-- A random `d × n` real matrix whose entries are iid `normal(0, v)`: every entry
has law `gaussianReal 0 v` and the family of all entries is mutually independent. -/
structure IidNormalEntries {Ω : Type*} [MeasurableSpace Ω] {d n : ℕ}
    (P : Measure Ω) (Γ : Ω → Matrix (Fin d) (Fin n) ℝ) (v : NNReal) : Prop where
  entry_hasLaw : ∀ i j,
    ProbabilityTheory.HasLaw (fun ω => Γ ω i j) (ProbabilityTheory.gaussianReal 0 v) P
  entries_iIndep :
    ProbabilityTheory.iIndepFun (fun p : Fin d × Fin n => fun ω => Γ ω p.1 p.2) P

/-- mt2020 thm:rsv-gauss. For a fixed nonempty subset `E` of the unit sphere and a
Gaussian matrix `Γ ∈ ℝ^{d×n}` with iid `normal(0, d⁻¹)` entries, for all `t > 0`,
`P{σ_min(Γ;E) ≤ 1 - (w(E)+1)/√d - t} ≤ e^{-dt²/2}` and
`P{σ_max(Γ;E) ≥ 1 + w(E)/√d + t} ≤ e^{-dt²/2}`.

The hypothesis `E.Nonempty` is the definitional precondition of
`σ_min(S;E) = min_{x∈E} ‖Sx‖`, `σ_max(S;E) = max_{x∈E} ‖Sx‖` and
`w(E) = 𝔼 sup_{x∈E} ⟨g,x⟩`, which are undefined for `E = ∅`. -/
theorem rsv_gauss {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    [IsProbabilityMeasure P] (d n : ℕ)
    (E : Set (Fin n → ℝ)) (hE : E ⊆ unitSphere n) (hEne : E.Nonempty)
    (Γ : Ω → Matrix (Fin d) (Fin n) ℝ)
    (hΓ : IidNormalEntries P Γ ((d : NNReal)⁻¹)) :
    ∀ t : ℝ, 0 < t →
      P {ω | sigmaMinRestricted (Γ ω) E
          ≤ 1 - (gaussianWidth E + 1) / Real.sqrt d - t}
        ≤ ENNReal.ofReal (Real.exp (-(d : ℝ) * t ^ 2 / 2)) ∧
      P {ω | 1 + gaussianWidth E / Real.sqrt d + t
          ≤ sigmaMaxRestricted (Γ ω) E}
        ≤ ENNReal.ofReal (Real.exp (-(d : ℝ) * t ^ 2 / 2)) := by
  sorry

end RNLAPhaseB.MT2020RsvGauss