Robust Optimization

Motivation

In stochastic optimization and statistical learning one chooses a parameter $\theta$ from a set $\Theta\subseteq\mathbb R^d$ to make the risk $R(\theta)=\mathbb E_P[\ell(\theta;X)]$ small, having seen only a sample $X_1,\dots,X_n$ from $P$. Generalization bounds suggest trading empirical risk against its standard deviation, but the variance-penalized objective is non-convex even for convex losses. Duchi and Namkoong (arXiv:1610.02581v3) replace it by the robustly regularized risk, the worst-case expected loss over a $\chi^2$-divergence ball around the empirical distribution. This objective is convex whenever $\ell$ is, and it agrees with the variance-penalized objective up to a small error.

When the risk has curvature near its minimizers, empirical risk minimization attains rates faster than $1/\sqrt n$ (Bartlett, Bousquet and Mendelson 2005; Shapiro, Dentcheva and Ruszczyński 2009). Section 4.1 of the paper asks whether minimizers of the robust risk, which carry an extra variance-dependent penalty of order $\sqrt{\rho/n}$, keep these fast rates. Its Theorem 5 answers yes, and does so for approximate minimizers, which is what iterative solvers return.

Setting

A loss $\ell:\mathbb R^d\times\mathcal X\to\mathbb R$ is fixed, with $\ell(\cdot;x)$ convex and $L$-Lipschitz on a convex set $\Theta$ for every $x$, and $\ell(\theta;\cdot)$ integrable. The risk is $R(\theta)=\mathbb E_P[\ell(\theta;X)]$.

For a radius $\rho\ge0$, the $\chi^2$ ball around the empirical distribution $\widehat P_n$ is the set of weight vectors

$$\mathcal P_n=\Big\{p\in\mathbb R^n_+:\tfrac12\|np-\mathbf 1\|_2^2\le\rho,\ \langle\mathbf 1,p\rangle=1\Big\},$$

and the robust risk is $R_n(\theta,\mathcal P_n)=\sup_{p\in\mathcal P_n}\sum_i p_i\,\ell(\theta;X_i)$.

For $\epsilon\ge0$ the $\epsilon$-suboptimal sets of the risk and of the robust risk are

$$S_\star^\epsilon=\{\theta\in\Theta:R(\theta)\le\inf_\Theta R+\epsilon\},\qquad\widehat S_\star^\epsilon=\{\theta\in\Theta:R_n(\theta,\mathcal P_n)\le\inf_\Theta R_n(\cdot,\mathcal P_n)+\epsilon\},$$

with $S_\star=S_\star^0$ the solution set and $\pi_{S_\star}$ the Euclidean projection onto it. The risk satisfies a growth condition of order $\gamma>1$ if, for some $\lambda>0$ and $r>0$,

$$R(\theta)-\inf_\Theta R\ \ge\ \lambda\,\mathrm{dist}(\theta,S_\star)^\gamma\quad\text{whenever }\mathrm{dist}(\theta,S_\star)\le r.\tag{26}$$

The complexity of the problem enters through the localized class $\{x\mapsto\ell(\theta;x)-\ell(\pi_{S_\star}(\theta);x):\theta\in A\}$ and its empirical Rademacher complexity $\mathfrak R_n(A)=\mathbb E_\varepsilon\big[\sup_{\theta\in A}\frac1n\sum_i\varepsilon_i(\ell(\theta;X_i)-\ell(\pi_{S_\star}(\theta);X_i))\big]$, with independent uniform signs $\varepsilon_i\in\{\pm1\}$.

Formalization targets

Goal: Theorem 5 (p. 19)

For $t>0$, $\rho\ge0$, and $0<\epsilon\le\frac12\lambda r^\gamma$ satisfying

$$\epsilon\ge\Big(2\frac{8^\gamma L^\gamma}{\lambda}\Big)^{\frac1{\gamma-1}}\Big(\frac\rho n\Big)^{\frac\gamma{2(\gamma-1)}}\quad\text{and}\quad\frac\epsilon2\ge2\,\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+L\Big(\frac{2\epsilon}\lambda\Big)^{\frac1\gamma}\sqrt{\frac{2t}n},\tag{27}$$ $$\mathbb P\big(\widehat S_\star^\epsilon\subset S_\star^{2\epsilon}\big)\ \ge\ 1-e^{-t}.$$

Milestones, in attack order

1. Localization (p. 44). Under (26), $S_\star^{2\epsilon}$ lies in $\{\theta\in\Theta:\mathrm{dist}(\theta,S_\star)\le(2\epsilon/\lambda)^{1/\gamma}\}$.
2. Theorem 1, upper half of (10) (p. 7). $\sup_{p\in\mathcal P_n}\langle p,z\rangle-\bar z\le\sqrt{2\rho s_n^2/n}$ for every $z\in\mathbb R^n$.
3. Claim E.1 (p. 44). If $\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon}$, the localized deviation $\Delta_n$ plus a variance term reaches $\epsilon$ somewhere on $S_\star^{2\epsilon}$.
4. Display (43) (p. 45). $\mathbb P(\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon})\le\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge\epsilon/2)$.
5. Concentration (p. 45). $\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge2\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+u)\le\exp(-\frac{nu^2}{2L^2}(\frac\lambda{2\epsilon})^{2/\gamma})$.

Significance

The theorem says that the variance penalty implicit in the robust objective does not cost the fast rates available under curvature. The $\rho$-dependent condition in (27) is of order $(\rho/n)^{\gamma/(2(\gamma-1))}$, which for quadratic growth ($\gamma=2$) is $\rho/n$, the same order as the localized complexity term in typical parametric problems. Corollary 4.1 of the paper derives explicit rates of order $\frac dn\log\frac nd+\frac tn+\frac\rho n$ from it for a unique minimizer. The result applies to $\epsilon$-approximate minimizers, so it covers the output of the stochastic-gradient methods used to solve the robust problem.

The result is proved in the paper (Appendix E). None of it is formalized: no statement about growth conditions, localized deviations of a robust objective, or fast rates for robust minimizers is on Prove2Me. A formal proof would check the printed constants, settle the boundary case $\epsilon=0$ (see below), and produce a localization lemma and a reduction from approximate robust minimizers to empirical processes that apply to other estimators.

Difficulty

The obvious argument fails at two points. First, a uniform deviation bound over all of $\Theta$ gives only the $1/\sqrt n$ rate: the speed-up comes from localizing to $S_\star^{2\epsilon}$, which requires transferring the growth condition, assumed only within distance $r$ of $S_\star$, to every $2\epsilon$-suboptimal point by convexity. Second, the robust risk is not an empirical average, so standard comparisons between empirical and population minimizers do not apply. Claim E.1 handles this by moving along the segment from a bad approximate minimizer to its projection, which needs the projection to be preserved along that segment (a normal-cone property of $\pi_{S_\star}$) and the risk to be continuous there. The robust–empirical gap is then controlled by the variance expansion of Theorem 1. The concentration step needs a bounded-differences inequality for a supremum over an uncountable class, together with symmetrization; neither is in Mathlib in this form.

Formalization scope

Parameters live in EuclideanSpace ℝ (Fin d), so norms, distances and projections are Euclidean. The sample is the coordinate process of the product measure $P^{\otimes n}$ on Fin n → X, $n\ge1$, and probabilities are measures of sample sets (the outer measure for a set that is not measurable). The $\chi^2$ ball is the weight-vector form (8). The suboptimal sets are written without infima ($R(\theta)\le R(\theta')+\epsilon$ for all $\theta'\in\Theta$). Each supremum "$\sup\ge c$" is written as "for every $\delta>0$ some $\theta$ reaches $c-\delta$", so no statement relies on the default value of a real supremum. The Rademacher complexity is the published UnderstandingML.rademacher, and its expectation over the sample is assumed integrable, so that it is the true expectation and not the default value $0$ of a Bochner integral. Lipschitz continuity is required on $\Theta$, as printed.

Corrections and presuppositions:

• $\epsilon>0$. The paper prints $0\le\epsilon$. At $\epsilon=0$, $\rho=0$, both conditions of (27) hold, yet for $\ell(\theta;x)=\frac12(\theta-x)^2$ on $\Theta=[-1,1]$ with $X$ uniform on $[-\frac12,\frac12]$ the robust minimizer is the sample mean, which is almost surely not in $S_\star=\{0\}$. The proof divides by $\epsilon$ (p. 45). The goal is stated for $\epsilon>0$.
• $S_\star$ nonempty and closed are assumed. The projection $\pi_{S_\star}$ presupposes them, and Appendix E calls $S_\star$ closed.
• Only the upper half of Theorem 1's (10) is stated; it needs no boundedness of the values.

The constant $\big(2\cdot8^\gamma L^\gamma/\lambda\big)^{1/(\gamma-1)}$ is the printed one; the proof uses a smaller one, which the printed condition implies. The hypotheses $\epsilon>0$, $\gamma>1$ and $\lambda>0$ make every power well defined. A formalization that assumed (26) vacuously, took $\epsilon=0$, or let the Rademacher term be a non-integrable Bochner integral would trivialize the goal; the statements rule these out.

Infrastructure: Euclidean projection onto closed convex sets and its normal-cone characterization (partly in Mathlib), convexity of integral functionals, McDiarmid's bounded-differences inequality, and symmetrization for suprema of empirical processes. The concentration tools and the localization lemma can be reused beyond this mission. Contributions toward McDiarmid's inequality and symmetrization are especially welcome.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
• P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
• S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT, 2009. https://arxiv.org/abs/0907.3740

Motivation

A robust Markov decision process (robust MDP) evaluates a policy against the worst transition kernel and reward in an uncertainty set around a nominal model $(P_0, r_0)$. It is the standard model for planning when the dynamics are estimated from data (Iyengar 2005; Nilim and El Ghaoui 2005; Wiesemann, Kuhn and Rustem 2013). Its Bellman update contains an inner optimization over the uncertainty set at every state, which makes robust planning costly when the sets are not $(s,a)$-rectangular.

Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) show that, for $s$-rectangular ball uncertainty sets, this inner optimization can be replaced by an explicit penalty that depends both on the policy and on the value function. The resulting twice regularized (R²) MDPs have Bellman operators with no inner optimization over models. The first mission of this series formalizes the robust–regularized equivalence (Theorem 4.1 of the paper). This mission formalizes Section 5: the R² Bellman operators are monotone and contracting under a bound on the transition radius, and the greedy policy of the R² optimal value is optimal.

Setting

Let $\mathcal S$ and $\mathcal A$ be finite nonempty sets of states and actions, $\gamma\in(0,1)$ a discount factor, $P_0(s'\mid s,a)$ a transition kernel and $r_0(s,a)$ a reward. A policy $\pi\in\Delta_{\mathcal A}^{\mathcal S}$ assigns to each state a probability distribution $\pi_s$ on $\mathcal A$. For $v\in\mathbb R^{\mathcal S}$ write $q_s(a)=r_0(s,a)+\gamma\sum_{s'}P_0(s'\mid s,a)v(s')$ and

$$[T^\pi_{(P_0,r_0)}v](s)=\sum_a\pi_s(a)\,q_s(a).$$

All norms $\|\cdot\|$ below are $\ell_2$-norms, $\|a\|=\big(\sum_z a(z)^2\big)^{1/2}$; $\|\cdot\|_\infty$ is the sup norm.

Fix nonnegative radii $\alpha^r_s,\alpha^P_s$ for each state. The R² regularizer is $\Omega_{v,\mathrm R^2}(\pi_s)=\|\pi_s\|\,(\alpha^r_s+\alpha^P_s\gamma\|v\|)$, and the R² Bellman operators are

$$[T^{\pi,\mathrm R^2}v](s)=[T^\pi_{(P_0,r_0)}v](s)-\Omega_{v,\mathrm R^2}(\pi_s),\qquad [T^{*,\mathrm R^2}v](s)=\max_{\pi\in\Delta^{\mathcal S}_{\mathcal A}}[T^{\pi,\mathrm R^2}v](s).$$

A policy $\pi$ is greedy for $v$ when $T^{\pi,\mathrm R^2}v=T^{*,\mathrm R^2}v$.

Assumption 5.1 (bounded radius). For each $s$ there is $\epsilon_s>0$ with

$$\alpha^P_s\le\min\Big(\frac{1-\gamma-\epsilon_s}{\gamma\sqrt{|\mathcal S|}}\ ;\ \min_{u\in\mathbb R^{\mathcal A}_+,\|u\|=1,\ w\in\mathbb R^{\mathcal S}_+,\|w\|=1}\ \sum_{a,s'}u(a)P_0(s'\mid s,a)w(s')\Big),$$

and $\epsilon_*=\min_s\epsilon_s$. The R² value function $v^{\pi,\mathrm R^2}$ of a policy and the R² optimal value $v^{*,\mathrm R^2}$ are the fixed points of $T^{\pi,\mathrm R^2}$ and $T^{*,\mathrm R^2}$.

Formalization targets

Goal: Theorem 5.1 (p. 8)

Under Assumption 5.1, $T^{*,\mathrm R^2}$ and every $T^{\pi,\mathrm R^2}$ have unique fixed points; a greedy policy $\pi^{*,\mathrm R^2}$ for $v^{*,\mathrm R^2}$ exists, and every such policy satisfies

$$v^{\pi^{*,\mathrm R^2},\mathrm R^2}=v^{*,\mathrm R^2}\ \ge\ v^{\pi,\mathrm R^2}\qquad\text{for all }\pi\in\Delta^{\mathcal S}_{\mathcal A};$$

every optimal policy is greedy; and when $\alpha^r_s>0$ for all $s$ the greedy policy is unique, hence the unique optimal R² policy.

Milestones

1. Proposition 2.1 (p. 3): for $\Omega$ strongly convex on the simplex, $\Omega^*(y)=\max_{a\in\Delta}\langle a,y\rangle-\Omega(a)$ is differentiable with Lipschitz gradient equal to the unique maximizer, satisfies $\Omega^*(y+c\mathbb 1)=\Omega^*(y)+c$, and is non-decreasing.
2. Proposition 5.1 (i) (p. 8): $v_1\le v_2$ implies $T^{\pi,\mathrm R^2}v_1\le T^{\pi,\mathrm R^2}v_2$ and $T^{*,\mathrm R^2}v_1\le T^{*,\mathrm R^2}v_2$.
3. Proposition 5.1 (iii) (p. 8):

$$\|T^{\pi,\mathrm R^2}v_1-T^{\pi,\mathrm R^2}v_2\|_\infty\le(1-\epsilon_*)\|v_1-v_2\|_\infty,\qquad \|T^{*,\mathrm R^2}v_1-T^{*,\mathrm R^2}v_2\|_\infty\le(1-\epsilon_*)\|v_1-v_2\|_\infty.$$

Significance

Theorem 5.1 is the R² counterpart of the fundamental theorem of discounted dynamic programming: optimal R² values are achieved by stationary policies obtained by a single greedy step. Together with the contraction of Proposition 5.1 (iii) it justifies the R² modified policy iteration algorithm of the paper, whose greedy step is a projection onto the simplex rather than a robust max–min problem. Combined with the first mission of the series, which identifies the robust value of an $s$-rectangular ball-constrained MDP with the optimum of an R²-regularized program, it gives a route to robust planning at the cost of regularized planning.

The results are proved in the paper (App. C), partly by reference to Geist, Scherrer and Pietquin (2019) for the optimality operator. No machine-checked proof of any of them exists; this mission produces the first. Prop. 2.1 is a general fact of convex analysis (Danskin-type smoothness of a conjugate on the simplex) that is reusable for any regularized MDP or entropy-regularized game.

Difficulty

The R² evaluation operator is not affine: the value regularizer $-\alpha^P_s\gamma\|\pi_s\|\,\|v\|$ is concave in $v$ and decreases as $\|v\|$ grows. Monotonicity therefore does not follow from the positivity of $P_0$ as in the standard case; it requires the second bound of Assumption 5.1, which compares the $\ell_2$ variation of $\|v\|$ with the minimal nonnegative bilinear form of $P_0(\cdot\mid s,\cdot)$. Likewise the contraction modulus is not $\gamma$ but $1-\epsilon_*$, because the regularizer is $\sqrt{|\mathcal S|}$-Lipschitz between the $\ell_2$ and sup norms. The optimality step of the classical proof uses linearity of $T^\pi$ when comparing values of policies; here only monotonicity and contraction are available. Uniqueness of the greedy policy rests on strict concavity on the simplex, which holds only when the regularization weight is positive.

Formalization scope

States and actions are finite nonempty types; transitions are arrays P₀ : S → A → S → ℝ with the published predicate IsTransitionKernel; value functions are S → ℝ with the pointwise order. The $\ell_2$-norm is an explicit l2norm (Mathlib's norm on S → ℝ is the sup norm, used only for $\|\cdot\|_\infty$). $T^{*,\mathrm R^2}v(s)$ is the real supremum over the simplex $\Delta_{\mathcal A}$ (attained), and the inner minimum of Assumption 5.1 is the real infimum over nonnegative $\ell_2$-unit vectors; the witnesses $\epsilon_s$ are explicit. Greedy policies are a predicate, never a function, and the R² value functions are not defined by choice: the goal asserts their existence and uniqueness and speaks about the fixed points.

Disclosed deviations from the page. Assumption 5.1 is a hypothesis of Theorem 5.1 (its proof assumes it). The uniqueness clause of Theorem 5.1 additionally assumes $\alpha^r_s>0$ for all $s$: with one state, two actions, zero reward and zero radii every policy is greedy and optimal. Proposition 2.1 assumes $\Omega$ continuous on the simplex, without which the maximum need not be attained, and strong convexity is Mathlib's StrongConvexOn for some modulus (norm-independent in finite dimension). Proposition 5.1 (ii) is false as printed and is not drafted: with one state, one action, $P_0=1$, $r_0=0$, $\gamma=1/2$, $\alpha^r=0$, $\alpha^P=1/2$, $\epsilon=1/4$, one has $Tv=v/2-|v|/4$, and $v_1=-1$, $c=1$ give $T(v_1+c)=0>-1/4=Tv_1+\gamma c$. Remark 5.1, Algorithm 1 and the $\ell_p$ variant of App. C.1 are out of scope. The inner minimum of Assumption 5.1 is $0$ whenever some $P_0(s'\mid s,a)=0$, forcing $\alpha^P_s=0$; this is the assumption as printed.

A formalization in which $\|\cdot\|$ is the sup norm, the inner minimum ranges over all unit vectors (making the assumption unsatisfiable), or the value functions are postulated rather than shown to exist would be trivial or wrong; the drafted statements avoid all three. Contributions welcome: Prop. 2.1 as a general convex-analysis lemma, Banach fixed-point plumbing for S → ℝ with the sup norm, and the strict concavity of $p\mapsto\langle p,q\rangle-c\|p\|$ on the simplex.

Selected references

• E. Derman, M. Geist, S. Mannor, Twice regularized MDPs and the equivalence between robustness and regularization, NeurIPS 2021. arXiv:2110.06267v1
• M. Geist, B. Scherrer, O. Pietquin, A theory of regularized Markov decision processes, ICML 2019. arXiv:1901.11275
• A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. doi:10.1287/opre.1050.0216
• G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. doi:10.1287/moor.1040.0129
• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov decision processes, Mathematics of Operations Research 38(1), 2013. doi:10.1287/moor.1120.0566
• A. Mensch, M. Blondel, Differentiable dynamic programming for structured prediction and attention, ICML 2018. arXiv:1802.03676

Motivation

A linear program is solved with data that, in practice, is rarely known exactly: coefficients come from measurements, estimates or forecasts. Robust optimization asks for a solution that remains feasible for every realization of the data in a prescribed uncertainty set, and among those the one with the best guaranteed objective value. Ben-Tal and Nemirovski introduced this framework for linear programming in Robust solutions of uncertain linear programs (Oper. Res. Lett. 25, 1999), following their treatment of robust convex optimization (Math. Oper. Res. 23, 1998) and Soyster's earlier work on inexact linear programming (Oper. Res. 21, 1973). The robust counterpart has since become the starting point of a large literature on uncertainty sets, budgets of uncertainty and adjustable policies.

A natural first objection is that the robust counterpart might be needlessly conservative: by demanding feasibility for all realizations simultaneously, it could be infeasible, or have a worse value, even when every individual realization is perfectly well behaved. This mission formalizes the paper's answer (§2.2): under two structural hypotheses, the robust counterpart is no worse than the worst realization.

Setting

Fix $c, f \in \mathbb R^n$ and write a linear program in the homogeneous form (6)

$$(P)\qquad \min\{c^{T}x \mid Ax \ge 0,\ f^{T}x = 1\},$$

where $A$ is a real $m\times n$ matrix and $Ax\ge0$ is componentwise. Every linear program can be put in this form. The matrix $A$ is uncertain: it is only known to lie in an uncertainty set $\mathcal U$ of $m\times n$ matrices. Each $A\in\mathcal U$ gives an instance $(P)$ with feasible set $\{x\mid Ax\ge0,\ f^{T}x = 1\}$ and optimal value $c^*(P)$; the family of instances is $\mathcal P$. The robust counterpart (7) is

$$(P_{\mathcal U})\qquad \min\{c^{T}x \mid x \in G_{\mathcal U}\},\qquad G_{\mathcal U} = \{x\mid Ax\ge0\ \ \forall A\in\mathcal U;\ f^{T}x = 1\},$$

and its optimal value is $c^*$. Since $G_{\mathcal U}$ does not change when $\mathcal U$ is replaced by its closed convex hull, the paper assumes throughout that $\mathcal U$ is convex and closed.

Let $\mathcal U_i\subseteq\mathbb R^n$ be the set of all realizations of the $i$-th row, the projection of $\mathcal U$ onto the data of the $i$-th constraint. The uncertainty is constraint-wise if $\mathcal U = \mathcal U_1\times\dots\times\mathcal U_m$: the rows vary independently. The Boundedness Assumption asks for a convex compact set $Q\subseteq\mathbb R^n$ that contains the feasible set of every instance.

Formalization targets

Goal: Proposition 2.1 (p. 5)

If the uncertainty is constraint-wise and the Boundedness Assumption holds, then

1. $(P_{\mathcal U})$ is infeasible if and only if some instance is infeasible:

$$G_{\mathcal U} = \emptyset \iff \exists A\in\mathcal U:\ \{x\mid Ax\ge0,\ f^{T}x=1\}=\emptyset;$$

2. if $(P_{\mathcal U})$ is feasible with optimal value $c^*$, then

$$c^* = \sup\{c^*(P)\mid (P)\in\mathcal P\}. \tag{9}$$

Milestones

The milestones follow the paper's proof: the row-wise description (8) of robust feasibility; the inclusion of $G_{\mathcal U}$ in every instance's feasible set; the reduction of the semi-infinite system (8) on $Q$ to a finite subsystem; the statement that the finite system (10) $A_1x\ge0,\dots,A_Nx\ge0,\ f^{T}x=1$ then has no solution at all; the Farkas certificate (11); the construction of one infeasible instance from it; and part (i) alone, which part (ii) uses for an augmented program.

Companions

The §2.2 example (every instance has optimal value 1, the robust counterpart is infeasible), and the two invariance remarks: $G_{\mathcal U}$ is unchanged under passing to the closed convex hull of $\mathcal U$ (§2.1) or to the product $\mathcal U_1\times\dots\times\mathcal U_m$ of its projections (§2.2).

Significance

Proposition 2.1 says that, for constraint-wise uncertainty, robustness costs nothing beyond what the worst realization already costs: the robust counterpart is feasible exactly when every instance is, and its optimal value equals the worst instance value. The §2.2 example shows the hypothesis cannot be dropped: there, correlated uncertainty in two rows makes every instance solvable with value 1 while the robust counterpart is infeasible. Together with the invariance of $G_{\mathcal U}$ under passing to the product of projections, this explains why row-wise (constraint-wise) uncertainty sets are the standard modelling choice in robust linear optimization.

The result is proved in the paper; no machine-checked version is known to exist. Formalizing it produces a reusable development of semi-infinite linear systems: the compactness reduction to finite subsystems, a homogeneous Farkas alternative, and the row-averaging argument that uses convexity and the product structure of $\mathcal U$.

Difficulty

The robust counterpart has a continuum of constraints, one for each $A\in\mathcal U$, so Farkas' Lemma cannot be applied to it directly. The step that requires care is passing from infeasibility of this semi-infinite system to infeasibility of a single instance. Compactness yields only finitely many instances whose joint system has no solution in $Q$; those instances are in general all feasible individually, and the infeasible instance has to be manufactured from their rows. Without constraint-wise uncertainty the manufactured matrix need not lie in $\mathcal U$, which is exactly what the §2.2 example exploits. Part (ii) needs the optimal values of the instances to be attained on compact feasible sets, which is where the Boundedness Assumption enters again.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and $Ax\ge0$ is 0 ≤ A *ᵥ x in the componentwise order. The $i$-th row of $A$ is A i and $a^{T}x$ is a ⬝ᵥ x. The projections $\mathcal U_i$ are the images of $\mathcal U$ under $A\mapsto A_i$, not free sets, and constraint-wise uncertainty is the inclusion $\mathcal U_1\times\dots\times\mathcal U_m\subseteq\mathcal U$ (the reverse inclusion always holds). The Boundedness Assumption keeps both convexity and compactness of $Q$, as on the page.

Optimal values are infima: $c^*$ is the greatest lower bound (IsGLB) of $c^{T}x$ over $G_{\mathcal U}$, and (9) states that $c^*$ is the least upper bound (IsLUB) of the set of real optimal values of the instances. No real sInf/sSup is used, so no junk value can make the statement true.

The goal carries the paper's standing assumption that $\mathcal U$ is convex and closed, and one disclosed addition: $\mathcal U$ is nonempty. The paper takes this for granted; without it part (i) fails for $f = 0$ and the supremum in (9) ranges over the empty set. The goal does not assume that the robust counterpart or any instance attains its optimum, and it does not mention finite subsystems, multipliers or the averaged matrix; those appear only in the milestones. A formalization in which the uncertainty sets $\mathcal U_i$ are arbitrary sets with $\mathcal U = \prod_i\mathcal U_i$, or in which optimal values are taken as sInf without boundedness, would not be faithful and is ruled out.

A complete development needs: compactness arguments for families of closed half-spaces, a Farkas alternative for homogeneous systems with one normalizing equation, and elementary convexity of linear images. These pieces are general and reusable beyond robust optimization. Proofs of the milestones, alternative arguments (for instance via LP duality for part (ii)) and proofs of the companion statements are welcome.

Selected references

• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/s0167-6377(99)00016-4 (cited here by the pages of the authors' manuscript).
• 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
• A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Operations Research 21(5):1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154

Motivation

An optimization model often needs a probability distribution for an uncertain cost or demand, while a practitioner has only a finite sample from that distribution. Replacing the distribution by the empirical one can hide uncertainty in its estimated mean and covariance. Delage and Ye use a finite-sample confidence region for these two moments to justify a distributional ambiguity set in data-driven stochastic programming Delage and Ye, 2010. The present mission concerns the confidence region itself: it asks how far the population moments can be from the sample estimates when the normalized random vector has bounded support.

The source for every theorem index and page number here is the authors' draft dated 20 February 2008, not an independently checked pagination of the published article. Its §4 starts from independent observations and Assumption 4, then obtains a sample-mean bound, a covariance bound around the known mean, and finally the joint bound for estimates computed entirely from the sample.

Setting

Let $\xi\in\mathbb R^m$ have distribution $P$, mean $\mu=\mathbb E_P[\xi]$, and covariance $\Sigma=\mathbb E_P[(\xi-\mu)(\xi-\mu)^\mathsf T]$. Assume $\Sigma$ is positive definite. For $M\ge1$ independent observations $\xi_1,\ldots,\xi_M$, the empirical mean and empirical covariance in this section are

$$\widehat\mu=\frac1M\sum_{i=1}^M\xi_i,\qquad \widehat\Sigma=\frac1M\sum_{i=1}^M(\xi_i-\widehat\mu)(\xi_i-\widehat\mu)^\mathsf T.$$

The divisor is $M$, including for the covariance; the paper's earlier discussion of an unbiased estimator with divisor $M-1$ does not govern §4. When the true mean is known, write $\widehat\Sigma(\mu)=M^{-1}\sum_i(\xi_i-\mu)(\xi_i-\mu)^\mathsf T$. Matrix order $A\preceq B$ means $B-A$ is positive semidefinite. The squared Mahalanobis distance of a vector $v$ is $v^\mathsf T\Sigma^{-1}v$.

Assumption 4 bounds the normalized observations: for some $R\ge0$, $(\xi-\mu)^\mathsf T\Sigma^{-1}(\xi-\mu)\le R^2$ with probability one. Equivalently, $\zeta=\Sigma^{-1/2}(\xi-\mu)$ lies almost surely in a Euclidean ball of radius $R$; it has mean zero and covariance $I$. The sample law is $P^M$, the product measure of $M$ identical copies. These choices make the probability in each target an assertion about genuinely independent observations.

Formalization targets

Simultaneous confidence region

For $0<\delta<1$, set

$$\alpha(t)=\frac{R^2}{\sqrt M}\left(\sqrt{1-\frac m{R^4}}+\sqrt{\log(1/t)}\right),\qquad \beta(t)=\frac{R^2}{M}\left(2+\sqrt{2\log(1/t)}\right)^2.$$

Theorem 2 is the goal. Write $a=\alpha(\delta/4)$ and $b=\beta(\delta/2)$, and assume $a+b<1$. The target is the simultaneous event

$$(\widehat\mu-\mu)^\mathsf T\Sigma^{-1}(\widehat\mu-\mu)\le b, \qquad \Sigma\preceq\frac{\widehat\Sigma}{1-a-b}, \qquad \frac{\widehat\Sigma}{1+a}\preceq\Sigma$$

with probability at least $1-\delta$. The last denominator is a correction: printed (12c) says $1-a$, while the authors' union-bound display on draft p. 13 says $1+a$. The printed version fails, for example, for symmetric $\pm1$ observations, whose sample covariance is $1-\widehat\mu^2$ and for which its claimed lower bound would require an implausibly large sample-mean square. The proof's displayed bound gives the stated $1+a$ draft pp. 13–14.

Supporting results

Lemma 2 bounds the normalized sample mean. Corollary 1 turns it into the Mahalanobis bound for $\widehat\mu-\mu$. Lemma 3 gives a two-sided matrix bound for $M^{-1}\sum_i\zeta_i\zeta_i^\mathsf T$; Corollary 2 transfers that bound to $\widehat\Sigma(\mu)$. A separate theorem item states the centring identity $\widehat\Sigma(\mu)=\widehat\Sigma+(\widehat\mu-\mu)(\widehat\mu-\mu)^\mathsf T$. The final milestone is the rank-one matrix inequality used in Theorem 2's proof. Their statements follow the draft's §4.1–4.2.

Significance

The joint region places both true moments inside explicit data-dependent matrix inequalities at a chosen confidence level. That is the statistical input for the paper's later moment-based distributional uncertainty sets. The result is known in the source; this mission asks for machine-checked proofs of its corrected statement and its supporting concentration and matrix results. The Lean items are currently open theorem statements, so a successful draft compilation does not constitute formal verification of the inequalities.

Related platform results include a proved two-sided constant-bound McDiarmid inequality (UnderstandingML.mcdiarmid_inequality_pi) and an open per-coordinate upper-tail version (StabGen.Uniform.mcdiarmid_inequality). Neither is identical to the cited Theorem 1 of this draft, so the milestone list starts with the paper's Lemma 2 and does not restate Theorem 1.

Difficulty

The known-mean covariance estimate is a sum of outer products of normalized observations. Controlling its largest and smallest eigenvalues together requires concentration of a matrix-valued statistic, rather than a separate scalar bound for each entry. Once the true mean is replaced by $\widehat\mu$, the covariance changes by a rank-one matrix; the mean bound must control that correction in Loewner order. A direct replacement of $\widehat\Sigma(\mu)$ by $\widehat\Sigma$ therefore does not preserve both sides of Corollary 2 automatically.

Formalization scope

Vectors are Fin m → ℝ, and matrices are real Fin m × Fin m matrices. The Euclidean squared length is a dot product; Lean's generic norm on functions is a supremum norm and is not used for it. The Loewner order is (B - A).PosSemidef. The distribution has a probability measure and coordinatewise finite $L^2$ moments, so its real-valued mean and covariance integrals are well defined. The true covariance is positive definite, reflecting the section's nonsingularity assumption. Samples have the product law $P^M$. The chapter's normalized case records zero mean, identity covariance, and the almost-sure ball bound.

Every statistical result assumes $0<\delta<1$; the logarithms and confidence levels are then in their intended domain. Positive $M$ rules out division by zero in empirical averages. Lemma 3 carries the paper's explicit sample-size threshold, and the goal reads “$M$ large enough” as $a+b<1$, which keeps the upper covariance denominator positive. The expression under the other square root is nonnegative in every satisfiable positive-dimensional normalized setting, because $\mathbb E\|\zeta\|_2^2=m\le R^2$. It is not an added assumption. The probability conclusions use $\ge1-\delta$, which is what the paper's proofs show despite the phrase “greater than.”

The goal assumes the source's distributional and support conditions, not the probability conclusions of its supporting corollaries. This prevents a vacuous route that merely postulates the desired confidence event. A complete proof will need reusable product-measure concentration facts, moment and matrix algebra, and a positive-definite quadratic-form bridge. Contributions to those components and to each milestone are in scope. Corollary 3's data-derived radius is excluded because the draft's conditioning argument does not establish its claimed confidence level. Corollary 4 as a probability statement, Theorem 3, and Corollary 5 depend on it; Remark 2 concerns a separate Gaussian eigenvalue density.

Selected references

• Erick Delage and Yinyu Ye, Distributionally Robust Optimization under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3), 595–612, 2010; source used here: authors' draft of 20 February 2008. DOI.

Motivation

Robust optimization protects a decision against every realization of uncertain data in a prescribed uncertainty set. The standard approach replaces the uncertain constraints by a deterministic robust counterpart and solves that counterpart directly (Ben-Tal, El Ghaoui, Nemirovski, Robust Optimization, 2009). The counterpart is often a harder problem than the original: a robust linear program with ellipsoidal uncertainty becomes a second-order cone program, and a robust quadratic program can become a semidefinite program. A practitioner who has an efficient, specialised solver for the nominal problem may therefore have no efficient solver for its robust version.

Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) ask whether the robust problem can be solved by repeatedly calling a solver of the nominal problem, with the number of calls independent of the dimension. Their first answer, the dual-subgradient meta-algorithm of §3.1, does so whenever the constraints are concave in the noise and the uncertainty set is convex. It is a primal–dual scheme: an online-learning algorithm picks the noise, and the nominal solver answers. This mission formalizes that result, Theorem 3.

Setting

Let $\mathcal D\subseteq\mathbb R^n$ be a convex domain, $\mathcal U\subseteq\mathbb R^d$ a convex uncertainty set, and $f_1,\dots,f_m:\mathbb R^n\times\mathbb R^d\to\mathbb R$ constraint functions. The robust feasibility problem (3) is

$$\exists\,x\in\mathcal D:\qquad f_i(x,u_i)\le 0\quad\forall u_i\in\mathcal U,\ i=1,\dots,m .$$

(An objective is handled by binary search on its value, so feasibility is the core question.) A point $x\in\mathcal D$ is an $\epsilon$-approximate solution if $f_i(x,u)\le\epsilon$ for all $u\in\mathcal U$ and all $i$.

An $\epsilon$-approximate oracle $\mathcal O_\epsilon$ (Figure 1) takes a noise vector $u=(u_1,\dots,u_m)\in\mathcal U^m$ and either returns some $x\in\mathcal D$ with $f_i(x,u_i)\le\epsilon$ for all $i$, or answers "infeasible", which it may do only if no $x\in\mathcal D$ has $f_i(x,u_i)\le 0$ for all $i$.

The standing assumptions of §3.1 are: each $f_i(\cdot,u)$ is convex on $\mathcal D$; each $f_i(x,\cdot)$ is concave on $\mathcal U$ for $x\in\mathcal D$; $D\ge\|u-v\|_2$ for all $u,v\in\mathcal U$; and $\|\nabla_u f_i(x,u)\|_2\le G$ for $x\in\mathcal D$, $u\in\mathcal U$. Write $P$ for the Euclidean projection onto $\mathcal U$.

Algorithm 1 sets $T=\lceil G^2D^2/\epsilon^2\rceil$ and $\eta=D/(G\sqrt T)$, starts from $u^0_1,\dots,u^0_m\in\mathcal U$, and for $t=1,\dots,T$ updates

$$u^t_i=P\bigl(u^{t-1}_i+\eta\,\nabla_u f_i(x^{t-1},u^{t-1}_i)\bigr),\qquad x^t=\mathcal O_\epsilon(u^t_1,\dots,u^t_m),$$

stopping with "infeasible" as soon as the oracle says so, and otherwise returning $\bar x=\frac1T\sum_{t=1}^T x^t$. In Lean these are alg1T, alg1Eta, alg1U, alg1X, alg1Output and alg1Calls in the namespace OracleRO.DualSubgrad.

Formalization targets

Goal: Theorem 3 (p. 7)

For every $\epsilon$-approximate oracle,

$$\text{output}=\text{"infeasible"}\ \Longrightarrow\ \neg\,\exists x\in\mathcal D\ \forall i\ \forall u\in\mathcal U:\ f_i(x,u)\le 0,$$ $$\text{output}=\bar x\ \Longrightarrow\ \bar x\in\mathcal D\ \text{ and }\ f_i(\bar x,u)\le 2\epsilon\ \ \forall i,\ \forall u\in\mathcal U,$$

and the number of oracle calls is at most $\lceil G^2D^2/\epsilon^2\rceil$.

Milestones

1. Lemma 1 (p. 5, Zinkevich 2003): projected online gradient ascent with step $\eta=D/(G\sqrt T)$ on concave rewards has regret $\sum_t f_t(x^*)-\sum_t f_t(x_t)\le GD\sqrt T$ for every $x^*$ in the decision set.
2. (6) (p. 7): if a point is returned, $\frac1T\sum_{t=1}^T f_i(x^t,u^t_i)\le\epsilon$ for every $i$.
3. (7) (p. 8): for every $i$ and $u\in\mathcal U$, $\frac1T\sum_t f_i(x^t,u)-\frac1T\sum_t f_i(x^t,u^t_i)\le GD/\sqrt T\le\epsilon$.
4. Final inequality of the proof (p. 8): $f_i(\bar x,u)\le\frac1T\sum_t f_i(x^t,u)$ for $u\in\mathcal U$.

Significance

The result. Theorem 3 turns any approximate solver of the nominal problem into an approximate solver of its robust counterpart, at a cost of $\lceil G^2D^2/\epsilon^2\rceil$ solver calls, a number that depends on the geometry of $\mathcal U$ and the sensitivity of the constraints to the noise but not on $n$, $d$ or $m$. It is the prototype of the paper's oracle-based reductions: the same primal–dual template, with a different online learner, gives the dual-perturbation algorithm of §3.2–3.3 for non-convex uncertainty sets, and the applications of §4 (robust linear programs, quadratic programs, semidefinite programs) instantiate it.

Formalizing it. The theorem is proved in the paper; none of it is machine-checked. A formal development adds a checked statement of the reduction with an explicit call count in place of the paper's $O(\cdot)$, and a reusable regret bound for projected online gradient ascent on concave rewards (Lemma 1), which the paper quotes from Zinkevich without proof and which many other online-learning results rest on.

Difficulty

The obvious argument for the dual side fails at one point: in round $t$ the primal point $x^t$ is computed from $u^t$, so the reward $f_i(x^t,\cdot)$ that the dual player faces depends on its own current move. A regret bound that assumed rewards fixed in advance, or drawn independently of the learner's play, would not apply. Lemma 1 must be used in its adversarial form, valid for every sequence of reward functions, including adaptively chosen ones. A second point is that the projection step requires the variational characterization of a nearest point in a convex set, which a mere "map into $\mathcal U$" does not provide.

Formalization scope

Points are elements of EuclideanSpace ℝ (Fin k), so every norm is the $\ell_2$ norm. The projection is a predicate IsProjOnto U P (each $P(y)$ is a nearest point of $\mathcal U$ to $y$), not a construction; the oracle is a function (Fin m → E d) → Option (E n) with none for "infeasible", constrained by the predicate IsApproxOracle on inputs in $\mathcal U^m$. The goal is quantified over every oracle meeting that specification. The gradient $\nabla_u f_i(x,u)$ is a given map gradU with HasGradientAt at points of $\mathcal U$; no differentiability in $x$ is assumed. Rounds are indexed by natural numbers with index $0$ for the initialization; the starting primal point $x^0\in\mathcal D$, used by the first update and left undefined by the algorithm, is an input. Hypotheses $D>0$ and $G>0$ are added so that $\eta$ and $T\ge1$ are meaningful. Maxima over $\mathcal U$ are stated as "for every $u\in\mathcal U$".

Explicit instantiations and corrections:

• The paper's "$O(G^2D^2/\epsilon^2)$ calls" is stated as at most $\lceil G^2D^2/\epsilon^2\rceil$ calls (one call per round, $T$ rounds).
• Lemma 1's "$G\ge\max_t\|f_t(x_t)\|$" is read as the gradient bound $\|\nabla f_t(x_t)\|\le G$, as the same sentence describes it.
• The proof's "Combining (10) and (12)" refers to (6) and (7).

Trivializing formalizations are ruled out: an oracle specification under which "infeasible" is never returned, or an output that is not the average of the oracle's answers, would not be Theorem 3. The "infeasible" conclusion is about the robust problem, not the nominal one.

A complete development needs the variational inequality for nearest points in a convex set, the gradient (supergradient) inequality for a concave function differentiable at a point of a convex set, Zinkevich's telescoping argument, and Jensen's inequality for finite averages. The first two and Lemma 1 are reusable beyond this mission. Proofs of the milestones, in any order, are welcome.

Selected references

• A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-Based Robust Optimization via Online Learning, arXiv:1402.6361v1, 2014; Operations Research 63(3), 2015. https://arxiv.org/abs/1402.6361v1
• M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization, 2016. https://arxiv.org/abs/1909.05207

Motivation

In robust optimization, a decision must satisfy a constraint for every parameter value in a prescribed uncertainty set. A nonlinear uncertain constraint can be difficult to use directly because it contains a universal condition over a continuum of parameters. Ben-Tal, den Hertog, and Vial study constraints whose value is concave in the uncertain parameter. Their Theorem 2 replaces the universal condition by one inequality involving a new vector and two conjugate functions. The replacement is the general framework used for the paper's later examples, including uncertainty regions assembled from simpler sets and nonlinear functions whose conjugates have explicit forms. The discussion paper, §§2–4 is the source for this mission; theorem and page numbers refer to that 2012 version.

The paper's result extends a more specialized counterpart for a linear uncertain constraint under a φ-divergence uncertainty region. That 2013 result has a proved formalization on Prove2Me, but its divergence-specific conjugate and uncertainty set are different objects. The same earlier formalization also supplies a proved version of the self-concordant-barrier statement that this paper quotes as Lemma 33, with a differently printed constant. Neither earlier theorem supplies the general concave-constraint result here.

Setting

Fix dimensions $m,n,L$. The nominal vector is $a^0\in\mathbb R^m$, and $A\in\mathbb R^{m\times L}$ maps a primitive uncertainty $\zeta\in Z\subseteq\mathbb R^L$ to an uncertain parameter $a=a^0+A\zeta$. Thus the uncertainty set is $U=\{a^0+A\zeta:\zeta\in Z\}$. The paper assumes that $Z$ is nonempty, convex, and compact, with $0$ in its relative interior $\operatorname{ri}Z$. Relative interior is taken inside the affine hull of a set, so $Z$ may lie in a lower-dimensional plane.

A decision is $x\in\mathbb R^n$. For each decision, $D(x)$ is the effective domain of the uncertain constraint $f(\cdot,x)$: $f(a,x)$ is real on $D(x)$ and is interpreted as $-\infty$ outside it. The function is concave in $a$ on $D(x)$ for every $x$; the paper imposes no convexity assumption in the decision $x$. The robust constraint (RC) is $f(a,x)\le0$ for every $a\in U$. In the domain representation used here, this means every $a\in U\cap D(x)$. The nominal vector is regular when $a^0\in\operatorname{ri}D(x)$ for every decision $x$, as in Definition 1.

The support function of $S$ is $\delta^*(y\mid S)=\sup_{a\in S}y^Ta$. The partial concave conjugate is $f_*(v,x)=\inf_{a\in D(x)}(a^Tv-f(a,x))$. Both have extended-real values: an empty support set has support value $-\infty$, and the conjugate can be $-\infty$ when its infimum is unbounded below. These values matter in the equivalence; replacing them by a default real number changes the constraint.

Formalization targets

The goal is the paper's Theorem 2. Under the standing assumptions and regularity, for every decision $x$,

$$\left[\forall a\in U\cap D(x),\ f(a,x)\le0\right] \quad\Longleftrightarrow\quad \left[\exists v\in\mathbb R^m:\ (a^0)^Tv+\delta^*(A^Tv\mid Z)-f_*(v,x)\le0\right].$$

The right-hand inequality is the Fenchel robust counterpart (FRC). Its existence claim is essential: equality of primal and dual infima alone would not show that an auxiliary vector satisfying FRC exists.

Four source statements form the milestone path. Remark 5 gives the weak-duality inequality and the FRC-to-RC implication without concavity. Equations (16)–(18) calculate the support function of $U$. Equation (7) states the relative-interior qualification. Equations (13)–(15) state the worst-case/dual-value identity and, through the printed minimum, attainment of the dual infimum. The milestone list quotes those source passages and identifies their printed pages. Theorem 2 and its proof appear on pp. 4–5.

Significance

The equivalence gives an exact way to replace an infinite family of uncertain inequalities by an existential constraint. In examples where the support function and concave conjugate can be evaluated or represented with standard optimization constraints, it yields a finite robust counterpart. The conclusion remains a mathematical equivalence even when such an explicit representation has not been found. It is also independent of any convexity of $f$ in the decision variable, a point the paper makes after Corollary 3.

This mission supplies reusable, domain-aware support and conjugate definitions and formal statements for the duality path in the paper's central result. The new goal and milestones are open proof obligations: their Lean declarations compile, but they do not yet have machine-checked proofs. The proved 2013 φ-divergence case is narrower and does not close them. A completed development would make the general relative-interior and attained-duality steps reusable for other robust optimization models.

Difficulty

The delicate point is the direction from RC to the existence of an FRC vector. Weak duality gives only a one-sided bound. Identifying the two optimal values still leaves an existence question when an infimum is not attained. The paper invokes Fenchel duality under a relative-interior intersection condition; replacing relative interior by ordinary interior would exclude lower-dimensional uncertainty sets and effective domains that the source permits. A second difficulty is keeping finite and infinite conjugate values distinct while subtracting them in the counterpart inequality. An unbounded-below conjugate must make a finite-support FRC value $+\infty$, not a plausible finite number.

Formalization scope

Vectors are functions on Fin m, Fin n, and Fin L; $A$ is a real matrix, and dot products use the finite-vector dot product. Mathlib's intrinsicInterior ℝ represents relative interior. The domain map $D(x)$ is explicit, with the concavity hypothesis imposed on that domain. The real representative of $f$ outside $D(x)$ is ignored everywhere. The paper's Notation paragraph calls its generic concave functions closed, but the statements here omit closedness: the finite-dimensional duality qualification used for Theorem 2 needs relative-interior overlap, not that extra regularity. This is a stated strengthening of the source theorem, not a change of its feasible points.

Support functions, conjugates, worst-case values, and dual values use EReal. The paper's “max” in (8), (13), and Remark 5 is read as an extended-real supremum; its “min” in (15) is an infimum accompanied by an attaining vector. The support identity includes $Z=\varnothing$, where both sides are $-\infty$, although Theorem 2 keeps the paper's nonempty, convex, compact $Z$. On the theorem's hypotheses the support value is finite and $D(x)$ is nonempty, so the undefined-looking combinations $+\infty-(+\infty)$ and $-\infty+(+\infty)$ cannot occur in FRC. No all-space real-valued substitute for $f_*$ is used, and the theorem still quantifies over every decision and every allowed uncertainty vector.

The proof development needs finite-dimensional relative-interior behavior under affine maps and Fenchel duality with attainment. General convex conjugates and support functions can serve later missions. Corollary 3 and the paper's complexity discussion are outside this mission. Theorem A.1 is not separately made a milestone here: as printed, its domain-restricted dual maximum has a problematic $-\infty$ case; the directly used, attained identity (13)–(15) is the target under the main theorem's standing assumptions.

Selected references

• A. Ben-Tal, D. den Hertog, J.-P. Vial, Deriving robust counterparts of nonlinear uncertain inequalities, CentER Discussion Paper 2012-053, Tilburg University, 2012. Discussion-paper PDF; journal version, Mathematical Programming, 2015, DOI 10.1007/s10107-014-0750-8.
• A. Ben-Tal et al., Robust solutions of optimization problems affected by uncertain probabilities, Management Science, 2013. Prove2Me formalization of its φ-divergence case.