Concentration inequalities

Non-asymptotic tail and moment bounds: Hoeffding, McDiarmid, Efron–Stein, Khintchine and Paley–Zygmund inequalities, sampling without replacement, sub-Gaussian convex comparison, and hypercontractivity (Bonami–Beckner, p-biased two-point inequalities) on the discrete cube.

• Bonami–Beckner hypercontractivity
• Convex comparison under sub-Gaussian tails
• Efron–Stein inequality
• Hoeffding's inequality
• McDiarmid's inequality

TheoremKhintchine inequality#✓fully proved

For every real \(p > 0\) there are constants \(A_p > 0\) and \(B_p > 0\) such that the following holds for every \(N \in \mathbb{N}\), all real numbers \(a_1, \dots, a_N\) and every probability space. Let \(\varepsilon_1, \dots, \varepsilon_N\) be independent measurable random variables, each almost surely equal to \(1\) or \(-1\) and each with mean \(0\), and let \(S = \sum_{i=1}^N a_i \varepsilon_i\) and \(\|a\|_2 = \big(\sum_{i=1}^N a_i^2\big)^{1/2}\). Then

\[A_p \|a\|_2 \le \big(\mathbb{E}\,|S|^p\big)^{1/p} \le B_p \|a\|_2.\]

MetaMathlibExt.khintchine_inequality · 18 lines

theorem khintchine_inequality :
    ∀ (p : ℝ), 0 < p →
      ∃ (A B : ℝ), 0 < A ∧ 0 < B ∧
        ∀ (N : ℕ) (a : Fin N → ℝ) (Ω : Type*) [MeasurableSpace Ω]
          (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ]
          (ε : Fin N → Ω → ℝ),
          (∀ i, Measurable (ε i)) →
          (∀ i, ∀ᵐ ω ∂μ, ε i ω = 1 ∨ ε i ω = -1) →
          (∀ i, MeasureTheory.integral μ (ε i) = 0) →
          ProbabilityTheory.iIndepFun ε μ →
          A * Real.sqrt (∑ i, (a i) ^ 2) ≤
            Real.rpow
              (MeasureTheory.integral μ (fun ω => Real.rpow |∑ i, a i * ε i ω| p))
              (1 / p) ∧
          Real.rpow
            (MeasureTheory.integral μ (fun ω => Real.rpow |∑ i, a i * ε i ω| p))
            (1 / p) ≤
            B * Real.sqrt (∑ i, (a i) ^ 2)

Sources

• https://en.wikipedia.org/wiki/Khintchine_inequality

TheoremThe Paley–Zygmund inequality#✓fully proved

Let \(Z\) be a real random variable on a probability space with probability measure \(\mathbb{P}\), such that \(Z \ge 0\) almost surely and \(\mathbb{E}[Z^2] < \infty\), and let \(\theta\) be a real number with \(0 \le \theta \le 1\). Then

\[(1-\theta)^2 (\mathbb{E}[Z])^2 \le \mathbb{E}[Z^2] \, \mathbb{P}(Z > \theta \, \mathbb{E}[Z]).\]

When \(\mathbb{E}[Z^2] > 0\), this says \(\mathbb{P}(Z > \theta \, \mathbb{E}[Z]) \ge (1 - \theta)^2 (\mathbb{E}[Z])^2 / \mathbb{E}[Z^2]\).

theorem paley_zygmund [IsProbabilityMeasure μ] {Z : Ω → ℝ} (hZ_nn : 0 ≤ᵐ[μ] Z) (hZ2 : MemLp Z 2 μ)
    {θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) :
    (1 - θ) ^ 2 * (∫ ω, Z ω ∂μ) ^ 2 ≤
      (∫ ω, Z ω ^ 2 ∂μ) * μ.real {ω | θ * ∫ ω, Z ω ∂μ < Z ω}

Used by 1

Used byThree-series necessity, second half of the variance step

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.