## Formalized Name Sauer–Shelah Lemma ## Proof The proof establishes the following stronger claim by induction on $|\mathcal{H}(x_{1:n})|$: for any $x_{1:n}$ and any $Q \subseteq \{1, \ldots, n\}$ nonempty, writing $x_Q$ for the subvector indexed by $Q$, there are at least $|\mathcal{H}(x_{1:n})| - 1$ nonempty subsets $Q \subseteq \{1, \ldots, n\}$ such that $\mathcal{H}$ shatters $x_Q$. To deduce the lemma from the claim: take $x_{1:n}$ maximizing $|\mathcal{H}(x_{1:n})| = s(\mathcal{H}, n)$. Since $\operatorname{VC}(\mathcal{H}) = d$, no $x_Q$ with $|Q| > d$ is shattered. Counting the shattered sets and using the claim gives $s(\mathcal{H}, n) - 1 \leq \sum_{i=1}^{\min(d,n)} \binom{n}{i}$. For $n \geq d$, the right side satisfies $\sum_{i=1}^{d}\binom{n}{i} \leq n^d + \binom{d}{1}n^{d-1} + \cdots + \binom{d}{d} - 1 = (n+1)^d - 1$, so $s(\mathcal{H}, n) \leq (n+1)^d$. For the inductive claim: the base case $|\mathcal{H}(x_{1:n})| = 1$ is vacuous. For the inductive step, take $|\mathcal{H}(x_{1:n})| = k+1$ and choose $j$ such that both $\mathcal{H}^+ = \{h \in \mathcal{H} : h(x_j) = 1\}$ and $\mathcal{H}^- = \{h \in \mathcal{H} : h(x_j) = -1\}$ are nonempty. Let $X^{\pm}$ be the families of subvectors shattered by $\mathcal{H}^{\pm}$ respectively; by induction $|X^-| + |X^+| \geq k - 1$. Subvectors in $X^- \cup X^+$ are all shattered by $\mathcal{H}$ and none contains $x_j$ (since $\mathcal{H}^{\pm}$ assign constant sign at $x_j$). For $x_Q \in X^- \cap X^+$, both $x_Q$ and $x_{Q \cup \{j\}}$ are shattered by $\mathcal{H}$, and $x_j$ itself is shattered. Counting gives at least $1 + |X^- \cup X^+| + |X^- \cap X^+| = 1 + |X^-| + |X^+| \geq k$ shattered sets, completing the induction.