Hoeffding's inequality for random bit strings

Fix real weights a : ι → ℝ. For all but a 2 exp (-2 t² / ∑ i, a i ^ 2) fraction of the bit strings x : ι → Bool, the centred weighted sum ∑ i, a i * (x i - 1 / 2) has absolute value less than t (card_filter_le_abs_sum_mul_sub_half_le). This is Hoeffding's inequality for a weighted sum of independent unbiased bits, in counting form. With the weights ±1 on a finite set R and 0 elsewhere, it bounds the binomial tail: for all but a 2 exp (-2 t² / |R|) fraction of the strings, the number of true coordinates of x in R is within t of |R| / 2 (card_filter_le_abs_card_filter_sub_half_le).

The tail bounds are McDiarmid's inequality (Cslib.Probability.HasBoundedDifferences) for the sum of the coordinate scores a i * (x i - 1 / 2), each varying by at most |a i| and of mean 0 under independent uniform bits; the probability of an event under uniform bits is its fraction of all strings. The exact exponential moment is recorded separately: the sum over all strings of exp (s ∑ i, a i (x i - 1 / 2)) factors over the coordinates, and equals 2 ^ |ι| ∏ i, cosh (s a i / 2) (sum_exp_mul_sum_mul_sub_half).

Main results

• Cslib.BitString.sum_exp_mul_sum_mul_sub_half: the weighted exponential moment.
• Cslib.BitString.card_filter_le_sum_mul_sub_half_le: the weighted one-sided tail bound.
• Cslib.BitString.card_filter_le_abs_sum_mul_sub_half_le: Hoeffding's inequality for weighted bit sums.
• Cslib.BitString.sum_exp_mul_card_filter_sub_half: the exponential moment of a bit count.
• Cslib.BitString.card_filter_le_card_filter_sub_half_le: the one-sided tail bound for a bit count.
• Cslib.BitString.card_filter_le_abs_card_filter_sub_half_le: Hoeffding's inequality for a bit count.

References

• N. Alon, J. H. Spencer, The Probabilistic Method, Theorem A.1.1
• W. Hoeffding, Probability inequalities for sums of bounded random variables
• C. McDiarmid, On the method of bounded differences, Lemma 1.2

theorem Cslib.BitString.sum_exp_mul_sum_mul_sub_half {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a : ι → ℝ) (s : ℝ) : ∑ x : ι → Bool, Real.exp (s * ∑ i : ι, a i * (↑(x i).toNat - 1 / 2)) = 2 ^ Fintype.card ι * ∏ i : ι, Real.cosh (s * a i / 2)

The weighted exponential moment. Summed over all bit strings x, the exponential of s times the centred weighted sum ∑ i, a i * (x i - 1 / 2) is 2 ^ |ι| ∏ i, cosh (s a i / 2).

theorem Cslib.BitString.card_filter_le_sum_mul_sub_half_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a : ι → ℝ) {t : ℝ} (ht : 0 ≤ t) : ↑{x : ι → Bool | t ≤ ∑ i : ι, a i * (↑(x i).toNat - 1 / 2)}.card ≤ 2 ^ Fintype.card ι * Real.exp (-(2 * t ^ 2 / ∑ i : ι, a i ^ 2))

The weighted one-sided tail bound. At most an exp (-2 t² / ∑ i, a i ^ 2) fraction of the bit strings x have centred weighted sum ∑ i, a i * (x i - 1 / 2) at least t. This is McDiarmid's inequality HasBoundedDifferences.pi_ge_mean_add for independent uniform bits.

theorem Cslib.BitString.card_filter_le_abs_sum_mul_sub_half_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a : ι → ℝ) {t : ℝ} (ht : 0 ≤ t) : ↑{x : ι → Bool | t ≤ |∑ i : ι, a i * (↑(x i).toNat - 1 / 2)|}.card ≤ 2 * 2 ^ Fintype.card ι * Real.exp (-(2 * t ^ 2 / ∑ i : ι, a i ^ 2))

Hoeffding's inequality for weighted bit sums. At most a 2 exp (-2 t² / ∑ i, a i ^ 2) fraction of the bit strings x have a centred weighted sum ∑ i, a i * (x i - 1 / 2) of absolute value at least t. This is HasBoundedDifferences.pi_abs_sub_mean_ge.

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.