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.
Statement (informal)
The governed claim has no exact TeX statement, so this section shows its informal summary. The Lean wrapper below checks a narrower declaration.
Bounded variables are sub-Gaussian after centering. Once each centered variable has sub-Gaussian MGF parameter ((bi−ai)/2)2, independence lets those parameters add across the finite sum.
Assumptions
finite independent family
each variable is almost surely bounded in an interval
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.