Theorem 21.3: for finite H, the Halving algorithm has mistake bound M_Halving(H) ≤ log₂|H|

Proved

UnderstandingML.halving_mistake_bound

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

halvingmistake-boundonline-learning

Theorem 21.3. Let $H$ be a finite hypothesis class. The Halving algorithm enjoys the mistake bound $M_{\mathrm{Halving}}(H) \le \log_2(|H|)$ .

Formally: $M_{\mathrm{Halving}}(H) \le \lfloor\log_2|H|\rfloor$ , the number of mistakes being an integer; Halving predicts the majority label of the version space, $1$ in case of a tie.

Preamble

import Definitions.Def_UnderstandingML_Online

open MeasureTheory
open scoped InnerProductSpace

Formal statement

namespace UnderstandingML

/-- **Theorem 21.3** (p. 290). Let `H` be a finite hypothesis class. The Halving algorithm
enjoys the mistake bound `M_Halving(H) ≤ log₂(|H|)` (the number of mistakes being an integer,
`⌊log₂ |H|⌋`). -/
theorem halving_mistake_bound {X : Type*} (H : Set (X → Bool)) (hH : H.Finite) :
    mistakeBound (halving H) H ≤ (Nat.log 2 H.ncard : ℕ∞) := 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, §21.1 p. 290, Theorem 21.3

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