Optimization

Why adaptive decisions matter

A planner often chooses a first action before uncertain inputs are known and a corrective action afterward. If the uncertain input has no trusted probability law, a distributionally robust model tests the first action against all laws consistent with known support and moment information. The corrective action may depend on the realized input. This combination produces a difficult optimization problem: the adversary chooses a probability law, while the planner chooses a function of the input. Bertsimas, Sim, and Zhang study a class in which the support and moment bounds have second-order-cone representations. Their particular question is whether a tractable affine corrective rule can recover the exact worst-case cost.

Earlier work on moment-based distributionally robust optimization developed other ambiguity sets and reformulations. The related Prove2Me drafts MinimaxSLP and TractableDRO address mean and second-moment equality classes or bounds on positive parts of affine functions. Their model conventions differ from this paper's lifted SOC support, so this mission develops its own definitions. The affine-policy result of Bertsimas, Iancu, and Parrilo concerns a different multistage robust model. The paper places these contributions in its account of robust and distributionally robust decision rules (pp. 604–605).

Two-stage model and lifted ambiguity set

Write $x\in\mathbb R^{N_1}$ for the first-stage decision and $z\in\mathbb R^{I_1}$ for the observed uncertainty. After observing $z$, the planner chooses a free second-stage vector $y\in\mathbb R^{N_2}$. The constraint data depend affinely on $z$: $A(z)=A^0+\sum_i A^i z_i$ and $b(z)=b^0+\sum_i b^i z_i$. The fixed recourse matrix is $B$, and $d$ gives the second-stage cost. The recourse value is

$$Q(x,z)=\min\{d^\top y:A(z)x+By\ge b(z),\ y\in\mathbb R^{N_2}\}.$$

The support set $W$ restricts possible realizations. An SOC ambiguity set $F$ contains probability laws $P$ on $z$ for which $P(W)=1$, $\mathbb E_P[Gz]=\mu$, and $\mathbb E_P[g_i(z)]\le\sigma_i$ for each auxiliary function $g_i$. The paper assumes that $W$ and each epigraph $\{(z,u_i):g_i(z)\le u_i\}$ can be represented using products of second-order cones (Definition 3). Its exact worst-case expected recourse cost is $\beta(x)=\sup_{P\in F}\mathbb E_P[Q(x,z)]$.

The model introduces an auxiliary vector $u\in\mathbb R^{I_2}$ with lifted support $\bar W=\{(z,u):z\in W,\ g(z)\le u\}$. The lifted ambiguity set $\mathcal G$ consists of joint laws on $(z,u)$ supported on $\bar W$ with $\mathbb E[Gz]=\mu$ and $\mathbb E[u]\le\sigma$. Proposition 1 states that the primary marginals of these joint laws are exactly $F$. A regular linear decision rule has $y(z)=y^0+Y^1z$. An extended linear decision rule has $y(z,u)=y^0+Y^1z+Y^2u$. Their best worst-case costs are $\beta_L(x)$ and $\beta_E(x)$, with feasibility enforced at every point of $W$ or $\bar W$ respectively (§3.1).

Formalization targets

Theorem 2 gives the comparison that holds for the two rule classes:

$$\beta(x)\le\beta_E(x)\le\beta_L(x).$$

Theorem 1 identifies $\beta(x)$ with the robust program (9). Its variables are $r\in\mathbb R$, $s\in\mathbb R^{L_1}$, and $t\in\mathbb R^{I_2}_+$, constrained by $r+s^\top Gz+t^\top u\ge Q(x,z)$ at every $(z,u)\in\bar W$; its objective is $r+s^\top\mu+t^\top\sigma$. This result assumes relative complete recourse and Assumption 1, which represents the actual lifted support by a product of second-order cones and supplies a strict Slater point.

The mission's goal is Theorem 4. Under complete recourse and one second-stage decision variable, the extended affine class gives the exact value for every first-stage vector:

$$\forall x\in\mathbb R^{N_1},\qquad \beta(x)=\beta_E(x).$$

The equality is stronger than the bounds alone: it says that optimizing over this finite-parameter decision-rule class loses no worst-case value in the stated regime (Theorems 1, 2, and 4).

What the result supplies

Theorem 4 gives a precise case where the lifted affine approximation is exact. This matters because the unrestricted corrective decision is a function, while the affine class is described by finitely many coefficients. The paper observes that, with one recourse variable, the associated dual polyhedron has only $M$ extreme points; the robust reformulation can therefore be handled using a finite collection of constraints in this regime (p. 610). Proposition 3 marks a boundary: relative complete recourse by itself does not ensure that any extended affine rule is feasible.

The results are proved mathematically in the published paper and its electronic companion; the proofs of Theorems 1 and 4 are located in the companion, which is not held with this mission's source PDF. The Lean statements here are open proof obligations. A completed development would add reusable interfaces for free-variable linear recourse, SOC-supported moment ambiguity sets, lifted joint laws, and extended-real optimization values. It would also make the assumptions behind the paper's real-valued expectations and recourse costs explicit.

The hard point

Replacing the adaptive function $y(z)$ by an affine function of $z$ alone can fail even when the recourse LP is feasible for every realization: a single affine rule must satisfy every pointwise constraint simultaneously. Adding $u$ enlarges the rule class, but the lifted support contains all $u\ge g(z)$, not just $u=g(z)$. Thus its feasibility condition is stronger than feasibility on a convenient graph. Theorem 4 asserts exactness despite that universal lifted-support constraint. The direct comparison $\beta\le\beta_E$ does not by itself give the reverse inequality; the robust moment reformulation must describe the same worst-case value under its Slater and recourse hypotheses (§§2.2–3.1).

Formalization scope

Finite vectors are functions on Fin n, so the paper's indices $1,\ldots,n$ become zero-based. Laws are probability measures on finite real-vector spaces. The original and lifted ambiguity sets include integrability of all primary coordinates; the lifted set also includes integrability of all auxiliary coordinates, and the original set includes integrability of each $g_i$. This is a finite-first-moment reading of the paper's expectations. It excludes laws whose constrained linear moments exist while an unconstrained coordinate has infinite absolute moment. These conditions ensure that expected affine rule costs are genuine. The paper's Theorem 3 itself explicitly asks for finite coordinate first moments.

The recourse LP is represented as a separate reusable definition with free $y$, constraints $By\ge t$, and dual feasibility $p\ge0$, $B^\top p=d$. Statements using its real value require primal and dual feasibility. Theorem 2 states primal feasibility on the support at its chosen $x$; Theorem 1 uses relative complete recourse on $X\times W$; Theorem 4 uses complete recourse for every right-hand side. Theorems 1 and 4 also state dual feasibility explicitly because primal feasibility alone does not ensure it. Assumption 1 is explicit in both, including equality between its cone representation and the previously defined $\bar W$. Its bound $u^\dagger<\sigma$ means strict inequality in every auxiliary coordinate, and strict cone feasibility means membership in the interior of the product cone.

The values $\beta$, $\beta_L$, $\beta_E$, and (9) lie in the extended reals. Each printed “min” is an infimum, and no optimizer is presumed. A value is never formed by subtracting infinities. The SOC support, the epigraphs, and all rule feasibility conditions retain their pointwise meanings. Neither an empty ambiguity set nor an impossible rule class is silently replaced by a favorable real default. Contributions to LP value regularity, integrability, moment duality, and SOC geometry are all useful beyond this mission. The goal must continue to compare the original $\beta$ with the actual lifted-rule value $\beta_E$; replacing either by an easier surrogate would remove its content.

Selected references

• Dimitris Bertsimas, Melvyn Sim, and Meixia Zhang, Adaptive Distributionally Robust Optimization, Management Science 65(2):604–618, 2019. DOI.

Why subgradients of value functions matter

Stochastic dual dynamic programming (SDDP) and related decomposition methods solve multistage stochastic programs by approximating each stage's recourse function from below by a maximum of affine cuts. Every cut needs a value and a slope: the value of a convex subproblem at a trial point, and a subgradient of that subproblem's optimal value as a function of the trial point. For linear subproblems the slope is a vector of dual multipliers. For convex subproblems in which the trial point enters the objective and the nonlinear constraints, the slope requires a formula for the subdifferential of the value function of a parametric convex program.

Vincent Guigues, in Convergence Analysis of Sampling-Based Decomposition Methods for Risk-Averse Multistage Stochastic Convex Programs (arXiv:1408.4439v4, SIAM J. Optim. 2016), states such a formula as Lemma 2.1 and announces it in the abstract and in contribution (C) as a result of independent interest. Earlier convergence proofs for convex SDDP (Girardeau, Leclère and Philpott, Math. Oper. Res. 2015) avoid the question by copying the trial point into new variables and linear constraints, so that only the classical formula for a value function of right-hand-side perturbations is needed. Lemma 2.1 removes that device.

This mission is the second in the series on Guigues' paper. The first mission formalizes the almost-sure convergence of the risk-averse algorithm (Theorem 4.1) and takes the subgradient property of cut slopes as part of its model, so the two missions are independent.

Setting

Write $\mathbb R^k$ for Euclidean space with the scalar product $\langle x,y\rangle = x^\top y$, and pair $\mathbb R^m\times\mathbb R^n$ by $\langle (s,t),(x,y)\rangle=\langle s,x\rangle+\langle t,y\rangle$. Let $A\in\mathbb R^{q\times m}$, $B\in\mathbb R^{q\times n}$, $b\in\mathbb R^q$, let $f:\mathbb R^m\times\mathbb R^n\to\mathbb R\cup\{+\infty\}$, let $g=(g_1,\dots,g_p)$ be constraint functions on $\mathbb R^m\times\mathbb R^n$, and let $X\subseteq\mathbb R^m$ and $Y\subseteq\mathbb R^n$ be nonempty, compact and convex. The value function (2.1) is

$$\mathcal Q(x)=\inf\{\,f(x,y):\ y\in S(x)\,\},\qquad S(x)=\{y\in Y:\ Ax+By=b,\ g(x,y)\le 0\},$$

defined for every $x\in\mathbb R^m$, with $\mathcal Q(x)=+\infty$ when $S(x)=\emptyset$. The solution set is $\operatorname{Sol}(x)=\{y\in S(x): f(x,y)=\mathcal Q(x)\}$ and the active set is $I(x,y)=\{i: g_i(x,y)=0\}$.

The subdifferential of an extended-real function $h$ at $z_0$ is $\partial h(z_0)=\{s: h(z_0)\in\mathbb R,\ h(z)\ge h(z_0)+\langle s,z-z_0\rangle\ \forall z\}$, and the normal cone of a set $C$ at $z_0\in C$ is $\mathcal N_C(z_0)=\{v:\langle v,z-z_0\rangle\le0\ \forall z\in C\}$. The Lagrangian dual (2.3) maximizes

$$\theta_x(\lambda,\mu)=\inf_{y\in Y}\ f(x,y)+\lambda^\top(Ax+By-b)+\mu^\top g(x,y)$$

over $\lambda\in\mathbb R^q$, $\mu\in\mathbb R^p_+$; its solution set is $\Lambda(x)$.

Assumption (H): $f$ is lower semicontinuous, proper and convex; each $g_i$ is convex and lower semicontinuous with values in $\mathbb R\cup\{+\infty\}$; and $X^\varepsilon\times Y\subseteq\operatorname{dom} f$ for some $\varepsilon>0$, where $X^\varepsilon=X+\varepsilon B_m$.

Formalization targets

Goal: Lemma 2.1, formula (2.4), repaired

Assume (H) and the repaired Slater condition: every $g_i$ is real-valued (R1), and there is $(\bar x,\bar y)\in X\times\operatorname{ri}(Y)$ with $A\bar x+B\bar y=b$, $g_i(\bar x,\bar y)<0$ for all $i$ (R2), and $(\bar x,\bar y)\in\operatorname{ri}(\operatorname{dom} f)$ (R3). For $x_0\in X$ with $S(x_0)\ne\emptyset$, the set $\operatorname{Sol}(x_0)$ is nonempty and for every $y_0\in\operatorname{Sol}(x_0)$

$$s\in\partial\mathcal Q(x_0)\iff (s,0)\in\partial f(x_0,y_0)+\{[A^\top;B^\top]\lambda\}+\Big\{\sum_{i\in I(x_0,y_0)}\mu_i\,\partial g_i(x_0,y_0):\mu_i\ge0\Big\}+\{0\}\times\mathcal N_Y(y_0).$$

Differentiable case

If $f$ and the $g_i$ are real-valued, convex and differentiable, then under (R2)

$$\partial\mathcal Q(x_0)=\Big\{\nabla_x f(x_0,y_0)+A^\top\lambda+\sum_{i\in I(x_0,y_0)}\mu_i\nabla_x g_i(x_0,y_0):\ (\lambda,\mu)\in\Lambda(x_0)\Big\}.$$

Steps of the proof (milestones)

1. $\mathcal Q(x)=\inf_y f(x,y)+\mathbb I_{\operatorname{Gr}(S)}(x,y)$, and $s\in\partial\mathcal Q(x_0)\iff(s,0)\in\partial(f+\mathbb I_{\operatorname{Gr}(S)})(x_0,y_0)$ — (2.5).
2. The sum rule $\partial(f+\mathbb I_{\operatorname{Gr}(S)})=\partial f+\mathcal N_{\operatorname{Gr}(S)}$ under (2.6) — (2.5)-(a).
3. $\mathcal N_{\operatorname{Gr}(S)}=\mathcal N_{C_1}+\mathcal N_{C_2}+\mathcal N_{\mathbb R^m\times Y}$ and $\mathcal N_{\mathbb R^m\times Y}=\{0\}\times\mathcal N_Y$.
4. $\mathcal N_{C_1}(x_0,y_0)=\{(A^\top\lambda,B^\top\lambda)\}$.
5. $\mathcal N_{C_2}(x_0,y_0)=\{\sum_{i\in I}\mu_i\partial g_i(x_0,y_0):\mu_i\ge0\}$ (repaired).
6. Primal-dual solutions satisfy (2.7)-(b), and (2.7)-(b) with $\mu\ge0$ yields $(\lambda,\mu)\in\Lambda(x_0)$.
7. The differentiable case above.

Significance

Formula (2.4) yields cut slopes for SDDP applied to convex multistage programs directly from a primal solution and multipliers of the stage subproblem, without auxiliary copies of the state, and it is the source of the subgradient property used in the convergence analysis of the paper's Algorithm 1. The differentiable case is the form an implementation uses: any optimal dual pair gives a subgradient, and every subgradient arises this way.

For formalization, the result is a self-contained piece of finite-dimensional convex analysis: infimal projection, the subdifferential sum rule under a relative-interior condition, normal cones of intersections, of affine sets and of convex sublevel sets, and Lagrangian duality under Slater's condition. None of these steps is in Mathlib in the extended-real form needed here. No machine-checked proof of Lemma 2.1 or of its differentiable case exists. The platform has Shor's subgradient formula for value functions (ShorNonsmooth.Decomposition.value_function_convex_and_subgradient, subgradient_formula, subgradient_formula_differentiable, proved). Those statements cover real-valued data with inequality constraints only and prove one inclusion. They have no equality block $Ax+By=b$, no set $Y$ and no converse, so they are related to this mission but are not instances of it.

Difficulty

The printed lemma is false. Two steps of its proof fail. First, the formula for $\mathcal N_{C_2}$ needs a strict Slater point: for $g(x,y)=y^2$, $C_2=\mathbb R\times\{0\}$ equals its own relative interior, but $\mathcal N_{C_2}(0,0)=\{0\}\times\mathbb R$ is not generated by $\partial g(0,0)=\{0\}$. With $f(x,y)=y$, $X=Y=[-1,1]$ and $A=B=0$, all printed hypotheses hold, $\mathcal Q\equiv0$, and no $s$ satisfies (2.4). Second, $X^\varepsilon\times Y\subseteq\operatorname{dom} f$ does not give $\operatorname{ri}(X^\varepsilon\times Y)\subseteq\operatorname{ri}(\operatorname{dom}f)$: with $Y=\{0\}$, $g\equiv-1$ and $f(x,y)=-\sqrt y$, $\partial f(x_0,0)=\emptyset$ while $\partial\mathcal Q(x_0)=\{0\}$. The repair (R1)–(R3) adds hypotheses and leaves every step of the printed proof valid.

The remaining work is the relative-interior calculus. The sum rule and the intersection formula for normal cones hold only under qualification conditions phrased with relative interiors, and the converse direction of (2.4) needs that the qualification passes from $(\bar x,\bar y)$ to $\operatorname{Gr}(S)$. A proof that uses only interiors fails as soon as $Y$ is lower-dimensional, which the hypotheses allow.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin k). The product $\mathbb R^m\times\mathbb R^n$ is the Lean product type, and subgradients and normal cones on it use the explicit pairing $\langle s,x\rangle+\langle t,y\rangle$. No norm of the product is involved. Extended values are EReal. $\mathcal Q$ is an EReal infimum on all of $\mathbb R^m$, and $\partial\mathcal Q(x_0)$ is its subdifferential on $\mathbb R^m$, not relative to $X$. An encoding of $\mathcal Q$ on $X$ only, or of $\partial\mathcal Q$ relative to $X$, would describe a different function, whose subdifferential is unbounded at boundary points of $X$; it is excluded. Subdifferentials require a finite value at the base point, so the equivalence cannot hold vacuously at a point where a function is $+\infty$. $X^\varepsilon$ is Metric.cthickening ε X; relative interiors are intrinsicInterior ℝ. Indices are 0-based (Fin p, Fin q). The sums in (2.4) are written with explicit witnesses $\mu_i\ge0$, $w_i\in\partial g_i$ indexed by the active set, which avoids the convention $0\cdot\emptyset=\emptyset$.

Repaired statements, each labelled "(repaired)" in its title:

• Lemma 2.1 (2.4): adds (R1) real-valued $g_i$, (R2) strict Slater point, (R3) Slater point in $\operatorname{ri}(\operatorname{dom}f)$, and concludes $\operatorname{Sol}(x_0)\ne\emptyset$, which the printed "where $y_0$ is any element" presupposes.
• $\mathcal N_{C_2}$ formula: assumes (R1) and (R2) instead of a point of $\operatorname{ri}(C_2)$.
• Differentiable case: "$f$ and $g$ differentiable" is read as real-valued and differentiable on the whole space, and (R2) replaces the printed condition.

The sum-rule milestone keeps (2.6) as a hypothesis, as the page states it. The dual-solution milestone reads "primal-dual solution" as $y_0\in\operatorname{Sol}(x_0)$, $(\lambda,\mu)\in\Lambda(x_0)$ with zero duality gap, assumes only primal feasibility of $y_0$ for the converse (as the page does), and extends $\mu$ by zero outside the active set.

A complete development needs: the subdifferential sum rule for proper convex extended-real functions under a relative-interior condition; normal cones of intersections of convex sets with one affine set; normal cones of sublevel sets of finite convex functions under Slater's condition; existence of minimizers of lower semicontinuous functions on compact sets; and a zero-duality-gap (minimax) theorem for Lagrangians of convex programs over a compact convex set. These are reusable well beyond this mission. Contributions of any of these lemmas, in the generality of an arbitrary finite-dimensional inner product space, are welcome.

Selected references

• V. Guigues, Convergence Analysis of Sampling-Based Decomposition Methods for Risk-Averse Multistage Stochastic Convex Programs, arXiv:1408.4439v4, 2016; SIAM J. Optim. 26(4), 2016. https://arxiv.org/abs/1408.4439
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorems 23.8, 24(a), 28.2; Corollary 23.8.1). https://doi.org/10.1515/9781400873173
• P. Girardeau, V. Leclère, A. B. Philpott, On the Convergence of Decomposition Methods for Multistage Stochastic Convex Programs, Math. Oper. Res. 40(1), 2015. https://doi.org/10.1287/moor.2014.0664
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Programming 52, 1991. https://doi.org/10.1007/BF01582895
• N. Z. Shor, Nondifferentiable Optimization and Polynomial Problems, Kluwer, 1998. https://doi.org/10.1007/978-1-4757-6015-6

Motivation

Multistage stochastic programs model sequential decisions under uncertainty: hydro-thermal scheduling, portfolio management and capacity planning are standard examples. Their dynamic programming equations involve recourse functions (cost-to-go functions) of the decision history, which cannot be computed exactly. Stochastic Dual Dynamic Programming (SDDP), introduced by Pereira and Pinto in 1991, approximates each recourse function from below by a maximum of affine cuts, built at trial points generated by simulating sampled scenarios. SDDP is the method of choice in the energy industry for long-horizon stochastic planning.

Two extensions motivate this mission. Risk-averse planning replaces the expectation at each stage by a coherent risk measure (for instance the Conditional Value-at-Risk), and many applications have convex but nonlinear stage problems. Guigues (2016) proves that the risk-averse sampling algorithm for convex stage problems converges almost surely.

Timeline.

• 1991: Pereira and Pinto introduce SDDP for linear multistage problems.
• 2008: Philpott and Guan prove almost sure finite convergence of SDDP-type methods for linear problems with finitely many scenarios.
• 2011: Shapiro analyses the sample-average SDDP method and formulates its risk-averse variant with nested conditional risk measures; 2013: Philpott, de Matos and Finardi treat SDDP with coherent risk measures in dual form.
• 2015: Girardeau, Leclère and Philpott prove almost sure (asymptotic) convergence of sampling-based decomposition methods for risk-neutral multistage stochastic convex programs.
• 2016: Guigues extends that analysis to risk-averse problems in dual form, with nonlinear constraints and interstage independent processes (arXiv:1408.4439, SIAM J. Optim.); the convergence theorem is Theorem 4.1.

Setting

There are $T$ stages with decisions $x_t\in\mathbb R^n$ and a given $x_0$. A history $x_{1:t}=(x_1,\dots,x_t)$ is identified with the vector $[x_1;\dots;x_t]\in\mathbb R^{nt}$ with its Euclidean norm. The random data $\xi_t$ are interstage independent (H1). For $t\ge2$, $\xi_t$ takes $M$ values $\xi_{t,1},\dots,\xi_{t,M}$ with probabilities $\Phi_{t,j}>0$, and $\xi_1$ is deterministic. A realization $\xi_{t,j}$ consists of a cost $f_t(\cdot,\Psi_{t,j})$ with values in $\mathbb R\cup\{+\infty\}$, convex constraints $g_t(x_0,\cdot,\Psi_{t,j})\le0$ and linear constraints $\sum_{\tau=0}^tA_{t,\tau,j}x_\tau=b_{t,j}$. Together with a compact set $\mathcal X_t$, they define the feasible set $X_t(x_{0:t-1},\xi_{t,j})$.

The risk measure of stage $t$ is given in dual form,

$$\rho_t(Z)=\sup_{p\in\mathcal P_t}\sum_{j=1}^Mp_j\Phi_{t,j}Z_j,\qquad \mathcal P_t\subseteq\mathcal D_t=\Big\{p\ge0:\sum_jp_j\Phi_{t,j}=1\Big\}.$$

The recourse functions satisfy $\mathcal Q_{T+1}\equiv0$ and, for $t=T,\dots,2$,

$$\mathfrak Q_t(x_{1:t-1},\xi_{t,j})=\inf_{x_t\in X_t(x_{0:t-1},\xi_{t,j})}f_t(x_{1:t},\Psi_{t,j})+\mathcal Q_{t+1}(x_{1:t}),\qquad \mathcal Q_t(x_{1:t-1})=\rho_t\big(\mathfrak Q_t(x_{1:t-1},\xi_t)\big).$$

The first-stage value is $\mathcal Q_1(x_0)=\mathfrak Q_1(x_0,\xi_1)$. Assumption (H2) requires convexity, lower semicontinuity and properness of the data, and fixes an $\varepsilon>0$ such that the costs are finite and the feasible sets nonempty on the $\varepsilon$-fattening $[\mathcal X_1\times\dots\times\mathcal X_{t-1}]^\varepsilon$. It also asks for a relative-interior point of the nonlinear constraints.

Algorithm 1 keeps cutting-plane models $\mathcal Q^k_t$, starting from $\mathcal Q^0_t\equiv-\infty$. At iteration $k$ it computes decisions $x^k_m$ at every node $m$ of the scenario tree, by solving the stage problems with $\mathcal Q^{k-1}_{t+1}$ in place of $\mathcal Q_{t+1}$. It then samples one scenario $n^k_1,\dots,n^k_T$, with indices $\xi^k_t$ satisfying the independence assumption (H3), and adds at each sampled node one cut

$$\theta^k_t+\langle\beta^k_t,\,\cdot-x^k_{[n^k_{t-1}]}\rangle,\qquad \theta^k_t=\sum_mp_{k,m}\Phi_m\mathfrak Q^{k-1}_t(x^k_{[n]},\xi_m),\quad\beta^k_t=\sum_mp_{k,m}\Phi_m\pi_{k,m}.$$

Here $p^k$ attains the supremum in $\rho_t$, and $\pi_{k,m}$ is a subgradient of $\mathfrak Q^{k-1}_t(\cdot,\xi_m)$.

Formalization targets

Goal: Theorem 4.1 (p. 12)

Almost surely, for $t=2,\dots,T+1$ and every node $n$ of stage $t-1$,

$$\lim_{k\to\infty}\mathcal Q_t(x^k_{[n]})-\mathcal Q^k_t(x^k_{[n]})=0.$$

Almost surely, moreover, $\mathfrak Q^k_1(x_0,\xi_1)\to\mathcal Q_1(x_0)$, and every accumulation point of the first-stage decisions $(x^k_1)$ is an optimal solution of the first-stage problem.

Milestones

• Proposition 2.2: subgradient bound $\|s\|\le(M_0-m_0)/\varepsilon$ for the value function of a convex program.
• Proposition 3.1: $\mathcal Q_t$ is convex, finite and continuous on $[\mathcal X_1\times\dots\times\mathcal X_{t-1}]^{\hat\varepsilon}$, $0<\hat\varepsilon<\varepsilon$.
• Lemma 3.2: valid cuts $\mathcal Q^k_t\le\mathcal Q_t$, bounded cut coefficients and slopes, and Lipschitz models for $k\ge T-t+1$.
• Lemma 3.4: $\mathcal Q^k_t(x^k_{[n^k_{t-1}]})=\theta^k_t$.
• Lemma 3.5: a uniform Lipschitz constant $L$ for the models.
• (4.26), (4.28), (4.29), (4.31): the steps of the proof of Theorem 4.1. These are the error propagation along the tree, the limit along the iterations through a node, the almost sure limit along the other iterations, and the first-stage bound.

Significance

Theorem 4.1 guarantees that the algorithm's lower bound $\mathfrak Q^k_1(x_0,\xi_1)$ converges to the true risk-averse optimal value, and that its first-stage decisions approach optimal ones. It covers nonlinear convex stages, where finite convergence arguments for polyhedral problems do not apply. It also covers every risk measure with a dual representation, including CV@R and its combinations with expectation. Practitioners rely on this to justify stopping rules based on the lower bound.

The result is proved on paper. To our knowledge neither Theorem 4.1 nor its risk-neutral counterpart (Girardeau–Leclère–Philpott, Theorem 3.1) has been machine-checked; the risk-neutral statements are posed, unproved, on this platform. A formalization would check a proof that combines convex analysis (value functions of convex programs, subgradient bounds, Lipschitz continuity on fattenings), cutting-plane bookkeeping and a probabilistic argument (strong law of large numbers along a predictable subsequence).

Difficulty

The cuts are built only along sampled scenarios, so at a given node the approximation is refined only at the iterations whose scenario passes through it. The obvious induction argument controls the error $\mathcal Q_t-\mathcal Q^k_t$ only along those iterations. Extending it to all iterations is the probabilistic core (4.29). It needs the samples to be independent of everything the algorithm has computed so far, and it needs a strong law of large numbers along the subsequence of iterations at which the error is still large. A second difficulty is passing from the current model $\mathcal Q^k_{t+1}$ to the previous one $\mathcal Q^{k-1}_{t+1}$. This needs uniform Lipschitz bounds on the models (Lemmas 3.2, 3.5), which in turn rest on the fattening in (H2) and on the subgradient bound of Proposition 2.2.

Formalization scope

• Histories and norms. Histories are $L^2$ products of copies of $\mathbb R^n$ (PiLp 2), so fattenings, inner products and Lipschitz constants use the Euclidean norm on $\mathbb R^{n(t-1)}$. Fattenings are closed thickenings.
• Extended reals. Values are in EReal, infima are $+\infty$ on empty feasible sets, and weights $p_j\Phi_{t,j}$ are real numbers (with $0\cdot(\pm\infty)=0$). Limits of gaps are taken in EReal, so that convergence to $0$ forces the gaps to become finite.
• Data and indices. The recourse functions are constructed by the backward recursion from the data. The scenario tree is the product tree indexed by histories of realization indices, so (H1) is built into the model. Stage 1 uses the data of the first realization index.
• Runs. A run is pinned to fixed deterministic choice rules (minimizers, maximizing $p^k$, subgradients), so it uses only present and past samples. The goal holds for every choice of rules.
• Departures from the printed text, disclosed in the items.
  • The cut slope $\pi_{k,m}$ is any subgradient of $\mathfrak Q^{k-1}_t(\cdot,\xi_m)$. The printed formula on p. 9 uses a partial subgradient of $f_t$, which is not a subgradient when $f_t$ is nonsmooth, and the proof only uses the subgradient property.
  • $\mathcal P_t\ne\emptyset$ is assumed; it is implicit, because $\rho_t$ is a real-valued coherent risk measure.
  • In Proposition 2.2, $M_0$ is an extended-real supremum. The proof's claim that $M_0$ is finite does not follow from lower semicontinuity.
  • Lemma 3.2's vacuous "almost surely" is dropped.
  • One $\varepsilon$ serves all stages in (H2).
• Ruled out. A formalization in which the decisions or cuts ignore the models, or in which $\mathcal P_t=\emptyset$ or every stage value is $+\infty$, would make the limits trivial. The decisions must minimize against $\mathcal Q^{k-1}_{t+1}$, the cut must use the attained supremum, and the companion item run_exists shows that under (H2), with closed $\mathcal P_t$, rules producing a run exist for every sample path.
• Infrastructure and contributions. A complete development needs value functions of parametric convex programs, subgradient bounds for convex functions on fattenings, Lipschitz continuity of finite maxima of affine functions, and a strong law of large numbers along predictably selected subsequences (Lemma A.3 of Girardeau–Leclère–Philpott). The last two are reusable well beyond this mission. Contributions to any milestone, or to these general lemmas, are welcome.

Selected references

• V. Guigues, Convergence analysis of sampling-based decomposition methods for risk-averse multistage stochastic convex programs, SIAM J. Optim. 26(4), 2016; preprint arXiv:1408.4439v4. https://arxiv.org/abs/1408.4439
• P. Girardeau, V. Leclère, A. B. Philpott, On the convergence of decomposition methods for multistage stochastic convex programs, Math. Oper. Res. 40(1), 2015. https://doi.org/10.1287/moor.2014.0664
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52, 1991. https://doi.org/10.1007/BF01582895
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Oper. Res. Lett. 36(4), 2008. https://doi.org/10.1016/j.orl.2008.01.013
• A. B. Philpott, V. L. de Matos, E. Finardi, On solving multistage stochastic programs with coherent risk measures, Oper. Res. 61(4), 2013. https://doi.org/10.1287/opre.2013.1175
• A. Shapiro, Analysis of stochastic dual dynamic programming method, European J. Oper. Res. 209(1), 2011. https://doi.org/10.1016/j.ejor.2010.08.007

Motivation

Multistage stochastic programs model decisions taken over time while uncertain data are revealed: generation scheduling in hydro-thermal power systems, capacity expansion, unit commitment, portfolio management. When the uncertainty is represented by a finite scenario tree, the problem becomes one very large deterministic program, and decomposition algorithms solve it stage by stage. For linear problems the standard methods are nested Benders decomposition and its sampling variant, stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto (1991). Both rely on the convexity of the value functions, which they approximate from below by linear cuts.

Many applications need integer decisions (on/off status of generators, investment choices), and integer variables destroy convexity. Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) observed that when the state variables passed between stages are binary, exact convex polyhedral representations still exist on the binary points. They proposed stochastic nested decomposition (SND) and its stage-wise independent special case SDDiP, and identified three properties of cuts (valid, tight, finite) under which the algorithms converge. This mission formalizes that convergence theorem, Theorem 2 of the paper.

Timeline. Birge (1985) gave nested decomposition for multistage linear programs; Pereira and Pinto (1991) introduced SDDP. Philpott and Guan (2008) proved almost sure finite convergence of SDDP-type methods for linear problems, and Girardeau, Leclère and Philpott (2015) extended convergence to convex problems. Zou, Ahmed and Sun (2019) proved finite convergence with probability one for mixed integer problems with binary states and abstract valid, tight and finite cuts, and showed that their Lagrangian cuts have the first two properties.

Setting

Let $\mathcal T$ be a scenario tree with stages $1,\dots,T$, root $1$, parent map $a(n)$ and children $\mathcal C(n)$. The nodes of the last stage are the scenarios. Node probabilities satisfy $p_n>0$, $p_1=1$, and $p_n=\sum_{m\in\mathcal C(n)}p_m$ before the last stage, and $q_{nm}=p_m/p_n$. Each node has a linear cost $f_n(x_n,y_n)$ and a nonempty compact mixed integer polyhedral set $X_n$ (assumption (A1)). The state $x_n\in\{0,1\}^d$ is binary, the local variables $y_n$ are general, and the root's parent state $\bar x_0$ is fixed. The problem in local-copy form (2.1) is

$$\min\sum_{n\in\mathcal T}p_nf_n(x_n,y_n)\quad\text{s.t.}\quad(z_n,x_n,y_n)\in X_n,\ z_n=x_{a(n)},\ x_n\in\{0,1\}^d .$$

Its value functions satisfy the recursion (2.3): $Q_n(x_{a(n)})=\min\{f_n(x_n,y_n)+\mathcal Q_n(x_n)\}$ over the nodal feasible set, with the expected cost-to-go function $\mathcal Q_n(x)=\sum_{m\in\mathcal C(n)}q_{nm}Q_m(x)$.

The SND algorithm keeps an under-approximation $\psi^i_n$ of each $\mathcal Q_n$: the maximum of a lower bound $L_n$ and the aggregated cuts $\sum_{m\in\mathcal C(n)}q_{nm}(v^\ell_m+(\pi^\ell_m)^\top x)$ collected so far (3.2). Each iteration $i$ samples $M$ scenarios with replacement. In the forward step it solves the nodal problems $P^i_n(x^i_{a(n)},\psi^i_n)$ from the root down, which yields the forward tree solution $\{(x^i_n,y^i_n)\}$ of (3.6). In the backward step, at every sampled node it generates one cut per child at the state $x^i_n$ and adds their aggregate to $\psi_n$. Cuts are valid if $Q_m(x)\ge v^i_m+(\pi^i_m)^\top x$ on $\{0,1\}^d$ (3.4). They are tight if they equal the value $\underline Q^i_m(x^i_n,\psi^{i+1}_m)$ of the child's updated nodal problem at $x^i_n$ (3.5). They are finite if only finitely many distinct cuts occur. Assumption (A3) requires the nodal solver to return the same optimal solution whenever it is given the same problem.

Formalization targets

Goal: Theorem 2 (p. 474)

With sampling with replacement, valid, tight and finite cuts, and a solver satisfying (A3), the following holds with probability one:

$$\exists\, i_0\ \ \forall i\ge i_0:\quad \{(x^i_n,y^i_n)\}_{n\in\mathcal T}\ \text{is an optimal solution of (2.1)}.$$

Milestones, in the order the proof uses them

1. Valid cuts give under-approximations, $\psi^i_n\le\mathcal Q_n$ and $\underline Q^i_n\le Q_n$ (proof of Claim 1, p. 475).
2. Claim 1: if $\psi^i_n(x^i_n)=\mathcal Q_n(x^i_n)$ for all $n$, the forward solution is optimal for (2.1) (p. 475).
3. With finitely many possible cuts, the approximations $\{\psi^i_n\}$ change only in finitely many iterations (pp. 474–475).
4. (3.8a)–(3.8f): a sampled node whose children are exact becomes exact after its backward step (p. 476).
5. Under sampling with replacement, every scenario is sampled in infinitely many iterations, almost surely (p. 476).
6. Claim 2: almost surely, no infinite block of unchanged approximations has a non-optimal forward solution (p. 475).

Significance

Theorem 2 separates the convergence of nested decomposition from the choice of cuts. Any cut family with the three properties yields an exact algorithm for multistage stochastic integer programs with binary states. The paper verifies the properties for integer optimality cuts and, through its Theorem 3, shows that Lagrangian cuts from the local-copy reformulation are valid and tight. The convergence of SDDiP, the variant used in computations, follows from the same theorem, and binary expansion of general integer states extends the reach to mixed integer state spaces.

The result is proved in the paper; no machine-checked proof exists. A formal development would turn its informal points into checked statements: that the minima are attained, that the DP recursion is equivalent to the extensive form, and that the finiteness of cuts is global. It would also supply a reusable framework (scenario trees with node probabilities, cut-based approximations, sampled runs) for the convergence theory of SDDP-type methods.

Difficulty

No single step is deep; the difficulty is the interaction of the pieces. A tempting argument says the approximations stop changing, so the algorithm stops at an optimum. But a stalled run need not be optimal: if a node at which $\psi_n$ is inexact is never sampled again, nothing changes and the forward solution stays suboptimal. The proof must therefore combine three things: the deterministic finiteness of changes, an almost sure statement about sampling, and the exactness chain (3.8). That chain depends on tightness with respect to the updated approximation of the child, and it fails if tightness refers to the approximation from before the backward step. The equivalence between optimality for the DP recursion and for the extensive form (2.1), used without proof in Claim 1, also requires a backward induction over the tree.

Formalization scope

The tree is the platform definition StochasticProg.Multistage.Tree H, with stage $t$ of the paper equal to stage = t − 1. Binary vectors are Fin d → Bool, embedded in $\mathbb R^d$. The copy variable $z_n$ is eliminated through $z_n=x_{a(n)}$. Minima are written as infima over sets that the standing assumptions make nonempty, bounded below and attained. Lean iterations are numbered from $0$, and the run is infinite (stopping criteria and bounds play no role).

Readings of informal words. "Optimal solution of (2.1)" means a feasible tree solution of least cost $\sum_np_nf_n$ among all feasible tree solutions. "After a finite number of iterations" means from some iteration on, in every iteration (∀ᶠ i in atTop). "With probability one" refers to a probability space carrying independent draws, $M\ge1$ per iteration, each with law $\{p_n:n\in S_T\}$. "Finite" cuts means one finite set for the whole run, as the proof uses it, not a different finite set per iteration. (A3) means the solver is a function of the node, the parent state and the approximation, and returns an optimal solution.

Added hypotheses, which the paper uses without stating them: $p_n>0$; every nodal problem is feasible for every binary parent state, which replaces (A2) (not used by Theorem 2); and the lower bounds under-estimate, $L_n\le\mathcal Q_n$, which is Algorithm 1's "initial under-approximation".

Trivializing formalizations are ruled out: tightness refers to the child's approximation after its own update, optimality is for the true extensive form and not relative to $\psi$, and the probability statement is over independent sampling, not over a fixed sample sequence assumed to visit every scenario.

Contributions welcome: the attainment lemmas for nodal minima, the DP/extensive-form equivalence on trees, and the second Borel–Cantelli argument for repeated sampling. All of these are reusable for other SDDP-type convergence results.

Selected references

• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Math. Program. 175 (2019) 461–502. https://doi.org/10.1007/s10107-018-1249-5
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52 (1991) 359–375. https://doi.org/10.1007/BF01582895
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Oper. Res. Lett. 36 (2008) 450–455. https://doi.org/10.1016/j.orl.2008.01.013
• P. Girardeau, V. Leclère, A. B. Philpott, On the convergence of decomposition methods for multistage stochastic convex programs, Math. Oper. Res. 40 (2015) 130–145. https://doi.org/10.1287/moor.2014.0664
• J. R. Birge, Decomposition and partitioning methods for multistage stochastic linear programs, Oper. Res. 33 (1985) 989–1007. https://doi.org/10.1287/opre.33.5.989

Motivation

Algorithms for smooth nonlinear programming, such as augmented Lagrangian, interior point and sequential quadratic programming methods, do not stop at exact Karush–Kuhn–Tucker (KKT) points. They stop at points where the KKT conditions hold approximately. Sequential optimality conditions make this precise: they are properties of sequences $x^k\to x^*$ with approximate multipliers, satisfied at every local minimizer without any constraint qualification, and verified by the iterates of practical methods. To conclude that a limit point is a KKT point, one still needs a condition on the constraints. Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) identify, for each of several sequential conditions, the weakest such condition. They call it the weakest strict constraint qualification associated with that condition, and they place each one within the classical hierarchy of constraint qualifications.

This mission concerns the Complementary AKKT condition (CAKKT) of Andreani, Martínez and Svaiter (SIAM J. Optim. 20(6), 2010). CAKKT is strictly stronger than AKKT and is satisfied by the limit points of an augmented Lagrangian method under a weak Łojasiewicz-type hypothesis. The paper's §6.1 compares the associated weakest strict CQ, CAKKT-regularity, with Abadie's constraint qualification, one of the classical conditions of nonlinear programming. The answer is that CAKKT-regularity implies Abadie's CQ, and the converse fails.

Timeline:

• 1967: Abadie introduces the condition $L_\Omega(x^*)=T_\Omega(x^*)$.
• 1969: Guignard weakens it to equality of the polars.
• 1971: Gould and Tolle prove that Guignard's condition is the weakest CQ guaranteeing KKT at local minimizers.
• 2010: Andreani, Martínez and Svaiter introduce CAKKT.
• 2016: Andreani, Martínez, Ramos and Silva characterize the weakest strict CQ for AKKT, the cone continuity property (SIAM J. Optim. 26(1)).
• 2015/2018: the present paper defines CAKKT-regularity and proves Theorems 4.3 and 6.4.

Setting

Let $h_1,\dots,h_m,g_1,\dots,g_p:\mathbb R^n\to\mathbb R$ be continuously differentiable, and let

$$\Omega=\{x\in\mathbb R^n:\ h_i(x)=0\ (i\le m),\ g_j(x)\le 0\ (j\le p)\}.$$

For feasible $x^*$, $J(x^*)=\{j: g_j(x^*)=0\}$ is the set of active inequalities. The polar of a set $K$ is $K^\circ=\{v:\langle v,k\rangle\le 0\ \forall k\in K\}$.

• The tangent cone $T_\Omega(x^*)$ is the set of $d$ for which there are $t_k\downarrow 0$ and $d^k\to d$ with $x^*+t_kd^k\in\Omega$.
• The linearized cone is $L_\Omega(x^*)=\{d:\langle\nabla h_i(x^*),d\rangle=0\ \forall i,\ \langle\nabla g_j(x^*),d\rangle\le 0\ \forall j\in J(x^*)\}$.
• The regular normal cone $\widehat N_\Omega(z)$ is the set of $w$ with $\langle w,y-z\rangle\le o(\|y-z\|)$ for $y\in\Omega$.
• The limiting normal cone $N_\Omega(x^*)$ is the set of limits of $w^k\in\widehat N_\Omega(z^k)$ along $z^k\to x^*$ in $\Omega$.

Abadie's CQ holds at $x^*$ when $L_\Omega(x^*)=T_\Omega(x^*)$.

An objective $f$ satisfies CAKKT at $x^*$ if there are $x^k\to x^*$, $\lambda^k\in\mathbb R^m$ and $\mu^k\in\mathbb R^p_+$ with

$$\nabla f(x^k)+\sum_i\lambda_i^k\nabla h_i(x^k)+\sum_j\mu_j^k\nabla g_j(x^k)\to 0,\qquad \sum_i|\lambda_i^kh_i(x^k)|+\sum_j|\mu_j^kg_j(x^k)|\to 0.$$

For $x\in\mathbb R^n$ and $r\ge 0$, let $K_C(x,r)$ be the set of vectors $\sum_i\lambda_i\nabla h_i(x)+\sum_{j\in J(x^*)}\mu_j\nabla g_j(x)$ with $\mu\ge 0$ and $\sum_i|\lambda_ih_i(x)|+\sum_{j\in J(x^*)}|\mu_jg_j(x)|\le r$. The point $x^*$ is CAKKT-regular if $(x,r)\rightrightarrows K_C(x,r)$ is outer semicontinuous at $(x^*,0)$:

$$\limsup_{(x,r)\to(x^*,0)}K_C(x,r)\subseteq K_C(x^*,0).$$

Formalization targets

Goal: Theorem 6.4

$$x^*\in\Omega\ \text{CAKKT-regular}\quad\Longrightarrow\quad L_\Omega(x^*)=T_\Omega(x^*).$$

Milestones

The inclusion $T_\Omega(x^*)\subseteq L_\Omega(x^*)$ always holds, so the content of the goal is the reverse inclusion. The milestones are the statements the paper's proof uses, in attack order:

1. Lemma 6.1: every $y\in T_\Omega(\bar x)^\circ$ equals $-\nabla F(\bar x)$ for a $C^1$ function $F$ that has a strict global minimum over $\Omega$ at $\bar x$.
2. Lemma 6.2: such a $y$ is the limit of multiplier combinations $\omega^k$ at points $x^k\to\bar x$. The multipliers satisfy $\mu^k_j=c_k\max\{0,g_j(x^k)\}$, and the complementarity residual $r^k$ tends to $0$.
3. $\widehat N_S(z)=T_S(z)^\circ$ for every set $S$.
4. $T_\Omega(x^*)\subseteq L_\Omega(x^*)$.
5. $K_C(x^*,0)=L_\Omega(x^*)^\circ$.
6. Under CAKKT-regularity, $N_\Omega(x^*)\subseteq L_\Omega(x^*)^\circ$.
7. $N_S(z)^\circ\subseteq T_S(z)$ for closed $S$.

Companion: Theorem 4.3

$$x^*\ \text{CAKKT-regular}\iff\big(\forall f\in C^1:\ \text{CAKKT at }x^*\Rightarrow\text{KKT at }x^*\big),$$

with the equivalence of the two formulations (4.12)–(4.13) and (4.14)–(4.15) of CAKKT as a milestone.

Significance

Theorem 6.4 places CAKKT-regularity in the classical hierarchy. Every point at which CAKKT forces KKT for all objectives also satisfies Abadie's CQ, and therefore Guignard's. The paper's Example 6.1 shows that Abadie's CQ does not imply CAKKT-regularity. A convergence theorem for an algorithm that produces CAKKT sequences therefore cannot be stated under Abadie's CQ alone. Together with Theorem 4.3, this fixes exactly what a CAKKT-based method needs from the constraints.

The results are proved in the paper. None of them, and none of the variational-analysis facts they rest on, is formalized on Prove2Me, and Mathlib has no regular or limiting normal cones of nonconvex sets. The work is to formalize the paper's proof together with the parts of Rockafellar–Wets it cites: Theorem 6.11 (gradients of smooth functions as normals), Proposition 6.5, and Theorems 6.26 and 6.28(b). The last is Clarke's theorem that the regular tangent cone of a closed set is the polar of its limiting normal cone. These facts are reusable well beyond this mission.

Difficulty

The inclusion $T_\Omega\subseteq L_\Omega$ is elementary. The reverse inclusion cannot be obtained from CAKKT-regularity at $x^*$ alone, because CAKKT-regularity is a statement about multiplier combinations, which live on the polar side. The argument therefore has to pass through normal cones at points $x^k\ne x^*$ near $x^*$. At such points the active set may differ from $J(x^*)$, and the complementarity residual must be controlled uniformly. Returning from polars to cones requires the passage from the limiting normal cone to the tangent cone (milestone 7). That is a deep fact about closed sets in finite dimension; it is not a formal manipulation of cones. Equality of polars would only give Guignard's CQ.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), indices are Fin m and Fin p, and gradients are Mathlib's gradient. The objects are:

• Constraints. The constraints are a structure Constraints n m p of two index families. Every theorem assumes IsC1 (each $h_i$ and $g_j$ is $C^1$, the paper's standing hypothesis) and feasibility of $x^*$.
• KKT is the multiplier form, with $\mu\ge 0$ and $\mu_j=0$ off $J(x^*)$.
• Cones. The tangent cone uses positive scalars $t_k\to 0$ (Mathlib's tangentConeAt allows negative scalars and is not used). The regular normal cone is empty off the set. The limiting normal cone and outer semicontinuity use the sequential Painlevé–Kuratowski outer limit, and the outer limit in CAKKT-regularity is taken over pairs with $r\ge 0$.
• CAKKT includes $x^k\to x^*$. The page's (4.12)–(4.13) omit it, but p. 1 and (4.14)–(4.15) make it part of the condition.
• Sums over $J(x^*)$ are written over all indices, with the multipliers forced to $0$ off $J(x^*)$.
• Abadie's CQ is the equality of cones of p. 5. The proof's "$T_\Omega(x^*)=L_\Omega(x^*)^\circ$" is a misprint and is not copied.
• Closedness of $\Omega$ is not assumed; it follows from continuity.

The following would trivialize the goal and are excluded:

• a normal cone that is nonempty outside the set;
• the convex normal cone used for the nonconvex $\Omega$;
• KKT without the sign or complementarity conditions;
• for Theorem 4.3, an objective quantified outside the equivalence;
• Abadie's CQ weakened to equality of polars.

A complete development needs Clarke's tangent–normal polarity for closed sets in $\mathbb R^n$, the existence of $C^1$ functions realizing regular normals, and a penalty argument for Lemma 6.2. Proofs of the general variational-analysis milestones (3 and 7) are especially welcome, since they serve any mission on nonconvex constraint sets.

Selected references

• R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, Strict constraint qualifications and sequential optimality conditions for constrained optimization, Optimization Online 5197, 2015 (https://optimization-online.org/wp-content/uploads/2015/11/5197.pdf); Math. Oper. Res. 43(3), 2018. https://doi.org/10.1287/moor.2017.0879
• R. Andreani, J. M. Martínez, B. F. Svaiter, A new sequential optimality condition for constrained optimization and algorithmic consequences, SIAM J. Optim. 20(6):3533–3554, 2010. https://doi.org/10.1137/090777189
• R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, A cone-continuity constraint qualification and algorithmic consequences, SIAM J. Optim. 26(1):96–110, 2016. https://doi.org/10.1137/15M1008488
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• F. J. Gould, J. W. Tolle, A necessary and sufficient qualification for constrained optimization, SIAM J. Appl. Math. 20(2):164–172, 1971. https://doi.org/10.1137/0120021

Motivation

Stochastic dual dynamic programming (SDDP) and its relatives are the standard algorithms for multistage stochastic programs: hydro-thermal scheduling, energy storage and long-horizon capacity planning are solved with them in industry. They approximate each future cost function from below by a maximum of affine cuts, compute new cuts only at a few randomly chosen nodes of the scenario tree, and use the current approximations to simulate decisions forward. Whether such sampled cutting-plane schemes converge, and in what sense, decides whether their bounds can be trusted.

• Pereira and Pinto (1991) introduced SDDP for multistage stochastic linear programs.
• Chen and Powell (1999) proposed CUPPS, which samples a single scenario per iteration.
• Philpott and Guan (2008) proved almost-sure convergence in finitely many iterations of DOASA and SDDP-type methods for linear stage problems with stagewise independent data, using the finiteness of the set of possible cuts.
• Girardeau, Leclère and Philpott (2015) removed linearity: stage problems are convex with compact feasible sets, the data need not be stagewise independent, and the node selection is any τ-admissible random process. Convergence is then asymptotic, not finite.

This mission formalizes the stochastic part (§3) of the 2015 paper. Mission 1 of the series covers its deterministic part (§2).

Setting

A finite scenario tree has nodes $\mathcal N$, root $0$, parent map $p$, children $r(n)$, leaves $\mathcal L$, and node probabilities $\Phi_n>0$ with $\Phi_0=1$ and $\Phi_n=\sum_{m\in r(n)}\Phi_m$. Every node $m\neq0$ carries a control multifunction $\mathcal U_m:\mathbb R^d\rightrightarrows\mathbb R^p$, a cost $C_m(x,u)\in\mathbb R\cup\{+\infty\}$ and linear dynamics $x_m=f_m(x_{p(m)},u_m)$; every node carries a compact convex stock set $\mathcal X_n$; leaves carry final costs $V_m$. The future cost functions are defined backwards by (20):

$$V_n(x)=\sum_{m\in r(n)}\frac{\Phi_m}{\Phi_n}\min_{u\in\mathcal U_m(x)}\underbrace{C_m(x,u)+V_m\big(f_m(x,u)\big)}_{W_m(x,u)},\qquad x\in\mathcal X_n .$$

Assumptions $(H_2)$ ask for convex, lower semicontinuous, proper costs, convex compact-valued convex multifunctions $\mathcal U_m$, Lipschitz final costs, and an extended relatively complete recourse condition: feasibility and finite cost on a $\delta$-neighbourhood of every $\mathcal X_n$.

The algorithm keeps approximations $V^{k}_n$, starting from $V^{-1}_n\equiv-\infty$. At iteration $k$ it simulates the whole tree with $V^{k-1}$, producing stocks $x^k_n$ and controls $u^k_m$. Cuts $\theta^k_n+\langle\beta^k_n,\cdot-x^k_n\rangle$ are computed at the selected nodes by solving the stage problems (21) at their children and averaging optimal values and Lagrange multipliers with weights $\Phi_m/\Phi_n$. Every approximation is then updated by (22), $V^k_n=\max(V^{k-1}_n,\text{cut})$. The selections $y^k_n\in\{0,1\}$ form a random process. It is τ-admissible (Definition 1) when, inside each block of $\tau$ iterations, cuts are computed backwards along the tree, and when the block indicators $\tilde y^k_n=\max_{\kappa<\tau}y^{k\tau+\kappa}_n$ are i.i.d. in $k$, independent of the past, and equal to $1$ with positive probability.

Formalization targets

Goal: Theorem 3.1

Under $(H_2)$ and a τ-admissible selection process, almost surely, for every non-leaf node $n$ and every node $n$ respectively,

$$\lim_{k\to\infty}\sum_{m\in r(n)}\frac{\Phi_m}{\Phi_n}W_m\big(x^{k\tau}_n,u^{k\tau}_m\big)-V_n\big(x^{k\tau}_n\big)=0,\qquad \lim_{k\to\infty}V_n\big(x^{k\tau}_n\big)-V^{k\tau}_n\big(x^{k\tau}_n\big)=0 .$$

The decisions become optimal for the true problem and the approximations become exact at the visited stocks. Nothing is claimed about exactness elsewhere in the state space.

Milestones

• (26): every new cut is tight at the stock where it is computed.
• Lemma 3.1 (i)–(iii): the $V_n$ are convex and Lipschitz on $\mathcal X_n$; the approximations are lower bounds; finite approximations are uniformly Lipschitz.
• Lemma 3.2: exact approximations at the children make the decisions at a node asymptotically optimal.
• Lemma 5.3: under Definition 1 (i), a node selected inside a block is visited at the stock and with the approximation it had at the start of the block.
• Lemma 5.4: the terms of an i.i.d. sequence selected by a predictable rule are again i.i.d. with the same law.
• (32): exactness along the iterations at which a node is selected.

Significance

The theorem covers in one statement CUPPS (1-admissible), DOASA and SDDP ($(T-1)$-admissible), and many other sampling schemes, for stage problems that are convex rather than linear and for scenario trees without stagewise independence. It shows that the lower bound produced by these methods converges to the optimal value along the simulated trajectories.

The result is proved on paper. It is not formalized anywhere: no proof assistant library contains SDDP-type algorithms for convex stage problems. This mission makes the algorithm, the τ-admissibility notion and the convergence statement precise. Formalizing them corrects slips of the printed statements: the lower-bound property holds on the affine hull of $\mathcal X_n$ only, the boundedness of the cut slopes concerns finite cuts only, and the theorem's two limits concern different node sets. The rest of the work is the formalization of the published proof.

Difficulty

The deterministic argument (mission 1) shows exactness at stage $t$ from exactness at stage $t+1$ along the whole iteration sequence. In the stochastic case a node is updated only at the random iterations at which it is selected, while its stock $x^{k\tau}_n$ moves at every iteration. Exactness along the selected iterations (32) does not transfer to the others: a selection rule that updated a node only when its stock lay in a given region would leave the approximation inexact elsewhere. The proof has to show that the iterations at which the approximation is still $\varepsilon$-inexact are, by independence, selected with positive frequency. This requires the event "$k$ is $\varepsilon$-inexact" to be measurable with respect to the past selections, so the algorithm's choices among multiple minimisers and multipliers must be deterministic (footnote 6). It also requires the optional-skipping Lemma 5.4 and the strong law of large numbers. The first idea of conditioning on the stocks directly fails because the stocks depend on all past selections.

Formalization scope

• Spaces and values. Stocks in EuclideanSpace ℝ (Fin d), controls in EuclideanSpace ℝ (Fin p). Costs and value functions take values in EReal; convexity is epigraph convexity; $V_n=+\infty$ off $\mathcal X_n$; the initial approximation is $-\infty$. Limits are EReal limits, so convergence to $0$ forces the differences to be finite eventually.
• Tree. The platform definition StochasticProg.Multistage.Tree (a finite rooted tree with stages) is referenced; leaves, ascendents and node probabilities are defined on it. Costs are indexed by the child node as in (19a) and (20).
• Standing assumptions, all disclosed in the items: $(H_2)(1)$–$(6)$ clause by clause, with the full ball $B(\delta)$ of $(H_2)(6)$ as printed; $x_0\in\mathcal X_0$; $\Phi$ are node probabilities.
• Algorithm. A run is a predicate on the generated data (stocks, controls, cut values and slopes, approximations). Minimisers, Lagrange multipliers and subgradients are chosen by fixed rules, functions of the stage problem only (footnote 6), so a run is determined by its selection path. Lagrange multipliers of (21b) are encoded by the subgradient inequality of the optimal value of (21) on $\operatorname{Aff}(\mathcal X_n)$, with the multiplier in its direction space. The Lean index is shifted: Vc k is the paper's $V^{k-1}$.
• Selections. $y^k$ are measurable Bool-valued maps on a probability space; Definition 1 (i) holds on every path; (ii) is per node, i.i.d. in $k$ and independent of $\sigma(y^{k'}:k'<k\tau)$, with no independence across nodes.
• Ruling out trivializations. The goal's hypotheses are only $(H_2)$, the choice rules, a run on every sample path, measurable selections and τ-admissibility. The companion statement run_exists shows that runs exist for every selection path, and a sanity check shows $(H_2)$ and τ-admissibility are satisfiable, so the goal is not vacuous. Its conclusion mentions none of the proof's auxiliary objects.
• Infrastructure. The development needs marginal functions of convex problems over convex multifunctions, subdifferentiability of finite convex functions on affine hulls, Lipschitz bounds for maxima of affine functions, and the optional-skipping Lemma 5.4. Lemma 5.4 is a self-contained probability statement and is reusable on its own. Lemma 5.2 of the paper (a Dini-type lemma) is posed in mission 1. Proofs of any milestone, and of auxiliary lemmas on EReal-valued convex functions, are welcome.

Selected references

• P. Girardeau, V. Leclère, A. B. Philpott, On the Convergence of Decomposition Methods for Multistage Stochastic Convex Programs, Mathematics of Operations Research 40(1), 2015. https://doi.org/10.1287/moor.2014.0664 (author's version: https://hal.science/hal-01208295v1)
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Operations Research Letters 36(4), 2008. https://doi.org/10.1016/j.orl.2008.01.013
• Z. L. Chen, W. B. Powell, Convergent cutting-plane and partial-sampling algorithm for multistage stochastic linear programs with recourse, Journal of Optimization Theory and Applications 102(3), pp. 497–524, 1999 (reference [1] of the paper).
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52, 1991. https://doi.org/10.1007/BF01582895

Motivation

In distributed optimization a network of $m$ agents minimizes a sum of private functions while each agent talks only to its neighbours. Applications include federated and decentralized learning, sensor networks and multi-robot systems, where the data cannot be pooled at one site. Many of these networks are directed (communication links are one-way, for instance because transmission powers differ) and time-varying (links come and go). On such networks no doubly stochastic mixing matrix is available in general, and plain averaging drifts toward a weighted average instead of the true one. The push-sum protocol corrects this drift by carrying an auxiliary weight $\phi_i$ at every agent (Kempe, Dobra & Gehrke 2003; Nedić & Olshevsky 2015).

Y. Sun, A. Daneshmand and G. Scutari (arXiv:1905.02637v2) analyse SONATA, a gradient-tracking method in which each agent solves a strongly convex surrogate of its local problem instead of taking a gradient step, for composite problems (a convex, possibly nonsmooth regulariser $G$ and a convex constraint set). They prove linear convergence on undirected graphs (their Theorem 3.9, the companion mission of this series) and, in Section 4, for a push-sum version over time-varying digraphs (Theorem 4.5). This mission formalizes the second result.

Timeline. Gradient tracking with push-sum over time-varying digraphs appears in NEXT/SONATA (Di Lorenzo & Scutari 2016; Scutari & Sun 2019), where convergence was proved without rates for nonconvex problems. Linear rates for smooth unconstrained strongly convex problems over time-varying digraphs were obtained for Push-DIGing (Nedić, Olshevsky & Shi 2017). Sun, Daneshmand and Scutari (2019, revised 2020) extend the linear rate to the composite, constrained setting with surrogates, and require only the average $F$, not every $f_i$, to be strongly convex.

Setting

Problem (P). Agent $i\in[m]$ holds $f_i:\mathbb R^d\to\mathbb R$; the agents solve

$$\min_{x\in\mathcal K}U(x)\triangleq F(x)+G(x),\qquad F=\frac1m\sum_{i=1}^mf_i .$$

Assumption A: $\mathcal K$ is nonempty, closed and convex; each $f_i$ is twice differentiable on an open set $\mathcal O\supseteq\mathcal K$ and convex; $\mu I\preceq\nabla^2F(x)\preceq LI$ on $\mathcal K$ with $\mu>0$; $G$ is convex on $\mathcal K$. $x^\star$ is the solution and $U^\star=U(x^\star)$.

Surrogates (Assumption C). Each agent has $\tilde f_i(x;z)$, $C^2$ on $\mathcal O\times\mathcal O$, with $\nabla\tilde f_i(x;x)=\nabla f_i(x)$, $\nabla\tilde f_i(\cdot;x)$ $\tilde L_i$-Lipschitz and $\tilde f_i(\cdot;x)$ $\tilde\mu_i$-strongly convex on $\mathcal K$. Constants $D^\ell_i\le D^u_i$ satisfy $D^\ell_iI\preceq\nabla^2\tilde f_i(x;y)-\nabla^2F(x)\preceq D^u_iI$ on $\mathcal K\times\mathcal K$ (15); $\tilde\mu_{\rm mn}=\min_i\tilde\mu_i$, $D^\ell_{\rm mn}=\min_iD^\ell_i$.

Network (Assumption B′). At time $\nu$ the digraph $\mathcal G^\nu$ has edge set $\mathcal E^\nu$; $(i,j)\in\mathcal E^\nu$ is a link from $i$ to $j$. There is an integer $B>0$ such that the union of the edge sets over every window $[\nu B,(\nu+1)B-1]$ is strongly connected.

Weights (Assumption E). $C^\nu=(c^\nu_{ij})$ is column stochastic, $c^\nu_{ii}\ge c_\ell>0$, $c^\nu_{ij}\ge c_\ell$ if $(j,i)\in\mathcal E^\nu$ and $c^\nu_{ij}=0$ for other $j\ne i$.

Algorithm 3. From $x_i^0\in\mathcal K$, $y_i^0=\nabla f_i(x_i^0)$, $\phi_i^0=1$, each agent computes

$$\hat x_i^\nu\in\operatorname*{argmin}_{x_i\in\mathcal K}\ \tilde f_i(x_i;x_i^\nu)+(y_i^\nu-\nabla f_i(x_i^\nu))^\top(x_i-x_i^\nu)+G(x_i),\qquad x_i^{\nu+1/2}=x_i^\nu+\alpha(\hat x_i^\nu-x_i^\nu),$$

then $\phi_i^{\nu+1}=\sum_jc^\nu_{ij}\phi_j^\nu$, $x_i^{\nu+1}=\frac1{\phi_i^{\nu+1}}\sum_jc^\nu_{ij}\phi_j^\nu x_j^{\nu+1/2}$ and $y_i^{\nu+1}=\frac1{\phi_i^{\nu+1}}\sum_jc^\nu_{ij}(\phi_j^\nu y_j^\nu+\nabla f_j(x_j^{\nu+1})-\nabla f_j(x_j^\nu))$.

The analysis uses the weighted gap $p_\phi^\nu=\sum_i\phi_i^\nu(U(x_i^\nu)-U^\star)$, the tracking error $\delta_i^\nu=\nabla F(x_i^\nu)-y_i^\nu$, and the consensus errors $x^\nu_{\phi,\perp}$, $y^\nu_{\phi,\perp}$ measured against the $\phi$-weighted averages.

Formalization targets

Goal: Theorem 4.5

If $\tilde\mu_{\rm mn}\ge D^\ell_{\rm mn}$, there is $\bar\alpha\in(0,1]$ such that for every $\alpha\in(0,\bar\alpha)$, every run and every agent $i$,

$$\exists\,C,\ z\in[0,1):\qquad|U(x_i^\nu)-U^\star|\le C\,z^\nu\quad\forall\nu .$$

The goal is qualitative: neither $\bar\alpha$ nor the rate is fixed, so it survives any improvement of the constants.

Milestones

In attack order: the weighted tracking identity (74) and its consequence $\bar y^\nu_\phi=\overline{\nabla f}^\nu$; the bounds $\phi_{lb}\le\phi_i^\nu\le\phi_{ub}$ (p. 29); the per-agent descent inequality (Lemma I.1); the lower bound on the weighted step length (Lemma I.2); the tracking-error bound $\|\delta^\nu\|^2\le8L^2_{\rm mx}\|x^\nu_{\phi,\perp}\|^2+2\|y^\nu_{\phi,\perp}\|^2$ (Lemma I.3); the contraction $p_\phi^{\nu+1}\le\sigma(\alpha)p_\phi^\nu+\eta(\alpha)\phi_{ub}(\cdots)$ (Proposition 4.1); the bound of $\|d^\nu\|^2$ by $p_\phi^\nu$ and $\|y^\nu_{\phi,\perp}\|^2$ (Proposition 4.3).

Significance

Theorem 4.5 gives a linear rate for distributed composite and constrained optimization over time-varying directed networks. Two features matter: the individual $f_i$ need not be strongly convex, and the surrogates cover proximal-gradient steps, DANE-type local solves and mirror-descent steps under one analysis. The rate depends on the surrogate-mismatch constants $D_i$, which is the mechanism by which the paper shows that local computation helps when the $f_i$ are similar.

The result is proved in the paper; the proof of Theorem 4.5 refers to the undirected argument, and several of its supporting statements (Propositions 4.1 and 4.3) have their proofs omitted or relegated to the supplement, with consensus estimates quoted from Scutari & Sun (2019). To our knowledge none of it is machine-checked. A formalization produces a checked proof of the directed result together with reusable statements about push-sum weights over $B$-strongly connected digraphs.

Difficulty

The obvious argument is to repeat the undirected proof with weighted averages. Two steps fail. First, the $\phi$-weighted average is not the minimiser of $\sum_i\|x_i-c\|^2$, so consensus errors measured against it lose a constant (the 8 in Lemma I.3 instead of 4), and every passage between weighted and unweighted sums needs the bounds $\phi_{lb}\le\phi_i^\nu\le\phi_{ub}$, which rest on a product-of-matrices argument over windows of length $(m-1)B$. Second, the matrices change with $\nu$, so there is no single contraction factor; geometric decay of the consensus errors holds only over windows, and the coupling between the optimality gap, the consensus errors and the step lengths must be closed by a small-gain argument whose constants are uniform over the run. The step-size threshold must not depend on the starting point.

Formalization scope

Points are EuclideanSpace ℝ (Fin d); stacked vectors are Fin m → ℝ^d with the Euclidean norm $\|v\|^2=\sum_i\|v_i\|^2$, never Lean's sup norm. The Hessian is the derivative of the gradient, and Loewner bounds are quadratic-form inequalities. Time is 0-based. A run is a relational predicate: $\hat x_i^\nu$ is some minimizer of the subproblem, whose existence the paper takes for granted; $x^\star$ is assumed to exist. The divisions by $\phi_i^{\nu+1}$ appear as in the paper and are genuine, since Assumption E keeps the weights positive. $f_i$ is convex on $\mathcal K$ and locally convex on $\mathcal O$ (positive semidefinite Hessian; $\mathcal O$ need not be convex), $\tilde\mu_i>0$, and $D^\ell_i,D^u_i$ are parameters: the statements hold for every valid choice. The graph sequence, $B$, $c_\ell$ and the matrices $C^\nu$ come before $\bar\alpha$; the starting point and the run come after $\alpha$. The bounds on $\phi$ are stated for $m\ge2$ (the printed $\phi_{ub}$ is $0$ at $m=1$), and positivity of $\sigma(\alpha)$ is claimed only when $D_{\rm mx}>0$ or $\alpha<1$.

The following do not count as a formalization of the goal: an unsatisfiable run predicate (a sorry-free verification file exhibits a run satisfying every hypothesis), a $\bar\alpha$ chosen after the run, the $\phi$ bounds or a contraction factor assumed in place of Assumptions B′ and E, and dropping the $1/\phi_i^{\nu+1}$ normalisation.

Not posed: the explicit rate (Theorem III.1), the complexity corollaries, and the consensus estimates Lemma 4.2 and Proposition 4.4, whose constants $c_0,\rho_B$ come from Scutari & Sun (2019) (as printed, $c_0$ is negative). A complete development needs Taylor expansions with integral remainder along segments, first-order optimality for composite problems on convex sets, and products of column-stochastic matrices over strongly connected windows; the last is reusable for any push-sum method. Contributions to any milestone, and to the missing consensus estimates as auxiliary lemmas, are welcome.

Selected references

• Y. Sun, A. Daneshmand, G. Scutari, Distributed Optimization Based on Gradient-tracking Revisited: Enhancing Convergence Rate via Surrogation, arXiv:1905.02637v2, 2020; SIAM J. Optim. 32(2), 2022. https://arxiv.org/abs/1905.02637v2
• G. Scutari, Y. Sun, Distributed nonconvex constrained optimization over time-varying digraphs, Math. Program. 176, 2019. https://doi.org/10.1007/s10107-018-01357-w
• P. Di Lorenzo, G. Scutari, NEXT: In-Network Nonconvex Optimization, IEEE Trans. Signal Inf. Process. Netw. 2(2), 2016. https://doi.org/10.1109/TSIPN.2016.2524588
• A. Nedić, A. Olshevsky, W. Shi, Achieving Geometric Convergence for Distributed Optimization over Time-Varying Graphs, SIAM J. Optim. 27(4), 2017. https://doi.org/10.1137/16M1084316
• A. Nedić, A. Olshevsky, Distributed optimization over time-varying directed graphs, IEEE Trans. Autom. Control 60(3), 2015. https://doi.org/10.1109/TAC.2014.2364096
• D. Kempe, A. Dobra, J. Gehrke, Gossip-based computation of aggregate information, FOCS 2003. https://doi.org/10.1109/SFCS.2003.1238221