theorem ChernoffBound.chernoff_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n) {X : Fin n → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : Fin n), AEMeasurable (X i) μ) (h_bdd : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, X i ω ∈ Set.Icc (-1) 1) (h_mean : ∀ (i : Fin n), ∫ (x : Ω), X i x ∂μ = 0) {a : ℝ} (ha : 0 < a) : μ.real {ω : Ω | a * √↑n ≤ ∑ i : Fin n, X i ω} ≤ Real.exp (-a ^ 2 / 2)

Chernoff bound (Theorem 5.0.5). For independent random variables $X_1, \dots, X_n$ with $X_i \in [-1,1]$ and $\mathbb{E}[X_i] = 0$, the one-sided tail bound $\mathbb{P}\!\left(\sum_i X_i \geq a\sqrt{n}\right) \leq e^{-a^2/2}$ holds for any $a > 0$.

theorem ChernoffBound.chernoff_bound_two_sided {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n) {X : Fin n → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : Fin n), AEMeasurable (X i) μ) (h_bdd : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, X i ω ∈ Set.Icc (-1) 1) (h_mean : ∀ (i : Fin n), ∫ (x : Ω), X i x ∂μ = 0) {a : ℝ} (ha : 0 < a) : μ.real {ω : Ω | a * √↑n ≤ |∑ i : Fin n, X i ω|} ≤ 2 * Real.exp (-a ^ 2 / 2)

Two-sided Chernoff bound (Corollary 5.0.6). For independent random variables $X_1, \dots, X_n$ with $X_i \in [-1,1]$ and $\mathbb{E}[X_i] = 0$, $\mathbb{P}\!\left(\left|\sum_i X_i\right| \geq a\sqrt{n}\right) \leq 2e^{-a^2/2}$ for any $a > 0$.