Helper lemmas for the Chernoff bounds

Auxiliary results for Dynamics.Chernoff (roadmap FND-3, Mitzenmacher–Upfal, Theorems 4.4 and 4.5 with Exercise 4.7). The proof is the textbook one: Markov's inequality applied to exp (t X), the moment-generating function of X = ∑ᵢ Xᵢ factors over the independent coordinates, each {0,1}-valued factor is 1 + pᵢ (eᵗ - 1) ≤ exp (pᵢ (eᵗ - 1)), and then t = log (1 + δ) (upper tail) or t = log (1 - δ) (lower tail).

• Scalar inequalities: two_mul_div_two_add_le_log_one_add (2δ/(2+δ) ≤ log (1+δ)), neg_add_sq_div_two_le_one_sub_mul_log (-δ + δ²/2 ≤ (1-δ) log (1-δ)), and the identity exp_div_rpow_self_rpow rewriting the ratio forms as exponentials.
• Distribution.prob_le_expect_exp: Markov's inequality for exp (t X).
• Distribution.independent_expect_exp_sum_le: 𝔼 exp (t X) ≤ exp (μ (eᵗ - 1)).
• Distribution.prob_ge_le_exp, Distribution.prob_le_le_exp: the tails before optimizing t, with an upper (resp. lower) bound on the mean.
• Distribution.sum_ite_mem_ite_eq_card: the number of heads among the coins of S as a sum of {0,1} coordinates (the coin Distribution.bernoulli and its expectations are in Dynamics.Chernoff, next to the pinned definition).
• Uniform rounds: Distribution.independent_expect_eq_avg and avg_indicator_le_of_independent, which transfer a bound on independent products to avg over ι → γ.

Scalar inequalities

theorem Dynamics.two_mul_div_two_add_le_log_one_add {δ : ℝ} (hδ : 0 ≤ δ) : 2 * δ / (2 + δ) ≤ Real.log (1 + δ)

2δ / (2 + δ) ≤ log (1 + δ) for δ ≥ 0: the first term of the series log (1 + x) - log (1 - x) = ∑ₖ 2 x^(2k+1) / (2k+1) at x = δ / (2 + δ).

theorem Dynamics.half_sub_inv_le_log_of_le_one {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) : (x - x⁻¹) / 2 ≤ Real.log x

log x ≥ (x - 1/x)/2 for 0 < x ≤ 1.

theorem Dynamics.neg_add_sq_div_two_le_one_sub_mul_log {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ < 1) : -δ + δ ^ 2 / 2 ≤ (1 - δ) * Real.log (1 - δ)

-δ + δ²/2 ≤ (1 - δ) log (1 - δ) for 0 ≤ δ < 1.

theorem Dynamics.sub_one_add_mul_log_le {δ : ℝ} (hδ : 0 ≤ δ) : δ - (1 + δ) * Real.log (1 + δ) ≤ -(δ ^ 2 / (2 + δ))

The exponent of the upper ratio form is at most -δ²/(2 + δ).

theorem Dynamics.neg_sub_one_sub_mul_log_le {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ < 1) : -δ - (1 - δ) * Real.log (1 - δ) ≤ -(δ ^ 2 / 2)

The exponent of the lower ratio form is at most -δ²/2.

theorem Dynamics.exp_div_rpow_self_rpow {a : ℝ} (ha : 0 < a) (c μ : ℝ) : (Real.exp c / a ^ a) ^ μ = Real.exp (μ * (c - a * Real.log a))

The ratio forms as exponentials: (e^c / a^a)^μ = exp (μ (c - a log a)) for a > 0.

Markov's inequality and the moment-generating function

theorem Dynamics.Distribution.prob_le_expect_exp {β : Type u_1} [Fintype β] (p : Distribution β) (s : β → Prop) (X : β → ℝ) (t k : ℝ) (hs : ∀ (ω : β), s ω → t * k ≤ t * X ω) : p.prob s ≤ (p.expect fun (ω : β) => Real.exp (t * X ω)) * Real.exp (-(t * k))

Markov's inequality for exp (t X): if the event s forces t k ≤ t X, then P(s) ≤ 𝔼[exp (t X)] exp (-(t k)).

theorem Dynamics.Distribution.independent_expect_exp_sum {ι : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype α] (P : ι → Distribution α) (Y : ι → α → ℝ) (t : ℝ) : ((independent P).expect fun (ω : ι → α) => Real.exp (t * ∑ i : ι, Y i (ω i))) = ∏ i : ι, (P i).expect fun (a : α) => Real.exp (t * Y i a)

The moment-generating function of a sum of independent coordinates factors.

theorem Dynamics.Distribution.expect_exp_mul_le {α : Type u_2} [Fintype α] (p : Distribution α) (Y : α → ℝ) (hY : ∀ (a : α), Y a = 0 ∨ Y a = 1) (t : ℝ) : (p.expect fun (a : α) => Real.exp (t * Y a)) ≤ Real.exp (p.expect Y * (Real.exp t - 1))

The moment-generating function of one {0,1}-valued trial: 𝔼[e^{tY}] = 1 + 𝔼[Y] (eᵗ - 1) ≤ exp (𝔼[Y] (eᵗ - 1)).

theorem Dynamics.Distribution.independent_expect_exp_sum_le {ι : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype α] (P : ι → Distribution α) (Y : ι → α → ℝ) (hY : ∀ (i : ι) (a : α), Y i a = 0 ∨ Y i a = 1) (t : ℝ) : ((independent P).expect fun (ω : ι → α) => Real.exp (t * ∑ i : ι, Y i (ω i))) ≤ Real.exp ((∑ i : ι, (P i).expect (Y i)) * (Real.exp t - 1))

MGF bound for a sum of independent {0,1}-valued trials: 𝔼[exp (t X)] ≤ exp (μ (eᵗ - 1)) with μ = ∑ᵢ 𝔼[Y i], for every real t.

theorem Dynamics.Distribution.sum_expect_nonneg {ι : Type u_1} {α : Type u_2} [Fintype ι] [Fintype α] (P : ι → Distribution α) (Y : ι → α → ℝ) (hY : ∀ (i : ι) (a : α), Y i a = 0 ∨ Y i a = 1) : 0 ≤ ∑ i : ι, (P i).expect (Y i)

The mean ∑ᵢ 𝔼[Y i] of {0,1}-valued trials is nonnegative.

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

Upper tail before optimizing t: for t ≥ 0 and an upper bound μH on the mean, P(X ≥ k) ≤ exp (μH (eᵗ - 1) - t k).

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

Lower tail before optimizing t: for t ≤ 0 and a lower bound μL on the mean, P(X ≤ k) ≤ exp (μL (eᵗ - 1) - t k).

Counting heads

theorem Dynamics.Distribution.sum_ite_mem_ite_eq_card {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) (ω : ι → Bool) : (∑ i : ι, if i ∈ S then if ω i = true then 1 else 0 else 0) = ↑{i ∈ S | ω i = true}.card

The number of heads among the coins of S as a sum of {0,1} coordinates.

Uniform rounds

theorem Dynamics.Distribution.independent_expect_eq_avg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {γ : Type u_3} [Fintype γ] (P : ι → Distribution γ) (hP : ∀ (i : ι) (a : γ), (P i).weight a = (↑(Fintype.card γ))⁻¹) (f : (ι → γ) → ℝ) : (independent P).expect f = avg f

If every coordinate distribution has the uniform weights (card γ)⁻¹, the independent product is the uniform average over ι → γ.

theorem Dynamics.avg_indicator_le_of_independent {ι : Type u_1} {γ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype γ] (E : (ι → γ) → Prop) [DecidablePred E] {B : ℝ} (hB : 0 ≤ B) (h : ∀ (P : ι → Distribution γ), (∀ (i : ι) (f : γ → ℝ), (P i).expect f = avg f) → (Distribution.independent P).prob E ≤ B) : (avg fun (ω : ι → γ) => if E ω then 1 else 0) ≤ B

Transfer to uniform rounds. A bound on the probability of an event E under every independent product whose factors are uniform ((P i).expect = avg) bounds the uniform average of its indicator over ι → γ. No Nonempty γ is needed: if ι → γ is empty the average vanishes, and if γ is empty but ι → γ is not, then ι is empty.