theorem Concentration.hoeffding_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {Y : Fin n → Ω → ℝ} (hindep : ProbabilityTheory.iIndepFun Y μ) (hbound : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, |Y i ω| ≤ 1) {ε : ℝ} (hε : 0 < ε) : μ.real {ω : Ω | ε * ↑n ≤ ∑ i : Fin n, Y i ω - ∑ i : Fin n, ∫ (ω' : Ω), Y i ω' ∂μ} ≤ 2 * Real.exp (-(ε ^ 2 / (2 + ε)) * ↑n)