Optimization

Motivation

In shoppertainment live streaming a single streamer sells products from many manufacturers during live sessions that mix product presentation with entertainment. Some of the most successful streamers spend much of their air time on content unrelated to the products; the paper cites Dong Yuhui, who devotes his sessions to English lessons. Traditional TV shopping (QVC) does the opposite and spends all air time on product features. This raises a question for operations and marketing: how should a streamer split a session's limited bandwidth between entertainment and product information?

Gu, Zhao and Wu (Management Science, 2024) answer it in a three-stage game between a streamer, a pool of manufacturers and a population of consumers. Entertainment attracts consumers directly, but it also leaves them less certain whether a product fits, and that uncertainty changes how manufacturers price. The paper's headline result, Proposition 3, says that zero entertainment is never optimal. This mission formalizes Proposition 3 together with the chain of lemmas and propositions of Section 4 on which it rests.

Setting

A product has quality $q \in [0,1]$, the probability that it fits a consumer. A good fit is worth $v > 0$ and a bad fit $0$. The qualities of the contracted manufacturers are uniform on $[\underline q, 1]$, where $\underline q \in [0,1)$ is the streamer's quality threshold; write $dF(q) = dq/(1-\underline q)$. The streamer keeps a commission rate $\alpha \in (0,1)$ of sales revenue.

The streamer chooses an entertainment bandwidth $t_e \in [0,1]$, the share of a session spent on entertainment. Each attending consumer receives a fit signal whose accuracy is $1 - t_e$. After a good signal the posterior fit probability is $1 - t_e + t_e q$, after a bad one it is $t_e q$. The two willingness-to-pay levels are therefore

$$p_H = (1 - t_e + t_e q)\,v, \qquad p_L = t_e q v .$$

With $T$ attending consumers, the demand at price $p$ is $T$ if $p \le p_L$ (everyone buys), $qT$ if $p_L < p \le p_H$ (only good-signal consumers buy), and $0$ above $p_H$. A manufacturer earns $(1-\alpha)\,p\,D(p)$.

Write $\hat t_e = 1/(2-\underline q)$ and $\hat q = 2 - 1/t_e$. In equilibrium a manufacturer of quality $q$ prices low ($p_L$) exactly when $t_e > 1/(2-q)$, that is, when $q < \hat q$. A consumer's expected shopping surplus $Eu_p(t_e)$ is the average, over manufacturers, of what the consumer gains at the equilibrium price. Attending costs are uniform on $[0,K]$, and the streamer's entertaining capability $v_e \ge 0$ gives the entertainment utility $v_e t_e$, so the attending traffic is

$$T(t_e) = \frac{v_e t_e + Eu_p(t_e)}{K}.$$

The individual profitability $\pi(t_e)$ is the streamer's expected commission from one attending consumer, and the streamer's payoff is $\Pi(t_e) = T(t_e)\,\pi(t_e)$.

Formalization targets

Goal: Proposition 3 (p. 33)

For $0 < \alpha < 1$, $v > 0$, $K > 0$, $0 \le \underline q < 1$ and $v_e \ge 0$:

1. $t_e = 0$ is not a maximizer of $\Pi$ on $[0,1]$, and $\Pi$ attains its maximum on $[0,1]$;
2. if $v_e \le v(1+\underline q)/4$, every maximizer $t^*_e$ of $\Pi$ satisfies $t^*_e \ge t^T_e$ for every maximizer $t^T_e$ of $T$;
3. if $v_e > v(1+\underline q)/4$, then

$$\Pi(t_e) < \Pi(1) \qquad \text{for all } t_e \in [0,1).$$

Milestones

• Lemma 2 (p. 24): a manufacturer of quality $q > 0$ maximizes profit at $p_L$ (uniquely) when $t_e > 1/(2-q)$ and at $p_H$ when $t_e \le 1/(2-q)$.
• Proposition 1 (p. 25): the proportion of low-pricing manufacturers is $\psi(t_e) = (\hat q - \underline q)/(1-\underline q)$ for $t_e > \hat t_e$ and $0$ otherwise; it increases in $t_e$ and decreases in $\underline q$.
• Lemma 3 (p. 27): $Eu_p = \int_{\underline q}^{\hat q}(1-t_e)\,q v\,dF(q)$ for $t_e > \hat t_e$, and $0$ otherwise.
• Display (14) (p. 31): $\pi(t_e) = \alpha\big(\int_{\underline q}^{\hat q} p_L\,dF + \int_{\hat q}^1 p_H q\,dF\big)$ for $t_e > \hat t_e$, and $\alpha \int_{\underline q}^1 p_H q\,dF$ otherwise.
• Proposition 2 (p. 27): $T$ is strictly increasing on $[0,1]$ if $v_e > v(1+\underline q)/2$; otherwise it strictly increases up to a peak $t^T_e \in [\hat t_e, 1]$ and strictly decreases after it.
• Lemma 4 (p. 32): $\pi$ strictly decreases and then strictly increases on $[0,1]$, is maximal at both $t_e = 0$ and $t_e = 1$, and is strictly increasing in $\underline q$.

Significance

Proposition 3 is the paper's managerial conclusion. Spending all bandwidth on product information, as TV shopping does, is never optimal. A streamer should allocate at least the traffic-maximizing share to entertainment, and should go to full entertainment once its entertaining capability exceeds $v(1+\underline q)/4$. Corollary 2 and the extensions of Section 5 of the paper (informing capability, in-session adjustment, competing streamers) build on this result and on the Section 4 chain.

The results are proved in the paper and its Online Supplementary, and none is machine-checked. The supplement's argument for the regime $v_e > v(1+\underline q)/4$ shows only that $d\Pi/dt_e > 0$ at $t_e = 1$, a local statement. The goal here asks for the global claim that $t_e = 1$ is the unique maximizer, so a complete formalization closes a gap in the published argument. The milestones make the paper's equilibrium derivation (manufacturer pricing, consumer surplus, traffic, profitability) checkable step by step.

Difficulty

Lemma 2, Proposition 1, Lemma 3 and display (14) are elementary: case analysis of a price and integrals of piecewise polynomials whose switch point $\hat q(t_e)$ depends on $t_e$. Proposition 2 and Lemma 4 need sign analysis of explicit rational functions of $t_e$ on $[\hat t_e, 1]$, uniformly in $\underline q \in [0,1)$. The traffic is not concave there: its surplus component is convex on part of the interval and concave on the rest.

The goal is the hard part. $\Pi = T\pi$ is the product of a function that rises and then falls (Proposition 2) and a function that falls and then rises (Lemma 4), so the shape of either factor does not settle where the product peaks. Comparing maximizers of $\Pi$ with maximizers of $T$, and ruling out an interior maximum of $\Pi$ above the threshold $v(1+\underline q)/4$ for every $\underline q$ and $v_e$, requires quantitative control of the product, not just the monotonicity pattern of its factors. Checking the sign of $d\Pi/dt_e$ at $t_e = 1$ alone is not enough.

Formalization scope

All parameters are real numbers and every function of the model is total; the statements carry the standing ranges as hypotheses. The bandwidth domain is Set.Icc 0 1, and "optimal" means IsMaxOn on that set. The single definitions file Shoppertainment.OptimalBandwidth.Model contains $p_H$, $p_L$, the demand (8) extended by $0$ above $p_H$, the manufacturer's profit, $\hat t_e$, $\hat q$, the equilibrium pricing rule, $\psi$ (as a Lebesgue measure), the consumer's ex-ante surplus, $Eu_p$, $T$, the revenue per attending consumer, $\pi$ and $\Pi$. $Eu_p$ and $\pi$ are integrals over the uniform law of quantities evaluated at each manufacturer's equilibrium price. They are not defined by the closed forms (12) and (14). This keeps Lemma 3 and (14) genuine statements and ties the goal to the manufacturers' equilibrium.

Conventions and pinned hypotheses:

• $\underline q < 1$, so that the uniform law on $[\underline q,1]$ exists (the paper allows $\underline q \le 1$).
• $\alpha < 1$, the standing range of p. 13.
• Lemma 2 pins $q > 0$ and $T > 0$. Without them every positive price earns $0$.
• Lemma 2 uses the manufacturer's own threshold $1/(2-q)$, as in the Online Supplementary A.2 and Figure 4(b). The printed display (10) reads $1/(2-\underline q)$, which would contradict Proposition 1.
• A tie $t_e = 1/(2-q)$ is priced high, as in (10). It is a null set for every integral.
• Proposition 2 assumes $v_e > 0$ (Table 1), and the goal assumes $v_e \ge 0$ (as printed in Proposition 3).
• The peaks $t^T_e$ and $t^*_e$ are stated as maximizers, never through the first-order conditions of the supplement.
• Proposition 1's decrease in $\underline q$ is strict for $t_e < 1$ and weak at $t_e = 1$, where $\psi \equiv 1$.

Two formalizations would trivialize the mission, and both are excluded. Without the existence clause, a "for every maximizer" statement could hold vacuously, so the goal asserts existence. Defining $Eu_p$ and $\pi$ by (12) and (14) would make two milestones true by definition.

Lemma 1, Corollaries 1–2, Remark 1 and the Section 5 extensions are not posed. A complete development needs only Mathlib's interval integrals, Lebesgue measure on $\mathbb R$ and elementary real analysis. Proofs of the closed forms of the Online Supplementary ($\Gamma$ in A.4, (A1) in A.6) are welcome as auxiliary lemmas.

Selected references

• Z. Gu, X. Zhao, D. J. Wu, A Model of Shoppertainment Live Streaming, Management Science, 2024; authors' accepted manuscript, October 2024. https://doi.org/10.1287/mnsc.2023.01724
• R. Lal, M. Sarvary, When and How Is the Internet Likely to Decrease Price Competition?, Marketing Science 18(4), 1999. https://doi.org/10.1287/mksc.18.4.485

Motivation

A Markov decision process (MDP) models sequential decisions under uncertainty: in each state a decision maker picks an action, collects a reward, and the system moves to a random next state according to a transition kernel. In applications the kernel is estimated from data, and an optimal policy for the estimated kernel can perform poorly under a slightly different one. Robust MDPs replace the single kernel by an uncertainty set and maximize the worst-case discounted reward over that set (Iyengar 2005; Nilim and El Ghaoui 2005; Wiesemann, Kuhn and Rustem 2013).

Goyal and Grand-Clément (arXiv:1811.00215v8) introduce r-rectangular uncertainty sets, in which transitions are mixtures of a small number of uncertain factors chosen independently by an adversary. Beyond the algorithmic results (the subject of the first mission of this series), they prove two structural properties of optimal robust policies in this model: a robust maximum principle and robust Blackwell optimality.

In a classical MDP, a policy is Blackwell optimal if it is optimal for every discount factor close enough to $1$ (Blackwell 1962; Puterman 1994, §10.1.2). Blackwell optimal policies are optimal for the long-run average reward and for every finer $n$-discount criterion, so they connect discounted and average-reward control. For two-player perfect-information zero-sum stochastic games the existence of Blackwell optimal strategies is due to Gaubert and Gunawardena (1998). Goyal and Grand-Clément establish the analogous statement for robust MDPs with r-rectangular uncertainty, under the assumption that the factor sets have finitely many extreme points, as polyhedral factor sets do.

Setting

Let $\mathbb S$ and $\mathbb A$ be finite sets of states and actions, with rewards $r_{sa}\ge0$, an initial distribution $p_0\in\Delta(\mathbb S)$, and a discount factor $\lambda\in(0,1)$. Fix coefficients $u^i_{sa}\ge0$, $i\in[r]$, with $\sum_i u^i_{sa}=1$. A factor matrix $W=(w_1,\dots,w_r)$ has probability vectors $w_i\in\Delta(\mathbb S)$ as columns and induces the kernel

$$P_{sas'}=\sum_{i=1}^r u^i_{sa}\,w_{i,s'} .$$

The adversary chooses $W$ from a nonempty convex compact set $\mathcal W$. Its projections are the factor sets $\mathcal W^1,\dots,\mathcal W^r$, and $\mathcal W$ is r-rectangular when $\mathcal W=\mathcal W^1\times\dots\times\mathcal W^r$.

A stationary policy $\pi\in\Pi$ picks $\pi_s\in\Delta(\mathbb A)$ in each state; it is deterministic when each $\pi_s$ is a point mass. With $r_\pi=(\sum_a\pi_{sa}r_{sa})_s$ and $L(\pi,W)_{ss'}=\sum_a\pi_{sa}P_{sas'}$, the value function and the expected reward are

$$v^{\pi,W}_\lambda=\sum_{t\ge0}\lambda^tL(\pi,W)^tr_\pi,\qquad R(\pi,W,\lambda)=p_0^\top v^{\pi,W}_\lambda .$$

The worst-case value of $\pi$ is $z_\lambda(\pi)=\min_{W\in\mathcal W}R(\pi,W,\lambda)$. A pair $(\pi^*,W^*)$ is an optimal solution of the robust MDP problem (1.2) at discount $\lambda$ when $\pi^*$ maximizes $z_\lambda$ over $\Pi$ and $W^*$ attains $\min_{W\in\mathcal W}R(\pi^*,W,\lambda)$. The Lean development uses this notation: value, R, z, IsRobustSolution, IsRRect, factorSet, IsDeterministic.

Formalization targets

Goal: robust Blackwell optimality (Proposition 6.2)

If $\mathcal W$ is r-rectangular and every factor set $\mathcal W^i$ has finitely many extreme points, there exist a deterministic policy $\pi^*$, a factor matrix $W^*\in\mathcal W$ and $\lambda_0\in(0,1)$ with

$$\forall\lambda\in(\lambda_0,1):\quad(\pi^*,W^*)\ \text{is an optimal solution of (1.2) at discount }\lambda .$$

The pair is fixed before $\lambda_0$ and does not depend on $\lambda$. The statement fixes no constant and no rate.

Milestones

1. Proposition 6.1.1: a minimizer $W^1$ of $R(\pi,\cdot,\lambda)$ is a worst case from every initial state, $v^{\pi,W^1}_{\lambda,s}\le v^{\pi,W^0}_{\lambda,s}$ for all $W^0\in\mathcal W$.
2. Proposition 6.1.2 (robust maximum principle): if $(\pi^*,W^*)$ solves (1.2), then $v^{\pi,W^1}_{\lambda,s}\le v^{\pi^*,W^*}_{\lambda,s}$ for every policy $\pi$, every minimizer $W^1$ of $R(\pi,\cdot,\lambda)$ and every state $s$.
3. Appendix G.1, p. 26: for each $\lambda$, (1.2) has an optimal solution $(\pi_\lambda,W_\lambda)$ with $\pi_\lambda$ deterministic and $W_\lambda$ an extreme point of $\mathcal W$.
4. Appendix G.1, p. 27: $v^{\pi,W}_t=(I-tL(\pi,W))^{-1}r_\pi$ on $(0,1)$, and each coordinate is a rational function of $t$ whose denominator has no zero in $(0,1)$.

Stronger: finitely many breakpoints (Proposition 6.3, optional)

Under the same hypotheses there are $0=\lambda_0<\lambda_1<\dots<\lambda_p=1$ and, for each $j$, a single deterministic pair $(\pi_j,W_j)$ optimal for every $\lambda\in(\lambda_j,\lambda_{j+1})$.

Significance

The result. Robust Blackwell optimality says that, for polyhedral r-rectangular uncertainty, a decision maker who is patient enough does not need to know the discount factor exactly: one deterministic policy is robust-optimal for all discounts near $1$, and the adversary has one matching worst-case factor matrix. This is the robust counterpart of the classical bridge from discounted to average-reward criteria, and it is the natural entry point for a theory of robust MDPs under the long-run average criterion, for which the paper notes no results were known. The robust maximum principle states that an optimal robust policy has the highest worst-case value from every starting state, a comparison that has been used to derive structural properties of robust policies in a healthcare setting (Grand-Clément et al. 2020, cited on p. 13 of the paper).

Formalizing it. The results are proved in the paper; none has a machine-checked proof. The nominal analogues (Blackwell 1962, Theorem 5, and the rationality of the discounted value) are posed on Prove2Me as open targets on a different, nominal model and are not reused here. The formalization also corrects two printed statements: Proposition 6.1 is false for an initial distribution with a zero entry and is posed with $p_0>0$, and the claim in Appendix G.1 that the factor matrix of a solution is an extreme point is posed in its existential form, the form the proof uses.

Difficulty

The obvious argument for the goal is a pigeonhole over the finitely many candidate pairs (deterministic policies and extreme factor matrices): some pair is optimal for discounts $\lambda_n\to1$. The step that fails is passing from this sequence to a whole interval. Optimality of a pair is not a comparison between two fixed rational functions of $\lambda$: the worst-case value $z_\lambda(\pi)$ is a minimum over $\mathcal W$, and optimality quantifies over all randomized policies. A comparison of worst-case values at one discount does not by itself give a comparison of value functions that can be propagated to other discounts. The paper bridges this gap with the robust maximum principle, which turns a worst-case comparison into a statewise comparison of two value functions, each rational in $\lambda$. The maximum principle itself rests on the saddle-point structure of r-rectangular robust MDPs (Theorem 4.2 and Lemma 4.3 of the paper), which a solver must develop.

Formalization scope

All objects live in the definition FactorRMDP.Blackwell.Model. States and actions are finite types, with $\mathbb A$ nonempty. Factors are indexed by Fin r, i.e. 0-based. A factor matrix is a function Fin r → S → ℝ. $\mathcal W$ is a nonempty convex compact set of factor matrices with stochastic factors. Its factor sets are its projections, and r-rectangularity is the predicate IsRRect, not built into the structure. Rewards are nonnegative and $p_0\in\Delta(\mathbb S)$. The value function is the discounted series, not a fixed point, so no Bellman identity holds by definition. Minima and maxima are stated with IsLeast/IsGreatest, and statements at a fixed discount assume $0<\lambda<1$. Optimality in (1.2) is over stationary randomized policies, as in the paper's proof, and requires both halves: $\pi^*$ maximizes $z_\lambda$ and $W^*$ attains $\min_W R(\pi^*,W,\lambda)$. "Finitely many extreme points" is Mathlib's Set.extremePoints of each factor set. The second sentence of Assumption 2.4 (an optimization oracle) is not formalized.

Explicit choices relative to the printed text:

• $\mathcal W$ nonempty, $\mathbb A$ nonempty and $\lambda\in(0,1)$ are stated explicitly.
• Proposition 6.1 (both parts) assumes $p_0(s)>0$ for every state. As printed, it is false when $p_0$ vanishes on a state.
• The extreme-point claim of Appendix G.1 is posed as the existence of an optimal pair with an extreme factor matrix.
• The goal (Proposition 6.2) keeps $p_0$ arbitrary.

A goal in which the pair $(\pi^*,W^*)$ may depend on $\lambda$ would only restate milestone 3 and is not robust Blackwell optimality; the pair is quantified before $\lambda_0$.

A complete development needs the saddle-point theory of r-rectangular robust MDPs (shared with the first mission of this series), Neumann series and Cramer's rule for $I-tL$, extreme points of products of compact convex sets, and the finiteness of zeros of a nonzero polynomial. The rationality of discounted values and the extreme-point lemmas are reusable for nominal Blackwell optimality and for other robust models. Proofs of any milestone, of the optional Proposition 6.3, and auxiliary lemmas are welcome.

Selected references

• V. Goyal and J. Grand-Clément, Robust Markov Decision Process: Beyond Rectangularity, arXiv:1811.00215v8, 2021; Mathematics of Operations Research, 2023. https://arxiv.org/abs/1811.00215, https://doi.org/10.1287/moor.2022.1259
• D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33, 1962. https://doi.org/10.1214/aoms/1177704593
• S. Gaubert and J. Gunawardena, A Non-Linear Hierarchy for Discrete Event Dynamical Systems, 1998 (as cited in Goyal and Grand-Clément, reference list, arXiv:1811.00215v8).
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30, 2005. https://doi.org/10.1287/moor.1040.0129
• A. Nilim and L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53, 2005. https://doi.org/10.1287/opre.1050.0216
• W. Wiesemann, D. Kuhn and B. Rustem, Robust Markov Decision Processes, Mathematics of Operations Research 38, 2013. https://doi.org/10.1287/moor.1120.0566
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Two-stage adjustable robust optimization models decisions taken in two steps around an uncertain demand: a first-stage decision is fixed now, the demand is revealed, and a second-stage (recourse) decision reacts to it. The objective is the worst-case total cost over a set of possible demands. The model covers set cover, capacity planning and network design under uncertain demand (Bertsimas, Goyal 2012; Gupta, Nagarajan, Ravi 2014). Computing the optimal adjustable solution is intractable in general: Feige, Jain, Mahdian and Mirrokni (2007) showed that, for the budget of uncertainty sets below, the problem cannot be approximated within a factor better than $\Omega(\log n/\log\log n)$ under a standard complexity assumption, where $n$ is the number of decision variables.

Affine policies, in which the recourse is restricted to an affine function of the revealed demand (Ben-Tal et al. 2004), are computable by a single linear program and perform well empirically. The question is how much they can lose in the worst case.

Timeline. Bertsimas and Goyal (2012) proved that affine policies are within $O(\sqrt m)$ of the adjustable optimum for general uncertainty sets ($m$ = number of uncertain parameters) and that this is tight for some sets. El Housni and Goyal (arXiv:1807.00163, 2018; Mathematics of Operations Research 2021) proved that for budget of uncertainty sets the factor is $O(\log n/\log\log n)$, matching the hardness bound. That result is the goal of this mission.

Setting

Let $A\in\mathbb R^{m\times n}$, a non-negative recourse matrix $B\in\mathbb R^{m\times n}_+$, costs $c,d\in\mathbb R^n_+$ and a polyhedral set $\mathcal X\subseteq\mathbb R^n$ be given. For an uncertainty set $\mathcal U\subseteq\mathbb R^m$ of right-hand sides, problem (1.1) is

$$z_{AR}(\mathcal U)=\min_{x\in\mathcal X}\ c^Tx+\max_{h\in\mathcal U}\ \min_{y(h)\ge0}\big\{d^Ty(h)\ :\ Ax+By(h)\ge h\big\}.$$

A first-stage $x$ and a recourse rule $y(\cdot)$ form a feasible solution when $x\in\mathcal X$ and $y(h)\ge0$, $Ax+By(h)\ge h$ for every $h\in\mathcal U$. The affine problem (2.1) restricts the rule to $y(h)=Ph+q$ with $P\in\mathbb R^{n\times m}$, $q\in\mathbb R^n$ (still requiring $Ph+q\ge0$ on $\mathcal U$); its value is $z_{Aff}(\mathcal U)\ge z_{AR}(\mathcal U)$.

The budget of uncertainty set (1.2) with weights $w_i\in[0,1]$ is

$$\mathcal U=\Big\{h\in[0,1]^m\ :\ \sum_{i=1}^mw_ih_i\le1\Big\}.$$

The fractional covering value (3.2) of a requirement $h$ is $z(h)=\min_{y\ge0}\{d^Ty: By\ge h\}$, and $z(\mathcal W)=z(\mathbb 1(\mathcal W))$ for $\mathcal W\subseteq[m]$. Throughout, $\log$ is the natural logarithm and $\beta=4\log n/\log\log n$.

Formalization targets

Goal: Theorem 3.1

$$z_{Aff}(\mathcal U)=O\Big(\frac{\log n}{\log\log n}\Big)\cdot z_{AR}(\mathcal U)$$

for every instance with $\mathcal U$ a budget of uncertainty set: there are $C>0$ and $N$ such that $z_{Aff}\le C\frac{\log n}{\log\log n}z_{AR}$ for all $n\ge N$, all $m$ and all data. The constant is left unfixed, so the goal survives any improvement of the constant.

Milestones (the paper's proof, in order)

1. Lemma 3.1 — the explicit affine solution (3.5), a linear part $y_{Lin}(h)=\sum_{i\in\mathcal I}\alpha_ih_iv_i$ plus a static part from (3.4), is feasible.
2. Lemma 3.2 — the linear part costs at most $\beta\cdot\mathrm{OPT}$ for every $h\in\mathcal U$.
3. Lemmas B.1, B.2 — two Chernoff bounds for weighted sums of independent Bernoulli variables.
4. Claims 3.1–3.3 — rescaling of the covering problem, and two probability bounds for a randomized rounding of a dual (packing) solution.
5. Lemma 3.3 (structural result) — if covering each single row $i\in\mathcal J$ costs more than $4\gamma\frac{\log n}{\log\log n}w_i$, while every scenario $\mathcal W\subseteq\mathcal J$ with $\sum_{\mathcal W}w_i\le1$ costs at most $\gamma$, then $z(\mathcal J)\le4\gamma\frac{\log n}{\log\log n}$.
6. Lemma 3.4 — the static part costs $O(\beta)\cdot\mathrm{OPT}$.

Significance

The result. The bound shows that affine policies are an optimal approximation for this class, up to a constant factor: no polynomial-time algorithm can beat them by more than a constant in the worst case (under the hardness assumption). It improves the earlier $O(\sqrt m)$ bound for budget sets exponentially, and it is the base case from which the paper derives bounds for intersections of budget constraints (Sections 4–5). Lemma 3.3 is a statement about fractional covering problems alone; it generalizes a set-cover result of Gupta, Nagarajan and Ravi (2014) to arbitrary non-negative matrices and weights, and improves its bound from $O(\log n)$ to $O(\log n/\log\log n)$.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of the structural lemma is known. A formal development would also settle the paper's slips: Claim 3.2's $1-O(1/n)$ does not follow from its proof (stated here in the explicit form the proof gives), Lemma B.2's strict inequality fails when $\mu=0$, and Lemma 3.3 needs $n$ large.

Difficulty

Feasibility and the cost of the linear part follow directly from the construction. The difficulty is the static part, that is, Lemma 3.3. The obvious argument covers $\mathcal J$ by a union of cheap scenarios, and it fails: each scenario covers rows of total weight at most $1$, there can be many disjoint scenarios, and adding up their costs gives a bound proportional to $\sum_{i\in\mathcal J}w_i$, which may be as large as $m$. The lemma asserts a bound that depends on $n$ alone, at the rate $\log n/\log\log n$ of the hardness result. Any argument therefore has to exploit condition 1 (every single row is expensive) together with condition 2 across all $2^{|\mathcal J|}$ scenarios at once. As printed, the lemma holds only for $n$ large; for $n=2$ it is false.

Formalization scope

• Data. Vectors are functions on Fin m, Fin n with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ; Lean index $i$ is the paper's $i+1$. First stage and recourse share the same dimension $n$, as on p. 1.
• Values. $z_{AR}$, $z_{Aff}$, $z(h)$ and the static value $z_{Sta}$ are infima in the extended reals, $+\infty$ when infeasible. The recourse is a function of $h$, which gives the same value as the paper's inner minimum. A formalization with real infima (equal to $0$ on infeasible problems) or without $Ph+q\ge0$ would trivialize the goal and is excluded.
• Standing assumptions of p. 1: $B\ge0$, $c,d\ge0$, $\mathcal X$ polyhedral, $w_i\in[0,1]$. The assumption "$\mathcal U\subseteq[0,1]^m$ compact convex with $e_i\in\mathcal U$" holds for the budget set and is not added.
• Added hypotheses and corrections. (i) $c^Tx\ge0$ for $x\in\mathcal X$: Theorem 3.1 is false without it, and it holds whenever $\mathcal X\subseteq\mathbb R^n_+$. (ii) $n\ge3$ where $\beta>0$ is needed, and a threshold $N_0$ in Lemma 3.3. (iii) Lemma B.2 in non-strict form. (iv) Claim 3.2 with the explicit bound $1-n\,e^\delta/(1+\delta)^{1+\delta}$, $\delta=\eta/2-2$. (v) Covering solutions $v_i$ are required only for $i\in\mathcal I$.
• Quantifiers. In the goal and in Lemmas 3.3, 3.4 the constants $C$, $N$, $N_0$ are chosen before $m$ and the instance; a constant allowed to depend on the instance would make the goal trivial.
• Randomness is finite: independent Bernoulli selection with probabilities and expectations as finite sums, reusing the published definition SpectralSparsify.Sampling.BernoulliSubset. No measure theory is needed.
• Infrastructure. LP strong duality (LinearOptimization.lp_strong_duality, proved on the platform) is a tool for Lemma 3.3. The Chernoff bounds and the structural lemma are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 3.3, are welcome.

The source is arXiv:1807.00163v2; its printed page numbers equal the PDF page numbers.

Selected references

• O. El Housni, V. Goyal, On the Optimality of Affine Policies for Budgeted Uncertainty Sets, arXiv:1807.00163v2, 2019; Mathematics of Operations Research 46(2), 2021. https://arxiv.org/abs/1807.00163
• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134(2), 2012. https://doi.org/10.1007/s10107-011-0444-4
• U. Feige, K. Jain, M. Mahdian, V. Mirrokni, Robust combinatorial optimization with exponential scenarios, IPCO 2007, LNCS 4513 (cited as [19] in the source).
• A. Gupta, V. Nagarajan, R. Ravi, Thresholded covering algorithms for robust and max–min optimization, Mathematical Programming 146(1–2), 2014 (cited as [21] in the source).
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99(2), 2004. https://doi.org/10.1007/s10107-003-0454-y
• P. Raghavan, Probabilistic construction of deterministic algorithms: approximating packing integer programs, FOCS 1986 (cited as [26] in the source).

Motivation

Food, blood and pharmaceuticals are perishable: a unit not sold within its lifetime is thrown away. A seller decides each period how much to order, which price to charge, and whether to dispose of stock early. A large stock of old units argues for a lower price and a smaller order.

Optimal policies for fixed-lifetime inventory are hard to characterize: the state is a vector of inventory levels by remaining lifetime (Fries 1975; Nahmias 1982), and later work turned largely to heuristics.

Chen, Pang and Pan (Oper. Res. 62(2), 2014) obtained structural results for the joint ordering, pricing and disposal problem with a positive replenishment lead time. They used L♮-concavity, a notion from discrete convex analysis (Murota 2003) that Zipkin (2008) used to analyze lost-sales inventory systems with lead times. This mission formalizes the paper's result for the case where unmet demand is backlogged.

Setting

A product with a lifetime of exactly $l \ge 2$ periods is reviewed periodically over a finite horizon of $T$ periods. Orders arrive after a lead time of $k$ periods, $0 \le k < l$. Write $L = l - 1$.

Vectors and L♮-convexity. For vectors $u, v \in \mathbb{R}^n$, $u \wedge v$ and $u \vee v$ are the componentwise minimum and maximum, and $e$ is the all-ones vector. A set $\mathcal{V}$ is L♮-convex if $(u + \alpha e) \wedge v$ and $u \vee (v - \alpha e)$ lie in $\mathcal{V}$ for all $u, v \in \mathcal{V}$ and $\alpha \ge 0$. A function $f$ is L♮-convex on $\mathcal{V}$ if moreover

$$f(u) + f(v) \ge f\big((u + \alpha e) \wedge v\big) + f\big(u \vee (v - \alpha e)\big),$$

and L♮-concave if $-f$ is L♮-convex. The ordered sets are $\mathcal{V}_{n,k} = \{s \in \mathbb{R}^n : s_1 \le \dots \le s_k\}$.

Data. The unit costs are $c$ (ordering), $h^+$ (holding), $h^-$ (backlogging) and $\theta$ (disposal), all nonnegative, and $\gamma \in [0, 1]$ is the discount factor. The seller chooses the expected demand $d \in \mathcal{D} = [\underline d, \bar d]$ in place of the price. The price is $P(d)$, strictly decreasing, and the expected revenue $P(d)d$ is continuous and concave on $\mathcal{D}$. The realized demand is $d_t = d + \varepsilon_t$, where the noise terms are i.i.d. with mean zero and support in $[A, B]$, $A \le 0 \le B$, and $\underline d + A \ge 0$.

State and decisions. The state $s = (s_1, \dots, s_{l-1})$ satisfies $s_1 \le \dots \le s_{l-1}$, so the state space is $\mathcal{S} = \mathcal{V}_{l-1,l-1}$. The coordinate $s_i$ is the inventory, net of backorders, with residual lifetime at most $i$, including orders in transit. Each period the seller chooses:

• an order-up-to level $s_l \ge s_{l-1}$;
• a demand level $d \in \mathcal{D}$;
• after demand is realized, a depletion $a$ with $s_1 \vee d_t \le a \le s_{l-k} \vee d_t$, so $a - d_t$ units are disposed of.

The next state is $\tilde s = (s_2 - a, \dots, s_l - a)$.

Recursion. The modified profit-to-go satisfies $f_{T+1} = 0$ and

$$f_t(s) = \max_{s_l \ge s_{l-1},\ d \in \mathcal{D}} \Big\{ P(d)d + \mathbb{E}\big[g_t(s, s_l, d \mid \varepsilon_t)\big] \Big\}, \qquad g_t = \max_{s_1 \vee d_t \le a \le s_{l-k} \vee d_t} \phi_t,$$ $$\phi_t(s, s_l, d, a \mid \varepsilon_t) = \gamma c\,\tilde s_{l-1} - c s_l - \theta(a - d_t) - h^+(s_{l-k} - a)^+ - h^-(a - s_{l-k})^+ + \gamma f_{t+1}(\tilde s).$$

In §4 the paper also assumes $c \le h^-/(1 - \gamma)$.

Formalization targets

Goal: Theorem 1 (p. 291)

For $t = 1, \dots, T+1$, $f_t$, $g_t$ and $\phi_t$ are L♮-concave in $s$, $(s, s_l, d)$ and $(s, s_l, d, a)$. The largest optimal order-up-to level $s_{lt}(s)$ and demand level $d_t(s)$ are nondecreasing in $s$, the optimal price is nonincreasing, and

$$s_{lt}(s + \omega e) \le s_{lt}(s) + \omega, \qquad d_t(s + \omega e) \le d_t(s) + \omega \qquad (\omega \ge 0).$$

The largest optimal depletion $a_t(s, s_l, d \mid \varepsilon)$ is nondecreasing, and $a_t(s + \omega e, s_l + \omega, d + \omega \mid \varepsilon) \le a_t(s, s_l, d \mid \varepsilon) + \omega$.

Milestones

• The ordered sets $\mathcal{V}_{n,k}$, $\mathcal{V}^+_{n,k}$ are L♮-convex (p. 287).
• Lemma 1: $g(x, \xi) = f(x - \xi e)$ is L♮-convex when $f$ is (p. 287).
• Lemma 2: partial minimization over an L♮-convex set preserves L♮-convexity (p. 287).
• The set $\{a \ge s_1 \vee d_t\}$ is L♮-convex (p. 291).
• The bound $f_{t+1}(\tilde s') - f_{t+1}(\tilde s) \le (\theta + c)\delta$ for the next states generated by $a' > a \ge s_{l-k}\vee d_t$ (p. 291).
• (9): $\phi_t$ is nonincreasing in $a$ beyond $s_{l-k} \vee d_t$, so the upper bound on $a$ can be dropped (p. 291).
• Lemma 3: the largest minimizer of an L♮-convex function is monotone, with $\xi(x + \omega e) \le \xi(x) + \omega$ (p. 287).
• The first sentence of Theorem 1, the L♮-concavity of $f_t$, $g_t$, $\phi_t$.
• Corollary 1: monotone sensitivity of the order quantity and the demand level in each age class (p. 292).
• Proposition 1: if $\theta \ge h^+/(1-\gamma)$, depleting only $d_t \vee s_1$ is optimal (p. 292).

Significance

The result. Theorem 1 gives a qualitative description of the optimal policy in a model where no closed form is available. Fresher inventory leads to ordering less and charging more. One more unit of inventory of any age raises the order-up-to level and the demand level by at most one unit. Corollary 1 refines this by age: the order quantity is most sensitive to young inventory, and the price discount is most sensitive to inventory close to expiry. These properties underlie the bounds and heuristics of §6 of the paper.

The formalization. The result is proved in the paper, but parts of the argument are informal: the $(\theta + c)\delta$ bound is a coupling argument, existence of optimal solutions is "straightforward to check and thus omitted", and Lemmas 1–3 are stated without proof. A formalization makes the induction checkable and yields a reusable library of L♮-convexity on real vectors with domains, used by the wider family of inventory models built on the same technique. None of these results is known to be machine-checked.

Difficulty

The obvious induction, that each step of the recursion preserves L♮-concavity, fails at the depletion problem (5): its constraint set is not L♮-convex, because of the upper bound $a \le s_{l-k} \vee d_t$, so Lemma 2 does not apply. The bound must first be shown inactive, which needs a quantitative estimate of how the profit-to-go changes when backorders are added, a property of the value function itself.

Lemma 3 handles a scalar decision, while Theorem 1 has a pair $(s_l, d)$ and needs the componentwise-largest maximizer; every supremum and expectation must also be shown to be finite.

Formalization scope

• Carrier. The paper treats $\mathbb{F} \in \{\mathbb{R}, \mathbb{Z}\}$ at once. The mission formalizes the real case only.

• L♮-convexity. Functions are real-valued on an explicit domain set, which is the paper's own convention for "L♮-convex on a set". The submodularity characterization is not used as the definition.

• Indexing. States are Fin L → ℝ with $L = l - 1 \ge 1$, indexed from 0, and the lead time satisfies $k \le L$. The paper's $s_{l-k}$ is coordinate $L - k$ of $(s_1, \dots, s_l)$: at $k = 0$ it is the decision $s_l$, and at $k = L$ it is $s_1$.

• Time. Time is counted in periods to go, which is faithful because the data are stationary. f 0 = 0 is $f_{T+1}$. The parts of Theorem 1 about $g_t$, $\phi_t$ and decisions cover the decision periods $t \le T$.

• Suprema and expectations. Every maximum is sSup of the image of a nonempty feasible set that is bounded above. Expectations are Bochner integrals against the noise law $\mu$.

• Optimal decisions. Largest optimal decisions are hypotheses at the points compared; at $\gamma = 1$, $k \ge 1$ no largest order-up-to level exists in the last period.

• Standing assumptions. All the §3 assumptions (nonnegative costs, $\gamma \in [0,1]$, strictly decreasing $P$, continuous concave revenue, zero-mean noise with support in $[A, B]$, $\underline d + A \ge 0$) are fields of the model structure. The §4 assumption $c \le h^-/(1-\gamma)$ is a hypothesis $(1-\gamma)c \le h^-$ of every §4 statement.

• Corrected slips.

  • The paper sets $f_t = +\infty$ off $\mathcal{S}$, a slip for $-\infty$. The Lean evaluates $f_t$ on $\mathcal{S}$ only.
  • In Lemma 3, "$\xi(x) + \omega \in \mathrm{dom}(f)$" reads $x + \omega e \in \mathrm{dom}(f)$.
  • The final "$< 0$" of (9) is stated as "$\le 0$". It is an equality when $h^- = 0$ and either $\gamma = 1$ or $\theta = 0$.
  • Proposition 1 needs $\gamma < 1$ for its quotient, and it asserts that $d_t \vee s_1$ is optimal, not that it is unique.

• Ruled-out formalizations. Any of the following would trivialize the mission:

  • defining $f_t$ as an arbitrary L♮-concave function, or taking the continuation in $\phi_t$ as a hypothesis-bound function;
  • dropping the upper bound $a \le s_{l-k} \vee d_t$ from the depletion interval;
  • restricting to $l = 2$.

  The value functions here are the model's own recursion, for every $l \ge 2$.

• What is needed. L♮-convexity on $\mathbb{R}^n$ with domains (shifts, sums, expectations, partial maximization, comparative statics for largest maximizers) and integrability of $g_t$ in the noise; all reusable. Proofs of single milestones are welcome.

• Source. The source is the published Operations Research article; in the copy held, printed page = PDF page + 282.

Selected references

• X. Chen, Z. Pang, L. Pan, Coordinating Inventory Control and Pricing Strategies for Perishable Products, Operations Research 62(2):284–300, 2014. https://doi.org/10.1287/opre.2014.1261
• P. Zipkin, On the Structure of Lost-Sales Inventory Models, Operations Research 56(4):937–944, 2008. https://doi.org/10.1287/opre.1070.0482
• K. Murota, Discrete Convex Analysis, SIAM Monographs on Discrete Mathematics and Applications, 2003. https://doi.org/10.1137/1.9780898718508
• B. Fries, Optimal Ordering Policy for a Perishable Commodity with Fixed Lifetime, Operations Research 23(1):46–61, 1975. https://doi.org/10.1287/opre.23.1.46
• S. Nahmias, Perishable Inventory Theory: A Review, Operations Research 30(4):680–708, 1982. https://doi.org/10.1287/opre.30.4.680

Motivation

A Markov decision process (MDP) is optimized for a transition kernel that, in practice, is estimated from data, and the optimal policy for the estimated kernel can perform poorly under small perturbations of it. The robust MDP approach replaces the single kernel by an uncertainty set of kernels and asks for the policy with the best worst-case expected reward. It goes back to Satia and Lave (1973).

Whether a robust MDP is tractable depends on the shape of the uncertainty set.

• 2005. Iyengar and Nilim and El Ghaoui treat (s,a)-rectangular sets, in which every row $P_{sa}$ is chosen independently. An optimal robust policy is stationary and deterministic, and robust value iteration computes it.
• 2013. Wiesemann, Kuhn and Rustem treat s-rectangular sets. Optimal robust policies are stationary but may need randomization. For general uncertainty sets, computing an optimal robust policy is strongly NP-hard.
• 2018. Goh et al. introduce factor-based uncertainty for a medical cost-effectiveness application and evaluate the worst case of a fixed policy.
• 2021–2023. Goyal and Grand-Clément compute optimal robust policies for factor uncertainty with independent factors. This mission formalizes that result.

Rectangular sets let the adversary choose the transitions out of different states independently, which is conservative when all transitions depend on a few common factors, such as a patient's physiology across health states. Factor uncertainty couples the states, and it is the first coupled model in which an optimal robust policy can still be computed.

Setting

There are finite sets of states $\mathbb S$ and actions $\mathbb A$, with $S = |\mathbb S|$ and $A=|\mathbb A|$. The rewards satisfy $r_{sa}\ge 0$, $p_0$ is an initial distribution on $\mathbb S$, and $\lambda\in(0,1)$ is the discount factor. Fix $r$ factors indexed by $[r]$ and coefficients $u^i_{sa}\ge0$ with $\sum_i u^i_{sa}=1$. A factor matrix $W=(w_1,\dots,w_r)$ has probability vectors $w_i$ on $\mathbb S$ as columns, and it induces the kernel

$$P_{sas'}=\sum_{i=1}^r u^i_{sa}\,w_{i,s'} .$$

The uncertainty set is a nonempty convex compact set $\mathcal W$ of factor matrices. It is r-rectangular if $\mathcal W=\mathcal W^1\times\cdots\times\mathcal W^r$, so that each factor is chosen independently of the others.

A stationary policy $\pi\in\Pi$ gives a distribution $\pi_s$ on $\mathbb A$ at each state. It is deterministic if each $\pi_s$ is a point mass. Write $r_\pi=(\sum_a\pi_{sa}r_{sa})_s$ and $T_\pi=(\sum_a \pi_{sa}u^i_{sa})_{s,i}$. The decision maker's value function and the expected discounted reward are

$$v^{\pi,W}=\sum_{t\ge0}\lambda^t (T_\pi W^\top)^t r_\pi, \qquad R(\pi,W)=p_0^\top v^{\pi,W}.$$

The policy evaluation problem computes $z(\pi)=\min_{W\in\mathcal W}R(\pi,W)$. The policy improvement problem computes $z^*=\max_{\pi\in\Pi}z(\pi)$. Let

$$F(v)_s=\max_{a\in\mathbb A}\Big\{r_{sa}+\lambda\sum_{i=1}^r u^i_{sa}\min_{w_i\in\mathcal W^i}w_i^\top v\Big\}.$$

Algorithm VI-PI is the iteration $v^0=0$, $v^{k+1}=F(v^k)$.

Formalization targets

Goal: Theorem 5.1, by its mathematical content

Assume $\mathcal W$ is r-rectangular. Then $F$ has a unique fixed point $v^*$, and

$$z^*=\max_{\pi\in\Pi}\min_{W\in\mathcal W}R(\pi,W)=p_0^\top v^*,\qquad v^k\to v^* .$$

Write $\theta(\varepsilon)=\varepsilon(1-\lambda)(2\lambda)^{-1}$. If $\|v^{k+1}-v^k\|_\infty<\theta(\varepsilon)$, then $\|v^{k+1}-v^*\|_\infty\le\varepsilon$, and the deterministic policy that VI-PI computes at that iteration is $\varepsilon$-optimal. The test is passed as soon as $\lambda^k\max r<\theta(\varepsilon)$.

Milestones

The milestones follow the paper's route to the goal.

1. The adversary's Bellman recursion (Proposition 3.1).
2. The identity $W^\top v^{\pi,W}=\beta^{\pi,W}$ (Lemma 4.3).
3. The resolvent and linear-programming forms of $z(\pi)$ (Lemmas A.2, A.3).
4. The monotone contraction $\varphi(\pi,\cdot)$ (Appendix A).
5. The reformulation of $z(\pi)$ with constraints $\beta_i\le\min_{w_i}w_i^\top(r_\pi+\lambda T_\pi\beta)$ (Lemma 3.3).
6. The existence of a deterministic optimal robust policy (Lemma 4.1).
7. The saddle point and the min-max duality (Theorem 4.2):

$$\max_{\pi\in\Pi}\min_{W\in\mathcal W}R(\pi,W)=\min_{W\in\mathcal W}\max_{\pi\in\Pi}R(\pi,W).$$

8. The monotone contraction $F$ (Lemma E.1).
9. The fixed-point equation (5.1).

Theorem 3.2, the policy-evaluation analogue of the goal (Algorithm VI-PE), is included as a further item.

Significance

The theorem shows that factor uncertainty, in which transitions out of different states are coupled, is as tractable as (s,a)-rectangular uncertainty, provided the factors are independent. An optimal robust policy exists among deterministic stationary policies, the robust and nominal problems share a saddle point, and value iteration on a $\lambda$-contraction computes the robust value. The structure is also what the companion mission builds on: the robust maximum principle and robust Blackwell optimality are derived from (5.1) and Theorem 4.2.

The results are proved in the paper. None of them is formalized: no factor-matrix robust MDP exists in Lean. The platform's robust-MDP items for (s,a)-rectangular sets (Nilim–El Ghaoui, Iyengar) and s-rectangular sets (Wiesemann et al.) are other uncertainty models and do not specialize to this one. A formal proof would also check a printed statement, since one clause of Theorem 4.2 needs correcting (see below).

Difficulty

The obvious argument writes a robust Bellman equation state by state and appeals to the contraction principle. Here that argument fails. Under factor uncertainty the adversary cannot choose the transitions out of each state separately, because one factor $w_i$ enters every row $P_{sa}$ with $u^i_{sa}>0$. Minimizing state by state therefore yields kernels that need not come from a single feasible $W$. The decision maker's equation for $v$ does not close on its own.

The step that requires care links two dynamic programs, the decision maker's over $\mathbb S$ and the adversary's over $[r]$, and shows that factor-wise minimization is feasible. That is where r-rectangularity enters. The paper's Appendix A gives an instance in which the factor-wise minimizers are infeasible once a constraint couples the factors.

Formalization scope

• States and actions are arbitrary finite types. $\mathbb A$ is nonempty, and $\mathbb S$ is nonempty because $p_0$ is a distribution. Factors are indexed by Fin r (0-based).
• $\mathcal W$ is a set of maps Fin r → S → ℝ whose values are probability vectors. It is nonempty, convex and compact. Nonemptiness is implicit in the paper and explicit here. $\mathcal W^i$ is the projection of $\mathcal W$, and r-rectangularity is a hypothesis (IsRRect). Proposition 3.1, Lemmas 4.3, A.2 and A.3, and both contraction statements are stated without it. Lemma 3.3 is stated with it, since it is false without it.
• Rewards are nonnegative, as on p. 1. The discount satisfies $0<\lambda<1$ in every statement.
• $v^{\pi,W}$ and the adversary's value $\beta^{\pi,W}$ are discounted sums, never solutions of a Bellman equation by definition. Defining them as fixed points would make Proposition 3.1, Lemma 4.3 and (5.1) true by definition.
• Every min and max is attained. Statements use IsLeast/IsGreatest, and Lemma A.2 states the invertibility of $I-\lambda W^\top T_\pi$, because Lean's matrix inverse is $0$ on singular matrices.
• $F$ is stated with a maximum over actions. The paper (p. 10) says this is equivalent to its maximum over $\pi_s\in\Delta$. Lemma E.1 and the contraction of $\varphi$ are stated on all of $\mathbb R^S$ and $\mathbb R^r$.
• Not formalized: the count of arithmetic operations in Theorems 3.2 and 5.1, and the $\varepsilon$-optimization oracle of Assumption 2.4 that it counts. The iteration count is stated explicitly instead.
• Corrections. The paper states (4.6) for every robust solution $(\pi^*,W^*)$ with $\pi^*$ deterministic. That claim is false: a two-state instance has every policy robust-optimal, yet one robust solution is not nominally optimal against its own $W^*$. Theorem 4.2 and (5.1) are stated in existence form, which is the form the proof of Theorem 5.1 uses.
• A goal that kept only the convergence $v^k\to v^*$ would be a different and weaker theorem. The goal also requires $z^*=p_0^\top v^*$, the stopping rule, and the $\varepsilon$-optimality of the computed deterministic policy.

Reusable infrastructure includes the discounted value of a stationary policy for a stochastic matrix, monotone sup-norm contractions with the standard stopping rule, and minimization of linear forms over compact sets. Contributions to any of these are welcome.

Selected references

• V. Goyal, J. Grand-Clément, Robust Markov Decision Processes: Beyond Rectangularity, Mathematics of Operations Research, 2023; preprint arXiv:1811.00215v8, 2021 (the version formalized). https://arxiv.org/abs/1811.00215 · https://doi.org/10.1287/moor.2022.1259
• A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition probabilities, Operations Research 53(5), 2005. https://doi.org/10.1287/opre.1050.0216
• G. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. https://doi.org/10.1287/moor.1040.0129
• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov decision processes, Mathematics of Operations Research 38(1), 2013. https://doi.org/10.1287/moor.1120.0566
• J. Goh, M. Bayati, S. A. Zenios, S. Singh, D. Moore, Data uncertainty in Markov chains: application to cost-effectiveness analyses of medical innovations, Operations Research 66(3), 2018. https://doi.org/10.1287/opre.2017.1685
• J. K. Satia, R. L. Lave, Markov decision processes with uncertain transition probabilities, Operations Research 21(3), 1973. https://doi.org/10.1287/opre.21.3.728
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994.

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 2.1 for $\delta>0$

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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