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.

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).