Hoeffding's inequality

TheoremTwo-sided Hoeffding inequality for Bernoulli sums#✓fully proved

Let \(X_0, \dots, X_{n-1}\) be independent real random variables on a probability space, each almost everywhere measurable, almost surely equal to \(0\) or \(1\), and with expectation \(p\), and let \(\varepsilon > 0\). Then the probability that \(\lvert X_0 + \dots + X_{n-1} - np \rvert > \varepsilon n\) is at most \(2 e^{-2 \varepsilon^2 n}\).

theorem hoeffding_bernoulli_sum_abs_tail {n : ℕ} (X : Fin n → Ω → ℝ)
    (p ε : ℝ) (h_indep : iIndepFun X μ)
    (hmeas : ∀ i, AEMeasurable (X i) μ)
    (hBernoulli : ∀ i, ∀ᵐ ω ∂μ, X i ω = 0 ∨ X i ω = 1)
    (hexp : ∀ i, ∫ x, X i x ∂μ = p) (hε : 0 < ε) :
    μ.real {ω | ε * (n : ℝ) < |(∑ i, X i ω) - (n : ℝ) * p|} ≤
      2 * Real.exp (-2 * ε ^ 2 * (n : ℝ))

Sources

• https://cs.uwaterloo.ca/journals/JIS/VOL28/Jackson/jackson5.tex (Proposition, Hoeffding's Inequality, Thm. 2 of Hoe63).

TheoremHoeffding lower-tail bound for Bernoulli sums#✓fully proved

Let \(X_0, \dots, X_{n-1}\) be independent real random variables on a probability space, each almost everywhere measurable, almost surely equal to \(0\) or \(1\), and with expectation \(p\), and let \(\varepsilon > 0\). Then the probability that \(X_0 + \dots + X_{n-1} \le n(p - \varepsilon)\) is at most \(e^{-2 \varepsilon^2 n}\).

theorem hoeffding_binomial_lower_tail {Ω : Type*}
    [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
    [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ}
    (X : Fin n → Ω → ℝ) (p ε : ℝ)
    (h_indep : ProbabilityTheory.iIndepFun X μ)
    (hmeas : ∀ i, AEMeasurable (X i) μ)
    (hBernoulli : ∀ i, ∀ᵐ ω ∂μ, X i ω = 0 ∨ X i ω = 1)
    (hexp : ∀ i, ∫ x, X i x ∂μ = p)
    (hε : 0 < ε) :
    μ.real {ω | (∑ i, X i ω) ≤ (n : ℝ) * (p - ε)} ≤
      Real.exp (-2 * ε ^ 2 * (n : ℝ))

Sources

• Griffiths JIS VOL16, source lines 167-191, https://cs.uwaterloo.ca/journals/JIS/VOL16/Griffiths/griffiths22.tex.

TheoremHoeffding's bound for sampling without replacement#✓fully proved

Hoeffding's upper-tail bound for sampling without replacement, stated as a count.

Among the n-element subsets S of s, at most exp (-2 * n * t ^ 2) * choose (#s) n satisfy n * mean(c) + t * n * R ≤ ∑ i ∈ S, c i. The event is non-strict; n = 0 and #s < n are included without separate assumptions.

theorem card_sample_tail_le (s : Finset ι) (c : ι → ℝ) {R t : ℝ} (hR : 0 < R)
    (hc : ∀ i ∈ s, 0 ≤ c i ∧ c i ≤ R) (hs : s.Nonempty) (n : ℕ) (ht : 0 ≤ t) :
    (#{S ∈ powersetCard n s |
        n * ((∑ i ∈ s, c i) / #s) + t * n * R ≤ ∑ i ∈ S, c i} : ℝ) ≤
      Real.exp (-(2 * n * t ^ 2)) * ((#s).choose n : ℝ)

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.