Example 6: Lasso is $(\mathcal N(\gamma/2, \mathcal Z, \|\cdot\|_\infty), (Y(\mathbf s)/c + 1)\gamma)$-robust

Let $\mathcal Z$ be a compact subset of $\mathbb R^{m+1}$, whose points are written $z = (z^{(y)}, z^{(x)})$ with $z^{(y)} \in \mathbb R$ and $z^{(x)} \in \mathbb R^m$, and let $c > 0$. Let $\mathcal A$ be a Lasso algorithm: for every training set $\mathbf s = (s_1, \dots, s_n)$, $\mathcal A_{\mathbf s} = w$ is a solution of

and let the loss be $l(\mathcal A_{\mathbf s}, z) = |z^{(y)} - \mathcal A_{\mathbf s}(z^{(x)})| = |z^{(y)} - w^\top z^{(x)}|$. Then for every $\gamma > 0$ the Lasso is

Together with the paper's Theorem 1 this gives a generalization bound for the Lasso that holds for every selection of a minimizer.

Formalization Note $\mathbb R^{m+1}$ is ℝ × (Fin m → ℝ), whose Lean norm is the maximum of the absolute values of the $m+1$ coordinates, i.e. $\|\cdot\|_\infty$. The covering number is Mathlib's Metric.coveringNumber (closed balls, centres in $\mathcal Z$) at radius Real.toNNReal (γ/2), converted to ℕ with toNat; its finiteness is not assumed but follows from compactness. The algorithm is any function returning a Lasso minimizer for every training set; $c > 0$ is assumed explicitly.