Operations Research

Motivation

Designing a revenue-maximizing auction for several items is hard once buyers have budgets. Myerson's optimal auction (Myerson 1981) solves the single-item problem without budgets, under a known prior on the buyers' values. With several items, correlated values or budget constraints, no comparable characterization is known, and the Bayesian formulation requires a prior the seller rarely has.

Bandi and Bertsimas (2014) replace the prior by an uncertainty set: a set $\mathcal U$ of valuation matrices that the seller considers possible. The seller then maximizes worst-case revenue over $\mathcal U$, subject to incentive compatibility, budget feasibility and individual rationality. This is the approach of robust optimization (Ben-Tal and Nemirovski 1998; Bertsimas and Sim 2004) applied to mechanism design. The paper's central object is a mechanism built from linear optimization problems, the robust optimal mechanism ROM. It looks like a Vickrey–Clarke–Groves mechanism with reservation prices that depend on both the buyer and the item.

Setting

There are $n$ buyers $\mathcal N=\{1,\dots,n\}$ and $m$ divisible items $\mathcal M=\{1,\dots,m\}$. A valuation vector is an $n\times m$ real matrix $\mathbf v=(v_{ij})$, with $v_{ij}$ buyer $i$'s value for one unit of item $j$. The uncertainty set $\mathcal U$ is a set of such matrices, and $B_1,\dots,B_n$ are public budgets. Writing $(\mathbf u_i,\mathbf v_{-i})$ for $\mathbf v$ with row $i$ replaced by $\mathbf u_i$, a mechanism assigns to each bid vector $\mathbf v\in\mathcal U$ an allocation $x^{\mathbf v}\ge 0$ and payments $p^{\mathbf v}$. It is feasible for the robust auction LP (5) if, for all $\mathbf v\in\mathcal U$ and $i\in\mathcal N$:

• (7) $\sum_i x^{\mathbf v}_{ij}\le 1$ for every item $j$;
• (8) $\sum_j v_{ij}x^{(\mathbf u_i,\mathbf v_{-i})}_{ij}-p^{(\mathbf u_i,\mathbf v_{-i})}_i\le\sum_j v_{ij}x^{\mathbf v}_{ij}-p^{\mathbf v}_i$ whenever $(\mathbf u_i,\mathbf v_{-i})\in\mathcal U$ (incentive compatibility);
• (9) $p^{\mathbf v}_i\le B_i$ (budget feasibility);
• (10) $p^{\mathbf v}_i\le\sum_j v_{ij}x^{\mathbf v}_{ij}$ (individual rationality).

ROM has two stages. ROM.a runs before any bid. It picks a valuation $\mathbf z\in\mathcal U$ and a nominal allocation $\mathbf x^*$ solving the robust optimization problem (12). For each buyer it picks a minimizer $\tilde{\mathbf u}^i\in\mathcal U$ of $\sum_j x^*_{ij}u_{ij}$ (14), and an optimal solution $(\xi^*,\eta^*,\theta^*)$ of a linear program (13). It then sets reservation prices $r^*_{ij}=\xi^*_j+\eta^*_iz_{ij}+\theta^*_iz_{ij}$ (15). ROM.b runs on the bids $\mathbf v$:

• it maximizes $\sum_{i,j}y_{ij}(v_{ij}-r^*_{ij})$ over a polyhedron $\mathcal P$ (16), (18), and for each buyer $k$ the same objective without buyer $k$ over a polyhedron $\mathcal Q_k$ (17), (19);
• it allocates $a^{\mathbf v}=\mathbf x^*+\mathbf y^{\mathbf v}$ (20) and charges VCG-type payments $p^{\mathbf v}$ (21).

The Lean development uses the same names: ROMData for the chosen optimizers, IsROMa, IsROM, rStar, PSet, QSet, alloc, pay, and IsFeasibleMechanism for (7)–(10).

Formalization targets

Goal: ROM is feasible for (5)

For every uncertainty set of nonnegative valuation matrices, every nonnegative budget vector and every choice of optimal solutions of (12), (13), (14), (16), (17):

$$(a,p)\ \text{satisfies (7)},\ a\ge 0,\ \text{(8)},\ \text{(9)},\ \text{(10) on } \mathcal U.$$

This is the feasibility half of the paper's Theorem 1; its proof (p. 1025) says "the feasibility follows from Propositions 3–5".

Milestones

• Proposition 2 (p. 1020): the relations (22)–(27) among $\mathbf z,\mathbf x^*,\xi^*,\eta^*,\theta^*,r^*$, among them $x^*_{ij}r^*_{ij}=x^*_{ij}z_{ij}$ and $\sum_jx^*_{ij}r^*_{ij}\le B_i$.
• Proposition 3 (p. 1021): ROM satisfies (8).
• Proposition 4 (p. 1022): ROM satisfies (9).
• Proposition 5 (p. 1023): ROM satisfies (10).

Significance

The result shows that a mechanism specified by the paper's optimization problems is incentive compatible, budget feasible and individually rational over an arbitrary uncertainty set. No distributional assumption is made, and multiple items and budgets are allowed. Proposition 2 also records the identity between the total reserved revenue and the optimal value of the auxiliary program (13).

Status. The paper's main claim, Theorem 1, says that ROM is optimal for (5), i.e. that it maximizes worst-case revenue. That claim is false as printed, and so is Proposition 6 (the worst case of ROM is attained at $\mathbf z$). Small counterexamples refute both:

• with one buyer, one item, $\mathcal U=\{1,2\}$ and a large budget, some choice of optimal dual solution in (13) makes ROM's worst-case revenue $0$, while a posted price of $1$ earns $1$;
• with two buyers, one item and $\mathcal U=\{(1,2),(2,1)\}$, full surplus extraction earns $2$, while ROM earns at most $1$ for every choice of optimizers.

The feasibility half is true, and this mission formalizes exactly that half. No result of this paper is on Prove2Me yet, and no machine-checked proof of it is known.

Difficulty

The difficulty lies in the definitions and in how many problems interlock, not in any single deep step. ROM is defined through five optimization problems, none with a unique solution. The payments (21) of a buyer depend on the optimizer chosen in (17), which may differ between a truthful and a deviating bid vector. Incentive compatibility must therefore rest on properties of optimal values, not of particular optimizers. The robust constraints of (12) and (18) range over the whole of $\mathcal U$, which may be infinite. Relating $\mathbf x^*$ to the multipliers of (13) requires replacing the robust constraint by a finite one before linear programming duality applies. Budget feasibility requires comparing two polyhedra whose budget rows differ by a term involving $\theta^*$ and $\tilde{\mathbf u}^i$. Neighbouring statements in the same section (Theorem 1, Proposition 6) are false, so no step can be taken on the paper's word.

Formalization scope

Buyers are Fin n and items Fin m. A valuation matrix is Fin n → Fin m → ℝ, the uncertainty set an arbitrary Set of them, and $(\mathbf u_i,\mathbf v_{-i})$ is Function.update v i u_i. Every optimizer is a field of ROMData. IsROMa/IsROM assert optimality for exactly the page's problems, built from the same $\mathbf z$, $\mathbf x^*$, $\theta^*$, $\tilde{\mathbf u}^i$. Every statement holds for every such choice, never for one canonical selection. Allocation and payments are $0$ for bids outside $\mathcal U$ (step 1 of ROM.b); constraints (7)–(10) are imposed only on $\mathcal U$.

Committed conventions and additions to the page:

• Nonnegative valuations ($u_{ij}\ge 0$ for $\mathbf u\in\mathcal U$) and nonnegative budgets are standing assumptions the paper uses without stating. The proof of Proposition 5 invokes "$\tilde u_{kj}$ ... nonnegative", and (12) is infeasible for negative budgets. Both are explicit hypotheses.
• No finiteness, boundedness or convexity of $\mathcal U$ is assumed. Existence of the optimizers is part of the hypothesis IsROM, and its satisfiability has been checked on a one-buyer, one-item instance.
• Payments may be negative; no $p\ge 0$ is imposed, as (5) has none.
• In $\mathcal Q_k$ row $k$ is only nonnegative; it enters neither constraint nor objective.
• Printed slip corrected: in (18) the term $\sum_jx^*_{kj}\theta^*_i\tilde u^i_j$ has an unbound $k$ and is read as $\sum_jx^*_{ij}\theta^*_i\tilde u^i_j$, matching (13) and (34).
• The paper's optimality claims (Theorem 1, Proposition 6), the objective (5)–(6) and the dual (11) are deliberately not part of the mission.

A trivializing formalization is ruled out: the optimizers are not fixed to degenerate values (such as $\theta^*=0$ or a canonical $\mathbf y$), constraint (8) ranges over all deviations that stay in $\mathcal U$ with the true values multiplying both allocations, and the hypotheses are jointly satisfiable.

A complete development needs finite-dimensional LP duality and complementary slackness (for Proposition 2), and finite-sum manipulation over Fin n with one index removed. LP duality lemmas in matrix form are reusable well beyond this mission. Contributions are welcome on any milestone, and on general LP duality statements stated in a form that applies directly to (33)–(34).

Selected references

• S. Bandi, D. Bertsimas, Optimal Design for Multi-Item Auctions: A Robust Optimization Approach, Mathematics of Operations Research 39(4):1012–1038, 2014. https://doi.org/10.1287/moor.2014.0645
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1):58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• A. Ben-Tal, A. Nemirovski, Robust Convex Optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• D. Bertsimas, M. Sim, The Price of Robustness, Operations Research 52(1):35–53, 2004. https://doi.org/10.1287/opre.1030.0065

Motivation

Optimization under uncertainty usually fixes one probability distribution $\mathbb P$ for the uncertain data and optimizes an expected payoff, or fixes a set $\mathcal Q$ of distributions and protects against the worst one (robust optimization). The first is sensitive to a misspecified $\mathbb P$; the second can be very conservative, because it treats a barely plausible distribution exactly like the nominal one. Ben-Tal, Bertsimas and Brown (Oper. Res. 58(4), 2010) propose a graded alternative, the soft robust model: the decision maker accepts a loss of at most $\varepsilon$ in expected payoff under every distribution of a set $\mathcal Q(\varepsilon)$, simultaneously for all levels $\varepsilon$ up to a budget $\delta$. Larger sets of distributions are allowed a larger shortfall.

The paper's central result, Theorem 2.1, shows that this model is exactly a constraint on a convex risk measure in the sense of Föllmer and Schied (Finance Stoch. 6, 2002), and that every normalized convex risk measure arises from some soft robust model. This connects distributionally robust optimization with the theory of monetary risk measures, and gives a tractable convex reformulation of soft robust constraints. Related earlier work connected coherent risk measures with standard robust optimization (Bertsimas and Brown, Oper. Res. 57(6), 2009).

Setting

Let $(\Omega,\mathcal F)$ be a measurable space and $\mathcal P$ the set of all probability measures on it. A decision $x$ ranges over a nonempty, closed, convex set $X\subseteq\mathbb R^n$; a random variable $u:\Omega\to\mathbb R^m$ carries the uncertain parameters, and $f(x,u(\omega))$ is the payoff, concave in $x\in X$ for every $\omega$. For each $x\in X$ the random variable $f(x)=f(x,u(\cdot))$ is assumed bounded and measurable.

A family of measures is $\mathbf Q=\{\mathcal Q(\varepsilon)\subseteq\mathcal P:\varepsilon\ge0\}$. It is nondecreasing if $\mathcal Q(\varepsilon_1)\subseteq\mathcal Q(\varepsilon_2)$ for $\varepsilon_1\le\varepsilon_2$, and convex if $\mathbb Q_i\in\mathcal Q(\varepsilon_i)$ implies $\lambda\mathbb Q_1+(1-\lambda)\mathbb Q_2\in\mathcal Q(\lambda\varepsilon_1+(1-\lambda)\varepsilon_2)$ for $\lambda\in[0,1]$. The standing assumptions are that $\mathbf Q$ is nondecreasing and convex and that $\mathcal Q(0)\neq\emptyset$. The soft robust feasible set at level $\delta\ge0$ is

$$X^Q(\delta)=\Big\{x\in X:\ \inf_{\mathbb Q\in\mathcal Q(\varepsilon)}\mathbb E_{\mathbb Q}[f(x)]\ \ge\ -\varepsilon\quad\forall\,\varepsilon\in[0,\delta]\Big\}.\tag{5}$$

A risk measure, on the space $\mathcal Y$ of bounded payoffs, is a map $\rho:\mathcal Y\to\mathbb R$ with $Y_1\ge Y_2\Rightarrow\rho(Y_1)\le\rho(Y_2)$ and $\rho(Y+c)=\rho(Y)-c$ for $c\in\mathbb R$; it is convex if $\rho(\lambda Y_1+(1-\lambda)Y_2)\le\lambda\rho(Y_1)+(1-\lambda)\rho(Y_2)$. It is generated by a convex penalty $\alpha:\mathcal P\to[0,\infty]$ if $\rho(Y)=\sup_{\mathbb Q\in\mathcal P}\{-\mathbb E_{\mathbb Q}[Y]-\alpha(\mathbb Q)\}$, and normalized if in addition $\alpha(\mathbb Q)=0$ for some $\mathbb Q$. A family and a penalty determine each other:

$$\alpha^Q(\mathbb Q)=\inf\{\varepsilon\ge0:\mathbb Q\in\mathcal Q(\varepsilon)\},\qquad \mathcal Q^\alpha(\varepsilon)=\{\mathbb Q\in\mathcal P:\alpha(\mathbb Q)\le\varepsilon\},$$

and $\rho^Q$ denotes the risk measure generated by $\alpha^Q$.

Formalization targets

Goal: Theorem 2.1 for $\delta>0$

For every nondecreasing, convex family $\mathbf Q$ with $\mathcal Q(0)\ne\emptyset$, $\rho^Q$ is a convex risk measure generated by the normalized convex penalty $\alpha^Q$, the minimum below is attained for every $x\in X$, and

$$X^Q(\delta)=\Big\{x\in X:\ \min_{\lambda\ge0}\Big\{\lambda\delta+(\lambda+1)\,\rho^Q\Big(\frac{f(x)}{\lambda+1}\Big)\Big\}\le0\Big\}.\tag{6}$$

Conversely, for every convex risk measure $\rho$ generated by a normalized convex penalty $\alpha$, the family $\mathbf Q^\alpha$ is nondecreasing and convex with $\mathcal Q^\alpha(0)\ne\emptyset$, and (6) holds with $\rho$ on the right and $\mathbf Q^\alpha$ on the left.

Milestones: the steps of the proof (p. 1224)

1. The soft robust infimum $\inf\{\mathbb E_{\mathbb Q}[f(x)]+\varepsilon:\varepsilon\in[0,\delta],\ \mathbb Q\in\mathcal Q(\varepsilon)\}$ equals $\inf\{\mathbb E_{\mathbb Q}[f(x)]+\alpha^Q(\mathbb Q):\alpha^Q(\mathbb Q)\le\delta\}$.
2. Strong duality with an attained multiplier: that infimum equals $\max_{\lambda\ge0}\{-\lambda\delta+\inf_{\mathbb Q}\{\mathbb E_{\mathbb Q}[f(x)]+(\lambda+1)\alpha^Q(\mathbb Q)\}\}$.
3. The scaling identity $\inf_{\mathbb Q}\{\mathbb E_{\mathbb Q}[Y]+(\lambda+1)\alpha^Q(\mathbb Q)\}=-(\lambda+1)\rho^Q(Y/(\lambda+1))$.
4. $\rho^Q$ is a convex risk measure generated by the convex, normalized penalty $\alpha^Q$.
5. For a convex normalized $\alpha$, $\mathbf Q^\alpha$ is nondecreasing and convex with $\mathcal Q^\alpha(0)\ne\emptyset$.
6. $\alpha^{Q^\alpha}=\alpha$.

Significance

Theorem 2.1 makes the soft robust constraint usable: the right side of (6) is a single constraint in $(\lambda,x)$, and the function $(\lambda+1)\rho(f(x)/(\lambda+1))$ is jointly convex in $(\lambda,x)$ for $\lambda\ge0$, so soft robust problems are convex programs whenever the risk measure can be evaluated. Read in the other direction, it gives every normalized convex risk measure an interpretation as a graded robustness requirement over the level sets of its penalty, which is how the paper derives soft robust counterparts of optimized certainty equivalents, CVaR and entropic risk, and its later bounds on the probability of a loss.

The theorem is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a Lean development of convex risk measures generated by penalties on an arbitrary measurable space, with extended-valued penalties and mixtures of probability measures, and a one-constraint Lagrange duality theorem over a convex set of probability measures. Mathlib does not currently provide Lagrange duality in this form.

Difficulty

The equalities of the proof read as routine, and two of them are not. The first equality is described as "the definition of $\alpha^Q$", but a measure with $\alpha^Q(\mathbb Q)=\delta$ need not belong to $\mathcal Q(\delta)$, because the infimum defining $\alpha^Q$ need not be attained; the equality relies on the convexity of the family, the nonemptiness of $\mathcal Q(0)$ and the boundedness of $f(x)$. The second equality is Lagrange duality with dual attainment for a convex program whose variable is a probability measure and whose objective and constraint are extended-valued; the classical theorem applies to convex subsets of vector spaces, and transferring it to mixtures of probability measures with $[0,\infty]$-valued penalties is the main formal work. Attainment of the minimum in (6), which the paper asserts by writing "min", is exactly dual attainment and does not follow from the inequality alone.

Formalization scope

The probability measures are ProbabilityMeasure Ω on a measurable space; a family is a map from levels $\varepsilon\in\mathbb R_{\ge0}$ to sets of probability measures, and mixtures are built from the measures $t\,\mathbb Q_1+(1-t)\,\mathbb Q_2$. Penalties, including $\alpha^Q$, take values in $[0,\infty]$, so that a measure in no $\mathcal Q(\varepsilon)$ has penalty $+\infty$; a real-valued $\alpha^Q$ would give such measures penalty $0$ through the junk value of an empty infimum, and is excluded. Risk measures are real functions whose axioms are imposed on bounded measurable payoffs, "generated by" includes the least-upper-bound property of the supremum, and "min" in (6) is attainment on $[0,\infty)$ together with a nonpositive minimum. The decision set and payoff carry the paper's assumptions; concavity of the payoff and closedness and convexity of $X$ are kept although Theorem 2.1 does not use them. Infima over measures in the milestones are taken in the extended reals.

The case $\delta=0$ is excluded. The paper states Theorem 2.1 for $\delta\ge0$, but at $\delta=0$ its proof interchanges a limit in $\lambda$ with a supremum over measures without justification, and (6) fails: on $\Omega=\{a,b\}$ with $\mathcal Q(0)$ the measures giving $a$ mass at most $1/4$ and $\mathcal Q(\varepsilon)$ those giving it mass at most $1/2$ for $\varepsilon>0$, the payoff $f(a)=-2$, $f(b)=1$ is soft robust at level $0$ while the right side of (6) is empty. The goal and the milestones therefore fix $\delta>0$, the case the paper's main argument treats.

A complete development needs: convex risk measures and their generation by penalties, mixtures of probability measures, Lagrange duality with Slater's condition over convex sets of measures, and the scaling identity for $\rho^Q$. The duality theorem and the risk-measure layer are reusable beyond this mission. Contributions of any milestone are welcome, as are general convex-duality lemmas that the strong-duality step can import.

Selected references

• A. Ben-Tal, D. Bertsimas, D. B. Brown, A Soft Robust Model for Optimization Under Ambiguity, Operations Research 58(4, Part 2):1220–1234, 2010. https://doi.org/10.1287/opre.1100.0821
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072
• H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, 2nd ed., de Gruyter, 2004. https://doi.org/10.1515/9783110212075
• D. G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969, Chapter 8.
• D. Bertsimas, D. B. Brown, Constructing Uncertainty Sets for Robust Linear Optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0695

Motivation

Many engineering and operations problems must guarantee that a system operates safely with high probability, when the uncertain parameters $\tilde z$ are only partially known. A chance constraint asks that the safety condition $S\tilde z \le t$ hold with probability at least $1-\epsilon$ for a tolerance $\epsilon \in (0,1)$. When the distribution of $\tilde z$ is itself uncertain, the distributionally robust version asks this for every distribution in an ambiguity set $\mathcal P$ built from what is known: moments, supports, confidence regions. Two problems then arise: computing the worst-case probability $\inf_{\mathbb P \in \mathcal P}\mathbb P[S\tilde z \le t]$ (uncertainty quantification), and optimizing a design $x$ under the constraint $\inf_{\mathbb P \in \mathcal P}\mathbb P[S(x)\tilde z \le t(x)] \ge 1-\epsilon$ (chance constrained programming).

Hanasusanto, Roitch, Kuhn and Wiesemann (Math. Program. 151, 2015) chart which combinations of ambiguity sets and constraint structures admit exact finite reformulations and which are strongly NP-hard. This mission takes the positive core of that chart: for Markov ambiguity sets (first-order moment information plus a conic support), the worst-case probability is the value of a finite conic program, and an individual chance constraint is equivalent to a finite system of linear conic inequalities.

Timeline. Chebyshev-type bounds for worst-case probabilities under moment information go back to the generalized Chebyshev inequalities of Vandenberghe, Boyd and Comanor (2007), and to the duality theory of moment problems summarized by Shapiro (2001). Wiesemann, Kuhn and Sim (2014) introduced the nested conic ambiguity sets used here to evaluate worst-case expectations. Hanasusanto et al. (2015) applied them to worst-case probabilities of polytopes and to chance constraints, proving Theorem 3 (moment problem reformulation) and Theorem 7 (individual chance constraints over Markov sets), together with strong NP-hardness results, such as Theorem 8, showing that the restrictions cannot be dropped.

Setting

Let $\tilde z \in \mathbb R^P$ be the uncertain parameters and $\tilde u \in \mathbb R^Q$ an auxiliary random vector. Fix $A \in \mathbb R^{K\times P}$, $B \in \mathbb R^{K\times Q}$, $b \in \mathbb R^K$, and a confidence set

$$\mathcal C_1 = \{(z,u) : C_1 z + D_1 u \preccurlyeq_{\mathcal K_1} d_1\},$$

where $C_1 \in \mathbb R^{L_1\times P}$, $D_1 \in \mathbb R^{L_1\times Q}$, $d_1 \in \mathbb R^{L_1}$ and $\mathcal K_1$ is a proper cone (closed, convex, pointed, with nonempty interior); $x \preccurlyeq_{\mathcal K} y$ means $y - x \in \mathcal K$, and $\mathcal K_1^\star = \{y : x^\top y \ge 0\ \forall x \in \mathcal K_1\}$ is the dual cone. The Markov ambiguity set is

$$\mathcal P = \{\mathbb P : \mathbb E_{\mathbb P}[A\tilde z + B\tilde u] = b,\ \mathbb P[(\tilde z,\tilde u) \in \mathcal C_1] = 1\},$$

the case $I = 1$, $\underline p_1 = \overline p_1 = 1$ of the paper's nested set (4).

Two regularity notions enter. $\mathcal C_1$ is essentially strictly feasible if it contains a point satisfying all non-polyhedral constraints of its description strictly. The Slater condition (S) for $I = 1$ requires $b$ to lie in the interior of $\{Az + Bu : (z,u) \in \mathcal C_1\}$.

For the safety system $S\tilde z \le t$ with rows $s_j^\top$, $j \in \mathcal J = \{1,\dots,J\}$, let $\mathcal L = \{j : \exists (z,u) \in \mathcal C_1,\ s_j^\top z > t_j\}$ be the rows that can be violated on $\mathcal C_1$. Problem (17) at $I = 1$ maximizes $b^\top\gamma + \underline p_1\lambda - \overline p_1\kappa$ over $\gamma \in \mathbb R^K$, $\lambda,\kappa \ge 0$, $\phi \in \mathcal K_1^\star$ and, for $j \in \mathcal L$, $\tau_j \ge 0$, $\psi_j \in \mathcal K_1^\star$, subject to $\lambda - \kappa + d_1^\top\phi \le 1$, $A^\top\gamma = C_1^\top\phi$, $B^\top\gamma = D_1^\top\phi$ and, for $j \in \mathcal L$, $\lambda - \kappa + d_1^\top\psi_j - \tau_j t_j \le 0$, $A^\top\gamma + \tau_j s_j = C_1^\top\psi_j$, $B^\top\gamma = D_1^\top\psi_j$.

For an individual constraint ($J = 1$) write $s^\top\tilde z \le t$. System (26) asks for $\beta \in \mathbb R$, $\gamma \in \mathbb R^K$, $\phi,\psi \in \mathcal K_1^\star$, $\tau \ge 0$ with

$$\beta + b^\top\gamma \ge (1-\epsilon)\tau,\ \ \beta + d_1^\top\phi \le \tau,\ \ \beta + d_1^\top\psi \le t,\ \ A^\top\gamma = C_1^\top\phi,\ \ B^\top\gamma = D_1^\top\phi,\ \ A^\top\gamma + s = C_1^\top\psi,\ \ B^\top\gamma = D_1^\top\psi.$$

Formalization targets

Goal: Theorem 7 (p. 18)

Under essential strict feasibility of $\mathcal C_1$, (S), and $\epsilon \in (0,1)$,

$$\inf_{\mathbb P \in \mathcal P}\mathbb P[s^\top\tilde z \le t] \ge 1-\epsilon \iff \text{(26) is solvable}.$$

Milestones

1. Theorem 3 (case $I = 1$), sufficiency. Every feasible point of (17) has objective value at most $\mathbb P[S\tilde z \le t]$ for every $\mathbb P \in \mathcal P$.
2. Theorem 3 (case $I = 1$). Under essential strict feasibility and (S),

$$\inf_{\mathbb P \in \mathcal P}\mathbb P[S\tilde z \le t] = \sup\,(17).$$

3. §5 feasibility claim (with (17), case $I = 1$). Under the same hypotheses and $\epsilon \in (0,1)$, the chance constraint holds iff (17) has a feasible point of value at least $1-\epsilon$.
4. Theorem 7, sufficiency. Any solution of (26) certifies $\mathbb P[s^\top\tilde z \le t] \ge 1-\epsilon$ for all $\mathbb P \in \mathcal P$.

Significance

Theorem 7 turns an individual distributionally robust chance constraint over a Markov ambiguity set into finitely many linear conic constraints whose size is polynomial in the data. Since $s(x)$ and $t(x)$ are affine in the design $x$, the chance constrained program becomes a single conic program, solvable with standard software. The paper notes (p. 18) that, apart from the Wasserstein set, all ambiguity sets of its Section 2.3 are Markov sets or intersections of Markov sets with structural ambiguity sets, and Theorem 8 shows that adding a second confidence set already makes the problem strongly NP-hard, so the theorem marks a precise tractability boundary. Theorem 3 underlies the paper's later results and its §5 heuristic for intractable cases.

All five statements are proved in the literature: the paper defers its proofs to an accompanying technical report. None is machine-checked. A formal proof would supply a verified duality theory for moment problems with conic supports, a reusable bridge between semi-infinite constraints and conic certificates, and a verified basis for the paper's hardness results to be stated against.

Difficulty

The sufficiency halves are weak-duality arguments. The converse directions are not: the worst-case probability is an infimum over an infinite-dimensional set of measures, and the conclusion of Theorem 7 requires the dual certificate to be attained, not just approached. Two separate duality steps must both close without a gap and with attainment: the moment problem against its semi-infinite dual, which is where (S) enters, and each semi-infinite constraint against its conic dual over $\mathcal C_1$, which is where essential strict feasibility enters. The event $\{s^\top z > t\}$ is open, so the semi-infinite constraint must also be passed to its closure. Mathlib has neither a duality theorem for moment problems nor conic strong duality with attainment.

Formalization scope

The mission covers Markov ambiguity sets only ($I = 1$, $\underline p_1 = \overline p_1 = 1$). The general nested case of Theorem 3 is not stated, because the paper does not make (S) explicit for $I > 1$. Symmetry and unimodality information, joint chance constraints and the hardness results are out of scope. The paper's proofs are in a technical report that the mission does not use.

Conventions committed to in Lean:

• Vectors are Fin n → ℝ, the single confidence set is index 0 : Fin 1 of the published DRConvexOpt.Reform.AmbData, and its field c 0 is $d_1$.
• Probabilities are μ.real. The local paperAmbiguitySet reuses the published data and confidence-set definitions and requires integrability only of $A\tilde z+B\tilde u$. This makes the expectation condition void when $K=0$, as the paper states.
• "$\inf_{\mathbb P}\mathbb P[E] \ge 1-\epsilon$" is stated as "$1-\epsilon \le \mathbb P[E]$ for every $\mathbb P \in \mathcal P$", so an empty $\mathcal P$ is not mishandled by sInf ∅ = 0.
• "Coincides with the optimal value" is one real number that is both the greatest lower bound of the probabilities and the least upper bound of the objective values of (17).
• Essential strict feasibility is read as: $\mathcal K_1 = \mathcal K_p \cap \mathcal K_n$ for some polyhedral cone $\mathcal K_p$ and closed convex cone $\mathcal K_n$, with a point of $\mathcal C_1$ whose slack lies in $\mathcal K_p \cap \operatorname{int}\mathcal K_n$.
• The decision $x$ is fixed: $s, t$ stand for $s(x), t(x)$, and the program (2) and the set $\mathcal X$ are not formalized.
• $\epsilon \in (0,1)$, proper $\mathcal K_1$, essential strict feasibility and (S) are explicit hypotheses. The sufficiency halves drop (S) and essential strict feasibility, which they do not need.

Replacing essential strict feasibility by full strict feasibility, adding $\tau > 0$ to (26), or imposing the $\psi_j$-constraints for $j \notin \mathcal L$ would each change the theorem and is ruled out. The hypotheses are jointly satisfiable: $\mathcal C_1 = [-1,1]$, $A = 1$, $b = 0$, $\mathcal K_1 = \mathbb R^2_+$ satisfies all of them, with a nonempty ambiguity set.

A complete development needs conic duality with attainment under partial Slater conditions, Lagrangian duality for moment problems, and the reduction of a measure-valued infimum to finitely supported measures. All three are reusable well beyond this mission, and contributions to any of them are welcome.

Selected references

• G. A. Hanasusanto, V. Roitch, D. Kuhn, W. Wiesemann, A distributionally robust perspective on uncertainty quantification and chance constrained programming, Mathematical Programming 151(1), 35–62, 2015. https://doi.org/10.1007/s10107-015-0896-z
• W. Wiesemann, D. Kuhn, M. Sim, Distributionally robust convex optimization, Operations Research 62(6), 1358–1376, 2014. https://doi.org/10.1287/opre.2014.1314
• A. Shapiro, On duality theory of conic linear problems, in: Semi-Infinite Programming, Kluwer, 135–165, 2001. https://doi.org/10.1007/978-1-4757-3403-4_7
• L. Vandenberghe, S. Boyd, K. Comanor, Generalized Chebyshev bounds via semidefinite programming, SIAM Review 49(1), 52–64, 2007. https://doi.org/10.1137/S0036144504440543
• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718829

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