Lemma 29.4 (Natarajan): |H| ≤ |X|^{Ndim(H)} k^{2 Ndim(H)} for a class of functions from a finite X to [k]
ProvedUnderstandingML.natarajan_lemmagrowth-functionnatarajan-dimensionsauer-lemma
Lemma 29.4 (Natarajan). .
Formally: for a finite domain , a finite label set of size , and .
Preamble
import Definitions.Def_UnderstandingML_MulticlassLearnability open MeasureTheory open scoped InnerProductSpace
Formal statement
namespace UnderstandingML
/-- **Lemma 29.4 (Natarajan)** (p. 404). For a class `H` of functions from a finite domain `X`
to `[k]`, `|H| ≤ |X|^{Ndim(H)} · k^{2 Ndim(H)}`. -/
theorem natarajan_lemma {X Y : Type*} [Fintype X] [Fintype Y] (H : Set (X → Y)) (d : ℕ)
(hd : ndim H = d) :
H.ncard ≤ Fintype.card X ^ d * Fintype.card Y ^ (2 * d) := 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, §29.2.1 p. 404, Lemma 29.4
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.