McDiarmid's inequality

TheoremMcDiarmid's inequality when the sensitivities are not all zero#✓fully proved

Let \(n \in \mathbb{N}\), let \(\alpha\) be a finite nonempty set with weights \(p : \alpha \to \mathbb{R}\) such that \(p(a) \ge 0\) for all \(a\) and \(\sum_{a \in \alpha} p(a) = 1\), and give each \(x \in \alpha^n\) the product weight \(P(x) = \prod_{i\lt n} p(x_i)\). Let \(f : \alpha^n \to \mathbb{R}\) and let \(c_0, \dots, c_{n-1} \ge 0\) be such that \(|f(x) - f(y)| \le c_i\) whenever \(x, y \in \alpha^n\) agree in every coordinate other than \(i\), and suppose \(\sum_{i\lt n} c_i^2 > 0\). Write \(\mu = \sum_{x \in \alpha^n} P(x) f(x)\) for the mean of \(f\). Then for every real \(t > 0\),

\[ \sum_{x \in \alpha^n,\ f(x) - \mu \ge t} P(x) \le \exp\Big(-\frac{2t^2}{\sum_{i\lt n} c_i^2}\Big). \]
MathlibExt.Probability.McDiarmid.mcdiarmid_one_sided_finite_iid_general · 18 lines 
theorem mcdiarmid_one_sided_finite_iid_general
    {α : Type*} [Fintype α] [Nonempty α]
    {n : ℕ}
    (p : α → ℝ)
    (hp_nonneg : ∀ a, 0 ≤ p a)
    (hp_sum : ∑ a : α, p a = 1)
    (f : (Fin n → α) → ℝ)
    (c : Fin n → ℝ)
    (hc_nonneg : ∀ i, 0 ≤ c i)
    (hc_pos : 0 < ∑ i : Fin n, c i ^ 2)
    (t : ℝ) (ht : 0 < t)
    (hbd : ∀ (i : Fin n) (x y : Fin n → α),
      (∀ j, j ≠ i → x j = y j) → |f x - f y| ≤ c i) :
    let mu : ℝ := ∑ x : Fin n → α, (∏ i : Fin n, p (x i)) * f x
    let prob : ℝ :=
      ∑ x ∈ (Finset.univ.filter fun x => decide (t ≤ f x - mu)),
        ∏ i : Fin n, p (x i)
    prob ≤ Real.exp (-2 * t ^ 2 / ∑ i : Fin n, c i ^ 2)
Used by 1
Used byMcDiarmid's bounded-differences inequality, finite i.i.d. case

TheoremThe upper tail vanishes when every sensitivity is zero#✓fully proved

Let \(n \in \mathbb{N}\), let \(\alpha\) be a finite nonempty set with weights \(p : \alpha \to \mathbb{R}\) such that \(p(a) \ge 0\) for all \(a\) and \(\sum_{a \in \alpha} p(a) = 1\), and give each \(x \in \alpha^n\) the product weight \(P(x) = \prod_{i\lt n} p(x_i)\). Let \(f : \alpha^n \to \mathbb{R}\) and let \(c_0, \dots, c_{n-1} \ge 0\) be such that \(|f(x) - f(y)| \le c_i\) whenever \(x, y \in \alpha^n\) agree in every coordinate other than \(i\), and suppose \(\sum_{i\lt n} c_i^2 = 0\). Write \(\mu = \sum_{x \in \alpha^n} P(x) f(x)\) for the mean of \(f\). Then for every real \(t > 0\),

\[ \sum_{x \in \alpha^n,\ f(x) - \mu \ge t} P(x) = 0. \]

Indeed, changing one coordinate never changes \(f\), so the upper tail is empty.

MathlibExt.Probability.McDiarmid.mcdiarmid_one_sided_finite_iid_of_sum_sq_eq_zero · 18 lines 
theorem mcdiarmid_one_sided_finite_iid_of_sum_sq_eq_zero
    {α : Type*} [Fintype α] [Nonempty α]
    {n : ℕ}
    (p : α → ℝ)
    (hp_nonneg : ∀ a, 0 ≤ p a)
    (hp_sum : ∑ a : α, p a = 1)
    (f : (Fin n → α) → ℝ)
    (c : Fin n → ℝ)
    (hc_nonneg : ∀ i, 0 ≤ c i)
    (hc_zero : ∑ i : Fin n, c i ^ 2 = 0)
    (t : ℝ) (ht : 0 < t)
    (hbd : ∀ (i : Fin n) (x y : Fin n → α),
      (∀ j, j ≠ i → x j = y j) → |f x - f y| ≤ c i) :
    let mu : ℝ := ∑ x : Fin n → α, (∏ i : Fin n, p (x i)) * f x
    let prob : ℝ :=
      ∑ x ∈ (Finset.univ.filter fun x => decide (t ≤ f x - mu)),
        ∏ i : Fin n, p (x i)
    prob = 0
Used by 1
Used byMcDiarmid's bounded-differences inequality, finite i.i.d. case

TheoremMcDiarmid's bounded-differences inequality, finite i.i.d. case#✓fully proved

Let \(n \in \mathbb{N}\), let \(\alpha\) be a finite nonempty set with weights \(p : \alpha \to \mathbb{R}\) such that \(p(a) \ge 0\) for all \(a\) and \(\sum_{a \in \alpha} p(a) = 1\), and give each \(x \in \alpha^n\) the product weight \(P(x) = \prod_{i\lt n} p(x_i)\). Let \(f : \alpha^n \to \mathbb{R}\) and let \(c_0, \dots, c_{n-1} \ge 0\) be such that \(|f(x) - f(y)| \le c_i\) whenever \(x, y \in \alpha^n\) agree in every coordinate other than \(i\). Write \(\mu = \sum_{x \in \alpha^n} P(x) f(x)\) for the mean of \(f\). Then for every real \(t > 0\),

\[ \sum_{x \in \alpha^n,\ f(x) - \mu \ge t} P(x) \le \exp\Big(-\frac{2t^2}{\sum_{i\lt n} c_i^2}\Big), \]

where a quotient by \(0\) is read as \(0\), so the bound is \(1\) when every \(c_i\) is \(0\).

MathlibExt.Probability.McDiarmid.mcdiarmid_one_sided_finite_iid · 17 lines 
theorem mcdiarmid_one_sided_finite_iid
    {α : Type*} [Fintype α] [DecidableEq α] [Nonempty α]
    {n : ℕ}
    (p : α → ℝ)
    (hp_nonneg : ∀ a, 0 ≤ p a)
    (hp_sum : ∑ a : α, p a = 1)
    (f : (Fin n → α) → ℝ)
    (c : Fin n → ℝ)
    (hc_nonneg : ∀ i, 0 ≤ c i)
    (t : ℝ) (ht : 0 < t)
    (hbd : ∀ (i : Fin n) (x y : Fin n → α),
      (∀ j, j ≠ i → x j = y j) → |f x - f y| ≤ c i) :
    let mu : ℝ := ∑ x : Fin n → α, (∏ i : Fin n, p (x i)) * f x
    let prob : ℝ :=
      ∑ x ∈ (Finset.univ.filter fun x => decide (t ≤ f x - mu)),
        ∏ i : Fin n, p (x i)
    prob ≤ Real.exp (-2 * t ^ 2 / ∑ i : Fin n, c i ^ 2)
Sources
  • C. McDiarmid, Surveys in Combinatorics 1989, 148-188, DOI 10.1017/CBO9781107359949.008. When every c i is 0 (including n = 0), the right-hand side is Real.exp 0 = 1 by Lean's convention x / 0 = 0; mcdiarmid_one_sided_finite_iid_of_sum_sq_eq_zero gives the sharp value prob = 0 there, and mcdiarmid_one_sided_finite_iid_general covers 0 < ∑ i, c i ^ 2. The instance [DecidableEq α] is unused and keeps the source's shape.
Uses 2
Proof usesMcDiarmid's inequality when the sensitivities are not all zero · The upper tail vanishes when every sensitivity is zero
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.