theorem
SubGaussian.lemma_1_3_upper_tail
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : Ω → ℝ}
{σsq : ℝ}
(hX : IsSubGaussian X σsq μ)
(t : ℝ)
(ht : 0 < t)
:
Upper tail bound for sub-Gaussian random variables (Lemma 1.3). For X ~ subG(σ²) and t > 0, P(X > t) ≤ exp(-t²/(2σ²)). The proof uses the Chernoff bound with the optimal choice s = t/σ².
theorem
SubGaussian.lemma_1_3_lower_tail
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : Ω → ℝ}
{σsq : ℝ}
(hX : IsSubGaussian X σsq μ)
(t : ℝ)
(ht : 0 < t)
:
Lower tail bound for sub-Gaussian random variables (Lemma 1.3). For X ~ subG(σ²) and t > 0, P(X < -t) ≤ exp(-t²/(2σ²)). The proof uses the lower Chernoff bound with s = -(t/σ²).
theorem
SubGaussian.subGaussian_tail_bounds
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{X : Ω → ℝ}
{σsq : ℝ}
(hX : IsSubGaussian X σsq μ)
(t : ℝ)
(ht : 0 < t)
:
Lemma 1.3: Sub-Gaussian tail bounds. For X ~ subG(σ²) and t > 0, both P(X > t) ≤ exp(-t²/(2σ²)) and P(X < -t) ≤ exp(-t²/(2σ²)) hold.