theorem corollary_1_7_upper_tail {Ω : 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 → ℝ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | ∑ i : Fin n, a i * X i ω > t} ≤ ENNReal.ofReal (Real.exp (-(t ^ 2 / (2 * σsq * ∑ i : Fin n, a i ^ 2))))

Corollary 1.7 — Upper tail bound for linear combinations. For independent sub-Gaussian random variables Xᵢ ~ subG(σ²) and any a : Fin n → ℝ, P[∑ᵢ aᵢXᵢ > t] ≤ exp(-t²/(2σ²·∑ᵢ aᵢ²)).

theorem corollary_1_7_lower_tail {Ω : 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 → ℝ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | ∑ i : Fin n, a i * X i ω < -t} ≤ ENNReal.ofReal (Real.exp (-(t ^ 2 / (2 * σsq * ∑ i : Fin n, a i ^ 2))))

Corollary 1.7 — Lower tail bound for linear combinations. For independent sub-Gaussian random variables Xᵢ ~ subG(σ²) and any a : Fin n → ℝ, P[∑ᵢ aᵢXᵢ < -t] ≤ exp(-t²/(2σ²·∑ᵢ aᵢ²)).

theorem corollary_1_7_linear_combination_tail {Ω : 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 → ℝ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | ∑ i : Fin n, a i * X i ω > t} ≤ ENNReal.ofReal (Real.exp (-(t ^ 2 / (2 * σsq * ∑ i : Fin n, a i ^ 2)))) ∧ μ {ω : Ω | ∑ i : Fin n, a i * X i ω < -t} ≤ ENNReal.ofReal (Real.exp (-(t ^ 2 / (2 * σsq * ∑ i : Fin n, a i ^ 2))))

Corollary 1.7 — Combined tail bound for linear combinations. For independent sub-Gaussian random variables Xᵢ ~ subG(σ²), any a : Fin n → ℝ, and t > 0, both tails satisfy exp(-t²/(2σ²·‖a‖₂²)).