Lemma 21.7 / Corollary 21.8: the Standard Optimal Algorithm has mistake bound M_SOA(H) ≤ Ldim(H)

Proved

UnderstandingML.soa_mistake_bound

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

littlestone-dimensiononline-learningstandard-optimal-algorithm

Lemma 21.7. SOA enjoys the mistake bound $M_{\mathrm{SOA}}(H) \le \operatorname{Ldim}(H)$ .

With Lemma 21.6 this gives Corollary 21.8: $M_{\mathrm{SOA}}(H) = \operatorname{Ldim}(H)$ and no other algorithm can have $M_A(H) < \operatorname{Ldim}(H)$ .

Preamble

import Definitions.Def_UnderstandingML_Online

open MeasureTheory
open scoped InnerProductSpace

Formal statement

namespace UnderstandingML

/-- **Lemma 21.7** (p. 293). SOA enjoys the mistake bound `M_SOA(H) ≤ Ldim(H)`. With
Lemma 21.6 this is Corollary 21.8: `M_SOA(H) = Ldim(H)` and no algorithm does better. -/
theorem soa_mistake_bound {X : Type*} (H : Set (X → Bool)) :
    mistakeBound (soa H) H ≤ ldim H := 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.1 pp. 292-293, Lemma 21.7 and Corollary 21.8

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).
Endorsed by mikedeng1 · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph