Statistics

Motivation

In 1955 Charnes, Cooper and Ferguson proposed to estimate the weights of an executive compensation scheme by linear programming instead of least squares: the weights minimise a sum of absolute deviations subject to ranking, ceiling and floor constraints, which is a linear program. The coefficients of that program are not known exactly. They are averages of ratings collected from a sample of job holders, so the program actually solved is a random perturbation of a "true" program built from population means. The Appendix of the paper (§8, Consistency of Estimates) asks the basic statistical question about such an estimator: as the sample grows, does the optimal solution of the sample program converge to the optimal solution of the true program?

The question is not specific to compensation. Whenever the constraint matrix of a linear program is estimated from data, the computed optimum is an estimator, and its consistency is the first property one wants. The Appendix is one of the earliest statements of this kind for linear programming, written at a time when the simplex method itself was only a few years old (Dantzig 1951).

Setting

Fix integers $m$ (the number of constraints, indexed by $i$) and $n$ (the number of variables, indexed by $j$), a right-hand side $b\in\mathbb R^m$ and a cost vector $c\in\mathbb R^n$. For a real $m\times n$ matrix $X=(x_{ij})$ consider the linear program (8)

$$\min\ \sum_j c_ja_j\quad\text{subject to}\quad \sum_j x_{ij}a_j\ge b_i\ \ (i=1,\dots,m),\qquad a_j\ge0\ \ (j=1,\dots,n).$$

Its feasible set $F(X,b)$ is a polyhedron in $\mathbb R^n$, and a minimizing solution is a feasible point at which the objective is no larger than at any other feasible point.

The true matrix $\xi=(\xi_{ij})$ collects population means. For each sample size $N$ the observed matrix is

$$x_{ij}=\xi_{ij}+\eta_{ij}\qquad(9)$$

where the sampling errors $\eta_{ij}=\eta^{(N)}_{ij}$ are random variables on a probability space $(\Omega,\mathcal F,P)$ with $\eta_{ij}\to0$ in probability as $N\to\infty$.

The paper makes two assumptions about the true program:

• (I) the program (8) with matrix $\xi$ has a unique solution vector $\hat\alpha$;
• (II) every set of $m$ columns of $\xi$ is linearly independent.

A feasible point $a$ is nondegenerate if the number of strictly positive variables $a_j$ plus the number of constraints with strictly positive surplus $\sum_jx_{ij}a_j-b_i$ equals $m$. At an extreme point this means that the basis of the point, after adding one surplus variable per constraint, consists of $m$ strictly positive basic variables.

Formalization targets

Goal: consistency of the LP estimate

Under (I), (II) and nondegeneracy of $\hat\alpha$, for every $\varepsilon>0$,

$$P\bigl(\text{(8) with matrix }\xi+\eta^{(N)}\text{ has a unique minimizing solution }\hat a\text{ and }|\hat a-\hat\alpha|<\varepsilon\bigr)\longrightarrow1\qquad(N\to\infty).$$

The event asserts that the sample minimiser exists and is unique, as the paper's phrase "the minimizing solution of (8), $\hat a(\eta)$" presupposes, and that it is close to $\hat\alpha$.

Milestones

1. Claim A (p. 150): linear independence of a set of columns is preserved under sufficiently small entrywise perturbation.
2. Claim B (p. 150): the extreme points of $F(X,b)$ are exactly the feasible points whose positive variables and positive surpluses index linearly independent columns of $[X,-I]$.
3. Corresponding extreme points (p. 150): a nondegenerate extreme point of the true set has, for every nearby matrix, an extreme point of the sample set with the same positive support, arbitrarily close to it.
4. The Lipschitz bound (p. 151): $|c'(\alpha-a)|\le B|\alpha-a|$ for a positive constant $B$.
5. The gap argument (p. 151), deterministic form: under (I) and nondegeneracy of $\hat\alpha$, every matrix close enough to $\xi$ gives a program with a unique minimiser, close to $\hat\alpha$.

A companion item records that the claim as printed, under (I) and (II) alone, is false.

Significance

The theorem says that the linear programming estimator of the paper is consistent: with enough data, the computed weights are, with high probability, the unique optimum of the sample program and close to the true weights. More generally it is a stability statement for linear programs with a unique nondegenerate optimum under perturbation of the constraint matrix, which is the setting of sensitivity analysis and of sample-average approximation for linear programs.

The paper gives a sketch, not a complete proof. Its argument transfers extreme points of the true polyhedron to the sample polyhedron and compares objective values. That transfer is valid at nondegenerate extreme points only, and the claim as printed fails without such a condition: for $\xi=\begin{pmatrix}1&1\\-1&-2\end{pmatrix}$ and $b=(1,-1)$ the true feasible set is the single point $(1,0)$, so (I) holds, the two columns are independent, so (II) holds, yet replacing $\xi_{11}$ by any value in $(\tfrac12,1)$ makes the program infeasible. The mission therefore adds one disclosed hypothesis, nondegeneracy of the true optimum $\hat\alpha$, and keeps everything else as on the page. To the best of the curators' knowledge, neither the paper's statement nor the repaired one has been machine-checked; this mission formalizes the repaired theorem, the steps of the paper's argument, and the counterexample to the printed statement.

Difficulty

The natural first idea is that the feasible set and the optimum move continuously with the data. That is false in general: a polyhedron defined by perturbed inequalities can lose extreme points, gain new ones, or become empty, and the optimum of a linear program is not a continuous function of the constraint matrix. The paper's claim that the sample polyhedron has "precisely the same number of extreme points as the true convex set" and that the parenthetical of claim B is preserved under small modifications both fail at degenerate extreme points. The difficulty is to control, near a unique nondegenerate optimum $\hat\alpha$, both the feasibility of the sample program and the identity of its optimal extreme point, and to turn this into a probability statement without any measurability assumption on the estimator.

Formalization scope

All objects live in the namespace ExecCompLP.Consistency. Matrices are Matrix (Fin m) (Fin n) ℝ with X i j the entry $x_{ij}$; column $j$ is fun i => X i j. Indices are 0-based. Vectors are Fin n → ℝ, and distances between them use the maximum norm (dist on Fin n → ℝ); closeness of matrices is entrywise. Every norm gives the same statements.

• The optimal value of (8) is never defined as an infimum; a minimizer is a feasible point no worse than every feasible point. Assumption (I) includes existence.
• Assumption (II) is about $m$-element sets of columns, with $m$ the number of rows; it is vacuous when $n<m$, as on the page. It is a hypothesis of the goal, as printed, although the repaired argument does not need it; milestone 5 drops it.
• Nondegeneracy of $\hat\alpha$ is the only added hypothesis. It is not replaced by anything stronger (nondegeneracy of all extreme points, a Slater point, boundedness).
• Randomness enters only through $\eta^{(N)}_{ij}\to0$ in probability (TendstoInMeasure), which is the conclusion of (9) on p. 149 taken as a hypothesis; sample means and variances are not modelled. The probability of the goal's event is an outer measure, so no measurability of $\eta$ or of the estimator is assumed.
• Ruled out as trivializations: a conclusion that only bounds every minimizer "if any" (vacuous on infeasible samples), and a conclusion conditioned on feasibility. The goal's event asserts existence and uniqueness of the sample minimizer.

A complete development needs: openness of linear independence, the inequality-form characterization of extreme points by linearly independent positive columns, continuity of basic solutions in the data, and positivity of reduced costs at a unique nondegenerate optimum. The first three are reusable for any perturbation analysis of linear programs. Proofs of any item, and alternative arguments for the goal, are welcome.

Selected references

• A. Charnes, W. W. Cooper and R. O. Ferguson, Optimal estimation of executive compensation by linear programming, Management Science 1(2):138–151, 1955. https://doi.org/10.1287/mnsc.1.2.138
• G. B. Dantzig, Maximization of a linear function of variables subject to linear inequalities, in T. C. Koopmans (ed.), Activity Analysis of Production and Allocation, Wiley, 1951.
• L. S. Pontryagin, Foundations of Combinatorial Topology, Graylock Press, 1952 (cited for claim A).
• W. Feller, An Introduction to Probability Theory and Its Applications, Wiley, 1950 (cited for (9)).

Why coverage of an optimal value matters

Many stochastic optimization problems choose a decision by minimizing an expected loss. The optimum depends on an unknown distribution, so a data-based optimum alone gives no measure of uncertainty about the best achievable expected loss. This mission concerns a confidence set for that optimal value, rather than a confidence set for the decision itself. The result of Duchi, Glynn, and Namkoong shows that a broad class of divergence neighborhoods of the empirical distribution yields a calibrated limit for this set. The same construction covers nonsmooth losses and constrained decisions when the regularity assumptions below hold.

The paper develops generalized empirical likelihood for smooth functionals of a distribution and then applies it to optimization. Its Theorem 3 states the exact asymptotic coverage result for the optimal value; Appendix C identifies the functional derivative, while Appendix B gives the uniform linearization and expansion on which calibration rests. The statistical result is proved in the paper. The mission asks for a machine-checked development of its statements and proof under an explicit nondegeneracy condition required by the paper's general coverage theorem.

Decisions, losses, and divergence neighborhoods

Let $\mathcal X\subseteq\mathbb R^d$ be a nonempty compact decision set. An observation $\xi$ has population law $P_0$, and $\ell(x;\xi)\in\mathbb R$ is the loss at decision $x$. The quantity of interest is the optimal-value functional

$$T_{\rm opt}(P)=\inf_{x\in\mathcal X}\mathbb E_P[\ell(x;\xi)].$$

The observations $\xi_1,\ldots,\xi_n$ are independent and identically distributed with law $P_0$. Write $\widehat P_n$ for their empirical distribution. A candidate distribution supported on the indexed observations is represented by nonnegative weights $p_i$ with $\sum_i p_i=1$. Indexed weights also cover samples with repeated observations. For a convex divergence generator $f$ normalized by $f(1)=f'(1)=0$ and $f''(1)=2$, its divergence from the empirical law is $D_f(p\|\widehat P_n)=n^{-1}\sum_i f(np_i)$. Assumption A further requires $f$ to be three times continuously differentiable near $1$; it permits $f(0)=+\infty$.

At radius $\rho/n$, the divergence ball consists of the weights with $\sum_i f(np_i)\le\rho$. The confidence set is its image under $T_{\rm opt}$:

$$C_{n,\rho}=\{T_{\rm opt}(p):D_f(p\|\widehat P_n)\le\rho/n\}.$$

Assumption B makes $\mathcal X$ compact and requires $\ell(\cdot;\xi)$ to be Lipschitz on it with a measurable random coefficient $M(\xi)$. The theorem adds finite second moments for $M$ and for the loss at one feasible decision. These conditions control losses at every feasible decision. They also make the population and weighted empirical infima finite on the cases used in the limit.

Formalization targets

The goal is the exact asymptotic coverage of the population optimal value, with $x^\star$ the unique optimizer and $\operatorname{Var}_{P_0}(\ell(x^\star;\xi))>0$:

$$P^*\!\left(T_{\rm opt}(P_0)\in C_{n,\rho}\right)\longrightarrow P(\chi_1^2\le\rho),\qquad \rho\ge0.$$

Here $P^*$ denotes outer probability, and $\chi_1^2$ is the square of a standard normal variable. The milestone statements follow the paper's path to this theorem. Lemma 17 gives the directional derivative of an optimal-value functional. Lemma 13 bounds feasible empirical weights relative to uniform weights. Lemma 16 makes the nonlinear remainder uniformly negligible on the divergence ball. The display after (37) then gives a first-order expansion of the upper endpoint of $C_{n,\rho}$; the next display gives its one-sided Gaussian coverage limit. The goal concerns membership in the image set $C_{n,\rho}$, including both sides of that interval.

What the result provides

The limit specifies a radius through a one degree of freedom chi square quantile. It applies to the value of a constrained stochastic optimization problem without requiring the optimizer or the loss to be differentiable. The positive variance condition ensures that the influence function supplies a genuine Gaussian scale. Without such a condition, a deterministic optimal loss can make coverage identically one, so the stated chi square limit would fail. The general theorem in the paper explicitly requires positive influence variance; this mission makes the condition visible in the specialized optimal-value statement.

A complete formalization would connect finite-sample divergence geometry to an asymptotic confidence claim about an optimization functional. The empirical mean and variance definitions, divergence ball, and normalized generator already exist as reusable declarations. This mission adds the optimal-value functional, its influence function, the nonlinear remainder, and the statistical limits. Those definitions can also support later confidence statements for other stochastic optimization models. The result is proved in the source paper; the Lean statements here are open targets awaiting proofs.

The mathematical obstacle

Pointwise control of each loss $\ell(x;\xi)$ is insufficient for the optimal value: the decision minimizing an empirical weighted objective can move with the weights. A pointwise mean expansion therefore does not by itself control the infimum over $x$. The required limit combines uniform control over the loss class with sensitivity of the infimum functional near its population minimizer. The uniform remainder in Lemma 16 is stronger than a statement for the ordinary empirical distribution because it covers every distribution in the shrinking divergence ball. The final event is membership in the image of that ball; bounds on its upper endpoint alone do not establish two-sided coverage.

Formalization scope

Lean represents decisions by EuclideanSpace ℝ (Fin d) and assumes a nonempty compact feasible set. Assumption B uses its Euclidean norm. The paper allows any norm in finite dimension; norm equivalence permits this choice after rescaling the Lipschitz coefficient. The population law is the pushforward of the first measurable observation from a probability space. Samples are indexed from zero, so the first $n$ observations are indices $0,\ldots,n-1$. Independence and identical distribution are explicit hypotheses. Loss measurability is explicit so the population integrals have their intended values. Square integrability and compact Lipschitz control keep the real infima meaningful.

The generator takes values in EReal so a divergence infinite at zero is representable. The ball uses the published probability uncertainty set with radius $\rho/n$ and includes nonnegativity and unit mass. Its weights represent distributions absolutely continuous with respect to the empirical law. With tied observations, equal splitting across copies preserves the induced distribution and does not increase a convex divergence. The upper endpoint is $\sup_p\inf_x$; the different minimax expression $\inf_x\sup_p$ is not substituted. The chi square target uses the standard Gaussian measure of $\{z:z^2\le\rho\}$.

Mathlib measures are outer measures on arbitrary sets, so the probability of a possibly nonmeasurable membership or supremum event is the paper's outer probability. The Lemma 17 milestone expresses a signed measure through its action $H(x)$ on the losses, as Appendix C.2 does, and uses positive directional steps. Real suprema and infima are used only where the hypotheses provide nonempty bounded values. The variance hypothesis rules out the trivial deterministic-loss counterexample. Useful contributions include the compactness and continuity facts needed for those extrema, the action-level derivative, empirical process limits, and the final two-sided event argument.

Selected references

• John C. Duchi, Peter W. Glynn, and Hongseok Namkoong, Statistics of Robust Optimization: A Generalized Empirical Likelihood Approach, arXiv:1610.03425v3, 2018; published in Mathematics of Operations Research 46(3), 2021. arXiv preprint

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