English
Azuma-Hoeffding type bound: if Y_i are conditionally sub-Gaussian with parameters cY_i relative to a filtration and the base process is adapted, then the sum has a bound exp(-ε^2/(2∑ cY_i)).
Русский
Тип bound Азумы–Хоэффдинга: если Y_i условно субгауссовы с параметрами cY_i относительно фильтрации и база адаптивна, то сумма имеет bound.
LaTeX
$$$\mathrm{HasSubgaussianMGF}(\{Y_i\},\{c_{Y,i}\},\mu) \Rightarrow \mu\text{ real bound} \le \exp\left(-\frac{\varepsilon^2}{2\sum_{i< n} c_{Y,i}}\right)$$$
Lean4
/-- **Hoeffding inequality** for sub-Gaussian random variables. -/
theorem measure_sum_range_ge_le_of_iIndepFun {X : ℕ → Ω → ℝ} (h_indep : iIndepFun X μ) {c : ℝ≥0} {n : ℕ}
(h_subG : ∀ i < n, HasSubgaussianMGF (X i) c μ) {ε : ℝ} (hε : 0 ≤ ε) :
μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤ exp (-ε ^ 2 / (2 * n * c)) :=
by
have h := (sum_of_iIndepFun h_indep (c := fun _ ↦ c) (s := Finset.range n) (by simpa)).measure_ge_le hε
simpa [← mul_assoc] using h
