Hoeffding One-Sided Finite-Sum Bound

Exact statement

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

Copy-safe source

Bounded variables are sub-Gaussian after centering. Once each centered variable has sub-Gaussian MGF parameter $((b_i-a_i)/2)^2$, independence lets those parameters add across the finite sum.

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.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