theorem theorem_1_6_subgaussian_vector {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} {σsq : ℝ} (hX_sg : ∀ (i : Fin n), IsSubGaussian (X i) σsq μ) (hX_indep : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (i : Fin n), Measurable (X i)) (a : Fin n → ℝ) : IsSubGaussian (fun (ω : Ω) => ∑ i : Fin n, a i * X i ω) (σsq * ∑ i : Fin n, a i ^ 2) μ

Theorem 1.6