Robust Optimization

Motivation

A Markov decision process (MDP) is solved by dynamic programming once its transition probabilities are known. In practice they are estimated from data, and the optimal policy of an MDP can be sensitive to estimation error: a policy computed from point estimates may perform much worse under the true transition matrices. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) study the robust version of the problem, in which the controller minimises the worst-case expected cost when the transition matrices are only known to lie in given uncertainty sets, and motivate it with aircraft routing under uncertain weather.

Earlier work on MDPs with uncertain transition probabilities includes Satia and Lave (1973) and White and Eldeib (1994), which treat interval and set-valued transition models, and Givan, Leach and Dean (1997) on bounded-parameter MDPs. The robust Bellman recursion under a rectangularity assumption was obtained independently by Iyengar (Columbia technical report 2002, published as Robust dynamic programming, Math. Oper. Res. 30(2), 2005). This mission targets the finite-horizon result of Nilim and El Ghaoui: Theorem 1, which shows that the robust problem is solved by a recursion of the same shape as the nominal one and that the associated min–max game has a value.

Setting

The states form a finite set $\mathcal X=\{1,\dots,n\}$, the decision horizon is $T=\{0,1,\dots,N-1\}$, and the action set $\mathcal A$ is finite, nonempty and the same in every state. Costs are $c_t(i,a)\ge0$ for $t\in T$, and there is a terminal cost $c_N(i)$. The system starts in a given state $i_0$.

Write $\Delta_n=\{p\in\mathbb R^n_+ : p^{\mathsf T}\mathbf 1=1\}$ for the probability simplex. For every action $a$ and state $i$, a nonempty set $\mathcal P_i^a\subseteq\Delta_n$ describes the possible $i$-th rows of the transition matrix under $a$. No convexity or closedness is assumed. The rectangular uncertainty property says the uncertainty set of the matrix $P^a$ is the product $\mathcal P^a=\mathcal P_1^a\times\cdots\times\mathcal P_n^a$.

A controller policy $\pi=(\mathbf a_0,\dots,\mathbf a_{N-1})$ consists of maps $\mathbf a_t:\mathcal X\to\mathcal A$, and $\Pi=\mathcal A^{nN}$ is the set of such policies. A policy of nature $\tau=(P_t^a)_{a\in\mathcal A,t\in T}$ picks, for every stage, action and state, a row $p_i^a(t)\in\mathcal P_i^a$. The admissible set is $\mathcal T=(\bigotimes_a\mathcal P^a)^N$, so nature may change the matrices from stage to stage. The expected total cost is

$$C_N(\pi,\tau)=\mathbf E\Big(\sum_{t=0}^{N-1}c_t(i_t,\mathbf a_t(i_t))+c_N(i_N)\Big),$$

where the state $i_t$ evolves as a Markov chain with transition matrix $P_t^{\mathbf a_t(i)}$ from state $i$. The support function of a set $\mathcal P$ is $\sigma_{\mathcal P}(v)=\sup\{p^{\mathsf T}v : p\in\mathcal P\}$. The robust recursion (7) starts from $v_N=c_N$ and sets

$$v_t(i)=\min_{a\in\mathcal A}\big(c_t(i,a)+\sigma_{\mathcal P_i^a}(v_{t+1})\big),$$

and for a fixed $\pi$ the evaluation recursion (10) starts from $v_N^\pi=c_N$ and sets $v_t^\pi(i)=c_t(i,\mathbf a_t(i))+\sigma_{\mathcal P_i^{\mathbf a_t(i)}}(v_{t+1}^\pi)$.

Formalization targets

Goal: Theorem 1 (Robust Dynamic Programming)

$$\min_{\pi\in\Pi}\sup_{\tau\in\mathcal T}C_N(\pi,\tau)=v_0(i_0)=\sup_{\tau\in\mathcal T}\min_{\pi\in\Pi}C_N(\pi,\tau),$$

together with three further statements. First, $\sup_{\tau}C_N(\pi,\tau)=v_0^\pi(i_0)$ for every $\pi$. Second, every policy that chooses actions attaining the minimum in (7) (rule (8)) achieves $v_0(i_0)$ in the worst case. Third, every nature policy whose rows attain the suprema $\sigma_{\mathcal P_i^a}(v_{t+1})$ (rule (9)) forces the value $v_0(i_0)$ on every controller.

Milestones

1. Lemma 1: a problem $\max q^{\mathsf T}v_0$ subject to $v_t\le g_t(v_{t+1})$ with monotone $g_t$ and $q\ge0$ is solved by the recursion $v_t=g_t(v_{t+1})$.
2. Support functions of nonempty subsets of $\Delta_n$ are componentwise nondecreasing.
3. The constraint maps of problems (15) and (16) are componentwise nondecreasing.
4. Eq. (14): for fixed $\pi$ and fixed matrices, $C_N(\pi,\tau)$ is the value of a linear program.
5. Eq. (16): $\sup_{\tau\in\mathcal T}C_N(\pi,\tau)=v_0^\pi(i_0)$.
6. Eq. (15): $\sup_{\tau\in\mathcal T}\min_{\pi}C_N(\pi,\tau)=v_0(i_0)$.

Significance

Theorem 1 shows that, under rectangular uncertainty, robustness costs one inner optimisation per state and action: the expected continuation cost $p^{\mathsf T}v_{t+1}$ of nominal dynamic programming is replaced by the support function $\sigma_{\mathcal P_i^a}(v_{t+1})$. The equality of the min–max and max–min values says that it does not matter whether nature commits before or after the controller. The optimal controller policy remains deterministic and Markov. The later sections of the paper build on this recursion. They cover the discounted infinite-horizon case, the gap between stationary and time-varying uncertainty, and the computation of $\sigma$ for likelihood and entropy models, which the other missions of this series formalize.

The result is proved in the paper, and independently by Iyengar. It has no machine-checked proof that this mission is aware of. A formal proof yields a reusable development: a finite-horizon MDP with a forward-defined expected cost, the link between that expectation and backward linear programs, and the finite-horizon robust Bellman equation for arbitrary nonempty uncertainty sets.

Difficulty

The nominal Bellman recursion is standard. The robust statement is harder than "apply the nominal recursion under the worst matrix", because no single worst matrix need exist. The sets $\mathcal P_i^a$ are neither closed nor convex, so the suprema in $\sigma$ need not be attained, and $\mathcal T$ is not compact. Minimax theorems for convex–concave or compact games therefore do not apply. The expected cost is defined forward, as an expectation over a Markov chain, while the recursions run backward, and connecting the two is part of the work. The max–min side needs nature policies that come within any tolerance of the value simultaneously at every stage, state and action.

Formalization scope

• States are Fin n and stages Fin N. Values $v_0,\dots,v_N$ are indexed by natural numbers, and only $t\le N$ is meaningful. Vectors are Fin n → ℝ with the componentwise order.
• The model is a structure holding the costs ($c_t\ge0$), the terminal cost (no sign assumed), and the row sets. Every row set must be nonempty and contained in stdSimplex ℝ (Fin n). Nonemptiness is implicit in the paper: without it $\mathcal T$ is empty, and a real supremum over an empty index is $0$.
• Rectangularity is built in: a nature policy is a function $\tau(t,a,i)$ with $\tau(t,a,i)\in\mathcal P_i^a$. Nature does not observe the realised trajectory, and stationary nature ($\mathcal T_s$) is not the set used here.
• $C_N$ is defined by the forward state distribution, not by a backward recursion. Defining it backward would make the evaluation statements hold by definition, which is the trivializing formalization this choice rules out.
• $\sigma_{\mathcal P}$ is the real sSup of $\{p^{\mathsf T}v\}$. This is the true supremum because the set is nonempty and bounded above by $\max_j v_j$.
• Maxima over nature are suprema: ⨆ τ in the goal and IsLUB in the milestones, because the row sets need not be closed. Minima over the finite nonempty $\Pi$ and over $\mathcal A$ are ⨅. The argmax rule (9) is stated only for nature policies attaining the row suprema. The argmin rule (8) is stated for every attaining policy.
• The terminal value $v_N=c_N$ is not printed in Theorem 1. It is taken from the proof and from Step 1 of the paper's algorithm (p. 785). The composition $g_1\circ\cdots\circ g_N$ in Lemma 1 is read as $g_0\circ\cdots\circ g_{N-1}$.
• Not included: Corollary 1 (the sequential game) and the accuracy part of Theorem 2. Contributions of either as additional theorems on these definitions are welcome.

Selected references

• A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• J. K. Satia, R. E. Lave, Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• C. C. White, H. K. Eldeib, Markov Decision Processes with Imprecise Transition Probabilities, Operations Research 42(4):739–749, 1994. https://doi.org/10.1287/opre.42.4.739
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

A Markov decision process (MDP) is controlled with transition probabilities estimated from data, and optimal policies computed for the estimated model can perform badly when the estimates are off. Robust MDPs replace the single transition model by a set of models and optimize the worst case over that set. Two readings of "the set" are possible. In the stationary uncertainty model, the unknown transition matrices are fixed but unknown; this is the reading that confidence regions from statistics support, but the resulting min–max problem is hard to solve. In the time-varying uncertainty model, an adversary ("nature") may pick different matrices at every stage; this relaxation is solved exactly by robust dynamic programming. Nilim and El Ghaoui (Oper. Res. 2005) solve the second problem in place of the first, and Theorem 4 of their paper justifies the substitution for discounted costs: in the infinite horizon the two readings, and the restriction to stationary controllers, all give the same value, and in the finite horizon the two readings differ by an amount that decays geometrically in the horizon.

Timeline:

• 1973: Satia and Lave study MDPs with uncertain transition probabilities (Oper. Res. 21).
• 1994: Puterman's monograph collects the nominal theory, including the optimality of stationary deterministic policies for discounted finite MDPs (Wiley).
• 2001: Bagnell, Ng and Schneider state a robust Bellman recursion for stationary games without proof (CMU-RI-TR-01-25).
• 2005: Iyengar (Math. Oper. Res. 30) and Nilim and El Ghaoui independently prove the robust Bellman recursion under rectangular uncertainty; Nilim and El Ghaoui add Theorem 4.
• 2013: Wiesemann, Kuhn and Rustem extend robust MDPs beyond rectangular sets (Math. Oper. Res. 38).

Setting

States form a finite set $\mathcal X = \{0,\dots,n-1\}$ and actions a finite nonempty set $\mathcal A$. A stage cost $c(i,a)\ge 0$ is given for every state and action, together with a discount factor $0<\nu<1$ and an initial state $i_0$. For every action $a$ and state $i$ a nonempty set $\mathcal P_i^a$ of probability vectors in the simplex $\Delta_n$ is given: the possible rows of the transition matrix $P^a$. Rectangularity means that every row is chosen independently: one stage of nature is a family $(P^a)_{a\in\mathcal A}$ with $i$-th row of $P^a$ in $\mathcal P_i^a$, and the set of such families is $\mathcal Q$.

A controller policy $\pi=(\mathbf a_0,\mathbf a_1,\dots)$ assigns an action $\mathbf a_t(i)$ to each state at each stage; the set of all of them is $\Pi$, and the stationary ones (the same map at every stage) form $\Pi_s$. A nature policy $\tau=(P_t^a)$ picks one element of $\mathcal Q$ per stage; the set is $\mathcal T$, and the stationary ones form $\mathcal T_s$. Starting from $\mu_0 = e_{i_0}$, the state law evolves by $\mu_{t+1}(j)=\sum_i \mu_t(i)P_t^{\mathbf a_t(i)}(i,j)$. The discounted costs over horizon $N$ and over the infinite horizon are

$$C_N(\pi,\tau)=\sum_{t=0}^{N-1}\nu^t\sum_i\mu_t(i)\,c(i,\mathbf a_t(i)),\qquad C_\infty(\pi,\tau)=\lim_{N\to\infty}C_N(\pi,\tau).$$

For a controller class $\mathcal C\in\{\Pi,\Pi_s\}$ and a nature class $\mathcal S\in\{\mathcal T,\mathcal T_s\}$ the robust values are $\phi_\infty(\mathcal C,\mathcal S)=\inf_{\pi\in\mathcal C}\sup_{\tau\in\mathcal S}C_\infty(\pi,\tau)$ and $\phi_N(\Pi,\mathcal S)=\inf_{\pi\in\Pi}\sup_{\tau\in\mathcal S}C_N(\pi,\tau)$. Finally $c_{\max}=\max_{i,a}c(i,a)$ and $\varepsilon_N=\nu^Nc_{\max}/(1-\nu)$.

Formalization targets

Goal: Theorem 4 (p. 786)

$$\phi_\infty(\Pi,\mathcal T)=\phi_\infty(\Pi_s,\mathcal T_s)=\phi_\infty(\Pi_s,\mathcal T)=\phi_\infty(\Pi,\mathcal T_s),$$ $$0\le \phi_N(\Pi,\mathcal T)-\phi_N(\Pi,\mathcal T_s)\le \frac{\nu^N c_{\max}}{1-\nu}\quad\text{for every }N .$$

The second line is the paper's "the gap goes to zero at a geometric rate $\nu$", with the constant the paper's own argument produces.

Milestones (proof order of the paper)

1. Eq. (34): $C_N(\pi,\tau)\le C_\infty(\pi,\tau)\le C_N(\pi,\tau)+\varepsilon_N$ for all $\pi\in\Pi$, $\tau\in\mathcal T$, $N$.
2. Eq. (35): $\phi_N(\Pi,\mathcal T)\le\phi_\infty(\Pi,\mathcal T)\le\phi_N(\Pi,\mathcal T)+\varepsilon_N$.
3. Step (e): the same sandwich for $\phi_N(\Pi,\mathcal T_s)$ and $\phi_\infty(\Pi,\mathcal T_s)$.
4. Eq. (33): for every $\varepsilon>0$ and all large $N$, $\phi_\infty(\Pi_s,\mathcal T_s)-\varepsilon\le\phi_N(\Pi,\mathcal T)\le\phi_\infty(\Pi_s,\mathcal T_s)$.
5. Step (c): for every stationary $\pi$, $\sup_{\tau\in\mathcal T}C_\infty(\pi,\tau)=\sup_{\tau\in\mathcal T_s}C_\infty(\pi,\tau)$, hence $\phi_\infty(\Pi_s,\mathcal T)=\phi_\infty(\Pi_s,\mathcal T_s)$.
6. Step (d), nominal fact: for stationary $\tau$, $\inf_{\pi\in\Pi}C_N(\pi,\tau)\to\inf_{\pi\in\Pi_s}C_\infty(\pi,\tau)$.
7. Step (d): $\phi_\infty(\Pi,\mathcal T_s)=\phi_\infty(\Pi_s,\mathcal T_s)$.

Significance

The first half of Theorem 4 says that, for discounted robust MDPs with rectangular uncertainty, nothing is gained by either player from non-stationary behaviour: the controller may restrict itself to stationary deterministic policies and nature's time variation buys it nothing. This is what makes the stationary game (6), solved by the robust Bellman recursion of Theorem 3, the right infinite-horizon object. The second half is a quantitative guarantee for practitioners: solving the tractable time-varying problem (4) instead of the statistically motivated but hard stationary problem (3) costs at most $\nu^Nc_{\max}/(1-\nu)$ in value.

The result is proved on paper. As far as a search of the platform shows (September 2026), no robust MDP result has a machine-checked proof here; the nominal counterpart, optimality of stationary policies for discounted finite MDPs, is on the platform as BertsekasDP.discounted_main_theorem in a different model encoding (state-dependent control sets). A complete development contributes a reusable encoding of robust MDPs with time-varying and stationary adversaries, the truncation estimates for discounted costs, and a formal record of one step whose printed argument is incomplete (Step (d), see Difficulty).

Difficulty

The truncation estimates (34), (35) and Step (e) are elementary. The equalities in (31) are not: they compare values of games whose players have infinite-dimensional strategy sets, and the paper writes "min" and "max" where the infima and suprema need not be attained, since the row sets are neither closed nor convex. Two steps of the printed proof rely on results the mission does not import. Step (a) identifies $\phi_N(\Pi,\mathcal T)$ with iterates of the robust Bellman recursion, which is Theorems 1 and 3 of the paper (formalized in sibling missions of this series). Step (c) says only "following similar steps as in Step (a)". Step (d) is incomplete as printed: it shows that for each fixed stationary nature the controller's best time-varying and best stationary responses agree, which is a statement about a max–min value, whereas $\phi_\infty(\Pi,\mathcal T_s)$ is a min–max value. The obvious attempt to exchange the infimum over $\Pi$ with the supremum over $\mathcal T_s$ from that per-nature fact alone fails; the exchange requires a duality statement for the stationary game.

Formalization scope

States are Fin n; the action type is finite and nonempty. The row sets are an arbitrary family rows a i ⊆ stdSimplex ℝ (Fin n) with each set nonempty; nonemptiness is implicit in the paper and explicit here, and no convexity or closedness is assumed. A stage of nature is the subtype of families A → Fin n → (Fin n → ℝ) whose rows lie in the given sets, so rectangularity is built in. Controller policies are sequences ℕ → Fin n → A, nature policies sequences of stage choices; stationary policies of either player are the constant sequences. $C_N$ is defined from the forward state distribution (not from a Bellman recursion) and reads only stages $<N$, so the finite-horizon values over infinite sequences are exactly the paper's values (3) and (4) with stage costs $\nu^tc$ and zero terminal cost. $C_\infty$ is the sum of the series of nonnegative stage costs, which converges for $0\le\nu<1$ and equals $\lim_N C_N$. Every min and max of the paper is a real infimum ⨅ or supremum ⨆; all families are nonempty and lie in $[0,c_{\max}/(1-\nu)]$, and attainment is not assumed anywhere. The discount factor satisfies $0<\nu<1$, as in §4 of the paper.

The rate in the goal is the explicit bound $\nu^Nc_{\max}/(1-\nu)$; a formalization stating only that the gap tends to zero, or stating (31) with the infinite-horizon cost replaced by a Bellman fixed point, proves a different theorem and is not accepted.

A complete development needs: the stochastic-matrix facts for the forward distribution, geometric-series bounds, robust value iteration for the time-varying and the stationary adversary, and nominal stationarity of discounted MDPs. The model and truncation estimates are reusable for any discounted robust MDP result. Contributions of any milestone, and of proofs of Step (c) and Step (d) by any route, are welcome.

Selected references

• A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
• J. K. Satia, R. E. Lave, Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• J. A. Bagnell, A. Y. Ng, J. Schneider, Solving Uncertain Markov Decision Processes, Technical Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001.
• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov Decision Processes, Mathematics of Operations Research 38(1):153–183, 2013. https://doi.org/10.1287/moor.1120.0566

Motivation

A robust Markov decision process replaces the unknown transition probabilities of an MDP by sets of plausible values and optimises against the worst case. Nilim and El Ghaoui (Oper. Res. 53 (2005)) showed that, when the uncertainty is rectangular (each row of each transition matrix varies independently in its own set), the robust problem is solved by a Bellman-type recursion. Each step of that recursion needs, for every state and action, the value of an inner problem: the largest expectation of the next-stage value vector over the uncertainty set of one transition row. The recursion is only as tractable as this inner problem.

The paper studies several uncertainty models built from statistical estimates of the transition rows. In the entropy model the uncertain row is any distribution within a prescribed Kullback–Leibler divergence of a nominal distribution. For this model the paper reduces the inner problem to the minimisation of a scalar convex function, which is then solved by bisection. Iyengar (Math. Oper. Res. 30 (2005)) obtained the same robust recursion independently, and the same scalar reduction is the basic computation in later KL-constrained distributionally robust optimisation. This mission formalizes that reduction and the properties of the scalar function that the paper derives from it.

Setting

Let $n\ge 1$ and let $\Delta_n=\{p\in\mathbb R^n : p\ge 0,\ \sum_j p(j)=1\}$ be the probability simplex. For $p,q\in\mathbb R^n$ the Kullback–Leibler divergence is

$$D(p\|q)=\sum_j p(j)\log\frac{p(j)}{q(j)},$$

with $0\log 0=0$. Fix a nominal distribution $q\in\Delta_n$ with $q(j)>0$ for every $j$, and a level $\beta>0$. The entropy uncertainty set is

$$\mathcal P=\{p\in\Delta_n : D(p\|q)\le\beta\}.$$

For a vector $v\in\mathbb R^n$ (in the MDP, the value function of the next stage), the inner problem (17) is

$$\sigma_{\mathcal P}(v)=\max_{p\in\mathcal P} p^{\mathsf T}v .$$

The paper's scalar dual function (47) is, for $\lambda>0$,

$$\sigma(\lambda)=\lambda\log\Big(\sum_j q(j)\,e^{v(j)/\lambda}\Big)+\beta\lambda .$$

Write $v_{\max}=\max_j v(j)$ and $Q(v)=\sum_{j:\,v(j)=v_{\max}}q(j)$, the $q$-mass of the maximisers of $v$. The tilted distribution at $\lambda>0$ is $p^*(j)=q(j)e^{v(j)/\lambda}/\sum_i q(i)e^{v(i)/\lambda}$.

In Lean, vectors are Fin n → ℝ, $\Delta_n$ is stdSimplex ℝ (Fin n), and $D$, $\mathcal P$, $\sigma$, $p^*$, $v_{\max}$, $Q(v)$ are klDiv, klBall, dualFn, tiltedDist, vmax, maxMass in the namespace RobustMDP.EntropyInner.

Formalization targets

Goal: the dual of the inner problem (§6.2, Eq. (47), p. 791)

$$\max_{p\in\mathcal P} p^{\mathsf T}v=\inf_{\lambda>0}\sigma(\lambda),$$

with the maximum attained. This is kl_ball_inner_problem_dual. It holds for every $n$, every $v$, every $q>0$ in $\Delta_n$ and every $\beta>0$.

Milestones

1. §6.1: $\max_{p\in\Delta_n}D(p\|q)=\max_i(-\log q_i)$, and for $\beta\ge\max_i(-\log q_i)$ the set $\mathcal P$ is all of $\Delta_n$ and the inner value is $v_{\max}$.
2. Eq. (48): $q^{\mathsf T}v+\beta\lambda\le\sigma(\lambda)\le v_{\max}+\beta\lambda$ for $\lambda>0$.
3. §6.2, the optimal distribution: $p^{\mathsf T}v-\lambda D(p\|q)\le\lambda\log\sum_j q(j)e^{v(j)/\lambda}$ on $\Delta_n$, with equality at $p^*$.
4. §6.2, elimination of $\mu$: $\min_{\mu}\big[\mu+\beta\lambda+\lambda\sum_j q(j)e^{(v(j)-\mu)/\lambda-1}\big]=\sigma(\lambda)$.
5. Eq. (49): $\sigma(\lambda)=v_{\max}+(\beta+\log Q(v))\lambda+o(\lambda)$ as $\lambda\to0^+$.
6. Eq. (50): $\sigma(\lambda)=q^{\mathsf T}v+\beta\lambda+o(1)$ as $\lambda\to\infty$.
7. §6.3: if $\beta\ge-\log Q(v)$, then $\inf_{\lambda>0}\sigma=v_{\max}$ and the inner value is $v_{\max}$.

Significance

The goal turns an $n$-dimensional optimisation over a nonpolyhedral convex set into a one-dimensional convex minimisation whose objective costs $O(n)$ to evaluate. Combined with the bisection bracket from (48) and the behaviour at $0$ from (49), it gives the paper's $O(n\log(v_{\max}/\delta))$ cost per inner problem (§6.4), and hence the per-step cost of the robust Bellman recursion under entropy uncertainty. Milestone 7 identifies exactly when the uncertainty set is large enough that the robust step ignores the nominal model; unlike the cruder threshold of milestone 1, it depends on $v$.

The result is proved in the paper modulo "standard duality arguments". The paper gives no proof of the duality step itself, and its expansions (49)–(50) are proved only in outline in Appendix C. No formal proof of any of these statements is known to exist; Mathlib has the measure-theoretic Donsker–Varadhan ingredients but not the finite, constrained dual stated here. The mission produces a machine-checked version of the whole chain, with the attainment questions (which side is a max, which is only an infimum) settled explicitly.

Difficulty

The inequality $\max_{\mathcal P}p^{\mathsf T}v\le\sigma(\lambda)$ for every $\lambda>0$ is the routine half. The obstacle is the reverse inequality. The paper appeals to Lagrangian strong duality under a Slater condition, but the Lagrangian dual function equals $\sigma(\lambda)$ only for $\lambda>0$; at $\lambda=0$ it is $v_{\max}$, and the dual infimum may be approached only as $\lambda\to0^+$. A proof that looks for a minimiser $\lambda^*>0$ and a matching primal point $p^*$ fails in precisely the regime $\beta\ge-\log Q(v)$ of milestone 7, where no such $\lambda^*$ exists and the primal optimum sits on the face of the simplex spanned by the maximisers of $v$. The strong-duality argument must also handle the boundary of $\Delta_n$, where $D(\cdot\|q)$ is not differentiable.

Formalization scope

• Vectors are Fin n → ℝ; $\Delta_n$ is stdSimplex ℝ (Fin n). $D(p\|q)$ is a local finite sum with Lean's $\log 0=0$, which gives $0\log0=0$; Mathlib's measure-valued InformationTheory.klDiv is not used.
• Standing hypotheses in every theorem: $q\in\Delta_n$, $q(j)>0$ for all $j$, and $\beta>0$, as in §6.1. No restriction on $v$ is imposed; the "without loss of generality $v\ge0$" of the paper's §5 is not assumed here.
• The primal "max" is stated with IsGreatest (attained, since the KL ball is compact). The paper's "$\min_{\lambda>0}\sigma(\lambda)$" is an infimum, stated with IsGLB over $\{\sigma(\lambda):\lambda>0\}$: it is not attained when $\beta\ge-\log Q(v)$.
• dualFn is total in $\lambda$ and equals $0$ at $\lambda=0$ (division by zero), not the paper's $\sigma(0)=v_{\max}$. Every statement uses $\lambda>0$; the value at $0$ appears as the one-sided limit of (49). Accordingly (48) is stated for $\lambda>0$.
• $v_{\max}$ is ⨆ j, v j, the attained maximum over the finite nonempty index set; $\max_i(-\log q_i)$ likewise.
• (49) is stated as a limit along 𝓝[>] 0 together with a little-o remainder; (50) as a limit along atTop.
• Milestone 7 uses the non-strict condition $\beta\ge-\log Q(v)$ of the paper's first sentence, which contains the strict version of its second.
• Trivializing formalizations are excluded: the statements quantify over all $n$, $v$ and $q$, so a constant $v$, $n=1$, or the whole-simplex case of milestone 1 does not discharge the goal.

Useful infrastructure: a finite Gibbs variational inequality, compactness of the KL ball, and convexity and one-sided asymptotics of the log-sum-exp function in the temperature parameter. These are reusable for any KL-constrained robust optimisation mission. Proofs of the milestones, alternative proofs of the goal that avoid a general strong-duality theorem, and the sharper $O(\lambda e^{-t/\lambda})$ remainder of Appendix C are all welcome.

Selected references

• A. Nilim and L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• M. D. Donsker and S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time, I, Communications on Pure and Applied Mathematics 28(1):1–47, 1975. https://doi.org/10.1002/cpa.3160280102

Motivation

Linear programs solved in practice carry data that are measured, estimated or rounded. Ben-Tal and Nemirovski (Math. Program. 88, 2000) examined the NETLIB collection of real-world LPs and found that in 13 of them a relative perturbation of only 0.01% in the "ugly" coefficients of the inequality constraints can make the nominal optimal solution more than 50% infeasible (§2.3). Their remedy is the robust counterpart methodology: replace the nominal problem by a deterministic problem whose feasible solutions remain nearly feasible for every, or for all but a small probability of, data realizations.

The paper made the approach concrete for entry-wise uncertainty and gave the probabilistic guarantee that became a standard tool of robust and chance-constrained optimization. The main steps of the history are:

• 1973, A. L. Soyster: the interval (worst-case, "box") counterpart, here called (IRC).
• 1998–1999, Ben-Tal and Nemirovski (Math. Oper. Res. 23; Oper. Res. Lett. 25), and independently El Ghaoui and co-authors: robust optimization with ellipsoidal uncertainty sets.
• 2000, this paper: the ellipsoid-plus-box counterpart (RC[ε, δ, Ω]) and Proposition 1, which bounds each constraint's violation probability by $\exp\{-\Omega^2/2\}$ under independent symmetric perturbations.
• 2004, Bertsimas and Sim (Oper. Res. 52): the budgeted counterpart, with an analogous probability bound.

Setting

An uncertain linear program is

$$\text{minimize } c^Tx\quad\text{s.t.}\quad Ex=e,\qquad Ax\le b,\qquad \ell\le x\le u,\tag{LP}$$

with $x\in\mathbb{R}^n$, $E\in\mathbb{R}^{p\times n}$, $A=(a_{ij})\in\mathbb{R}^{m\times n}$, and bounds $\ell_j\in\mathbb{R}\cup\{-\infty\}$, $u_j\in\mathbb{R}\cup\{+\infty\}$. For each inequality row $i$ a set $J_i\subseteq\{1,\dots,n\}$ lists the uncertain entries $a_{ij}$, $j\in J_i$. Only these entries are uncertain; $E,e,b,\ell,u,c$ are exact.

Given an uncertainty level $\epsilon>0$ and a feasibility tolerance $\delta>0$, write $b_i^+=b_i+\delta\max[1,|b_i|]$.

• $x$ is reliable if it is feasible for (LP) and $\sum_{j\notin J_i}a_{ij}x_j+\sum_{j\in J_i}\tilde a_{ij}x_j\le b_i^+$ for every $i$ and every choice of $\tilde a_{ij}$ with $|\tilde a_{ij}-a_{ij}|\le\epsilon|a_{ij}|$.
• In the random symmetric uncertainty model, the true coefficients are $\tilde a_{ij}=(1+\epsilon\xi_{ij})a_{ij}$, where $\xi_{ij}=0$ for $j\notin J_i$ and, for each row $i$, $\{\xi_{ij}\}_{j\in J_i}$ are independent random variables, each symmetrically distributed in $[-1,1]$.
• $x$ is almost reliable with level $\kappa$ if it is feasible for (LP) and $\Pr\{\sum_j\tilde a_{ij}x_j>b_i^+\}\le\kappa$ for every $i$.

The robust counterpart (RC[ε, δ, Ω]), with a safety parameter $\Omega>0$, has variables $x_j$, $y_{ij}$, $z_{ij}$ and constraints $Ex=e$, $Ax\le b$, $\ell\le x\le u$, $-y_{ij}\le x_j-z_{ij}\le y_{ij}$ for all $i,j$, and

$$\sum_j a_{ij}x_j+\epsilon\Big[\sum_{j\in J_i}|a_{ij}|y_{ij}+\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}\Big]\le b_i^+\qquad\forall i.$$

The interval robust counterpart (IRC[ε, δ]) has variables $x_j,y_j$ and the constraint $\sum_ja_{ij}x_j+\epsilon\sum_{j\in J_i}|a_{ij}|y_j\le b_i^+$ with $-y_j\le x_j\le y_j$, besides the nominal ones. Problem (∗) is the same with $y_j$ replaced by $|x_j|$.

Formalization targets

Goal: Proposition 1 (pp. 418–419)

If $x$ extends to a feasible solution $(x,y,z)$ of (RC[ε, δ, Ω]), then $x$ is feasible for (LP) and, for every $i$,

$$\Pr\Big\{\sum_j(1+\epsilon\xi_{ij})a_{ij}x_j>b_i+\delta\max[1,|b_i|]\Big\}\le\exp\{-\Omega^2/2\}.$$

Milestones

1. The reduction in the proof of Proposition 1 (p. 419), in corrected pointwise form: a violation of row $i$ forces $\sum_{j\in J_i}\xi_{ij}a_{ij}z_{ij}>\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}$.
2. Eq. (1), p. 419: for independent symmetric $\eta_j\in[-1,1]$ and reals $p_j$,

$$\Pr\Big\{\sum_j\eta_jp_j>\Omega\sqrt{\textstyle\sum_jp_j^2}\Big\}\le\exp\{-\Omega^2/2\}.$$

3. $x$ is reliable iff it is feasible for (∗) (p. 417).
4. (∗) is equivalent to (IRC[ε, δ]) (pp. 417–418).
5. Every feasible solution of (IRC) yields one of (RC) with $y_{ij}=y_j$, $z_{ij}=0$ (p. 420).
6. Feasibility for (LP) together with $\sum_ja_{ij}x_j+\epsilon\beta_i(x)\le b_i^+$, $\beta_i(x)=\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2x_j^2}$, suffices to extend $x$ to (RC) (p. 420).
7. The ratio $\alpha_i(x)/\beta_i(x)$, $\alpha_i(x)=\sum_{j\in J_i}|a_{ij}||x_j|$, is at most $\sqrt{\mathrm{card}(J_i)}/\Omega$, with equality attained (p. 420, corrected).

Significance

Proposition 1 turns a probabilistic requirement, which is hard to handle directly, into a single convex (second-order-cone) program. The bound $\exp\{-\Omega^2/2\}$ does not depend on the dimension, on the number of uncertain entries, or on which symmetric distributions the perturbations follow, so $\Omega$ can be chosen from the desired reliability level alone. Together with milestones 3–6, the mission certifies the whole chain: the worst-case notion of reliability is exactly Soyster's linear program (IRC), and (RC) is never more conservative than (IRC), with an advantage that can reach the factor $\sqrt{\mathrm{card}(J_i)}/\Omega$.

The results are proved in the paper; to our knowledge none of them is machine-checked. A formal development produces a reusable model of entry-wise uncertain LPs, the counterparts (∗), (IRC) and (RC) as Lean predicates, and a Hoeffding-type bound for weighted sums of symmetric bounded variables in the exact form (1). The platform's HighDimProb.Concentration.hoeffding_rademacher covers the Rademacher special case only.

Difficulty

The deterministic parts (milestones 1, 3–7) are elementary: worst cases of interval perturbations, and the Cauchy–Schwarz inequality. The obstacle lies in the probabilistic step. The printed proof passes from $\xi_{ij}a_{ij}$ to $\xi_{ij}|a_{ij}|$ with an equality that holds only in distribution, and contains index misprints, so it cannot be transcribed line by line; the reduction has to be restated pointwise. Eq. (1) is a tail bound for general symmetric variables in $[-1,1]$, not only for random signs; the step (c) of the printed proof of (1) is written as an equality that holds only for random signs, so that proof too needs repair. The degenerate case $\sum_jp_j^2=0$ must be handled rather than assumed away.

Formalization scope

• Data are a structure UncertainLP n p m over Fin indices (0-based), with A : Matrix (Fin m) (Fin n) ℝ, J : Fin m → Finset (Fin n) arbitrary, and EReal bounds so that infinite bounds are expressible. The objective $c$ is omitted: no statement involves it.
• The probability space is $(S,\mathbb P)$ with IsProbabilityMeasure; the name $S$ avoids a clash with the safety parameter $\Omega$. Symmetry is equality of the laws of $\xi_{ij}$ and $-\xi_{ij}$; values lie in $[-1,1]$ at every outcome; independence is required within each row only, with no identical distribution (§3.1 says only "independent", which is weaker than the "iid" of §2.2). Probabilities are P.real.
• The hypotheses $\epsilon>0$, $\delta>0$, $\Omega>0$ are the paper's standing assumptions and are carried by every theorem that mentions the parameter.
• Corrections of the printed text: $a_{ij}x_i\to a_{ij}x_j$ in (IRC); $\sum_{j\in J}\to\sum_{j\in J_i}$ in (RC); the reduction of milestone 1 is stated with $a_{ij}$ and $z_{ij}$ in place of the printed $|a_{ij}|$, $x_i-y_{ij}$ and $y_j$, $y_{ij}$; and the ratio of milestone 7 carries the factor $1/\Omega$ that the printed "$\sqrt{\mathrm{card}(J_i)}$" omits.
• Ruling out trivializations: the violation event uses the signed multiplicative model $(1+\epsilon\xi_{ij})a_{ij}$, never $|a_{ij}|$ or an additive perturbation; the goal concludes both nominal feasibility (i) and the probability bound (ii′) for every row; no hypothesis excludes the degenerate case $\sum_{j\in J_i}a_{ij}^2z_{ij}^2=0$; and the probability model is satisfiable (e.g. by $\xi\equiv0$ or by Rademacher signs), so the goal is not vacuous.
• The numerical remarks of the paper (0.92, 5.24, $10^{-6}$, "at least 30") and the NETLIB case study are not formalized.
• Reusable beyond this mission: the uncertain-LP model and the three counterparts, and the tail bound (1). Contributions of general lemmas about symmetric bounded random variables are welcome.

Selected references

• A. Ben-Tal, A. Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Math. Program. Ser. A 88 (2000) 411–424. https://doi.org/10.1007/s101070000163
• A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Oper. Res. 21 (1973) 1154–1157. https://doi.org/10.1287/opre.21.5.1154
• A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23 (1998) 769–805. https://doi.org/10.1287/moor.23.4.769
• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Oper. Res. Lett. 25 (1999) 1–13. https://doi.org/10.1016/S0167-6377(99)00016-4
• D. Bertsimas, M. Sim, The price of robustness, Oper. Res. 52 (2004) 35–53. https://doi.org/10.1287/opre.1030.0065
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

Motivation

Robust optimization (RO) protects a decision against every realisation of an uncertain parameter in a prescribed uncertainty set; distributionally robust stochastic programming (DRSP) protects it against every probability distribution in a prescribed distribution set. The two paradigms are usually treated separately. When the n uncertain parameters live in different spaces, it is folklore that RO over a product of sets is DRSP over the distributions supported on that product (Delage and Ye, Operations Research 2010).

In data-driven problems the situation is different: the parameters $x_1,\dots,x_n$ are samples, and all of them lie in the same space $\mathbb R^m$. Robustifying each sample by its own uncertainty set $\mathcal Z_i$ gives the objective $\sum_i c_i\inf_{x_i\in\mathcal Z_i}f(x_i)$, and the sets $\mathcal Z_i$ typically overlap. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that this objective is again a worst-case expectation, now over distributions on $\mathbb R^m$ itself rather than on $\mathbb R^{m\times n}$. This equivalence is what the same paper uses to prove that box-robust sample average optimisation is statistically consistent, and to explain the shrinkage heuristic of RO.

Setting

Let $m,n\ge1$ and write $[1:n]=\{1,\dots,n\}$. Let $\mathcal P$ be the set of Borel probability measures on $\mathbb R^m$. The data are:

• a measurable utility $f:\mathbb R^m\to\mathbb R$ (the decision variable is suppressed);
• weights $c_1,\dots,c_n>0$ with $\sum_{i=1}^n c_i=1$;
• nonempty Borel uncertainty sets $\mathcal Z_1,\dots,\mathcal Z_n\subseteq\mathbb R^m$, which may intersect or coincide.

For $S\subseteq[1:n]$ write $\mathcal Z_S=\bigcup_{i\in S}\mathcal Z_i$ and $N=[1:n]$. The distribution set is

$$\mathcal P_n=\Big\{\mu\in\mathcal P\ \Big|\ \forall S\subseteq[1:n]:\ \mu(\mathcal Z_S)\ge\sum_{i\in S}c_i\Big\}.$$

Each $\mu\in\mathcal P_n$ must give every union of uncertainty sets at least the total weight of its indices. For $\mu\in\mathcal P$ the expectation $\int f\,d\mu$ is the extended integral $\int f^+d\mu-\int f^-d\mu\in[-\infty,+\infty]$.

Formalization targets

Goal: Theorem 2.1 (Eq. (4), pp. 96–97)

$$\sum_{i=1}^n\Big[c_i\inf_{x_i\in\mathcal Z_i}f(x_i)\Big]=\inf_{\mu\in\mathcal P_n}\int_{\mathbb R^m}f(x)\,d\mu(x),$$

as an identity in $[-\infty,+\infty]$, with no boundedness assumption on $f$ and no disjointness assumption on the $\mathcal Z_i$.

Milestones (proof of Theorem 2.1, p. 97)

1. Every $\mu\in\mathcal P_n$ satisfies $\mu(\mathbb R^m\setminus\mathcal Z_N)=0$, hence $\int_{\mathbb R^m}f\,d\mu=\int_{\mathcal Z_N}f\,d\mu$.
2. Weak duality. With $f_i=\inf_{\mathcal Z_i}f$ finite, every $\alpha\in\mathbb R^{2^n}$ satisfying $\sum_S\alpha_S\mathbf 1(x\in\mathcal Z_S)\le f(x)$ on $\mathcal Z_N$ and $\alpha_S\ge0$ for $S\ne N$ obeys $\sum_i c_i\sum_S\alpha_S\mathbf 1(i\in S)\le\sum_i c_if_i$.
3. The nested dual solution. If $f_1\ge\dots\ge f_n$, the vector with $\alpha_{\{1,\dots,i\}}=f_i-f_{i+1}$, $\alpha_N=f_n$ and all other coordinates $0$ is feasible and has objective $\sum_i c_if_i$.

Further statements

• For pairwise disjoint $\mathcal Z_i$: $\mathcal P_n=\{\mu\in\mathcal P\mid\mu(\mathcal Z_i)=c_i,\ i=1,\dots,n\}$ (p. 97).
• Corollary 2.1 (Eq. (5)): $\inf_{x'\in\mathcal Z}f(x')=\inf_{\mu\in\mathcal P,\ \mu(\mathcal Z)=1}\int f\,d\mu$.
• Corollary 5.2 (nested distributions, p. 107): for $\mathcal Z_1\subseteq\dots\subseteq\mathcal Z_n$ and $0=p_0<p_1<\dots<p_n=1$,

$$\inf_{\mu\in\mathcal P,\ \mu(\mathcal Z_i)\ge p_i\ \forall i}\int f\,d\mu=\sum_{i=1}^n(p_i-p_{i-1})\inf_{x_i\in\mathcal Z_i}f(x_i).$$

Significance

The result. Theorem 2.1 turns a robust problem with overlapping uncertainty sets into a distributionally robust one on the original space $\mathbb R^m$. This is what allows distributions in $\mathcal P_n$ to be compared with the true data-generating distribution as $n$ grows: in §3 of the paper a kernel density estimator is shown to lie in $\mathcal P_n$ for box uncertainty sets, which yields consistency of box-robust sample average optimisation (Theorem 3.1); in §4.2 the nested-distribution form (Corollary 5.2) explains why shrinking an uncertainty set approximates a two-scenario DRSP (Theorem 4.1). The disjoint case recovers the classical product-space equivalence.

Formalizing it. The result is proved in the paper, through the strong duality of a semi-infinite linear program (Isii 1962). It has no machine-checked proof. The mission produces the equivalence as an identity of extended reals, together with a reusable definition of the union-mass distribution set. A proof need not follow the paper's duality route; any correct argument is welcome.

Difficulty

The inequality $\ge$ from the left side is the easy half: point masses $\sum_ic_i\delta_{x_i}$ with $x_i\in\mathcal Z_i$ belong to $\mathcal P_n$. The substance is the reverse bound, that no $\mu\in\mathcal P_n$ can do better than $\sum_ic_if_i$. For disjoint sets this is immediate, since $\mu(\mathcal Z_i)=c_i$. For overlapping sets a measure may place mass in intersections, and a single point of $\mathcal Z_i\cap\mathcal Z_j$ can serve several indices at once; the constraint family over all $2^n$ subsets is what prevents this, and the bound has to exploit the whole family, not the singleton constraints. The paper does this by appeal to semi-infinite LP duality, a theorem that Mathlib does not contain. Measure-theoretic side conditions (unbounded $\mathcal Z_i$, infinite integrals, infima equal to $-\infty$) must also be handled rather than assumed away.

Formalization scope

• $\mathbb R^m$ is Fin m → ℝ with its Borel $\sigma$-algebra; no norm is used. Indices $1,\dots,n$ are Fin n, subsets are Finset (Fin n), and $\{1,\dots,i\}$ is Finset.Iic i.
• $\mathcal P_n$ is a Set (Measure (Fin m → ℝ)) whose membership includes IsProbabilityMeasure; the constraint is imposed for every subset, $\emptyset$ and $[1:n]$ included.
• $\int f\,d\mu$ is expect μ f, defined in EReal as the difference of two lower Lebesgue integrals, $\int f^+-\int f^-$. The Bochner integral is not used, because its value $0$ on non-integrable functions would falsify Eq. (4). Both sides of Eq. (4) are EReal infima; the left infimum ranges over the nonempty set $\mathcal Z_i$.
• Readings of the printed statements. (i) The paper allows $f$ to take the value $-\infty$; here $f$ is real-valued. The excluded case is the one the proof disposes of in its first sentence, where both sides are $-\infty$. (ii) No boundedness hypothesis is added: when some $\inf_{\mathcal Z_i}f=-\infty$ both sides are $-\infty$, and otherwise every $\mu\in\mathcal P_n$ has a finite negative part. (iii) Corollary 2.1 prints "$f:\mathbb R\cup\{-\infty\}$" without a domain; it is read as $f:\mathbb R^m\to\mathbb R$. (iv) Corollary 5.2 is corrected: the paper prints the coefficient $(p_n-p_{n-1})$, while its proof sets $c_i=p_i-p_{i-1}$; the printed version is false (for $\mathcal Z_1=\{a\}\subseteq\mathcal Z_2=\{a,b\}$, $f(a)=1$, $f(b)=0$, $p_1=1/4$, the left side is $1/4$ and the printed right side $3/4$). The mission states $(p_i-p_{i-1})$. (v) The standing hypotheses of Theorem 2.1 ($f$ measurable, $\mathcal Z_i$ nonempty Borel) are made explicit in Corollary 5.2.
• The ordering $f_1\ge\dots\ge f_n$ is a hypothesis of the nested-dual milestone only, as the proof's "without loss of generality"; the goal does not assume it. Milestones 2 and 3 assume $f$ bounded below on each $\mathcal Z_i$ (the proof's first reduction), so that $f_i$ is a real number.
• Ruled out. A Bochner-integral formulation, a restriction to disjoint sets, a distribution set containing non-probability measures, or a set $\mathcal P_n$ defined by the singleton constraints $\mu(\mathcal Z_i)\ge c_i$ alone would each change or trivialise the theorem; none is used.
• Definitions (file Model): the set $\mathcal P_n$, the extended expectation, dual feasibility, and the nested dual vector. The extended expectation and the union-mass distribution set are reusable beyond this mission. Welcome contributions: a proof through semi-infinite LP duality, a direct measure-theoretic proof (for instance a layer-cake argument for the lower bound), and proofs of the corollaries from the goal.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14:185–197, 1962. https://doi.org/10.1007/BF02868641
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050

Why robustify a sampled stochastic program

Many decision problems under uncertainty take the form of a stochastic program: choose a decision $v$ from a feasible set $\mathcal F$ to maximise the expected utility $\mathbb E_{x\sim\mu}[f(v,x)]$, where the distribution $\mu$ of the uncertain parameter $x\in\mathbb R^m$ is known only through i.i.d. samples $x_1,\dots,x_n$. The standard remedy, sample average approximation, maximises $\frac1n\sum_i f(v,x_i)$ instead. Its consistency (convergence of the optimal expected utility of its solutions to the true optimum) is classical, but it needs regularity assumptions of its own, for example those of King and Wets (Stochastics and Stochastic Reports, 1991), cited on p. 98 of the paper; the paper presents its construction as a route to consistency under weaker conditions.

Robust optimization (RO) takes a different route: it protects each sample by an uncertainty set and optimises against the worst point in it. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that RO over several overlapping uncertainty sets is equivalent to a distributionally robust stochastic program (their Theorem 2.1, the subject of mission I of this series). Section 3 of the paper uses that equivalence to show that a specific robustification of the sampled problem, with $\ell_\infty$ boxes of shrinking radius around each sample, is consistent under only boundedness and equicontinuity of $f$. This mission formalizes that result, Theorem 3.1.

Setting

Equip $\mathbb R^m$ with the sup norm $\|z\|_\infty=\max_k|z_k|$, its Borel $\sigma$-algebra and Lebesgue measure $dx$. The data are:

• a set of decisions $V$ and a nonempty feasible set $\mathcal F\subseteq V$;
• a utility $f:V\times\mathbb R^m\to\mathbb R$, Borel measurable in $x$ for each $v$;
• a true density $h^*$ on $\mathbb R^m$ (nonnegative, $\int h^*\,dx=1$) and i.i.d. samples $x_1,x_2,\dots$ with distribution $h^*(x)\,dx$;
• radii $\epsilon(n)>0$.

For a sample $x_1,\dots,x_n$ the boxes are $\mathcal Z_i=\{x_i+\delta\mid\|\delta\|_\infty\le\epsilon(n)\}$, and the box-robust sample objective is

$$J_n(v)=\frac1n\sum_{i=1}^n\ \inf_{\|\delta_i\|_\infty\le\epsilon(n)}f(v,x_i+\delta_i)=\sum_{i=1}^n\frac1n\inf_{x_i'\in\mathcal Z_i}f(v,x_i').$$

The RO solution $v(n)$ is a maximiser of $J_n$ over $\mathcal F$. The equicontinuity modulus of $f$ is

$$d(\epsilon)=\sup_{v,\,x,\ \|\delta\|_\infty\le\epsilon}|f(v,x)-f(v,x+\delta)|.$$

The proof works with the distribution set $\mathcal P_n$ of probability measures $\mu$ with $\mu(\bigcup_{i\in S}\mathcal Z_i)\ge|S|/n$ for every $S\subseteq\{1,\dots,n\}$, and with the uniform box kernel density estimator

$$h_n(x)=(n\epsilon(n)^m)^{-1}\sum_{i=1}^nK\Big(\frac{x-x_i}{\epsilon(n)}\Big),\qquad K(z)=\frac{\mathbf 1(\|z\|_\infty\le1)}{2^m}.$$

Formalization targets

Goal: Theorem 3.1 (p. 98)

Assume $|f(v,x)|\le C$ for all $v,x$; $d(\epsilon)\to0$ as $\epsilon\downarrow0$; $\epsilon(n)\downarrow0$ and $n\epsilon(n)^m\uparrow\infty$. Then for every choice of maximisers $v(n)$, with probability one,

$$\lim_{n\to\infty}\int_{\mathbb R^m}f(v(n),x)\,h^*(x)\,dx=\sup_{v\in\mathcal F}\int_{\mathbb R^m}f(v,x)\,h^*(x)\,dx .$$

Milestones (proof of Theorem 3.1, p. 99)

1. $h_n$ is the density of a probability measure in $\mathcal P_n$.
2. $J_n(v)\le\int f(v,x)\,h_n(x)\,dx$ for every $v$.
3. Oscillation over a box: $\sup_{\mathcal Z_i}f(v,\cdot)-\inf_{\mathcal Z_i}f(v,\cdot)\le d(2\epsilon(n))$.
4. Eq. (7): with $M_n=C\int|h_n-h^*|\,dx$, for every $v$,

$$J_n(v)-M_n\le\int f(v,x)h^*(x)\,dx\le J_n(v)+M_n+d(2\epsilon(n)).$$

5. Strong $L^1$ consistency of the box kernel density estimator: if $\epsilon(n)\to0$ and $n\epsilon(n)^m\to\infty$, then $\int|h_n-h^*|\,dx\to0$ almost surely.

Milestones 1–4 are deterministic statements about a fixed sample; milestone 5 is the only probabilistic input.

Significance

Theorem 3.1 gives consistency of a tractable robust reformulation of a sampled stochastic program under conditions the paper notes are weaker than those of King and Wets for sampled stochastic programs: $f$ need only be bounded and equicontinuous in $x$, uniformly in $v$, and the true distribution need only have a density. It also gives an explicit schedule for the size of the uncertainty set, $\epsilon(n)\to0$ with $n\epsilon(n)^m\to\infty$, the bandwidth condition of kernel density estimation. Section 4 of the paper applies the same distributional interpretation to regularised learning methods such as the support vector machine and the Lasso.

The result is proved in the paper, with the $L^1$ consistency of kernel density estimators (Devroye 1983; Devroye and Györfi 1985) cited rather than proved. No part of it is formalized in Lean or on this platform as far as a search of the platform found. A complete development would produce, besides Theorem 3.1, a machine-checked strong $L^1$ consistency theorem for kernel density estimators, which is a basic result of nonparametric statistics in its own right.

Difficulty

The deterministic part (milestones 1–4) is measure-theoretic bookkeeping: the kernel integrates to one only because the box is a sup-norm ball of volume $(2\epsilon)^m$, and every infimum and supremum must be handled with care, since $f$ need not attain them.

The obstacle is milestone 5. Almost-sure $L^1$ convergence of $h_n$ to an arbitrary density $h^*$, with no continuity or support assumption, does not follow from the strong law of large numbers applied pointwise: $h_n(x)$ is an average of $n$ terms whose law changes with $n$ through $\epsilon(n)$, and almost-sure convergence at each fixed $x$ does not give convergence of the integral along a single sample path. The theorem needs both a bias estimate valid for every integrable density and a concentration estimate for the random $L^1$ error. Mathlib has Lebesgue differentiation and the strong law, but no kernel density estimator and no such concentration result.

Formalization scope

• $\mathbb R^m$ is Fin m → ℝ, whose Mathlib norm is the sup norm; boxes are Metric.closedBall. The integrals $\int f(v,x)h^*(x)\,dx$ are Bochner integrals against Lebesgue measure of integrable integrands.
• The samples are a sequence X : ℕ → Ω → Fin m → ℝ on a probability space, independent (iIndepFun) and each with law volume.withDensity h*; $x_1,x_2,\dots$ become X 0, X 1, …, and the $n$-th problem uses the first $n$. "With probability one" is ∀ᵐ ω ∂P.
• The goal quantifies over every selection $v(n)$ of maximisers, with no measurability assumed; a version with one chosen maximiser would be weaker and is ruled out.
• Readings and corrections of the printed text:
  • the kernel argument printed $(x-x_i)/\epsilon$ on p. 98 is read as $(x-x_i)/\epsilon(n)$, as the proof on p. 99 writes it;
  • "$\max_{v,x}|f(v,x)|\le C$" is read as the uniform bound $|f|\le C$ and the "max" in $d(\epsilon)$ as a supremum;
  • "$d(\epsilon)\downarrow0$" is read as $d(\epsilon)\to0$ as $\epsilon\downarrow0$;
  • implicit hypotheses made explicit: $\mathcal F\ne\emptyset$, $\epsilon(n)>0$, measurability of $f(v,\cdot)$, $h^*$ a Lebesgue density;
  • the monotonicity in "$\epsilon(n)\downarrow0$, $n\epsilon(n)^m\uparrow\infty$" is kept in the goal; milestone 5 uses the limits only, as the paper states it;
  • the paper's $M_n$ ("there exists $\{M_n\}\to0$") is made explicit as $M_n=C\int|h_n-h^*|$, so Eq. (7) is stated for every sample.
• Remark 3.2 and Appendix B (an integrable envelope in place of boundedness) are not part of this mission.
• Every real infimum and supremum ranges over a nonempty set of values bounded by $C$ in absolute value, so no statement holds through a junk value; a formalization in which the supremum over $\mathcal F$ or the box infimum could be vacuous is excluded.
• The definitions (boxes, $\mathcal P_n$, the kernel, the estimator, $J_n$, $d$) live in one definition file. $\mathcal P_n$ duplicates, with weights $1/n$, the distribution set of mission I; the duplication is deliberate because draft missions cannot import each other.
• Welcome contributions: the kernel density estimator and its strong $L^1$ consistency as reusable infrastructure, and any of the deterministic milestones.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• L. Devroye, The equivalence of weak, strong and complete convergence in $L_1$ for kernel density estimates, Annals of Statistics 11(3):896–904, 1983.
• L. Devroye, L. Györfi, Nonparametric Density Estimation: The $L_1$ View, Wiley, 1985.
• A. J. King, R. J.-B. Wets, Epi-consistency of convex stochastic programs, Stochastics and Stochastic Reports 34(1), 1991 (reference [22] of the paper).