All missions

Motivation

A forward–backward stochastic differential equation (FBSDE) couples a forward diffusion $X$ with a backward equation for a pair $(Y,Z)$ whose terminal value depends on $X_T$. FBSDEs are the probabilistic form of quasilinear parabolic PDEs and appear in stochastic control (the stochastic maximum principle), in mathematical finance (hedging with large investors, stochastic differential utility) and in mean-field games. Their solvability over an arbitrary horizon is delicate: the coupling can make a solution exist only on short time intervals.

Ma, Wu, Zhang and Zhang (arXiv:1110.4658v2, Ann. Appl. Probab. 25 (2015)) reduce well-posedness of a general one-dimensional FBSDE to the behaviour of two scalar dominating ODEs: when these have solutions that stay bounded on $[0,T]$, the FBSDE has a regular decoupling field and a unique solution. Section 5.1 of the paper tests this programme on the simplest class, the linear FBSDE with constant coefficients, and obtains necessary and sufficient conditions. The authors describe these as setting the "limits" for the solvability of general FBSDEs.

Earlier approaches each covered part of the picture: the method of contraction mappings for small time (Antonelli 1993, MR1233625), the four-step scheme for Markovian FBSDEs with regular coefficients (Ma, Protter, Yong 1994, MR1262970), and the method of continuation under monotonicity conditions (Hu, Peng 1995, MR1355060; Peng, Wu 1999, MR1675098; later Yong 1997, MR1440146). The unified approach of the paper contains these as special cases.

Setting

Let $b_1,b_2,b_3,\sigma_1,\sigma_2,f_1,f_2,f_3,h$ be real numbers and consider the linear FBSDE (4.1)

in Case 1, $\sigma_3=0$. Then the two dominating ODEs coincide and become the scalar backward equation

with the cubic

In the Appendix's notation (A.3), $F(y)=f_1+a_1y+a_2y^2+a_3y^3$ with $a_1=f_2+b_1+\sigma_1f_3$, $a_2=b_2+f_3\sigma_2+b_3\sigma_1$, $a_3=\sigma_2b_3$.

A solution on $[0,T]$ of $y_t=h+\int_t^TG(s,y_s)\,ds$ is a function $y$ such that, for every $t\in[0,T]$, $s\mapsto G(s,y_s)$ is integrable on $[t,T]$ and the equation holds at $t$. A bounded solution additionally has $\sup_{[0,T]}|y|<\infty$. In Lean the coefficients form the structure UnifiedFBSDE.Cubic.Coeffs, $F$ is Coeffs.F, and the predicates are IsSolution and IsBoundedSolution.

Formalization targets

Goal: Theorem 5.3

Milestones

1. Lemma 5.1: comparison for backward ODEs. Between a bounded sub-solution and a bounded super-solution, (5.1) has a unique solution.
2. Remark 5.2: a checkable sufficient condition for hypothesis (iv) of Lemma 5.1.
3. Sufficiency of (i), (ii): the solution stays in $[h,\lambda]$ (resp. $[\lambda,h]$).
4. (5.5): under (iii), (5.3) is linear and has a bounded solution.
5. (A.4): if $a_3>0$ and $F$ has no zero in $[h,\infty)$, then $F(y)\ge\varepsilon(y-y_1)^3$ on $[h,\infty)$ for some $\varepsilon>0$, $y_1<h$.
6. (A.6): the explicit comparison solution $\tilde y_t-y_1=(2\varepsilon(t-T)+(h-y_1)^{-2})^{-1/2}$ and its blow-up time $T-1/(2\varepsilon(h-y_1)^2)$.
7. Blow-up by comparison: a continuous $G\ge\varepsilon(y-y_1)^3$ on $[h,\infty)$ admits no solution on $[0,T]$ when $T>1/(2\varepsilon(h-y_1)^2)$.
8. Case 2: if $a_3=0$, $a_2>0$, $F(h)>0$ and $F$ has no zero above $h$, then $F(y)\ge\varepsilon(y-y_1)^2$ on $[h,\infty)$ and (5.3) has no solution for $T$ large.

Companion: Theorem 5.4

For a fixed horizon $T$: (i) $\sigma_2b_3<0$ or $F(h)=0$; (ii) $F(h)>0$, $\sigma_2b_3\le\varepsilon$, $a_2\le\varepsilon$; (iii) $F(h)<0$, $\sigma_2b_3\le\varepsilon$, $a_2\ge-\varepsilon$, with $\varepsilon=\varepsilon(T)$ small. Each guarantees a bounded solution on $[0,T]$.

Significance

Theorem 5.3 turns the existence of a global bounded solution of the dominating ODE into a finite check on a cubic polynomial: the sign of $F(h)$, the location of a real root, and two coefficient identities. Through the paper's main construction, a bounded solution yields a uniformly Lipschitz decoupling field, and hence well-posedness of the linear FBSDE on any horizon. When none of (i)–(iii) holds, the dominating ODE explodes in finite time. This is the sense in which the paper says the constant-coefficient results "more or less set the 'limits'" for the solvability of general FBSDEs: the conditions it later imposes on random coefficients (§5.2, §7) are modelled on the cases (i)–(iii).

The result is proved in the paper: sufficiency on p. 21, necessity in the Appendix (pp. 46–47). To our knowledge none of it is machine-checked. A formalization produces a reusable comparison theorem for scalar backward integral equations with Lipschitz-on-a-band nonlinearities (Lemma 5.1), explicit finite-time blow-up criteria for polynomial ODEs, and a complete, checked classification of global solvability for the cubic Riccati-type equation (5.3).

Difficulty

Sufficiency rests on Lemma 5.1, which requires Carathéodory existence and uniqueness for an equation that is only Lipschitz on a time-dependent band, followed by an integrating-factor comparison argument. Mathlib's Picard–Lindelöf and Gronwall tools are stated for forward equations with continuous right-hand sides, so they need adaptation.

Necessity is a case analysis whose obvious version fails at two points. First, one cannot simply bound $F$ below by $a_3(y-y_1)^3$ using the smallest real root: the intermediate inequality (A.5) as printed points the wrong way for some root orderings, and the correct bound uses the largest root or an infimum over $[h,\infty)$. Second, the blow-up step compares a solution of (5.3) with an explicit exploding solution. This needs the solution to stay above $h$ for the whole interval, which in turn needs continuity of the right-hand side. For a discontinuous right-hand side the comparison fails.

Formalization scope

Time is real, with $0<T$ and $t\in[0,T]$. Solutions are functions $\mathbb R\to\mathbb R$ whose values outside $[0,T]$ are irrelevant. The integral $\int_t^T$ is Mathlib's interval integral. "For arbitrary $T$" is $\forall T>0,\ \exists y$, with the universal quantifier outside. "A zero point in $[h,\infty)$" is $\exists\lambda\ge h,\ F(\lambda)=0$.

Pinned readings, all disclosed in the items:

• Lemma 5.1 adds $y^1\le y^2$ on $[0,T]$ (the lemma is false without it), $L\ge0$, and integrability of $c^1,c^2$. Its $\alpha$ ranges over measurable functions with $|\alpha|\le L$, and $F^i$ is measurable on $\mathbb R\times\mathbb R$.
• The blow-up milestone assumes $G$ continuous.
• In Theorem 5.4(ii)–(iii), $\varepsilon$ is chosen after $T$, $h$, $f_1$ and $a_1$, the data its proof uses.
• (A.5) is not stated.

Trivializing formalizations are ruled out. The solution predicate carries integrability of the integrand, so Lean's junk value $0$ for a non-integrable integral cannot make an arbitrary $y$ with $y_t=h$ a solution. The goal assumes neither a zero of $F$ nor a blow-up: both are proved in the milestones. Lemma 5.1's uniqueness is over solutions in the band.

The needed infrastructure is scalar ODE theory on Mathlib: existence for Lipschitz Carathéodory equations, differentiation of $t\mapsto\int_t^T g$, comparison of sub- and super-solutions, and elementary real-root facts for cubics. The comparison lemma and the blow-up lemma are reusable beyond this mission. Contributions of either the sufficiency or the necessity chain are welcome independently.

Selected references

• J. Ma, Z. Wu, D. Zhang, J. Zhang, On well-posedness of forward–backward SDEs—a unified approach, Ann. Appl. Probab. 25(4):2168–2214, 2015. https://arxiv.org/abs/1110.4658 , https://doi.org/10.1214/14-AAP1046
• F. Antonelli, Backward–forward stochastic differential equations, Ann. Appl. Probab. 3(3):777–793, 1993. MR1233625, https://mathscinet.ams.org/mathscinet-getitem?mr=1233625
• J. Ma, P. Protter, J. Yong, Solving forward–backward stochastic differential equations explicitly—a four step scheme, Probab. Theory Related Fields 98:339–359, 1994. MR1262970, https://mathscinet.ams.org/mathscinet-getitem?mr=1262970
• Y. Hu, S. Peng, Solution of forward–backward stochastic differential equations, Probab. Theory Related Fields 103:273–283, 1995. MR1355060, https://mathscinet.ams.org/mathscinet-getitem?mr=1355060
• S. Peng, Z. Wu, Fully coupled forward–backward stochastic differential equations and applications to optimal control, SIAM J. Control Optim. 37(3):825–843, 1999. MR1675098, https://mathscinet.ams.org/mathscinet-getitem?mr=1675098
• J. Yong, Finding adapted solutions of forward–backward stochastic differential equations: method of continuation, Probab. Theory Related Fields 107:537–572, 1997. MR1440146, https://mathscinet.ams.org/mathscinet-getitem?mr=1440146

Motivation

Two-stage robust optimization models decisions taken in two steps around an uncertain parameter: a first-stage decision $x$ is fixed before a parameter $\xi$ is revealed from an uncertainty set $\Xi$, and a second-stage (recourse) decision $y$ is taken afterwards. When the recourse is binary (whether to open a facility, route a vehicle, schedule a task), the exact two-stage problem is computationally out of reach, and the classical tool of affine decision rules does not apply. $K$-adaptability, introduced by Bertsimas and Caramanis (2010), replaces the full recourse function by $K$ candidate second-stage policies $y^1,\dots,y^K$ chosen here-and-now, of which the best feasible one is selected once $\xi$ is known.

Hanasusanto, Kuhn and Wiesemann (Oper. Res. 63(4), 2015; preprint) study this approximation for problems in which the uncertainty affects both the objective and the constraints. When the constraints are uncertain, the $K$-adaptability problem has a discontinuous objective, and the authors approximate it by a family of problems $(6_\epsilon)$, $\epsilon>0$, whose uncertainty sets are closed polyhedra. Their Theorem 5 states that each $(6_\epsilon)$ is equivalent to an explicit mixed-integer bilinear program (7), which standard Big-M techniques turn into a mixed-integer linear program solvable by off-the-shelf software. This mission formalizes Theorem 5.

Setting

The data are matrices $C\in\mathbb R^{Q\times N}$, $Q\in\mathbb R^{Q\times M}$, $T\in\mathbb R^{L\times N}$, $W\in\mathbb R^{L\times M}$, $H\in\mathbb R^{L\times Q}$, and a polyhedral uncertainty set $\Xi=\{\xi\in\mathbb R^Q: A\xi\le b\}$, $A\in\mathbb R^{R\times Q}$, $b\in\mathbb R^R$, assumed nonempty and bounded. The first-stage feasible set is $\mathcal X\subseteq\{0,1\}^N$ and the second-stage feasible set is $\mathcal Y\subseteq\{0,1\}^M$. A decision is a tuple $(x,\{y^k\}_{k\in\mathcal K})\in\mathcal X\times\mathcal Y^K$, $\mathcal K=\{1,\dots,K\}$. Under the parameter $\xi$, policy $y^k$ is feasible if $Tx+Wy^k\le H\xi$ and then costs $\xi^\top Cx+\xi^\top Qy^k$.

A vector $\ell\in\mathcal L=\{0,1,\dots,L\}^K$ records, for each policy $k$, either $\ell_k=0$ (policy $k$ is feasible) or the index $\ell_k$ of a violated constraint. Write $\mathcal L_+$ for the $\ell$ with every component nonzero and $\partial\mathcal L=\mathcal L\setminus\mathcal L_+$. For $\epsilon>0$ the approximate uncertainty sets are

and problem $(6_\epsilon)$ minimizes over decisions the objective

where a minimum over no index is $+\infty$. The set $\Delta_K(\ell)=\{\lambda\in\mathbb R^K_+: e^\top\lambda=1,\ \lambda_k=0\ \forall k:\ell_k\ne0\}$ is the face of the probability simplex supported on the feasible policies, and $H_{\ell_k}$ is the $\ell_k$-th row of $H$ as a column vector.

Problem (7) minimizes $\tau$ over $x\in\mathcal X$, $y^k\in\mathcal Y$, $\tau\in\mathbb R$ and, for every $\ell$, auxiliary variables $\lambda(\ell)\in\Delta_K(\ell)$, $\alpha(\ell)\ge0$, $\beta^k(\ell)\ge0$, $\gamma(\ell)\ge0$, subject to

for $\ell\in\partial\mathcal L$, and

for $\ell\in\mathcal L_+$.

Formalization targets

Goal: Theorem 5 (p. 19)

For every $\epsilon>0$ and every decision $(x,\{y^k\})\in\mathcal X\times\mathcal Y^K$,

and the optimal values of $(6_\epsilon)$ and (7) coincide.

Milestones (proof of Theorem 5, pp. ec8–ec10)

1. $\varphi_\epsilon=\max_{\ell}\max_{\xi\in\Xi_\epsilon(\ell)}\big[\xi^\top Cx+\min_{\lambda\in\Delta_K(\ell)}\sum_k\lambda_k\xi^\top Qy^k\big]$, and $\Delta_K(\ell)=\emptyset\iff\ell\in\mathcal L_+$.
2. If $\Xi_\epsilon(\ell)=\emptyset$ for all $\ell\in\mathcal L_+$, the maximization over $\xi$ and the minimization over $\lambda$ can be exchanged, and the weights can be chosen per $\ell$.
3. The epigraph problem (EC.6) has the same value as $(6_\epsilon)$ at every decision.
4. If $\Xi$ is nonempty and bounded then $\{A^\top\alpha:\alpha\ge0\}=\mathbb R^Q$.
5. For $\ell\in\partial\mathcal L$, the semi-infinite constraint of (EC.6) is equivalent, by LP duality, to the first block of (7).
6. For $\ell\in\mathcal L_+$, $\Xi_\epsilon(\ell)=\emptyset$ if and only if the second block of (7) is feasible.

Significance

The result. Theorem 5 is what makes the approximation $(6_\epsilon)$ computable: a robust problem with infinitely many constraints indexed by $\xi$ becomes one finite program whose only nonlinear terms are products of a binary variable and a continuous one. Remark 7 of the paper notes that these products can be linearized with standard Big-M techniques, giving a mixed-integer linear program. Combined with the convergence of $(6_\epsilon)$ to the $K$-adaptability problem as $\epsilon\to0$ (Proposition 2 of the paper), it yields a practical solution scheme for two-stage robust binary programs with constraint uncertainty.

Formalizing it. The result is proved in the paper; no machine-checked proof exists. The proof chains a min-max exchange, an epigraph reformulation, LP strong duality and a Farkas-type certificate, each applied to a polyhedron that depends on the decision. A formalization pins down the conventions the paper leaves implicit (values $\pm\infty$, which sets may be empty, why the dual programs are always feasible) and produces a reusable statement of LP duality in the presence of an infeasible primal.

Difficulty

The equivalence must hold in three regimes at once: decisions for which some $\Xi_\epsilon(\ell)$, $\ell\in\mathcal L_+$, is nonempty (both sides $+\infty$, program (7) infeasible); decisions for which every $\Xi_\epsilon(\ell)$ is empty (both sides $-\infty$); and the finite case. A naive application of LP duality fails exactly when $\Xi_\epsilon(\ell)$ is empty for some $\ell\in\partial\mathcal L$: the primal maximum is then $-\infty$, and one needs the dual to be feasible, which requires the nonemptiness and boundedness of $\Xi$. The min-max exchange needs compactness and convexity of $\Xi_\epsilon(\ell)$, which must be checked for each $\ell$, and the exchange of $\min_\lambda$ with $\max_\ell$ requires the weights $\lambda(\ell)$ to be chosen separately for each $\ell$.

Formalization scope

Vectors are Fin n → ℝ and matrices are Matrix (Fin a) (Fin b) ℝ; inequalities between vectors are componentwise. The problem data, with $\Xi$ nonempty and bounded and $\mathcal X,\mathcal Y$ consisting of 0/1 vectors, form one structure. An index $\ell\in\mathcal L$ is a function Fin K → Fin (L+1); $\mathcal L_+$ is "every component nonzero" (never the order 0 < ℓ on functions, which means only "nonzero somewhere"). The value $\ell_k=i+1$ refers to row i : Fin L. All objective values and optimal values are in EReal: a minimum over an empty index set is $+\infty$, a maximum over an empty set is $-\infty$, and the infimum of an empty set of $\tau$ is $+\infty$. The auxiliary variables of (7) are functions of $\ell$; a single shared $\alpha$ would describe a different, stronger program.

"Equivalent" is formalized as a per-decision identity (the feasible $\tau$ are exactly those $\ge\varphi_\epsilon$) together with equality of the optimal values; a statement giving only one inequality, or only the optimal values, would not rule out a reformulation that loses decisions. A statement in which every $\Xi_\epsilon(\ell)$ is assumed empty, or in which (7) is replaced by its feasibility without the bound $\tau$, would be trivially true and is not the theorem.

A complete development needs: the minimax theorem for bilinear functions on compact convex sets (Mathlib's Sion.minimax), LP strong duality for inequality-form programs including the infeasible-primal case, and a Farkas alternative for systems $A\xi\le b$, $G\xi\le g$. The duality statements are reusable beyond this mission. Proofs of individual milestones are welcome.

Selected references

• G. A. Hanasusanto, D. Kuhn, W. Wiesemann, K-Adaptability in Two-Stage Robust Binary Programming, Operations Research 63(4):877–891, 2015. https://doi.org/10.1287/opre.2015.1392 (preprint: Optimization Online 2014/03/4294, https://optimization-online.org/wp-content/uploads/2014/03/4294.pdf)
• D. Bertsimas, C. Caramanis, Finite Adaptability in Multistage Linear Optimization, IEEE Transactions on Automatic Control 55(12):2751–2766, 2010. https://doi.org/10.1109/TAC.2010.2049764
• M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1):171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171

Motivation

Many planning problems are made in two stages: a first decision is fixed before an uncertain parameter is observed, and a second, corrective decision is made afterwards. When the second-stage decisions are binary (which route, which facility, which crew), the resulting two-stage robust binary programs are notoriously hard: the second-stage decision is a function of the uncertain parameter, and no general finite reformulation is known.

Bertsimas and Caramanis (IEEE Trans. Automatic Control, 2010) proposed the K-adaptability approximation: instead of a full second-stage policy, the decision maker commits here-and-now to $K$ candidate second-stage decisions and implements the best of them once the parameter is known. Besides being computable, this matches practice in vehicle routing, production scheduling and emergency planning, where a small number of contingency plans is preferred to re-optimizing after every observation. The basic question is how many candidates are needed before nothing is lost. Hanasusanto, Kuhn and Wiesemann (Oper. Res. 63(4), 2015) answer it when the uncertainty affects only the objective function; this mission formalizes that answer, Theorem 1 of their paper.

Setting

The data are matrices $C\in\mathbb R^{Q\times N}$, $Q\in\mathbb R^{Q\times M}$, $T\in\mathbb R^{L\times N}$, $W\in\mathbb R^{L\times M}$, a vector $h\in\mathbb R^L$, a set $\mathcal X\subseteq\mathbb R^N_+$ of first-stage decisions $x$, a set $\mathcal Y\subseteq\{0,1\}^M$ of binary second-stage decisions $y$, and an uncertainty set

a nonempty bounded polyhedron. (The paper writes $Q$ both for the number of uncertain parameters and for the cost matrix; in Lean the dimension is nQ and the matrix Q.)

The two-stage robust binary program with objective uncertainty is

For $K\ge1$ and $\mathcal K=\{1,\dots,K\}$, the K-adaptability problem is

The affine dimension $\dim\mathcal Y$ is the dimension of the smallest affine subspace containing $\mathcal Y$, and $\operatorname{rk}Q$ is the rank of the cost matrix $Q$.

Formalization targets

Goal: Theorem 1

For every number of policies $K\ge\min\{\dim\mathcal Y,\operatorname{rk}Q\}+1$,

Steps of the paper's proof (milestones)

1. Conservative approximation (p. 12): $\operatorname{opt}(\mathcal{PO})\le\operatorname{opt}(\mathcal{PO}_K)$ for every $K$.
2. With $K=|\mathcal Y|$ policies (p. ec1): $\operatorname{opt}(\mathcal{PO}_{|\mathcal Y|})=\operatorname{opt}(\mathcal{PO})$.
3. Min-max reformulation (EC.1) (p. ec1): for every decision,

with $\Delta_K$ the unit simplex in $\mathbb R^K$. 4. (EC.1) = (EC.2) (p. ec2): the randomized problem with $|\mathcal Y|$ policies has the same optimal value as the one with $\dim\mathcal Y+1$ policies; and, for the case $\operatorname{rk}Q<\dim\mathcal Y$, as the one with $\operatorname{rk}Q+1$ policies. 5. (EC.2) is the $(D+1)$-adaptability problem (p. ec2): for every $K$, the randomized problem with $K$ policies has the optimal value of $\mathcal{PO}_K$.

Significance

The set $\mathcal Y$ may contain exponentially many binary vectors, so a priori full adaptability could require exponentially many policies. Theorem 1 says that under objective uncertainty at most $\min\{M,\operatorname{rk}Q\}+1$ policies are ever needed, a number linear in the problem size. It justifies solving $\mathcal{PO}_K$ for small $K$ as an exact method rather than a heuristic whenever $\dim\mathcal Y$ or $\operatorname{rk}Q$ is small, and it is the reason the paper's mixed-integer linear reformulation of $\mathcal{PO}_K$ (Theorem 2) solves $\mathcal{PO}$ itself for such $K$. It also contrasts with the constraint-uncertainty case, where the same paper shows that every $K<|\mathcal Y|$ can leave a strict gap.

Theorem 1 is proved in the paper's e-companion. As far as is known, neither the theorem nor any step of its proof has a machine-checked proof; this mission produces one, together with reusable Lean statements of the problems $\mathcal{PO}$, $\mathcal{PO}_K$ and their randomized relaxations in the extended reals.

Difficulty

The obvious argument lists all feasible second-stage decisions as policies, which needs $|\mathcal Y|$ of them. Reducing this number is not a matter of discarding unused policies: for different $\xi$ different policies are optimal, and which subset of $\dim\mathcal Y+1$ policies suffices is not determined by any single $\xi$. The reduction to $\dim\mathcal Y+1$ policies holds only for the optimal value, not decision by decision, and it passes through a relaxation in which the policies are mixed with weights; exchanging the maximum over $\Xi$ with the minimum over the weights requires compactness and convexity of $\Xi$, and in Lean the exchange has to be carried out for extended-real values. The bound must also hold for every $K$ above the threshold, so monotonicity in the number of policies is part of the statement.

Formalization scope

• The data form one structure Problem N M L nQ R; its fields include the standing assumptions: $\mathcal X\subseteq\mathbb R^N_+$, every point of $\mathcal Y$ is a 0/1 vector ($\mathcal Y$ is a Finset), and $\Xi$ is nonempty and bounded. $\mathcal X$ is an arbitrary set (the paper allows mixed binary first-stage decisions).
• All objective functions and optimal values take values in EReal. Maxima and minima are suprema and infima, as in the paper's notation: a first-stage decision without a feasible second-stage decision has objective $+\infty$, and an infeasible problem has optimal value $+\infty$.
• Policies are indexed by Fin K and need not be distinct; every policy must satisfy $Tx+Wy^k\le h$, as in problem $\mathcal{PO}_K$ of Observation 1.
• $\dim\mathcal Y$ is Module.finrank ℝ (vectorSpan ℝ 𝒴) (so $\dim\emptyset=0$ in Lean; both optimal values are then $+\infty$), and $\operatorname{rk}Q$ is Matrix.rank.
• $\mathcal{PO}_K$ is defined with the minimum over the $K$ policies, not through weights $\lambda\in\Delta_K$; defining it through the randomized relaxation would make the min-max step true by definition and is ruled out.
• Proofs will need Sion's minimax theorem (Sion.minimax in Mathlib), Carathéodory's theorem (convexHull_eq_union), compactness of bounded polyhedra and extended-real iSup/iInf manipulation. Lemmas on suprema of linear functions over compact polyhedra and on min-max exchange in EReal are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome.

Selected references

• G. A. Hanasusanto, D. Kuhn, W. Wiesemann, K-Adaptability in Two-Stage Robust Binary Programming, Operations Research 63(4), 877–891, 2015; formalized from the preprint, Optimization Online 2014/03/4294 (revision of 2015-03-30). https://doi.org/10.1287/opre.2015.1392
• D. Bertsimas, C. Caramanis, Finite Adaptability in Multistage Linear Optimization, IEEE Transactions on Automatic Control 55(12), 2751–2766, 2010. https://doi.org/10.1109/TAC.2010.2049764
• M. Sion, On General Minimax Theorems, Pacific Journal of Mathematics 8(1), 171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171

Motivation

Two-stage robust optimization models decisions taken in two steps around an uncertain parameter: a here-and-now decision $x$ is fixed before the parameter $\xi$ is revealed, and a wait-and-see decision $y$ adapts to it, and the decision maker guards against the worst $\xi$ in an uncertainty set $\Xi$. When the second-stage decisions are binary, as in routing, scheduling and network design, the exact two-stage problem is computationally out of reach. Bertsimas and Caramanis (IEEE TAC, 2010) proposed the K-adaptability approximation: choose $K$ second-stage policies $y^1,\dots,y^K$ here and now, and once $\xi$ is revealed implement the best of those that are feasible. Hanasusanto, Kuhn and Wiesemann (Oper. Res., 2015; preprint Optimization Online 2014/03/4294) study this problem in depth. When the uncertain parameter enters the second-stage constraints, the K-adaptability problem is in general neither convex nor continuous, and to obtain a solvable reformulation the authors first approximate it by a family of problems with closed uncertainty sets. This mission formalizes the statement that this approximation is asymptotically exact.

Setting

The data are matrices $C\in\mathbb R^{Q\times N}$, $Q\in\mathbb R^{Q\times M}$, $T\in\mathbb R^{L\times N}$, $W\in\mathbb R^{L\times M}$, $H\in\mathbb R^{L\times Q}$, a nonempty bounded polyhedron $\Xi=\{\xi\in\mathbb R^Q: A\xi\le b\}$, a first-stage set $\mathcal X\subseteq\{0,1\}^N$ (the standing assumption of §3 of the paper) and a second-stage set $\mathcal Y\subseteq\{0,1\}^M$. A decision is $(x,\{y^k\}_{k\in\mathcal K})\in\mathcal X\times\mathcal Y^K$ with $\mathcal K=\{1,\dots,K\}$. Policy $y^k$ is feasible for $\xi$ if $Tx+Wy^k\le H\xi$. The K-adaptability problem $\mathcal P_K$ minimizes over decisions

which is $+\infty$ when some $\xi$ leaves no feasible policy.

Let $\mathcal L=\{0,\dots,L\}^K$. For $\ell\in\mathcal L$, the set $\Xi(\ell)$ collects the $\xi\in\Xi$ for which every policy with $\ell_k=0$ is feasible and every policy with $\ell_k\neq0$ violates constraint $\ell_k$ strictly: $[Tx+Wy^k]_{\ell_k}>[H\xi]_{\ell_k}$. Problem (6) minimizes

The sets $\Xi(\ell)$ are not closed. For $\varepsilon>0$ the closed inner approximations $\Xi_\varepsilon(\ell)$ replace the strict inequality by $[Tx+Wy^k]_{\ell_k}\ge[H\xi]_{\ell_k}+\varepsilon$, and problem $(6_\varepsilon)$ has objective $\varphi_\varepsilon$, defined like $\varphi$ with $\Xi_\varepsilon(\ell)$. The effective domains $\mathrm{dom}(6)$ and $\mathrm{dom}(6_\varepsilon)$ are the decisions at which $\varphi$, respectively $\varphi_\varepsilon$, is not $+\infty$.