Corollary 3.2: every finite hypothesis class is PAC learnable, by ERM, with sample complexity m_H(ε, δ) ≤ ⌈log(|H|/δ)/ε⌉

Proved

UnderstandingML.finite_class_pac_learnable

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

ermfinite-classespac-learningsample-complexity

Corollary 3.2. Every finite hypothesis class is PAC learnable with sample complexity $m_H(\epsilon, \delta) \le \lceil \log(|H|/\delta)/\epsilon \rceil$ .

Formally: for a nonempty finite class $H$ of measurable hypotheses $X \to \{0,1\}$ , there is a learning algorithm implementing the $ERM_H$ rule that PAC learns $H$ (Definition 3.1) with the sample-complexity function $(\epsilon, \delta) \mapsto \lceil \log(|H|/\delta)/\epsilon \rceil$ ; in particular $H$ is PAC learnable.

Preamble

import Definitions.Def_UnderstandingML_Framework

open MeasureTheory

Formal statement

namespace UnderstandingML

/-- **Corollary 3.2** (p. 44). Every finite hypothesis class is PAC learnable with sample complexity
`m_H(ε, δ) ≤ ⌈log(|H|/δ)/ε⌉`, and (Corollary 2.3) the `ERM_H` rule is a successful learner:
for a nonempty finite class of measurable hypotheses there is an ERM learner that PAC learns `H`
with the sample-complexity function `(ε, δ) ↦ ⌈log(|H|/δ)/ε⌉`; in particular `H` is PAC
learnable. -/
theorem finite_class_pac_learnable {X : Type*} [MeasurableSpace X] (H : Finset (X → Bool))
    (hne : H.Nonempty) (hH : ∀ h ∈ H, Measurable h) :
    (∃ A : Learner (X × Bool) (X → Bool), IsERMLearner loss01 (↑H) A ∧
      IsPACWith (↑H) A (fun ε δ ↦ ⌈Real.log (H.card / δ) / ε⌉₊)) ∧
    PACLearnable (↑H : Set (X → Bool)) := 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, §3.1 p. 44, Corollary 3.2 (rephrasing Corollary 2.3 in the PAC model)

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