The OR Formalization Drive

Motivation

Smooth optimization with nonnegative variables appears when the variables are Lagrange multipliers for inequality constraints or when an objective incorporates an augmented Lagrangian or an exact penalty. Bertsekas studies how to retain a Newton-like convergence rate in this setting while using an iteration that projects a scaled gradient step onto the nonnegative orthant. His 1982 paper also discusses large optimal-control examples, where repeatedly solving a quadratic subproblem may be costly. These are the applications motivating the method, rather than assumptions of the theorem. Bertsekas, 1982.

The paper contrasts a partly diagonal scaling matrix with two other approaches: a fully diagonal projected gradient step, which generally has a linear rate, and a constrained Newton step defined by a quadratic program. The main theoretical question is whether the simpler projected iteration can still identify binding coordinates and converge superlinearly near the solution. The mission covers the nonnegative-orthant method in §2 and its stated convergence results. The paper's later extension to general linear constraints and its computational examples concern different objects. Bertsekas, 1982.

Setting

Fix a dimension $n\ge1$ and a continuously differentiable function $f:\mathbb R^n\to\mathbb R$. Problem (1) minimizes $f(x)$ over the nonnegative orthant $\mathbb R_+^n=\{x:x^i\ge0\text{ for every }i\}$. The positive part $[z]^+$ replaces each negative coordinate of $z$ by zero. A feasible $x$ is critical when every partial derivative $\partial_i f(x)$ is nonnegative and $\partial_i f(x)=0$ wherever $x^i>0$. This is the paper's componentwise first-order condition.

For a feasible iterate $x_k$, the binding set is $B(x_k)=\{i:x_k^i=0\}$. The paper selects a larger working set $I_k^+$ using a fixed $\varepsilon>0$ and the projected-gradient residual $w_k=\|x_k-[x_k-M\nabla f(x_k)]^+\|$, where $M$ is fixed, diagonal and positive definite. More precisely, $I_k^+$ contains the indices with $0\le x_k^i\le\min(\varepsilon,w_k)$ and $\partial_i f(x_k)>0$. The matrix $D_k$ is symmetric positive definite and has zero off-diagonal entries in the rows indexed by $I_k^+$. The projected arc and update are

$$p_k=D_k\nabla f(x_k),\qquad x_k(a)=[x_k-a p_k]^+,\qquad x_{k+1}=x_k(\beta^{m_k}).$$

Here $0<\beta<1$, and $m_k$ is the first nonnegative integer passing the paper's two-sum Armijo test (37), with $0<\sigma<1/2$. One sum uses the scaled gradient outside $I_k^+$; the other uses the actual projected displacement on $I_k^+$. These details define the algorithm whose rate is at issue. Bertsekas, 1982, pp. 228–229.

Formalization targets

The first targets establish the fixed-point and descent properties of the projected arc, positivity of the Armijo right-hand side, well-defined step selection, criticality of limit points, and local attraction with finite binding-set identification. Proposition 3 identifies both the working set and the actual binding set:

$$I_k^+=B(x_k)=B(x^*)\quad\text{for all sufficiently late }k.$$

The goal is Proposition 4. Let $f$ be convex and $C^2$, let $x^*$ be the unique minimizer on $\mathbb R_+^n$ satisfying Assumption (C), and suppose the Hessian quadratic form has uniform positive lower and finite upper bounds on the initial, unrestricted sublevel set. The scaling matrix is $D_k=H_k^{-1}$, where $H_k$ retains Hessian entries except for off-diagonal entries touching $I_k^+$. Then

$$x_k\longrightarrow x^*,\qquad \forall c>0\ \exists K\ \forall k\ge K:\ \|x_{k+1}-x^*\|\le c\|x_k-x^*\|.$$

If the Hessian is Lipschitz in a neighborhood of $x^*$, the same proposition states an at-least-quadratic error bound: $\|x_{k+1}-x^*\|\le C\|x_k-x^*\|^2$ eventually for some $C>0$. The separate final milestone records the paper's claim that the initial unit trial is eventually accepted. Bertsekas, 1982, pp. 233–236.

Significance

Proposition 4 says that this specific orthant-projected Newton iteration converges to the unique constrained optimum with a superlinear rate under its stated smoothness and curvature conditions. Proposition 3 supplies a distinct finite-identification statement: the working and binding coordinates eventually match those at the optimum. These facts specify the behavior of an algorithm that does not define its direction by solving a quadratic program at every step. The paper proves the preceding propositions and states Proposition 4 with its proof left to the reader, referring to its earlier discussion and standard unconstrained Newton results. Bertsekas, 1982, pp. 234–236.

Formalizing the claims would provide machine-checked statements and, once solved, proofs for the exact projected arc, two-part line search, matrix selection, identification result and rate conclusion. The local mission items are open proof obligations; their compilation checks the definitions and theorem types, not the mathematical claims. The geometry definitions can also support other orthant-constrained algorithms, while the enlarged working set and Armijo rule belong to this paper's method.

Difficulty

A positive definite matrix by itself does not make projection along $[x-aD\nabla f(x)]^+$ a descent move. An off-diagonal coupling can push coordinates against the boundary in a way that defeats the usual unconstrained descent calculation; the paper gives such a situation before Proposition 1. The partly diagonal condition is therefore substantive. A second obstacle is that the exact active set $I^+(x)$ can jump at a boundary point: iterates approaching that point from the interior need not have the same indexed rows. The enlarged $I_k^+$ and its dependence on the residual are central to the finite-identification and rate claims. Bertsekas, 1982, pp. 225–229.

Formalization scope

Lean represents $\mathbb R^n$ as EuclideanSpace ℝ (Fin n), with the Euclidean norm and zero-based coordinates. The dimension is positive. gradient and the derivative of gradient represent first and second derivatives; the paper's $M$ is diag μ with every $\mu^i>0$. The run predicate includes a feasible initial point and the first acceptable integer $m_k$, and the matrix choices are indexed by iteration. Propositions 1–3 use the paper's explicit admissibility condition. Proposition 4 constructs $D_k$ from $H_k$ and does not assume its invertibility, admissibility, convergence or eventual active-set equality.

Assumption (C) includes local $C^2$ smoothness, curvature bounds on directions zero at the binding coordinates, and strict complementarity. A local minimum is required to be feasible as well as locally minimal on the orthant. Limit points use subsequential convergence. Superlinearity uses a uniform eventual error inequality, which also covers an iterate that reaches the solution exactly; a ratio with a zero denominator would distort this case. The paper's Proposition 4 display mistakenly binds a direction to the level set while leaving the Hessian's point free. The formalization states the intended reading: every point in the unrestricted initial level set and every direction satisfy the Hessian bounds. The displayed level set has no $x\ge0$ restriction, so neither does the Lean hypothesis.

A definition that accepts any Armijo exponent or a goal that assumes the eventual identification or convergence conclusion would erase the paper's claim. Contributions can build the matrix and projected-arc lemmas, the convergence and identification proofs, and the final rate proof. The local inverse-Hessian observation before Proposition 4 is discussed in the notes but has no separate milestone until its full local setting can be captured without weakening it.

Selected references

• Dimitri P. Bertsekas, Projected Newton Methods for Optimization Problems with Simple Constraints, SIAM Journal on Control and Optimization 20(2), 221–246, 1982. DOI: 10.1137/0320018.

Motivation: curvature of the central path as a complexity measure

Path-following interior point methods solve a linear program by tracking its central path, a smooth curve that runs through the interior of the feasible set and ends at an optimal solution. Their number of iterations is polynomial in the bit size of the input, and whether some interior point method is strongly polynomial (bounded by a polynomial in the number of variables and constraints alone) is open. Bayer and Lagarias called the central path "a fundamental mathematical object underlying Karmarkar's algorithm". Dedieu and Shub proposed its total curvature as an informal complexity measure: a path that turns little should be easy to follow with straight steps. Several results bound that curvature:

• 2005. Dedieu and Shub conjecture that the total curvature of the central path is bounded linearly in the dimension. Dedieu, Malajovich and Shub prove an $O(n)$ bound on average over the regions of a hyperplane arrangement. De Loera, Sturmfels and Vinzant later obtain the same averaged bound with matroid methods (arXiv:1012.3978).
• 2008–2009. Deza, Terlaky and Zinchenko build redundant Klee–Minty cubes and "snakes" with curvature $\Omega(m)$ for $m$ inequalities, which refutes the dimension version. They then conjecture the continuous analogue of the Hirsch conjecture: the total curvature is bounded linearly in the number of constraints.
• 2014–2017. Allamigeon, Benchimol, Gaubert and Joswig disprove that conjecture with a family of linear programs whose central paths have curvature exponential in the number of constraints. The bound first appeared in arXiv:1405.4161 and was given an elementary tropical proof in arXiv:1708.01544v2, Theorem 25, which is the result of this mission.

Setting

A linear program in slack form has a real $m\times n$ matrix $A$, $b\in\mathbb R^m$, $c\in\mathbb R^n$ and $N:=n+m$:

$$\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. } Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .$$

For $\mu>0$ the point of the central path $(x^\mu,w^\mu,s^\mu,y^\mu)\in\mathbb R^{2N}$ is the unique solution of

$$Ax+w=b,\quad s-A^\top y=c,\quad x_js_j=\mu,\quad w_iy_i=\mu,\quad x,w,s,y>0. \tag{1}$$

The primal central path is $\mu\mapsto(x^\mu,w^\mu)\in\mathbb R^N$.

For $r\ge1$ and $t>0$, the program $\mathbf{LW}_r(t)$ minimizes $x_1$ over $x\in\mathbb R^{2r}$ subject to

$$x_1\le t^2,\quad x_2\le t,\quad x_{2j+1}\le t\,x_{2j-1},\quad x_{2j+1}\le t\,x_{2j},\quad x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ \ (1\le j<r),\quad x\ge0 .$$

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$, $m=3r-1$, $N=5r-1$.

For points $U,V,W$ of Euclidean space with $U\ne V\ne W$, the turning angle $\angle UVW\in[0,\pi]$ is the angle between the vectors $V-U$ and $W-V$. For a curve $\sigma$ parameterized over $I\subseteq\mathbb R$, the total curvature is

$$\kappa(\sigma,I)=\sup\Big\{\sum_{k=1}^{p-1}\angle\,\sigma(\mu_{k-1})\sigma(\mu_k)\sigma(\mu_{k+1})\ :\ \mu_0<\dots<\mu_p\ \text{in } I\Big\}\in[0,+\infty].$$

The milestones also use the field $\mathbb K$ of absolutely convergent generalized real Puiseux series $\sum_{\alpha\in\mathbb R}a_\alpha t^\alpha$. Such a series can be evaluated at large real $t$, and it has a valuation $\mathrm{val}\in\mathbb T=\mathbb R\cup\{-\infty\}$, its leading exponent. Read over $\mathbb K$, $\mathbf{LW}_r$ is one linear program. The valuation of its central path at $\mu=t^\lambda$ is the tropical central path $\mathcal C^{\mathrm{trop}}(\lambda)\in\mathbb R^{2N}$, a piecewise-linear curve with an explicit recursive description (Propositions 20–21 of the paper).

Formalization targets

Goal: Theorem 25

For every $r\ge1$ and $\epsilon>0$ there is $t_0$ such that for all $t>t_0$,

$$\kappa\big(\mu\mapsto(x^\mu,w^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon\quad\text{and}\quad\kappa\big(\mu\mapsto(x^\mu,w^\mu,s^\mu,y^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon$$

for the central path of $\mathbf{LW}^=_r(t)$. Here $t_0$ may depend on $r$ and $\epsilon$. Both the primal and the primal-dual curves are part of the goal, as in the paper.

Milestones, in the order of the paper's argument

1. Lemma 22: for non-null $\mathbf x,\mathbf y\in\mathbb K^d$, the angle $\angle\mathbf x(t)\mathbf y(t)$ has a limit, which is $\pi/2$ when the arg maxes of $\mathrm{val}\,\mathbf x$ and $\mathrm{val}\,\mathbf y$ are disjoint.
2. Lemma 23: the turning angle $\angle\mathbf U(t)\mathbf V(t)\mathbf W(t)\to\pi/2$ when $\max\mathrm{val}\,\mathbf U<\max\mathrm{val}\,\mathbf V<\max\mathrm{val}\,\mathbf W$ and the arg maxes of $\mathrm{val}\,\mathbf V$ and $\mathrm{val}\,\mathbf W$ are disjoint.
3. Proposition 24: $\liminf_{t}\kappa(\mathcal C_t,[t^{\lambda_0},t^{\lambda_p}])\ge\sum_{k=1}^{p-1}\angle^*\mathcal C^{\mathrm{trop}}(\lambda_{k-1})\mathcal C^{\mathrm{trop}}(\lambda_k)\mathcal C^{\mathrm{trop}}(\lambda_{k+1})$, where $\angle^*$ is the weak tropical angle ($\pi/2$ under the conditions of Lemma 23, else $0$).
4. Table 1: the coordinates of the tropical central path of $\mathbf{LW}_r$ at $\lambda=(4k+2c)/2^j$.
5. Claims in the proof of Theorem 25 (p. 23): on $[0,2]$ the dual coordinates of $\mathcal C^{\mathrm{trop}}$ are at most $\max(0,\lambda-1)$. At $\lambda_k=4k/2^{r-1}$ the largest coordinate is $r-1+(2k+2)/2^{r-1}$, attained only by $w_{3(r-1)}$ or $w_{3(r-1)+1}$. Hence $\angle^*=\pi/2$ at each interior subdivision point.

Significance

The theorem shows that the total curvature of the central path is not bounded by any polynomial in the number of constraints: $\mathbf{LW}_r$ has $3r+1$ constraints and curvature at least about $2^{r-2}\pi/2$. This settles the conjecture of Deza, Terlaky and Zinchenko in the negative. It also shows that the averaged upper bounds of Dedieu–Malajovich–Shub and De Loera–Sturmfels–Vinzant cannot hold for every region. A companion mission of this series formalizes the paper's second main result, an exponential lower bound on the number of iterations of log-barrier path-following methods on the same family.

The result is proved on paper. As far as is known, it has not been formalized in any proof assistant, and Mathlib has no notion of the total curvature of a curve, of Puiseux-series evaluation and valuation, or of the tropical central path. Formalizing the theorem would give a machine-checked reference point for a much-cited negative result in interior point theory. The Lean definitions of total curvature and of the turning angle are general and reusable.

Difficulty

The total curvature is a supremum over inscribed polygons, and a lower bound needs explicit polygons whose angles can be estimated for every large $t$. The central path of $\mathbf{LW}^=_r(t)$ has no closed form, so its points cannot be written down at given parameters $\mu$. Numerical evidence at a fixed $t$ says nothing uniform in $r$. The natural first idea, to compute the path's angles directly from system (1) for a fixed instance, gives no handle on how the number of turns grows with $r$. What is needed is control of the path's geometry uniformly over the whole scale of $t$, with $2^{r-2}$ turns located at once, and the threshold $t_0$ is not explicit.

Formalization scope

Vectors in which angles are measured are EuclideanSpace ℝ (Fin d). The turning angle is InnerProductGeometry.angle (V - U) (W - V), not Mathlib's vertex angle ∠ U V W, which is $\pi$ minus it. A degenerate triple ($U=V$ or $V=W$) contributes angle $0$. Total curvature is an EReal-valued supremum over strictly increasing parameter sequences in the parameter set, and the goal uses the set $(0,\infty)$. The primal and primal-dual curves are the vectors $(x,w)\in\mathbb R^{5r-1}$ and $(x,w,s,y)\in\mathbb R^{2(5r-1)}$. System (1) is the published Vanderbei central-path system with objective $-c$. The goal quantifies over every curve solving (1) for all $\mu>0$. Existence and uniqueness of that curve is the referenced platform statement VanderbeiLP.CentralPath.central_path_exists_unique and is not posed again. Indices are the paper's, 1-based, mapped to Fin by subtracting one. Powers $2^{r-2}$ use integer exponents of the real number $2$.

A trivializing formalization is ruled out explicitly: the curvature is a supremum in EReal (a real sSup of an unbounded set would be $0$), the turning angle is not the vertex angle, and degenerate polygons cannot add spurious right angles.

Lemmas 22–24 are stated over a model of $\mathbb K$ by coefficient functions with the paper's support and absolute-convergence conditions. Equalities, products and order in $\mathbb K$ are expressed through evaluation at all sufficiently large $t$, which is how the paper characterizes them. Table 1 and the claims of the proof are stated for the explicit tropical central path of $\mathbf{LW}_r$ given by Propositions 20–21 (milestones of the companion mission), written as a definition here. One repair: the paper's "uniquely attained" claim fails at $r=2$, $k=0$, where $w_1=w_4=2$. It is stated with that case excluded, which the proof does not use.

Welcome contributions: a general theory of total curvature of curves (monotonicity under refinement, behaviour under limits), asymptotics of evaluated Puiseux series, and the comparison between the central path over $\mathbb K$ and its real specializations.

Selected references

• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-Barrier Interior Point Methods Are Not Strongly Polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; preprint v2 (cited throughout) arXiv:1708.01544, doi:10.1137/17M1142132.
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Long and winding central paths, preprint, 2014. arXiv:1405.4161
• J. A. De Loera, B. Sturmfels, C. Vinzant, The central curve in linear programming, Found. Comput. Math. 12(4), 2012. arXiv:1012.3978
• J.-P. Dedieu, G. Malajovich, M. Shub, On the curvature of the central path of linear programming theory, Found. Comput. Math. 5(2), 2005.
• J.-P. Dedieu, M. Shub, Newton flow and interior point methods in linear programming, Int. J. Bifurcation and Chaos 15(3), 2005.
• A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Springer, 2009.
• L. van den Dries, P. Speissegger, The real field with convergent generalized power series, Trans. Amer. Math. Soc. 350(11), 1998.

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

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