Skip to main content
Theorem pageFormalizedPublicly reproducible

Hoeffding One-Sided Finite-Sum Bound

This page traces one bounded independent finite-sum Hoeffding claim from the informal theorem statement to the checked Lean declaration, then shows which diagnostics test the assumptions. It does not claim that the whole concentration page or the finite-class uniform-convergence theorem is fully formalized.

Exact statement

This is the governed exact statement. The Lean wrapper below checks this one-sided centered finite-sum scope, not every common textbook corollary of Hoeffding's inequality.

Exact LaTeX source

\[\Pr\!\left[\sum_{i \in I} (X_i-\mathbb{E}X_i) \geq \epsilon\right] \leq \exp\!\left(-\frac{\epsilon^2}{2\sum_{i \in I} ((b_i-a_i)/2)^2}\right)\]

Assumptions

  • finite independent family
  • each variable is almost surely bounded in an interval
  • epsilon >= 0

Lean declaration

Declaration
TheoremPath.Probability.Concentration.hoeffdingBoundedFiniteSumTail
File
verification/lean/TheoremPath/Probability/Concentration.leanFormalSLT/Probability/Concentration.lean
Lean version
4.30.0-rc2
Checked
2026-04-28T00:00:00.000Z
theorem hoeffdingBoundedFiniteSumTail
    {Ω ι : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : ι → Ω → ℝ} (hIndep : iIndepFun X μ)
    {a b : ι → ℝ} {s : Finset ι}
    (hMeas : ∀ i ∈ s, AEMeasurable (X i) μ)
    (hBound : ∀ i ∈ s, ∀ᵐ ω ∂μ, X i ω ∈ Set.Icc (a i) (b i))
    {ε : ℝ} (hε : 0 ≤ ε) :
    μ.real {ω | ε ≤ ∑ i ∈ s, (X i ω - μ[X i])}
      ≤ Real.exp
          (-ε ^ 2 / (2 * (↑(∑ i ∈ s, ((‖b i - a i‖₊ / 2) ^ (2 : ℕ))) : ℝ)))

The proof composes existing mathlib facts rather than reproving concentration theory from scratch. That is intentional: the checked artifact is the exact TheoremPath-facing declaration.

Dependency path

upstream lemmaFormalized

Hoeffding's Lemma

claim:subgaussian-random-variables::hoeffding-lemma

TheoremPath.Probability.Concentration.hoeffdingLemmaBoundedCenteredSubgaussianMGF

probability dependencyFormalized

Finite Union Bound for Probability Measures

claim:kolmogorov-probability-axioms::probability-measure-finite-union-bound

TheoremPath.Probability.KolmogorovAxioms.probabilityMeasureFiniteUnionBound

downstream learning-theory targetDependency formalized

Uniform Convergence for Finite Classes

claim:uniform-convergence::finite-class-uniform-convergence

TheoremPath.LearningTheory.UniformConvergence.finiteClassEpsilonRepresentativeHighProbabilityFromOneSidedTails