def ChernoffBound.IsBernoulliRV {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : Ω → ℝ) (p : ℝ) (μ : MeasureTheory.Measure Ω) : Prop

IsBernoulliRV X p μ says that under measure μ, the random variable X is almost surely $\{0,1\}$-valued, takes the value $1$ with probability $p$, and $p \in [0,1]$.

theorem ChernoffBound.chernoff_upper_tail_sharp {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ_meas : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ_meas] {ι : Type u_2} [Fintype ι] (X : ι → Ω → ℝ) (p : ι → ℝ) (hBernoulli : ∀ (i : ι), IsBernoulliRV (X i) (p i) μ_meas) (hIndep : ProbabilityTheory.iIndepFun X μ_meas) (hMeas : ∀ (i : ι), Measurable (X i)) (μ_val : ℝ) (hμ : μ_val = ∑ i : ι, p i) (hμ_pos : 0 < μ_val) (ε : ℝ) (hε : 0 < ε) : μ_meas {ω : Ω | ∑ i : ι, X i ω ≥ (1 + ε) * μ_val} ≤ ENNReal.ofReal (Real.exp (-((1 + ε) * Real.log (1 + ε) - ε) * μ_val))

Sharp Chernoff upper-tail bound (Theorem 5.0.5). For independent Bernoullis $X_i$ with mean $\mu = \sum_i p_i > 0$ and $\varepsilon > 0$, $\Pr\!\left(\sum_i X_i \ge (1+\varepsilon)\mu\right) \le \exp(-((1+\varepsilon)\log(1+\varepsilon) - \varepsilon)\mu)$.

theorem ChernoffBound.chernoff_upper_tail_weak {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ_meas : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ_meas] {ι : Type u_2} [Fintype ι] (X : ι → Ω → ℝ) (p : ι → ℝ) (hBernoulli : ∀ (i : ι), IsBernoulliRV (X i) (p i) μ_meas) (hIndep : ProbabilityTheory.iIndepFun X μ_meas) (hMeas : ∀ (i : ι), Measurable (X i)) (μ_val : ℝ) (hμ : μ_val = ∑ i : ι, p i) (hμ_pos : 0 < μ_val) (ε : ℝ) (hε : 0 < ε) : μ_meas {ω : Ω | ∑ i : ι, X i ω ≥ (1 + ε) * μ_val} ≤ ENNReal.ofReal (Real.exp (-(ε ^ 2 / (1 + ε)) * μ_val))

Weak Chernoff upper-tail bound (Theorem 5.0.6 / Corollary 5.0.3). For independent Bernoullis $X_i$ with mean $\mu > 0$ and $\varepsilon > 0$, $\Pr\!\left(\sum_i X_i \ge (1+\varepsilon)\mu\right) \le \exp\!\left(-\dfrac{\varepsilon^2}{1+\varepsilon}\,\mu\right)$.

theorem ChernoffBound.chernoff_lower_tail {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ_meas : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ_meas] {ι : Type u_2} [Fintype ι] (X : ι → Ω → ℝ) (p : ι → ℝ) (hBernoulli : ∀ (i : ι), IsBernoulliRV (X i) (p i) μ_meas) (hIndep : ProbabilityTheory.iIndepFun X μ_meas) (hMeas : ∀ (i : ι), Measurable (X i)) (μ_val : ℝ) (hμ : μ_val = ∑ i : ι, p i) (hμ_pos : 0 < μ_val) (ε : ℝ) (hε : 0 < ε) : μ_meas {ω : Ω | ∑ i : ι, X i ω ≤ (1 - ε) * μ_val} ≤ ENNReal.ofReal (Real.exp (-(ε ^ 2 * μ_val / 2)))

Chernoff lower-tail bound (Theorem 5.0.7). For independent Bernoullis $X_i$ with mean $\mu > 0$ and $\varepsilon > 0$, $\Pr\!\left(\sum_i X_i \le (1-\varepsilon)\mu\right) \le \exp(-\varepsilon^2 \mu / 2)$.

theorem ChernoffBound.chernoff_upper_exponent_ineq (ε : ℝ) (hε : 0 < ε) : ε ^ 2 / (1 + ε) ≤ (1 + ε) * Real.log (1 + ε) - ε

Elementary inequality underlying the weakening from sharp to weak Chernoff: $\dfrac{\varepsilon^2}{1+\varepsilon} \le (1+\varepsilon)\log(1+\varepsilon) - \varepsilon$ for all $\varepsilon > 0$.