Hoeffding's inequality for the biased binomial distribution

For a Bernoulli trial with parameter p ∈ [0, 1], the centered moment generating function (1 - p) exp (-s p) + p exp (s (1 - p)) is bounded above by exp (s² / 8) for every s : ℝ (Cslib.one_sub_mul_exp_add_mul_exp_le). Raising this bound to the Q-th power via the binomial theorem (Cslib.sum_choose_mul_pow_mul_exp) and optimizing the Chernoff parameter at s = 4 t / Q gives one-sided (Cslib.sum_filter_le_sub_choose_mul_pow_le, Cslib.sum_filter_le_mul_sub_choose_mul_pow_le) and two-sided (Cslib.sum_filter_le_abs_sub_choose_mul_pow_le) Hoeffding tail bounds for Bin(Q, p), together with the interval-complement form (Cslib.sum_filter_notMem_choose_mul_pow_le) used in Lemma 4.8 of [OpenAI2026ETH] at p = (r - 1) / (2 r). All tail inequalities hold for every Q : ℕ, including Q = 0.

For the unbiased case p = 1 / 2 in counting form on ι → Bool, see Cslib.BitString.card_filter_le_abs_card_filter_sub_half_le.

Main results

• Cslib.one_sub_mul_exp_add_mul_exp_le: Hoeffding's lemma for a biased Bernoulli trial.
• Cslib.sum_choose_mul_pow_eq_one: binomial probability weights sum to 1.
• Cslib.sum_choose_mul_pow_mul_exp: centered moment generating function of Bin(Q, p).
• Cslib.sum_filter_le_sub_choose_mul_pow_le: upper-tail Hoeffding bound for Bin(Q, p).
• Cslib.sum_filter_le_mul_sub_choose_mul_pow_le: lower-tail Hoeffding bound for Bin(Q, p).
• Cslib.sum_filter_le_abs_sub_choose_mul_pow_le: two-sided Hoeffding bound for Bin(Q, p).
• Cslib.sum_filter_notMem_choose_mul_pow_le: tail bound outside a subset covering [Q p - t, Q p + t].

References

• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables
• OpenAI, The Exponential Time Hypothesis is False, Section 4.7, Lemma 4.8, pp. 34–35.

theorem Cslib.one_sub_mul_exp_add_mul_exp_le {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) (s : ℝ) : (1 - p) * Real.exp (-s * p) + p * Real.exp (s * (1 - p)) ≤ Real.exp (s ^ 2 / 8)

Hoeffding's lemma for a biased Bernoulli trial [Hoeffding1963]: for p ∈ [0, 1] and s : ℝ, the centered moment generating function (1 - p) exp (-s p) + p exp (s (1 - p)) is at most exp (s² / 8).

theorem Cslib.sum_choose_mul_pow_eq_one (Q : ℕ) (p : ℝ) : ∑ k ∈ Finset.range (Q + 1), ↑(Q.choose k) * p ^ k * (1 - p) ^ (Q - k) = 1

The binomial weights C(Q, k) p^k (1 - p)^(Q - k) sum to 1.

theorem Cslib.sum_choose_mul_pow_mul_exp (Q : ℕ) (p s : ℝ) : ∑ k ∈ Finset.range (Q + 1), ↑(Q.choose k) * p ^ k * (1 - p) ^ (Q - k) * Real.exp (s * (↑k - ↑Q * p)) = ((1 - p) * Real.exp (-s * p) + p * Real.exp (s * (1 - p))) ^ Q

The centered binomial moment generating function: summing C(Q, k) p^k (1 - p)^(Q - k) exp (s (k - Q p)) over 0 ≤ k ≤ Q factors as the Q-th power of the single-trial moment generating function.

theorem Cslib.sum_filter_le_sub_choose_mul_pow_le (Q : ℕ) {p t : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) (ht : 0 ≤ t) : ∑ k ∈ Finset.range (Q + 1) with t ≤ ↑k - ↑Q * p, ↑(Q.choose k) * p ^ k * (1 - p) ^ (Q - k) ≤ Real.exp (-2 * t ^ 2 / ↑Q)

Upper-tail Hoeffding inequality for Bin(Q, p): for p ∈ [0, 1] and 0 ≤ t, the binomial probability mass on k - Q p ≥ t is at most exp (-2 t² / Q). At Q = 0 the right-hand side is exp 0 = 1.

theorem Cslib.sum_filter_le_mul_sub_choose_mul_pow_le (Q : ℕ) {p t : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) (ht : 0 ≤ t) : ∑ k ∈ Finset.range (Q + 1) with t ≤ ↑Q * p - ↑k, ↑(Q.choose k) * p ^ k * (1 - p) ^ (Q - k) ≤ Real.exp (-2 * t ^ 2 / ↑Q)

Lower-tail Hoeffding inequality for Bin(Q, p): for p ∈ [0, 1] and 0 ≤ t, the binomial probability mass on Q p - k ≥ t is at most exp (-2 t² / Q).

theorem Cslib.sum_filter_le_abs_sub_choose_mul_pow_le (Q : ℕ) {p t : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) (ht : 0 ≤ t) : ∑ k ∈ Finset.range (Q + 1) with t ≤ |↑k - ↑Q * p|, ↑(Q.choose k) * p ^ k * (1 - p) ^ (Q - k) ≤ 2 * Real.exp (-2 * t ^ 2 / ↑Q)

Two-sided Hoeffding inequality for Bin(Q, p) [Hoeffding1963]: for p ∈ [0, 1] and 0 ≤ t, the binomial probability mass on |k - Q p| ≥ t is at most 2 exp (-2 t² / Q).

theorem Cslib.sum_filter_notMem_choose_mul_pow_le (Q : ℕ) (I : Finset ℕ) {p t : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) (ht : 0 ≤ t) (hI : ∀ k ∈ Finset.range (Q + 1), |↑k - ↑Q * p| ≤ t → k ∈ I) : ∑ k ∈ Finset.range (Q + 1) with k ∉ I, ↑(Q.choose k) * p ^ k * (1 - p) ^ (Q - k) ≤ 2 * Real.exp (-2 * t ^ 2 / ↑Q)

Interval-complement Hoeffding bound for Bin(Q, p): if I contains every integer 0 ≤ k ≤ Q within t of the mean Q p, then the binomial mass outside I is at most 2 exp (-2 t² / Q).