English
If X has a subgaussian MGF with parameter c relative to a kernel κ and ν, then for any nonnegative ε, the probability that X exceeds ε under κ(ω') is at most exp(-ε^2/(2c)) for ν-almost every ω'.
Русский
Если X имеет субгауссов MGФ с параметром c относительно ядра κ и меры ν, то для любого ε ≥ 0 вероятность того, что X превысит ε под распределением κ(ω'), не более exp(-ε^2/(2c)) для ν-почти каждого ω'.
LaTeX
$$$\forall ε \ge 0:\ ∀^{⋄} ω' \partial ν:\ (κ(ω'))\{ω : ε ≤ X(ω)\} ≤ \exp(-ε^2/(2c))$$$
Lean4
/-- Chernoff bound on the right tail of a sub-Gaussian random variable. -/
theorem measure_ge_le (h : HasSubgaussianMGF X c κ ν) {ε : ℝ} (hε : 0 ≤ ε) :
∀ᵐ ω' ∂ν, (κ ω').real {ω | ε ≤ X ω} ≤ exp (-ε ^ 2 / (2 * c)) :=
by
by_cases hc0 : c = 0
· filter_upwards [h.measure_univ_le_one] with ω' h
simp only [hc0, NNReal.coe_zero, mul_zero, div_zero, exp_zero]
refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_
simp only [ENNReal.ofReal_one]
exact (measure_mono (Set.subset_univ _)).trans h
filter_upwards [measure_ge_le_exp_add h ε] with ω' h
calc
(κ ω').real
{ω | ε ≤ X ω}
-- choose the minimizer of the r.h.s. of `h` for `t ≥ 0`. That is, `t = ε / c`.
_ ≤ exp (-(ε / c) * ε + c * (ε / c) ^ 2 / 2) := (h (ε / c) (by positivity))
_ = exp (-ε ^ 2 / (2 * c)) := by congr; field_simp; ring
