Concentration of a sampled second-moment matrix

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

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

namespace RNLAPhaseB.DM2017.Oliveira

/-- The second-moment matrix `E[x xᵀ]` of a `d`-dimensional random vector `x`,
written entrywise as `(E[x xᵀ])_{jk} = E[x_j x_k]`. -/
noncomputable def secondMomentMatrix {Ω : Type*} [MeasurableSpace Ω] {d : ℕ}
    (P : Measure Ω) (x : Ω → Fin d → ℝ) : Matrix (Fin d) (Fin d) ℝ :=
  fun j k => ∫ ω, x ω j * x ω k ∂P

/-- Lemma (Oliveira), dm2017 `lem:oliveira`.
Let `x^1, …, x^c` be i.i.d. copies of a `d`-dimensional random vector `x` with
`‖x‖₂ ≤ M` and `‖E[x xᵀ]‖₂ ≤ 1`. Then for any `α > 0`,
`‖(1/c) ∑ᵢ xⁱ xⁱᵀ − E[x xᵀ]‖₂ ≤ α` holds with probability at least
`1 − (2c²) exp(−c α² / (16 M² + 8 M² α))`.
The matrix norm is the spectral (ℓ₂ operator) norm, via the scoped instance
`Matrix.Norms.L2Operator`; the vector norm is the Euclidean norm `l2Norm`.
The copies are indexed by `Fin c` (i.e. `x^1,…,x^c` shifted to `0,…,c-1`). -/
theorem oliveira_sample_covariance
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (d c : ℕ) (hc : 0 < c) (M : ℝ)
    (x : Ω → Fin d → ℝ) (X : Fin c → Ω → Fin d → ℝ)
    (hindep : ProbabilityTheory.iIndepFun X P)
    (hident : ∀ i, ProbabilityTheory.IdentDistrib (X i) x P P)
    (hnorm : ∀ ω, l2Norm (x ω) ≤ M)
    (hmoment : ‖secondMomentMatrix P x‖ ≤ 1)
    (α : ℝ) (hα : 0 < α) :
    ENNReal.ofReal
        (1 - (2 * (c : ℝ) ^ 2) *
          Real.exp (-((c : ℝ) * α ^ 2) / (16 * M ^ 2 + 8 * M ^ 2 * α)))
      ≤ P {ω | ‖(1 / (c : ℝ)) • (∑ i : Fin c, Matrix.vecMulVec (X i ω) (X i ω))
                - secondMomentMatrix P x‖ ≤ α} := by
  sorry

end RNLAPhaseB.DM2017.Oliveira