Machine Learning

Motivation

Policy gradient methods are the main family of reinforcement learning algorithms that search directly over a parameterized class of stochastic policies $\pi_\theta$, $\theta\in\mathbb R^d$, by stochastic gradient ascent on the expected discounted return. They underlie REINFORCE, actor-critic methods and their deep-learning descendants. The return is a nonconvex function of $\theta$, and the gradient is available only through Monte Carlo samples of trajectories, so the basic question is what the iterates of such a method converge to.

Classical analyses of actor-critic algorithms (Konda and Tsitsiklis, 2003) use the ODE method of stochastic approximation and assume that the gradient estimate is unbiased. In the infinite-horizon discounted setting, a trajectory of finite length cannot by itself produce an unbiased sample of the gradient. Zhang, Koppel, Zhu and Başar (arXiv:1906.08383, SIAM J. Control Optim. 58(6), 2020) resolve this with random horizons: drawing the trajectory lengths from geometric distributions makes the resulting estimate exactly unbiased and almost surely bounded. They then prove convergence of the resulting random-horizon policy gradient (RPG) algorithm with the supermartingale convergence theorem, an optimization argument that also yields rates. This mission formalizes that first part of the paper (§2–§4 and App. A.1–A.4). The paper's later results on escaping saddle points are not part of it.

Setting

A finite Markov decision process is a tuple $(\mathcal S,\mathcal A,P,R,\gamma)$: finite state and action sets, transition probabilities $P(s'\mid s,a)$, rewards $R(s,a)$ and a discount factor $\gamma\in(0,1)$. A stochastic policy $\pi$ gives a probability vector $\pi(\cdot\mid s)$ on $\mathcal A$ at each state. Its value $V_\pi(s)=\mathbb E\big(\sum_{t\ge0}\gamma^tR(s_t,a_t)\mid s_0=s\big)$ and Q-function $Q_\pi(s,a)$ are the expected discounted returns from a state, respectively a state-action pair.

A parameterized policy assigns to each $\theta\in\mathbb R^d$ a policy $\pi_\theta$. Fix an initial state $s_0$. The objective is

$$J(\theta)=V_{\pi_\theta}(s_0),\qquad \max_{\theta\in\mathbb R^d}J(\theta).$$

The score function is $\nabla_\theta\log\pi_\theta(a\mid s)$. The discounted state-occupancy measure is $\rho_{\pi_\theta}(s)=(1-\gamma)\sum_{t\ge0}\gamma^tp(s_t=s\mid s_0,\pi_\theta)$, and $\rho_\theta(s,a)=\rho_{\pi_\theta}(s)\pi_\theta(a\mid s)$.

Assumption 3.1 asks for $|R(s,a)|\le U_R$ and for a differentiable policy whose score exists, is $L_\Theta$-Lipschitz in $\theta$ and is bounded in norm by $B_\Theta>0$. Two constants recur below:

$$L=\frac{U_RL_\Theta}{(1-\gamma)^2}+\frac{(1+\gamma)U_RB_\Theta^2}{(1-\gamma)^3},\qquad \hat\ell=\frac{B_\Theta U_R}{(1-\gamma)(1-\gamma^{1/2})}.$$

The RPG algorithm (Algorithm 3) works as follows at the current iterate $\theta_k$:

1. Draw a horizon $T\sim\mathrm{Geom}(1-\gamma)$ and simulate $s_0,a_0,\dots,s_T,a_T$ under $\pi_{\theta_k}$.
2. From the last pair $(s_T,a_T)$, the subroutine EstQ draws an independent $T'\sim\mathrm{Geom}(1-\gamma^{1/2})$, rolls out $T'$ further steps and returns $\hat Q=\sum_{t=0}^{T'}\gamma^{t/2}R(s_t,a_t)$.
3. Update

$$\theta_{k+1}=\theta_k+\alpha_k\hat\nabla J(\theta_k),\qquad \hat\nabla J(\theta)=\frac{1}{1-\gamma}\hat Q\,\nabla\log\pi_\theta(a_T\mid s_T).$$

Assumption 4.1 is the Robbins–Monro condition $\sum_k\alpha_k=\infty$, $\sum_k\alpha_k^2<\infty$.

Formalization targets

Goal: Theorem 4.2, in the form its proof establishes

Under Assumptions 3.1 and 4.1, almost surely

$$\lim_{k\to\infty}\|\nabla J(\theta_k)\|=0,$$

and almost surely every cluster point $\bar\theta$ of $(\theta_k)$ satisfies $\nabla J(\bar\theta)=0$. The page states the conclusion as "$\lim_k\theta_k\in\Theta^*$", where $\Theta^*$ is the set of stationary points. Read literally, that asserts convergence of $\theta_k$, which fails when $J$ has no stationary point at all (one state, two actions, a softmax policy). The goal states what the proof on p. 30 concludes.

Milestones

1. $|Q_\pi(s,a)|,|V_\pi(s)|\le U_R/(1-\gamma)$ (p. 6).
2. The policy gradient theorem (3.4): $\nabla J(\theta)=\frac1{1-\gamma}\mathbb E_{(s,a)\sim\rho_\theta}[\nabla\log\pi_\theta(a\mid s)Q_{\pi_\theta}(s,a)]$.
3. Lemma 3.2: $\nabla J$ is $L$-Lipschitz.
4. Theorem 3.4, $\hat\nabla J$ clauses: $\mathbb E\hat\nabla J(\theta)=\nabla J(\theta)$, $\|\nabla J(\theta)\|\le B_\Theta U_R/(1-\gamma)^2$, $\|\hat\nabla J(\theta)\|\le\hat\ell$ a.s.
5. Lemma A.1: the ascent inequality (A.23), and $W_k=J(\theta_k)-L\hat\ell^2\sum_{j\ge k}\alpha_j^2$ is a bounded submartingale with $\mathbb E[W_{k+1}\mid\mathcal F_k]\ge W_k+\alpha_k\|\nabla J(\theta_k)\|^2$.
6. (A.26): $\sum_k\alpha_k\|\nabla J(\theta_k)\|^2<\infty$ a.s.
7. (A.27): $\liminf_k\|\nabla J(\theta_k)\|=0$ a.s.

Companion: Corollary 4.4 in its explicit form (A.37)

With constant stepsize $\alpha>0$ and Assumption 3.1 only, for every $k\ge1$,

$$\frac1k\sum_{m=1}^k\mathbb E\|\nabla J(\theta_m)\|^2\le\frac{1}{k\alpha}\cdot\frac{2U_R}{1-\gamma}+L\alpha\hat\ell^2.$$

Significance

The theorem shows that Monte Carlo policy gradient, with a sampling scheme that can be implemented from simulated trajectories alone, behaves like an exact stochastic gradient method on a smooth nonconvex objective. It needs no ODE approximation, no two-timescale critic and no assumption that the estimate is unbiased: unbiasedness is proved (Theorem 3.4). The same estimates give the finite-time bound of Corollary 4.4 and are the starting point of the paper's second part, which adds perturbations to escape saddle points.

To our knowledge none of these results has been machine-checked. The mission's work is to formalize the known proof: the infinite-horizon policy gradient theorem with a vector parameter, the smoothness bound with its explicit constant, the exact law of the random-horizon estimator and its moments, and the supermartingale argument. The formal statements also repair three misprints of the source: the conclusion of Theorem 4.2, the tail $\sum_{j=k}^\infty\alpha_k^2$ of (A.22), which is read as $\sum_{j\ge k}\alpha_j^2$, and the $O(\cdot)$ of Corollary 4.4, which is replaced by its explicit form (A.37).

Difficulty

Each step of the argument is standard on paper. The work is in the parts that the paper treats in one line:

• Unbiasedness. It rests on two separate identities. The law of the last state of a $\mathrm{Geom}(1-\gamma)$-length trajectory is $\rho_{\pi_\theta}$. A $\gamma^{1/2}$-discounted sum over a $\mathrm{Geom}(1-\gamma^{1/2})$ horizon has the mean of a $\gamma$-discounted infinite sum. Both are exchanges of infinite sums over trajectories of unbounded length.
• Smoothness. Lemma 3.2 requires differentiating $J$ twice through an infinite series of policy-dependent transition matrices, with bounds uniform in $\theta$.
• The final step. (A.26) and the non-summability of the stepsizes give only $\liminf\|\nabla J(\theta_k)\|=0$. Upgrading this to a limit needs a separate pathwise argument, which uses the Lipschitz continuity of $\nabla J$ and the almost sure convergence of the martingale part of the iterates. The tempting first idea, that a summable series with non-summable weights forces its terms to zero, is false.

Formalization scope

• Finite case. The state and action spaces are finite types. The paper also allows compact real vector spaces; this mission does not cover them. Values, Q-functions and occupation probabilities are the published FoundationsML layer (PolicyValue, QFunction, OccupationDist, IsPolicy, IsTransitionKernel). $\mathbb R^d$ is EuclideanSpace ℝ (Fin d), and $\nabla$ is Mathlib's gradient.
• Assumption 3.1 includes $\pi_\theta(a\mid s)>0$: this is the reading of "the score function exists", since $\log 0$ is a junk value in Lean. It also states $L_\Theta\ge0$, which is implicit in "$L_\Theta$-Lipschitz".
• The algorithm is encoded by its exact sampling law. rpgLaw θ is the law of $\hat\nabla J(\theta)$, built from the geometric horizons, the trajectory probabilities and EstQ. A run is a filtered probability space carrying $\theta_k$ and $g_k$ with $\theta_{k+1}=\theta_k+\alpha_kg_k$ on every path, $\theta_k$ adapted, and the conditional law of $g_k$ given $\mathcal F_k$ equal to rpgLaw θ_k.
• Ruled out. Postulating an abstract "unbiased bounded oracle" in place of rpgLaw would assume Theorem 3.4 and turn the goal into generic SGD; that encoding is ruled out. A sorry-free example shows that the run hypothesis is satisfiable and that rpgLaw is a probability measure.
• Stepsizes and limits. The stepsizes are positive; the page says only "stepsize", and its proofs divide by $\alpha_k$. Divergence of $\sum\alpha_k$ is Tendsto of the partial sums to $+\infty$. "Cluster point" is MapClusterPt.
• Contributions welcome: proofs of any milestone, in particular the infinite-horizon policy gradient theorem with vector parameters and the unbiasedness of rpgLaw. These are reusable for every Monte Carlo policy gradient analysis.

Selected references

• K. Zhang, A. Koppel, H. Zhu, T. Başar, Global Convergence of Policy Gradient Methods to (Almost) Locally Optimal Policies, SIAM J. Control Optim. 58(6), 2020. https://arxiv.org/abs/1906.08383 (v3 is the source of this mission)
• R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, NeurIPS 1999. https://papers.nips.cc/paper/1713-policy-gradient-methods-for-reinforcement-learning-with-function-approximation
• V. R. Konda, J. N. Tsitsiklis, On Actor-Critic Algorithms, SIAM J. Control Optim. 42(4), 2003. https://doi.org/10.1137/S0363012901385691
• D. P. Bertsekas, J. N. Tsitsiklis, Gradient Convergence in Gradient Methods with Errors, SIAM J. Optim. 10(3), 2000. https://doi.org/10.1137/S1052623497331063
• H. Robbins, D. Siegmund, A Convergence Theorem for Non Negative Almost Supermartingales and Some Applications, in Optimizing Methods in Statistics, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8

Why saddle points matter for nonconvex learning

Training a model in machine learning usually means minimizing a nonconvex function $f:\mathbb R^d\to\mathbb R$ with first-order methods. Finding a global minimum of a general nonconvex function is NP-hard, so the classical guarantee for gradient descent (GD), $x_{t+1}=x_t-\eta\nabla f(x_t)$, is weaker: with step size $\eta=1/\ell$ it reaches a point with $\|\nabla f(x)\|\le\varepsilon$ within $\ell(f(x_0)-f^\star)/\varepsilon^2$ iterations, independently of the dimension (Nesterov, 1998). Such a point can be a saddle point. For many learning problems (matrix sensing and completion, phase retrieval, dictionary learning, tensor decomposition), every approximate second-order stationary point is an approximate global minimum, so an algorithm that avoids saddle points solves the problem.

Jin, Netrapalli, Ge, Kakade and Jordan (arXiv:1902.04811, J. ACM 2021) show that simple perturbed versions of GD and SGD find approximate second-order stationary points in essentially the number of iterations GD needs for first-order stationarity, up to polylogarithmic factors in the dimension. Their §5 gives a short, self-contained proof for a variant of perturbed GD (Algorithm 4). That proof is the subject of this mission.

Timeline:

• 2015: Ge, Huang, Jin and Yuan show that noisy SGD escapes strict saddle points in polynomial time.
• 2017: Jin, Ge, Netrapalli, Kakade and Jordan (ICML) prove that perturbed GD finds an $\varepsilon$-second-order stationary point in $\tilde O(\ell\Delta_f/\varepsilon^2)$ iterations, with a geometric argument on the "stuck region".
• 2019: arXiv:1902.04811 extends this to SGD and simplifies the deterministic proof through the improve or localize lemma (Lemma 21). §5 of that paper is formalized here.

Setting

Let $f:\mathbb R^d\to\mathbb R$, $d\ge1$, with gradient $\nabla f$ and Hessian $\nabla^2 f$; $\|\cdot\|$ is the Euclidean norm on vectors and the spectral norm on matrices. Assumption A: $f$ is $\ell$-gradient Lipschitz, $\|\nabla f(x_1)-\nabla f(x_2)\|\le\ell\|x_1-x_2\|$, and $\rho$-Hessian Lipschitz, $\|\nabla^2f(x_1)-\nabla^2f(x_2)\|\le\rho\|x_1-x_2\|$. A point $x$ is an $\varepsilon$-second-order stationary point ($\varepsilon$-SOSP) if

$$\|\nabla f(x)\|\le\varepsilon\qquad\text{and}\qquad\nabla^2 f(x)\succeq-\sqrt{\rho\varepsilon}\,I .$$

Write $f^\star=\inf f$ and $\Delta_f=f(x_0)-f^\star$.

Algorithm 4 (Perturbed GD, Variant). With step size $\eta$, radius $r$, time interval $\mathscr T$ and tolerance $\varepsilon$, start with $t_{\text{perturb}}=0$. At iteration $t$: if $\|\nabla f(x_t)\|\le\varepsilon$ and $t-t_{\text{perturb}}>\mathscr T$, replace $x_t$ by $x_t-\eta\xi_t$ with $\xi_t\sim\mathrm{Uniform}(B_0(r))$ and set $t_{\text{perturb}}=t$; then $x_{t+1}=x_t-\eta\nabla f(x_t)$. The parameters are those of Eq. (6):

$$\eta=\frac1\ell,\quad r=\frac{\varepsilon}{400\iota^3},\quad\mathscr T=\frac{\ell}{\sqrt{\rho\varepsilon}}\,\iota,\quad\mathscr F=\frac{1}{50\iota^3}\sqrt{\frac{\varepsilon^3}{\rho}},\quad\mathscr S=\frac{1}{4\iota}\sqrt{\frac{\varepsilon}{\rho}},$$

where $\iota$ is a logarithmic factor, and $\omega=2^{2-\iota}\ell\mathscr S$.

Formalization targets

Goal: Theorem 18

For $T=\lceil 8\max\{\Delta_f\mathscr T/\mathscr F,\ \Delta_f/(\eta\varepsilon^2)\}\rceil$ (which equals $\lceil400\iota^4\ell\Delta_f/\varepsilon^2\rceil$) and every $\iota\ge1$ with

$$\frac{T\ell\sqrt d}{\sqrt{\rho\varepsilon}}\,\iota^2 2^{8-\iota}\le\delta,$$

with probability at least $1-\delta$ over the perturbations,

$$\#\{t<T:\ x_t\text{ is an }\varepsilon\text{-SOSP}\}\ \ge\ T/2 .$$

The paper writes the count as $\tilde O(\ell\Delta_f/\varepsilon^2)$ with $\iota=c\log(d\ell\Delta_f/(\rho\varepsilon\delta))$.

Milestones, in the order the proof uses them

1. Lemma 19 (descent): $f(x_{t+1})-f(x_t)\le-\eta\|\nabla f(x_t)\|^2/2$ for $\eta\le1/\ell$.
2. Lemma 21 (improve or localize): $\|x_\tau-x_0\|\le\sqrt{2\eta t(f(x_0)-f(x_t))}$ for $t\ge\tau>0$.
3. Lemma 22 (coupling sequence): if $\lambda_{\min}(\nabla^2f(\tilde x))\le-\sqrt{\rho\varepsilon}$ and two GD runs start within $\eta r$ of $\tilde x$, $\eta r_0$ apart along the bottom eigenvector with $r_0>\omega$, one of them decreases $f$ by $\mathscr F$ within $\mathscr T$ steps.
4. Volume display (§5, proof of Lemma 20, p. 15): $w\,\mathrm{Vol}(\mathbb B^{d-1}_0(a))/\mathrm{Vol}(\mathbb B^d_0(a))=\frac{w}{a\sqrt\pi}\frac{\Gamma(d/2+1)}{\Gamma(d/2+1/2)}\le\frac wa\sqrt{d/\pi}$.
5. Lemma 20 (escaping saddle points): at $\tilde x$ with $\|\nabla f(\tilde x)\|\le\varepsilon$ and $\lambda_{\min}\le-\sqrt{\rho\varepsilon}$,

$$\mathbb P\bigl(f(x_{\mathscr T})-f(\tilde x)\le-\mathscr F/2\bigr)\ge1-\frac{\ell\sqrt d}{\sqrt{\rho\varepsilon}}\,\iota^22^{8-\iota}\quad\text{for }x_0=\tilde x+\eta\xi .$$

Significance

The result. Theorem 18 says that adding occasional small random perturbations to gradient descent costs only a polylogarithmic factor over the first-order rate $\ell\Delta_f/\varepsilon^2$ and buys second-order stationarity. Combined with the landscape results above, it gives polynomial-time guarantees for gradient methods on those learning problems. Lemma 20, on its own, is a quantitative statement that strict saddle points are unstable under perturbed GD; Lemmas 21 and 22 are reusable tools for any analysis of first-order methods near saddle points.

Formalizing it. The results are proved in the paper; none of them is formalized. A formal development would give machine-checked versions of the descent lemma for Hessian-Lipschitz functions, the improve-or-localize lemma, the coupling argument and the probabilistic escape bound. It would also settle the issue disclosed under Formalization scope.

Difficulty

Lemmas 19 and 21 are short. The difficulty is in Lemma 22 and Lemma 20. The obvious approach, linearizing GD around the saddle and following the unstable eigendirection, fails because the stuck region (starting points that do not escape within $\mathscr T$ steps) has no simple shape once $f$ is not quadratic. The coupling argument controls the difference of two runs instead. It needs an induction in which the non-quadratic error term stays below half of the leading term for all $\mathscr T$ steps, with the constants of Eq. (6) used exactly ($2\eta\rho\mathscr S\mathscr T=1/2$). Lemma 20 then turns a statement about pairs of points into a measure bound: a set whose every line parallel to $e_1$ meets it in a segment of length at most $\eta\omega$ has volume at most $\eta\omega$ times the $(d-1)$-volume of the ball. In Lean this needs Fubini over a rotated coordinate system and measurability of the stuck region. Theorem 18 requires a probabilistic accounting over the whole run, under the product law of the perturbations.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with $d\ge1$. The Hessian is fderiv ℝ (gradient f) x, the derivative of the gradient map, with the operator norm. Statements about $\lambda_{\min}$ use the quadratic form: $\lambda_{\min}(H)\le-c$ is "some unit $v$ has $\langle Hv,v\rangle\le-c$", and $H\succeq-cI$ is "$\langle Hv,v\rangle\ge-c\|v\|^2$ for all $v$". $\mathrm{Uniform}(B_0(r))$ is normalized Lebesgue measure on the open ball. Algorithm 4 is a deterministic function of the perturbation vectors, which have the product law on $(\mathbb R^d)^T$. The $t$-th iterate is the point tested at the start of iteration $t$, and "half of its iterations" counts $t\in\{0,\dots,T-1\}$. Probability statements bound the failure event from above.

The paper's $\tilde O(\cdot)$ is instantiated as the proof does:

• the parameters are exactly Eq. (6), and $T=\lceil8\max\{\Delta_f\mathscr T/\mathscr F,\Delta_f/(\eta\varepsilon^2)\}\rceil$ (p. 16);
• $\iota$ is any real $\ge1$ satisfying the proof's condition $(T\ell\sqrt d/\sqrt{\rho\varepsilon})\iota^22^{8-\iota}\le\delta$, in place of $\iota=c\log(d\ell\Delta_f/(\rho\varepsilon\delta))$. The printed argument of the logarithm changes under rescaling $x\mapsto\lambda x$ while every quantity in the proof does not, so the printed choice can give $\iota\le0$;
• $\mathscr T$ is a natural number equal to $\ell\iota/\sqrt{\rho\varepsilon}$, with no rounding, because the proof uses $x_{\mathscr T}$ and $2\eta\rho\mathscr S\mathscr T=1/2$ exactly;
• $\ell\ge\sqrt{\rho\varepsilon}$ (footnote 1, p. 14), $\iota\ge1$, $\eta>0$ and $f$ bounded below are the standing assumptions of §5.

A Hessian not tied to $f$, an arbitrary unit vector in place of the bottom eigenvector in Lemma 22, a per-realization or existential statement in place of the product-law probability, or a vacuous $\iota$ would each trivialize the statements; none is used.

Disclosed gap. The proof of Theorem 18 (p. 16) bounds the number of perturbations by applying Lemma 20 at each one. Algorithm 4 also perturbs at points that are already $\varepsilon$-SOSPs, where Lemma 20 does not apply, and the $\mathscr T$ iterations after such a perturbation are not counted. The goal is posed as printed; a solver who finds it false should report this in the discussion. The milestones do not depend on the gap.

Needed infrastructure: second-order Taylor bounds for Hessian-Lipschitz functions, symmetry of the Hessian and existence of a bottom eigenvector, volumes of Euclidean balls (in Mathlib through $\Gamma$), a Fubini-type slicing bound for sets of bounded width along a direction, and measurability of the GD iterates. The volume-ratio and slicing lemmas are reusable beyond this mission. Proofs of any milestone, and alternative proofs, are welcome.

Selected references

• C. Jin, P. Netrapalli, R. Ge, S. M. Kakade, M. I. Jordan, On Nonconvex Optimization for Machine Learning: Gradients, Stochasticity, and Saddle Points, arXiv:1902.04811v2 (2019); J. ACM 68(2), 2021. https://arxiv.org/abs/1902.04811
• C. Jin, R. Ge, P. Netrapalli, S. M. Kakade, M. I. Jordan, How to Escape Saddle Points Efficiently, ICML 2017. https://arxiv.org/abs/1703.00887
• R. Ge, F. Huang, C. Jin, Y. Yuan, Escaping From Saddle Points — Online Stochastic Gradient for Tensor Decomposition, COLT 2015. https://arxiv.org/abs/1503.02101
• Y. Nesterov, Introductory Lectures on Convex Programming, Volume I: Basic Course, 1998; Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• Y. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Math. Program. 108 (2006). https://doi.org/10.1007/s10107-006-0706-8

Motivation

Many operational decisions are linear programs whose cost vector is uncertain but partly predictable: shortest-path routing with uncertain travel times, portfolio choice with uncertain returns, shipment planning with uncertain costs. Before deciding, one observes features $X$ (traffic, market signals) correlated with the costs $Y$. Contextual linear optimization asks for a policy mapping features to decisions that minimizes the conditional expected cost, learned from past data $(X_1, Y_1), \dots, (X_n, Y_n)$.

Two families of methods compete. Estimate-then-optimize fits a regression of $Y$ on $X$ and plugs it into the optimizer. Empirical risk minimization (ERM) and its "integrated" variants choose a policy directly to minimize the empirical decision cost. A widespread view holds that the integrated approach should win because it targets the decision cost. Hu, Kallus and Mao (arXiv:2011.03030, Management Science 2022) compare the two through their regret rates. Slow, noise-independent rates of order $n^{-1/2}$ do not separate them. The separation appears under a margin (noise) condition controlling how often the problem is nearly dual-degenerate. This mission formalizes the paper's fast rate for ERM, Theorem 6.

Timeline. Margin conditions for classification go back to Mammen–Tsybakov (1999) and Tsybakov (2004); Massart–Nédélec (2006) obtained the corresponding fast rates for ERM over VC classes. El Balghiti, Elmachtoub, Grigas and Tewari (2019) gave slow generalization bounds for decision-focused losses in terms of the Natarajan dimension. Hu, Kallus and Mao (2020, revised 2021) proved the fast rate for ERM over policy classes of finite Natarajan dimension, a matching lower bound, and a faster rate for estimate-then-optimize.

Setting

The decision set is a polytope $\mathcal Z = \{z \in \mathbb R^d : Az \le b\}$, nonempty, with $\|z\| \le B$ on $\mathcal Z$ for some $B > 0$; $\mathcal Z^\angle$ is its finite set of extreme points. The pair $(X, Y) \in \mathbb R^p \times \mathbb R^d$ has $\|Y\| \le 1$, and $f^*(x) = \mathbb E[Y \mid X = x]$. The optimal set at $x$ is $\mathcal Z^*(x) = \arg\min_{z \in \mathcal Z} f^*(x)^\top z$.

A policy is a map $\pi : \mathbb R^p \to \mathcal Z^\angle$. A data-driven policy $\hat\pi$ maps a sample $\mathcal D$ of $n$ i.i.d. draws to a policy, and its regret is

$$\mathrm{Regret}(\hat\pi) = \mathbb E_{\mathcal D}\mathbb E_X\bigl[f^*(X)^\top\hat\pi(X) - \min_{z \in \mathcal Z} f^*(X)^\top z\bigr].$$

Given a class $\Pi$ of policies, $\hat\pi^{\mathrm{ERM}}_\Pi$ returns a member of $\Pi$ minimizing $\frac1n\sum_i Y_i^\top\pi(X_i)$.

The gap $\Delta(x)$ is the difference between the best value over suboptimal extreme points and the optimal value, set to $0$ when every point of $\mathcal Z$ is optimal. Assumption 2 (noise condition) with parameters $\alpha, \gamma \ge 0$ requires

$$\mathbb P_X\bigl(0 < \Delta(X) \le \delta\bigr) \le (\gamma\delta/B)^\alpha \qquad \text{for all } \delta > 0.$$

The Natarajan dimension of $\Pi$ is the largest $k$ for which there are points $x_1, \dots, x_k$ and labels $s_i \ne s'_i$ such that every pattern of choices between $s_i$ and $s'_i$ is realized by some $\pi \in \Pi$.

Formalization targets

Goal: Theorem 6

If Assumption 2 holds, $\mathbb P(|\mathcal Z^*(X)| > 1) = 0$, $\Pi$ has Natarajan dimension at most $\eta$, and $\Pi$ contains an optimal policy $\pi^*$, then for a constant $C(\alpha, \gamma)$ depending only on $\alpha, \gamma$,

$$\mathrm{Regret}(\hat\pi^{\mathrm{ERM}}_\Pi) \le C(\alpha, \gamma)\,B\left(\frac{\eta\log(|\mathcal Z^\angle| + 1)\log(n + 1)}{n}\right)^{\frac{1+\alpha}{2+\alpha}}.$$

The constant is existential and uniform over all dimensions, polytopes, distributions, classes, $\eta$ and $n$; the goal fixes no numerical value.

Milestones

With $d(\pi, \pi') = \frac1B\mathbb E_X[f^*(X)^\top(\pi'(X) - \pi(X))]$ and $d_\Delta(\pi, \pi') = \mathbb P_X(\pi(X) \ne \pi'(X))$:

1. Lemma 1: $d(\pi^*, \pi) \le 2d_\Delta(\pi^*, \pi)$ and $d_\Delta(\pi^*, \pi) \le c_1 d(\pi^*, \pi)^{\alpha/(\alpha+1)}$ with $c_1 = (\alpha\gamma^\alpha)^{-\alpha/(\alpha+1)}(\alpha+1)\gamma^\alpha$.
2. Lemma 2 (Bousquet's inequality): for a countable class bounded by $\bar H$ with second moments at most $\delta^2$, $S - \mathbb E S$ exceeds $\sqrt{2(\delta^2 + 4\bar H\mathbb E S)t/n} + 2\bar Ht/(3n)$ with probability at most $e^{-t}$.
3. Lemma 3: the localized excess-loss process satisfies $\mathbb E_{\mathcal D}[\sup_{h \in \mathcal H_\delta}(\mathbb E_n h - \mathbb E_P h)] \le (1+\sqrt2)C_0\sqrt{5\eta\log(|\mathcal Z^\angle|^2+1)\log(n+1)/n}\,\delta$ for $n$ above a threshold.
4. Tail bound (proof of Theorem 6, p. 27): for $t \ge 1$, $\mathbb P(d(\pi^*, \hat\pi^{\mathrm{ERM}}_\Pi) \ge K t(\bar V\log(n+1)/n)^{(1+\alpha)/(2+\alpha)}) \le e^{-t}$ with $\bar V = 5\eta\log(|\mathcal Z^\angle|^2+1)$ and $n \ge c\bar V\log(n+1)$.

Significance

Theorem 6 shows that the regret of ERM improves from $n^{-1/2}$ to $n^{-(1+\alpha)/(2+\alpha)}$ when the instance is rarely near dual degeneracy. With $\alpha = 1$, the generic case when $X$ has a bounded density and $f^*$ is linear, the rate is $n^{-2/3}$. Theorem 7 of the same paper (mission 2 of this series) shows that the exponent is optimal for any method that uses only the policy class. Theorem 8 (mission 3) shows that estimate-then-optimize can reach $n^{-(1+\alpha)/2}$, which is the paper's case against the conventional preference for integrated methods.

The result is proved in the paper; no machine-checked proof is known. Formalizing it adds a checked fast-rate theorem for a decision-focused learning method, a Lean statement of Bousquet's inequality in the form used throughout statistical learning theory, and a localized empirical-process bound for classes of finite Natarajan dimension.

Difficulty

The slow rate follows from uniform convergence of the empirical cost over $\Pi$. This argument cannot give more than $n^{-1/2}$: it bounds the deviation of every policy by the same worst-case amount, ignoring that near-optimal policies have small variance. The fast rate needs a variance–mean relation (Lemma 1, which is where the noise condition and the uniqueness assumption $\mathbb P(|\mathcal Z^*(X)| > 1) = 0$ enter), a concentration inequality that exploits small variance (Lemma 2), and a localized complexity bound (Lemma 3), combined over shells of the class. Lemma 2 is itself a deep result whose known proofs go through the entropy method. Lemma 3 rests on chaining and on bounding the pseudo-dimension of the excess-loss class by the Natarajan dimension, neither of which is in Mathlib.

Formalization scope

All declarations live in the namespace FastCLO.ERM. Conventions:

• Spaces are EuclideanSpace ℝ (Fin k). The polytope is a structure carrying $A$, $b$, $B > 0$, nonemptiness and the bound $\|z\| \le B$; $|\mathcal Z^\angle|$ is the cardinality of Set.extremePoints, whose finiteness is a proof obligation, not a hypothesis.
• The distribution is given by the law $\mu$ of $X$ and a Markov kernel $\kappa$ for $Y$ given $X$, with $\|Y\| \le 1$ $\kappa(x)$-almost surely for every $x$; $f^*$ is the kernel mean; data are Measure.pi of $\mu \otimes \kappa$.
• Regret is measured against the optimal value; this equals the paper's $f^*(X)^\top(\hat\pi(X) - \pi^*(X))$.
• ERM is any selection from the empirical argmin over the whole class; the paper's tie-breaking order is not encoded. The ERM rule is assumed jointly measurable in the data and the feature (an added hypothesis, so that the regret is a genuine integral).
• "$\pi^* \in \Pi$" means some member of $\Pi$ is optimal at almost every $x$; "Natarajan dimension at most $\eta$" means $\Pi$ does not shatter $\eta + 1$ points.
• Added hypotheses: $n \ge 1$ wherever the paper divides by $n$; $\bar H > 0$ in Lemma 2; measurability of the supremum in Lemma 3; $\eta \ge 1$ in the tail bound (the paper's $\epsilon_n > 0$). Constants ($C$, $C_0$, $K$, $c$) are quantified before everything they are uniform over.

A statement in which the regret integrated the empirical cost instead of $f^*$, or in which ERM minimized over a subset of the class, or in which the constant could depend on the instance, would be a different theorem; the Lean statements rule these out by construction.

Needed infrastructure: Bousquet's (or Talagrand's) inequality, symmetrization and Dudley chaining for empirical processes, packing bounds for classes of finite pseudo-dimension, and the Natarajan-to-pseudo-dimension reduction. These are reusable far beyond this mission; contributions of any of them are welcome.

Selected references

• Y. Hu, N. Kallus, X. Mao, Fast Rates for Contextual Linear Optimization, Management Science, 2022; arXiv:2011.03030v3, 2021. https://arxiv.org/abs/2011.03030
• O. Bousquet, A Bennett concentration inequality and its application to suprema of empirical processes, Comptes Rendus Mathématique 334(6), 2002. https://doi.org/10.1016/S1631-073X(02)02292-6
• P. Massart, É. Nédélec, Risk bounds for statistical learning, Annals of Statistics 34(5), 2006. https://doi.org/10.1214/009053606000000786
• A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Annals of Statistics 32(1), 2004. https://doi.org/10.1214/aos/1079120131
• O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, NeurIPS 2019; arXiv:1905.11488. https://arxiv.org/abs/1905.11488
• B. K. Natarajan, On learning sets and functions, Machine Learning 4, 1989. https://doi.org/10.1007/BF00114804

Motivation

Least-squares regression over a class of functions is the basic problem of statistical learning theory: given an i.i.d. sample $(X_i,Y_i)_{i=1}^N$ from an unknown joint law, select a function in a class $F$ whose prediction error $\mathbb E(f(X)-Y)^2$ is close to the best possible in $F$. The standard analysis of empirical risk minimization (ERM) compares empirical means with true means uniformly over the class, which requires the class and the target to concentrate: bounded functions, or sub-Gaussian tails. Heavy-tailed classes and targets, which arise as soon as the data are not bounded, fall outside that analysis.

S. Mendelson, Learning without Concentration (arXiv:1401.0304, J. ACM 62(3), 2015), showed that concentration is not needed for the lower half of the argument. The only property used for the quadratic part of the loss is a small-ball condition: functions in $F-F$ are not too concentrated near zero. Under that condition, ERM over a closed convex class attains an error governed by two localized complexity parameters, one intrinsic to the class and one measuring its interaction with the noise. The same lower-bound mechanism appears, for random matrices, in Koltchinskii–Mendelson (arXiv:1312.3580); the localized complexity parameters follow Lecué–Mendelson (arXiv:1305.4825).

Setting

Let $(\Omega,\mu)$ be a probability space and let $(X,Y)$ have joint law $\nu$ on $\Omega\times\mathbb R$, with $X\sim\mu$ and $\mathbb EY^2<\infty$. Let $F\subset L_2(\mu)$ be a closed, convex class of real functions on $\Omega$, and let $f^*\in F$ minimize $\mathbb E(f(X)-Y)^2$ over $F$. The noise is $\xi=f^*(X)-Y$. Given an i.i.d. sample $(X_i,Y_i)_{i=1}^N$ from $\nu$, an empirical minimizer $\hat f$ minimizes $\frac1N\sum_{i=1}^N(f(X_i)-Y_i)^2$ over $F$. Let $(\varepsilon_i)_{i=1}^N$ be independent random signs, independent of the sample, and write $F\cap rD_{f^*}=\{f\in F:\|f-f^*\|_{L_2}\le r\}$.

• The small-ball function of a class $H$ is $Q_H(u)=\inf_{h\in H}\Pr(|h(X)|\ge u\|h\|_{L_2})$; it is applied to $F-F=\{f-h:f,h\in F\}$.
• The intrinsic parameter (Definition 2.1) is

$$\beta^*_N(\gamma)=\inf\Bigl\{r>0:\mathbb E\sup_{f\in F\cap rD_{f^*}}\Bigl|\tfrac1{\sqrt N}\textstyle\sum_{i}\varepsilon_i(f-f^*)(X_i)\Bigr|\le\gamma\sqrt N r\Bigr\}.$$

• The multiplier process (2.2) is $\phi_N(s)=\sup_{f\in F\cap sD_{f^*}}\bigl|\tfrac1{\sqrt N}\sum_i\varepsilon_i\xi_i(f-f^*)(X_i)\bigr|$ with $\xi_i=f^*(X_i)-Y_i$, and the noise parameter is

$$\alpha^*_N(\gamma,\delta)=\inf\bigl\{s>0:\Pr(\phi_N(s)\le\gamma s^2\sqrt N)\ge1-\delta\bigr\}.$$

• For the proof (§5), $\beta_N(H,\gamma)=\inf\{r>0:\mathbb E\sup_{h\in H\cap rD}|\frac1N\sum_i\varepsilon_ih(X_i)|\le\gamma r\}$, with $D$ the unit ball of $L_2(\mu)$, and $H$ is star-shaped around 0 if $\lambda h\in H$ for all $h\in H$, $0<\lambda\le1$.

Formalization targets

Goal: Theorem 3.1

Fix $\tau>0$ with $Q_{F-F}(2\tau)>0$ and $\gamma<\tau^2Q_{F-F}(2\tau)/16$. For every $0<\delta<1$, with probability at least $1-\delta-\exp(-NQ^2_{F-F}(2\tau)/2)$, every empirical minimizer satisfies

$$\|\hat f-f^*\|_{L_2}\le2\max\Bigl\{\alpha^*_N(\gamma,\delta/4),\ \beta^*_N\Bigl(\frac{\tau Q_{F-F}(2\tau)}{16}\Bigr)\Bigr\}.$$

The joint law, the class and the target are arbitrary subject to the hypotheses above; no boundedness, moment or tail condition beyond $L_2$ is imposed.

Milestones

In attack order:

1. Localization for a star-shaped class (§5, p. 20): $r>\beta_N(H,\gamma)$ implies $\mathbb E\sup_{h\in H\cap rD}|\frac1N\sum_i\varepsilon_ih(X_i)|\le\gamma r$.
2. $\beta^*_N(\gamma)=\beta_N(F-f^*,\gamma)$ (§5, p. 20).
3. Theorem 5.4 (p. 21), the uniform empirical small-ball estimate: for $H$ in the unit sphere of $L_2(\mu)$, if $\mathbb E\sup_{h\in H}|\frac1N\sum_i\varepsilon_ih(X_i)|\le\tau Q_H(2\tau)/16$, then with probability at least $1-2\exp(-NQ_H^2(2\tau)/2)$, $\inf_{h\in H}|\{i:|h(X_i)|\ge\tau\}|\ge NQ_H(2\tau)/4$.
4. Corollary 5.5 (p. 22): the same estimate, $|\{i:|h(X_i)|\ge\tau\|h\|_{L_2}\}|\ge NQ_H(2\tau)/4$, for every $h$ of a star-shaped class with $\|h\|_{L_2}\ge r>\beta_N(H,\tau Q_H(2\tau)/16)$.
5. $F-f^*$ is star-shaped when $F$ is convex (proof of Theorem 5.3, p. 23).
6. Theorem 5.3 (p. 21): estimate (5.1) for $H=F-f^*$.
7. The projection inequality $\mathbb E\xi(f-f^*)(X)\ge0$ for $f\in F$ (§5, p. 23).
8. Display (5.3) (p. 23): with probability at least $1-2\exp(-NQ^2_{F-F}(2\tau)/2)$,

$$\frac1N\sum_{i=1}^N(f-f^*)^2(X_i)\ge\frac{\tau^2}4Q_{F-F}(2\tau)\|f-f^*\|^2_{L_2}$$

for all $f\in F$ with $\|f-f^*\|_{L_2}\ge r$. 9. Display (5.5) (p. 24): a bound $4\gamma\alpha^2$ on $|P_N\xi(f-f^*)-\mathbb E\xi(f-f^*)|$ on the sphere $\|f-f^*\|_{L_2}=\alpha$ extends to $4\gamma\|f-f^*\|^2_{L_2}$ outside it (deterministic).

Significance

Theorem 3.1 separates the error of ERM into a "low-noise" term $\beta^*_N$, which depends on the class only and matches the realizable rate, and a "high-noise" term $\alpha^*_N$, which depends on how the class correlates with the actual noise. Both are computable for heavy-tailed classes: the paper derives from it sharp rates for linear regression with heavy-tailed design and for the persistence problem in $\ell_1^n$ (§4). The small-ball lower bound (Theorem 5.4 and (5.3)) is reusable on its own: it gives lower isometry estimates for random matrices with heavy-tailed rows (the setting of Koltchinskii–Mendelson).

The result is proved in the paper. As far as is known, none of it has been machine-checked: there is no formal statement of Theorem 3.1, of the small-ball estimate, or of the localized parameters $\alpha^*_N,\beta^*_N$ in Lean. The mission produces the first formal statements of these objects, and a formal proof would also check the constants of the printed argument.

Difficulty

The obvious approach, a uniform law of large numbers for the squared loss over $F$, fails: without concentration, $\frac1N\sum_i(f-f^*)^2(X_i)$ need not be close to $\|f-f^*\|^2_{L_2}$ uniformly, and an upper estimate is unavailable. The proof needs only a one-sided lower estimate, and the difficulty is to obtain it uniformly over an infinite, unbounded class from the small-ball condition alone, with a probability that is exponential in $N$. A second difficulty is the multiplier term $\frac1N\sum_i\xi_i(f-f^*)(X_i)$, where the noise $\xi$ may be heavy-tailed and dependent on $X$; it must be controlled through the random-sign process defining $\alpha^*_N$, not through a bound on $\xi$. The standard tools involved (bounded differences, symmetrization, contraction for Bernoulli processes) are not in Mathlib.

Formalization scope

All objects live in one definitions file, LearnNoConc.ERM.Setting. The conventions are:

• The data are a joint law ν on Ω × ℝ; the law of $X$ is ν.map Prod.fst. The sample is a point of Fin N → Ω × ℝ under Measure.pi; $N\ge1$ is assumed.
• $\|\cdot\|_{L_2}$ is eLpNorm · 2 μ, valued in $[0,\infty]$. The expectation over random signs is the average over all $2^N$ sign vectors.
• Suprema and expectations of suprema are taken in $[0,\infty]$ (⨆, ‖·‖ₑ, lower Lebesgue integral), and $\alpha^*_N,\beta^*_N,\beta_N$ are $[0,\infty]$-valued infima, so an empty set of admissible radii gives $+\infty$ and a vacuous bound, as on the page. Defining inequalities are compared in the extended reals.
• "With probability at least $1-p$, $A$" is stated as "the outer probability of the complement of $A$ is at most $p$".
• The goal quantifies over every empirical minimizer, and $f^*$ is any minimizer of the risk over $F$.
• Added, disclosed hypotheses: $\mathbb EY^2<\infty$; every $f\in F$ measurable; and pointwise separability of $F$ (a countable subclass approximating every element pointwise and in $L_2$), which stands in for the measurability of suprema the paper takes for granted. Without it the lower integral of a non-measurable supremum would make $\beta^*_N$ smaller and the goal stronger than the paper.

A formalization in which an infimum over an empty set is $0$, a supremum or an integral of a non-integrable function is truncated to $0$, $f^*$ is an arbitrary element of $F$, or $\hat f$ is one chosen minimizer would trivialize or change the statement; all of these are ruled out above.

A complete development needs McDiarmid's bounded differences inequality, Giné–Zinn symmetrization (in expectation and in probability), the Ledoux–Talagrand contraction inequality for Bernoulli processes, and the measurability theory of suprema over separable classes. These are reusable well beyond this mission, and contributions of any of them are welcome, as are proofs of the milestones independently of the goal.

Selected references

• S. Mendelson, Learning without Concentration, J. ACM 62(3), Article 21, 2015. Preprint arXiv:1401.0304v2 (the version cited here). https://arxiv.org/abs/1401.0304, https://doi.org/10.1145/2699439
• V. Koltchinskii, S. Mendelson, Bounding the smallest singular value of a random matrix without concentration, preprint, 2013. https://arxiv.org/abs/1312.3580
• G. Lecué, S. Mendelson, Learning subgaussian classes: Upper and minimax bounds, preprint, 2013. https://arxiv.org/abs/1305.4825
• A. W. van der Vaart, J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996, §2.3.3 (pointwise separable classes). https://doi.org/10.1007/978-1-4757-2545-2

Motivation

Kernel ridge regression is a standard nonparametric estimator with optimal statistical guarantees, but it needs the $n\times n$ kernel matrix of the data: roughly $O(n^3)$ time and $O(n^2)$ memory. Random features (Rahimi and Recht, NeurIPS 2007) replace the kernel by an average over $M$ randomly sampled feature functions, turning the problem into ridge regression in dimension $M$, at cost $O(nM^2)$ time and $O(nM)$ memory. The question is how many features are needed before the statistical accuracy of the exact kernel method is lost.

The first statistical analysis of a random-features estimator (Rahimi and Recht, NeurIPS 2009), for Lipschitz losses over a ball of fixed radius, needs $O(n)$ features to reach an $O(1/\sqrt n)$ bound. Rudi and Rosasco (arXiv:1602.04474, NeurIPS 2017) showed that $M$ of order $\sqrt n\log n$ features already give the $O(1/\sqrt n)$ excess risk that exact kernel ridge regression attains with regularization $\lambda=n^{-1/2}$ (Caponnetto and De Vito 2007), assuming only that the best predictor in the reproducing kernel Hilbert space exists.

Setting

Let $X$ be a separable input space and $(\Omega,\pi)$ a probability space. A random feature is a function $\psi:X\times\Omega\to\mathbb R$, continuous in both variables with $|\psi(x,\omega)|\le\kappa$ for some $\kappa\ge1$. It defines the kernel

$$K(x,x')=\int_\Omega\psi(x,\omega)\psi(x',\omega)\,d\pi(\omega),$$

whose reproducing kernel Hilbert space is $\mathcal H$. Data $(x_1,y_1),\dots,(x_n,y_n)$ are drawn i.i.d. from a probability $\rho$ on $X\times\mathbb R$ with $|y|\le b$ almost surely, $b>0$. The expected risk is $\mathcal E(f)=\int(f(x)-y)^2\,d\rho(x,y)$, and $f_{\mathcal H}\in\mathcal H$ is a minimizer of $\mathcal E$ over $\mathcal H$, assumed to exist.

Given features $\omega_1,\dots,\omega_M$ drawn i.i.d. from $\pi$, independently of the data, the feature map is $\phi_M(x)=M^{-1/2}(\psi(x,\omega_1),\dots,\psi(x,\omega_M))$. With $\widehat C_M=\frac1n\sum_i\phi_M(x_i)\phi_M(x_i)^\top$ and $\widehat S_M^\top\widehat y=\frac1n\sum_iy_i\phi_M(x_i)$, the random-features ridge estimator with parameter $\lambda>0$ is

$$\widehat f_{\lambda,M}(x)=\phi_M(x)^\top\widehat w_{\lambda,M},\qquad\widehat w_{\lambda,M}=(\widehat C_M+\lambda I)^{-1}\widehat S_M^\top\widehat y .$$

In the Lean development these are kernelOf, featureMap, empCov, empCross, rfWeights, rfEstimator and risk in the namespace RFRidge.Basic.

Formalization targets

Goal: Theorem 1

There are constants $c_0,c_1>0$, independent of $n$, $\lambda$ and $\delta$, and a threshold $n_0$ such that for every $\delta\in(0,1]$ and $n\ge n_0$, with $\lambda_n=n^{-1/2}$ and

$$M_n=c_0\sqrt n\,\log\frac{108\kappa^2\sqrt n}{\delta}$$

features, with probability at least $1-\delta$ over the data and the features,

$$\mathcal E(\widehat f_{\lambda_n,M_n})-\mathcal E(f_{\mathcal H})\le\frac{c_1\log^2\frac{18}{\delta}}{\sqrt n}.$$

The constants are existential: the paper prints them without values, and the values in its appendix are not established by the printed proof. The goal therefore asserts the shape of the bound, which survives any later improvement of the constants.

Milestones

The proof goes through an analytic decomposition of the excess risk on $L^2(X,\rho_X)$ followed by concentration. The milestones are the results of that proof that are stated as printed:

1. Lemma 1: the integral operator $L$ of $K$ equals $\int\psi_\omega\otimes\psi_\omega\,d\pi(\omega)$.
2. Lemma 2: the component of the regression function orthogonal to the range of $L$ is invisible to every random-features predictor, almost surely.
3. Proposition 4 (Cordes), Proposition 9 (interpolation $\|XA^\sigma\|\le\|X\|^{1-\sigma}\|XA\|^\sigma$) and Proposition 8 (a multiplicative bound between regularized operators).
4. Lemma 5: the bound on the approximation error under the source condition $Pf_\rho=L^rg$. Lemmas 3 and 4 remain draft items, but are omitted from the milestone list because the PDF text layer corrupts their displayed equations and the mechanical verbatim checker rejects the exact visual transcription.
5. Propositions 1 and 2: Bernstein inequalities for real random variables and for random vectors in a Hilbert space.

Significance

Theorem 1 shows that, in the basic setting, random features reduce the cost of kernel ridge regression from $O(n^3)$ time and $O(n^2)$ memory to $O(n^2)$ and $O(n\sqrt n)$ without losing the minimax-optimal $O(1/\sqrt n)$ rate. It is the reference result on the statistical cost of random-features approximations, and the same decomposition yields the paper's faster rates under source and capacity conditions (Theorems 2 and 3) and the analysis of data-dependent feature sampling.

To the best of the mission's knowledge, none of these results has a machine-checked proof. Formalizing them requires real infrastructure: integral operators on $L^2$ defined by a kernel with an integral representation, operator inequalities for the continuous functional calculus, and Bernstein inequalities in Hilbert spaces. The Bernstein inequalities and the operator inequalities (Cordes, interpolation, Proposition 8) are reusable well beyond this paper.

Difficulty

The obvious argument controls $\sup_{x,x'}|K_M(x,x')-K(x,x')|$ uniformly and transfers it to the estimator. It needs $M$ of order $n$ to keep the $O(1/\sqrt n)$ rate, because a uniform kernel approximation ignores that the estimator only probes $K$ through a regularized operator. Getting $\sqrt n\log n$ features requires comparing the integral operators $L$ and $L_M$ relative to $L+\lambda I$, in the operator norm weighted by $(L+\lambda I)^{-1/2}$, and this needs fractional powers of operators, operator monotonicity and concentration of random operators. A second subtlety is that the regression function need not lie in the closure of $\mathcal H$; Lemma 2 shows that the orthogonal component does not affect any random-features estimator.

Formalization scope

All models are posed in Lean 4 with Mathlib. The input space is a separable topological space with its Borel σ-algebra, the feature space $\Omega$ is the type W, and $\psi$ is jointly continuous, jointly measurable for the product σ-algebra (an added hypothesis: without second countability it does not follow from continuity), and bounded by $\kappa\ge1$ everywhere. The RKHS is Mathlib's RKHS ℝ H X ℝ, tied to the kernel by RKHS.kernel H x x' 1 = K x x'. Samples and features are indexed from $0$; the $n$ samples and $M_n$ features have the product law $\rho^{\otimes n}\otimes\pi^{\otimes M_n}$, and $M_n$ is rounded up. "With probability at least $1-\delta$" is "the failure event has probability at most $\delta$", with $\delta\in(0,1]$ and $n\ge1$.

Operators: the paper's Hilbert spaces are real, but Mathlib's continuous functional calculus for bounded operators, which defines $A^s$ and $(A+\lambda I)^{-1/2}$, exists only on complex Hilbert spaces. The operator milestones are therefore posed on complex Hilbert spaces, and every inverse or power is the functional calculus of an explicit real function; the real statements follow by complexification. Lemmas 3–5 are stated for abstract positive operators satisfying exactly the relations their proofs use, and add $r\le1$ (the range of Assumption 6), without which Lemma 5 is false. Proposition 8 states $\beta<1$ as a conclusion. Lemma 3 corrects a sign in the exponent of $C_{M,\lambda}$: its display prints $-1/2$ where its proof uses $+1/2$; the printed bound fails for scalar operators.

A trivializing formalization is ruled out: the goal mentions only the estimator, the risk and $f_{\mathcal H}$, never the operators of the proof, and its constants $c_0,c_1$ are fixed before $\delta$ and $n$, so they cannot absorb $\log^2(18/\delta)$ or $\sqrt n$.

Not included: Theorem 4 (the analytic decomposition), Propositions 5 and 7 (which need Hilbert–Schmidt norms and traces), Lemmas 6–10 and Theorems 5–7 of Appendix A.3–A.4. Contributions of these intermediate results, of a Lean theory of integral operators of kernels, and of Hilbert-space concentration inequalities are welcome.

Selected references

• A. Rudi, L. Rosasco, Generalization Properties of Learning with Random Features, NeurIPS 2017; arXiv:1602.04474v5. https://arxiv.org/abs/1602.04474
• A. Rahimi, B. Recht, Random Features for Large-Scale Kernel Machines, NeurIPS 2007. https://papers.nips.cc/paper/3182-random-features-for-large-scale-kernel-machines
• A. Caponnetto, E. De Vito, Optimal Rates for the Regularized Least-Squares Algorithm, Foundations of Computational Mathematics 7, 2007. https://doi.org/10.1007/s10208-006-0196-8
• A. Rahimi, B. Recht, Weighted Sums of Random Kitchen Sinks: Replacing Minimization with Randomization in Learning, NeurIPS 2008 (proceedings 2009). https://papers.nips.cc/paper/3495-weighted-sums-of-random-kitchen-sinks-replacing-minimization-with-randomization-in-learning
• H. O. Cordes, Spectral Theory of Linear Differential Operators and Comparison Algebras, Cambridge University Press, 1987. https://doi.org/10.1017/CBO9780511662836