def RudelsonVershynin.vecOuterProduct {n : ℕ} (v : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

noncomputable def RudelsonVershynin.euclideanNorm {n : ℕ} (v : Fin n → ℝ) : ℝ

theorem RudelsonVershynin.rv_theorem (n : ℕ) (hn : 0 < n) {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → Fin n → ℝ) (hY_meas : Measurable Y) (t : ℝ) (ht : 0 < t) (hY_bound : ∀ᵐ (ω : Ω) ∂μ, euclideanNorm (Y ω) ≤ t) (hY_cov : ‖∫ (ω : Ω), vecOuterProduct (Y ω) ∂μ‖ ≤ 1) (q : ℕ) (hq : 1 < q) {Ω' : Type u_2} [MeasurableSpace Ω'] (ν : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure ν] (Ys : Fin q → Ω' → Fin n → ℝ) (hYs_iid : ∀ (i : Fin q), MeasureTheory.Measure.map (Ys i) ν = MeasureTheory.Measure.map Y μ) (hYs_indep : ProbabilityTheory.iIndepFun Ys ν) : ∃ (k : ℝ), 0 < k ∧ ∫ (ω' : Ω'), ‖∫ (ω : Ω), vecOuterProduct (Y ω) ∂μ - (1 / ↑q) • ∑ i : Fin q, vecOuterProduct (Ys i ω')‖ ∂ν ≤ k * t * √(Real.log ↑q / ↑q)