7.2 The analytic measurability bridge
Analytic sets are the sets obtainable as continuous images of Polish spaces, equivalently, the projections of Borel sets in a product of Polish spaces, equivalently, the result of the Souslin operation applied to a Borel scheme. Every Borel set is analytic, the converse fails in the strongest possible way (there exist analytic sets of every cardinality up to the continuum that are not Borel), and the class of analytic sets is strictly larger than the Borel class while staying manageable under projection. This is classical, and Kechris [ is the standard modern reference.
Let \(Y\) and \(Z\) be standard Borel spaces and let \(B \subseteq Y \times Z\) be Borel. The projection \(\pi _Z(B) = \{ \, z : \exists y,\ (y,z) \in B\, \} \) is an analytic subset of \(Z\). This is the defining property of analytic sets in the Kechris formulation.
For every Borel-parameterized concept class \(C\) with parameter space \(\Theta \), every \(m\), and every \(\varepsilon {\gt} 0\), the parameterized ghost-gap bad event \(\mathrm{Bad}_{\mathrm{eval}}(m, \varepsilon )\) is an analytic subset of \(X^m \times X^m\) whenever \(X\) is standard Borel.
The condition \(|\hat{R}_{S'}(\mathrm{eval}(\theta ,\cdot )) - \hat{R}_S(\mathrm{eval}(\theta ,\cdot ))| {\gt} \varepsilon \) is jointly Borel in \((\theta , S, S') \in \Theta \times X^m \times X^m\) because \(\mathrm{eval}\) is jointly measurable and the empirical risks are finite sums of indicator evaluations. The bad event \(\mathrm{Bad}_{\mathrm{eval}}(m, \varepsilon )\) is the projection of this Borel set onto the last two factors, hence analytic by Lemma 7.7.
Corollary 7.8 reduces the measurability question for the bad event to a single question: are analytic sets null-measurable with respect to every Borel probability measure? That question was answered in 1955 by Gustave Choquet. The answer is yes, and the proof route is the capacitability theorem.
Lean: MeasureTheory.AnalyticSet.compactCap_eq
Let \(X\) be a Polish space and let \(\mu \) be a Borel probability measure on \(X\). For every analytic set \(A \subseteq X\),
where \(\mu ^*\) denotes the outer measure induced by \(\mu \). In particular, \(A\) is \(\mu \)-capacitable: its outer measure equals its inner measure, and \(A\) lies in the completion of the Borel \(\sigma \)-algebra with respect to \(\mu \).
The argument proceeds by showing that \(\mu ^*\) extended to analytic sets is a Choquet capacity: it is countably subadditive, monotone, and continuous from below on increasing unions, and continuous from above on decreasing intersections of compact sets. Any Choquet capacity is capacitable on analytic sets by an alternating game between approximating unions and intersections of compact sets. The compact approximations then converge in outer measure to \(\mu ^*(A)\) from below, and the Borel completion absorbs the gap. The full formalization runs 416 lines in FLT_Proofs.PureMath.ChoquetCapacity and is independent of learning theory; it is written in a form suitable for contribution to Mathlib as a standalone result. The blueprint treats it as a black box from here on.
Lean: analyticSet_nullMeasurableSet
Every analytic set in a Polish space is null-measurable with respect to every Borel probability measure.
By Theorem 7.9, the outer and inner measures of an analytic set agree, which is equivalent to the set lying in the \(\mu \)-completion of the Borel \(\sigma \)-algebra.
The bridge closes with a one-line composition: Corollary 7.8 says the bad event is analytic, Corollary 7.10 says analytic sets are null-measurable, and null-measurability of the bad event is exactly WellBehavedVCMeasTarget.
Lean: analyticSet_nullMeasurableSet_ghostPairs
Every Borel-parameterized concept class over a standard Borel space \(X\) satisfies WellBehavedVCMeasTarget.
The fundamental theorem of statistical learning (Theorem 3.7) therefore applies, in the kernel’s formulation, to every Borel-parameterized concept class, including the classes for which Krapp and Wirth originally stated it under the stronger Borel hypothesis. The refinement is automatic for practical examples. The question that remains is whether it is strictly weaker, and it is to that question we now turn.