theorem ChernoffBound.chernoff_bound_bounded_rv {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {n : ℕ} (hn : 0 < n) {X : ℕ → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (h_bounded : ∀ (i : ℕ), ∀ᵐ (ω : Ω) ∂μ, X i ω ∈ Set.Icc (-1) 1) (h_mean : ∀ (i : ℕ), ∫ (x : Ω), X i x ∂μ = 0) {t : ℝ} (ht : 0 < t) : μ.real {ω : Ω | t * √↑n ≤ ∑ i ∈ Finset.range n, X i ω} ≤ Real.exp (-t ^ 2 / 2)

Chernoff bound for bounded centred random variables. If $X_1, \dots, X_n$ are independent, mean-zero, and almost surely in $[-1,1]$, then $\Pr\!\left(\sum_{i<n} X_i \ge t\sqrt n\right) \le \exp(-t^2/2)$ for every $t>0$.

theorem ChernoffBound.chernoff_bernoulli_upper_tail {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {n : ℕ} (hn : 0 < n) {X : ℕ → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (h_bernoulli : ∀ (i : ℕ), ∀ᵐ (ω : Ω) ∂μ, X i ω ∈ {0, 1}) {t : ℝ} (ht : 0 < t) : μ.real {ω : Ω | ∑ i ∈ Finset.range n, ∫ (x : Ω), X i x ∂μ + t * √↑n ≤ ∑ i ∈ Finset.range n, X i ω} ≤ Real.exp (-t ^ 2 / 2)

Chernoff upper-tail bound for sums of independent Bernoulli random variables: with $\mu = \sum_i \mathbb{E}[X_i]$ and $t>0$, $\Pr\!\left(\sum_{i<n} X_i \ge \mu + t\sqrt n\right) \le \exp(-t^2/2)$.

theorem ChernoffBound.chernoff_bernoulli_lower_tail {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {n : ℕ} (hn : 0 < n) {X : ℕ → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (h_bernoulli : ∀ (i : ℕ), ∀ᵐ (ω : Ω) ∂μ, X i ω ∈ {0, 1}) {t : ℝ} (ht : 0 < t) : μ.real {ω : Ω | ∑ i ∈ Finset.range n, X i ω ≤ ∑ i ∈ Finset.range n, ∫ (x : Ω), X i x ∂μ - t * √↑n} ≤ Real.exp (-t ^ 2 / 2)

Chernoff lower-tail bound for sums of independent Bernoulli random variables: with $\mu = \sum_i \mathbb{E}[X_i]$ and $t>0$, $\Pr\!\left(\sum_{i<n} X_i \le \mu - t\sqrt n\right) \le \exp(-t^2/2)$.

theorem ChernoffBound.chernoff_bernoulli_tail {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {n : ℕ} (hn : 0 < n) {X : ℕ → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (h_bernoulli : ∀ (i : ℕ), ∀ᵐ (ω : Ω) ∂μ, X i ω ∈ {0, 1}) {t : ℝ} (ht : 0 < t) : μ.real {ω : Ω | ∑ i ∈ Finset.range n, ∫ (x : Ω), X i x ∂μ + t * √↑n ≤ ∑ i ∈ Finset.range n, X i ω} ≤ Real.exp (-t ^ 2 / 2) ∧ μ.real {ω : Ω | ∑ i ∈ Finset.range n, X i ω ≤ ∑ i ∈ Finset.range n, ∫ (x : Ω), X i x ∂μ - t * √↑n} ≤ Real.exp (-t ^ 2 / 2)

Two-sided Chernoff tail bound for sums of independent Bernoulli random variables, packaging the upper- and lower-tail inequalities together.