Hoeffding's inequality for random bit strings

Fix a finite set R of coordinates. For all but a 2 exp (-2 t² / |R|) fraction of the bit strings x : ι → Bool, the number of true coordinates of x in R is within t of |R| / 2 (card_filter_le_abs_card_filter_sub_half_le). This is Hoeffding's inequality for a sum of independent unbiased bits, a tail bound for the binomial distribution, in counting form.

The proof is the exponential-moment argument with the probabilities multiplied out. The sum over all strings of exp (s (#{i ∈ R | x i = c} - |R| / 2)) factors over the coordinates, and equals 2 ^ |ι| cosh (s / 2) ^ |R| (sum_exp_mul_card_filter_sub_half). As cosh u ≤ exp (u² / 2), Markov's inequality with s = 4 t / |R| bounds each tail.

Main results

• Cslib.BitString.sum_exp_mul_card_filter_sub_half: the exponential moment.
• Cslib.BitString.card_filter_le_card_filter_sub_half_le: the one-sided tail bound.
• Cslib.BitString.card_filter_le_abs_card_filter_sub_half_le: Hoeffding's inequality.

References

• N. Alon, J. H. Spencer, The Probabilistic Method, Theorem A.1.1
• W. Hoeffding, Probability inequalities for sums of bounded random variables

theorem Cslib.BitString.sum_exp_mul_card_filter_sub_half {ι : Type u_1} [Fintype ι] [DecidableEq ι] (R : Finset ι) (c : Bool) (s : ℝ) : ∑ x : ι → Bool, Real.exp (s * (↑{i ∈ R | x i = c}.card - ↑R.card / 2)) = 2 ^ Fintype.card ι * Real.cosh (s / 2) ^ R.card

The exponential moment. Summed over all bit strings x, the exponential of s times the deviation of #{i ∈ R | x i = c} from |R| / 2 is 2 ^ |ι| cosh (s / 2) ^ |R|.

theorem Cslib.BitString.card_filter_le_card_filter_sub_half_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (R : Finset ι) (c : Bool) {t : ℝ} (ht : 0 ≤ t) : ↑{x : ι → Bool | t ≤ ↑{i ∈ R | x i = c}.card - ↑R.card / 2}.card ≤ 2 ^ Fintype.card ι * Real.exp (-(2 * t ^ 2 / ↑R.card))

The one-sided tail bound. At most an exp (-2 t² / |R|) fraction of the bit strings x have at least |R| / 2 + t coordinates in R equal to c.

theorem Cslib.BitString.card_filter_le_abs_card_filter_sub_half_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (R : Finset ι) {t : ℝ} (ht : 0 ≤ t) : ↑{x : ι → Bool | t ≤ |↑{i ∈ R | x i = true}.card - ↑R.card / 2|}.card ≤ 2 * 2 ^ Fintype.card ι * Real.exp (-(2 * t ^ 2 / ↑R.card))

Hoeffding's inequality. At most a 2 exp (-2 t² / |R|) fraction of the bit strings x have a number of true coordinates in R that differs from |R| / 2 by at least t.