Optimization

Motivation

Minimizing a convex function $f:\mathbb R^n\to\mathbb R$ whose gradient is Lipschitz is the basic problem of first-order optimization, and it is the regime in which most large-scale methods of machine learning, signal processing and operations research are analysed. The natural method, gradient descent, reaches accuracy $\varepsilon$ after $O(1/\varepsilon)$ gradient evaluations. In 1983 Nesterov showed that a method using the same oracle, but combining the current and the previous iterate, reaches accuracy $\varepsilon$ after only $O(1/\sqrt\varepsilon)$ evaluations, and that no method using only gradient information can do better by more than a constant factor. This accelerated gradient descent and its proximal variants (FISTA) are now the default fast first-order methods for smooth and composite convex problems.

This mission formalizes the accelerated rate as presented in S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2), §3.7.2, Theorem 3.19, whose proof follows Beck and Teboulle (2009).

Timeline.

• 1983: Nesterov introduces the accelerated method with rate $O(1/t^2)$ for convex functions with Lipschitz gradient (Soviet Math. Dokl. 27).
• 1983: Nemirovski and Yudin's black-box lower bounds show that $\Omega(1/t^2)$ is the best possible rate for this class (Theorem 3.14 of the book gives $3\beta\|x_1-x^*\|^2/(32(t+1)^2)$).
• 2009: Beck and Teboulle's FISTA extends the method, with the same step sequence $\lambda_t$, to composite problems with a simple nonsmooth term (SIAM J. Imaging Sci. 2(1)).
• 2008: Tseng gives a unified treatment with simpler step sizes (manuscript).

Setting

Let $\mathbb R^n$ carry the Euclidean inner product $x^\top y$ and norm $\|\cdot\|$. A differentiable function $f:\mathbb R^n\to\mathbb R$ is β-smooth if its gradient is $\beta$-Lipschitz:

$$\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|\qquad(x,y\in\mathbb R^n).$$

Assume $f$ is convex and $\beta$-smooth with $\beta>0$, and let $x^*$ be a minimizer of $f$.

Define the step sequences $\lambda_0=0$,

$$\lambda_t=\frac{1+\sqrt{1+4\lambda_{t-1}^2}}{2}\quad(t\ge1),\qquad\gamma_t=\frac{1-\lambda_t}{\lambda_{t+1}}.$$

Then $\lambda_1=1$, $\lambda_t\ge1$ for $t\ge1$, and $\gamma_t\le0$. Nesterov's accelerated gradient descent for the smooth case starts from an arbitrary point $x_1=y_1$ and sets, for $t\ge1$,

$$y_{t+1}=x_t-\frac1\beta\nabla f(x_t),\qquad x_{t+1}=(1-\gamma_t)\,y_{t+1}+\gamma_t\,y_t.$$

The primary sequence $(y_t)$ consists of gradient steps of length $1/\beta$; the sequence $(x_t)$, at which the gradient is queried, moves past $y_{t+1}$ away from $y_t$ (since $\gamma_t\le0$). Write $\delta_t=f(y_t)-f(x^*)$ for the optimality gap.

Formalization targets

Goal: Theorem 3.19

For every run of the method and every $t\ge1$,

$$f(y_t)-f(x^*)\le\frac{2\beta\|x_1-x^*\|^2}{t^2}.$$

The constant $2$ and the exponent $2$ are those printed in the book.

Milestones

In the order of the book's proof (pp. 294–295):

1. Lemma 3.6, unconstrained (p. 270): $f(x-\tfrac1\beta\nabla f(x))-f(y)\le\nabla f(x)^\top(x-y)-\tfrac1{2\beta}\|\nabla f(x)\|^2$ for all $x,y$.
2. (3.23): $f(y_{s+1})-f(y_s)\le\beta(x_s-y_{s+1})^\top(x_s-y_s)-\tfrac\beta2\|x_s-y_{s+1}\|^2$.
3. (3.24): $f(y_{s+1})-f(x^*)\le\beta(x_s-y_{s+1})^\top(x_s-x^*)-\tfrac\beta2\|x_s-y_{s+1}\|^2$.
4. The λ identity: $\lambda_{s-1}^2=\lambda_s^2-\lambda_s$ for $s\ge1$.
5. (3.25): $\lambda_s^2\delta_{s+1}-\lambda_{s-1}^2\delta_s\le\tfrac\beta2\bigl(\|\lambda_sx_s-(\lambda_s-1)y_s-x^*\|^2-\|\lambda_sy_{s+1}-(\lambda_s-1)y_s-x^*\|^2\bigr)$.
6. (3.26): $\lambda_{s+1}x_{s+1}-(\lambda_{s+1}-1)y_{s+1}=\lambda_sy_{s+1}-(\lambda_s-1)y_s$.
7. Telescoped bound: $\delta_t\le\frac{\beta}{2\lambda_{t-1}^2}\|u_1\|^2$ for $t\ge2$, with $u_1=\lambda_1x_1-(\lambda_1-1)y_1-x^*$.
8. Growth of λ: $\lambda_{t-1}\ge t/2$ for $t\ge2$.

Significance

The result. Theorem 3.19 is the upper half of the statement that first-order methods on smooth convex functions have complexity $\Theta(\sqrt{\beta\|x_1-x^*\|^2/\varepsilon})$: together with the black-box lower bound of Theorem 3.14 it shows that the accelerated method is optimal up to a constant factor, while plain gradient descent (Theorem 3.3, rate $2\beta\|x_1-x^*\|^2/(t-1)$) is not. The same potential-function argument, with the gradient step replaced by a proximal step, yields the rate of FISTA for composite objectives, and the identity $\lambda_{s-1}^2=\lambda_s^2-\lambda_s$ is the algebraic core of most later analyses of accelerated and momentum methods.

Formalizing it. The theorem is classical and fully proved on paper. What this mission adds is a machine-checked proof of the $O(1/t^2)$ rate for the exact step sequence of the book, with every intermediate inequality of the proof stated separately so that each can be closed and reused. A Lean development of accelerated gradient descent with this rate is not, to our knowledge, in Mathlib.

Difficulty

The rate does not follow from monotone decrease of $f(y_t)$, which is the engine of the analysis of plain gradient descent: the accelerated iterates are not monotone, and no single-step inequality on $\delta_t$ alone gives $1/t^2$. The proof instead tracks a weighted potential $\lambda_{s-1}^2\delta_s+\frac\beta2\|u_s\|^2$ and needs three exact algebraic coincidences: the identity $\lambda_{s-1}^2=\lambda_s^2-\lambda_s$, the completion of a square $2a^\top b-\|a\|^2=\|b\|^2-\|b-a\|^2$, and the rewriting (3.26) of the update rule, which makes consecutive potentials match exactly. In Lean the work is in this bookkeeping (vector identities in an inner-product space, a real recursion with square roots, and a telescoping sum indexed from $1$), not in any deep analytic fact.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $x^\top y$ is ⟪x, y⟫_ℝ.
• The gradient is an explicit map $g$ with HasGradientAt f (g x) x for every $x$; β-smoothness is the Lipschitz bound on $g$ (not the quadratic upper bound (3.4), which is a consequence). Convexity is ConvexOn ℝ Set.univ f.
• $\lambda$ is a real sequence defined by recursion on $\mathbb N$ with $\lambda_0=0$; $\gamma_t=(1-\lambda_t)/\lambda_{t+1}$ never divides by zero because $\lambda_{t+1}\ge1$.
• A run is a predicate on two sequences $x,y:\mathbb N\to\mathbb R^n$, indexed from $1$ as in the book; index $0$ is unconstrained. Every theorem quantifies over all runs.
• Standing assumptions: $x^*$ is a minimizer of $f$ (book, p. 242); $\beta>0$ (implicit in the step $1/\beta$) is a stated hypothesis.
• The page prints the update as $x_{t+1}=(1-\gamma_s)y_{t+1}+\gamma_ty_t$; the formalization uses $\gamma_t$ in both places, as the proof's (3.26) requires. A run predicate with a fixed coefficient $\gamma_s$ would describe a different (non-accelerated) method and is ruled out.
• The goal is stated for all $t\ge1$, including $t=1$, which the printed proof does not cover but which follows from (3.4). The growth bound $\lambda_{t-1}\ge t/2$ is stated for $t\ge2$, since $\lambda_0=0$. The telescoping display prints $\delta_s^2$ for $\delta_s$; the formalization uses $\delta_s$.

Contributions of every kind are welcome: proofs of the λ facts and of (3.26) are pure algebra; (3.23)–(3.25) need the descent lemma for β-smooth functions and first-order convexity, both of which are reusable well beyond this mission.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27:372–376, 1983. mathnet
• A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sciences 2(1):183–202, 2009. doi:10.1137/080716542
• P. Tseng, On accelerated proximal gradient methods for convex-concave optimization, manuscript, 2008. pdf
• A. Nemirovski, D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

Motivation

A probability model $\mu$ for a random element $X$ is rarely known exactly. Distributionally robust performance analysis replaces the single expectation $E_\mu[f(X)]$ by its worst case over all models within a prescribed distance of $\mu$. When the distance is an optimal-transport cost, the neighbourhood contains models whose support differs from that of $\mu$. That matters in stochastic-process applications such as ruin probabilities for insurance reserves, where the natural alternatives (a compensated Poisson process against a Brownian motion) are mutually singular and likelihood-based divergences such as Kullback–Leibler are infinite.

Blanchet and Murthy (arXiv:1604.01446, Math. Oper. Res. 2019) prove that the worst-case expectation over an optimal-transport ball equals a one-dimensional dual problem. They assume only that the underlying space is Polish, the cost lower semicontinuous and the performance function upper semicontinuous and integrable.

Timeline. Esfahani and Kuhn (arXiv:1505.05116, 2015/2018) obtained a dual reformulation for Wasserstein balls around empirical measures on $\mathbb R^d$. Gao and Kleywegt (arXiv:1604.02199, 2016) proved a general duality whose proof, as Blanchet and Murthy note, uses the local compactness of the space. Blanchet and Murthy (2016, v2 2017) removed local compactness and continuity of the cost. This covers path spaces such as $C[0,T]$ and $D[0,T]$.

Setting

Let $S$ be a Polish space with Borel σ-algebra $\mathcal B(S)$, and let $\mu$ be a probability measure on $S$ (the baseline model).

• Cost (A1). $c : S\times S\to[0,\infty)$ is lower semicontinuous, and $c(x,y)=0$ if and only if $x=y$.
• Performance function (A2). $f : S\to\mathbb R$ is upper semicontinuous and $\mu$-integrable.
• Budget. $\delta>0$.

The primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S\times S$ whose first marginal is $\mu$ and whose transport cost satisfies $\int c\,d\pi\le\delta$. The second marginal of $\pi$ is the alternative model. The primal objective is $I(\pi)=\int f(y)\,d\pi(x,y)$, and the primal value is

$$I=\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}.$$

The universal σ-algebra $\mathcal U(S)$ is the intersection of the completions of $\mathcal B(S)$ under all probability measures. Write $m\mathcal U(S;\bar{\mathbb R})$ for the $\mathcal U(S)$-measurable functions $S\to[-\infty,\infty]$. The dual feasible set $\Lambda_{c,f}$ consists of the pairs $(\lambda,\varphi)$ with $\lambda\ge0$, $\varphi\in m\mathcal U(S;\bar{\mathbb R})$ and $\varphi(x)+\lambda c(x,y)\ge f(y)$ for all $x,y$. The dual objective is $J(\lambda,\varphi)=\lambda\delta+\int\varphi\,d\mu$, and the dual value is $J=\inf\{J(\lambda,\varphi):(\lambda,\varphi)\in\Lambda_{c,f}\}$. Finally,

$$\varphi_\lambda(x)=\sup_{y\in S}\{f(y)-\lambda c(x,y)\}\in\mathbb R\cup\{\infty\}.$$

Formalization targets

Goal: Theorem 1

Under (A1) and (A2):

1. strong duality,

$$\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}=\inf\{J(\lambda,\varphi):(\lambda,\varphi)\in\Lambda_{c,f}\};$$

2. there is $\lambda^*\ge0$ such that $(\lambda^*,\varphi_{\lambda^*})$ is a dual optimizer;
3. a feasible $\pi^*$ and a feasible $(\lambda^*,\varphi_{\lambda^*})$ with finite $J(\lambda^*,\varphi_{\lambda^*})$ are optimal with $I(\pi^*)=J(\lambda^*,\varphi_{\lambda^*})$ if and only if the complementary slackness conditions hold:

$$f(y)-\lambda^*c(x,y)=\varphi_{\lambda^*}(x)\ \ \pi^*\text{-a.s.},\qquad \lambda^*\Big(\int c\,d\pi^*-\delta\Big)=0.$$

The "if" direction is stated without the finiteness assumption.

Milestones

Weak duality $I\le J$ (5). Lemma 15. Strong duality with a primal optimizer on compact $S$, first for continuous costs (Proposition 5), then for lower semicontinuous ones (Proposition 6). Universal measurability of $\varphi_\lambda$ (§4.2). Lemma 16. The restricted dual bound of Proposition 7. Lemma 8. The univariate formula (9):

$$I=\inf_{\lambda\ge0}\Big\{\lambda\delta+E_\mu\Big[\sup_{y\in S}\{f(y)-\lambda c(X,y)\}\Big]\Big\}.$$

Significance

The result. Formula (9) turns an infinite-dimensional optimization over probability measures into a one-dimensional convex minimization that involves only the baseline $\mu$. A modeller can therefore evaluate it by sampling from $\mu$. Theorem 1 is the input for the worst-case probability formula for closed sets (Theorem 3 of the paper) and for the existence of worst-case transport plans (Corollary 1). Its complementary slackness conditions describe the structure of every worst-case plan: mass is moved from $x$ to maximizers of $f(z)-\lambda^*c(x,z)$, and the budget is exhausted whenever $\lambda^*>0$.

Formalizing it. The result is proved on paper. To our knowledge it has no machine-checked proof. The only related statement on Prove2Me is a special case (empirical baseline, bounded continuous loss, power-of-norm cost on $\mathbb R^m$). A complete development would contain duality on compact spaces via Fenchel duality, the extension to σ-compact supports, and measurable-selection arguments for universally measurable functions. The measurable-selection part reuses Bertsekas–Shreve's analytic-set theory, which is already posed on the platform.

Difficulty

The obvious route copies Kantorovich duality. That route fails here because the feasible set $\Phi_{\mu,\delta}$ fixes only one marginal, so it is not tight on a non-compact space. Prokhorov compactness is available only on compact pieces $S_n\times S_n$. The duality must then be transported to the whole space by a limiting argument that keeps control of the dual multipliers.

A second obstacle is measurability. For a merely lower semicontinuous cost on a non-locally-compact space, $\varphi_\lambda$ need not be Borel measurable, so the dual must range over universally measurable functions. Removing the restriction $y\in S_\pi$ from the envelope (Lemma 8) needs a measurable selection theorem. Arguments that assume closed balls are compact do not apply in the target spaces $C[0,T]$ and $D[0,T]$.

Formalization scope

• Space and costs. S carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]. The cost is a real-valued curried function c : S → S → ℝ; (A1) is the structure AssumptionA1; (A2) is UpperSemicontinuous f together with Integrable f μ; and 0 < δ is assumed throughout.
• Extended reals. $I$, $J$, $I(\pi)$, $J(\lambda,\varphi)$ and $\varphi_\lambda$ live in EReal. The integral of an extended-real function is $\int\varphi^+-\int\varphi^-$ with lower Lebesgue integrals, and $\infty-\infty$ evaluates to $-\infty$. A coupling with $\int f^-\,d\pi=\infty$ therefore never raises $I$, which is the paper's reading in footnote 2.
• Measurability and integrals. Universal measurability is the published BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. For such $\varphi$ the lower integral equals the integral against the completion of $\mu$.
• Variants. The dual feasible set takes a set $K$: with $K=S$ it is (6b), and with $K=S_\pi$ it is (29).
• Hidden hypothesis. The "only if" part of Theorem 1(b) carries the hypothesis $J(\lambda^*,\varphi_{\lambda^*})<\infty$. Without it the equivalence fails when $I=J=\infty$.
• Ruled-out trivializations. A primal that fixes both marginals (or neither), a dual over Borel-measurable $\varphi$, and a Bochner integral for $\int f\,d\pi$ (which is $0$ off $L^1(\pi)$) all describe different problems and are ruled out by the definitions.
• Infrastructure and contributions. Needed: Fenchel duality on $C_b(S\times S)$ and its dual $M(S\times S)$ (Riesz–Markov–Kakutani), Prokhorov's theorem, Sion's minimax theorem, and Jankov–von Neumann selection. Several are on the platform or in Mathlib, and all are reusable beyond this mission. Proofs of the milestones in any order, and of the posed Bertsekas–Shreve tools, are welcome.

Selected references

• J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2):565–600, 2019. arXiv:1604.01446v2, doi:10.1287/moor.2018.0936
• R. Gao and A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, 2016. arXiv:1604.02199
• P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171:115–166, 2018. arXiv:1505.05116
• D. Bertsekas and S. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978, Chapter 7. MIT open copy
• C. Villani, Optimal Transport: Old and New, Springer, 2008. doi:10.1007/978-3-540-71050-9

Motivation

Airlines sell the seats of one flight leg at several prices. Cheaper fare classes tend to book earlier, so the seller must decide, as low-fare requests arrive, how many seats to hold back for later and more valuable passengers. The standard control is nested protection levels: a number $p_k$ of seats is reserved for the $k$ most expensive classes together, and a request of class $k+1$ is accepted only while more than $p_k$ seats remain. Littlewood (1972) gave the optimal rule for two classes; Belobaba's EMSR heuristic (1987, 1989) extended it to many classes without an optimality guarantee.

S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes (Operations Research 41(1), 1993) treat any number of classes with independent random demands and characterize optimal protection levels by first-order conditions on the expected revenue: Theorem 1 states that a policy with $f_{k+1}$ in the subdifferential of the expected revenue of the $k$ highest classes at $p_k$, for every $k$, is optimal. Their Theorem 2 addresses the question practitioners face first: seats and bookings are whole numbers. If demand is integer valued, is an optimal policy available among integer protection levels? The theorem answers yes. This mission formalizes that theorem and the chain of results in its proof.

Timeline.

• Littlewood (1972): two fare classes, rule $f_2 = f_1 \Pr[X_1 > p_1]$.
• Belobaba (1987, 1989): EMSR heuristic for many classes.
• Curry (1990) and Wollmer (1992): multiple nested classes, continuous and discrete demand respectively.
• Brumelle and McGill (1993): subdifferential optimality conditions for any number of classes (Theorem 1), existence of an optimal integer policy for integer demand (Theorem 2), and the probability conditions (31) (Theorem 3).

Setting

Classes are numbered $k = 1, 2, \dots$, class $1$ paying the highest fare. Class $k$ has a random demand $X_k \ge 0$ and fare $f_k$, with $f_1 > f_2 > \cdots$. The demands are mutually independent on a probability space $(\Omega, \mathcal F, P)$. A protection-level policy is a sequence $p = (p_1, p_2, \dots)$ with $p_k \ge 0$; the dummy level $p_0 = 0$ is never used.

For a demand vector $x$ and $s$ available seats, the revenue of the $k$ highest classes is defined recursively (Eqs. (8)–(9), p. 130):

$$R_1[s; p; x] = \begin{cases} f_1 s & 0 \le s < x_1,\\ f_1 x_1 & x_1 \le s,\end{cases}$$ $$R_{k+1}[s; p; x] = \begin{cases} R_k[s; p; x] & 0 \le s < p_k,\\ (s - p_k) f_{k+1} + R_k[p_k; p; x] & p_k \le s < p_k + x_{k+1},\\ x_{k+1} f_{k+1} + R_k[s - x_{k+1}; p; x] & p_k + x_{k+1} \le s.\end{cases}$$

The expected revenue is $ER_k[s; p; X] = E\,R_k[s; p; X]$. A policy is optimal if it maximizes $ER_k[s; \cdot\,; X]$ for every $k$ and every $s \ge 0$ (p. 130).

For a function $g$ and $t \ge 0$, $\delta_+ g(t)$ and $\delta_- g(t)$ are the right and left derivatives, with $\delta_- g(0) = +\infty$, and the subdifferential is $\delta g(t) = [\delta_+ g(t), \delta_- g(t)]$ (p. 131). Condition (20) is

$$f_{k+1} \in \delta ER_k[p_k; (p_0, \dots, p_{k-1}); X], \qquad k = 1, 2, \dots$$

A function is CLBI (Concave and Linear Between Integers, p. 132) if it is concave on $s \ge 0$ and linear on each interval $[m, m+1]$, $m = 0, 1, 2, \dots$

Formalization targets

Goal: Theorem 2 (p. 132)

If every $X_k$ is integer valued and the fares are positive, there is a policy $p^*$ with $p^*_k \in \{0, 1, 2, \dots\}$ such that

$$ER_k[s; q; X] \le ER_k[s; p^*; X] \qquad \text{for every policy } q,\ k \ge 1,\ s \ge 0,$$

and $p^*$ satisfies (20). The competitor $q$ ranges over all real protection levels.

Milestones (in proof order)

1. (27): $\delta ER_1[s; p; X] = [f_1 \Pr[X_1 > s], f_1 \Pr[X_1 \ge s]]$, and $ER_1$ is CLBI.
2. Covering property (p. 132): if $g$ is CLBI and $\delta_+ g(s_2) < c < \delta_- g(s_1)$ with $s_1 < s_2$, then $c \in \delta g(n)$ for an integer $n \in [s_1, s_2]$.
3. (28)–(29): for $s \ge p_k$,

$$\delta_+ ER_{k+1}[s] = f_{k+1}\Pr[X_{k+1} > s - p_k] + \sum_{i=0}^{\lfloor s - p_k\rfloor} \delta_+ ER_k[s - i]\Pr[X_{k+1} = i],$$

and the analogous formula for $\delta_-$ at $s > p_k$. 4. Corollary 1 (p. 131): concavity of $ER_k$ and $f_{k+1} \in \delta ER_k[p_k]$ give concavity of $ER_{k+1}$. 5. CLBI propagation (p. 133): if $ER_k[\cdot; p^*; X]$ is CLBI and integer $p^*_1, \dots, p^*_k$ satisfy (20), then $ER_{k+1}[\cdot; p^*; X]$ is CLBI. 6. (30): for $s$ large enough, $\delta_+ ER_{k+1}[s; p; X] < f_{k+2}$. 7. Theorem 1 (p. 131): a policy satisfying (20) is optimal.

Significance

The result. Theorem 2 justifies computing protection levels in whole seats: with integer demand, restricting to integer policies loses nothing against arbitrary real protection levels. The construction also shows that (20) is solvable at every level, so the sufficient condition of Theorem 1 is never empty for integer demand. Many later revenue-management models assume an optimal nested policy exists and rely on this result or its dynamic-programming analogues.

Formalizing it. The theorem is proved on the page by an induction on the class index, but several steps are compressed: (28)–(29) are printed without the range of $s$ on which they hold, and (30) is asserted "by recursive application". To our knowledge none of these statements has a machine-checked proof. A formal development gives a verified account of one-sided derivatives of expectations of piecewise-linear random functions and of the integer covering property. These pieces are reusable for other newsvendor-type and nested-inventory models. The probability-condition characterization (Theorem 3) is the subject of a companion mission in the same series.

Difficulty

Concavity of the expected revenue does not hold for arbitrary policies. It is only guaranteed level by level, when the protection level already chosen at level $k$ satisfies (20). Existence of an integer optimum therefore cannot be obtained by rounding a real optimum: the integer levels must be chosen one at a time, and each choice must preserve both concavity and the CLBI shape needed for the next. A second obstacle is analytic. The one-sided derivatives of $ER_{k+1}$ are expectations of derivatives of a random piecewise-linear function. Exchanging differentiation and expectation, and computing the sums in (28)–(29) exactly at integer and non-integer $s$, is where informal arguments and formal ones diverge. Finally there are infinitely many classes, so the policy $p^*$ is an infinite sequence built by recursion.

Formalization scope

• Model. Classes are indexed by $\mathbb N$ from $1$; fares, demands and protection levels are sequences $\mathbb N \to \mathbb R$. Seats, demands and protection levels are real; an integer policy is a sequence of natural numbers read as reals. Integer-valued demand means each $X_k(\omega)$ is a natural number. Expectations are Bochner integrals.
• Standing assumptions (§1). $P$ is a probability measure. The demands are measurable, nonnegative and mutually independent, and the fares are strictly decreasing.
• Added hypotheses. The goal assumes positive fares, $f_k > 0$ for $k \ge 1$. The page leaves this implicit (fares are average revenues), and without it the theorem is false. The same assumption appears in (30), and (27) assumes $f_1 \ge 0$, without which $ER_1$ is convex rather than concave.
• Derivatives. One-sided derivatives are required to exist, with their value asserted; no default value of an undefined derivative is used. The convention $\delta_- g(0) = +\infty$ is built into the subdifferential.
• Optimality. Optimality is global: against every real protection-level policy, at every level $k \ge 1$ and every $s \ge 0$.
• Paper's slips corrected. (28)–(29) are stated on their range $s \ge p_k$ (resp. $s > p_k$). (30) is stated for every $k \ge 1$, as the induction uses it, rather than the printed $k = 2, 3, \dots$
• Not a trivialization. The goal assumes only the model, integer demand and positive fares. It does not assume concavity, CLBI, (20) or any derivative formula, and optimality is not restricted to integer competitors or to one $k$.
• Duplication. Corollary 1 and Theorem 1 are restated from the companion mission in this series.
• Contributions. Proofs of the measure-theoretic derivative lemmas, of the covering property (a statement about real functions), and of the induction are all welcome.

Selected references

• S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes, Operations Research 41(1):127–137, 1993. https://doi.org/10.1287/opre.41.1.127
• K. Littlewood, Forecasting and Control of Passenger Bookings, AGIFORS Symposium Proceedings 12:95–117, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 2005. https://doi.org/10.1057/palgrave.rpm.5170134
• P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT, 1987. http://hdl.handle.net/1721.1/68077
• P. P. Belobaba, Application of a Probabilistic Decision Model to Airline Seat Inventory Control, Operations Research 37(2):183–197, 1989. https://doi.org/10.1287/opre.37.2.183
• R. E. Curry, Optimal Airline Seat Allocation with Fare Classes Nested by Origins and Destinations, Transportation Science 24(3):193–203, 1990. https://doi.org/10.1287/trsc.24.3.193
• R. D. Wollmer, An Airline Seat Management Model for a Single Leg Route When Lower Fare Classes Book First, Operations Research 40(1):26–37, 1992. https://doi.org/10.1287/opre.40.1.26

Related work on the platform. The two-class, integer-capacity EMSR rule of Belobaba (1987) is formalized as SeatInventory.Nested.emsr_protection_level_optimal. It is a relative of the $k = 1$ case of Theorem 2, but it lives in a different model: two classes, a fixed integer capacity, and only integer competitors.

Why this problem arose

Dynamic programming often replaces a search over whole plans with an equation for a value function. That replacement is useful only when solving the equation recovers the value actually available through policies. In his 1967 paper, Eric Denardo isolated conditions on an abstract return function that make this identification possible, without committing to a particular transition law or a finite state space. The framework covers discounted decision models and other examples discussed in the paper, while allowing different decisions at different states. Denardo, 1967.

The mission concerns the paper's first regime: a one-step contraction together with monotonicity. It focuses on the question raised just after equation (4): does the solution of the functional equation equal the supremum of the return functions generated by policies? The paper proves that it does under these assumptions. Its later $N$-stage regime is a separate mission. Denardo, 1967, pp. 167–169.

States, decisions, and returns

Let $\Omega$ be a set of states. At each $x\in\Omega$ there is a decision set $D_x$. A policy $\delta$ selects a decision $\delta_x\in D_x$ at every state, so the policy space $\Delta$ is the full Cartesian product $\prod_{x\in\Omega}D_x$. Let $V$ be the bounded real functions on $\Omega$, with the uniform metric $\rho(u,v)=\sup_{x\in\Omega}|u(x)-v(x)|$. A return function $h(x,d,v)$ assigns a real return to a state, an available decision, and a continuation value $v\in V$. Denardo, 1967, p. 166.

For a policy $\delta$, its policy operator $H_\delta$ acts by $(H_\delta v)(x)=h(x,\delta_x,v)$. Under the contraction assumption, some $c$ satisfies $0\le c<1$ and $|h(x,d,u)-h(x,d,v)|\le c\rho(u,v)$ for all eligible $x,d,u,v$. Each $H_\delta$ then has a unique fixed point $v_\delta\in V$, called that policy's return function. The optimal return function is defined pointwise by $f(x)=\sup_{\delta\in\Delta}v_\delta(x)$. These are the paper's definitions, rather than a presumed equality between $f$ and a Bellman fixed point. Denardo, 1967, pp. 166–167.

The maximization operator $A$ instead chooses the best decision at each state for a supplied continuation value: $(Av)(x)=\sup_{d\in D_x}h(x,d,v)$. Denardo assumes that $H_\delta v$ and $Av$ remain bounded, so both operators act on $V$. The monotonicity assumption says that $u\ge v$ pointwise implies $H_\delta u\ge H_\delta v$ for every policy. These are separate conditions: contraction controls distance between value functions, while monotonicity controls their order. Denardo, 1967, pp. 166–168.

Formalization targets

The central target is Theorem 3. Under contraction and monotonicity, the unique bounded solution $v^*$ of equation (4) is the optimal return:

$$Av^*=v^*,\qquad v^*(x)=f(x)=\sup_{\delta\in\Delta}v_\delta(x)\quad(x\in\Omega).$$

The milestones follow the paper's route to that assertion. Theorem 1 bounds a policy's return by its fixed-point residual, $\rho(v_\delta,w)\le\rho(H_\delta w,w)/(1-c)$. Theorem 2 says that $A$ itself has modulus at most $c$. The text accompanying equation (4) establishes that $A$ has exactly one fixed point. Corollary 1 then gives, for each $\varepsilon>0$, a policy with residual at most $\varepsilon(1-c)$ at that fixed point and return within $\varepsilon$ of it, together with an exact equality criterion for zero residual. Denardo, 1967, pp. 167–168.

What the result gives

Theorem 3 justifies reading the functional equation as an optimization equation: its solution is the pointwise supremum of returns realized by the paper's policy model. Corollary 1 supplies policy returns arbitrarily close to that solution in the uniform metric. With the compactness and continuity assumptions of Corollary 2, the paper also obtains a policy that attains it, though that optional result is outside this mission's milestone list. Denardo, 1967, pp. 167–168.

The mathematical result was proved in the cited paper. This mission asks for machine-checked proofs of its abstract statements in Lean, including the residual estimate, the maximization operator's contraction, fixed-point existence, and the identification with optimal policy return. The definitions are reusable for decision models whose returns fit Denardo's assumptions; they do not prescribe a probability kernel or a finite action set.

Where the difficulty lies

The fixed-point theorem alone identifies a unique solution of $Av=v$; it does not identify that solution with $f$, because $f$ is defined through the separate fixed points of all $H_\delta$. The distinction matters: the paper observes that contraction without monotonicity can leave $v^*$ different from $f$, and gives $h(x,d,v)=-v(x)/2$ as a nonmonotone example. The formal goal therefore retains both definitions and requires monotonicity. Denardo, 1967, pp. 167–168.

There is also a choice issue in Corollary 1. A near-maximizing decision is available separately at every state, while its conclusion asks for one policy choosing all those decisions at once. The full Cartesian policy space is essential to the statement. On an infinite state set, the value functions must remain bounded even after applying $A$ or a policy operator; contraction of differences by itself does not provide that range condition. Denardo, 1967, pp. 166–168.

Formalization scope

Lean represents $V$ by bounded real functions lp (fun _ : Ω => ℝ) ⊤; its metric is $\rho$. The state type may be infinite or empty, and decision sets depend on the state. Policies are precisely dependent functions $\delta:(x:\Omega)\to D_x$. The operators $H_\delta$ and $A$ are maps into $V$ supplied with equations fixing their values from $h$. This expresses the bounded-range assumptions on pages 166–167. Pointwise order is explicit because the bounded-function type has no order instance. Denardo, 1967, pp. 166–168.

Every supremum in the mission is a genuine real least upper bound. IsMaxOperator requires it for the decision returns at each state; IsOptimalReturn requires it for the policy returns. These predicates avoid assigning a default value to an empty or unbounded supremum. Where states exist, IsMaxOperator also entails a nonempty decision set. The family $v_\delta$ is supplied with $H_\delta v_\delta=v_\delta$; contraction ensures each such return exists uniquely. Equation (4) and the main goal explicitly assert existence of the fixed point of $A$, so the goal cannot hold merely because there is no solution to identify. Defining $f$ from the fixed point of $A$, or defining $v^*$ from the policy supremum, would erase the paper's substantive claim and is excluded.

The definition layer needs bounded functions, uniform distance, real least upper bounds, and dependent policies. The theorem layer needs fixed-point and order reasoning on these objects. Contributions toward those general operator facts and the paper's four milestone statements are within scope.

Selected references

• Eric V. Denardo, Contraction Mappings in the Theory Underlying Dynamic Programming, SIAM Review 9(2), 165–177, 1967. DOI: 10.1137/1009030.

Motivation

Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They are among the most widely used methods in reinforcement learning, from REINFORCE (Williams 1992) and the policy gradient theorem to natural policy gradient and trust-region methods. The objective is not concave in the policy, even when the policy is a raw table of action probabilities, so standard optimization theory guarantees at best convergence to a stationary point, and it was long unclear whether or how fast these methods find an optimal policy.

Agarwal, Kakade, Lee and Mahajan (JMLR 2021) give a systematic answer for the tabular and function-approximation settings. This mission formalizes their warm-up result, Theorem 4.1: projected gradient ascent over the simplex of stochastic policies reaches an $\epsilon$-optimal policy after a number of iterations polynomial in the sizes of the MDP, the effective horizon $1/(1-\gamma)$, $1/\epsilon$, and a distribution mismatch coefficient. The gradient domination idea it rests on goes back to the analysis of conservative policy iteration by Kakade and Langford (2002) and to Scherrer and Geist (2014).

Setting

A finite discounted MDP consists of finite sets $\mathcal S$ of states and $\mathcal A$ of actions, a transition kernel $P(s'\mid s,a)$, rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in[0,1)$. A policy $\pi$ assigns to each state a probability distribution $\pi(\cdot\mid s)$ over actions. Its value from a start state $s_0$ is

$$V^\pi(s_0)=\mathbb E\Big[\sum_{t=0}^\infty\gamma^t r(s_t,a_t)\,\Big|\,s_0\Big],\qquad a_t\sim\pi(\cdot\mid s_t),\ s_{t+1}\sim P(\cdot\mid s_t,a_t),$$

and for a start distribution $\rho$, $V^\pi(\rho)=\sum_s\rho(s)V^\pi(s)$. The action value is $Q^\pi(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ and the advantage is $A^\pi(s,a)=Q^\pi(s,a)-V^\pi(s)$. The discounted state visitation distribution is $d^\pi_\rho(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr^\pi(s_t=s\mid s_0\sim\rho)$. An optimal policy $\pi^\star$ maximizes $V^\pi(s)$ at every state simultaneously; $V^\star=V^{\pi^\star}$.

In the direct parameterization the parameter is the table itself, $\pi_{s,a}=\pi(a\mid s)$, a point of the product simplex $\Delta(\mathcal A)^{|\mathcal S|}\subseteq\mathbb R^{\mathcal S\times\mathcal A}$. The algorithm optimizes $V^\pi(\mu)$ for a chosen start distribution $\mu$ by projected gradient ascent

$$\pi^{(t+1)}=P_{\Delta(\mathcal A)^{|\mathcal S|}}\big(\pi^{(t)}+\eta\nabla_\pi V^{(t)}(\mu)\big),$$

where $P_{\Delta(\mathcal A)^{|\mathcal S|}}$ is the Euclidean projection and $V^{(t)}=V^{\pi^{(t)}}$. Performance is measured under a possibly different distribution $\rho$, and the distribution mismatch coefficient $\|d^{\pi^\star}_\rho/\mu\|_\infty$ (componentwise ratio) measures how well $\mu$ covers the states an optimal policy visits from $\rho$.

Formalization targets

Goal: Theorem 4.1

With step size $\eta=(1-\gamma)^3/(2\gamma|\mathcal A|)$, from any initial policy, for every $\rho\in\Delta(\mathcal S)$ and $\epsilon>0$,

$$\min_{t\le T}\big\{V^\star(\rho)-V^{(t)}(\rho)\big\}\le\epsilon\qquad\text{whenever}\qquad T>\frac{64\gamma|\mathcal S||\mathcal A|}{(1-\gamma)^6\epsilon^2}\Big\|\frac{d^{\pi^\star}_\rho}{\mu}\Big\|_\infty^2 .$$

Milestones, in the order of the proof

1. Lemma 3.2 (performance difference): $V^\pi(s_0)-V^{\pi'}(s_0)=\frac1{1-\gamma}\mathbb E_{s\sim d^\pi_{s_0}}\mathbb E_{a\sim\pi(\cdot\mid s)}[A^{\pi'}(s,a)]$.
2. (7), the gradient of the direct parameterization: $\partial V^\pi(\mu)/\partial\pi(a\mid s)=\frac1{1-\gamma}d^\pi_\mu(s)Q^\pi(s,a)$.
3. Lemma 4.1 (gradient domination): $V^\star(\rho)-V^\pi(\rho)\le\frac1{1-\gamma}\|d^{\pi^\star}_\rho/\mu\|_\infty\max_{\bar\pi}(\bar\pi-\pi)^\top\nabla_\pi V^\pi(\mu)$, together with the sharper form with $d^\pi_\mu$ in place of $(1-\gamma)\mu$.
4. Lemma D.3 (smoothness): $\|\nabla_\pi V^\pi(s_0)-\nabla_\pi V^{\pi'}(s_0)\|_2\le\frac{2\gamma|\mathcal A|}{(1-\gamma)^3}\|\pi-\pi'\|_2$.
5. Theorem E.1(3) (Beck 2017, Theorem 10.15): projected gradient descent with step $1/\beta$ on a $\beta$-smooth function over a closed convex set has $\min_{t<T}\|G^\eta(x_t)\|\le\sqrt{2\beta(f(x_0)-f(x^*))}/\sqrt T$, with $G^\eta$ the gradient mapping.
6. Proposition B.1: a gradient mapping of norm at most $\epsilon$ at $\pi$ makes the next iterate $\pi^+$ $\epsilon(\eta\beta+1)$-stationary over feasible unit directions.

Significance

The theorem shows that, for the simplest constrained parameterization, a first-order method finds a globally optimal policy at a polynomial rate in spite of non-concavity. The guarantee holds for every performance distribution $\rho$ at once, and it isolates the role of exploration in a single quantity, the mismatch coefficient; Section 4.3 of the paper shows that without a well-covering $\mu$ gradient methods can need exponentially many steps. Lemma 4.1 and the smoothness bound are reused across the rest of the paper, and the performance difference lemma underlies essentially all of its analyses.

All results here are proved in the paper, with Theorem E.1 and Theorem E.2 cited from Beck (2017) and Ghadimi–Lan (2016). None of them has a machine-checked proof on the platform. A formal development provides a verified link between the policy gradient expression of the direct parameterization and a standard nonconvex projected-gradient rate, and a reusable formal library of discounted visitation distributions, the performance difference identity, and projected gradient methods on Euclidean spaces.

Difficulty

The obvious argument, "projected gradient ascent converges to a stationary point, and stationary points are optimal", fails on both counts as stated. Stationary points of $V^\pi(\mu)$ need not be optimal when $\mu$ does not cover the relevant states; the quantitative replacement is gradient domination, which only controls suboptimality through the mismatch coefficient. The convergence rate itself requires smoothness of the value as a function of the policy table, which is a bound on second derivatives of a matrix inverse $(I-\gamma P_\pi)^{-1}$ with the dependence $(1-\gamma)^{-3}$ and the factor $|\mathcal A|$ made explicit. Finally, the near-stationarity delivered by the gradient-mapping rate is at the next iterate, not the current one, which is why the conclusion is over $t\in\{0,\dots,T\}$. On the Lean side, the value is an infinite series in the policy entries, so its differentiability and the exact gradient formula have to be established for a function defined on the whole parameter space.

Formalization scope

Policies are parameter vectors in EuclideanSpace ℝ (S × A), so norms are $\ell_2$ and Mathlib's gradient is $\nabla_\pi$; the objective $\pi\mapsto V^\pi(\mu)$ is defined on the whole space and is only ever evaluated, with its gradient, at policies. The MDP layer (transition kernels, policies, $V^\pi$, $Q^\pi$, occupation distributions, optimal policies) is the published FoundationsML.ReinforcementLearning library; $V^\pi$ is the unnormalized discounted sum. The projection is any map satisfying the nearest-point property. The optimal policy is a hypothesis IsOptimalPolicy (optimal from every state), not a supremum over all functions.

Conventions committed to:

• The mismatch coefficient is any constant $D$ with $d^{\pi^\star}_\rho(s)\le D\mu(s)$ for all $s$; this avoids Lean's $x/0=0$ and is equivalent to the page's statement when the coefficient is finite.
• $\gamma>0$ and $\epsilon>0$ are explicit hypotheses of the goal (the step size divides by $\gamma$, the threshold by $\epsilon$).
• The goal concludes $\exists\,t\le T$. The printed $\min_{t<T}$ fails at $T=1$ (one state, two actions with rewards $1$ and $0$, $\gamma=0.001$, $\epsilon=1/2$, initial policy on the bad action); the proof on p. 50 establishes the range $0\le t\le T$.
• Proposition B.1 bounds the directions feasible at $\pi^+$, as its proof does; Theorem E.1 assumes smoothness on $C$ only and uses the radicand $2\beta(f(x_0)-f(x^*))$ of Beck and of p. 49.

A formalization that defines the update through formula (7), that assumes gradient domination or smoothness as hypotheses of the goal, or that takes the gradient off the simplex where the value series may diverge, would trivialize the goal; the goal mentions none of these, and (7) is a milestone theorem.

A complete development needs: summability and differentiability of the value series near the simplex; the performance difference lemma; the Euclidean projection inequality on a closed convex set; the descent lemma for functions smooth on a convex set; and the gradient-mapping argument. The projection and gradient-mapping results are independent of reinforcement learning and reusable. Contributions to any milestone are welcome, as are proofs of Theorem E.2 (Ghadimi–Lan) as a stepping stone to Proposition B.1.

Selected references

• A. Agarwal, S. M. Kakade, J. D. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22(98), 2021; arXiv:1908.00261v5. https://arxiv.org/abs/1908.00261
• A. Beck, First-Order Methods in Optimization, MOS-SIAM Series on Optimization, SIAM, 2017. https://doi.org/10.1137/1.9781611974997
• S. Ghadimi, G. Lan, Accelerated gradient methods for nonconvex nonlinear and stochastic programming, Mathematical Programming 156, 2016. https://doi.org/10.1007/s10107-015-0871-8
• S. Kakade, J. Langford, Approximately optimal approximate reinforcement learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• B. Scherrer, M. Geist, Local Policy Search in a Convex Space and Conservative Policy Iteration as Boosted Policy Search, ECML PKDD 2014, pp. 35–50 (arXiv version: https://arxiv.org/abs/1306.1520)
• R. J. Williams, Simple statistical gradient-following algorithms for connectionist reinforcement learning, Machine Learning 8, 1992. https://doi.org/10.1007/BF00992696

Motivation

Regularized least squares is the standard tool of high-dimensional linear regression. The square-root LASSO of Belloni, Chernozhukov and Wang (Biometrika, 2011) minimizes $\sqrt{\mathrm{MSE}_n(\beta)} + \lambda\|\beta\|_1$. Unlike the LASSO, its optimal regularization parameter does not depend on the unknown noise level. Regularization is usually justified through sparsity or bias–variance arguments. Blanchet, Kang and Murthy (arXiv:1610.05627, J. Appl. Probab. 56(3), 2019) give a different justification. The square-root LASSO, and every $\ell_p$-penalized square-root least-squares estimator, is exactly a distributionally robust estimator. It minimizes the worst-case expected square loss over all data distributions within a given optimal-transport distance of the empirical distribution.

The rest of the paper builds on this representation: the radius of the transport ball is the regularization parameter, which the paper's Robust Wasserstein Profile function selects by a statistical criterion (mission 3 of this series). The duality theorem underneath, Proposition 1, is due to Blanchet and Murthy (Math. Oper. Res., 2019). Closely related representations for logistic regression appear in Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NeurIPS 2015), where they are approximate. The cost function introduced in this paper makes them exact.

Setting

The training data are $n \ge 1$ pairs $(X_1, Y_1), \dots, (X_n, Y_n)$ with predictors $X_i \in \mathbb R^d$ and responses $Y_i \in \mathbb R$. No distributional assumption is made; the data are fixed vectors. The empirical distribution is $P_n = \frac1n \sum_{i=1}^n \delta_{(X_i, Y_i)}$. For $\beta \in \mathbb R^d$ the square loss is $l(x, y; \beta) = (y - \beta^T x)^2$ and the mean square error is $\mathrm{MSE}_n(\beta) = \frac1n\sum_{i=1}^n (Y_i - \beta^T X_i)^2$.

A cost function $c$ assigns to two points $z, w$ of $\mathbb R^d \times \mathbb R$ a value $c(z, w) \in [0, \infty]$, the cost of moving a unit of mass from $z$ to $w$. The optimal transport cost between probability measures $P$ and $Q$ is

$$D_c(P, Q) = \inf\Big\{ \mathbb E_\pi[c(U, W)] : \pi \text{ a probability measure on pairs } (U, W),\ \pi_U = P,\ \pi_W = Q \Big\}. \qquad (7)$$

The worst-case expected loss at radius $\delta \ge 0$ is $\sup_{P : D_c(P, P_n) \le \delta} \mathbb E_P[l(X, Y; \beta)]$, and the distributionally robust regression problem (8) minimizes it over $\beta$.

Two costs are used. With $q \in (1, \infty]$:

• the squared $\ell_q$ cost on $\mathbb R^{d+1}$, $c((x, y), (u, v)) = \|(x, y) - (u, v)\|_q^2$ (Proposition 2);
• the cost $N_q^2$, where (14) $N_q((x, y), (u, v)) = \|x - u\|_q$ if $y = v$ and $+\infty$ otherwise. Under this cost the responses cannot be moved, and only the predictors are perturbed (Theorem 1).

The exponent $p$ is the dual of $q$, $1/p + 1/q = 1$, and $\bar\beta = (-\beta, 1)$.

Formalization targets

Goal: Theorem 1 (p. 11)

For the cost $c = N_q^2$, every $\delta \ge 0$ and every $\beta \in \mathbb R^d$,

$$\sup_{P :\, D_c(P, P_n) \le \delta} \mathbb E_P\big[(Y - \beta^T X)^2\big] = \Big(\sqrt{\mathrm{MSE}_n(\beta)} + \sqrt\delta\,\|\beta\|_p\Big)^2 ,$$

and consequently

$$\inf_{\beta \in \mathbb R^d} \sup_{P :\, D_c(P, P_n) \le \delta} \mathbb E_P\big[(Y - \beta^T X)^2\big] = \inf_{\beta \in \mathbb R^d} \Big(\sqrt{\mathrm{MSE}_n(\beta)} + \sqrt\delta\,\|\beta\|_p\Big)^2 .$$

The second identity is the printed theorem; the first is what its proof establishes for each $\beta$. The goal states both.

Milestones

1. Proposition 1 (p. 10): strong duality. For a lower semicontinuous cost vanishing on the diagonal, an upper semicontinuous loss and $\delta > 0$, the worst-case expected loss equals $\min_{\gamma \ge 0} \{\gamma\delta + \frac1n \sum_i \varphi_\gamma(X_i, Y_i)\}$, with $\varphi_\gamma(z) = \sup_u \{l(u) - \gamma c(u, z)\}$ (11).
2. (28) (pp. 28–29): the closed form of $\varphi_\gamma$ for the square loss and the squared $\ell_q$ cost.
3. (29) and the display after it (p. 29): $\inf_{\gamma > b^2} \{\gamma\delta + \frac{\gamma}{\gamma - b^2} M\} = (\sqrt M + b\sqrt\delta)^2$ for $M, b, \delta \ge 0$.
4. Proposition 2 (p. 10): the analogue of the goal for the squared $\ell_q$ cost, with $\|\bar\beta\|_p$ in place of $\|\beta\|_p$ (13).
5. Outline of the proof of Theorem 1, last display (p. 29): the closed form of $\varphi_\gamma$ for the cost $N_q^2$.

Significance

The result. Theorem 1 identifies $\ell_p$-penalized square-root least squares with a min–max problem over data distributions. For $q = \infty$, $p = 1$ the minimizers are those of the square-root LASSO with $\lambda = \sqrt\delta$. The regularization parameter therefore acquires a meaning: it is the square root of the transport budget an adversary may spend perturbing the predictors. This is the basis of the paper's choice of $\delta$ by the Robust Wasserstein Profile function (§4), and of the interpretation of regularized estimators as robust to covariate perturbations. Proposition 2 shows that letting the adversary also move the responses changes the penalty to $\|(-\beta, 1)\|_p$, which is why the label-preserving cost $N_q$ is needed for an exact match.

Formalizing it. All results are proved on paper; none is formalized. A complete development gives a machine-checked strong-duality theorem for optimal-transport balls with possibly infinite costs (Proposition 1), two explicit worst-case computations, and corrected boundary cases of the closed forms (28) and the outline display, which print $+\infty$ for all $\gamma \le \|\bar\beta\|_p^2$ although the value can be finite at equality. The corrections do not affect the theorems.

Difficulty

The obvious argument fails in two places. The first is the duality step: the supremum ranges over all Borel probability measures on $\mathbb R^{d+1}$ within transport cost $\delta$, an infinite-dimensional set that is not compact in any convenient topology, with a loss that is unbounded above. Exchanging the supremum with the Lagrange multiplier of the budget constraint is Proposition 1, a theorem in its own right (Blanchet–Murthy), and its attainment claim needs $\delta > 0$.

The second is the cost $N_q$, which is $+\infty$ off $\{y = v\}$, so the standard Wasserstein duality theorems, which assume a finite metric cost, do not apply. The degenerate cases $\beta = 0$, $\mathrm{MSE}_n(\beta) = 0$, $\delta = 0$, where the objective in $\gamma$ does not blow up at both ends, must be covered separately.

Formalization scope

• Spaces. A data point is a pair in (Fin d → ℝ) × ℝ with the product σ-algebra and topology. Proposition 2's cost uses the stacked vector in Fin (d+1) → ℝ (response last, built with Fin.snoc), and $\bar\beta$ is the stacked vector of $(-\beta, 1)$.
• Norms. $\|\cdot\|_q$ and $\|\cdot\|_p$ are the norms of PiLp, with exponents in ℝ≥0∞, so $q = \infty$ (the square-root LASSO case) is included. The exponents are linked by p.HolderConjugate q, and $q \in (1, \infty]$ throughout. Theorem 1 does not print a range for $q$; the range is taken from Proposition 2, which the paper calls essentially the same result.
• Transport cost and worst case. Costs are ℝ≥0∞-valued, and $D_c$ is an infimum over probability couplings with both marginals fixed. Expectations of the nonnegative losses are lower Lebesgue integrals, and the worst case is a supremum in ℝ≥0∞ over all probability measures in the ball. No integrability side condition removes measures from the ball. Identities with a real right-hand side are stated after embedding it with ENNReal.ofReal.
• The empirical distribution is the published definition WassersteinDRO.Regularization.empiricalDistribution, applied to $i \mapsto (X_i, Y_i)$, with $n > 0$.
• $\varphi_\gamma$. A point at infinite cost contributes $-\infty$ for every $\gamma \ge 0$, including $\gamma = 0$, as in the paper's treatment of $N_q$. With the convention $0 \cdot \infty = 0$ instead, Proposition 1's minimum would not be attained for the cost $N_q^2$ at $\beta = 0$.
• Proposition 1 is stated for a nonnegative loss and $\delta > 0$; both are restrictions of the page, recorded in the item.
• Corrections. (28) and the outline display are stated with their corrected boundary cases. The one-dimensional lemma behind (29) is stated as a greatest lower bound over $\gamma > b^2$, including $b = 0$, $M = 0$, $\delta = 0$.

A formalization in which the transport infimum did not fix both marginals, allowed sub-probability couplings, or used a Bochner integral would make the worst case trivially $+\infty$ or $0$. The conventions above rule this out: at $\delta = 0$ the ball is $\{P_n\}$ and both sides of the goal equal $\mathrm{MSE}_n(\beta)$.

The work needs Kantorovich-type duality for lower semicontinuous costs on $\mathbb R^m$ (absent from Mathlib), Hölder's inequality with its equality case for PiLp, and elementary one-variable optimization. The duality theorem and the transport-cost definition are reusable beyond this mission: mission 2 of this series (classification) uses Proposition 1 with the cost $N_q$, $\rho = 1$. Contributions that prove Proposition 1, or its weak-duality half, are particularly welcome.

Selected references

• J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, J. Appl. Probab. 56(3), 2019; arXiv:1610.05627v4. https://arxiv.org/abs/1610.05627
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Math. Oper. Res. 44(2), 2019. https://doi.org/10.1287/moor.2018.0936
• A. Belloni, V. Chernozhukov, L. Wang, Square-root lasso: pivotal recovery of sparse signals via conic programming, Biometrika 98(4), 2011. https://doi.org/10.1093/biomet/asr043
• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally robust logistic regression, NeurIPS 2015. https://arxiv.org/abs/1509.09259
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9