Equation (24.2): for a Bernoulli(θ) sample of size m, |θ̂ − θ| ≤ √(log(2/δ)/(2m)) with probability at least 1 − δ

Proved

UnderstandingML.bernoulli_mle_hoeffding

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

concentrationhoeffding-inequalitymaximum-likelihood

Equation (24.2). Since $\hat\theta$ is the average of $m$ i.i.d. binary random variables we can use Hoeffding's inequality to get that with probability of at least $1-\delta$ over the choice of $S$ we have that $|\hat\theta - \theta| \le \sqrt{\log(2/\delta)/(2m)}$ .

Formally: $m \ge 1$ , $\theta \in [0,1]$ , $\delta \in (0,1)$ , the failure event $\{|\hat\theta - \theta| > \sqrt{\log(2/\delta)/(2m)}\}$ has probability at most $\delta$ under the i.i.d. Bernoulli law.

Preamble

import Definitions.Def_UnderstandingML_Generative

open MeasureTheory ProbabilityTheory
open scoped InnerProductSpace

Formal statement

namespace UnderstandingML

/-- **Equation (24.2)** (p. 343). Since `θ̂` is the average of `m` i.i.d. binary random variables,
by Hoeffding's inequality, with probability of at least `1 − δ` over the choice of `S` we have
`|θ̂ − θ| ≤ √(log(2/δ)/(2m))`. `m ≥ 1`, `δ ∈ (0, 1)`, `θ ∈ [0, 1]`. -/
theorem bernoulli_mle_hoeffding (m : ℕ) (hm : 0 < m) (θ : ℝ) (hθ : θ ∈ Set.Icc (0 : ℝ) 1) (δ : ℝ)
    (hδ : 0 < δ) (hδ1 : δ < 1) :
    iidLaw (bernoulliLaw θ) m {S | Real.sqrt (Real.log (2 / δ) / (2 * m)) < |bernoulliMLE S - θ|} ≤
      ENNReal.ofReal δ := by sorry

end UnderstandingML

Source

Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §24.1 p. 343, Equation (24.2) (Hoeffding's inequality)

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by naimengye · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph