Multiplicative Chernoff bounds

Let X = ∑ i, score i (outcome i) be a sum of independent scores with values in [0, 1], the coordinates of outcome drawn from the product Cslib.Probability.PMF.pi p, and let μ bound its mean ∑ i, ∑ a, p i a * score i a. The multiplicative Chernoff bounds compare X with multiples of μ; Mitzenmacher and Upfal prove them for sums of independent 0/1 trials with μ the mean Mitzenmacher and Upfal, Section 4.2, and the same proofs apply to [0, 1]-valued scores and to a bound μ on the mean in the appropriate direction:

• if the mean is at most μ, then X ≥ (1 + δ) μ with probability at most exp (μ (δ - (1 + δ) log (1 + δ))), hence at most exp (-δ² μ / (2 + δ)), and at most exp (-δ² μ / 3) when δ ≤ 1;
• if the mean is at least μ, then X ≤ (1 - δ) μ with probability at most exp (-δ² μ / 2).

The proofs follow the moment generating function method: Mathlib's Chernoff bound ProbabilityTheory.measure_ge_le_exp_mul_mgf, multiplicativity of the moment generating function under independence, and the convexity estimate exp (t s) ≤ 1 + s (exp t - 1) for s ∈ [0, 1] (Cslib.Probability.PMF.mgf_pi_sum_le). All client-facing statements are about ordinary PMF event probabilities. For fair coins, counting bit strings whose weight deviates from half the length, the additive Hoeffding bound Cslib.BitString.card_filter_le_card_filter_sub_half_le is already stronger than the multiplicative forms, so no separate counting form is given here.

Main results

• Cslib.Probability.PMF.mgf_pi_sum_le: the moment generating function of the sum is at most exp (mean * (exp t - 1)).
• Cslib.Probability.PMF.pi_sum_ge_le_exp, Cslib.Probability.PMF.pi_sum_le_le_exp: the Chernoff bound for every parameter t.
• Cslib.Probability.PMF.pi_sum_ge_one_add_mul_le_exp_log: the sharp multiplicative upper tail.
• Cslib.Probability.PMF.pi_sum_ge_one_add_mul, Cslib.Probability.PMF.pi_sum_ge_one_add_mul_of_le_one: the simplified upper tails.
• Cslib.Probability.PMF.pi_sum_le_one_sub_mul: the lower tail.
• Cslib.Probability.PMF.pi_sum_abs_sub_mean_ge_mul: the two-sided bound for δ ≤ 1.

References

• M. Mitzenmacher, E. Upfal, Probability and Computing, Section 4.2
• N. Alon, J. H. Spencer, The Probabilistic Method, Appendix A

theorem Cslib.Probability.PMF.mgf_pi_sum_le {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableSingletonClass (α i)] (p : (i : ι) → PMF (α i)) (score : (i : ι) → α i → ℝ) (hscore : ∀ (i : ι), ∀ a ∈ (p i).support, score i a ∈ Set.Icc 0 1) (t : ℝ) : ProbabilityTheory.mgf (fun (outcome : (i : ι) → α i) => ∑ i : ι, score i (outcome i)) (pi p).toMeasure t ≤ Real.exp ((∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a) * (Real.exp t - 1))

The Chernoff moment bound: the moment generating function of a sum of independent scores in [0, 1] is at most exp (mean * (exp t - 1)).

theorem Cslib.Probability.PMF.pi_sum_ge_le_exp {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (p : (i : ι) → PMF (α i)) (score : (i : ι) → α i → ℝ) (hscore : ∀ (i : ι), ∀ a ∈ (p i).support, score i a ∈ Set.Icc 0 1) {t : ℝ} (ht : 0 ≤ t) (ε : ℝ) : ((pi p).toOuterMeasure {outcome : (i : ι) → α i | ε ≤ ∑ i : ι, score i (outcome i)}).toReal ≤ Real.exp (-t * ε + (∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a) * (Real.exp t - 1))

The Chernoff bound for the upper tail, with a free parameter t ≥ 0: a sum of independent scores in [0, 1] is at least ε with probability at most exp (-t ε + mean * (exp t - 1)).

theorem Cslib.Probability.PMF.pi_sum_le_le_exp {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (p : (i : ι) → PMF (α i)) (score : (i : ι) → α i → ℝ) (hscore : ∀ (i : ι), ∀ a ∈ (p i).support, score i a ∈ Set.Icc 0 1) {t : ℝ} (ht : t ≤ 0) (ε : ℝ) : ((pi p).toOuterMeasure {outcome : (i : ι) → α i | ∑ i : ι, score i (outcome i) ≤ ε}).toReal ≤ Real.exp (-t * ε + (∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a) * (Real.exp t - 1))

The Chernoff bound for the lower tail, with a free parameter t ≤ 0: a sum of independent scores in [0, 1] is at most ε with probability at most exp (-t ε + mean * (exp t - 1)).

theorem Cslib.Probability.PMF.pi_sum_ge_one_add_mul_le_exp_log {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (p : (i : ι) → PMF (α i)) (score : (i : ι) → α i → ℝ) (hscore : ∀ (i : ι), ∀ a ∈ (p i).support, score i a ∈ Set.Icc 0 1) {μ δ : ℝ} (hμ : ∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a ≤ μ) (hδ : 0 ≤ δ) : ((pi p).toOuterMeasure {outcome : (i : ι) → α i | (1 + δ) * μ ≤ ∑ i : ι, score i (outcome i)}).toReal ≤ Real.exp (μ * (δ - (1 + δ) * Real.log (1 + δ)))

The sharp multiplicative Chernoff bound [Mitzenmacher and Upfal, Section 4.2] [MU17]: if independent scores in [0, 1] have mean at most μ, their sum is at least (1 + δ) μ with probability at most exp (μ (δ - (1 + δ) log (1 + δ))), that is, (exp δ / (1 + δ) ^ (1 + δ)) ^ μ, for every δ ≥ 0.

theorem Cslib.Probability.PMF.pi_sum_ge_one_add_mul {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (p : (i : ι) → PMF (α i)) (score : (i : ι) → α i → ℝ) (hscore : ∀ (i : ι), ∀ a ∈ (p i).support, score i a ∈ Set.Icc 0 1) {μ δ : ℝ} (hμ : ∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a ≤ μ) (hδ : 0 ≤ δ) : ((pi p).toOuterMeasure {outcome : (i : ι) → α i | (1 + δ) * μ ≤ ∑ i : ι, score i (outcome i)}).toReal ≤ Real.exp (-(δ ^ 2 * μ / (2 + δ)))

The multiplicative Chernoff bound: if independent scores in [0, 1] have mean at most μ, their sum is at least (1 + δ) μ with probability at most exp (-δ² μ / (2 + δ)), for every δ ≥ 0. This follows from the sharp bound and 2 δ / (2 + δ) ≤ log (1 + δ).

theorem Cslib.Probability.PMF.pi_sum_ge_one_add_mul_of_le_one {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (p : (i : ι) → PMF (α i)) (score : (i : ι) → α i → ℝ) (hscore : ∀ (i : ι), ∀ a ∈ (p i).support, score i a ∈ Set.Icc 0 1) {μ δ : ℝ} (hμ : ∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a ≤ μ) (hδ : 0 ≤ δ) (hδ₁ : δ ≤ 1) : ((pi p).toOuterMeasure {outcome : (i : ι) → α i | (1 + δ) * μ ≤ ∑ i : ι, score i (outcome i)}).toReal ≤ Real.exp (-(δ ^ 2 * μ / 3))

The multiplicative Chernoff bound for δ ≤ 1 [Mitzenmacher and Upfal, Section 4.2] [MU17]: if independent scores in [0, 1] have mean at most μ, their sum is at least (1 + δ) μ with probability at most exp (-δ² μ / 3), for 0 ≤ δ ≤ 1.

theorem Cslib.Probability.PMF.pi_sum_le_one_sub_mul {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (p : (i : ι) → PMF (α i)) (score : (i : ι) → α i → ℝ) (hscore : ∀ (i : ι), ∀ a ∈ (p i).support, score i a ∈ Set.Icc 0 1) {μ δ : ℝ} (hμ : μ ≤ ∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a) (hδ : 0 ≤ δ) : ((pi p).toOuterMeasure {outcome : (i : ι) → α i | ∑ i : ι, score i (outcome i) ≤ (1 - δ) * μ}).toReal ≤ Real.exp (-(δ ^ 2 * μ / 2))

The multiplicative Chernoff bound for the lower tail Mitzenmacher and Upfal, Section 4.2: if independent scores in [0, 1] have mean at least μ, their sum is at most (1 - δ) μ with probability at most exp (-δ² μ / 2), for every δ ≥ 0. The proof takes the parameter t = -δ and uses exp (-δ) ≤ 1 - δ + δ² / 2.

theorem Cslib.Probability.PMF.pi_sum_abs_sub_mean_ge_mul {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (p : (i : ι) → PMF (α i)) (score : (i : ι) → α i → ℝ) (hscore : ∀ (i : ι), ∀ a ∈ (p i).support, score i a ∈ Set.Icc 0 1) {δ : ℝ} (hδ : 0 ≤ δ) (hδ₁ : δ ≤ 1) : ((pi p).toOuterMeasure {outcome : (i : ι) → α i | δ * ∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a ≤ |∑ i : ι, score i (outcome i) - ∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a|}).toReal ≤ 2 * Real.exp (-((δ ^ 2 * ∑ i : ι, ∑ a : α i, ((p i) a).toReal * score i a) / 3))

The two-sided multiplicative Chernoff bound [Mitzenmacher and Upfal, Section 4.2] [MU17]: a sum of independent scores in [0, 1] deviates from its mean by at least δ times the mean with probability at most 2 exp (-δ² mean / 3), for 0 ≤ δ ≤ 1.