Theorem 1.6: Sub-Gaussian tail bound (linear combinations preserve sub-Gaussianity)

@[reducible, inline]

abbrev thm_1_6 {Ω : 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 (Sub-Gaussian random vectors): A linear combination of independent sub-Gaussian random variables is sub-Gaussian with variance proxy σ²‖a‖².

Corollary 1.7: Sub-Gaussian tail bound, symmetric form

@[reducible, inline]

abbrev cor_1_7_upper {Ω : 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): For independent sub-Gaussian Xᵢ ~ subG(σ²) and any a, P[∑ᵢ aᵢXᵢ > t] ≤ exp(-t²/(2σ²‖a‖₂²)).

@[reducible, inline]

abbrev cor_1_7_lower {Ω : 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): For independent sub-Gaussian Xᵢ ~ subG(σ²) and any a, P[∑ᵢ aᵢXᵢ < -t] ≤ exp(-t²/(2σ²‖a‖₂²)).

@[reducible, inline]

abbrev cor_1_7 {Ω : 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): Both upper and lower tail bounds for linear combinations.

Lemma 1.8: Hoeffding's lemma

@[reducible, inline]

abbrev lemma_1_8_mgf {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {a b : ℝ} (hab : a < b) (hXm : Measurable X) (hXa : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω) (hXb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) (hmean : ∫ (ω : Ω), X ω ∂μ = 0) (s : ℝ) : ∫ (ω : Ω), Real.exp (s * X ω) ∂μ ≤ Real.exp (s ^ 2 * (b - a) ^ 2 / 8)

Lemma 1.8 (Hoeffding's Lemma — MGF bound): If X has mean zero and X ∈ [a, b] a.s., then E[exp(sX)] ≤ exp(s²(b-a)²/8).

@[reducible, inline]

abbrev lemma_1_8 {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {a b : ℝ} (hab : a < b) (hXm : Measurable X) (hXi : MeasureTheory.Integrable X μ) (hXa : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω) (hXb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) (hmean : ∫ (ω : Ω), X ω ∂μ = 0) : IsSubGaussian X ((b - a) ^ 2 / 4) μ

Lemma 1.8 (Hoeffding's Lemma — sub-Gaussian): If X has mean zero and X ∈ [a, b] a.s., then X is sub-Gaussian with variance proxy (b-a)²/4.

Definition 1.11: Sub-exponential random variable

theorem def_1_11_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → ℝ) (lambda : ℝ) : IsSubExponential X lambda ↔ 0 < lambda ∧ MeasureTheory.Integrable X μ ∧ ∫ (ω : Ω), X ω ∂μ = 0 ∧ ∀ (s : ℝ), |s| ≤ 1 / lambda → ∫ (ω : Ω), Real.exp (s * X ω) ∂μ ≤ Real.exp (s ^ 2 * lambda ^ 2 / 2)

Definition 1.11: A random variable is sub-exponential with parameter λ if its MGF satisfies E[exp(sX)] ≤ exp(s²λ²/2) for all |s| ≤ 1/λ. See IsSubExponential.