Optimization

Motivation

Stochastic gradient descent (SGD) is the default method for minimizing an expected loss $F(w)=\mathbb E_z[\ell(w,z)]$ when only noisy gradients are available, which is the situation of nearly every large-scale learning problem. When $F$ is strongly convex (for instance, any convex loss with an $\ell_2$ regularizer), information-theoretic lower bounds show that no method using $T$ noisy gradients can guarantee an error better than order $1/T$, and some algorithms achieve this rate.

For plain SGD with step sizes $\eta_t=1/(\lambda t)$ and the standard averaged output, however, the classical analysis gives only $O(\log T/T)$. Rakhlin, Shamir and Sridharan (arXiv:1109.5647, ICML 2012) showed that the logarithm is real for full averaging on non-smooth problems, and that a minimal change to the output, averaging only the last fraction $\alpha$ of the iterates, restores the optimal $O(1/T)$ rate. This mission formalizes that positive result, the paper's main theorem.

Timeline of the relevant results:

• 2007. Hazan, Agarwal and Kale (Machine Learning 69) prove an $O(\log T)$ regret bound for online gradient descent on strongly convex losses, which by online-to-batch conversion gives $O(\log T/T)$ for averaged SGD.
• 2009. Nemirovski, Juditsky, Lan and Shapiro (SIAM J. Optim. 19) show an $O(1/T)$ rate for the last SGD iterate when $F$ is in addition smooth.
• 2011. Hazan and Kale (COLT 2011) obtain $O(1/T)$ for non-smooth strongly convex problems with a different, epoch-based algorithm.
• 2012. Rakhlin, Shamir and Sridharan prove that SGD with full averaging can suffer $\Omega(\log T/T)$, and that α-suffix averaging achieves $O(1/T)$ (Theorem 5).

Setting

Let $W\subseteq\mathbb R^d$ be a closed convex set containing $0$, and let $F:\mathbb R^d\to\mathbb R$. The function $F$ is $\lambda$-strongly convex on $W$ ($\lambda>0$) if

$$F(\theta x+(1-\theta)y)\le\theta F(x)+(1-\theta)F(y)-\tfrac\lambda2\theta(1-\theta)\|x-y\|^2\qquad(x,y\in W,\ \theta\in[0,1]).$$

A point $w^*\in W$ is a minimizer of $F$ over $W$.

Information about $F$ comes from a stochastic gradient oracle $g(w,z)$: at a query point $w$, a sample $z\sim D$ is drawn and $\hat g=g(w,z)$ is returned. The oracle is unbiased in the sense that its mean $\bar g(w)=\mathbb E_{z\sim D}\,g(w,z)$ is a subgradient of $F$ relative to $W$: $F(u)\ge F(w)+\langle u-w,\bar g(w)\rangle$ for all $u\in W$. Its second moment is bounded: $\mathbb E_z\|g(w,z)\|^2\le G^2$ at every $w\in W$.

Projected SGD with step sizes $\eta_t=1/(\lambda t)$ runs on an i.i.d. sample $z_1,\dots,z_T\sim D$:

$$w_1=0,\qquad w_{t+1}=\Pi_W\big(w_t-\eta_t\,g(w_t,z_t)\big),$$

where $\Pi_W$ is the Euclidean projection onto $W$. For $\alpha\in(0,1)$ with $(1-\alpha)T$ an integer, the α-suffix average is

$$\bar w^\alpha_T=\frac{w_{(1-\alpha)T+1}+\dots+w_T}{\alpha T}.$$

In Lean the iterates are UnderstandingML.sgdStrongIterates lam W g S, the oracle mean is oracleMean D g, the suffix average is suffixAverage lam W g S k with $k=(1-\alpha)T$, and expectations are integrals against the product law UnderstandingML.iidLaw D T.

Formalization targets

Goal: Theorem 5

$$\mathbb E\big[F(\bar w^\alpha_T)-F(w^*)\big]\ \le\ \frac{2+2.5\log\frac1{1-\alpha}}{\alpha}\cdot\frac{G^2}{\lambda T},$$

together with the finiteness of $\mathbb E\,F(\bar w^\alpha_T)$. The constants are the paper's.

Milestones, in the order the proof uses them

1. Lemma 2 (p. 12): $\mathbb E_z\|g(w,z)\|^2\le G^2$ at $w\in W$ implies $\|w-w^*\|^2\le 4G^2/\lambda^2$.
2. Lemma 1 (p. 4): $\mathbb E\|w_t-w^*\|^2\le 4G^2/(\lambda^2t)$ for every $t\ge1$.
3. (3) (p. 6): $\sum_{t=k+1}^T\mathbb E\langle g_t,w_t-w^*\rangle\le\sum_{t=k+1}^T\frac{\eta_tG^2}2+\sum_{t=k+1}^T\frac{\mathbb E\|w_t-w^*\|^2-\mathbb E\|w_{t+1}-w^*\|^2}{2\eta_t}$.
4. App. B.6, convexity display (p. 18): $\sum_{t}\mathbb E\langle g_t,w_t-w^*\rangle\ge\sum_t\mathbb E[F(w_t)-F(w^*)]\ge\alpha T\,\mathbb E[F(\bar w^\alpha_T)-F(w^*)]$.
5. App. B.6, penultimate bound (p. 18): $\mathbb E[F(\bar w^\alpha_T)-F(w^*)]\le\frac{2G^2}{\alpha T\lambda}(1+H)+\frac{G^2}{2\alpha T\lambda}H$ with $H=\sum_{t=(1-\alpha)T+1}^T 1/t$.
6. App. B.6, harmonic bound (p. 18): $H\le\log\frac1{1-\alpha}$.

Significance

Theorem 5 shows that the suboptimal $\log T$ factor of averaged SGD on non-smooth strongly convex problems is an artifact of which iterates are averaged, not of the gradient steps themselves: the same iterates, averaged over a constant fraction at the end, reach the minimax-optimal $O(G^2/(\lambda T))$ rate up to constants. This matches Hazan and Kale's guarantee with an unmodified algorithm, and the same paper's lower bound shows that full averaging cannot match it.

The result is proved in the paper; nothing in it is formalized. The platform holds the Understanding Machine Learning SGD model and its $O(\log T/T)$ bound for full averaging (UnderstandingML.sgd_strongly_convex), but no $O(1/T)$ rate for SGD on a non-smooth objective. The mission produces a machine-checked proof of Theorem 5 with its explicit constants and, along the way, of Lemma 1 (the $O(1/t)$ mean-square convergence of the last iterate), which is reused by every $O(1/T)$ analysis of SGD with step sizes $1/(\lambda t)$, including the paper's smooth-case Theorems 1 and 2.

Difficulty

The obvious argument, the online-gradient-descent regret bound summed over all rounds and divided by $T$, produces $\sum_{t\le T}\eta_t G^2\approx G^2\log T/\lambda$ and so cannot avoid the logarithm. Discarding early iterates does not by itself help: the resulting bound depends on the distance $\mathbb E\|w_t-w^*\|^2$ of the iterate at which the suffix starts, at the scale $1/t$, and the regret analysis says nothing about individual iterates of a non-smooth problem.

The formal difficulties are probabilistic. The iterates are random vectors built by composing a measurable oracle with a projection defined by choice; conditioning on the past to evaluate $\mathbb E\langle g(w_t,z_t),w_t-w^*\rangle$ requires the product structure of the sample; and every expectation must be shown finite, including that of $F(\bar w^\alpha_T)$ with $F$ not assumed measurable.

Formalization scope

• Space. $\mathbb R^d$ with the Euclidean inner product (UnderstandingML.Vec d); the paper allows any Hilbert space.
• Domain. W closed and convex with 0 ∈ W (the paper's $w_1=0\in W$; closedness makes $\Pi_W$ well defined).
• Strong convexity. Mathlib's StrongConvexOn W lam F with modulus $\frac\lambda2\|x-y\|^2$, equivalent to the paper's (1) when subgradients relative to $W$ exist at every point, which the oracle provides.
• Oracle. IsSubgradientOracleOn W F D g: for $w\in W$, $g(w,\cdot)$ is integrable and its mean is a subgradient of $F$ relative to $W$. The oracle is jointly measurable and $D$ is a probability measure. The subgradient condition is not global: $F$ is only assumed convex on $W$.
• Second moment. $\int^{-}\|g(w,z)\|^2\,dD\le G^2$ at every $w\in W$ (the paper's "regardless of how the iterates evolve"). Theorem 5's statement on p. 6 prints $\mathbb E\|\hat g_t\|^2\le G$; the standing assumption on p. 3 and the proof use $G^2$, which is what is formalized.
• Indices. sgdStrongIterates … t is the paper's $w_{t+1}$; the suffix average runs over indices $k,\dots,T-1$, $k=(1-\alpha)T$, passed as a natural number with $(k:\mathbb R)=(1-\alpha)T$, which encodes that $\alpha T$ and $(1-\alpha)T$ are integers.
• Logarithm. Real.log, the natural logarithm.
• Expectations. Every Bochner integral in a conclusion is accompanied by an integrability conjunct, and nonnegative quantities in Lemma 1 are lower Lebesgue integrals, so no bound holds through Lean's default value $0$ for non-integrable functions. The bounds are stated for the expectation over $S\sim D^T$; a pathwise version, or one in which $\hat g$ itself (rather than its mean) is a subgradient, would be a different and false or easier theorem.

Infrastructure a complete development needs: measurability of the projected iterates in the sample, the one-step conditional-expectation identity $\mathbb E\langle g(w_t,z_t),w_t-w^*\rangle=\mathbb E\langle\bar g(w_t),w_t-w^*\rangle$ for the product law, and the integral comparison $\sum_{t=k+1}^T 1/t\le\log(T/k)$. The first two are reusable for the companion missions on the same paper and for any SGD analysis built on sgdStrongIterates. Proofs of any milestone, and of reusable lemmas about iidLaw and sgdStrongIterates, are welcome.

Selected references

• A. Rakhlin, O. Shamir, K. Sridharan, Making Gradient Descent Optimal for Strongly Convex Stochastic Optimization, ICML 2012; arXiv:1109.5647v7, 2012. https://arxiv.org/abs/1109.5647
• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007) 169–192. https://doi.org/10.1007/s10994-007-5016-8
• E. Hazan, S. Kale, Beyond the regret minimization barrier: an optimal algorithm for stochastic strongly-convex optimization, COLT 2011. https://proceedings.mlr.press/v19/hazan11a.html
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19 (2009) 1574–1609. https://doi.org/10.1137/070704277
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Ch. 14. https://doi.org/10.1017/CBO9781107298019

Motivation

Stochastic gradient descent (SGD) is the standard first-order method for stochastic convex optimization and for training linear predictors on large data sets: at each step it queries a noisy subgradient of the objective, takes a step against it and projects back onto the feasible set. When the objective is strongly convex, the classical online-learning analysis of SGD with step sizes $\eta_t=\Theta(1/t)$ bounds the expected suboptimality of the averaged iterate $\bar w_T=\frac1T(w_1+\dots+w_T)$ by $O(\log(T)/T)$ (Hazan, Agarwal, Kale 2007). The information-theoretically optimal rate for this problem class is $O(1/T)$, and it is attained by other algorithms (Hazan, Kale 2011; Juditsky, Nesterov 2010).

This left a concrete question: is the logarithmic factor an artifact of the analysis, or a property of SGD with averaging? Rakhlin, Shamir and Sridharan (arXiv:1109.5647v7, ICML 2012) answer it by exhibiting strongly convex problems on which averaged SGD provably loses the logarithm. The same paper shows that for objectives that are smooth at the optimum the averaged iterate attains $O(1/T)$, and that averaging only a suffix of the iterates restores $O(1/T)$ in general. This mission is the lower-bound half of that picture; the two upper bounds are sibling missions of the same series.

Setting

Points live in $\mathbb R^d$, $d\ge1$, with the Euclidean norm; for a point $w$, $w_1$ denotes its first coordinate. A stochastic gradient oracle for an objective $F$ returns, at a query point $w_t$, a random vector $\hat g_t$ whose mean is a subgradient of $F$ at $w_t$. Projected SGD on a domain $W$ with step sizes $\eta_t=c/t$, $c>0$, starts at a point $w_1\in W$ and sets

$$w_{t+1}=\Pi_W\big(w_t-\eta_t\hat g_t\big),\qquad t=1,2,\dots,$$

where $\Pi_W$ is the Euclidean projection onto $W$. The output studied here is the average $\bar w_T=\frac1T(w_1+\dots+w_T)$. Throughout, $Z_1,Z_2,\dots$ are independent random variables, each uniformly distributed on $[-1,3]$.

Example A. $W=[0,1]^d$, $F(w)=\tfrac12\|w\|^2+w_1$, and the oracle returns $\hat g_t=w_t+(Z_t,0,\dots,0)$. The global minimum over $W$ is at $w^*=0$, a corner of the box.

Example B. $W=[-1,1]^d$ and

$$F(w)=\tfrac12\|w\|^2+\begin{cases}w_1&w_1\ge0\\-7w_1&w_1<0,\end{cases}\qquad \hat g_t=w_t+\begin{cases}(Z_t,0,\dots,0)&w_{t,1}\ge0\\(-7,0,\dots,0)&w_{t,1}<0.\end{cases}$$

Here $F$ is $1$-strongly convex and non-smooth along the hyperplane $w_1=0$, and its minimizer $w^*=0$ lies in the interior of $W$. The oracle is state-dependent: which branch it uses depends on the sign of the first coordinate of the query point. In both examples $\mathbb E[\hat g_t]$ is a subgradient of $F$ at $w_t$ and $\mathbb E\|\hat g_t\|^2$ is bounded for fixed $d$.

Formalization targets

Goal: Theorem 4 (p. 5)

In Example B, for every $c>0$, every starting point $w_1\in W$ with $w_{1,1}\ge0$, $T_0=\max\{2,6c+1\}$ and every integer $T\ge T_0+2$,

$$\mathbb E\big[F(\bar w_T)-F(w^*)\big]\ \ge\ \frac{3c}{16T}\sum_{t=T_0+2}^{T}\frac1t-\frac{T_0}{T}.$$

For fixed $c$ this is $\Omega(\log(T)/T)$. The goal is the paper's statement with its constants.

Milestones

1. Theorem 3 (p. 5). In Example A, for every $c>0$, every $w_1\in W$, $T_0=\max\{2,c/2\}$ and every integer $T\ge T_0+1$,

$$\mathbb E\big[F(\bar w_T)-F(w^*)\big]\ \ge\ \frac{c}{16T}\sum_{t=T_0}^{T-1}\frac1t.$$

2. Eq. (9) (p. 16). The pathwise recursion of the first coordinate in Example B:

$$w_{t+1,1}=\Pi_{[-1,1]}\Big(\big(1-\tfrac ct\big)w_{t,1}-\begin{cases}Z_t\,c/t&w_{t,1}\ge0\\-7c/t&w_{t,1}<0\end{cases}\Big).$$

3. App. B.5, p. 17. In Example B, whenever $c/t<1$,

$$\Pr\big(w_{t,1}\notin[0,c/t]\ \big|\ w_{t-1,1}\ge0\big)\ \ge\ \tfrac34 .$$

Significance

The result. Theorem 4 shows that the $O(\log(T)/T)$ guarantee for SGD with full averaging is tight up to constants on strongly convex problems, even when the optimum is interior. It separates SGD with averaging from algorithms that reach $O(1/T)$, and it is the reason the paper introduces $\alpha$-suffix averaging. It also explains why smoothness at the optimum (the paper's §3) matters: Example B is non-smooth exactly at $w^*$.

Formalizing it. The result is proved on paper but, as far as the platform's index shows, has no machine-checked proof. Formalization adds a verified lower bound with explicit constants. It also settles the paper's own argument. The printed proof of Theorem 4 relies on Lemma 4 (p. 16), whose first claim uses $Z_t\ge-1$ where the recursion subtracts $(c/t)Z_t$ with $Z_t$ up to $3$, so Lemma 4 fails with positive probability. Theorem 4 is believed true, but a complete proof needs a repaired argument. Theorem 3's printed proof uses $\eta_t\le1$ in step (8), while $t\ge T_0$ only gives $\eta_t\le2$. Numerical checks of Theorem 3 itself found no violation.

Difficulty

An expectation lower bound on the average needs control of every iterate $w_t$, not just of the last one, and the iterates form a non-linear Markov chain because of the projection and, in Example B, because of the state-dependent oracle. Upper-bound techniques do not transfer: they bound $\mathbb E\|w_t-w^*\|^2$ from above, which says nothing about the sign of $w_{t,1}$. In Example B, the natural first idea is to argue that $w_{t,1}$ never stays negative, so that it behaves like the constrained Example A; this is the claim of the paper's Lemma 4, and as stated it does not hold, because a single noise draw near $3$ can push the first coordinate below the level the lemma asserts. A proof must handle that event with explicit constants and still produce the $T_0/T$ slack of the statement.

Formalization scope

• Space. $\mathbb R^d$ is UnderstandingML.Vec d = EuclideanSpace ℝ (Fin d) with [NeZero d]; the paper's first coordinate is index 0.
• Projection. $\Pi_W$ onto the box $[lo,hi]^d$ is coordinatewise clamping $v_i\mapsto\max\{lo,\min\{hi,v_i\}\}$, which is the Euclidean projection onto the box.
• Indexing. sgdRun … k is the paper's $w_{k+1}$; the step at index $k$ uses $\eta_{k+1}=c/(k+1)$ and the noise value $Z$ at index $k$. The starting point is arbitrary (not $0$), as in Theorems 3–4.
• Noise. Each $Z_t$ has law ProbabilityTheory.cond volume (Set.Icc (-1) 3) (uniform on $[-1,3]$); a horizon-$T$ sequence has the product law UnderstandingML.iidLaw. Expectations are Bochner integrals over it.
• Constants and ranges. $c>0$ is the only condition on $c$. $T_0$ is real; $T$ is a natural number; $\sum_{t=T_0}^{T-1}$ is over the integers $\lceil T_0\rceil\le t\le T-1$, and $\sum_{t=T_0+2}^{T}$ over $\lceil T_0\rceil+2\le t\le T$. $F(w^*)$ is written $F(0)$.
• No junk integrals. Theorems 3 and 4 also assert integrability of $F(\bar w_T)-F(0)$, so the inequality cannot hold because an integral defaulted to $0$. The probability milestone is stated multiplicatively, $\Pr(A\cap B)\ge\frac34\Pr(B)$, rather than through ProbabilityTheory.cond, which would be the zero measure on a null conditioning event.
• Not trivializable. The examples (the constant $7$, the noise interval $[-1,3]$, the boxes $[0,1]^d$, $[-1,1]^d$) are fixed by the paper; replacing the oracle or the domain is a different theorem. Since $F(\bar w_T)\ge F(0)$ always, Theorem 4 is immediate whenever its right-hand side is negative, but it is a non-trivial inequality for large $T$, and the statement quantifies over all $T\ge T_0+2$.
• Not posed. Lemma 4 (false as stated), step (8) of App. B.4, and Eq. (10) with the displays after it in App. B.5 (they depend on Lemma 4).
• Infrastructure. Measurability of the SGD run in the noise sequence, independence of $Z_t$ from the past iterates under the product law, and probabilities of intervals under the uniform law are reusable for any analysis of SGD on explicit examples. Proofs of the milestones, a repaired proof of Lemma 4's role, and a complete proof of Theorem 4 are all welcome.

Selected references

• A. Rakhlin, O. Shamir, K. Sridharan, Making Gradient Descent Optimal for Strongly Convex Stochastic Optimization, ICML 2012; arXiv:1109.5647v7, 2012. https://arxiv.org/abs/1109.5647v7
• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69, 2007. https://doi.org/10.1007/s10994-007-5016-8
• E. Hazan, S. Kale, Beyond the regret minimization barrier: an optimal algorithm for stochastic strongly-convex optimization, COLT 2011. https://proceedings.mlr.press/v19/hazan11a.html
• A. Juditsky, Y. Nesterov, Primal-dual subgradient methods for minimizing uniformly convex functions, 2010. https://hal.science/hal-00508933
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19(4), 2009. https://doi.org/10.1137/070704277

Motivation

Interior-point methods solve linear, second-order cone and semidefinite programs in polynomial time, and they are the engine of most conic optimization software. The general theory of Nesterov and Nemirovskii (1994) covers any convex cone with a self-concordant barrier, but its methods are essentially primal and short-step: their analysis controls the barrier only inside a unit Dikin ellipsoid around the current point. Practical codes for linear programming, in contrast, use symmetric primal-dual methods that take long steps, a large fraction of the way to the boundary.

Nesterov and Todd (1997) isolated the class of cones and barriers for which the primal-dual long-step theory of linear programming carries over: self-scaled cones with self-scaled barriers. The class contains the nonnegative orthant, the second-order cone and the cone of positive semidefinite matrices, and their products. This mission formalizes the paper's §8 result: a primal-dual potential-reduction method with joint scaling decreases a symmetric potential function by an absolute constant at every iteration, which yields an $O(\sqrt\nu\ln(1/\epsilon))$ iteration bound.

Timeline. Todd and Ye (1990) introduced the symmetric primal-dual potential function for linear programming with a short-step method. Kojima, Mizuno and Yoshise (1991) gave a symmetric long-step primal-dual potential-reduction method for linear complementarity problems; their Lemma 2.5 is the linear-programming case of the key inequality posed here. Nesterov and Nemirovskii (1994, §4.5) extended Ye's non-symmetric method to general cones. Nesterov and Todd (1997) extended the method of Kojima et al. to self-scaled cones; the companion paper (1998) treats short-step and functional-proximity variants.

Setting

Let $E$ be a finite-dimensional real vector space with dual $E^*$ and pairing $\langle s,x\rangle$. Let $K\subset E$ be a proper cone: closed, convex, with nonempty interior, and pointed (it contains no line). Its dual cone is $K^*=\{s:\langle s,x\rangle\ge0\ \forall x\in K\}$.

A $\nu$-self-concordant logarithmically homogeneous barrier for $K$ is a convex $C^3$ function $F$ on $\operatorname{int}K$ that tends to $+\infty$ at the boundary, satisfies the self-concordance inequality $|F'''(x)[h,h,h]|\le2\langle F''(x)h,h\rangle^{3/2}$, the bound $\langle F'(x),h\rangle^2\le\nu\langle F''(x)h,h\rangle$, and $F(\tau x)=F(x)-\nu\ln\tau$ for $\tau>0$. Its conjugate barrier is

$$F_*(s)=\max\{-\langle s,x\rangle-F(x):x\in\operatorname{int}K\},\qquad s\in\operatorname{int}K^*.$$

$F$ is $\nu$-self-scaled (Definition 2.1) if for all $v,x\in\operatorname{int}K$, $F''(v)x\in\operatorname{int}K^*$ and $F_*(F''(v)x)=F(x)-2F(v)-\nu$. For $x\in\operatorname{int}K$, $s\in\operatorname{int}K^*$ the scaling point is the $w\in\operatorname{int}K$ with $F''(w)x=s$.

The distance to the boundary is measured by

$$\sigma_x(p)=\min\{\beta\ge0:\beta x-p\in K\},\qquad\sigma^*_s(q)=\min\{\beta\ge0:\beta s-q\in K^*\},$$

so $x-\alpha p\in\operatorname{int}K$ for $\alpha\in[0,1/\sigma_x(p))$; local norms are $\|p\|_x=\langle F''(x)p,p\rangle^{1/2}$.

The problem is the primal-dual pair $\min\{\langle c,x\rangle:Ax=b,\ x\in K\}$, $\max\{\langle b,y\rangle:A^*y+s=c,\ s\in K^*\}$ with $A$ surjective. For $\rho\ge\sqrt\nu$ the primal-dual potential is

$$\phi(x,s)=(\nu+\rho)\ln\langle s,x\rangle+F(x)+F_*(s).$$

One iteration from a strictly feasible $(x,y,s)$: take the scaling point $w$ and $\sigma=\sigma_x(w)$; solve

$$F''(w)\Delta x+\Delta s=\tfrac{\nu+\rho}{\langle s,x\rangle}s+F'(x),\qquad A\Delta x=0,\qquad A^*\Delta y+\Delta s=0;\qquad(8.1)$$

put $\bar\sigma=\max\{\sigma_x(\Delta x),\sigma^*_s(\Delta s)\}$, $\bar\alpha=1/(\sigma^2+\bar\sigma)$, and accept any $\alpha$ with $\phi(x-\alpha\Delta x,s-\alpha\Delta s)\le\phi(x-\bar\alpha\Delta x,s-\bar\alpha\Delta s)$.

Formalization targets

Goal: Theorem 8.2

$$\phi(x-\bar\alpha\Delta x,\,s-\bar\alpha\Delta s)\le\phi(x,s)-\frac{\sqrt3}{2}+\ln\Big(1+\frac{\sqrt3}{2}\Big),$$

with $x-\bar\alpha\Delta x\in\operatorname{int}K$ and $s-\bar\alpha\Delta s\in\operatorname{int}K^*$, and the same bound for every accepted step $\alpha$, whose iterate is again strictly feasible. The constant $\sqrt3/2-\ln(1+\sqrt3/2)\approx0.243$ is the paper's.

Milestones

In attack order: the structure of Hessians (Theorem 3.1), existence and uniqueness of scaling points (Theorem 3.2), convexity of $-\langle F'(\cdot),v\rangle$ (Lemma 3.1) and the third-derivative bounds (Corollary 3.2 (i)–(ii)); the long-step Hessian comparison (Theorem 4.1), its corollaries (Corollary 4.1 (i)–(ii)), the barrier estimate (4.8) (Theorem 4.2) and the scalar monotonicity facts (Proposition 4.1); separability along orthogonal boundary directions (Lemma 5.1, Theorem 5.1) and the key inequality

$$\langle F'(x),F_*'(s)\rangle\ge\frac{\nu(\nu-1)}{\langle s,x\rangle}+\frac34\sigma_x^2(w)\qquad(\text{Theorem 5.2});$$

and unique solvability of the projection system (Proposition 6.1).

Significance

A constant decrease of $\phi$ per iteration gives, through the bound of Nesterov–Nemirovskii (Theorem 8.1 of the paper), primal and dual solutions within $\epsilon$ of optimal in $O(\sqrt\nu\ln(1/\epsilon))$ iterations when $\rho=\gamma\sqrt\nu$, with step sizes that are long (a fixed fraction of the distance to the boundary) rather than confined to a Dikin ellipsoid. Theorems 4.1–4.2 and 5.2 are reused by the potential-reduction and path-following analyses of the same paper and by later work on symmetric cones.

The results are proved in the paper. They are not formalized anywhere known to us: Mathlib has no self-concordant barriers, and the platform has the definitions of self-scaled barriers (from the companion 1998 paper) but none of these theorems. The mission produces machine-checked versions of the paper's structure theory of self-scaled barriers (§§3–5) and of the per-iteration decrease of its primal-dual method.

Difficulty

The obvious attempt bounds the change of $F$ and $F_*$ along the step by self-concordance alone. Self-concordance controls $F''(x-\alpha p)$ only for $\|\alpha p\|_x<1$, so it cannot certify a step of length $\bar\alpha$, which may be far outside the Dikin ellipsoid. The long-step analysis needs Theorem 4.1, which compares Hessians all the way to the boundary and holds for self-scaled barriers but fails for general self-concordant ones. The constant decrease then needs a lower bound on $\mu/\sigma$, where $\mu$ is the scaled norm of the right-hand side of (8.1); that bound is Theorem 5.2, whose proof rests on the separability of $F$ along orthogonal boundary directions (Theorem 5.1), a structural property with no analogue for general barriers.

Formalization scope

• Spaces. $E=E^*=\mathbb R^n$ and $Y=Y^*=\mathbb R^m$ (EuclideanSpace), identified through the inner product; $A^*$ is ContinuousLinearMap.adjoint A. $F''$ is hess F (derivative of gradient F), $F'''(x)[u]$ is fderiv ℝ (hess F) x u, $[F''(v)]^{-1}$ is ContinuousLinearMap.inverse.
• Published setting reused. IsProperCone, IsSelfScaledBarrier, conj, IsScalingPoint, IsPrimalStrict, IsDualStrict, sigma, lnorm (SelfScaledIPM.ShortStep), and ConvexOptimization.dualCone. The barrier definition includes nondegeneracy of $F''$ on $\operatorname{int}K$, which follows from the other axioms for a pointed cone. conj K F is a supremum over $\operatorname{int}K$ and is only evaluated at points of $\operatorname{int}K^*$. $\sigma$ is an infimum, equal to the page's minimum at interior centres.
• Standing binders. Every theorem except Proposition 4.1 assumes IsProperCone K, IsSelfScaledBarrier K F ν and $\nu\ge1$; the paper derives $\nu\ge1$ from pointedness.
• Conventions. Operator inequalities are quadratic-form inequalities. Step ranges $\alpha\in[0,1/\sigma_x(p))$ are encoded as $0\le\alpha$, $\alpha\sigma_x(p)<1$. Scaling points and search directions are data satisfying their equations; their existence is Theorem 3.2 and Proposition 6.1. "Monotonically" in Proposition 4.1 is read strictly.
• Goal form. Theorem 8.2 is stated for one iteration from any strictly feasible pair. It asserts that the $\bar\alpha$-step is strictly interior and achieves the bound. Without that clause, a goal asserting the bound only for steps accepted by rule (c) would be vacuous whenever no step is accepted, since $F_*$ and $\ln$ take junk values off their domains.
• New definitions (SelfScaledLongStep.PrimalDual.Defs): the projection system (6.4), the potential $\phi$, the system (8.1), $\bar\sigma$ and $\bar\alpha$. The projection system is shared, under the same name, with the other missions of this series.
• Contributions welcome: calculus of self-concordant barriers on cones (C³ smoothness, logarithmic homogeneity identities, Legendre duality between $F$ and $F_*$), which is reusable for any interior-point formalization; proofs of the milestones in any order.

Selected references

• Yu. E. Nesterov and M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Mathematics of Operations Research 22(1), 1997, 1–42. https://doi.org/10.1287/moor.22.1.1
• Yu. E. Nesterov and M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM Journal on Optimization 8(2), 1998, 324–364. https://doi.org/10.1137/S1052623495290209
• Yu. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
• M. Kojima, S. Mizuno and A. Yoshise, An $O(\sqrt n L)$ iteration potential reduction algorithm for linear complementarity problems, Mathematical Programming 50, 1991, 331–342. https://doi.org/10.1007/BF01594942
• M. J. Todd and Y. Ye, A centered projective algorithm for linear programming, Mathematics of Operations Research 15(3), 1990, 508–529. https://doi.org/10.1287/moor.15.3.508

Motivation

Periodic-review inventory models with a fixed ordering cost are the setting in which the $(s,S)$ policy is optimal: when the stock falls below a reorder point $s$, order up to a level $S$, otherwise order nothing. Scarf (1960) proved this for independent demands over a finite horizon by introducing $K$-convexity, and Iglehart (1963) extended it to the discounted infinite horizon. In practice the demand distribution changes with an exogenous environment: the economy, the season, the stage of a product's life cycle. Song and Zipkin (Oper. Res. 41(2), 1993) modelled this environment as a Markov chain of demand states in continuous time with Poisson demand.

Sethi and Cheng (Oper. Res. 45(6), 1997) treat the discrete-time version with general demand densities, nonstationary costs and convex surplus costs of linear growth. The companion mission (I) covers their finite-horizon result, Theorem 4.1. This mission covers the nonstationary discounted infinite-horizon result, Theorem 6.2, together with the existence theory (Theorem 6.1, proved in the paper's Appendix) on which it rests.

Setting

Demand states form the finite set $I = \{1,\dots,L\}$ and follow a Markov chain with transition matrix $P = (p_{ij})$. In period $k = 0,1,2,\dots$ the demand $\xi_k \ge 0$ has the conditional density $\varphi_{i,k}$ given $i_k = i$, with mean at most $M$. Orders are placed at the start of a period and delivered at once, and unmet demand is backlogged, so the surplus evolves by $x_{k+1} = x_k + u_k - \xi_k$ (2.4). Ordering $u \ge 0$ costs $c_k(i,u) = K^i_k\,\delta(u) + c^i_k u$ with $K^i_k, c^i_k \ge 0$ (2.1), where $\delta(z) = 1$ for $z > 0$ and $0$ otherwise. The surplus cost $f_k(i,\cdot)$ is convex and nonnegative, vanishes at $0$, and satisfies $f_k(i,x) \le C(1+|x|)$ (2.2).

An admissible policy $U$ chooses each order $u_k \ge 0$ as a measurable function of the past demand states and demands. With a discount factor $\alpha$, the objective from period $n$, state $i$ and surplus $x$ is

$$J_n(i,x;U) = \sum_{k=n}^{\infty} \alpha^{k-n}\,E\big[c_k(i_k,u_k) + f_k(i_k,x_k)\big], \tag{6.1}$$

and the value function is $v_n(i,x) = \inf_U J_n(i,x;U)$. With $F_{n+1}(b)(i,y) = \sum_j p_{ij}\int_0^\infty b(j,y-z)\,\varphi_{i,n}(z)\,dz$ (3.1), the dynamic programming equations are

$$v_n(i,x) = f_n(i,x) + \inf_{u\ge0}\big\{c_n(i,u) + \alpha F_{n+1}(v_{n+1})(i,x+u)\big\}, \qquad n = 0,1,2,\dots \tag{6.2}$$

The truncations $J_{n,k}$ keep the first $k$ periods of (6.1) (6.3), their values are $v_{n,k}$ (6.4), and $w_n = J_n(\cdot;\mathbf 0)$ is the cost of never ordering (6.6). The function classes are $B_0$ (nonnegative pointwise limits of continuous functions), $B_1$ (those of linear growth) and $C_1$ (those also uniformly continuous in $x$). A function $g$ is $K$-convex if $K + g(z+y) \ge g(y) + z\,(g(y)-g(y-b))/b$ for all $z \ge 0$, $b > 0$ (4.3). Assumption (4.1) asks $K^i_n \ge \sum_j p_{ij}K^j_{n+1} \ge 0$, and (4.2) asks $c^i_n x + F_{n+1}(f_{n+1})(i,x) \to +\infty$ as $x \to \infty$.

Formalization targets

Goal: Theorem 6.2

Under (2.1), (2.2), (4.1), (4.2) and $0 < \alpha < 1$, there are $s^i_n \le S^i_n$ in $[-\infty,\infty)$ such that

$$\hat u_n(i,x) = (S^i_n - x)\,\delta(s^i_n - x)$$

attains the infimum in (6.2) at every $(n,i,x)$, and its feedback policy, started at any period $n$ and surplus $x$, has cost $J_n(i,x;\hat U) = v_n(i,x)$: it is optimal among all history-dependent policies.

Milestones

1. The order-nothing cost $w_n$ is finite, lies in $C_1$, and is the unique $C_1$ solution of $w_n = f_n + \alpha F_{n+1}(w_{n+1})$ (6.7).
2. The truncated values solve the dynamic programming equations (6.5), $v_{n,0} = 0$, $v_{n,k} \in C_1$, and under (4.2) the infimum in (6.4) is attained.
3. Theorem 6.1, (6.8): $0 = v_{n,0} \le v_{n,1} \le \cdots \le v_{n,k} \le w_n$.
4. Appendix: $|v_{n,k}(i,x') - v_{n,k}(i,x)| \le C|x'-x|/(1-\alpha)$, and the same for $v_n = \lim_k v_{n,k}$.
5. Theorem 6.1, (6.9): $v_{n,k} \uparrow v_n$, a solution of (6.2) in $B_1$.
6. Theorem 6.1, (6.10): $v_n \in C_1$, a $B_0$ minimizer $\hat U$ of (6.2) exists, and every such $\hat U$ is optimal: $v_n(i,x) = \min_U J_n(i,x;U) = J_n(i,x;\hat U)$.
7. Proof of Theorem 6.2: $v_{n,k}(i,\cdot)$ is $K^i_n$-convex.
8. Proof of Theorem 6.2: $v_n(i,\cdot)$ is $K^i_n$-convex.

The structural lemma behind the step from $K$-convexity to the $(s,S)$ form, Proposition 4.2 of the paper (an extension of Bertsekas' lemma to lower semicontinuous functions coercive only at $+\infty$, with possibly infinite $s$, $S$), is posed in the companion finite-horizon mission and is not repeated here.

Significance

Theorem 6.2 says that the classical $(s,S)$ structure survives two generalizations at once: demand driven by a Markov environment, and nonstationary data over an infinite horizon. The two levels may depend on the period and on the current demand state, so only $2L$ numbers per period describe an optimal policy, and with cyclic demand only $L$ pairs are needed (Corollary 7.1 of the paper). Theorem 6.1 is a self-contained existence result for a positive-cost, unbounded-state dynamic program: value iteration from zero converges to the value function, which solves the optimality equation, and any measurable minimizer is optimal among history-dependent policies.

The results are proved in the paper, with the finite-horizon existence theory delegated to Beyer, Sethi and Taksar (1998). No machine-checked proof of any of them is known. The platform has $K$-convexity (BertsekasKConvex) and the $(s,S)$ structure lemma of Bertsekas for continuous functions coercive at both ends; it has no discounted infinite-horizon $(s,S)$ theorem with Markov-modulated demand. The related posed items SongZipkinFluct.FixedCost.theorem5e_theorem6 and theorem5ab concern the Song–Zipkin model (continuous time, Poisson demand, integer levels, stationary data), a different model.

Difficulty

The obvious argument is "the finite-horizon value functions are $K$-convex, so their limit is, and a minimizer of a $K$-convex optimality equation is $(s,S)$". Three steps of it fail as stated.

First, the limit of value iteration need not be the value function, nor solve (6.2), in a positive-cost problem with unbounded actions: exchanging $\lim_k$ with $\inf_u$ requires the minimizers of the truncated problems to stay in a compact set uniformly in $k$, and that bound is where the coercivity assumption (4.2) enters. Second, optimality against history-dependent policies, not only Markov ones, requires a verification argument along histories of states and demands. Third, the functions $z_n(i,y) = c^i_n y + \alpha F_{n+1}(v_{n+1})(i,y)$ may be unbounded below, in which case the reorder level is $s = -\infty$ and the order-up-to level does not exist; the goal allows this case.

Formalization scope

The Lean development (namespace SethiChengSS.Infinite) commits to the following.

• Demand states are Fin L; periods are natural numbers with the paper's base $0$.
• Expectations are sums over state paths of Lebesgue integrals against the product weight $\prod_t p_{i_t i_{t+1}}\varphi_{i_t,t}(\xi_t)$, valued in $[0,\infty]$. This builds in the conditional independence of $\xi_k$ and $i_{k+1}$ given $i_k$ that (3.1) uses.
• A policy is a function of the state history and the past demands; admissible means nonnegative and measurable in the demands. The comparison class is never restricted to Markov policies.
• $J_n$ (6.1) is the supremum over $k$ of the truncations $J_{n,k}$ (6.3), which equals the series because all costs are nonnegative.
• $F_{n+1}$ uses the Bochner integral, which is $0$ on non-integrable integrands; the $C_1$ conclusions are what make it genuine.
• The levels $s$, $S$ are extended reals with $s \le S$, $S \ne +\infty$, and $S$ real whenever $s$ is (Remark 4.4).

Pins. The paper prints $0 < \alpha \le 1$; the mission assumes $0 < \alpha < 1$, since $w_n$ is infinite at $\alpha = 1$ and the Appendix divides by $1-\alpha$. Theorem 6.2 is printed without (4.1), which its proof uses through the induction of Section 4; (4.1) is assumed for every period. Theorem 6.1 is printed under (2.1)–(2.2) only, but attainment in (6.2) can fail without coercivity and the Appendix bound (A.3) divides by $c^i_n$; (4.2) is added to (6.9), (6.10) and to the attainment clause of (6.5). "In class $C_1$" for the sequence $w_n$ is read with one growth constant for all periods. The boundary condition "$v_{n+k,0} = 0$" of (6.5) is read as $v_{n,0} = 0$, as the next sentence of the paper states.

The goal cannot be met by a degenerate encoding: the value function is the infimum over all admissible history-dependent policies (not the solution of (6.2) by definition), the demand data must be genuine probability densities with bounded mean, and the levels may not be $S = +\infty$.

A complete development needs: monotone convergence for the path-measure costs, measurable selection of minimizers, the $K$-convexity closure properties (Proposition 4.1 of the paper; several are proved on the platform as BertsekasDP.kconvex_*), and Proposition 4.2. The model file and the infinite-horizon verification argument are reusable for other Markov-modulated inventory models. Contributions toward any milestone, or toward general lemmas on positive-cost dynamic programs, are welcome.

Selected references

• S. P. Sethi and F. Cheng, Optimality of (s, S) policies in inventory models with Markovian demand, Operations Research 45(6), 931–939, 1997. https://doi.org/10.1287/opre.45.6.931
• J.-S. Song and P. Zipkin, Inventory control in a fluctuating demand environment, Operations Research 41(2), 351–370, 1993. https://doi.org/10.1287/opre.41.2.351
• H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• D. L. Iglehart, Optimality of (s, S) policies in the infinite horizon dynamic inventory problem, Management Science 9(2), 259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• D. P. Bertsekas, Dynamic Programming and Stochastic Control, Academic Press, 1976.
• A. Bensoussan, M. Crouhy and J.-M. Proth, Mathematical Theory of Production Planning, North-Holland, 1983.
• D. Beyer, S. P. Sethi and M. Taksar, Inventory models with Markovian demands and cost functions of polynomial growth, Journal of Optimization Theory and Applications 98, 1998 (cited by Sethi and Cheng as forthcoming).

Linear decision rules for stochastic programs with random recourse

In a one-stage stochastic program a decision maker observes a random outcome $\xi$ and then picks a decision $x(\xi)$, subject to constraints that depend on $\xi$, so as to minimize expected cost. The optimization variable is a whole function $x$, and computing the optimal value is #P-hard even for a uniform distribution on the unit cube (Dyer and Stougie, 2006, cited in the paper as [16, Theorem 3.2]). A standard tractable approximation, introduced for robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004) and carried to stochastic programming by Shapiro–Nemirovski and Chen–Sim–Sun, restricts decisions to linear decision rules $x(\xi)=X\xi$. This restriction gives an upper bound on the optimal value.

Kuhn, Wiesemann and Georghiou (2009/2011) study these approximations systematically. Their §3 treats the case where the constraint matrix itself depends on $\xi$ (random recourse). Linear decisions then produce constraints that are quadratic in $\xi$, and the paper reformulates the resulting semi-infinite problem as a semidefinite program. This mission formalizes that reformulation, the primal half of the paper's Theorem 2.

Setting

Uncertainty is a probability measure $\mathbb P$ on $\mathbb R^k$, with outcomes $\xi$. The support $\Xi$ of $\mathbb P$ is the smallest closed set of probability one. It is assumed to have the form

$$\Xi=\{\xi\in\mathbb R^k:\ e_1^\top\xi=1,\ \ \xi^\top W_\ell\xi\ge0,\ \ell=1,\dots,l\}\qquad(3.11)$$

for symmetric matrices $W_1,\dots,W_l$, where $e_1$ is the first standard basis vector. The first coordinate of every outcome is therefore $1$, so linear functions of $\xi$ are affine functions of the remaining coordinates. $\Xi$ is assumed nonempty and bounded, and its linear hull is assumed to be $\mathbb R^k$. Let $\mathbb S$ denote the symmetric $k\times k$ matrices and $M=\mathbb E(\xi\xi^\top)$ the second-moment matrix.

The data are $C\in\mathbb R^{n\times k}$ (cost $c(\xi)=C\xi$), $B\in\mathbb R^{m\times k}$ (right-hand side $b(\xi)=B\xi$, with rows $b_\mu^\top$), and $A_1,\dots,A_m\in\mathbb R^{k\times n}$, where the $\mu$th row of the recourse matrix $A(\xi)$ is $\xi^\top A_\mu$. The stochastic program $\mathcal{SP}$ minimizes $\mathbb E(c(\xi)^\top x(\xi))$ over square-integrable $x$ subject to $A(\xi)x(\xi)\le b(\xi)$ almost surely. It is strictly feasible if some square-integrable $\bar x,\bar s$ and some $\varepsilon>0$ satisfy $A(\xi)\bar x(\xi)+\bar s(\xi)=b(\xi)$ and $\bar s(\xi)\ge\varepsilon e$ almost surely.

With linear decisions $X\xi$ and quadratic slacks $\xi^\top S_\mu\xi$, $S_\mu\in\mathbb S$, one obtains the primal approximation

$$\mathcal{SP}^u:\quad \min\ \operatorname{Tr}(MC^\top X)\ \ \text{s.t.}\ \ \xi^\top A_\mu X\xi+\xi^\top S_\mu\xi=b_\mu^\top\xi,\ \ \xi^\top S_\mu\xi\ge0\ \ \mathbb P\text{-a.s.},\ \mu=1,\dots,m,$$

and the SDP (3.14)

$$\min\ \operatorname{Tr}(MC^\top X)\ \ \text{s.t.}\ \ \tfrac12(A_\mu X+X^\top A_\mu^\top)+S_\mu=\tfrac12(e_1b_\mu^\top+b_\mu e_1^\top),\ \ S_\mu-\textstyle\sum_\ell\Lambda_{\mu\ell}W_\ell\succeq0,\ \ \Lambda\ge0 .$$

Formalization targets

Goal: Theorem 2, primal half (p. 17)

$$\operatorname{Feas}(3.14)\ \text{projects into}\ \operatorname{Feas}\mathcal{SP}^u,\qquad \operatorname{val}\mathcal{SP}^u\le\operatorname{val}(3.14),$$ $$l=1\ \text{and}\ \mathcal{SP}\ \text{strictly feasible}\ \Longrightarrow\ \operatorname{val}\mathcal{SP}^u=\operatorname{val}(3.14).$$

Milestones

1. §3.2, (3.13), p. 12. The $\mu$th equality constraint of $\mathcal{SP}^u$ holds almost surely if and only if $H_\mu:=\tfrac12(A_\mu X+X^\top A_\mu^\top-e_1b_\mu^\top-b_\mu e_1^\top)+S_\mu=0$.
2. Lemma 1 (S-lemma), p. 12. If $\bar\xi^\top W\bar\xi>0$ for some $\bar\xi$, then $[\xi^\top W\xi\ge0\Rightarrow\xi^\top S\xi\ge0]\iff\exists\lambda\ge0:\ S\succeq\lambda W$. This is linked to the platform's proved S-procedure, of which it is the homogeneous case.
3. Proposition 6, p. 12. For symmetric $S$: $\exists\lambda\ge0$ with $S-\sum_\ell\lambda_\ell W_\ell\succeq0$ implies $\xi^\top S\xi\ge0$ almost surely, and the converse holds when $l=1$.

Significance

The theorem replaces a problem with infinitely many constraints, one per outcome, by a semidefinite program with $O(mk^2+ml)$ variables. Its value is always an upper bound on $\mathcal{SP}^u$, and hence on $\mathcal{SP}$. When the support is a single ellipsoid in the hyperplane $e_1^\top\xi=1$ ($l=1$), the bound loses nothing beyond the restriction to linear decisions. For $l>1$ the gap is unavoidable in general: an exact tractable reformulation would decide copositivity, which is NP-hard (Remark 7). Random recourse arises whenever technology or yield coefficients are uncertain, for example in production planning and portfolio problems with uncertain returns.

The result is proved in the paper. As far as is known it has no machine-checked proof. A formalization adds a precise statement of the hypotheses. Writing those hypotheses out showed that the unnumbered §3.2 step needs $\Xi$ to have dimension $k-1$, which spanning alone does not give for nonconvex $\Xi$ (see Formalization scope). The other half of Theorem 2, about the lower-bounding SDP (3.18), is false in this preprint and is not part of the mission.

Difficulty

The semi-infinite constraints hold only $\mathbb P$-almost surely. The first step is to pass from "almost surely" to "for every $\xi\in\Xi$", which uses that $\Xi$ is exactly the support and that the constraint functions are continuous. A bound $\mathbb P(\Xi)=1$ alone is not enough. For the equality constraints, a quadratic form that vanishes on $\Xi$ must vanish identically. This requires $\Xi$ to be large enough, and the obvious argument from "$\Xi$ spans $\mathbb R^k$" fails when $\Xi$ is a finite set. For the inequality constraints with $l=1$, the implication $\xi^\top W_1\xi\ge0\Rightarrow\xi^\top S\xi\ge0$ must be established on all of $\mathbb R^k$ and not only on the slice $e_1^\top\xi=1$. Doing so needs boundedness of $\Xi$ (no recession directions) and a strictly feasible point for the S-lemma. The S-lemma itself is a nonconvex duality statement. It is available on the platform.

Formalization scope

Outcomes live in Fin k → ℝ, with $k\ge1$ carried in the setting. Indices are 0-based: $\xi_1$ is coordinate 0, and $\mu,\ell$ range over Fin m, Fin l. "$\Xi$ is the support of $\mathbb P$" is stated as: $\Xi$ is closed, $\mathbb P(\Xi^{\mathrm c})=0$, and every ball centred in $\Xi$ has positive measure. Mathlib has no Measure.support at this revision. The standing assumptions (probability measure, symmetric $W_\ell$, support, nonempty, bounded, spanning) form one predicate assumed by every theorem. Decision rules are Borel measurable square-integrable functions. Optimal values are infima in EReal, $+\infty$ for an empty feasible set and $-\infty$ for an unbounded one. "Equivalent" means equal optimal values. Each $S_\mu$ is required symmetric in both problems; $\succeq$ is positive semidefiniteness and $\Lambda\ge0$ is componentwise. Strict feasibility of $\mathcal{SP}$ in §3 is the paper's condition (2.9) of §2 with $A$ replaced by $A(\xi)$. The paper uses the phrase without restating it.

Repairs and narrowings:

• Only the clauses of Theorem 2 about (3.14) and $\mathcal{SP}^u$ are stated. The clauses about (3.18) and $\mathcal{SP}^l$ are false in this preprint: a strictly feasible instance with $l=1$ has $\operatorname{val}(3.18)\approx1.170>\ln3=\operatorname{val}\mathcal{SP}$. Propositions 7–9 serve only that half and are not included. "Polynomial size, efficiently solvable" is informal and omitted.
• The §3.2 milestone carries the extra hypothesis that $\Xi$ contains a relatively open piece of the hyperplane $e_1^\top\xi=1$ (the paper's "dimension $k-1$", p. 10). Without it the claim is false for $l\ge2$. For $l=1$ the hypothesis follows from the standing assumptions, so the goal is unaffected.
• Strict feasibility is kept in the $l=1$ clause as printed, although the argument does not use it.

The goal cannot be trivialized through its definitions. Feasibility is quantified $\mathbb P$-almost surely for a measure whose support is $\Xi$, not over an empty or arbitrary set. Both optimal values are infima of the same real objective over the problems' own feasible sets. The standing assumptions are satisfiable, for instance by $k=2$, $W_1=\operatorname{diag}(1,-1)$, and $\mathbb P$ the uniform law on $\{1\}\times[-1,1]$.

The definitions (support of a measure, $\mathcal L^2$ decision rules, the random-recourse data) are reusable for the other sections of the paper and for related work on decision rules. Proofs of any milestone, Lean lemmas on quadratic forms vanishing on open cones, and an almost-sure-to-support transfer lemma are welcome.

Selected references

• D. Kuhn, W. Wiesemann, A. Georghiou, Primal and dual linear decision rules in stochastic and robust optimization, Optimization Online 2009/02/2218 (2009); Math. Program. 130 (2011) 177–209. https://optimization-online.org/wp-content/uploads/2009/02/2218.pdf, https://doi.org/10.1007/s10107-009-0331-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
• S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM Studies in Applied Mathematics 15, 1994 (the paper's source for Lemma 1). https://doi.org/10.1137/1.9781611970777
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004, Appendix B (the S-procedure as stated on the platform). https://web.stanford.edu/~boyd/cvxbook/
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007) 371–418. https://doi.org/10.1137/S003614450444614X
• M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Math. Program. 106 (2006) 423–432. https://doi.org/10.1007/s10107-005-0597-0