AcceptedLemma · Statement with omitted proof

Hoeffding inequality for bounded independent variables

A two-sided exponential bound controls the deviation of a sum from its expectation.

Drineas & Mahoney ↗
Source label: lem:hoef

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

A two-sided exponential bound controls the deviation of a sum from its expectation.

\Pr\left\{\left|\sum_i X_i-\sum_i\mathbb EX_i\right|\ge nt\right\}\le2\exp\left(-\frac{2n^2t^2}{\sum_i(a_i-b_i)^2}\right)

Assumptions & context

The variables are independent, have the stated moments and satisfy aᵢ ≤ Xᵢ ≤ bᵢ; t > 0.

Source

Drineas & Mahoney. Lectures on randomized numerical linear algebra.

Source label: lem:hoef

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem hoeffding_inequality
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (n : ℕ) (X : Fin n → Ω → ℝ) (a b : Fin n → ℝ)
    (hindep : ProbabilityTheory.iIndepFun X P)
    (hint : ∀ i, Integrable (X i) P)
    (hL2 : ∀ i, MemLp (X i) 2 P)
    (hbound : ∀ i, ∀ ω, a i ≤ X i ω ∧ X i ω ≤ b i)
    (t : ℝ) (ht : 0 < t) :
    P {ω | (n : ℝ) * t ≤
        |∑ i, X i ω - ∑ i, ∫ ω', X i ω' ∂P|}
      ≤ ENNReal.ofReal
          (2 * Real.exp (-(2 * (n : ℝ) ^ 2 * t ^ 2) / ∑ i, (a i - b i) ^ 2)) := by
  sorry

Complete Lean file and local definitions

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal

namespace RNLAPhaseB.DM2017.LemHoef

/-- Hoeffding's inequality (dm2017, lem:hoef).

Let `X_i`, `i = 1, …, n`, be independent random variables with finite first and
second moments such that `a_i ≤ X_i ≤ b_i` for all `i`. Then for any `t > 0`,
`Pr[|∑ X_i - ∑ E[X_i]| ≥ n t] ≤ 2 exp(-2 n² t² / ∑ (a_i - b_i)²)`.

The random variables live on a sample space `Ω` with probability measure `P`,
indexed by `Fin n` (0-based rather than 1-based). Finite first and second moments
are stated as `Integrable` and `MemLp · 2`. The bounds are pointwise in `ω`.
The expectation `E[X_i]` is the Bochner integral `∫ ω, X i ω ∂P`. -/
theorem hoeffding_inequality
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (n : ℕ) (X : Fin n → Ω → ℝ) (a b : Fin n → ℝ)
    (hindep : ProbabilityTheory.iIndepFun X P)
    (hint : ∀ i, Integrable (X i) P)
    (hL2 : ∀ i, MemLp (X i) 2 P)
    (hbound : ∀ i, ∀ ω, a i ≤ X i ω ∧ X i ω ≤ b i)
    (t : ℝ) (ht : 0 < t) :
    P {ω | (n : ℝ) * t ≤
        |∑ i, X i ω - ∑ i, ∫ ω', X i ω' ∂P|}
      ≤ ENNReal.ofReal
          (2 * Real.exp (-(2 * (n : ℝ) ^ 2 * t ^ 2) / ∑ i, (a i - b i) ^ 2)) := by
  sorry

end RNLAPhaseB.DM2017.LemHoef

How to read the formalization

The probability event retains the source's non-strict threshold. Finite first and second moments are explicit Lean hypotheses.

← Back to all statements