Formal Learning Theory Kernel: Blueprint v1

3.2 The VC Characterization

The main result of this section is:

Theorem 3.7 VC Characterization of PAC Learnability [

Lean: fundamental_theorem

Let \(\mathcal{H}\) be a hypothesis class over domain \(X\). The following are equivalent:

  1. \(\mathcal{H}\) is PAC learnable.

  2. \(\mathcal{H}\) has the uniform convergence property.

  3. \(\mathrm{VCdim}(\mathcal{H}) {\lt} \infty \).

Moreover, if \(d = \mathrm{VCdim}(\mathcal{H}) {\lt} \infty \), then \(\mathcal{H}\) is PAC learnable with sample complexity

\[ m_\mathcal {H}(\varepsilon , \delta ) = O\! \left(\frac{d + \log (1/\delta )}{\varepsilon }\right). \]
Remark 3.8 Refinement formalized in this kernel

The statement of Theorem 3.7 as written here is silent on the measurability of the hypothesis class. The symmetrization argument in Stage 2 below picks up a two-sided ghost-gap bad event on \(X^m \times X^m\) whose measurability is a separate requirement on \(\mathcal{H}\). The literature proof of Krapp and Wirth  [ states this requirement as a Borel hypothesis on the bad event. This kernel formalizes the fundamental theorem under a strictly weaker hypothesis: the bad event need only be null-measurable with respect to the completion of the product measure. The weakening is not cosmetic. Chapter 7 constructs a concept class whose ghost-gap bad event is analytic but not Borel, and thereby witnesses the strict gap between the two hypotheses. The Lean identifier

Lean: WellBehavedVCMeasTarget

names the refined hypothesis used in the kernel statement, and

Lean: KrappWirthWellBehaved

names the Krapp and Wirth version; the implication

Lean: KrappWirthWellBehaved.toWellBehavedVC

sits on one side of the strict gap, and Corollary 7.18 witnesses the other.

The proof proceeds in four stages. Each stage is a separate lemma, and each lemma is a foothold on the ascent.

Stage 1: Finite VC dimension \(\Longrightarrow \) polynomial growth function (Sauer–Shelah).

Stage 2: Polynomial growth function \(\Longrightarrow \) uniform convergence (\(\varepsilon \)-net/symmetrization argument).

Stage 3: Uniform convergence \(\Longrightarrow \) ERM is a PAC learner.

Stage 4 (Converse): Infinite VC dimension \(\Longrightarrow \) not PAC learnable.