Hoeffding's upper-tail inequality for a sum of bounded independent variables

A packaged, optimized Chernoff/Hoeffding upper tail: for finitely many independent random variables X i on a probability space, each valued in [0,1], the sum exceeds its mean by t ≥ 0 with probability at most exp(−2t²/n).

Mathlib provides the single-variable Hoeffding lemma (hasSubgaussianMGF_of_mem_Icc) and the sub-Gaussian sum machinery (HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun), but not the packaged exp(−2t²/n) upper tail for a sum of [0,1]-variables. This file assembles it: center each summand, obtain sub-Gaussian parameter 1/4 per variable, combine by independence, and apply the optimized Chernoff bound.

• Contrib.Hoeffding.hoeffding_upper — the upper-tail bound.

Sorry-free and axiom-clean [propext, Classical.choice, Quot.sound].

theorem Contrib.Hoeffding.hoeffding_upper {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {n : ℕ} (X : Fin n → Ω → ℝ) (hmeas : ∀ (i : Fin n), Measurable (X i)) (hindep : ProbabilityTheory.iIndepFun X MeasureTheory.volume) (h01 : ∀ (i : Fin n), ∀ᵐ (ω : Ω), X i ω ∈ Set.Icc 0 1) (t : ℝ) (ht : 0 ≤ t) : MeasureTheory.volume {ω : Ω | ∑ i : Fin n, X i ω ≥ (∑ i : Fin n, ∫ (ω : Ω), X i ω) + t} ≤ ENNReal.ofReal (Real.exp (-2 * t ^ 2 / ↑n))

Hoeffding upper tail. For finitely many independent random variables X i on a probability space, each valued in [0,1], the sum exceeds its mean by t ≥ 0 with probability at most exp(−2t²/n).

The proof centers each summand, applies Mathlib's Hoeffding lemma to obtain sub-Gaussian parameter 1/4, combines these bounds using independence, and then applies the optimized Chernoff bound. Measurability and boundedness imply the integrability needed for the expectations.