Proof of Theorem 8 — the expected test average loss equals the expected loss

Let $\mathcal Z$ be a measurable space with a probability measure $\mu$, $\mathcal H$ a set of hypotheses, and $l : \mathcal H \times \mathcal Z \to [0, M]$ a loss measurable in its sample argument. Let $n \ge 1$ and let $\mathbf t(n) = (t_1, \dots, t_n) \sim \mu^n$ be $n$ i.i.d. samples. Then for every hypothesis $h \in \mathcal H$

where $L(h, \mathbf t(n)) = \frac1n \sum_{i=1}^n l(h, t_i)$ and $\mathcal L(h) = \mathbb E_{z \sim \mu} l(h, z)$.

In the proof of Theorem 8 this is applied to the fixed hypothesis $h = \mathcal A_{\mathbf s^*(n)}$, turning the generalization gap $|\mathcal L(\mathcal A_{\mathbf s^*(n)}) - L(\mathcal A_{\mathbf s^*(n)}, \mathbf s^*(n))|$ into $|\mathbb E_{\mathbf t(n)} L(\mathcal A_{\mathbf s^*(n)}, \mathbf t(n)) - L(\mathcal A_{\mathbf s^*(n)}, \mathbf s^*(n))|$.

Formalization Note The law of $\mathbf t(n)$ is the product measure Measure.pi (fun _ : Fin n => μ). Measurability of $l(h, \cdot)$ is added (the paper ignores measurability). The case $n = 0$ is excluded, where the average loss is $0$ in Lean.