Hoeffding and Bernstein bounds on finite product spaces

Concentration for a sum ∑ i, Y i (ω i) of independent coordinates, where ω : Fin n → γ is drawn uniformly (so the coordinates ω i are independent uniform draws from the finite type γ). As everywhere in this library the probability of an event is the average of its indicator, and independence is avg_prod_pi; no measure theory is used.

• one_sub_add_mul_exp_le: Hoeffding's lemma for a Bernoulli variable, 1 - p + p eᵗ ≤ exp(p t + t²/8), proved by two monotonicity arguments.
• avg_hoeffding: Hoeffding's inequality for {0,1}-valued coordinates, P(X ≥ 𝔼X + λ) ≤ exp(-2λ²/n).
• exp_le_bernstein: the scalar inequality behind Bernstein's bound, e^y ≤ 1 + y + y² / (2(1 - u/3)) for y ≤ u < 3, from the monotonicity of (1 + y + y²/(2(1 - y/3))) e^{-y} on either side of 0.
• avg_bernstein: Bernstein's inequality, P(X ≥ 𝔼X + λ) ≤ exp(-λ² / (2σ²(1 + bλ/(3σ²)))) whenever every coordinate satisfies Yᵢ - 𝔼Yᵢ ≤ b and σ² bounds the variance of X.
• avg_hoeffding_lower: Hoeffding's lower tail, and variance_le_avg_of_zero_one: the variance of a {0,1} coordinate is at most its mean.

The multiplicative Chernoff bounds are in Dynamics.Chernoff.

Scalar inequalities

theorem Dynamics.exp_le_one_add_add_sq_div {x : ℝ} (hx3 : x < 3) : Real.exp x ≤ 1 + x + x ^ 2 / (2 * (1 - x / 3))

e^x ≤ 1 + x + x² / (2(1 - x/3)) for every x < 3.

theorem Dynamics.exp_le_bernstein {y u : ℝ} (hyu : y ≤ u) (hu3 : u < 3) : Real.exp y ≤ 1 + y + y ^ 2 / (2 * (1 - u / 3))

The Bernstein scalar inequality: for y ≤ u < 3, e^y ≤ 1 + y + y² / (2(1 - u/3)).

theorem Dynamics.one_sub_add_mul_exp_le {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (t : ℝ) : 1 - p + p * Real.exp t ≤ Real.exp (p * t + t ^ 2 / 8)

Hoeffding's lemma for a Bernoulli variable: for p ∈ [0,1] and every real t, 1 - p + p eᵗ ≤ exp(p t + t²/8).

Tail bounds for sums of independent coordinates

theorem Dynamics.avg_ite_le_one {α : Type u_2} [Fintype α] (P : α → Prop) [DecidablePred P] : (avg fun (a : α) => if P a then 1 else 0) ≤ 1

The average of an indicator is at most 1, also on an empty type.

theorem Dynamics.avg_tail_le_of_mgf {n : ℕ} {γ : Type u_1} [Fintype γ] (X : (Fin n → γ) → ℝ) {t : ℝ} (ht : 0 ≤ t) (k : ℝ) : (avg fun (ω : Fin n → γ) => if k ≤ X ω then 1 else 0) ≤ (avg fun (ω : Fin n → γ) => Real.exp (t * X ω)) * Real.exp (-(t * k))

Markov's inequality applied to exp (t (X - k)): an exponential-moment bound turns into a tail bound.

theorem Dynamics.avg_exp_sum {n : ℕ} {γ : Type u_1} [Fintype γ] (Y : Fin n → γ → ℝ) (t : ℝ) : (avg fun (ω : Fin n → γ) => Real.exp (t * ∑ i : Fin n, Y i (ω i))) = ∏ i : Fin n, avg fun (y : γ) => Real.exp (t * Y i y)

The exponential moment of a sum of independent coordinates factors.

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

Hoeffding's inequality for independent {0,1}-valued coordinates: P(X ≥ 𝔼X + λ) ≤ exp(-2λ²/n).

noncomputable def Dynamics.variance {γ : Type u_1} [Fintype γ] (f : γ → ℝ) : ℝ

The variance of a coordinate, 𝔼[(Y - 𝔼Y)²].

Equations

• Dynamics.variance f = Dynamics.avg fun (y : γ) => (f y - Dynamics.avg f) ^ 2

theorem Dynamics.variance_nonneg {γ : Type u_1} [Fintype γ] (f : γ → ℝ) : 0 ≤ variance f

theorem Dynamics.variance_le_avg_sq {γ : Type u_1} [Fintype γ] [Nonempty γ] (f : γ → ℝ) : variance f ≤ avg fun (y : γ) => f y ^ 2

The variance is at most the second moment.

theorem Dynamics.avg_bernstein {n : ℕ} {γ : Type u_1} [Fintype γ] [Nonempty γ] (Y : Fin n → γ → ℝ) {b σ2 lam : ℝ} (hb : 0 < b) (hYb : ∀ (i : Fin n) (x : γ), Y i x - avg (Y i) ≤ b) (hσ : ∑ i : Fin n, variance (Y i) ≤ σ2) (hσ0 : 0 < σ2) (hlam : 0 ≤ lam) : (avg fun (ω : Fin n → γ) => if ∑ i : Fin n, avg (Y i) + lam ≤ ∑ i : Fin n, Y i (ω i) then 1 else 0) ≤ Real.exp (-(lam ^ 2 / (2 * σ2 * (1 + b * lam / (3 * σ2)))))

Bernstein's inequality (Dubhashi–Panconesi): if every coordinate satisfies Yᵢ - 𝔼Yᵢ ≤ b and σ² is at least the variance of X = ∑ᵢ Yᵢ, then P(X ≥ 𝔼X + λ) ≤ exp(-λ² / (2σ²(1 + bλ/(3σ²)))).

Lower tails and the variance of a {0,1} coordinate

theorem Dynamics.avg_lower_tail_le_of_mgf {n : ℕ} {γ : Type u_1} [Fintype γ] (X : (Fin n → γ) → ℝ) {t : ℝ} (ht : t ≤ 0) (k : ℝ) : (avg fun (ω : Fin n → γ) => if X ω ≤ k then 1 else 0) ≤ (avg fun (ω : Fin n → γ) => Real.exp (t * X ω)) * Real.exp (-(t * k))

Markov's inequality applied to exp (t (X - k)) with t ≤ 0: the lower-tail companion of avg_tail_le_of_mgf.

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

Hoeffding's inequality, lower tail, for independent {0,1}-valued coordinates: P(X ≤ 𝔼X - λ) ≤ exp(-2λ²/n). Replaces Median.avg_hoeffding_lower.

theorem Dynamics.variance_le_avg_of_zero_one {γ : Type u_1} [Fintype γ] {f : γ → ℝ} (hf : ∀ (y : γ), f y = 0 ∨ f y = 1) : variance f ≤ avg f

The variance of a {0,1}-valued coordinate is at most its mean (p (1 - p) ≤ p). Generalizes Median.variance_fcoord_le.