Chernoff bounds for independent, non-identical Bernoulli trials

Roadmap target FND-3. Source: M. Mitzenmacher and E. Upfal, Probability and Computing, Cambridge University Press, 2005, Section 4.2.1: Theorem 4.4, bound (4.1) (upper tail), Theorem 4.5, bounds (4.4) and (4.5) (lower tail), and Exercise 4.7 (the mean μ = 𝔼X may be replaced by any μ_H ≥ μ in the upper tail and any μ_L ≤ μ in the lower tail).

Let X = ∑ᵢ Xᵢ be a sum of independent {0,1}-valued trials with P(Xᵢ = 1) = pᵢ and μ = ∑ᵢ pᵢ. For μ_L ≤ μ ≤ μ_H:

• P(X ≥ (1 + δ) μ_H) ≤ (e^δ / (1 + δ)^(1 + δ))^μ_H ≤ exp (-δ² μ_H / (2 + δ)) for δ > 0;
• P(X ≤ (1 - δ) μ_L) ≤ (e^(-δ) / (1 - δ)^(1 - δ))^μ_L ≤ exp (-δ² μ_L / 2) for 0 < δ < 1.

Taking μ_H = μ or μ_L = μ gives the bounds for the exact mean. Each bound is stated in three settings, all on the finite product space ι → α (no measure theory):

• general: ω is drawn from the independent product Distribution.independent P of a family P : ι → Distribution α, and Xᵢ = Y i (ω i) for observables Y i : α → {0,1}, so that pᵢ = (P i).expect (Y i);
• Bernoulli coins: ω : ι → Bool has independent coordinates ω i ~ bernoulli (p i) and X counts the heads among the coins of a finite set S (S = univ is the textbook statement);
• uniform rounds: ω : ι → γ is uniform (one independent uniform draw per agent, as in Dynamics.Concentration), probabilities are avg of indicators and pᵢ = avg (Y i). This is the form produced by Kernel.prob_ofStep for one round of a dynamics.

For uniform rounds over Fin n the file also gives the MGF bound avg_chernoff_mgf, the tails for a free parameter t (avg_chernoff_upper_of_mgf, avg_chernoff_lower_of_mgf), the closed forms exp(k - μ - k log(k/μ)) at an arbitrary threshold k (avg_chernoff_upper_log, avg_chernoff_lower_log) and avg_chernoff_lower_mul.

noncomputable def Dynamics.Distribution.bernoulli (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) : Distribution Bool

A biased coin: true with probability p.

Equations

• Dynamics.Distribution.bernoulli p h0 h1 = { weight := fun (b : Bool) => if b = true then p else 1 - p, nonneg := ⋯, sum_one := ⋯ }

Independent {0,1}-valued observables on a product distribution

theorem Dynamics.Distribution.chernoff_upper_ratio {ι : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype α] (P : ι → Distribution α) (Y : ι → α → ℝ) (hY : ∀ (i : ι) (a : α), Y i a = 0 ∨ Y i a = 1) {δ μH : ℝ} (hδ : 0 < δ) (hμH : ∑ i : ι, (P i).expect (Y i) ≤ μH) : ((independent P).prob fun (ω : ι → α) => (1 + δ) * μH ≤ ∑ i : ι, Y i (ω i)) ≤ (Real.exp δ / (1 + δ) ^ (1 + δ)) ^ μH

Chernoff upper tail, ratio form (Mitzenmacher–Upfal, Theorem 4.4, bound (4.1), with an upper bound μH on the mean as in Exercise 4.7): if ω ~ independent P, every Y i is {0,1}-valued and ∑ᵢ 𝔼[Y i] ≤ μH, then for δ > 0, P(∑ᵢ Y i (ω i) ≥ (1 + δ) μH) ≤ (e^δ / (1 + δ)^(1 + δ))^μH.

theorem Dynamics.Distribution.chernoff_upper {ι : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype α] (P : ι → Distribution α) (Y : ι → α → ℝ) (hY : ∀ (i : ι) (a : α), Y i a = 0 ∨ Y i a = 1) {δ μH : ℝ} (hδ : 0 < δ) (hμH : ∑ i : ι, (P i).expect (Y i) ≤ μH) : ((independent P).prob fun (ω : ι → α) => (1 + δ) * μH ≤ ∑ i : ι, Y i (ω i)) ≤ Real.exp (-(δ ^ 2 * μH / (2 + δ)))

Chernoff upper tail (Mitzenmacher–Upfal, Theorem 4.4 and Exercise 4.7, in the closed form obtained from (4.1) by log (1 + δ) ≥ 2δ / (2 + δ)): if ω ~ independent P, every Y i is {0,1}-valued and ∑ᵢ 𝔼[Y i] ≤ μH, then for δ > 0, P(∑ᵢ Y i (ω i) ≥ (1 + δ) μH) ≤ exp (-δ² μH / (2 + δ)).

theorem Dynamics.Distribution.chernoff_lower_ratio {ι : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype α] (P : ι → Distribution α) (Y : ι → α → ℝ) (hY : ∀ (i : ι) (a : α), Y i a = 0 ∨ Y i a = 1) {δ μL : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 1) (hμL : μL ≤ ∑ i : ι, (P i).expect (Y i)) : ((independent P).prob fun (ω : ι → α) => ∑ i : ι, Y i (ω i) ≤ (1 - δ) * μL) ≤ (Real.exp (-δ) / (1 - δ) ^ (1 - δ)) ^ μL

Chernoff lower tail, ratio form (Mitzenmacher–Upfal, Theorem 4.5, bound (4.4), with a lower bound μL on the mean as in Exercise 4.7): if ω ~ independent P, every Y i is {0,1}-valued and μL ≤ ∑ᵢ 𝔼[Y i], then for 0 < δ < 1, P(∑ᵢ Y i (ω i) ≤ (1 - δ) μL) ≤ (e^(-δ) / (1 - δ)^(1 - δ))^μL.

theorem Dynamics.Distribution.chernoff_lower {ι : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype α] (P : ι → Distribution α) (Y : ι → α → ℝ) (hY : ∀ (i : ι) (a : α), Y i a = 0 ∨ Y i a = 1) {δ μL : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 1) (hμL : μL ≤ ∑ i : ι, (P i).expect (Y i)) : ((independent P).prob fun (ω : ι → α) => ∑ i : ι, Y i (ω i) ≤ (1 - δ) * μL) ≤ Real.exp (-(δ ^ 2 * μL / 2))

Chernoff lower tail (Mitzenmacher–Upfal, Theorem 4.5, bound (4.5), with a lower bound μL on the mean as in Exercise 4.7): if ω ~ independent P, every Y i is {0,1}-valued and μL ≤ ∑ᵢ 𝔼[Y i], then for 0 < δ < 1, P(∑ᵢ Y i (ω i) ≤ (1 - δ) μL) ≤ exp (-δ² μL / 2).

Independent Bernoulli coins

theorem Dynamics.Distribution.bernoulli_expect (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) (f : Bool → ℝ) : (bernoulli p h0 h1).expect f = p * f true + (1 - p) * f false

Expectation under a biased coin.

theorem Dynamics.Distribution.sum_bernoulli_expect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ι → ℝ) (hp0 : ∀ (i : ι), 0 ≤ p i) (hp1 : ∀ (i : ι), p i ≤ 1) (S : Finset ι) : (∑ i : ι, (bernoulli (p i) ⋯ ⋯).expect fun (b : Bool) => if i ∈ S then if b = true then 1 else 0 else 0) = ∑ i ∈ S, p i

The number of heads among the coins of S has mean ∑_{i ∈ S} pᵢ.

theorem Dynamics.Distribution.bernoulli_chernoff_upper_ratio {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ι → ℝ) (hp0 : ∀ (i : ι), 0 ≤ p i) (hp1 : ∀ (i : ι), p i ≤ 1) (S : Finset ι) {δ μH : ℝ} (hδ : 0 < δ) (hμH : ∑ i ∈ S, p i ≤ μH) : ((independent fun (i : ι) => bernoulli (p i) ⋯ ⋯).prob fun (ω : ι → Bool) => (1 + δ) * μH ≤ ↑{i ∈ S | ω i = true}.card) ≤ (Real.exp δ / (1 + δ) ^ (1 + δ)) ^ μH

Chernoff upper tail for Bernoulli(pᵢ) coins, ratio form (Mitzenmacher–Upfal, Theorem 4.4, bound (4.1), and Exercise 4.7): for independent coins ω i ~ bernoulli (p i), a finite set S of coins with ∑_{i ∈ S} pᵢ ≤ μH and δ > 0, the number of heads in S satisfies P(#heads ≥ (1 + δ) μH) ≤ (e^δ / (1 + δ)^(1 + δ))^μH.

theorem Dynamics.Distribution.bernoulli_chernoff_upper {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ι → ℝ) (hp0 : ∀ (i : ι), 0 ≤ p i) (hp1 : ∀ (i : ι), p i ≤ 1) (S : Finset ι) {δ μH : ℝ} (hδ : 0 < δ) (hμH : ∑ i ∈ S, p i ≤ μH) : ((independent fun (i : ι) => bernoulli (p i) ⋯ ⋯).prob fun (ω : ι → Bool) => (1 + δ) * μH ≤ ↑{i ∈ S | ω i = true}.card) ≤ Real.exp (-(δ ^ 2 * μH / (2 + δ)))

Chernoff upper tail for Bernoulli(pᵢ) coins (Mitzenmacher–Upfal, Theorem 4.4 and Exercise 4.7, closed form via log (1 + δ) ≥ 2δ / (2 + δ)): for independent coins ω i ~ bernoulli (p i), a finite set S of coins with ∑_{i ∈ S} pᵢ ≤ μH and δ > 0, P(#heads in S ≥ (1 + δ) μH) ≤ exp (-δ² μH / (2 + δ)).

theorem Dynamics.Distribution.bernoulli_chernoff_lower_ratio {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ι → ℝ) (hp0 : ∀ (i : ι), 0 ≤ p i) (hp1 : ∀ (i : ι), p i ≤ 1) (S : Finset ι) {δ μL : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 1) (hμL : μL ≤ ∑ i ∈ S, p i) : ((independent fun (i : ι) => bernoulli (p i) ⋯ ⋯).prob fun (ω : ι → Bool) => ↑{i ∈ S | ω i = true}.card ≤ (1 - δ) * μL) ≤ (Real.exp (-δ) / (1 - δ) ^ (1 - δ)) ^ μL

Chernoff lower tail for Bernoulli(pᵢ) coins, ratio form (Mitzenmacher–Upfal, Theorem 4.5, bound (4.4), and Exercise 4.7): for independent coins ω i ~ bernoulli (p i), a finite set S of coins with μL ≤ ∑_{i ∈ S} pᵢ and 0 < δ < 1, P(#heads in S ≤ (1 - δ) μL) ≤ (e^(-δ) / (1 - δ)^(1 - δ))^μL.

theorem Dynamics.Distribution.bernoulli_chernoff_lower {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ι → ℝ) (hp0 : ∀ (i : ι), 0 ≤ p i) (hp1 : ∀ (i : ι), p i ≤ 1) (S : Finset ι) {δ μL : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 1) (hμL : μL ≤ ∑ i ∈ S, p i) : ((independent fun (i : ι) => bernoulli (p i) ⋯ ⋯).prob fun (ω : ι → Bool) => ↑{i ∈ S | ω i = true}.card ≤ (1 - δ) * μL) ≤ Real.exp (-(δ ^ 2 * μL / 2))

Chernoff lower tail for Bernoulli(pᵢ) coins (Mitzenmacher–Upfal, Theorem 4.5, bound (4.5), and Exercise 4.7): for independent coins ω i ~ bernoulli (p i), a finite set S of coins with μL ≤ ∑_{i ∈ S} pᵢ and 0 < δ < 1, P(#heads in S ≤ (1 - δ) μL) ≤ exp (-δ² μL / 2).

Uniform rounds

theorem Dynamics.avg_chernoff_upper_ratio {ι : Type u_1} {γ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype γ] (Y : ι → γ → ℝ) (hY : ∀ (i : ι) (x : γ), Y i x = 0 ∨ Y i x = 1) {δ μH : ℝ} (hδ : 0 < δ) (hμH : ∑ i : ι, avg (Y i) ≤ μH) : (avg fun (ω : ι → γ) => if (1 + δ) * μH ≤ ∑ i : ι, Y i (ω i) then 1 else 0) ≤ (Real.exp δ / (1 + δ) ^ (1 + δ)) ^ μH

Chernoff upper tail for one uniform round, ratio form (Mitzenmacher–Upfal, Theorem 4.4, bound (4.1), and Exercise 4.7): if ω : ι → γ is uniform, every Y i is {0,1}-valued and ∑ᵢ avg (Y i) ≤ μH, then for δ > 0, P(∑ᵢ Y i (ω i) ≥ (1 + δ) μH) ≤ (e^δ / (1 + δ)^(1 + δ))^μH.

theorem Dynamics.avg_chernoff_upper {ι : Type u_1} {γ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype γ] (Y : ι → γ → ℝ) (hY : ∀ (i : ι) (x : γ), Y i x = 0 ∨ Y i x = 1) {δ μH : ℝ} (hδ : 0 < δ) (hμH : ∑ i : ι, avg (Y i) ≤ μH) : (avg fun (ω : ι → γ) => if (1 + δ) * μH ≤ ∑ i : ι, Y i (ω i) then 1 else 0) ≤ Real.exp (-(δ ^ 2 * μH / (2 + δ)))

Chernoff upper tail for one uniform round (Mitzenmacher–Upfal, Theorem 4.4 and Exercise 4.7, closed form via log (1 + δ) ≥ 2δ / (2 + δ)): if ω : ι → γ is uniform, every Y i is {0,1}-valued and ∑ᵢ avg (Y i) ≤ μH, then for δ > 0, P(∑ᵢ Y i (ω i) ≥ (1 + δ) μH) ≤ exp (-δ² μH / (2 + δ)).

theorem Dynamics.avg_chernoff_lower_ratio {ι : Type u_1} {γ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype γ] (Y : ι → γ → ℝ) (hY : ∀ (i : ι) (x : γ), Y i x = 0 ∨ Y i x = 1) {δ μL : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 1) (hμL : μL ≤ ∑ i : ι, avg (Y i)) : (avg fun (ω : ι → γ) => if ∑ i : ι, Y i (ω i) ≤ (1 - δ) * μL then 1 else 0) ≤ (Real.exp (-δ) / (1 - δ) ^ (1 - δ)) ^ μL

Chernoff lower tail for one uniform round, ratio form (Mitzenmacher–Upfal, Theorem 4.5, bound (4.4), and Exercise 4.7): if ω : ι → γ is uniform, every Y i is {0,1}-valued and μL ≤ ∑ᵢ avg (Y i), then for 0 < δ < 1, P(∑ᵢ Y i (ω i) ≤ (1 - δ) μL) ≤ (e^(-δ) / (1 - δ)^(1 - δ))^μL.

theorem Dynamics.avg_chernoff_lower {ι : Type u_1} {γ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype γ] (Y : ι → γ → ℝ) (hY : ∀ (i : ι) (x : γ), Y i x = 0 ∨ Y i x = 1) {δ μL : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 1) (hμL : μL ≤ ∑ i : ι, avg (Y i)) : (avg fun (ω : ι → γ) => if ∑ i : ι, Y i (ω i) ≤ (1 - δ) * μL then 1 else 0) ≤ Real.exp (-(δ ^ 2 * μL / 2))

Chernoff lower tail for one uniform round (Mitzenmacher–Upfal, Theorem 4.5, bound (4.5), and Exercise 4.7): if ω : ι → γ is uniform, every Y i is {0,1}-valued and μL ≤ ∑ᵢ avg (Y i), then for 0 < δ < 1, P(∑ᵢ Y i (ω i) ≤ (1 - δ) μL) ≤ exp (-δ² μL / 2).

Uniform rounds: MGF, free parameter and logarithmic forms

For X = ∑ᵢ Yᵢ(ωᵢ) with ω : Fin n → γ uniform and {0,1}-valued coordinates (Dubhashi–Panconesi, Concentration of Measure for the Analysis of Randomized Algorithms, Theorem 1.1 and its proof; Mitzenmacher–Upfal, Theorem 4.5): the tails before the parameter t is optimized, the closed forms for an arbitrary threshold k, and the lower tail at the exact mean. These replace the bounds of the former 3-majority/ThreeMajority/Chernoff.lean (3-majority blueprint lem:mgf, lem:chernoff, lem:chernofflog) and Plurality.chernoff_lower.

theorem Dynamics.avg_chernoff_mgf {n : ℕ} {γ : Type u_1} [Fintype γ] (Y : Fin n → γ → ℝ) (hY : ∀ (i : Fin n) (x : γ), Y i x = 0 ∨ Y i x = 1) (t : ℝ) : (avg fun (ω : Fin n → γ) => Real.exp (t * ∑ i : Fin n, Y i (ω i))) ≤ Real.exp ((∑ i : Fin n, avg (Y i)) * (Real.exp t - 1))

The Chernoff MGF bound for one uniform round: for every real t, 𝔼[exp(tX)] ≤ exp(μ(eᵗ - 1)) (the uniform-round form of Distribution.independent_expect_exp_sum_le, also on an empty type γ). Replaces ThreeMajority.avg_exp_le.

theorem Dynamics.avg_chernoff_upper_of_mgf {n : ℕ} {γ : Type u_1} [Fintype γ] (Y : Fin n → γ → ℝ) (hY : ∀ (i : Fin n) (x : γ), Y i x = 0 ∨ Y i x = 1) {t : ℝ} (ht : 0 ≤ t) (k : ℝ) : (avg fun (ω : Fin n → γ) => if k ≤ ∑ i : Fin n, Y i (ω i) then 1 else 0) ≤ Real.exp ((∑ i : Fin n, avg (Y i)) * (Real.exp t - 1) - t * k)

Chernoff upper tail for a free parameter t ≥ 0: P(X ≥ k) ≤ exp(μ(eᵗ - 1) - t k) (before optimizing t; avg_chernoff_upper is the optimized form). Replaces ThreeMajority.avg_tail_ge.

theorem Dynamics.avg_chernoff_lower_of_mgf {n : ℕ} {γ : Type u_1} [Fintype γ] (Y : Fin n → γ → ℝ) (hY : ∀ (i : Fin n) (x : γ), Y i x = 0 ∨ Y i x = 1) {t : ℝ} (ht : t ≤ 0) (k : ℝ) : (avg fun (ω : Fin n → γ) => if ∑ i : Fin n, Y i (ω i) ≤ k then 1 else 0) ≤ Real.exp ((∑ i : Fin n, avg (Y i)) * (Real.exp t - 1) - t * k)

Chernoff lower tail for a free parameter t ≤ 0: P(X ≤ k) ≤ exp(μ(eᵗ - 1) - t k) (before optimizing t; avg_chernoff_lower is the optimized form). Replaces ThreeMajority.avg_tail_le.

theorem Dynamics.avg_chernoff_upper_log {n : ℕ} {γ : Type u_1} [Fintype γ] (Y : Fin n → γ → ℝ) (hY : ∀ (i : Fin n) (x : γ), Y i x = 0 ∨ Y i x = 1) {k μ : ℝ} (hμ : ∑ i : Fin n, avg (Y i) ≤ μ) (hμ0 : 0 < μ) (hk : μ ≤ k) : (avg fun (ω : Fin n → γ) => if k ≤ ∑ i : Fin n, Y i (ω i) then 1 else 0) ≤ Real.exp (k - μ - k * Real.log (k / μ))

Chernoff upper tail, closed form at a threshold k (t = log (k/μ)): if μ > 0 bounds the mean from above and μ ≤ k, then P(X ≥ k) ≤ exp(k - μ - k log(k/μ)). With μ = 𝔼X this is ThreeMajority.avg_tail_ge_log; it replaces that lemma and ThreeMajority.avg_tail_ge_log_le.

theorem Dynamics.avg_chernoff_lower_log {n : ℕ} {γ : Type u_1} [Fintype γ] (Y : Fin n → γ → ℝ) (hY : ∀ (i : Fin n) (x : γ), Y i x = 0 ∨ Y i x = 1) {k μ : ℝ} (hμ : μ ≤ ∑ i : Fin n, avg (Y i)) (hk0 : 0 < k) (hkμ : k ≤ μ) : (avg fun (ω : Fin n → γ) => if ∑ i : Fin n, Y i (ω i) ≤ k then 1 else 0) ≤ Real.exp (k - μ - k * Real.log (k / μ))

Chernoff lower tail, closed form at a threshold k (t = log (k/μ)): if μ bounds the mean from below and 0 < k ≤ μ, then P(X ≤ k) ≤ exp(k - μ - k log(k/μ)). With μ = 𝔼X this is ThreeMajority.avg_tail_le_log; it replaces that lemma and ThreeMajority.avg_tail_le_log_ge.

theorem Dynamics.avg_chernoff_lower_mul {n : ℕ} {γ : Type u_1} [Fintype γ] (Y : Fin n → γ → ℝ) (hY : ∀ (i : Fin n) (x : γ), Y i x = 0 ∨ Y i x = 1) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ < 1) : (avg fun (ω : Fin n → γ) => if ∑ i : Fin n, Y i (ω i) ≤ (1 - δ) * ∑ i : Fin n, avg (Y i) then 1 else 0) ≤ Real.exp (-((δ ^ 2 * ∑ i : Fin n, avg (Y i)) / 2))

Multiplicative Chernoff lower tail at the mean: P(X ≤ (1 - δ)μ) ≤ exp(-δ²μ/2) for 0 ≤ δ < 1 and μ = 𝔼X (avg_chernoff_lower with μL = 𝔼X, extended to δ = 0). Replaces Plurality.chernoff_lower (plurality blueprint lem:tails).