English
If a collection of random variables X_i is sub-Gaussian with parameters c_i and the X_i are independent in an iIndepFun sense, then the right tail of the sum ∑ X_i is bounded by a Chernoff-type bound exp(-ε^2/(2∑ c_i)).
Русский
Если набор случайных величин X_i субгауссов, параметры c_i, и X_i независимы, то правая сторона хвоста суммы имеет границу типа Чернова.
LaTeX
$$$\mathrm{measure}(\{\omega : \varepsilon \le \sum_{i\in s} X_i(\omega)\}) \le \exp\left(-\frac{\varepsilon^2}{2\sum_{i\in s} c_i}\right)$$$
Lean4
theorem sum_of_iIndepFun {ι : Type*} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {c : ι → ℝ≥0} {s : Finset ι}
(h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ) : HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ :=
by
have : HasSubgaussianMGF (fun ω ↦ ∑ (i : s), X i ω) (∑ (i : s), c i) μ :=
by
apply sum_of_iIndepFun_of_forall_aemeasurable
· exact h_indep.precomp Subtype.val_injective
· exact fun i ↦ (h_subG i i.2).aemeasurable
· exact fun i _ ↦ h_subG i i.2
rw [Finset.sum_coe_sort] at this
exact this.congr (ae_of_all _ fun ω ↦ Finset.sum_attach s (fun i ↦ X i ω))
