McDiarmid's bounded-differences inequality

A real function of several coordinates has bounded differences c when changing coordinate i alone changes its value by at most c i. If the coordinates are independent, such a function concentrates around its mean: it exceeds the mean by ε, or falls short of it by ε, each with probability at most exp (-2 ε² / ∑ i, c i ^ 2) McDiarmid, Lemma 1.2. For a sum of bounded independent scores this is Hoeffding's inequality [Hoe63].

The proof bounds the moment generating function of f - 𝔼 f by exp (t² ∑ i, c i ^ 2 / 8), by induction on the set of coordinates already averaged out. Averaging out one more coordinate i changes the partial average by a mean-zero amount that lies in an interval of length c i, so Hoeffding's lemma (Mathlib's ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc) bounds its contribution by exp (t² c i ^ 2 / 8). This is the Doob martingale argument, with the martingale written as iterated finite averages. The tail bounds are finite-PMF event probabilities; HasBoundedDifferences.hasSubgaussianMGF_pi records the sub-Gaussian bound in Mathlib's form.

Main definitions

• Cslib.Probability.HasBoundedDifferences: changing one coordinate changes the value boundedly.

Main results

• Cslib.Probability.hasBoundedDifferences_sum: sums of bounded coordinate scores.
• Cslib.Probability.HasBoundedDifferences.sum_pi_mul_exp_le: the moment generating function bound.
• Cslib.Probability.HasBoundedDifferences.hasSubgaussianMGF_pi: the sub-Gaussian form.
• Cslib.Probability.HasBoundedDifferences.pi_ge_mean_add, Cslib.Probability.HasBoundedDifferences.pi_le_mean_sub: McDiarmid's inequality for the upper and lower tails.
• Cslib.Probability.HasBoundedDifferences.pi_abs_sub_mean_ge: the two-sided bound.

References

• C. McDiarmid, On the method of bounded differences, Lemma 1.2
• W. Hoeffding, Probability inequalities for sums of bounded random variables

def Cslib.Probability.HasBoundedDifferences {ι : Type u_1} [DecidableEq ι] {α : ι → Type u_2} (f : ((i : ι) → α i) → ℝ) (c : ι → ℝ) : Prop

A function of several coordinates has bounded differences c if changing coordinate i alone changes its value by at most c i.

theorem Cslib.Probability.HasBoundedDifferences.neg {ι : Type u_1} [DecidableEq ι] {α : ι → Type u_2} {f : ((i : ι) → α i) → ℝ} {c : ι → ℝ} (hf : HasBoundedDifferences f c) : HasBoundedDifferences (fun (x : (i : ι) → α i) => -f x) c

Negation preserves bounded differences.

theorem Cslib.Probability.hasBoundedDifferences_sum {ι : Type u_1} [DecidableEq ι] {α : ι → Type u_2} [Fintype ι] {score : (i : ι) → α i → ℝ} {c : ι → ℝ} (hscore : ∀ (i : ι) (a b : α i), |score i a - score i b| ≤ c i) : HasBoundedDifferences (fun (x : (i : ι) → α i) => ∑ i : ι, score i (x i)) c

A sum of coordinate scores whose i-th score varies by at most c i has bounded differences c.

Hoeffding's lemma and partial averages

McDiarmid's inequality

theorem Cslib.Probability.HasBoundedDifferences.sum_pi_mul_exp_le {ι : Type u_1} [DecidableEq ι] {α : ι → Type u_2} [Fintype ι] [(i : ι) → Fintype (α i)] {f : ((i : ι) → α i) → ℝ} {c : ι → ℝ} (hf : HasBoundedDifferences f c) (p : (i : ι) → PMF (α i)) (t : ℝ) : ∑ x : (i : ι) → α i, ((PMF.pi p) x).toReal * Real.exp (t * (f x - ∑ y : (i : ι) → α i, ((PMF.pi p) y).toReal * f y)) ≤ Real.exp ((t ^ 2 * ∑ i : ι, c i ^ 2) / 8)

The bounded-differences moment bound. For independent coordinates, a function with bounded differences c has centered moment generating function at most exp (t² ∑ i, c i ^ 2 / 8).

theorem Cslib.Probability.HasBoundedDifferences.hasSubgaussianMGF_pi {ι : Type u_1} [DecidableEq ι] {α : ι → Type u_2} [Fintype ι] [(i : ι) → Fintype (α i)] {f : ((i : ι) → α i) → ℝ} {c : ι → ℝ} [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableSingletonClass (α i)] (hf : HasBoundedDifferences f c) (p : (i : ι) → PMF (α i)) : ProbabilityTheory.HasSubgaussianMGF (fun (x : (i : ι) → α i) => f x - ∑ y : (i : ι) → α i, ((PMF.pi p) y).toReal * f y) (∑ i : ι, (‖c i‖₊ / 2) ^ 2) (PMF.pi p).toMeasure

A function of independent coordinates with bounded differences c is sub-Gaussian about its mean with variance proxy ∑ i, (c i / 2) ^ 2.

theorem Cslib.Probability.HasBoundedDifferences.pi_ge_mean_add {ι : Type u_1} [DecidableEq ι] {α : ι → Type u_2} [Fintype ι] [(i : ι) → Fintype (α i)] {f : ((i : ι) → α i) → ℝ} {c : ι → ℝ} (hf : HasBoundedDifferences f c) (p : (i : ι) → PMF (α i)) {ε : ℝ} (hε : 0 ≤ ε) : ((PMF.pi p).toOuterMeasure {x : (i : ι) → α i | ∑ y : (i : ι) → α i, ((PMF.pi p) y).toReal * f y + ε ≤ f x}).toReal ≤ Real.exp (-2 * ε ^ 2 / ∑ i : ι, c i ^ 2)

McDiarmid's inequality, upper tail McDiarmid, Lemma 1.2: a function of independent coordinates with bounded differences c exceeds its mean by ε with probability at most exp (-2 ε² / ∑ i, c i ^ 2).

theorem Cslib.Probability.HasBoundedDifferences.pi_le_mean_sub {ι : Type u_1} [DecidableEq ι] {α : ι → Type u_2} [Fintype ι] [(i : ι) → Fintype (α i)] {f : ((i : ι) → α i) → ℝ} {c : ι → ℝ} (hf : HasBoundedDifferences f c) (p : (i : ι) → PMF (α i)) {ε : ℝ} (hε : 0 ≤ ε) : ((PMF.pi p).toOuterMeasure {x : (i : ι) → α i | f x ≤ ∑ y : (i : ι) → α i, ((PMF.pi p) y).toReal * f y - ε}).toReal ≤ Real.exp (-2 * ε ^ 2 / ∑ i : ι, c i ^ 2)

McDiarmid's inequality, lower tail: a function of independent coordinates with bounded differences c falls below its mean by ε with probability at most exp (-2 ε² / ∑ i, c i ^ 2).

theorem Cslib.Probability.HasBoundedDifferences.pi_abs_sub_mean_ge {ι : Type u_1} [DecidableEq ι] {α : ι → Type u_2} [Fintype ι] [(i : ι) → Fintype (α i)] {f : ((i : ι) → α i) → ℝ} {c : ι → ℝ} (hf : HasBoundedDifferences f c) (p : (i : ι) → PMF (α i)) {ε : ℝ} (hε : 0 ≤ ε) : ((PMF.pi p).toOuterMeasure {x : (i : ι) → α i | ε ≤ |f x - ∑ y : (i : ι) → α i, ((PMF.pi p) y).toReal * f y|}).toReal ≤ 2 * Real.exp (-2 * ε ^ 2 / ∑ i : ι, c i ^ 2)

McDiarmid's inequality, two-sided: a function of independent coordinates with bounded differences c deviates from its mean by ε with probability at most 2 exp (-2 ε² / ∑ i, c i ^ 2).