Statistics

Motivation

Distributionally robust optimization replaces the average of a loss over a sample by its worst-case average over all distributions close to the sample. When closeness is measured by an $f$-divergence, the worst case over a ball of radius $\rho/n$ around the empirical distribution is also the upper endpoint of a generalized empirical likelihood confidence interval. Empirical likelihood (Owen, 1988–2001) is the case $f(t)=-2\log t+2t-2$; the $\chi^2$, Cressie–Read and other divergences give the rest of the family.

Duchi, Glynn and Namkoong (arXiv:1610.03425, Mathematics of Operations Research 46(3), 2021) show that these robust objects behave, to first order, like the sample mean plus a variance penalty. Their Lemma 1 is the scalar version of that statement and, in the authors' words (p. 7), an expansion "that essentially gives all of the major distributional convergence results in this paper": with the central limit theorem it yields the asymptotically exact $\chi^2_1$ coverage of empirical likelihood intervals for a mean, and its uniform extension yields the coverage results for optimal values of stochastic programs.

Timeline. Owen (1988, 1990) proved the $\chi^2$ calibration of empirical likelihood for means of i.i.d. data. Its extension to smooth $f$-divergences is, as the paper notes (p. 6), essentially due to Baggerly (1998), Corcoran (1998) and Bertail, Gautherat and Harari-Kermadec (2014). Lam (arXiv:1605.09349) proved an in-probability version of the expansion below for $f(t)=-2\log t$. Namkoong and Duchi (2017, arXiv:1610.02581) proved a finite-sample, high-probability version for the $\chi^2$ divergence and bounded variables. Duchi, Glynn and Namkoong proved the almost-sure version for every smooth $f$ and for stationary ergodic data.

Setting

Let $f:[0,\infty)\to(-\infty,+\infty]$ be convex and lower semicontinuous, as every divergence generator in the paper is. Assumption A asks that $f$ be finite on $(0,\infty)$, three times differentiable near $1$, with $f(1)=f'(1)=0$ and $f''(1)=2$; the value $f(0)$ may be $+\infty$.

Let $z=(z_1,\dots,z_n)$ be a sample with empirical distribution $\widehat P_n$. A distribution $P\ll\widehat P_n$ is a weight vector $p\ge0$ with $\sum_ip_i=1$, and $D_f(P\|\widehat P_n)=\sum_{i=1}^n\frac1nf(np_i)$. The robust mean is

$$\sup_{P:\,D_f(P\|\widehat P_n)\le\rho/n}E_P[Z]=\sup\Big\{\sum_ip_iz_i : p\ge0,\ \sum_ip_i=1,\ \sum_i\tfrac1nf(np_i)\le\tfrac\rho n\Big\}.$$

The sample mean is $E_{\widehat P_n}[Z]=\frac1n\sum_iz_i$ and the sample variance is $s_n^2=E_{\widehat P_n}[Z^2]-E_{\widehat P_n}[Z]^2$ (normalised by $1/n$).

A sequence $Z_1,Z_2,\dots$ of real random variables is strictly stationary and ergodic if the law $\mu_Z$ of the path $(Z_1,Z_2,\dots)$ on $\mathbb R^{\mathbb N}$ is invariant under the left shift $\theta$ and every $\theta$-invariant measurable set of paths has $\mu_Z$-measure $0$ or $1$. Every i.i.d. sequence qualifies (Kolmogorov's $0$–$1$ law), as do stationary Markov chains started in a unique invariant law and stationary mixing sequences.

Formalization targets

Goal: Lemma 1, the almost-sure variance expansion (p. 7)

Let $Z_1,Z_2,\dots$ be strictly stationary and ergodic with $E[Z_1^2]<\infty$, let $f$ satisfy Assumption A and $\rho\ge0$. Then almost surely

$$\sqrt n\;\Big|\sup_{P:\,D_f(P\|\widehat P_n)\le\rho/n}E_P[Z]-E_{\widehat P_n}[Z]-\sqrt{\frac\rho n\,s_n^2}\Big|\;\longrightarrow\;0 .$$

This is the paper's (8), "$\le\epsilon_n/\sqrt n$ with $\epsilon_n\to0$ a.s.", with $\epsilon_n$ taken to be the left-hand side. No rate is asserted, so the goal is not tied to any constant.

Milestones (Appendix A, pp. 31–33)

1. (30): there are $0<c,C<\infty$ depending only on $f$ with $2(1-C\epsilon)h_\epsilon(t)\le f(t+1)$ for $t\ge-1$ and $f(t+1)\le(1+C\epsilon)t^2$ for $|t|\le\epsilon$, whenever $0<\epsilon\le c$. Here $h_\epsilon$ is the Huber function, $t^2/2$ for $|t|\le\epsilon$ and $\epsilon|t|-\epsilon^2/2$ otherwise.
2. (32): with the sets $\mathcal U_{\rm sm}\subset\mathcal U\subset\mathcal U_{\rm big}$ of (31), $\sup_{\mathcal U_{\rm sm}}u^Tz\le(\text{robust mean})-E_{\widehat P_n}[Z]=\sup_{\mathcal U}u^Tz\le\sup_{\mathcal U_{\rm big}}u^Tz$.
3. Lemma 8: $\sup_{u\in\mathcal U_{\rm sm}}u^Tz=\sqrt{\rho s_n(z)^2/n}\,/\sqrt{1+C\epsilon}$ when $\|z-\bar z_n\|_\infty/\sqrt n\le\epsilon s_n(z)\sqrt{(1+C\epsilon)/\rho}$.
4. Lemma 9: $\sup_{u\in\mathcal U_{\rm big}}u^Tz\le\sqrt{\rho s_n(z)^2/n}\,/\sqrt{1-C\epsilon}$ under the same condition with $1-C\epsilon$.
5. Lemma 6: on the event $\max_{i\le n}|z_i-\bar z_n|/\sqrt n\le\epsilon s_n\sqrt{(1-C\epsilon)/\rho}$, the robust mean lies between $E_{\widehat P_n}[Z]+\sqrt{\rho s_n^2/n}/\sqrt{1+C\epsilon}$ and $E_{\widehat P_n}[Z]+\sqrt{\rho s_n^2/n}/\sqrt{1-C\epsilon}$.
6. Lemma 7: for identically distributed (possibly dependent) $Z_i$ with $E|Z_1|^k<\infty$, $P(|Z_n|\ge\epsilon n^{1/k}\text{ i.o.})=0$ for every $\epsilon>0$ and $\max_{i\le n}|Z_i|/n^{1/k}\to0$ almost surely.

Significance

The result. The expansion says the robust mean is a variance-regularised mean, $E_{\widehat P_n}[Z]+\sqrt{\rho\,s_n^2/n}$, up to $o(n^{-1/2})$, for every smooth divergence at once. Combined with the central limit theorem and Slutsky's lemma, it gives $P\big(E[Z]\in\{E_P[Z]:D_f(P\|\widehat P_n)\le\rho/n\}\big)\to P(\chi^2_1\le\rho)$, the exact asymptotic coverage of generalized empirical likelihood intervals (the paper's Proposition 1 for $d=1$). The paper's uniform expansion (Theorem 2) and its coverage theorem for optimal values (Theorem 3) rest on the same mechanism. Because the statement is almost sure and allows stationary ergodic data, it also covers time series and simulation output.

Formalizing it. The lemma is proved in the paper; no machine-checked version of it, of (30), or of Lemmas 6–9 exists. A complete development would give the first formal link between $f$-divergence balls and variance regularisation for general $f$, and a formal almost-sure theory for empirical likelihood beyond the i.i.d. case. The $\chi^2$-only finite-sample expansion of Namkoong and Duchi (2017) is posed, not proved, on the platform.

Difficulty

The obvious route is a second-order Taylor expansion of $f$ around $1$ inside the supremum. It fails because the optimal weights $np_i$ are close to $1$ only if no single observation is large compared with $\sqrt n\,s_n$; a heavy observation drives a weight to $0$, where $f$ may be infinite and is not approximated by its Taylor polynomial. The argument has to sandwich the divergence ball between a quadratic ball and a Huber ball valid on all of $[0,\infty)$, then show that the event "no observation of order $\sqrt n$" holds eventually almost surely, which under only a second moment and no independence needs a Borel–Cantelli argument for identically distributed variables (Lemma 7). The sample variance limit needs Birkhoff's pointwise ergodic theorem, which Mathlib does not yet contain.

Formalization scope

• Samples. $Z:\mathbb N\to\Omega\to\mathbb R$ on a probability space; Lean's Z 0 is the paper's $Z_1$ and the $n$-th sample vector is fun i : Fin n => Z i ω. Stationary ergodicity is IsStationaryErgodic: each Z i measurable and Mathlib's Ergodic for the left shift on the path law (which includes shift invariance). The mixing display on p. 7 implies this; the Lean hypothesis is the weaker standard notion named in the lemma.
• Divergence. $f:\mathbb R\to$ EReal, using the published IsPhiDivergenceFunction (convex on $[0,\infty)$, finite on $(0,\infty)$, $f(1)=0$, $f(0)=+\infty$ allowed); AssumptionA adds lower semicontinuity on $[0,\infty)$ (the paper's standing condition on divergence generators), three-times differentiability on an interval $(a,b)\ni1$, $f'(1)=0$, $f''(1)=2$. The reading "finite on $(0,\infty)$" follows the paper's remark that only the behaviour at $0$ is unrestricted.
• Robust mean. Distributions are weight vectors on the sample ($P\ll\widehat P_n$), the ball is the published probUncertaintySet, and the supremum is a real sSup of a non-empty bounded set. Mean and variance are the published empMean, empVar.
• Constants. In (32) and Lemmas 6, 8, 9 the constant $C$ is a parameter, and the two inequalities of (30) at the given $\epsilon$ and $C$ are hypotheses; (30) itself asserts that such $c,C$ exist. $\epsilon>0$ throughout, $\epsilon<1$ where the sets (31) are used, and $C\epsilon<1$ wherever $\sqrt{1-C\epsilon}$ appears.
• Ruling out trivialisations. The ball always contains the uniform weights, so the robust mean is never the junk value of an empty supremum; the goal's limit statement makes $n=0$ irrelevant. A formalization that assumes i.i.d. data, a finite moment of order above two, or a specific $f$ proves a different, weaker statement.
• Infrastructure. Needed: Birkhoff's pointwise ergodic theorem for the shift (not in Mathlib; posed but unproved on the platform as PalmQueueing.Ergodic.discrete_pointwise, for bijective flows), Borel–Cantelli (in Mathlib), and elementary convex analysis of the Huber function. The pointwise ergodic theorem and Lemma 7 are reusable well beyond this mission. Proofs of any milestone, and of the ergodic theorem for one-sided shifts, are welcome.

Selected references

• J. C. Duchi, P. W. Glynn, H. Namkoong, Statistics of Robust Optimization: A Generalized Empirical Likelihood Approach, arXiv:1610.03425v3 (2018); Mathematics of Operations Research 46(3), 2021. https://arxiv.org/abs/1610.03425
• A. B. Owen, Empirical likelihood ratio confidence regions, Annals of Statistics 18(1), 1990. https://doi.org/10.1214/aos/1176347494
• K. A. Baggerly, Empirical likelihood as a goodness-of-fit measure, Biometrika 85(3), 1998. https://doi.org/10.1093/biomet/85.3.535
• H. Lam, Recovering best statistical guarantees via the empirical divergence-based distributionally robust optimization, Operations Research, 2019. https://arxiv.org/abs/1605.09349
• S. A. Corcoran, Bartlett adjustment of empirical discrepancy statistics, Biometrika 85(4), 1998. https://doi.org/10.1093/biomet/85.4.967
• H. Namkoong, J. C. Duchi, Variance-based regularization with convex objectives, NeurIPS 2017. https://arxiv.org/abs/1610.02581
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust solutions of optimization problems affected by uncertain probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641

Motivation

Operations research has long studied the stochastic problem $\min_{z\in\mathcal Z}\mathbb E[c(z;Y)]$: choose a decision $z$ before an uncertain quantity $Y$ (demand, prices, returns) is revealed. In practice the decision maker also observes covariates $X$ before deciding (web-search volume before stocking a product, weather before routing a shipment) and should solve the conditional problem instead. Bertsimas and Kallus (arXiv:1402.5481v4; Management Science 66(3), 2020) proposed predictive prescriptions: reweight historical observations $(x^i,y^i)$ by how relevant they are to the current $x$, using weights borrowed from a nonparametric regression method, and minimize the reweighted sample cost. Their asymptotic theorems guarantee that this procedure converges to the decision that full knowledge of the conditional distribution would give.

The unconditional special case, sample average approximation (SAA) with i.i.d. draws of $Y$ and no covariate, has a classical consistency theory (Dupačová–Wets 1988; Shapiro 2003). This mission conditions that theory on $X$, with $k$-nearest-neighbour weights.

Setting

Decisions $z$ lie in a set $\mathcal Z\subseteq\mathbb R^{d_z}$, covariates $X$ in $\mathcal X\subseteq\mathbb R^{d_x}$, uncertainty $Y$ in $\mathcal Y\subseteq\mathbb R^{d_y}$; all three spaces carry the Euclidean norm. A cost $c(z;y)\in\mathbb R$ is given. Let $\mu$ be the joint law of $(X,Y)$, $\mu_X$ the law of $X$ and $\mu_{Y|x}$ the conditional law of $Y$ given $X=x$. The conditional cost and the full-information problem (2) are

$$C(z\mid x)=\mathbb E\big[c(z;Y)\mid X=x\big],\qquad v^*(x)=\min_{z\in\mathcal Z}C(z\mid x),\qquad \mathcal Z^*(x)=\arg\min_{z\in\mathcal Z}C(z\mid x).$$

The data are $S_N=\{(x^1,y^1),\dots,(x^N,y^N)\}$, the first $N$ terms of an i.i.d. sequence with law $\mu$. The kNN weights (12) are $w_{N,i}(x)=\frac1k\mathbb I[x^i$ is one of the $k$ nearest neighbours of $x$ among $x^1,\dots,x^N]$, with ties among equidistant points broken by lower index first. The predictive prescription (3) is any

$$\hat z_N(x)\in\arg\min_{z\in\mathcal Z}\ \widehat C_N(z\mid x),\qquad \widehat C_N(z\mid x)=\sum_{i=1}^N w_{N,i}(x)\,c(z;y^i).$$

The paper's standing assumptions: Assumption 3 ($\mathbb E|c(z;Y)|<\infty$ for every $z\in\mathcal Z$, and $\mathcal Z^*(x)\ne\emptyset$ for a.e. $x$); Assumption 4 ($c(z;y)$ is equicontinuous in $z$, uniformly over $y\in\mathcal Y$); Assumption 5 ($\mathcal Z$ closed and nonempty, and either bounded, or $c$ is bounded below for large $\|z\|$ and for each $x$ there is a set $D_x$ of positive conditional probability on which $c(z;y)\to\infty$ uniformly as $\|z\|\to\infty$).

Definition 1. $\hat z_N$ is asymptotically optimal if, with probability 1, for $\mu_X$-a.e. $x$, $C(\hat z_N(x)\mid x)\to v^*(x)$; it is consistent if, with probability 1, for $\mu_X$-a.e. $x$, $\inf_{z\in\mathcal Z^*(x)}\|\hat z_N(x)-z\|\to0$.

Formalization targets

Goal: Theorem 5 (kNN), p. 19 (= Theorem 15, p. 43)

Under Assumptions 3, 4, 5 and i.i.d. sampling, with $k=\min\{\lceil CN^\delta\rceil,N-1\}$, $C>0$, $0<\delta<1$: with probability 1, for $\mu_X$-a.e. $x$, $\mathcal Z^*(x)$ is nonempty, the argmin is eventually nonempty, and every selection $\hat z_N(x)$ from it satisfies

$$\lim_{N\to\infty}C(\hat z_N(x)\mid x)=v^*(x)\qquad\text{and}\qquad\lim_{N\to\infty}\inf_{z\in\mathcal Z^*(x)}\|\hat z_N(x)-z\|=0 .$$

The goal covers both cases of Assumption 5, including unbounded $\mathcal Z$ such as the newsvendor's $[0,\infty)$.

Milestones, in the order the proof uses them

1. Walk step (proof of Theorem 15, p. 47). For any measurable $h$ with $\mathbb E|h(Y)|<\infty$, $\sum_i w_{N,i}(x)h(y^i)\to\mathbb E[h(Y)\mid X=x]$ a.s., for $\mu_X$-a.e. $x$.
2. Lemma 7 (p. 47). Fixed-$z$ and fixed-$D$ almost-sure convergence upgrade to convergence for all $z\in\mathcal Z$ simultaneously and weak convergence $\hat\mu_{Y|x,N}\to\mu_{Y|x}$, off one null set.
3. Lemma 5 (p. 45). Along one sample path, pointwise convergence $\widehat C_N(\cdot\mid x)\to C(\cdot\mid x)$ is uniform on compact subsets of $\mathcal Z$.
4. Lemma 6, case 1 (pp. 45–47). For bounded $\mathcal Z$, the minima and minimizers of $\widehat C_N(\cdot\mid x)$ converge to $v^*(x)$ and to $\mathcal Z^*(x)$.

Significance

Theorem 5 says that a decision computed from data alone, with no model of the conditional distribution, performs asymptotically as well as the decision a decision maker with full knowledge of $\mu_{Y|x}$ would take, for almost every covariate value and under mild conditions on the cost. It justifies the kNN prescription in the paper's newsvendor and shipment-planning experiments, and its proof skeleton (a pointwise strong law for the weights, then Lemmas 5–7) is reused for kernel, local-linear and recursive-kernel weights (Theorems 6–9), which could follow as missions of the same shape.

The result is proved in the paper; it has not been machine-checked anywhere. Formalizing it requires a strong law for nearest-neighbour regression with integrable responses (Walk 2010, building on Devroye, Györfi, Krzyżak and Lugosi 1994), which Mathlib does not have, and a careful treatment of conditional laws at a point. One of the paper's lemmas (Lemma 6) is false as printed for unbounded $\mathcal Z$; the formalization isolates the correct statement.

Difficulty

The deterministic optimization part (Lemmas 5 and 6 for bounded $\mathcal Z$) is a compactness argument. The central difficulty is the probabilistic input. A natural first idea, applying the strong law of large numbers to $\widehat C_N(z\mid x)$, fails: the kNN weights depend on all of $x^1,\dots,x^N$ and on $x$, the effective sample size $k_N$ grows sublinearly, and convergence is required for almost every $x$ simultaneously, including $x$ that are atoms of $\mu_X$ where ties are the rule. A second difficulty is the exchange of quantifiers: the strong law gives a null set depending on $z$ and on the set $D$, and the conclusion needs one null set for all $z\in\mathcal Z$. Finally, for unbounded $\mathcal Z$ the minimizers of $\widehat C_N(\cdot\mid x)$ must be kept bounded, and weak convergence of $\hat\mu_{Y|x,N}$ alone does not do so.

Formalization scope

All spaces are EuclideanSpace ℝ (Fin d), so kNN distances and $\|z-z'\|$ are Euclidean. The data are a measurable, mutually independent sequence S i : Ω → ℝ^{d_x} × ℝ^{d_y} with each term of law $\mu$; samples are indexed from $0$. The following readings are explicit in the Lean:

• $\mu_{Y|x}$ is the fixed version μ.condKernel x of the conditional law, and $C(z\mid x)$ is its Bochner integral; Assumption 5's "for every $x\in\mathcal X$" refers to this version, and $D_x$ is measurable.
• Quantifier order is "with probability 1, for $\mu_X$-a.e. $x$" (Definition 1), and the selection $\hat z_N$ is quantified inside both a.e. quantifiers: $\mathcal Z^*(x)$ is nonempty, the argmin is nonempty for all large $N$, and every sequence lying in it for all large $N$ is covered.
• $v^*(x)$ is never a real infimum; it is read as $C(z^\star\mid x)$ for $z^\star\in\mathcal Z^*(x)$, nonempty a.e. by Assumption 3.
• Ties are broken lower-index-first, so the weights sum to $1$ for $N\ge2$; at $N\le1$ the formula gives $k=0$ and all weights $0$.
• Lemmas 5–7 assume weights that are eventually nonnegative and sum to $1$, the reading of the paper's $\mathbb E_{\hat\mu_{Y|x,N}}$ notation; weak convergence is tested against bounded continuous functions.
• Lemma 6 is posed for bounded $\mathcal Z$ only, without its unused weak-convergence hypothesis; the goal is posed for both cases.

A formalization that replaces the conditional law by an arbitrary kernel unrelated to $\mu$, takes $\hat z_N$ to be a fixed measurable selection chosen outside the almost-sure quantifier, or reads $\inf_{z\in\mathcal Z^*(x)}$ on an empty set as $0$ without Assumption 3 would trivialize or weaken the result and is ruled out by the statements above.

Needed infrastructure: nearest-neighbour ranks and their combinatorics (Stone's lemma: a point is among the $k$ nearest neighbours of at most a bounded number of others), a strong law for kNN regression, portmanteau-type characterizations of weak convergence for weighted empirical measures, and stability of minimizers under locally uniform convergence. The kNN strong law and the stability lemmas are reusable well beyond this mission. Related platform items, credited but not reused (they concern unconditional SAA): SolutionQuality.SRP.prop1_i, SolutionQuality.SRP.prop1_ii, SolutionQuality.SRP.fbar_tendstoUniformlyOn (Bayraksan–Morton 2006) and DupacovaWets.Consistency.consistency_of_measurable_estimates (Dupačová–Wets 1988). Proofs of any milestone, and alternative routes to the goal, are welcome.

Selected references

• D. Bertsimas, N. Kallus, From Predictive to Prescriptive Analytics, arXiv:1402.5481v4, 2018; Management Science 66(3), 2020. https://arxiv.org/abs/1402.5481v4 , https://doi.org/10.1287/mnsc.2018.3253
• H. Walk, Strong laws of large numbers and nonparametric estimation, in Recent Developments in Applied Probability and Statistics, Physica-Verlag, 2010. https://doi.org/10.1007/978-3-7908-2598-5_8
• L. Devroye, L. Györfi, A. Krzyżak, G. Lugosi, On the strong universal consistency of nearest neighbor regression function estimates, Annals of Statistics 22(3), 1994. https://doi.org/10.1214/aos/1176325633
• J. Dupačová, R. Wets, Asymptotic behavior of statistical estimators and of optimal solutions of stochastic optimization problems, Annals of Statistics 16(4), 1988. https://doi.org/10.1214/aos/1176351052
• A. Shapiro, Monte Carlo sampling methods, in Handbooks in OR & MS 10, 2003. https://doi.org/10.1016/S0927-0507(03)10006-0

Motivation

Many operations decisions are made after observing side information: an inventory manager sees weather, search trends and calendar effects before ordering; a supply-chain planner sees market signals before shipping. Bertsimas and Kallus, in From Predictive to Prescriptive Analytics (arXiv:1402.5481v4, Management Science 2020), study how to turn such data into decisions. Besides their local, weight-based prescriptions (the subject of mission 1 of this series), their §8 analyses a second approach: choose a decision rule $z(\cdot)$ from a structured class, such as norm-bounded linear rules, by empirical risk minimization — minimizing the average historical cost of the rule.

The question this mission formalizes is the one any practitioner of that approach must answer: how far can the true expected cost of the chosen rule exceed its in-sample cost? Classical statistical learning answers it with Rademacher complexity (Bartlett and Mendelson, JMLR 2002), but only for real-valued predictors. Operations decisions are vectors (order quantities for several products, shipments to several locations), so the paper extends the theory to multivariate decision rules.

Setting

Covariates $x$ take values in a measurable space $\mathcal X$, the uncertain quantity $y$ in a measurable space $\mathcal Y$, and decisions $z$ in $\mathbb R^{d}$, unconstrained. Data are an i.i.d. sample $S_N=((x^1,y^1),\dots,(x^N,y^N))$ from a probability measure $\mu$ on $\mathcal X\times\mathcal Y$, and $S_N^x=(x^1,\dots,x^N)$ is its covariate part. A cost $c(z;y)$ is incurred when decision $z$ meets outcome $y$. A decision rule is a measurable map $z(\cdot):\mathcal X\to\mathbb R^d$; $\mathcal F$ is a class of decision rules. Its expected cost is $\mathbb E[c(z(X);Y)]$, and its empirical cost is $\frac1N\sum_{i=1}^N c(z(x^i);y^i)$, the objective of problem (4).

The empirical multivariate Rademacher complexity of $\mathcal F$ (Definition 3) on a sample $s_1,\dots,s_N$ is

$$\widehat{\mathfrak R}_N(\mathcal F;S_N)=\mathbb E_\sigma\Big[\frac2N\sup_{g\in\mathcal F}\sum_{i=1}^N\sum_{k=1}^d\sigma_{ik}\,g_k(s_i)\Big],$$

with $\sigma_{ik}$ independent uniform signs, and the marginal complexity $\mathfrak R_N(\mathcal F)$ is its expectation over the sample. For real-valued classes ($d=1$) these are the usual Rademacher complexities with factor $2/N$ and no absolute value. Lean notation: empRademacher, margRademacher, expCost, empCost, costClass in PrescAnalytics.ERM.

Formalization targets

Goal: Theorem 13 (out-of-sample guarantees)

If $0\le c(z;y)\le\bar c$ and $|c(z;y)-c(z';y)|\le L\|z-z'\|_\infty$, then for any $\delta>0$ each of the following holds with probability at least $1-\delta$:

$$\mathbb E[c(z(X);Y)]\le\frac1N\sum_{i=1}^N c(z(x^i);y^i)+\bar c\sqrt{\frac{\log(1/\delta)}{2N}}+L\,\mathfrak R_N(\mathcal F)\quad\forall z\in\mathcal F,\tag{26}$$ $$\mathbb E[c(z(X);Y)]\le\frac1N\sum_{i=1}^N c(z(x^i);y^i)+3\bar c\sqrt{\frac{\log(2/\delta)}{2N}}+L\,\widehat{\mathfrak R}_N(\mathcal F;S_N^x)\quad\forall z\in\mathcal F.\tag{27}$$

In particular they hold for the empirical risk minimizer. The goal is stated for a general class $\mathcal F$, not only the linear rules (25).

Milestones

1. Lemma 1 (comparison): for $\mathcal G=\{(x,y)\mapsto c(f(x);y):f\in\mathcal F\}$, $\widehat{\mathfrak R}_N(\mathcal G;S_N)\le L\,\widehat{\mathfrak R}_N(\mathcal F;S_N^x)$ and $\mathfrak R_N(\mathcal G)\le L\,\mathfrak R_N(\mathcal F)$.
2. Theorem 14 (29): for a class $\mathcal G$ of functions with values in $[0,\bar g]$, with probability at least $1-\delta$, $\mathbb E g\le\frac1N\sum_i g(u^i)+\bar g\sqrt{\log(1/\delta)/(2N)}+\mathfrak R_N(\mathcal G)$ for all $g\in\mathcal G$.
3. Theorem 14 (30): the data-dependent version with $3\bar g\sqrt{\log(2/\delta)/(2N)}+\widehat{\mathfrak R}_N(\mathcal G;S_N)$.

Significance

Theorem 13 says that the quantity empirical risk minimization optimizes is, up to confidence terms that do not depend on the rule, an upper bound on the true expected cost of every rule in the class, uniformly. Bound (27) is computable from data, so it certifies a learned policy without a holdout set. Combined with complexity bounds for norm-restricted linear rules (the paper's Lemmas 2 and 3, not part of this mission), it shows the confidence terms vanish as $N\to\infty$.

The results are known: (29) and (30) for $[0,\bar g]$-valued classes are the standard Rademacher bounds (Mohri, Rostamizadeh and Talwalkar, Foundations of Machine Learning, Thm 3.3, after rescaling). What is new in the paper is the $\infty$-norm vector comparison inequality of Lemma 1 with constant $1$. None of these statements has a machine-checked proof on the platform. A formal development would supply a reusable symmetrization-plus-McDiarmid pipeline and a vector contraction lemma. Related items posed in this repository are Bartlett–Mendelson's Theorem 8 (RadGauss.RiskBound.theorem_8, with an absolute value in the complexity and constant $\sqrt{8\ln(2/\delta)/n}$), Maurer's Euclidean vector contraction with constant $\sqrt2$ (SPOBounds.Margin.maurer_vector_contraction), and the open uniform law HighDimStat.UniformLaws.uniform_law_rademacher_complexity; none is the same statement as a target here.

Difficulty

The uniform bound needs three ingredients: a concentration inequality for the supremum of the deviation over the class (bounded differences), a symmetrization step relating the expected supremum to the Rademacher complexity, and a comparison inequality to pass from the cost class to the decision rules. The scalar contraction principle of Ledoux and Talagrand does not apply directly, since each cost depends on a $d$-dimensional output; applying it coordinatewise loses a factor of $d$, and Euclidean vector contraction loses $\sqrt2$ and uses the wrong norm. Lemma 1 needs an argument specific to the $\infty$-norm. Measure theory adds its own difficulty: the supremum over an uncountable class must be shown measurable before its expectation or probability means anything.

Formalization scope

Decisions are Fin d → ℝ, whose Lean norm is the $\infty$-norm; $\mathcal X$, $\mathcal Y$ are general measurable spaces. Samples are drawn from the product measure Measure.pi (fun _ : Fin N => μ), with $N\ge1$. The following readings are explicit:

• Each "with probability at least $1-\delta$, … for all $z\in\mathcal F$" is a bound $\le\delta$ on the outer measure of the set of samples where the inequality fails for some $z$; the quantifier over the class is inside the event.
• Empirical complexities are in EReal (an unbounded class gives $+\infty$), marginal ones are lower Lebesgue integrals in $[0,\infty]$; $0\cdot\infty=0$.
• The paper assumes only $\sup c\le\bar c$ (resp. $|g|\le\bar g$). With that alone (26) and (29) are false — a two-point outcome with a constant rule violates them with probability $1/2$ — so the costs are assumed to take values in $[0,\bar c]$, keeping every printed constant.
• The undefined $\delta',\delta''$ are $\delta$ (the i.i.d. case of the paper's Theorem 21); the Lipschitz denominator printed as $\|z_k-z'_k\|_\infty$ is $\|z-z'\|_\infty$.
• Decision rules and the cost are measurable and the class is pointwise separable (a countable subclass approximates every member pointwise). The paper takes probabilities and expectations of suprema over the class without comment; without such a convention the statement fails for pathological classes.

A trivializing formalization is ruled out: the quantifier over the class sits inside the probability, the complexity has no absolute value and is never a junk $0$ for unbounded classes, and the hypotheses are satisfied by a clipped newsvendor cost. Solvers will need McDiarmid's inequality, symmetrization with a ghost sample, and the comparison lemma; each is reusable for any Rademacher-based generalization bound. Formalizations of these tools as separate lemmas are welcome.

Selected references

• D. Bertsimas, N. Kallus, From Predictive to Prescriptive Analytics, arXiv:1402.5481v4, 2018; Management Science 66(3), 2020. https://arxiv.org/abs/1402.5481 , https://doi.org/10.1287/mnsc.2018.3253
• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, JMLR 3, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
• M. Ledoux, M. Talagrand, Probability in Banach Spaces, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4
• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018. https://mitpress.mit.edu/9780262039406/
• A. Maurer, A Vector-Contraction Inequality for Rademacher Complexities, ALT 2016. https://arxiv.org/abs/1605.00251

Why individual lower rates

Regularized least squares (RLS) in a reproducing kernel Hilbert space is a basic estimator of nonparametric regression and of kernel-based learning. Its learning rate is the speed at which the expected excess risk goes to zero as the sample size $\ell$ grows. A rate is useful only if it is known to be optimal, and optimality is a lower-bound statement about all learning algorithms.

Caponnetto and De Vito (Found. Comput. Math. 7 (2007)) prove two kinds of lower bound. The first is a minimax lower rate (their Theorem 2): for every algorithm and every $\ell$, some distribution in the prior is hard. Their Section 2 (p. 6) points out a weakness of this notion: the bad distribution may change with $\ell$. A practitioner, however, faces one fixed unknown distribution and asks how the error decreases as data accumulate. The individual lower rate answers that question. It asks for a single distribution, chosen against the algorithm but not depending on $\ell$, on which the expected excess risk stays above $a_\ell$ along infinitely many $\ell$.

The notion comes from nonparametric regression. Györfi, Kohler, Krzyżak and Walk (A Distribution-Free Theory of Nonparametric Regression, Springer 2002, §3, Theorem 3.3) proved individual lower rates for classes of smooth regression functions. Theorem 3 of Caponnetto–De Vito carries the result to vector-valued RKHS with the spectral priors $\mathcal P(b, c)$. Theorem 1 of the same paper shows that these priors are learned by RLS at rate $\ell^{-bc/(bc+1)}$.

Setting

The input space $X$ is Polish. The output space $Y$ is a real Hilbert space of finite dimension $d$. The hypothesis space $\mathcal H$ is a separable real Hilbert space of functions $f : X \to Y$ in which evaluation is continuous, so that $f(x) = K_x^* f$ for bounded operators $K_x : Y \to \mathcal H$. Hypothesis 1 asks that $(x, t) \mapsto \langle K_t v, K_x w\rangle_{\mathcal H}$ be measurable and that $\operatorname{Tr}(K_x^*K_x) \le \kappa$ for every $x$.

A distribution $\rho$ on $Z = X \times Y$ has marginal $\rho_X$ and conditional distributions $\rho(\cdot \mid x)$. The risk of $f \in \mathcal H$ is

$$\mathcal E[f] = \int_Z \|f(x) - y\|_Y^2 \, d\rho(x, y).$$

Hypothesis 2 asks for square-integrable outputs, a minimizer $f_{\mathcal H}$ of $\mathcal E$ over $\mathcal H$, and a Bernstein-type moment bound on the noise $y - f_{\mathcal H}(x)$ with constants $M, \Sigma$.

The operator $T = \int_X K_x K_x^*\, d\rho_X(x)$ on $\mathcal H$ satisfies $\langle Tf, g\rangle = \int_X \langle f(x), g(x)\rangle_Y \, d\rho_X$. Its nonzero eigenvalues are $t_1 \ge t_2 \ge \dots$, with orthonormal eigenvectors $e_n$.

For positive constants $M, \Sigma, R, \alpha, \beta$ and parameters $1 < b < \infty$, $1 \le c \le 2$, the prior $\mathcal P(b, c)$ (Definition 1) is the set of probability measures $\rho$ satisfying three conditions:

• Hypothesis 2 holds for the minimal-norm minimizer $f_{\mathcal H}$;
• $f_{\mathcal H} = T^{(c-1)/2} g$ with $\|g\|_{\mathcal H}^2 \le R$ (a source condition);
• the eigenvalues satisfy $\alpha \le n^b t_n \le \beta$ for all $n \ge 1$.

A learning algorithm is a sequence of maps $f_\ell : Z^\ell \to \mathcal H$, and $f^\ell_{\mathbf z}$ is its output on a sample $\mathbf z$ of size $\ell$ drawn from $\rho^\ell$.

Formalization targets

Goal: Theorem 3 (p. 11)

For every $B > b$,

$$\inf_{\{f_\ell\}}\ \sup_{\rho \in \mathcal P(b, c)}\ \limsup_{\ell \to \infty} \frac{\mathbb E_{\mathbf z \sim \rho^\ell}\big(\mathcal E[f^\ell_{\mathbf z}] - \mathcal E[f_{\mathcal H}]\big)}{\ell^{-cB/(cB+1)}} > 0 .$$

Equivalently, there is $C > 0$ such that every algorithm admits one $\rho \in \mathcal P(b, c)$ with expected excess risk at least $C\ell^{-cB/(cB+1)}$ for infinitely many $\ell$. The constant may depend on the prior and on $B$, but not on the algorithm.

Milestones

1. Proposition 7 (pp. 25–26). A fair sign $s$ observed as $y = sg + n$ with i.i.d. $\mathcal N(0, \sigma^2)$ noise has Bayes error $\Phi(-\|g\|/\sigma)$.
2. $\mathcal P' \subset \mathcal P(b, c)$ (pp. 26–27). This concerns distributions with marginal $\nu$ and conditional distribution $\mathcal N(m^{(s)}(x), \sigma^2\mathrm{Id})$, where

$$m^{(s)} = \sum_n s_n\sqrt{\gamma_n/t_n}\,e_n, \qquad \gamma_n = n^{-(Bc+1)}\tfrac{\epsilon}{\epsilon+1}\alpha^c R,$$

with $\epsilon = (B - b)c$ and $s \in \{\pm1\}^\infty$. Every such distribution belongs to the prior. 3. (63) (p. 27). Under these distributions, $\mathcal E[f] - \mathcal E[m^{(s)}] = \sum_n (c_n - s_n)^2\gamma_n$ with $c_n = \sqrt{t_n/\gamma_n}\langle f, e_n\rangle$. 4. (68) (p. 28, corrected). $\sum_{\ell\gamma_n \le 1} \gamma_n \ge \tfrac{u^{1/(Bc+1)}}{2Bc}\,\ell^{-Bc/(Bc+1)}$ for $\ell \ge (2Bc)^{Bc+1}/u$, where $u = \tfrac{\epsilon}{\epsilon+1}\alpha^c R$. 5. (67) (pp. 28–30). Averaged over independent fair signs $S$, the expected number of sign errors over $\{n : \ell\gamma_n \le 1\}$, weighted by $\gamma_n$, is at least $\Phi(-1/\sigma)\sum_{\ell\gamma_n \le 1}\gamma_n$.

Significance

Theorem 3 shows that no algorithm, RLS included, converges on every fixed distribution of $\mathcal P(b, c)$ faster than $\ell^{-cB/(cB+1)}$, for any $B > b$. For $c > 1$ this exponent is arbitrarily close to the exponent $bc/(bc+1)$ of the upper rate of Theorem 1, so RLS with the regularization parameter of Theorem 1 is near-optimal even in the individual sense. The paper notes (p. 6) that full individual optimality would still need an upper rate in expectation or an individual lower rate in probability; that question is outside this mission.

The theorem is proved on paper and has been cited widely. To our knowledge no part of it has been machine-checked. A formalization would produce:

• a checked reduction from a learning lower bound to Gaussian sign testing;
• a Lean model of Gaussian-noise regression with vector outputs;
• an explicit, checked version of the corrected computation (68).

Difficulty

A minimax argument picks a hard distribution for each $\ell$, and that is not allowed here: the distribution must be fixed before $\ell$ varies. The obvious repair, taking the worst distribution for one $\ell$ and keeping it, fails, because a distribution that is hard at sample size $\ell$ can be easy at sample size $10\ell$.

What has to be shown is a lower bound that holds for one distribution simultaneously along infinitely many sample sizes. Bounds that hold separately at each $\ell$, with a distribution that may depend on $\ell$, do not combine into such a bound.

A second difficulty arises in any reduction to a coordinatewise testing problem: each observation $y_i$ depends on all spectral coordinates of the regression function at once, so testing one coordinate is not literally the problem of Proposition 7.

Formalization scope

$\mathcal H$ is Mathlib's RKHS ℝ H X Y, with $K_x$ = RKHS.kerFun H x and $Y$ finite-dimensional. The paper's $\Sigma$ is written Sig.

• The operator $T$. It is never formed as an operator-valued integral. It enters through its quadratic form and through an eigen-system $(e_n, t_n)$ with summable weights.
• Indexing. Indices start at $0$, so the paper's $t_n$ is t (n-1).
• The prior. InPrior encodes $\rho \in \mathcal P(b, c)$, including "probability measure".
• Expectations. Expectations are lintegrals of nonnegative quantities, and samples are Fin ℓ → X × Y under the product measure.
• Algorithms. A learning algorithm is a family of maps from samples to $\mathcal H$, and it must be measurable.
• Added hypothesis. $\mathcal P(b, c)$ is assumed nonempty. The proof starts from "an arbitrary $\rho_0 \in \mathcal P(b, c)$", and with an empty prior the supremum is over the empty set and the statement fails.
• The noise. Gaussian noise with covariance $\sigma^2\mathrm{Id}$ is $\sigma\xi$ with $\xi \sim$ stdGaussian Y.
• $S^d$. It is read as the surface area of the unit sphere of $\mathbb R^d$.

Two parts of the print are corrected, and both corrections are stated in the items.

• (68). The printed constant $v = u^{-Bc/(Bc+1)}/(2Bc)$ and threshold $2Bc(2Bcu)^{Bc}$ come from dropping the factor $u$ in an integral, and the printed inequality fails for $u < 1/2$. The corrected constant is $u^{1/(Bc+1)}/(2Bc)$, with threshold $(2Bc)^{Bc+1}/u$.
• (67). It is stated with the explicit constant $C = \Phi(-1/\sigma)$ that the proof obtains.

The goal mentions none of $\mathcal P'$, $m^{(s)}$, $\gamma_n$ or $\Phi$. It is the lower rate (3) for the full prior $\mathcal P(b, c)$ with $a_\ell = \ell^{-cB/(cB+1)}$. A formalization that fixed the algorithm, let the distribution depend on $\ell$, or let the constant depend on the algorithm would prove a different, weaker statement.

A complete development needs:

• Gaussian measures on finite-dimensional inner product spaces, and the distribution function of the standard normal;
• conditional distributions on Polish products;
• infinite products of fair coins;
• series in Hilbert spaces with orthogonal terms.

Reusable pieces include Proposition 7, the Bayes-error monotonicity argument on p. 29, and the identification of the risk minimizer of a Gaussian-noise model. Contributions on any milestone are welcome, as are proofs of the measurability facts (elements of $\mathcal H$ are measurable under Hypothesis 1).

Selected references

• A. Caponnetto and E. De Vito, Optimal rates for the regularized least-squares algorithm, Found. Comput. Math. 7 (2007) 331–368. https://doi.org/10.1007/s10208-006-0196-8
• L. Györfi, M. Kohler, A. Krzyżak and H. Walk, A Distribution-Free Theory of Nonparametric Regression, Springer Series in Statistics, 2002 (§3, Theorem 3.3; Lemma 3.2).
• R. DeVore, G. Kerkyacharian, D. Picard and V. Temlyakov, Approximation methods for supervised learning, Found. Comput. Math. 6 (2006) 3–58.

Why lower bounds for kernel regression matter

Regularized least squares (RLS), also called kernel ridge regression, is one of the standard estimators of statistical learning: given a sample of input–output pairs, it fits a function from a reproducing kernel Hilbert space by minimizing the empirical squared error plus a multiple of the squared norm. Caponnetto and De Vito (FoCM 2007) proved that, over a class of distributions described by two parameters — the decay of the eigenvalues of the kernel's covariance operator and the smoothness of the regression function relative to it — RLS with a well-chosen regularization parameter converges at the rate $\ell^{-bc/(bc+1)}$ in the sample size $\ell$ (their Theorem 1). An upper rate on its own does not say whether another method could do better. This mission formalizes the matching minimax lower rate (their Theorem 2): when the output space is finite dimensional, no learning algorithm whatsoever converges faster than $\ell^{-bc/(bc+1)}$ uniformly over the class. Together the two theorems say that RLS is rate-optimal, and they are the reference point for later work on spectral regularization, early stopping and distributed kernel methods.

The paper's lower bound adapts the minimax analysis of DeVore, Kerkyacharian, Picard and Temlyakov (FoCM 2006) to the vector-valued RKHS setting.

Setting

Inputs $x$ lie in a Polish space $X$ and outputs $y$ in a real Hilbert space $Y$ of finite dimension $d$. The hypothesis space $\mathcal H$ is a separable Hilbert space of functions $f : X \to Y$ in which evaluation is continuous; $K_x : Y \to \mathcal H$ is the adjoint of evaluation at $x$, so $f(x) = K_x^* f$. Hypothesis 1 asks that $(x,t) \mapsto \langle K_t v, K_x w\rangle_{\mathcal H}$ be measurable and that $\operatorname{Tr}(K_x^*K_x) \le \kappa$ for every $x$.

A distribution $\rho$ on $Z = X \times Y$ has risk $\mathcal E[f] = \int \|f(x) - y\|^2\, d\rho$. Hypothesis 2 asks that $\int\|y\|^2 d\rho < \infty$, that the risk has a minimizer $f_{\mathcal H} \in \mathcal H$ (taken of minimal norm), and that the noise $y - f_{\mathcal H}(x)$ satisfies a Bernstein moment condition with constants $M, \Sigma$. With $\rho_X$ the marginal of $\rho$, the operator $T = \int K_x K_x^*\, d\rho_X(x)$ on $\mathcal H$ has the quadratic form $\langle Tf, g\rangle = \int \langle f(x), g(x)\rangle\, d\rho_X$ and a spectral decomposition $T = \sum_n t_n \langle\cdot, e_n\rangle e_n$.

The prior $\mathcal P(b,c)$ (Definition 1, with fixed positive $M, \Sigma, R, \alpha, \beta$, $1 < b < \infty$ and $1 \le c \le 2$) is the set of probability measures $\rho$ satisfying Hypothesis 2 with $M, \Sigma$ such that

• $T$ has infinitely many positive eigenvalues $t_1 \ge t_2 \ge \dots$ with $\alpha \le n^b t_n \le \beta$ (a capacity condition);
• $f_{\mathcal H} = T^{(c-1)/2} g$ for some $g$ with $\|g\|^2 \le R$ (a source condition).

Formalization targets

Goal: Theorem 2 (p. 11)

$$\lim_{\tau \to 0}\ \liminf_{\ell \to \infty}\ \inf_{f_\ell}\ \sup_{\rho \in \mathcal P(b,c)}\ \mathbb P_{\mathbf z \sim \rho^\ell}\Big[\mathcal E[f^\ell_{\mathbf z}] - \mathcal E[f_{\mathcal H}] > \tau\, \ell^{-\frac{bc}{bc+1}}\Big] = 1,$$

the infimum over all learning algorithms $f_\ell : Z^\ell \to \mathcal H$. The constant in front of the rate is left free, so the goal asserts only the exponent.

Milestones

1. Proposition 4 (p. 21): for $f = T^{(c-1)/2}g$, $\|g\|^2 \le R$, the explicit distribution $\rho_f$ with marginal $\nu$ (the marginal of some $\rho_0 \in \mathcal P(b,c)$) and $2d$-point conditional law is a probability measure with regression function $f$, and lies in $\mathcal P(b,c)$ when $\min(M,\Sigma) \ge 2(4d+1)\sqrt{\kappa^c R}$.
2. Proposition 4, (54): $\mathcal K(\rho_f, \rho_{f'}) \le \frac{16}{15 d L^2}\|\sqrt T(f - f')\|^2$ with $L = 4\sqrt{\kappa^c R}$.
3. Proposition 6 (p. 24): for $m > 16$ there are $N \ge e^{m/24}$ sign vectors in $\{-1,+1\}^m$ with pairwise $\sum_n(\sigma_i^n - \sigma_j^n)^2 \ge m$.
4. Proposition 5 (pp. 22–23): for small $\epsilon$ there are $N_\epsilon \ge e^{\gamma\epsilon^{-1/(bc)}}$ functions in the source class with $\epsilon \le \|\sqrt T(f_i - f_j)\|^2 \le 4\epsilon$.
5. Theorem 5 (p. 24): for every algorithm some $\rho_* \in \mathcal P(b,c)$ has $\mathbb P[\text{excess risk} > \epsilon/4] \ge \min\{N^*/(N^*+1),\ e^{-3/e}\sqrt{N^*}\, e^{-4\ell\epsilon/(15 d\kappa^c R)}\}$, $N^* = e^{\gamma\epsilon^{-1/(bc)}}$.

Significance

The result. Theorem 2 shows that the exponent $bc/(bc+1)$ attained by RLS cannot be improved by any estimator over $\mathcal P(b,c)$ when $\dim Y < \infty$; for $c = 1$ RLS is optimal up to a logarithmic factor. It separates what is a property of the problem class from what is a property of the algorithm: improvements to kernel methods must change the class (stronger assumptions) rather than the rate. The construction — a packing of the source class measured in the $\sqrt T$-norm, combined with a KL bound for an explicit noise model — is the template reused in many later lower bounds for kernel and inverse-problem estimators.

Formalizing it. The result has been proved since 2007; no machine-checked version exists. A formal proof needs the information-theoretic lower-bound machinery (a Fano-type inequality for many hypotheses), a Varshamov–Gilbert-type packing of the Hamming cube, KL divergence between explicit mixtures, and the spectral description of the covariance operator of a vector-valued RKHS. Each of these is reusable well beyond this paper. The mission also makes precise the paper's implicit conventions (see below), which a pen-and-paper reader fills in silently.

Difficulty

The upper half of the argument is not the hard part; the hard part is that the lower bound is uniform over all measurable algorithms, which no direct computation reaches. The step that does not follow from the paper alone is Theorem 5: its proof invokes Lemma 3.3 and Eq. 3.12 of DeVore et al., a Fano-type inequality bounding the probability of correct identification among $N$ hypotheses with pairwise KL divergence at most a given level. That lemma is not stated in the paper and is not in Mathlib; it must be formalized. A second obstacle is the packing (Proposition 6), whose proof is a probabilistic union bound with Hoeffding's inequality. A naive attempt to prove Theorem 2 by exhibiting a single bad distribution fails: for any fixed $\rho$ some algorithm (the constant one returning $f_{\rho}$) has zero excess risk, so the bad distribution must depend on the algorithm, and the order of quantifiers is essential.

Formalization scope

Mathlib's RKHS ℝ H X Y provides the function space with continuous evaluation, RKHS.kerFun is $K_x$, and InformationTheory.klDiv is the Kullback–Leibler information. The operator $T$ is never built as an operator-valued Bochner integral: it is recorded through its quadratic form $\int\langle f(x), g(x)\rangle d\rho_X$ and an eigen-system indexed by $\mathbb N$ from $0$ (the paper's $t_n$ is t (n-1)). The trace in Hypothesis 1 is a series over a Hilbert basis of $Y$; the conditional law in Hypothesis 2 is Measure.condKernel, and the moment integral there is a lintegral. $\mathcal E[f_{\mathcal H}]$ in the goal is $\inf_{f \in \mathcal H}\mathcal E[f]$.

Conventions and added hypotheses, each implicit on the page:

• $\mathcal P(b,c)$ is assumed nonempty; the proof fixes $\rho_0 \in \mathcal P(b,c)$, and over an empty prior the supremum is over the empty set and the statement is false.
• Algorithms are measurable maps $Z^\ell \to \mathcal H$; this is the reading under which the probability in the goal is defined, and it restricts the infimum relative to "all mappings".
• The constants $M, \Sigma, R, \alpha, \beta, \kappa$ are positive; the basis $(v_j)$ of $Y$ in Proposition 4 is orthonormal.
• Proposition 4's "$\|g\|^2 \le R$" for $f'$ is read as $\|g'\|^2 \le R$; Proposition 6's "$i \ne, j$" as $i \ne j$; (56) is required for $i \ne j$. The proof's variance display on p. 22 is wrong for $d \ge 2$, but the conclusion of Proposition 4 holds.

The goal is the $\varepsilon$–$\tau$–$L$ unfolding of the limit and mentions neither $\rho_f$, the KL bound nor the packing, so it cannot be discharged by any of the milestones' constructions in isolation; the distribution $\rho$ is chosen after the algorithm, never before it.

Contributions welcome: a general Fano/DeVore-type lemma for finitely many hypotheses, the Varshamov–Gilbert bound, KL ≤ χ² for finite mixtures, and lemmas relating covForm to the excess risk.

Selected references

• A. Caponnetto, E. De Vito, Optimal rates for the regularized least-squares algorithm, Found. Comput. Math. 7 (2007) 331–368. https://doi.org/10.1007/s10208-006-0196-8
• R. DeVore, G. Kerkyacharian, D. Picard, V. Temlyakov, Approximation methods for supervised learning, Found. Comput. Math. 6 (2006) 3–58. https://doi.org/10.1007/s10208-004-0158-6
• L. Györfi, M. Kohler, A. Krzyżak, H. Walk, A Distribution-Free Theory of Nonparametric Regression, Springer, 2002. https://doi.org/10.1007/b97848
• A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794

Motivation

Regularized least squares (RLS, also called kernel ridge regression or Tikhonov regularization) is the simplest learning algorithm built on a reproducing kernel Hilbert space. Given $\ell$ examples $(x_i,y_i)$ drawn independently from an unknown distribution $\rho$, it returns the function in a hypothesis space $\mathcal H$ that minimizes the empirical squared error plus $\lambda$ times the squared norm. It is used in regression, in multi-task learning with vector-valued outputs, and as the reference case for spectral regularization methods.

The basic statistical question is how fast the excess risk of the RLS estimator goes to zero as $\ell$ grows, and how to choose $\lambda=\lambda_\ell$ to get that speed. Caponnetto and De Vito (FoCM 2007) answered it for a family of priors $\mathcal P(b,c)$ described by two numbers: the decay rate $b$ of the eigenvalues of the covariance operator of the input distribution and the regularity $c$ of the target function. Their Theorem 1 gives the upper rate $\ell^{-bc/(bc+1)}$; Theorems 2 and 3 show that no algorithm does better when the output space is finite dimensional. This mission formalizes the upper rate.

Timeline. Cucker and Smale (2002) and De Vito, Caponnetto and Rosasco (2005) gave rates for RLS that did not depend on the eigenvalue decay of $\rho_X$. Zhang (2005) introduced the effective dimension $\mathcal N(\lambda)$ as the complexity measure. Caponnetto and De Vito (authors' copy dated 2006, published 2007) combined it with a source condition to obtain rates that are optimal over $\mathcal P(b,c)$, for vector-valued outputs. Steinwart, Hush and Scovel (2009) and Fischer and Steinwart (2020) later extended the analysis to other norms and to $c<1$.

Setting

The input space $X$ is a Polish space and the output space $Y$ is a real separable Hilbert space. The hypothesis space $\mathcal H$ is a real separable Hilbert space of functions $f:X\to Y$ in which evaluation at each point is continuous. For $x\in X$, $K_x:Y\to\mathcal H$ is the adjoint of evaluation at $x$, so $f(x)=K_x^*f$. Hypothesis 1 adds a measurability condition and a uniform trace bound $\operatorname{Tr}(K_x^*K_x)\le\kappa$.

A distribution $\rho$ on $Z=X\times Y$ has marginal $\rho_X$ and conditional laws $\rho(\cdot\mid x)$. The expected risk of $f\in\mathcal H$ is $\mathcal E[f]=\int\|f(x)-y\|_Y^2\,d\rho$. Hypothesis 2 asks that $\mathbb E\|y\|^2<\infty$, that $\mathcal E$ attains its infimum over $\mathcal H$ at some $f_{\mathcal H}$ (the minimizer of minimal norm is used), and that the noise $y-f_{\mathcal H}(x)$ satisfies a Bernstein moment condition with constants $M,\Sigma$.

The covariance operator $T=\int_XK_xK_x^*\,d\rho_X$ is positive and trace class, with $\langle Tf,f\rangle_{\mathcal H}=\int_X\|f(x)\|_Y^2\,d\rho_X$ and eigen-decomposition $T=\sum_nt_n\langle\cdot,e_n\rangle e_n$, $t_1\ge t_2\ge\dots>0$. The prior $\mathcal P(b,c)$, for $1<b<\infty$ and $1\le c\le2$, consists of the $\rho$ satisfying Hypothesis 2, with $f_{\mathcal H}=T^{(c-1)/2}g$ for some $\|g\|^2\le R$ (source condition), and with $\alpha\le n^bt_n\le\beta$ for all $n$ (eigenvalue decay).

The RLS estimator $f_{\mathbf z}^\lambda$ minimizes $\frac1\ell\sum_i\|f(x_i)-y_i\|_Y^2+\lambda\|f\|_{\mathcal H}^2$ over $\mathcal H$.

Formalization targets

Goal: Theorem 1, $1<b<+\infty$

With $\lambda_\ell=\ell^{-b/(bc+1)}$ and $a_\ell=\ell^{-bc/(bc+1)}$ for $c>1$, and $\lambda_\ell=a_\ell=(\log\ell/\ell)^{b/(b+1)}$ for $c=1$,

$$\lim_{\tau\to\infty}\limsup_{\ell\to\infty}\sup_{\rho\in\mathcal P(b,c)}\mathbb P_{\mathbf z\sim\rho^\ell}\Big[\mathcal E[f_{\mathbf z}^{\lambda_\ell}]-\mathcal E[f_{\mathcal H}]>\tau a_\ell\Big]=0.$$

The statement fixes the rate, not the constants: the threshold $\tau$ absorbs every constant of the prior.

Milestones

1. Proposition 1 iii)–v): the excess risk is $\|\sqrt T(f-f_{\mathcal H})\|^2$; the regularized expected and empirical risks have unique minimizers $f^\lambda=(T+\lambda)^{-1}Tf_{\mathcal H}$ and $f_{\mathbf z}^\lambda=(T_{\mathbf x}+\lambda)^{-1}g_{\mathbf z}$.
2. Proposition 2: a Bernstein inequality for means of i.i.d. Hilbert-space-valued variables.
3. Theorem 4: with probability $\ge1-\eta$,

$$\mathcal E[f_{\mathbf z}^\lambda]-\mathcal E[f_{\mathcal H}]\le3C_\eta\Big(\mathcal A(\lambda)+\frac{\kappa^2\mathcal B(\lambda)}{\ell^2\lambda}+\frac{\kappa\mathcal A(\lambda)}{\ell\lambda}+\frac{\kappa M^2}{\ell^2\lambda}+\frac{\Sigma^2\mathcal N(\lambda)}{\ell}\Big),$$

provided $\ell\ge2C_\eta\kappa\mathcal N(\lambda)/\lambda$ and $\lambda\le\|T\|$, where $C_\eta=32\log^2(6/\eta)$, $\mathcal A(\lambda)=\mathcal E[f^\lambda]-\mathcal E[f_{\mathcal H}]$, $\mathcal B(\lambda)=\|f^\lambda-f_{\mathcal H}\|^2$ and $\mathcal N(\lambda)=\operatorname{Tr}[(T+\lambda)^{-1}T]$. 4. Proposition 3: on $\mathcal P(b,c)$, $\mathcal A(\lambda)\le\lambda^c\|T^{(1-c)/2}f_{\mathcal H}\|^2$, $\mathcal B(\lambda)\le\lambda^{c-1}\|T^{(1-c)/2}f_{\mathcal H}\|^2$ and $\mathcal N(\lambda)\le\frac b{b-1}\beta^{1/b}\lambda^{-1/b}$.

Significance

The result. Theorem 1 says that RLS with $\lambda_\ell$ chosen from $(b,c)$ achieves the rate $\ell^{-bc/(bc+1)}$ uniformly over the prior, and the companion lower bounds show this is the minimax rate for $1<c\le2$ and finite-dimensional $Y$. The rate interpolates between the parametric rate $1/\ell$ (fast eigenvalue decay, smooth target) and slower nonparametric rates, and it identifies the effective dimension, rather than the dimension of $\mathcal H$, as the quantity that governs complexity. Theorem 4 is a non-asymptotic bound of independent use; it is the template for later analyses of spectral regularization, gradient descent with early stopping, and random-feature approximations of kernel methods.

The formalization. The result is proved on paper; no machine-checked proof of a kernel ridge regression rate is known to exist. A formal development requires a Bernstein inequality in Hilbert spaces, spectral calculus for a trace-class operator defined from a measure, and the operator-perturbation argument of Theorem 4. Two printed constants are corrected here: Theorem 4's proof yields $3C_\eta$, not $C_\eta$, and Proposition 3's bound on $\mathcal N(\lambda)$ has $\beta^{1/b}$ in place of $\beta$. The paper also states Theorem 1 for $b=+\infty$; that branch fails for $1\le c<2$ and is not posed.

Difficulty

The obvious argument bounds $\|f_{\mathbf z}^\lambda-f^\lambda\|_{\mathcal H}$ by uniform concentration of $T_{\mathbf x}$ around $T$ and multiplies by $\|\sqrt T\|$. That gives a variance term that ignores the eigenvalue decay of $T$, and hence a rate that does not improve with $b$. The optimal rate needs the variance measured through $\mathcal N(\lambda)$, which requires controlling $\sqrt T(T_{\mathbf x}+\lambda)^{-1}$ in operator norm with high probability. This in turn needs concentration of $(T+\lambda)^{-1/2}(T-T_{\mathbf x})$ in Hilbert–Schmidt norm, and the condition $\ell\gtrsim\mathcal N(\lambda)/\lambda$ under which the empirical operator is close enough to $T$. The noise is unbounded, so only the moment condition (9) is available, and the concentration step must use moment bounds rather than boundedness.

Formalization scope

$\mathcal H$ is Mathlib's RKHS ℝ H X Y, and $K_x$ is RKHS.kerFun H x. The trace in Hypothesis 1 is computed in a fixed Hilbert basis of $Y$. $\rho_X$ is the first marginal and $\rho(\cdot\mid x)$ is condKernel. The operator $T$ is not built as an operator-valued integral. It enters through its quadratic form $\int\langle f(x),g(x)\rangle\,d\rho_X$ and through an eigen-system $(e_n,t_n)$, indexed from $0$, so (17) reads $\alpha\le(n+1)^bt_n\le\beta$. The effective dimension is $\sum_nt_n/(t_n+\lambda)$. Samples are Fin ℓ → X × Y under the product measure, and probabilities of events are outer measures. "With probability at least $1-\eta$" is stated as "the bad event has measure at most $\eta$". The noise condition and the moments of Proposition 2 are integrals of nonnegative functions with values in $[0,\infty]$.

The hypotheses the paper uses but does not display are added: positivity of $M,\Sigma,R,\alpha,\beta,\kappa$, and integrability of the random variable in Proposition 2. The RLS estimator of the goal is any family of minimizers of (18) for $\ell\ge2$; at $\ell=1$ and $c=1$ the parameter $\lambda_1=0$ is degenerate. The goal quantifies uniformly: $L$ is chosen before $\rho$, and the estimator is fixed before $\rho$. The goal must not be replaced by a statement about $\mathcal A,\mathcal B,\mathcal N$ or by Theorem 4's event: it is the uniform rate for the estimator itself.

Reusable infrastructure: Hilbert-space Bernstein inequalities (Proposition 2 alone is a valuable target), spectral calculus for compact positive operators given by a quadratic form, and the representer/normal equation for vector-valued RLS. Contributions of proofs for any milestone, and of supporting lemmas about trace-class operators and effective dimension, are welcome.

Selected references

• A. Caponnetto, E. De Vito, Optimal rates for the regularized least-squares algorithm, Found. Comput. Math. 7 (2007) 331–368. https://doi.org/10.1007/s10208-006-0196-8
• F. Cucker, S. Smale, On the mathematical foundations of learning, Bull. Amer. Math. Soc. 39 (2002) 1–49. https://doi.org/10.1090/S0273-0979-01-00923-5
• E. De Vito, A. Caponnetto, L. Rosasco, Model selection for regularized least-squares algorithm in learning theory, Found. Comput. Math. 5 (2005) 59–85. https://doi.org/10.1007/s10208-004-0134-1
• T. Zhang, Learning bounds for kernel regression using effective data dimensionality, Neural Comput. 17 (2005) 2077–2098. https://doi.org/10.1162/0899766054323008
• I. Pinelis, Optimum bounds for the distributions of martingales in Banach spaces, Ann. Probab. 22 (1994) 1679–1706. https://doi.org/10.1214/aop/1176988477
• I. Steinwart, D. Hush, C. Scovel, Optimal rates for regularized least squares regression, COLT 2009. https://www.cs.mcgill.ca/~colt2009/papers/038.pdf
• S. Fischer, I. Steinwart, Sobolev norm learning rates for regularized least-squares algorithms, J. Mach. Learn. Res. 21 (2020) 1–38. https://jmlr.org/papers/v21/19-734.html