Optimization

Motivation

Regularized logistic regression and the support vector machine (SVM) are two of the most widely used linear classifiers. Both are usually introduced as empirical risk minimization plus a norm penalty $\|\beta\|_p$ whose size is tuned by cross-validation, with the penalty justified heuristically as a guard against overfitting. Distributionally robust optimization (DRO) offers a different reading: instead of minimizing the average loss on the training sample, minimize the worst average loss over all distributions close to the empirical one. Blanchet, Kang and Murthy (arXiv:1610.05627v4; J. Appl. Probab. 56(3), 2019) show that, for a suitable notion of closeness based on optimal transport, the robust problem and the penalized problem coincide exactly. The penalty is then the price of robustness against perturbations of the predictors, and the regularization parameter becomes the radius of an uncertainty set, which the same paper later chooses by a statistical criterion (the robust Wasserstein profile).

Related earlier work: Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) studied Wasserstein-robust logistic regression with a metric that charges a finite price $\kappa$ for flipping a label, and obtained regularized logistic regression only in the limit $\kappa \to \infty$. The result formalized here is the exact statement at $\kappa = \infty$, together with the analogous statement for the hinge loss.

Setting

Training data are pairs $(X_1,Y_1),\dots,(X_n,Y_n)$ with predictors $X_i \in \mathbb R^d$ and labels $Y_i \in \{-1,+1\}$, $n \ge 1$. Their empirical distribution is $P_n = \frac1n\sum_{i=1}^n \delta_{(X_i,Y_i)}$, a probability measure on $Z = \mathbb R^d \times \mathbb R$.

For a cost $c : Z \times Z \to [0,\infty]$, the optimal transport cost between probability measures $P$ and $Q$ on $Z$ is

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

The cost used here is the label-preserving cost: for $q \in [1,\infty]$,

$$N_q\big((x,y),(u,v)\big) = \|x - u\|_q \text{ if } y = v, \qquad +\infty \text{ otherwise}.$$

Every distribution $P$ with $D_{N_q}(P,P_n) < \infty$ has the same label distribution as $P_n$; only the predictors are perturbed. The exponent $p$ is the conjugate of $q$, $1/p + 1/q = 1$.

The losses are the log-exponential loss $\log(1 + e^{-y\beta^T x})$ and the hinge loss $(1 - y\beta^T x)^+$, for a coefficient vector $\beta \in \mathbb R^d$. The worst-case expected loss at radius $\delta \ge 0$ is $\sup\{\mathbb E_P[l] : D_{N_q}(P,P_n) \le \delta\}$, the supremum over probability measures $P$ on $Z$.

Formalization targets

Goal: Theorem 2 (p. 11)

For every $\delta \ge 0$ and every $\beta \in \mathbb R^d$,

$$\sup_{P:\ D_{N_q}(P,P_n)\le\delta} \mathbb E_P\big[\log(1 + e^{-Y\beta^T X})\big] = \frac1n\sum_{i=1}^n \log(1 + e^{-Y_i\beta^T X_i}) + \delta\|\beta\|_p,$$ $$\sup_{P:\ D_{N_q}(P,P_n)\le\delta} \mathbb E_P\big[(1 - Y\beta^T X)^+\big] = \frac1n\sum_{i=1}^n (1 - Y_i\beta^T X_i)^+ + \delta\|\beta\|_p,$$

and consequently the two identities obtained by taking $\inf_{\beta}$ on both sides, which is how the paper prints the theorem.

Milestones

1. Proposition 1 (p. 10): strong duality, $\sup_{P: D_c(P,P_n)\le\delta}\mathbb E_P[l] = \min_{\gamma\ge0}\{\gamma\delta + \frac1n\sum_i\varphi_\gamma(X_i,Y_i)\}$ with $\varphi_\gamma(z_0) = \sup_z\{l(z) - \gamma c(z,z_0)\}$, for a lower semicontinuous cost vanishing on the diagonal, an upper semicontinuous loss and $\delta > 0$.
2. Logistic inner supremum (proof of Theorem 2, p. 30): $\sup_x\{\log(1+e^{-y_0\beta^T x}) - \lambda\|x - x_0\|_q\}$ equals the loss at $x_0$ if $\|\beta\|_p \le \lambda$ and $+\infty$ otherwise.
3. Logistic outer minimisation (p. 30): the infimum over $\lambda \ge 0$ of $\delta\lambda$ plus the average of these suprema equals the regularized empirical loss.
4. Hinge inner supremum (pp. 30–31) and 5. hinge outer minimisation (p. 31): the same two steps for the hinge loss.

Significance

The theorem identifies two standard estimators as exact solutions of a robust decision problem. Consequences: the penalty $\delta\|\beta\|_p$ has a quantitative meaning (the adversary's transport budget), the regularization parameter can be chosen by the paper's robust Wasserstein profile instead of cross-validation, and the norm of the penalty is tied to the geometry of the perturbations (perturbations measured in $\ell_\infty$ give an $\ell_1$ penalty). The same identity is the input of the paper's coverage bound (Proposition 6) for $\rho = 1$.

The result is proved on paper; no machine-checked version is known. The formalization adds a precise statement of the objects involved (couplings with both marginals fixed, an infinite cost across labels, expectations of nonnegative losses with values in $[0,\infty]$), a checked version of the duality step specialised to this cost, and the treatment of boundary cases ($\delta = 0$, $\beta = 0$, $q \in \{1,\infty\}$) that the paper does not discuss.

Difficulty

The identities are short once Proposition 1 is available, so the weight of the mission lies in two places. First, Proposition 1 itself is a strong duality theorem for optimal transport over all probability measures on $\mathbb R^{d+1}$, with a cost that takes the value $+\infty$ and an unbounded loss, and with attainment of the dual minimum; it is quoted from Blanchet and Murthy (Math. Oper. Res. 2019) and not proved in this paper. The weak-duality inequality is routine; the reverse inequality requires constructing near-optimal distributions from the dual, which needs measurable selection of near-maximizers and does not follow from finite-dimensional convex duality. Second, the inner suprema require an exact Hölder-attainment argument for the pair of conjugate norms $\ell_p$ and $\ell_q$, including $q = 1$ and $q = \infty$, and for the hinge loss a minimax exchange over $\alpha \in [0,1]$. Bypassing duality by a direct construction of the worst distribution is possible for the upper value but not obviously for the lower bound at the boundary $\lambda = \|\beta\|_p$.

Formalization scope

• Predictors are Fin d → ℝ, a data point is (Fin d → ℝ) × ℝ with the product Borel σ-algebra, and samples are indexed by Fin n with 0 < n. Labels are real numbers with the hypothesis $Y_i \in \{-1,+1\}$, which Theorem 2 inherits from Example 2; the cost $N_q$ is defined on all of $\mathbb R^d\times\mathbb R$.
• The $\ell_q$ norm is the norm of PiLp q, with q p : ℝ≥0∞ and p.HolderConjugate q; $q = 1$ and $q = \infty$ are included, and no further restriction on $q$ is imposed.
• The transport cost is an infimum in $[0,\infty]$ over probability measures on $Z\times Z$ with both marginals fixed. Expectations are lower Lebesgue integrals of the nonnegative losses, and the worst case is a supremum in $[0,\infty]$ over probability measures. The empirical distribution is the published platform definition WassersteinDRO.Regularization.empiricalDistribution.
• Readings. The paper prints the SVM identity without $\inf_\beta$ on the right; the goal states the per-$\beta$ identities (what the proof establishes) and the identities of infima with $\inf_\beta$ on both sides. The proof's displays write the transport norm as $\|\cdot\|_p$ and the penalty as $\|\beta\|_q$, the reverse of the theorem; milestones use the theorem's convention. The logistic chain's printed indicators $\mathbf 1_{\{\lambda>\|\beta\|\}}$, $\infty\mathbf 1_{\{\lambda\le\|\beta\|\}}$ should read $\ge$ and $<$; the stated end-to-end identity is unaffected. Proposition 1 is stated with a fixed nonnegative loss and $\delta > 0$.
• A trivializing formalization is ruled out: a cost infimum over sub-probability couplings or with one marginal free, or a Bochner expectation that vanishes on non-integrable laws, would make the worst case $+\infty$ or $0$; the definitions here fix both marginals, use probability measures only and integrate in $[0,\infty]$. At $\delta = 0$ the ball is $\{P_n\}$ and both sides reduce to the empirical loss.
• Infrastructure needed: optimal-transport duality with extended-valued lower semicontinuous costs (reusable well beyond this mission), Hölder equality cases for PiLp, and calculus for the logistic function. Contributions to any of these are welcome, as are proofs of the inner suprema, which are independent of Proposition 1.

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
• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, NIPS 2015. https://arxiv.org/abs/1509.09259

Why lower bounds for first-order methods

Upper bounds for an optimization method say how fast it converges; oracle complexity lower bounds say how fast any method of a given kind can possibly converge. Chapter 3 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015, arXiv:1405.4980) proves upper bounds for subgradient descent on Lipschitz functions and for gradient methods on smooth functions. Section 3.5 (Lower bounds, pp. 279–283) shows that these rates cannot be improved by more than a numerical constant, as long as the number of queries is smaller than the dimension. For smooth convex functions the matching lower bound is what identifies Nesterov's accelerated gradient descent, with its $1/t^2$ rate, as an optimal method.

Timeline. The lower bounds first appeared in A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization (Wiley, 1983). The presentation followed by the book, with an explicit tridiagonal quadratic as the hard instance and the "span of past gradients" restriction on the method, is that of Y. Nesterov, Introductory Lectures on Convex Optimization (Kluwer, 2004), §2.1.2. Nesterov's accelerated method (1983) attains the matching upper bound.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $x^\top y$, coordinates $x(1),\dots,x(n)$, canonical basis $e_1,\dots,e_n$ and balls $\mathrm B_2(R)=\{x:\|x\|\le R\}$. A first-order oracle for $f$ answers a query $x$ with a subgradient $g\in\partial f(x)$ (the gradient when $f$ is differentiable). A black-box procedure maps the history $(x_1,g_1,\dots,x_t,g_t)$ to the next query $x_{t+1}$. Section 3.5 restricts attention to procedures with

$$x_1=0,\qquad x_{t+1}\in\mathrm{Span}(g_1,\dots,g_t)\quad(t\ge0), \tag{3.15}$$

which covers gradient descent, its accelerated variants and conjugate gradient. A function is $\beta$-smooth if its gradient is $\beta$-Lipschitz; $L$-Lipschitz on $\mathcal X$ if every subgradient at every point of $\mathcal X$ has norm at most $L$; $\alpha$-strongly convex if $x\mapsto f(x)-\frac\alpha2\|x\|^2$ is convex.

The hard smooth instance uses, for $k\le n$, the symmetric tridiagonal matrix $A_k$ with entries $2$ on the first $k$ diagonal positions and $-1$ on the neighbouring off-diagonal positions of the leading $k\times k$ block, zero elsewhere, and the quadratics

$$f_k(x)=\frac\beta8x^\top A_kx-\frac\beta4x^\top e_1 ,\qquad f_k^*=\inf_{x\in\mathbb R^n}f_k(x).$$

Formalization targets

Goal: Theorem 3.14 (p. 282)

For $1\le t\le\frac{n-1}2$ and $\beta>0$ there are a $\beta$-smooth convex $f$ and a minimizer $x^*$ such that every procedure satisfying (3.15) has

$$\min_{1\le s\le t}f(x_s)-f(x^*)\ \ge\ \frac{3\beta}{32}\,\frac{\|x_1-x^*\|^2}{(t+1)^2}.$$

The constant $3/32$ is the book's.

Milestones (proof of Theorem 3.14, pp. 282–283)

1. $0\preceq A_k\preceq4I_n$, through $x^\top A_kx=x(1)^2+x(k)^2+\sum_{i=1}^{k-1}(x(i)-x(i+1))^2$.
2. For $f=f_{2t+1}$ and any procedure satisfying (3.15), $x_s\in\mathrm{Span}(e_1,\dots,e_{s-1})$; hence $f(x_s)=f_s(x_s)$ for $s\le t$.
3. $x_k^*(i)=1-\frac i{k+1}$ solves $A_kx=e_1$, minimizes $f_k$, and $f_k^*=-\frac\beta8\bigl(1-\frac1{k+1}\bigr)$.
4. $\|x_k^*\|^2\le\frac{k+1}3$.
5. $f_t^*-f_{2t+1}^*=\frac\beta8\bigl(\frac1{t+1}-\frac1{2t+2}\bigr)\ge\frac{3\beta}{32}\frac{\|x^*_{2t+1}\|^2}{(t+1)^2}$.

Companion: Theorem 3.13 (p. 280)

For $1\le t\le n$ and $L,R>0$ there are a convex $f$, $L$-Lipschitz on $\mathrm B_2(R)$, and a first-order oracle for it such that every procedure satisfying (3.15) has $\min_{s\le t}f(x_s)-\min_{\mathrm B_2(R)}f\ge\frac{RL}{2(1+\sqrt t)}$; and for $\alpha>0$ there are an $\alpha$-strongly convex $f$, $L$-Lipschitz on $\mathrm B_2(\frac L{2\alpha})$, and an oracle with gap at least $\frac{L^2}{8\alpha t}$ over that ball.

Significance

The upper bounds of Chapter 3 (projected subgradient descent at rate $RL/\sqrt t$, accelerated gradient descent at rate $\beta\|x_1-x^*\|^2/t^2$) become optimal statements only through these lower bounds: no method in the class (3.15) can be faster by more than a constant factor while $t$ is below the dimension. The restriction to $t\lesssim n$ is necessary, since Chapter 2's cutting-plane methods converge exponentially once the number of queries exceeds the dimension.

The results are classical and proved. Formalizing them yields machine-checked versions of the quadratic-form computation for the tridiagonal matrix, of the Krylov-type support argument under (3.15), and of the explicit minimizer of $f_k$, each reusable in other lower-bound arguments (Theorem 3.15 in $\ell_2$, lower bounds for strongly convex smooth functions, conjugate gradient analyses). The platform held no formal statement of these oracle lower bounds when this mission was drafted.

Difficulty

Each analytic step is elementary; the difficulty is in the bookkeeping. The span argument is an induction that must track, at each step, that the gradient of a tridiagonal quadratic at a vector supported on the first $s-1$ coordinates is supported on the first $s$, and that the span hypothesis transfers this to the next query. The minimizer computation requires solving $A_kx=e_1$ on the leading block and showing that the coordinates beyond $k$ do not affect $f_k$. A natural first attempt, choosing the hard function after seeing the procedure, proves a much weaker statement and is excluded by the quantifier order: the function is fixed first and must defeat every procedure.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Coordinates in Lean are 0-based; the definitions provide the book's 1-based coordinate coord x i and basis vector basisVec n i, and the matrix tridiag n k translates book index $i$ to Fin n index $i-1$. The query sequence starts at index $1$. The oracle is a fixed map $g$, so (3.15) reads $x_{t+1}\in\mathrm{Span}(g(x_1),\dots,g(x_t))$ with $x_1=0$. In Theorem 3.14 the oracle is the gradient, given as a map with HasGradientAt everywhere; $\beta$-smoothness is the Lipschitz bound on that map. In Theorem 3.13 the oracle is part of what is constructed, because the book's proof uses a specific "resisting" subgradient selection and the claim fails for an arbitrary one.

Committed conventions, each stated in the item's Formalization Note: the minimum over $1\le s\le t$ is the bound for every such $s$, and $t\ge1$ is required; $t\le(n-1)/2$ is $2t+1\le n$; the minimizer $x^*$ is existentially chosen together with $f$ (the hard function has many minimizers when $2t+1<n$, and the bound is false for some of them); the minimum over a ball is the bound against every point of the ball; $f_k^*$ is the real infimum, asserted to be attained.

A formalization that let the function depend on the procedure, dropped $x_1=0$, or took the span over gradients at points other than the queries would state a different and weaker theorem; the statements here keep $f$ (and the oracle) before the universally quantified procedure.

Infrastructure needed: quadratic forms of explicit matrices on EuclideanSpace, gradients of quadratics, and span/support lemmas for EuclideanSpace.single-type vectors. Contributions of proofs for any milestone, and of the strongly convex $\ell_2$ lower bound (Theorem 3.15, not included here), are welcome.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. https://arxiv.org/abs/1405.4980
• A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Many planning problems are made in two stages: a first decision $x$ (capacity, inventory, a network design) is fixed before an uncertain demand is revealed, and a second decision $y$ (recourse, routing, overtime) is taken afterwards. Two-stage stochastic optimization models the demand as random and minimizes expected cost; its second stage is a whole policy $\omega\mapsto y(\omega)$, and the problem is intractable in general, especially with integer variables (Dyer and Stougie, 2006). Robust optimization instead picks one static pair $(x,y)$ that is feasible for every possible demand and minimizes its worst-case cost; it is a single deterministic mixed-integer program and needs no knowledge of the distribution (Ben-Tal and Nemirovski, 2002; Bertsimas and Sim, 2004).

The question this mission addresses is how much is lost by solving the robust problem in place of the stochastic one. Bertsimas and Goyal (Math. Oper. Res. 2010) show that when only the right-hand side is uncertain, the uncertainty set is symmetric and the distribution is centred at its point of symmetry, the loss is at most a factor of two, and that this factor is tight.

Setting

Fix $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$ and nonnegative costs $c\in\mathbb R^{n_1}_+$, $d\in\mathbb R^{n_2}_+$. A set $\Omega$ of scenarios carries a probability measure $\mu$, and each scenario $\omega$ has a right-hand side $b(\omega)\in\mathbb R^m_+$. The uncertainty set is $\mathcal I_b(\Omega)=\{b(\omega):\omega\in\Omega\}$. First-stage variables are nonnegative, with integer values on a designated set of coordinates; second-stage variables are nonnegative reals ($p_2=0$).

The stochastic problem $\Pi_{\mathrm{Stoch}}(b)$, (1.1), chooses $x$ and a policy $y(\cdot)$:

$$z_{\mathrm{Stoch}}(b)=\inf\ c^Tx+\mathbb E_\mu[d^Ty(\omega)]\quad\text{s.t.}\quad Ax+By(\omega)\ge b(\omega)\ \ \forall\omega\in\Omega .$$

The robust problem $\Pi_{\mathrm{Rob}}(b)$, (1.2), chooses one $y$ for all scenarios:

$$z_{\mathrm{Rob}}(b)=\inf\ c^Tx+d^Ty\quad\text{s.t.}\quad Ax+By\ge b(\omega)\ \ \forall\omega\in\Omega .$$

A set $P$ is symmetric (Definition 1.2) if there is $u^0\in P$ with $u^0+z\in P\iff u^0-z\in P$ for all $z$; $u^0$ is its point of symmetry. Hypercubes, ellipsoids and norm balls are symmetric. A probability measure on a symmetric set is symmetric (Definition 1.4) if it gives a set and its reflection $\{2u^0-x\}$ the same mass.

Formalization targets

Goal: Theorem 2.1 (p. 10)

If $\mathcal I_b(\Omega)$ is symmetric with point of symmetry $b(\omega^0)$, $p_2=0$, and $\mu$ satisfies

$$\mathbb E_\mu[b(\omega)]\ \ge\ b(\omega^0)\qquad(2.1)$$

then

$$z_{\mathrm{Rob}}(b)\ \le\ 2\cdot z_{\mathrm{Stoch}}(b).$$

Milestones on the way

• Lemma 2.2 (p. 12): the coordinatewise bounding box $H$ of a symmetric set $S$ is the smallest hypercube containing $S$.
• Lemma 2.3 (p. 12): the centre $x^0$ of $H$ is the point of symmetry of $S$, and $x\le 2x^0$ on $S$ when $S\subseteq\mathbb R^n_+$.
• Eqs. (2.9)–(2.10) (p. 13): if $(x,y)$ covers $b(\omega^0)$ then $(2x,2y)$ covers every $b(\omega)$, so it is robust feasible.
• p. 14 display: under (2.1), the mean second-stage decision $\mathbb E_\mu[y(\omega)]$ covers $b(\omega^0)$.
• Lemma 2.1 (p. 11): a symmetric probability measure has mean $u^0$, so it satisfies (2.1).
• Theorem 2.7 (p. 21): the same bound $z_{\mathrm{Rob}}(b)\le 2\,z_{\mathrm{Stoch}}(b)$ when $\mathcal I_b(\Omega)$ is convex and positive (contained in a symmetric subset of $\mathbb R^m_+$ whose centre lies in $\mathcal I_b(\Omega)$).

Significance

The result. The robust problem is one mixed-integer program, independent of $\mu$; the stochastic problem optimizes over policies and requires the distribution. Theorem 2.1 says that under symmetry the static robust solution $(x,y)$ used in every scenario is a 2-approximation of the optimal expected cost, for every centred distribution at once. The companion results of the paper show the hypotheses matter: the bound is tight for symmetric sets, the gap is unbounded (at least $n+1$) on the non-symmetric simplex (Theorem 2.6), and unbounded when costs are uncertain as well (Theorem 3.1). The theorem also underlies later work on the power of static and affine policies in adaptive optimization (Bertsimas and Goyal, 2012).

Formalizing it. The theorem and its proof are published; nothing in this mission is open mathematics. To our knowledge none of these statements has a machine-checked proof. The mission produces a reusable Lean model of two-stage stochastic and robust mixed-integer covering problems with arbitrary scenario spaces, extended-real optimal values and genuine expectations, together with the elementary geometry of point-symmetric sets. The same objects are used by the other missions of this series (the simplex and cost-uncertainty gaps, and the adaptability gap).

Difficulty

Each step of the published argument is short; the difficulty is in stating it at the right generality. The paper begins "consider an optimal solution" of $\Pi_{\mathrm{Stoch}}(b)$; optimal policies need not exist for an arbitrary scenario space, so the statement is about infima and every step must work for an arbitrary feasible pair. Passing from "$Ax+By(\omega)\ge b(\omega)$ for all $\omega$" to "$Ax+B\,\mathbb E_\mu[y]\ge\mathbb E_\mu[b]$" needs integrability of the policy and of $b$ and linearity of the Bochner integral through a matrix. The bound $b(\omega)\le 2b(\omega^0)$ uses symmetry together with nonnegativity of the uncertainty set; symmetry alone does not give it. Integrality of the second stage breaks the argument, since $\mathbb E_\mu[y(\omega)]$ need not be integral.

Formalization scope

• Vectors are Fin k → ℝ with the componentwise order, products A *ᵥ x and inner products c ⬝ᵥ x. The mixed-integer domain is "nonnegative with integer values on a set $I$ of coordinates", which is the paper's $\mathbb R^{n-p}_+\times\mathbb Z^p_+$ up to relabelling.
• $\Omega$ is an arbitrary measurable space with a probability measure; $\mathcal I_b(\Omega)$ is Set.range b. Constraints hold for every scenario, not almost surely.
• Second-stage policies are $\mu$-integrable, and $b$ is $\mu$-integrable in every statement that uses (2.1). Without these, Lean's integral of a non-integrable function is $0$ and (2.1) would degenerate.
• $z_{\mathrm{Stoch}}$ and $z_{\mathrm{Rob}}$ are infima in EReal, equal to $+\infty$ when infeasible; no attainment is assumed. A real-valued infimum would return $0$ on an infeasible robust problem and make the goal trivial; that formalization is ruled out.
• The bounding box of (2.5)–(2.7) uses suprema and infima, with boundedness assumed where needed.
• Corrections to the page: Lemma 2.3's inequality $x\le 2x^0$ is stated under $S\subseteq\mathbb R^n_+$, which its proof uses and which holds in every application; Lemma 2.1 assumes the measure has a mean; Theorem 2.7 carries the standing assumption $p_2=0$ of §2.

Contributions welcome: proofs of the milestones and the goal, and general lemmas on point-symmetric sets and on interchanging Bochner integrals with matrix–vector products, both reusable outside this mission.

Selected references

• D. Bertsimas, V. Goyal, On the power of robust solutions in two-stage stochastic and adaptive optimization problems, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1090.0440 (cited from the authors' manuscript, MIT DSpace)
• A. Ben-Tal, A. Nemirovski, Robust optimization — methodology and applications, Mathematical Programming 92, 2002. https://doi.org/10.1007/s101070100286
• D. Bertsimas, M. Sim, The price of robustness, Operations Research 52(1), 2004. https://doi.org/10.1287/opre.1030.0065
• M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Mathematical Programming 106, 2006. https://doi.org/10.1007/s10107-005-0578-0
• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134, 2012. https://doi.org/10.1007/s10107-011-0444-4

Motivation

Classical inventory theory chooses order quantities against a probability distribution of demand. The resulting dynamic programs are optimal in expectation but need the distribution, and they become intractable once several installations, capacities or fixed costs interact. Robust optimization replaces the distribution by an uncertainty set and asks for the order sequence whose worst-case cost over that set is smallest. Bertsimas and Thiele (Operations Research 54(1), 2006) applied the budget-of-uncertainty approach of Bertsimas and Sim (The Price of Robustness, Operations Research 52(1), 2004) to finite-horizon inventory control. Their main structural result says that robustness does not destroy the structure of the classical problem. The robust problem is a deterministic (nominal) inventory problem with an explicitly modified demand, and the price of robustness is an explicit constant.

Setting

A single item is ordered at a single installation over periods $k = 0, \dots, T-1$. The stock at the beginning of the horizon is $x_0$. Orders $u_k \ge 0$ arrive immediately, demand $w_k$ is subtracted, and excess demand is backlogged, so the stock at the end of period $k$ is

$$x_{k+1} = x_0 + \sum_{i=0}^{k} (u_i - w_i).$$

The demand of period $k$ is uncertain: $w_k = \bar w_k + \hat w_k z_k$ with a nominal demand $\bar w_k$, a maximal deviation $\hat w_k \ge 0$ and a scaled deviation $z_k \in [-1, 1]$. A budget of uncertainty $\Gamma_k$ limits the total scaled deviation up to period $k$. The budgets satisfy $0 \le \Gamma_0$ and $\Gamma_k \le \Gamma_{k+1} \le \Gamma_k + 1$.

Each period costs $C(u_k) + R(x_{k+1})$. The purchasing cost is $C(u) = K + cu$ for $u > 0$ and $C(0) = 0$, with $c > 0$ and $K \ge 0$. The holding/shortage cost is $R(x) = \max(hx, -px)$, with $h \ge 0$ and $p > c$. The nominal problem with demand $w$ minimizes $\sum_{k<T} (C(u_k) + R(x_{k+1}))$ over $u \ge 0$ for a fixed demand sequence $w$.

For each $k$, $A_k$ is the optimal value of the linear program

$$A_k = \max\Big\{\sum_{i=0}^{k} \hat w_i z_i \;:\; \sum_{i=0}^{k} z_i \le \Gamma_k,\ 0 \le z_i \le 1\Big\} \qquad (13)$$

It is the worst-case deviation of the cumulative demand up to $k$ from its nominal value, with $A_{-1} = 0$. Write $\bar x_{k+1} = x_0 + \sum_{i\le k}(u_i - \bar w_i)$ for the nominal stock. The robust formulation (14) minimizes $\sum_{k<T} (C(u_k) + y_k)$ over $(u, y, q, r)$ subject to the following constraints for every $k < T$:

• $u_k \ge 0$, $q_k \ge 0$, and $r_{ik} \ge 0$, $q_k + r_{ik} \ge \hat w_i$ for $i \le k$;
• $y_k \ge h(\bar x_{k+1} + q_k\Gamma_k + \sum_{i\le k} r_{ik})$;
• $y_k \ge p(-\bar x_{k+1} + q_k\Gamma_k + \sum_{i\le k} r_{ik})$.

The variables $q, r$ are the dual of (13). Formulation (14) is equivalent to requiring the holding and shortage constraints of period $k$ for every demand whose scaled deviations satisfy $|z_i| \le 1$ and $\sum_{i \le k}|z_i| \le \Gamma_k$.

Formalization targets

Goal: Theorem 3.2 (a), (b), (d)

Let the modified demand be

$$w'_k = \bar w_k + \frac{p-h}{p+h}\,(A_k - A_{k-1}). \qquad (20)$$

Write $N_{w'}(u)$ for the nominal cost of $u$ under demand $w'$. Then:

1. For every $u \ge 0$, the minimum of the objective of (14) over the feasible $(y, q, r)$ is attained and equals

$$N_{w'}(u) + \frac{2ph}{p+h}\sum_{k=0}^{T-1} A_k.$$

2. $u$ is the order part of an optimal solution of (14) if and only if $u$ is optimal for the nominal problem with demand $w'$.
3. The optimal cost of (14) is the optimal nominal cost under $w'$ plus $\frac{2ph}{p+h}\sum_k A_k$.
4. If $K = 0$ and $w'_k \ge 0$, the order-up-to policy with levels $S_k = w'_k$ is robust-optimal.

Milestones

The milestones are the steps of the paper's proof, in order:

• LP (13) and its dual are attained with the common value $A_k$.
• The constraints of (14) are the robust counterpart of the $k$-th holding/shortage pair (10)–(11).
• For fixed orders, the value of (14) is the sum (21).
• The modified stock (22) satisfies $x'_{k+1} = \bar x_{k+1} - \frac{p-h}{p+h}A_k$.
• The max identity (23): $\max(h(\bar x+A), p(-\bar x+A)) = \max(hx', -px') + \frac{2ph}{p+h}A$.
• Lemma 3.1(b): for nonnegative demand, the nominal problem without fixed cost is solved by ordering up to $S_k = w_k$.
• Remark 1: $A_{k-1} \le A_k$, so $w'_k \ge \bar w_k$ when $p \ge h$.
• Remark 3: under i.i.d. demand, $A_k = \hat w\Gamma_k$, which gives the closed-form thresholds.

Significance

The theorem reduces robust inventory control to nominal inventory control. Every structural fact known for the deterministic problem then transfers to the robust one. These include the optimality of base-stock policies without fixed cost and the threshold structure with a fixed cost. The robust base-stock levels are explicit: they shift the nominal levels by $\frac{p-h}{p+h}(A_k - A_{k-1})$, upward when shortage is more expensive than holding. The extra cost $\frac{2ph}{p+h}\sum_k A_k$ quantifies the price of protection as a function of the budgets. The paper uses the same reduction for capacitated orders (Theorem 3.3) and for supply networks (§4).

The result has been proved since 2006, and no machine-checked proof of it, or of any budgeted robust counterpart, is known to exist. This mission provides several formalizations for reuse:

• the budgeted robust counterpart of a pair of piecewise-linear constraints;
• the duality of the fractional knapsack LP (13);
• the optimality of base-stock orders for a deterministic backlogged inventory problem.

Difficulty

The algebraic core, identity (23), is elementary. The work is in the reductions around it. The first is that (14) really is the worst case of (10)–(11): this needs strong duality for (13), together with attainment on both sides, and the observation that the minimizing and maximizing deviations of a constraint pair differ. The second is that the minimum of (14) over the auxiliary variables, for fixed orders, is (21). This requires the dual optimum to be attained with the value of (13), and $h, p \ge 0$ so that the cost is monotone in $A_k$. The third is the base-stock part, which needs Lemma 3.1(b), a global optimality statement for a $T$-period problem with backlogging. The paper proves that lemma by an explicit dual certificate. An argument through first-order conditions in each period is not enough, because orders in one period affect every later stock level.

Formalization scope

All data are real numbers and sequences are ℕ → ℝ; only indices $k < T$ matter. stock w u k denotes $x_{k+1}$, the stock at the end of period $k$. The standing assumptions of §3.1 are fields of the model:

• $c > 0$, $K \ge 0$, $h \ge 0$, $p > c$;
• $\hat w_k \ge 0$;
• $\Gamma_0 \ge 0$ and $\Gamma_k \le \Gamma_{k+1} \le \Gamma_k + 1$.

The conventions and corrections are:

• Fixed cost. The paper writes it with binary variables and a big-$M$ constraint. Here it is the indicator $C(u_k)$ in the objective, as in the paper's own (21).
• "Optimal". It always means minimality over all feasible points.
• The policy. It is the order sequence chosen at time 0.
• $A_k$. It is the value of (13), as in Remark 1 after the theorem, not "the optimal $q^*, r^*$ of (14)", which need not be unique.
• The robust formulation. (14) is formalized as printed: the $k$-th constraint pair is protected by the budget $\Gamma_k$ alone, not by the intersection of all budgets up to $k$.
• Sign slip. The page's $x_{k+1} = \bar x_{k+1} + \sum \hat w_i z_i$ is a sign slip for $\bar x_{k+1} - \sum \hat w_i z_i$. The formal statements use the correct sign; the result is unaffected because the deviation set is symmetric.
• Part (b). It is stated under $w'_k \ge 0$. As printed it fails when $p < h$ makes $w'$ negative, for example $T = 2$, $\bar w = \hat w = (10, 0)$, $\Gamma = (0, 1)$, $c = 1$, $h = 4$, $p = 2$, $x_0 = 0$. Lemma 3.1(b) carries the matching hypothesis of nonnegative demand.
• Remark 3. It adds $\Gamma_0 \le 1$.
• Remark 1. Its inequalities are weak.
• Not stated. The (s, S) clause of (a) and part (c) are excluded. They rest on a stochastic theorem cited from Bertsekas (1995) and on thresholds stated through the optimal ordering times.

A trivializing formalization is ruled out: the robust cost is formulation (14) with its variables $y, q, r$, and $A_k$ is the value of LP (13). Neither is the closed-form objective (21) nor an arbitrary sequence. Contributions are welcome on the LP duality of (13) (a fractional knapsack), on the robust counterpart milestone, and on Lemma 3.1(b), each of which is independent of the others.

Selected references

• D. Bertsimas, A. Thiele, A Robust Optimization Approach to Inventory Theory, Operations Research 54(1):150–168, 2006. https://doi.org/10.1287/opre.1050.0238
• D. Bertsimas, M. Sim, The Price of Robustness, Operations Research 52(1):35–53, 2004. https://doi.org/10.1287/opre.1030.0065
• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. 1, Athena Scientific, 1995.

Motivation

Many constrained optimization problems in machine learning and statistics have a feasible set $\mathcal X$ over which a linear function is cheap to minimize but a Euclidean projection is expensive: the $\ell_1$-ball, the simplex, the nuclear-norm ball, the convex hull of a combinatorial family. Projected gradient descent needs a projection at every step. Conditional gradient descent, introduced by Frank and Wolfe in 1956 for quadratic programming, replaces the projection by a call to a linear minimization oracle over $\mathcal X$, and its iterates are convex combinations of oracle outputs, which makes them sparse when $\mathcal X$ is a polytope.

This mission is the seventh of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015, arXiv:1405.4980v2). It covers Section 3.3, whose main result, Theorem 3.8, is the $O(1/t)$ rate of the method in the form given by Jaggi (2013), going back to Dunn and Harshbarger (1978).

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$. For a linear form $g$ on $E$, written $v\mapsto g^\top v$, the dual norm is $\|g\|_*=\sup_{\|v\|\le1}g^\top v$. Let $\mathcal X\subseteq E$ be nonempty, compact and convex, with diameter $R=\sup_{x,y\in\mathcal X}\|x-y\|$.

Let $f:E\to\mathbb R$ be differentiable with gradient $\nabla f(x)$, a linear form on $E$. For $\beta\ge0$, $f$ is β-smooth with respect to $\|\cdot\|$ on $\mathcal X$ if

$$\|\nabla f(x)-\nabla f(y)\|_*\le\beta\|x-y\|\qquad(x,y\in\mathcal X).$$

A point $x^*\in\mathcal X$ with $f(x^*)=\min_{x\in\mathcal X}f(x)$ is fixed throughout, and $\delta_t=f(x_t)-f(x^*)$.

Given step sizes $(\gamma_s)_{s\ge1}$, a run of conditional gradient descent is a pair of sequences with $x_1\in\mathcal X$ and, for every $t\ge1$,

$$y_t\in\operatorname*{argmin}_{y\in\mathcal X}\nabla f(x_t)^\top y\quad(3.8),\qquad x_{t+1}=(1-\gamma_t)x_t+\gamma_ty_t\quad(3.9).$$

The minimizer $y_t$ need not be unique; any choice is allowed.

Formalization targets

Goal: Theorem 3.8 (p. 272)

If $f$ is convex and $\beta$-smooth with respect to $\|\cdot\|$ and $\gamma_s=\frac{2}{s+1}$ for $s\ge1$, then every run satisfies, for every $t\ge2$,

$$f(x_t)-f(x^*)\le\frac{2\beta R^2}{t+1}.$$

Milestones

1. Inequality (3.4) in an arbitrary norm (p. 267, used on p. 272): for $x,y\in\mathcal X$, $0\le f(x)-f(y)-\nabla f(y)^\top(x-y)\le\frac{\beta}{2}\|x-y\|^2$.
2. The one-step recursion (pp. 272–273): for any run with $\gamma_s\in[0,1]$,

$$\delta_{s+1}\le(1-\gamma_s)\delta_s+\frac{\beta}{2}\gamma_s^2R^2 .$$

3. Initialization (p. 273): if $\gamma_1=1$, then $\delta_2\le\frac{\beta}{2}R^2$.
4. The induction (p. 273): a real sequence with $\delta_2\le\frac{\beta}{2}R^2$ and the recursion of milestone 2 with $\gamma_s=\frac{2}{s+1}$ for $s\ge2$ satisfies $\delta_t\le\frac{2\beta R^2}{t+1}$ for $t\ge2$.

Significance

Theorem 3.8 is the basic guarantee for projection-free first-order optimization. Its rate does not depend on the dimension, and it depends on the geometry only through the product $\beta R^2$, both measured in the same norm, which may be chosen to fit $\mathcal X$: for the $\ell_1$-ball, smoothness in $\|\cdot\|_1$ with dual norm $\|\cdot\|_\infty$ gives much better constants than the Euclidean analysis. The book applies it this way to a LASSO-type problem (Section 3.3, pp. 274–276), and the same bound underlies the sparse-approximation corollary on the simplex (p. 273) and the many later variants of the method (away steps, stochastic and online conditional gradient).

The result is classical and proved in the book. What this mission adds is a machine-checked statement and proof in an arbitrary finite-dimensional normed space, with the dual norm as the operator norm on linear forms, and a reusable encoding of norm-smoothness and of conditional gradient runs. On Prove2Me a related result is already proved: Lan's Theorem 7.1 (First-order and Stochastic Optimization Methods), which bounds $f(y_k)-f^*$ by $\frac{2L}{k(k+1)}\sum_{i\le k}\|x_i-y_{i-1}\|^2$ with a different indexing; after the diameter bound it yields $2\beta R^2/t$ at Bubeck's iterate $x_t$, which is weaker than Theorem 3.8 by one step.

Difficulty

The difficulty is in the bookkeeping of norms and indices, not in a deep idea. Inequality (3.4) is proved in the book only for the Euclidean norm, where $\nabla f(x)\in\mathbb R^n$ and the Cauchy–Schwarz inequality is used; in a general norm it needs the pairing between a linear form and a vector and the bound $|g^\top v|\le\|g\|_*\|v\|$. The rate $2\beta R^2/(t+1)$ is attained only by starting the induction at $t=2$, where the step $\gamma_1=1$ erases the dependence on the starting point; at $t=1$ the bound can fail, since $\delta_1$ is arbitrary. A first attempt that runs the induction from $t=1$ with an arbitrary $\delta_1$ does not give the stated constant.

Formalization scope

$E$ is a type with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]; nothing is specialised to the Euclidean norm. The gradient is an explicit derivative map f' : E → (E →L[ℝ] ℝ) with HasFDerivAt f (f' x) x for every x; $\nabla f(x)^\top v$ is f' x v, and $\|\cdot\|_*$ is the operator norm, which equals $\sup_{\|v\|\le1}g^\top v$. $R$ is Metric.diam X, which equals the supremum of $\|x-y\|$ over $\mathcal X$ because $\mathcal X$ is compact. Sequences are indexed by ℕ with the first iterate at index 1.

Committed conventions: $\mathcal X$ compact, convex and containing $x^*$ (hence nonempty); convexity of $f$ and the Lipschitz bound on the gradient are assumed on $\mathcal X$ only, which is weaker than the book's global assumptions; $\beta\ge0$; the existence of the minimizer $x^*$ is the book's standing assumption (p. 242); the conclusion is stated for $t\ge2$, as in the book. Runs are predicates: $y_t$ is any minimizer of the linear form over $\mathcal X$ and $y_t\in\mathcal X$ is required, so the goal quantifies over every run with $\gamma_s=2/(s+1)$. A formalization in which $y_t$ need not lie in $\mathcal X$, or in which smoothness is assumed only along the iterates, states a different theorem and is excluded.

A complete development needs the descent inequality (3.4) for Fréchet derivatives in a normed space (reusable for every smooth method in the series and beyond), the fact that the iterates stay in $\mathcal X$, and a scalar induction. Proofs of the milestones are welcome independently; milestone 4 is a statement about real sequences only.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. https://arxiv.org/abs/1405.4980
• M. Frank and P. Wolfe, An algorithm for quadratic programming, Naval Research Logistics Quarterly 3(1–2):95–110, 1956. https://doi.org/10.1002/nav.3800030109
• J. C. Dunn and S. Harshbarger, Conditional gradient algorithms with open loop step size rules, Journal of Mathematical Analysis and Applications 62(2):432–444, 1978. https://doi.org/10.1016/0022-247X(78)90137-3
• M. Jaggi, Revisiting Frank–Wolfe: projection-free sparse convex optimization, Proceedings of ICML 2013, PMLR 28(1):427–435. https://proceedings.mlr.press/v28/jaggi13.html
• G. Lan, First-order and Stochastic Optimization Methods for Machine Learning, Springer, 2020, Theorem 7.1. https://doi.org/10.1007/978-3-030-39568-1

Motivation

Gradient descent is a basic method for minimizing a differentiable function when evaluating its gradient is practical but solving the optimization problem directly is not. The rate at which its iterates approach an optimizer depends on the assumptions about the function. For a convex function with a Lipschitz gradient, the value error decreases at a sublinear rate. Adding strong convexity changes the behavior: the distance from the optimizer contracts at each step, giving an exponential bound on the value error. This section of Bubeck's monograph identifies a fixed step size that uses both the smoothness and curvature constants and gives the corresponding rate.

The result matters when a high-accuracy answer is needed. A sublinear bound makes each extra digit progressively more expensive; an exponential bound says that a fixed number of additional gradient evaluations reduces the error by a fixed factor. The theorem is a textbook result, already proved mathematically. This mission asks for its precise machine-checked statement and the source's supporting inequalities, rather than for a new optimization method.

Setting

Work in Euclidean space $\mathbb R^n$ with $n\ge1$, equipped with its usual inner product and norm. A differentiable function $f:\mathbb R^n\to\mathbb R$ has gradient $g(x)=\nabla f(x)$. It is $\beta$-smooth when its gradient is $\beta$-Lipschitz: $\|g(x)-g(y)\|\le\beta\|x-y\|$ for every $x,y$. It is $\alpha$-strongly convex when, for every $x,y$,

$$f(y)\ge f(x)+\langle g(x),y-x\rangle+\frac\alpha2\|y-x\|^2.$$

The first condition limits how rapidly the gradient changes. The second gives a quadratic lower bound on the function around any point. Here $\alpha>0$ and $\beta\ge0$. In positive dimension, the two conditions together entail $\beta\ge\alpha$, so the condition number $\kappa=\beta/\alpha$ is at least one. The case $\alpha=\beta$ remains part of the target.

A point $x^*$ is a global minimizer when $f(x^*)\le f(y)$ for every $y$. The book assumes such a point exists as a standing convention. A gradient descent run is a sequence $(x_t)_{t\ge1}$ satisfying $x_{t+1}=x_t-\eta g(x_t)$ at each positive index. Its first iterate $x_1$ is arbitrary. The step size in this mission is fixed at $\eta=2/(\alpha+\beta)$, rather than chosen by line search or adapted along the run.

Formalization targets

The central target is Theorem 3.12 of Bubeck, p. 279. For every integer $t\ge0$, the gradient descent run satisfies

$$f(x_{t+1})-f(x^*)\le \frac\beta2\exp\!\left(-\frac{4t}{\kappa+1}\right)\|x_1-x^*\|^2.$$

At $t=0$ this is a smoothness bound on the initial value gap. For subsequent iterations it gives a linear convergence rate with the explicit exponential factor stated in the book. No initial-radius bound or bounded domain is imposed: the actual squared distance $\|x_1-x^*\|^2$ appears in the conclusion.

The milestones trace the mathematical claims stated in the source. Equation (3.6) is the co-coercivity inequality for gradients of convex smooth functions. The proof of Lemma 3.11 introduces $\phi(z)=f(z)-(\alpha/2)\|z\|^2$, and identifies it as convex and $(\beta-\alpha)$-smooth. Lemma 3.11 combines curvature and smoothness into a sharper inequality for two gradients. The proof of Theorem 3.12 then gives a value-gap bound, a one-step distance contraction, and its iterated exponential form. These statements are separately useful: the co-coercivity and contraction bounds can be reused in analyses of related first-order methods.

Significance

The theorem states a complete guarantee for the algorithm: an explicit rule, the hypotheses on the objective, and a bound valid for every iteration count. It makes the role of $\kappa$ visible. When $\kappa$ is close to one, the contraction is strong; when the smoothness constant is much larger than the curvature constant, more iterations are needed for the same error reduction. The stated dependence supports comparisons with projected and accelerated gradient methods elsewhere in the same monograph.

Formalizing the result requires a common interface for actual gradients, smoothness, strong convexity, and algorithm runs. The strong-convexity predicate is an existing published definition, while the local smoothness and run definitions use Bubeck's conventions. Once these interfaces and the inequalities are proved, later missions can use the resulting declarations to compare rates without translating between informal meanings of “smooth” or changing the iterate index. The source provides a mathematical proof; these draft Lean theorems carry sorry and do not yet constitute machine-checked proofs.

Difficulty

The main issue is getting the sharp contraction factor from two assumptions that control different parts of the gradient step. A direct Lipschitz estimate on the update map does not by itself express the mixed inner-product term with the constants needed for the stated factor. Lemma 3.11 is the source's precise bridge between the gradient difference, the point displacement, and their inner product. The case $\alpha=\beta$ also needs to remain valid: a proof route that divides by $\beta-\alpha$ cannot cover that boundary by the same calculation.

The last display in the proof of Theorem 3.12 joins a one-step inequality involving $x_t$ to an exponential inequality involving $x_1$. The latter is the cumulative statement after $t$ steps. Keeping these as separate milestones makes each quantified claim explicit while preserving the theorem's bound.

Formalization scope

Lean represents $\mathbb R^n$ as EuclideanSpace ℝ (Fin n), with $n>0$. The gradient is an explicit map $g$ required to be the actual gradient of $f$ at every point. Smoothness is the gradient Lipschitz condition, not a quadratic upper bound used as a definition. Strong convexity uses the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn predicate on the whole space; its formula is the book's (3.13). Iterates are indexed from one, and index zero imposes no condition. The norm, inner product, constants, and real exponential follow the printed formulas.

The added explicit conditions are $n>0$, $\alpha>0$, and $\beta>0$ where Equation (3.6) divides by $\beta$. Positive dimension excludes a degenerate space where curvature imposes no restriction on smoothness. The positivity of $\alpha$ makes $\kappa$ meaningful; the source treats it as a positive strong-convexity parameter. The minimizer hypothesis is the book's standing convention. There is no assumption that $g(x^*)=0$: that property follows from global minimality and differentiability. A gradient map unrelated to $f$ would trivialize the model, so the smoothness definition includes the gradient identity.

The local development needs Euclidean inner-product identities, convexity, differentiability, Lipschitz gradient bounds, and real exponential estimates. The auxiliary function and the two co-coercivity inequalities are reusable outside this chapter. Contributions should prove the exact milestone statements and the final theorem, including $t=0$ and $\alpha=\beta$, without weakening constants or substituting another gradient descent step.

Selected references

• Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2; DOI:10.1561/2200000050.

Motivation

A shortest path problem asks how to reach a destination at minimum cost. In a stochastic shortest path problem, a decision at a state selects a probability distribution over successor states, so both the route and its total cost are random. Costs may have either sign. This makes the problem relevant to finite-state control models where rewards and expenses occur before eventual termination. Bertsekas and Tsitsiklis analyze this setting without requiring all one-stage costs to be nonnegative or all to be nonpositive. Their condition instead rules out an improper stationary policy whose costs stay finite from every initial state. Bertsekas and Tsitsiklis (1991), pp. 580–583.

Earlier treatments established Bellman-equation and algorithmic conclusions under positive or nonnegative costs. The 1991 paper traces the finite-control development from Eaton and Zadeh and the compact-control extension from Kushner, then removes the sign restriction while retaining finite state space. It also explains why the Bellman mapping need not contract when an improper policy is available. Bertsekas and Tsitsiklis (1991), pp. 581, 585. A separate, proved Prove2Me theorem from Bertsekas's textbook treats the special case in which every policy is proper and controls are finite; the result here permits improper policies and compact control spaces.

Setting

There are $n\ge1$ states. State $1$ is the destination. At state $i$, a control $u\in U(i)$ incurs a real cost $c_i(u)$ and moves the process to state $j$ with probability $p_{ij}(u)$. A selector $\mu$ chooses one control $\mu(i)$ at every state. A policy $\pi=(\mu_0,\mu_1,\ldots)$ may change selectors over time; a stationary policy repeats one selector. The matrix $P(\mu)$ has entries $p_{ij}(\mu(i))$, and $c(\mu)$ is the vector of one-stage costs. Bertsekas and Tsitsiklis (1991), p. 582.

The cost vector $x(\pi)$ is the coordinatewise limit inferior of expected partial costs, including the possibility of infinite values. The optimal cost $x_i^*$ is the infimum of $x_i(\pi)$ over all policies, including nonstationary ones. Optimality of a policy means it attains that infimum from every initial state. The fixed-selector operator is $T_\mu(x)=c(\mu)+P(\mu)x$; the Bellman operator $T$ takes the coordinatewise infimum of these vectors over selectors. Bertsekas and Tsitsiklis (1991), pp. 582–583, equations (2)–(6).

A stationary policy is proper when its probability of reaching state $1$ tends to one from every starting state. Assumption 1 says state $1$ is absorbing and cost-free, at least one proper stationary policy exists, and every improper stationary policy has a partial-cost coordinate tending to $+\infty$. Assumption 2 makes each control space compact, each cost function lower semicontinuous, and each transition-probability coordinate continuous. Work takes place in $X=\{x\in\mathbb R^n:x_1=0\}$. Bertsekas and Tsitsiklis (1991), pp. 583–584.

Formalization targets

Proposition 2: Bellman's equation and value iteration

Under Assumptions 1 and 2, the optimal cost is finite and is the unique fixed point of $T$ in $X$. Every initial $x\in X$ has

$$\lim_{t\to\infty}T^t(x)=x^*.$$

A stationary selector $\mu$ is optimal exactly when $T_\mu(x^*)=T(x^*)$; an optimal proper stationary selector exists. These are all clauses of Proposition 2, rather than separate targets selected from it. Bertsekas and Tsitsiklis (1991), p. 586, Proposition 2.

Supporting results

The milestone list follows the source's Proposition 1, Lemmas 1–3, and the numbered equations used by their proof. Proposition 1 supplies a weighted maximum-norm contraction when every stationary policy is proper. Lemma 1 describes fixed costs of a proper policy and characterizes properness through a Bellman inequality. Lemma 2 gives continuity of $T$. Lemma 3 controls limits of proper policies; its second part detects a limit that becomes improper through diverging costs. Appendix equations (22) and (24), and the policy-improvement equation (15), provide the paper's intermediate targets. Bertsekas and Tsitsiklis (1991), pp. 585–587, 591–592.

Significance

Proposition 2 identifies the cost of the best policy by a finite-dimensional Bellman equation even though the definition of optimal cost ranges over all, possibly nonstationary, policies. Its convergence clause justifies value iteration from any vector whose destination coordinate is zero. Its policy criterion and existence clause connect a fixed point to an implementable stationary decision rule. The paper applies these conclusions to successive approximation and policy iteration in §4. Bertsekas and Tsitsiklis (1991), pp. 586, 590–591.

The paper proves these statements. This mission seeks machine-checked proofs of their exact finite-state formulation and of the listed intermediate results. The resulting finite stochastic-matrix, hitting, and policy-cost infrastructure can also support other undiscounted control problems. The related proved Prove2Me result for the all-proper finite-control case does not settle this mission's compact-control or improper-policy cases.

Difficulty

When every stationary policy is proper, a common weighted maximum norm makes the Bellman mapping contract. An improper policy can destroy this route: Figure 2 has an absorbing destination and satisfies both assumptions, yet $T(0,x_2)=(0,\min\{1+x_2,2\})$ is not a contraction in any norm on $X$. The main result therefore needs a way to retain fixed-point uniqueness and convergence without a uniform contraction rate. Compactness matters because a sequence of proper selectors may converge to an improper selector; Lemma 3 explains the associated cost behavior. Bertsekas and Tsitsiklis (1991), pp. 585–586, 591–595.

Formalization scope

States are Fin n, with the paper's state $1$ represented by 0; the model requires $n\ge1$. A control set $U(i)$ is a type with a metric, with compactness asserted for its whole carrier. Transition rows explicitly have nonnegative entries summing to one. These are the probability-vector conditions implicit in the word “probability.” Assumption 1 supplies a selector and therefore nonempty control sets. The paper writes $T:\mathbb R^n\to\mathbb R^n$; where a theorem uses only Assumption 1, finite real Bellman infima are made explicit through TRealValued. Under Assumption 2, compactness and lower semicontinuity give real attained minima. Bertsekas and Tsitsiklis (1991), pp. 582–584.

Policy costs and their infimum use extended reals so that an improper policy's $+\infty$ cost is represented without a default finite value. Proposition 2 concludes, rather than assumes, that $x^*$ has real coordinates. Its policy infimum ranges over every sequence of selectors. Matrix products use the identity at time zero; $T^0$ is the identity. The destination-zero restriction is retained in every fixed-point and iteration claim. Defining optimal cost as a Bellman fixed point, or restricting the infimum to stationary policies, would remove the result the paper proves. Solvers can contribute the finite-chain, matrix-inverse, semicontinuity, and convergence arguments needed by these targets.

Selected references

• Dimitri P. Bertsekas and John N. Tsitsiklis, An Analysis of Stochastic Shortest Path Problems, Mathematics of Operations Research 16(3), 580–595, 1991. DOI.