All missions

Motivation

Expected utility theory explains a single attitude toward risk by the curvature of a utility function of final wealth: a concave utility makes a decision maker risk averse, a convex one risk seeking. Several well documented patterns of behaviour do not fit this picture. The same people buy insurance against small-probability losses and buy lottery tickets with small-probability gains (Friedman and Savage, 1948, doi:10.1086/256692); subjects who are risk averse for gains are risk seeking for the mirrored losses, the reflection effect; and subjects who are indifferent between full insurance and bearing a risk reject half-price insurance that pays only half the time, probabilistic insurance (Kahneman and Tversky, 1979, doi:10.2307/1914185).

David E. Bell's 1982 paper Regret in Decision Making under Uncertainty (doi:10.1287/opre.30.5.961) proposes that a decision maker cares not only about what she obtains but also about what she would have obtained had she chosen differently. Its first part (the companion mission of this series) derives the representation $u(x,y)=\alpha v(x)+f(v(x)-v(y))$; its Section 2 shows that the single additive form with linear $v$ explains all of the patterns above at once, provided the regret function $f$ is decreasingly concave. Regret theory, developed at the same time by Loomes and Sugden (1982, doi:10.2307/2232669), remains one of the standard alternatives to expected utility in decision analysis and behavioural economics.

Setting

A decision maker chooses between two alternatives $a$ and $b$. Uncertainty is described by finitely many states $i$ with probabilities $\pi_i$; in state $i$ alternative $a$ gives final assets $a_i$ and $b$ gives $b_i$. Choosing $a$ means forgoing $b$, and an outcome is valued by the regret utility

$$u(x,y)=x+f(x-y),$$

where $x$ is the final assets received, $y$ the assets the foregone alternative would have given in the same state, and $f:\mathbb R\to\mathbb R$ the regret function. The expected utility of selecting $a$ when $b$ is foregone is

$$\mathrm{EU}_\pi(a\,|\,b)=\sum_i \pi_i\,u(a_i,b_i),$$

and $a$ is strictly preferred to $b$ when $\mathrm{EU}_\pi(b\,|\,a)<\mathrm{EU}_\pi(a\,|\,b)$ (the paper's inequality (1)); $a$ and $b$ are indifferent when the two expected utilities are equal.

The comparisons are given by three payoff tables. Table II: a horse wins with probability $p$; betting \p$gives$1-p$if it wins and$-p$if it loses, not betting gives$0$. Table III: a car is damaged with probability$p$at a cost of$1$; insuring gives$-p$in both states, not insuring gives$-1$or$0$. Table IV: an accident has probability$q$; self insurance gives$-1$or$0$, full insurance$-p$always, and probabilistic insurance, which charges half the premium and pays with probability one half given an accident, gives$-p$,$-1$or$-p/2$.

The regret function $f$ is decreasingly concave if it is twice differentiable with strictly increasing second derivative $f''$. Section 3 also uses $g(r)=r+f(r)-f(-r)$ and the negative exponential $f(r)=1-e^{-\gamma r}$, $\gamma>0$.

Formalization targets

Goal: coexistence of insurance and gambling

If $f$ is decreasingly concave and $0<p<\tfrac12$, then the bet of Table II is strictly preferred to not betting and insuring in Table III is strictly preferred to not insuring:

$$p\,[f(1-p)-f(p-1)]>(1-p)\,[f(p)-f(-p)].$$

Both comparisons have equal expected values, so the statement is a pure regret effect. The goal fixes no constants and assumes nothing about $f$ beyond decreasing concavity; it is the weakest hypothesis the page offers.

Milestones

1. Display (5): the bet is preferred iff the inequality above; display (6): insurance is preferred iff the same inequality, so the two preferences coincide.
2. The inequality holds for $0<p<\tfrac12$ whenever $(f(x)-f(-x))/x$ is strictly increasing on $x>0$; and that ratio is strictly increasing whenever $f''(x)>f''(-x)$ for $x>0$.
3. The reflection effect (Sec. 2(ii)): $x_2$ for sure is indifferent to the lottery $(p:x_1;\,1-p:x_3)$ iff $-x_2$ for sure is indifferent to $(p:-x_1;\,1-p:-x_3)$.
4. Probabilistic insurance (Sec. 2(iii)): display (9) characterises indifference between full and self insurance; under (9) and $0\le q<1$,

$$f(p/2)-f(-p/2)<\tfrac12\,[f(p)-f(-p)]\qquad(11)$$

holds iff full insurance is strictly preferred to probabilistic insurance, iff probabilistic insurance is strictly preferred to self insurance; and (11) follows from the same ratio condition. 5. The negative exponential (Sec. 3): $f$ concave, $g$ convex on $r\ge0$, $g(r)/r$ strictly increasing on $r>0$, and $f$ decreasingly concave.

Significance

The goal is the paper's central behavioural claim: one regret function explains why the same decision maker gambles on long odds and buys insurance at fair prices, behaviour that a single concave or convex utility of wealth cannot produce. The milestones show that the reflection effect and the rejection of probabilistic insurance follow from the same model, and two of them reduce to the same inequality on the odd part $f(x)-f(-x)$ of the regret function. The negative exponential example shows the hypotheses are met by a concrete, commonly used function, so the explanation is not vacuous.

The results are proved in the paper by short calculations, and none of them has been machine-checked before. The mission produces a formal statement of the regret model of Section 2 with its payoff tables, which pins down several points the printed text leaves loose: the meaning of "decreasingly concave", the domain on which "increasing" and "convex" are meant, and three misprinted intermediate displays.

Difficulty

The comparisons (5), (6), (9) and the reflection identity are algebraic once the payoff tables are expanded; the work is in expanding them correctly, since the foregone argument of $u$ changes with the alternative selected and three printed expansions are wrong. The substance lies in the analytic step: passing from a pointwise condition on $f''$ to strict monotonicity of $(f(x)-f(-x))/x$ on $(0,\infty)$, with strict inequalities throughout and through a quotient that is undefined at $0$. The naive reading of the page's condition, "$f''(x)>f''(-x)$ for all $x$", is unsatisfiable and cannot be used as a hypothesis.

Formalization scope

All quantities are real numbers. The utility is regretU f x y = x + f (x - y), i.e. form (4) with $v(x)=x$ exactly; the page assumes $v$ only "approximately linear" but computes every display with $v(x)=x$. A comparison is a finite state space Fin n with a real weight vector; the theorems instantiate it with $(p,1-p)$ for Tables II–III and with $(q/2,q/2,1-q)$ for Table IV, the accident state split by whether the insurer pays. Strict preference is strict inequality of expected regret utilities; indifference is equality.

Conventions and corrections, each disclosed in the item concerned:

• "Decreasingly concave" is not defined in the paper; it is read as Differentiable ℝ f, Differentiable ℝ (deriv f) and StrictMono (deriv (deriv f)). The page's presumption that $f$ is increasing and concave is not assumed.
• "Increasing" is read strictly, because the conclusions (5), (6), (11) are strict, and on $x>0$, because $(f(x)-f(-x))/x$ is undefined at $0$ and even.
• "$f''(x)>f''(-x)$ for all $x$" is read for $x>0$.
• The convexity of $g$ in the exponential example is stated on $r\ge0$: $g(r)=r+2\sinh(\gamma r)$ is concave for $r<0$, as the paper itself notes on p. 977.
• Misprints corrected: the last bracket of the second reflection equality on p. 973; $f(p/2)$ for $f(-p/2)$ in the expansion before (10) and in the probabilistic-versus-self display on p. 975, which also lacks a factor $q$. The normalisation $f(0)=0$ is not needed.
• The equivalences (5), (6), (9) and the reflection identity hold for every real probability and are stated without a range; the goal keeps $0<p<\tfrac12$ and the probabilistic-insurance statement keeps $0\le q<1$.

The goal cannot be satisfied vacuously: the negative exponential milestone exhibits a decreasingly concave $f$, and the conclusion is a strict preference between two alternatives of equal expected value. Section 2(iv) (preference reversals) is not formalized: its printed rewriting of (12) in terms of $h$ drops a linear term and its conclusion is unquantified ("for sufficiently small units of money").

Contributions welcome: proofs of the algebraic reductions, the slope argument for $(f(x)-f(-x))/x$, and the convexity facts for $\sinh$; the latter two are reusable beyond this mission.

Selected references

• D. E. Bell, Regret in Decision Making under Uncertainty, Operations Research 30(5), 961–981, 1982. doi:10.1287/opre.30.5.961
• D. Kahneman and A. Tversky, Prospect Theory: An Analysis of Decision under Risk, Econometrica 47(2), 263–291, 1979. doi:10.2307/1914185
• G. Loomes and R. Sugden, Regret Theory: An Alternative Theory of Rational Choice under Uncertainty, The Economic Journal 92(368), 805–824, 1982. doi:10.2307/2232669
• M. Friedman and L. J. Savage, The Utility Analysis of Choices Involving Risk, Journal of Political Economy 56(4), 279–304, 1948. doi:10.1086/256692

Motivation

Many planning problems are made in two stages: a first decision $x$ is fixed before an uncertain parameter is revealed, and a second decision $y$ is taken afterwards. Two models compete for such problems. Two-stage stochastic optimization assumes a probability distribution over the scenarios and minimizes the expected cost, letting the second-stage decision depend on the scenario. Robust optimization asks for one solution that is feasible in every scenario and minimizes the worst-case cost. The robust problem is usually far easier to solve: it is a single deterministic problem, while the stochastic problem optimizes over policies. The question is how much cost one gives up by solving the easy problem instead of the hard one.

Bertsimas and Goyal (Math. Oper. Res. 2010) measure this loss by the stochasticity gap, the ratio of the robust optimum to the stochastic optimum. Their Theorem 2.1 shows that when only the right-hand side of the constraints is uncertain, the uncertainty set is symmetric and the distribution is centred at the point of symmetry, the robust optimum is at most twice the stochastic one. Section 3 asks whether the same holds when the second-stage costs are uncertain as well, and answers no with an explicit instance: Theorem 3.1. This mission formalizes that instance.

Setting

There are no first-stage variables. The second-stage decision is a vector $y\in\mathbb R^n_+$ with $n\ge1$ continuous coordinates, subject to the single covering constraint

$$y_1+y_2+\dots+y_n\ \ge\ 1 ,$$

the constraint $By\ge b$ with $B=[1,1,\dots,1]\in\mathbb R^{1\times n}$ and $b=1$. A set $\Omega$ of scenarios carries a cost map $d:\Omega\to\mathbb R^n$; in scenario $\omega$ the second-stage cost is $d(\omega)^{\mathsf T}y$. The uncertainty set is $I_{(b,d)}(\Omega)=\{(b(\omega),d(\omega)) : \omega\in\Omega\}$, here $\{1\}\times[0,1]^n$: the range of $d$ is the whole cube $[0,1]^n$. A probability measure $\mu$ on $\Omega$ makes the coordinates $d_1,\dots,d_n$ independent, each uniformly distributed on $[0,1]$.

The stochastic problem $\Pi_{\mathrm{Stoch}}(b,d)$, display (1.4) of the paper, chooses a policy $\omega\mapsto y(\omega)\ge0$ satisfying the constraint in every scenario and minimizes $\mathbb E_\mu[d(\omega)^{\mathsf T}y(\omega)]$; its optimal value is $z_{\mathrm{Stoch}}(b,d)$. The robust problem $\Pi_{\mathrm{Rob}}(b,d)$, display (1.5), chooses one $y\ge0$ satisfying the constraint and minimizes $\max_{\omega\in\Omega} d(\omega)^{\mathsf T}y$; its optimal value is $z_{\mathrm{Rob}}(b,d)$. A set $P$ is symmetric (Definition 1.2) if there is $u^0\in P$ with $u^0+z\in P\iff u^0-z\in P$ for every $z$.

The Lean development names these zStochBD and zRobBD (the general problems (1.4) and (1.5) with data $A$, $B$, $b$, $c$, $d$ and integer coordinate sets), and IsSymmetricAbout (Definition 1.2).

Formalization targets

Goal: Theorem 3.1 (p. 22)

$$z_{\mathrm{Rob}}(b,d)\ \ge\ (n+1)\cdot z_{\mathrm{Stoch}}(b,d).$$

The constant $n+1$ is the paper's. Both sides are pinned down separately by the milestones, so the goal cannot be satisfied by a degenerate value of either side.

Milestones

1. Symmetry of the instance (proof of Theorem 3.1, pp. 22–23): the uncertainty set is symmetric about $(1,(\tfrac12,\dots,\tfrac12))$ and $\mathbb E_\mu[d(\omega)]=(\tfrac12,\dots,\tfrac12)$, so the hypotheses of the symmetric theory hold.
2. Robust side (p. 23): $z_{\mathrm{Rob}}(b,d)\ge1$.
3. Eq. (3.1) (p. 23): $z_{\mathrm{Stoch}}(b,d)\le\mathbb E_\mu[\min(d_1(\omega),\dots,d_n(\omega))]$.
4. Eq. (3.2) (p. 23): $\mathbb E_\mu[\min(d_1(\omega),\dots,d_n(\omega))]=\dfrac1{n+1}$.

Significance

Theorem 3.1 marks the boundary of the paper's positive results. The bound $z_{\mathrm{Rob}}\le2\,z_{\mathrm{Stoch}}$ of Theorem 2.1 needs only symmetry of the uncertainty set and a centred distribution. The instance here has both, has no integer variables and a single constraint, and still has a gap that grows linearly in the dimension. So symmetry alone does not make a robust solution a good approximation of the stochastic optimum when costs are uncertain. The paper's abstract states this as one of its main conclusions, and it is why Sections 4 and 5 compare the robust problem with the adaptive problem, whose worst-case objective does not suffer from it.

The result is proved in the paper; to our knowledge it has no machine-checked proof. What this mission adds is a formal proof of the instance against the general definitions of the two-stage problems, including the probabilistic computation (3.2), the expected minimum of independent uniform random variables, which Mathlib does not contain. That computation is reusable wherever order statistics of uniforms appear, for example in auctions, secretary problems and random-assignment bounds.

Difficulty

The robust half is short. The stochastic half has two parts. Eq. (3.1) needs a measurable policy that selects a cheapest coordinate; the policy printed in the paper puts a unit on every minimizing coordinate, which at ties overpays, so a formal proof must choose a single minimizer measurably and use integrability on the probability space. Eq. (3.2) is the main work: it is a genuine integral over the $n$-dimensional cube against a product measure, for every $n$, and Mathlib has no lemma on the distribution or the expectation of the minimum of independent random variables.

Formalization scope

• Vectors are Fin k → ℝ with the componentwise order; $B$ is the all-ones Matrix (Fin 1) (Fin n) ℝ, $A$ and $c$ live on Fin 0, $b(\omega)=1$, and the integer coordinate sets are empty ($p_1=p_2=0$).
• Optimal values are infima in EReal, $+\infty$ when infeasible; the robust worst-case cost is an EReal supremum. No optimal solution is assumed to exist: the paper's "consider an optimal solution" is a proof device, and the statements are about the infima.
• Stochastic policies must be integrable, together with their cost $\omega\mapsto d(\omega)^{\mathsf T}y(\omega)$, and satisfy the constraint in every scenario, as on the page, not only almost surely.
• The scenario space is an arbitrary probability space $(\Omega,\mu)$ with a measurable $d$ whose range is exactly $[0,1]^n$ and whose law is the product of $n$ uniform distributions on $[0,1]$. This is the paper's "each $d_j$ is distributed uniformly at random between 0 and 1 and independent of other coefficients" together with its description of $I_{(b,d)}(\Omega)$.
• $n\ge1$ is assumed; the paper leaves it implicit.
• The paper prints $\mathbb Z^{n_2}_+$ for the second-stage integer block in (1.4)–(1.5); $\mathbb Z^{p_2}_+$ is meant, and here $p_2=0$. Eq. (3.2) is called an inequality on the page; it is formalized as the equality it is.

A real-valued infimum would assign the value $0$ to an infeasible or ill-posed problem and make the goal trivially true; the EReal infima, and the separate milestones fixing $z_{\mathrm{Rob}}\ge1$ and $z_{\mathrm{Stoch}}\le\mathbb E[\min_j d_j]=1/(n+1)$, rule that out.

Contributions are welcome on each milestone separately. The expected-minimum computation (3.2) is self-contained and of independent use; a general lemma on the law of the minimum of independent random variables would serve it and other missions.

Selected references

• D. Bertsimas, V. Goyal, On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1090.0440 (cited here from the authors' manuscript, MIT DSpace).
• J. R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
• D. Bertsimas, M. Sim, The Price of Robustness, Operations Research 52(1), 2004. https://doi.org/10.1287/opre.1030.0065

Why regret enters the utility function

Expected utility theory predicts that a decision maker's choice between two lotteries depends only on the distribution of final wealth under each. Observed behaviour contradicts this in systematic ways: the Allais paradox, the coexistence of insurance and gambling, and the reflection effect documented by Kahneman and Tversky (1979). David Bell's 1982 paper (Operations Research 30(5), 961–981) explains these patterns by regret: the dissatisfaction of learning that the alternative not chosen would have done better. In the same year Loomes and Sugden (1982) proposed a closely related theory; together the two papers are the origin of regret theory in decision analysis.

Bell's contribution is axiomatic. Instead of postulating a regret term, he derives the shape of a utility function that incorporates regret from three behavioural assumptions about how preferences respond to shifting all outcomes by an equal increment of value. This mission formalizes that derivation, Section 1 of the paper (pp. 965–970), culminating in Theorem 1.

Setting

An endpoint is described by two attributes: the final assets $x$ and the foregone assets $y$, the asset level the decision maker would have had under the alternative not chosen. Utility is a function $u(x,y)$, strictly increasing in $x$ and strictly decreasing in $y$.

A simple comparison is a choice between two alternatives whose uncertainties are resolved by one predetermined joint distribution. With $n$ states, a probability vector $p=(p_1,\dots,p_n)$ and alternatives $A,B\in\mathbb R^n$ ($A_i$ the final assets of $A$ in state $i$), the expected utility of selecting $A$ while $B$ is foregone is

$$\mathrm{EU}_p(A\,|\,B)=\sum_{i=1}^n p_i\,u(A_i,B_i),$$

and $A$ is preferred to $B$ when $\mathrm{EU}_p(B\,|\,A)<\mathrm{EU}_p(A\,|\,B)$ (inequality (1) of the paper).

A value function $v:\mathbb R\to\mathbb R$, strictly increasing and onto $\mathbb R$, measures incremental value: moving from $a$ to $b$ is worth $v(b)-v(a)$. An alternative $A'$ is obtained from $A$ by a shift of incremental value $\delta$ if $v(A'_i)=v(A_i)+\delta$ for every state.

• Assumption 1. Shifting every outcome of both alternatives by the same incremental value leaves the preferred alternative unchanged.
• Assumption 2. If $v(x_2)-v(x_1)=v(x_3)-v(x_2)$, the decision maker is indifferent between $x_2$ for sure and a 50-50 lottery between $x_1$ and $x_3$.
• Assumption 3. If selecting $L_1$ over $L_2$ is preferred to selecting $L_3$ over $L_4$, that is $\mathrm{EU}_p(L_3\,|\,L_4)<\mathrm{EU}_p(L_1\,|\,L_2)$, this persists after all outcomes of all four alternatives are shifted by the same incremental value.

Formalization targets

Goal: the regret form (Theorem 1, p. 969, corrected)

Under Assumptions 2 and 3, there are a constant $\alpha$ and a function $f$ with

$$u(x,y)=\alpha\,v(x)+f\big(v(x)-v(y)\big)\quad\text{for all }x,y.$$

Utility separates additively into a term in the value of final assets and a function of the regret $v(x)-v(y)$. The coefficient $\alpha$ is left free (see Formalization scope).

Milestones, in the order of the paper's argument

1. Proof of Lemma 1 (p. 967): for $v(x)=x$, $w(x+h,y+h)=k(h)\,w(x,y)$ with $k(h)>0$, where $w(x,y)=u(x,y)-u(y,x)$.
2. Lemma 1, linear $v$ (p. 967): $u(x,y)-u(y,x)=[u(0,y-x)-u(y-x,0)]\,e^{-cx}$.
3. Lemma 1 (p. 967): Assumption 1 implies $u(x,y)-u(y,x)=g(v(x)-v(y))\,e^{-c\,v(x)}$.
4. Lemma 2, linear $v$ (p. 968): $u(x,y)-u(y,x)=u(0,y-x)-u(y-x,0)$.
5. Lemma 2 (p. 968): Assumptions 1 and 2 imply $u(x,y)-u(y,x)=g(v(x)-v(y))$.
6. Assumption 1 is a special case of Assumption 3 (p. 969).
7. Proof of Theorem 1 (p. 970): for $v(x)=x$, $u(x+h,y+h)-u(x,y)=j(h)$.
8. Theorem 1 for $v(x)=x$ (p. 970): $u(x,y)=\alpha x+u(0,y-x)$.

Significance

The additive form is the basis of the rest of Bell's paper: Section 2 uses it to show that a single decision maker with $f$ decreasingly concave both buys fair insurance and takes long-odds bets, and to account for the Allais paradox and the reflection effect. The same additive structure, a value term plus a function of the regret difference, is the form in which regret theory has been used since, alongside the parallel proposal of Loomes and Sugden (1982). Lemmas 1 and 2 have independent content: simple comparisons identify only the antisymmetric part $u(x,y)-u(y,x)$, and the lemmas pin that part down to a function of the regret difference.

The results are published with proofs in prose; none has a machine-checked proof. Formalizing them checks the argument as printed, which turns out to need a correction (the coefficient of $v(x)$ in (4)), and fills in the regularity steps the paper leaves implicit: the solutions of the Cauchy equations that appear, and the passage from $v(x)=x$ to a general value function.

Difficulty

The obvious argument reads each assumption as a functional equation and solves it. Two steps resist this. First, the functional equations $k(x+h)=k(x)k(h)$ and $j(x+h)=j(x)+j(h)$ have non-measurable solutions; excluding them needs boundedness of $k$ and $j$ on intervals, which must be extracted from the monotonicity of $u$ and is never stated on the page. Second, the proof of Theorem 1 compares two 50-50 lotteries that are indifferent and requires $g(a_1-b_1)$ to take an arbitrary value $u(c_1,c_2)-u(a_2,b_2)$; when $g$ is bounded no such indifference exists, so the printed step does not cover every case. Passing from $v(x)=x$ to a general $v$ requires transporting all three assumptions along $v^{-1}$.

Formalization scope

• Assets, probabilities and utilities are real numbers; $u$ is u : ℝ → ℝ → ℝ with u x y $=u(x,y)$. Every theorem assumes $u$ strictly increasing in $x$ and strictly decreasing in $y$ (the paper's "increasing"/"decreasing", p. 965, read strictly).
• A simple comparison is a probability vector on Fin n and two alternatives on the same states. Assumption 3 quantifies over four alternatives on one common state space, the setting of the paper's own use of it.
• The value function is strictly increasing (p. 968) and, as an added reading, maps $\mathbb R$ onto $\mathbb R$: Assumptions 1 and 3 shift outcomes by arbitrary equal incremental values, which presupposes that every shifted value is attained. "$v$ linear" (Lemmas 1, 2) is read as $v(x)=ax+b$ with $a>0$.
• Indifference in Assumption 2 is "neither alternative is preferred", equivalent to the first display on p. 969.
• Corrected slip. The paper's display (4) and the end of its proof have coefficient $1$ on $v(x)$ (resp. $x$). This is false as printed: $v(x)=x$, $u(x,y)=x-y$ satisfies every hypothesis, but $x-y=x+f(x-y)$ forces $f(0)=0$ at $x=y=0$ and $f(0)=-1$ at $x=y=1$. The proof derives $j(h)=\alpha h$ and silently sets $\alpha=1$. The goal and milestone 8 keep $\alpha$ free, with no sign or normalisation imposed; milestone texts stay verbatim.
• All existential objects ($k$, $c$, $g$, $j$, $\alpha$, $f$) are chosen before the variables $x,y,h$. The assumptions are statements about preferences between lotteries, never functional equations on $u$; a formalization that states an assumption as "$u(x+h,y+h)-u(x,y)$ is independent of $(x,y)$" would put the conclusion into the hypothesis and is ruled out.
• Needed infrastructure: monotone or locally bounded solutions of the Cauchy additive and multiplicative equations on $\mathbb R$, and transport of the assumptions along an order isomorphism of $\mathbb R$. Both are reusable; contributions proving either are welcome.

Selected references

• D. E. Bell, Regret in Decision Making under Uncertainty, Operations Research 30(5), 961–981, 1982. https://doi.org/10.1287/opre.30.5.961
• G. Loomes and R. Sugden, Regret Theory: An Alternative Theory of Rational Choice under Uncertainty, The Economic Journal 92(368), 805–824, 1982. https://doi.org/10.2307/2232669
• D. Kahneman and A. Tversky, Prospect Theory: An Analysis of Decision under Risk, Econometrica 47(2), 263–291, 1979. https://doi.org/10.2307/1914185

Motivation

Online bipartite matching models a platform that must commit each arriving request to a resource immediately. The motivating application of Feldman, Mehta, Mirrokni and Muthukrishnan is display advertising: an ad server knows from past traffic how many impressions of each type (web page, audience segment) to expect, sells them to advertisers in advance, and must assign each impression to an interested advertiser the moment a user loads the page. The goal is to fill as many contracted impressions as possible.

When arrivals are chosen by an adversary, the best ratio an online algorithm can guarantee is $1 - 1/e \approx 0.632$, achieved by the RANKING algorithm of Karp, Vazirani and Vazirani (STOC 1990). The ad server, however, is not facing an adversary: it has a forecast. The i.i.d. model captures this: the graph and the distribution of impression types are known in advance, and the impressions are independent draws. The paper asks whether this knowledge allows an online algorithm to beat $1 - 1/e$, and answers yes.

Timeline.

• 1990: Karp, Vazirani and Vazirani give RANKING, with ratio $1 - 1/e$ for adversarial arrivals, and show this is optimal in that model.
• 2005: Mehta, Saberi, Vazirani and Vazirani obtain $1 - 1/e$ for the budgeted AdWords generalization.
• 2009: Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) show that in the i.i.d. model the two suggested matchings algorithm achieves about $0.670$ with high probability when OPT is linear in $n$, the first ratio above $1 - 1/e$ for this model, and that no online algorithm reaches $26/27$ in expectation.

Setting

An instance is a bipartite graph $G = (A, I, E)$ with a finite set $A$ of advertisers, a finite set $I$ of impression types, and edges $E \subseteq A \times I$ recording which advertisers want which types. The mission treats the case analysed throughout §4.2 of the paper, in which one impression of each type is expected ($e_i = 1$). So $n = |I|$ impressions arrive one at a time, with types $\omega(0), \dots, \omega(n-1)$ drawn independently and uniformly from $I$. On arrival an impression must be assigned at once and irrevocably to a still unassigned advertiser adjacent to its type, or discarded. $\mathrm{ALG}(\omega)$ is the number of impressions an algorithm assigns. $\mathrm{OPT}(\omega)$ is the size of a maximum matching of the realization graph, which has one node per arrival $t$, joined to every advertiser $a$ with $(a, \omega(t)) \in E$.

The two suggested matchings (TSM) algorithm works offline first. Its boosted flow graph $G_f$ has a source arc of capacity $2$ into every advertiser, a unit-capacity arc along every edge of $E$, and an arc of capacity $2$ from every type to a sink. The algorithm takes the edge set $E_f$ of an integral maximum flow. Every vertex then has at most two edges of $E_f$, so $E_f$ splits into vertex-disjoint paths and cycles. The algorithm colours each component blue and red:

• on cycles, the colours alternate;
• on odd paths, the colours alternate, with more blue than red;
• on even paths between advertisers, the colours alternate;
• on even paths between types, the first two edges are blue, then the colours alternate, ending in blue.

Online, the first arrival of type $i$ tries the advertiser along $i$'s blue edge, the second tries the one along its red edge, and later arrivals are discarded. A tried advertiser that is already taken is not reassigned. The advertisers fall into four classes by their coloured edges: $A_{BR}$ (one blue, one red), $A_{BB}$ (two blue), $A_B$ (one blue only) and $A_R$ (one red only).

Formalization targets

Goal: Theorem 5, first sentence, $e_i = 1$

Let

$$\alpha = \frac{1 - 2/e^2}{4/3 - 2/(3e)} \approx 0.67029 .$$

The goal has three parts. First, every maximum flow edge set admits a colouring that follows the rules. Second, for every $\varepsilon > 0$ and $c > 0$ there are $\delta > 0$ and $N$ such that, for every instance with $n \ge N$, every maximum flow edge set and every rule-following colouring,

$$\Pr_\omega\big[\ \mathrm{OPT} \ge c\,n \implies \mathrm{ALG} \ge (\alpha - \varepsilon)\,\mathrm{OPT}\ \big] \;\ge\; 1 - e^{-\delta n}.$$

Third, $\alpha > 1 - 1/e$.

Milestones

1. Facts 1 and 2: concentration for two balls-in-bins statistics.
2. The note of §4.2.1: each type has no coloured edge, one blue edge, or one blue and one red edge.
3. Equation (1): $|E_f| = 2|A_{BR}| + 2|A_{BB}| + |A_B| + |A_R|$.
4. Equation (2): with high probability, $\mathrm{ALG} \ge (1 - 1/e^2)|A_{BB}| + (1 - 2/e^2)|A_{BR}| + (1 - 3/(2e))(|A_B| + |A_R|) - 4\varepsilon n$.
5. Equation (3): $|E_f| = 2(|A_T| + |I_S|) + |E_\delta|$ for the surgered residual cut $(S,T)$ of $G_f$.
6. Equation (4): with high probability, $\mathrm{OPT} \le |A_{BR}| + |A_{BB}| + \tfrac12(|A_B| + |A_R|) + (\tfrac12 - \tfrac1e)|E_\delta| + \varepsilon n$.
7. Lemma 1: $|E_\delta| \le \tfrac23|A_{BR}| + \tfrac43|A_{BB}| + |A_B| + \tfrac13|A_R|$.

Significance

The theorem separates the i.i.d. model from the adversarial one: knowing the distribution is worth a constant factor above $1 - 1/e$. The suggested matching algorithm of the same paper (Theorem 4) shows that following a single offline matching gets exactly $1 - 1/e$, so the second, red matching is what crosses the barrier. The paper's question started a line of work on the i.i.d. and random-order models, with later improvements to the constant by other authors under further assumptions.

The result has a written proof but, as far as the platform record shows, no machine-checked one. The mission formalizes the paper's own argument: the flow-and-colouring construction, the balls-in-bins concentration facts, the cut-based bound on OPT and the combinatorial Lemma 1. It also fixes two slips in the printed statements (see Formalization scope). The pieces are reusable beyond this paper. The occupancy concentration (Fact 1) and the satisfied-sequences bound (Fact 2) recur in analyses of online algorithms with stochastic input. The degree-capped flow encoding and its path/cycle decomposition are standard tools for 2-matchings.

Difficulty

The upper bound on OPT is the delicate part. A cut of the flow graph bounds the maximum matching of the realization graph only after a second surgery that depends on the random arrivals. Its size must then be compared with the colour classes, which are defined by a different structure (the components of $E_f$). Lemma 1 bridges the two, and it depends on the exact colouring rules: a colouring that only satisfies local degree conditions can put red edges at both ends of an even advertiser path, which breaks the inequality $|A_B| \ge |A_R|$ behind (2). On the probabilistic side, the advertisers of $A_{BR}$ share impression types with each other, so the success events are dependent, and Fact 2 needs a bounded-differences argument in which one ball affects up to $d$ sequences.

Formalization scope

All declarations live in the namespace OnlineStochMatching.TSM. Advertisers and types are finite types A I : Type, and $E$ is a Finset (A × I). Probabilities are counting ratios $\#\{\omega : \mathrm{Fin}\ n \to I \mid P\,\omega\}/|I|^n$, so there are no measurability side conditions. OPT is a maximum over the finite, nonempty set of partial injective assignments. An integral flow of $G_f$ is its set of saturated middle edges, i.e. a subset of $E$ with at most two edges per vertex; $E_f$ is such a set of maximum cardinality. A colouring is given by a listing of the components of $E_f$ as vertex sequences. Every theorem quantifies over every maximum $E_f$ and every colouring the rules allow, since the paper fixes neither.

The paper's asymptotic phrases are replaced by explicit quantifiers that come from its own proofs:

• "with probability $1 - e^{-\Omega(n)}$" and "with high probability" (Theorem 5, (2), (4)) become: $\exists\, \delta > 0,\ \exists\, N$, chosen before the instance, with probability at least $1 - e^{-\delta n}$ for all $n \ge N$;
• "as long as OPT $= \Omega(n)$" becomes the event $\mathrm{OPT} \ge c\,n$ for an arbitrary $c > 0$ fixed before $\delta$ and $N$;
• the $O(1)$ term in the bound on $|A^*_\delta|$ (p. 8) is absorbed into $\varepsilon n$ for $n \ge N$.

Corrections to the printed statements:

• Theorem 5 prints $\mathrm{ALG}/\mathrm{OPT} - \epsilon \ge \alpha$; the proof concludes $\mathrm{ALG}/\mathrm{OPT} + \epsilon \ge \alpha$, so the goal states $\mathrm{ALG} \ge (\alpha - \varepsilon)\mathrm{OPT}$;
• Fact 1 prints the failure probability $2e^{-\epsilon n/2}$; its proof gives $2e^{-\epsilon^2 n/2}$, which is used;
• Fact 2 states two hypotheses its proof uses: the bins of a sequence are distinct, and $c^2 < n$.

The ratio is multiplied out, so no division by OPT occurs. A colouring condition that is unsatisfiable, or a flow set that is not maximum, would make the goal vacuous or false; part (a) of the goal rules out the first, and every statement requires maximality. Not included: the reduction to general integer $e_i$ (§4.2.4), the tightness sentence of Theorem 5 (§4.2.5), and footnote 7's variant of the algorithm.

Useful infrastructure: bounded-differences (McDiarmid/Azuma) inequalities for functions of i.i.d. uniform variables, which exist on the platform as separate theorems; path/cycle decomposition of graphs of maximum degree two; and max-flow min-cut for unit-capacity bipartite networks. Contributions are welcome on Facts 1 and 2 independently of the combinatorics, and on Lemma 1 and equations (1) and (3), which are deterministic.

Selected references

• J. Feldman, A. Mehta, V. Mirrokni, S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, FOCS 2009; arXiv:0905.4100v1. https://arxiv.org/abs/0905.4100
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
• A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and generalized online matching, FOCS 2005; J. ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321

Assortment planning with nested choice

A retailer that groups its products into categories (brands, store sections, flight classes) and decides which products to display in each faces the assortment problem: offering more products attracts more customers but also diverts sales away from the most profitable products. The nested logit model is the standard description of customer choice in this setting. A customer first selects a category (a nest), then a product within it. Choice-based models of this kind are the basis of revenue management under customer choice (Talluri and van Ryzin 2004).

Davis, Gallego and Topaloglu (DGT 2014) study the assortment problem under the nested logit model with two features that earlier work excluded: dissimilarity parameters larger than one, under which products in a nest act as complements rather than substitutes, and a no-purchase option inside each nest, under which a customer may enter a nest and still leave without buying. They show that the problem is NP-hard once either feature is present. For each regime they give a small linear program whose solution yields an assortment with a provable performance guarantee. This mission formalizes the guarantee for the most general instances, where both features occur together (§6.1, Theorem 11).

Timeline. Rusmevichientong, Shmoys and Topaloglu (2010) bound nested-by-revenue assortments under a multinomial logit mixture. [DGT 2014] prove that nested-by-revenue assortments are optimal for dissimilarity parameters at most one without within-nest no-purchase options (Theorem 4). They give factor-(6) guarantees with synergistic products, a factor-two guarantee via knapsack relaxations for partially-captured nests (Theorem 10), and the general factor (12) of Theorem 11. Li, Rusmevichientong and Topaloglu (2015) extend the nested-by-revenue result to $d$-level nested logit models.

The model

There are nests $i\in M=\{1,\dots,m\}$ and, in each nest, products $j\in N=\{1,\dots,n\}$. Product $j$ of nest $i$ has revenue $r_{ij}\ge0$ and preference weight $v_{ij}>0$, with $r_{i1}\ge r_{i2}\ge\dots\ge r_{in}$. Nest $i$ has a no-purchase weight $v_{i0}\ge0$ and a dissimilarity parameter $\gamma_i>0$, and $v_0\ge0$ is the weight of choosing no nest at all. For an assortment $S_i\subseteq N$,

$$V_i(S_i)=v_{i0}+\sum_{j\in S_i}v_{ij},\qquad R_i(S_i)=\frac{\sum_{j\in S_i}r_{ij}v_{ij}}{V_i(S_i)} .$$

A customer chooses nest $i$ with probability $V_i(S_i)^{\gamma_i}/(v_0+\sum_l V_l(S_l)^{\gamma_l})$, and the expected revenue is

$$\Pi(S_1,\dots,S_m)=\frac{\sum_{i}V_i(S_i)^{\gamma_i}R_i(S_i)}{v_0+\sum_{i}V_i(S_i)^{\gamma_i}} .$$

The optimal value $Z^*$ of $\max\Pi$ equals the optimal value of the linear program

$$\text{(3)}\qquad \min\ x\quad\text{s.t.}\quad v_0x\ge\sum_i y_i,\qquad y_i\ge V_i(S_i)^{\gamma_i}\big(R_i(S_i)-x\big)\ \ \forall S_i\subseteq N,\ i\in M,$$

which has $2^n$ constraints per nest. Problem (4) keeps only the constraints for a chosen candidate collection of assortments in each nest.

A nest is fully captured if $v_{i0}=0$ ($i\in M^f$) and partially captured if $v_{i0}>0$ ($i\in M^p$). $N_{ij}=\{1,\dots,j\}$ is the nested-by-revenue assortment. $N^k_{ij}$ is the set of the $j$ highest-revenue products among the $k$ products of nest $i$ with the smallest preference weights, with $N^k_{i0}=\emptyset$ and $N^n_{ij}=N_{ij}$.

Formalization targets

Goal: Theorem 11

Let $(\hat x,\hat y)$ be an optimal solution of (4) when the candidate collection of every nest is $\{N^k_{ij}:k\in N,\ j=0,\dots,k\}\cup\{\{j\}:j\in N\}$, and let

$$\beta=\max_{i\in M^f,\ j=2,\dots,n}\left\{\frac{V_i(N_{ij})}{V_i(N_{i,j-1})}\right\}\vee\max_{i\in M^p,\ j=1,\dots,n}\left\{\frac{V_i(N_{ij})}{V_i(N_{i,j-1})}\right\}\vee2 \qquad (12).$$

Then $(\beta\hat x,\beta\hat y)$ is feasible for problem (3).

The theorem assumes $\bar\gamma=\max_i\gamma_i>1$, as all of §6 does. Otherwise it places no restriction on the $\gamma_i$ or the $v_{i0}$.

Milestones

1. $\hat x\ge0$ (A.4, p. 46).
2. Every greedy knapsack assortment $\hat S_i(\epsilon_i)$ of §5 is one of the $N^k_{ij}$ (pp. 24–25).
3. The relaxed nest problem over $[0,1]^n$ has an optimal solution of fractional-prefix form (A.4 Case 1, p. 47).
4. Inequality (30): for a nest with $\gamma_i>1$ and $\hat y_i\ge0$, $\beta\hat y_i$ bounds the relaxed objective at every fractional prefix (p. 47).
5. Case 1: $\gamma_i>1$, $\hat y_i\ge0$ gives the constraints of (3) for nest $i$ (pp. 47–48).
6. Problem (31) has a nested-by-revenue optimal solution when $\gamma_i>1$ and its coefficient $b=\beta\hat y_i$ is negative (p. 48).
7. Case 2: $\gamma_i>1$, $\hat y_i<0$ (p. 48).
8. Case 3: $\gamma_i\le1$, through the factor-two argument of Theorem 10 (pp. 48–49).

Two companions follow the goal. One is the resulting guarantee $\beta\,\Pi(\hat S)\ge Z^*\ge\Pi(\hat S)$, through Theorem 1. The other is the bound $\beta\le2\kappa$ when the preference weights within a nest differ by at most a factor $\kappa$ (p. 26).

Significance

Theorem 11, combined with Theorem 1 of the paper, gives a polynomial-size method for an NP-hard problem. The method solves one linear program with $1+m$ variables and $1+m(1+n+n^2)$ constraints, then reads off an assortment whose expected revenue is within the factor $\beta$ of the optimum. This holds for every nested logit instance, including nests where customers may walk away and nests whose products are complements. When the weights inside each nest are within a factor $\kappa$ of each other, the guarantee is at most $2\kappa$.

The theorem is proved in the paper's appendix. No part of it is machine-checked. Formalizing it checks a case analysis that reuses, by reference, arguments from two other theorems: Theorem 7 (synergistic, fully-captured nests) and Theorem 10 (competitive, partially-captured nests). It makes precise what these arguments need when the two regimes are mixed in one instance. The formalization also fixes the boundary conventions the printed proof leaves implicit: fully-captured nests with $k=1$, zero-weight denominators, and the sign of $\hat y_i$.

Difficulty

Each nest falls into one of three regimes, and a different argument controls each. With $\gamma_i\le1$ the nest behaves like a knapsack problem. Its guarantee of two needs the knapsack collection of §5 to sit inside $\{N^k_{ij}\}$. With $\gamma_i>1$ and $\hat y_i\ge0$, the constraint must be extended from nested-by-revenue sets to every subset. This goes through a continuous relaxation whose optimum has a fractional coordinate, and it costs the ratio $V_i(N_{ik})/V_i(N_{i,k-1})$, which is where (12) comes from. With $\gamma_i>1$ and $\hat y_i<0$, the scaling argument of Case 1 fails because multiplying by a factor at most one no longer preserves the inequality. The proof switches to the different objective (31), whose convexity in one coordinate forces an integral optimum.

The first idea, bounding every assortment by a nested-by-revenue one, is false here. With $\gamma_i>1$ or $v_{i0}>0$, nested-by-revenue assortments are not optimal, and the loss is exactly the factor $\beta$.

Formalization scope

Products are Fin n; $N_{ij}$ is nbr n j. Powers are Real.rpow, and $x/0=0$, so $R_i(\emptyset)=0$. Problems (3) and (4) are stated in constraint form: LP4Optimal means feasible and with $x$ minimal among feasible points. $\beta$ is the greatest element of the finite set betaSet I, which contains $2$ and the ratios of (12). Fully-captured nests skip $j=1$, as on the page. The collection is constructed: nestedPR breaks weight ties by index and revenue ties by index.

Standing assumptions, all disclosed:

• $v_{ij}>0$, $r_{ij}\ge0$ and $\gamma_i>0$. The page allows zero-weight padding products and $\gamma_i=0$, but its arguments do not cover them.
• $\bar\gamma>1$ on every statement set in Theorem 11's context.
• $n\ge1$ for the collection claim and the prefix claim.
• $v_{i0}>0$ for the statement about (31). That is the only kind of nest where Case 2 arises. For $v_{i0}=0$, Lean's $0^{1-\gamma_i}=0$ would remove the page's $+\infty$.
• $v_0>0$ for the guarantee, where Theorem 1 fails otherwise.
• $\kappa\ge1$, and $v_{i0}$ counted among the weights of a partially-captured nest ($v_{ij}\le\kappa v_{i0}$, $v_{i0}\le\kappa v_{ij}$), for the $2\kappa$ bound.

A trivializing formalization is ruled out. The goal states only feasibility for (3), with $\beta$ the maximum of (12), not any upper bound. The collection is the page's, not an arbitrary family containing it. The goal mentions none of the cases or the relaxations.

A complete development needs continuous knapsack solutions (greedy optimality, fractional prefixes), convexity of $t\mapsto t^{1-\gamma}$ on $(0,\infty)$, and the factor-two argument of Theorem 10. The knapsack and fractional-prefix lemmas are reusable for the companion missions of this series. Proofs of individual cases, and proofs of milestones in greater generality, are welcome.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 2014 (revised manuscript of June 18, 2013). https://doi.org/10.1287/opre.2014.1256
• P. Rusmevichientong, D. B. Shmoys, H. Topaloglu, Assortment optimization with mixtures of logits, technical report, Cornell University, 2010. http://legacy.orie.cornell.edu/~huseyin/publications/publications.html
• G. Li, P. Rusmevichientong, H. Topaloglu, The d-level nested logit model: assortment and price optimization problems, Operations Research 63(2), 2015.
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. https://doi.org/10.1017/CBO9780511921735

Motivation

Second-order stochastic dominance constraints let a decision maker require that a random outcome of a decision be preferred to a fixed benchmark outcome by every risk-averse expected-utility maximizer, without choosing a utility function in advance. Dentcheva and Ruszczyński introduced optimization under such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim., 2003), for the case where the decision enters the outcome linearly (the pure-dominance case). Their follow-up paper, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program., 2004), allows the decision to affect many random outcomes in a nonlinear, concave way, and derives optimality and duality theory in which the Lagrange multipliers of the dominance constraints are utility functions.

In applications (portfolio selection against a benchmark index is the paper's own example in §6) the probability space is a finite set of scenarios. Section 5 of the paper specialises the theory to that case. This mission formalizes that section: the reduction of the dominance constraints to finitely many inequalities, and the optimality and duality theorems (Theorems 6 and 7) in which the multipliers become piecewise-linear concave utilities.

Setting

There are $n$ scenarios $\omega_1,\dots,\omega_n$ with probabilities $p_j \ge 0$, $\sum_j p_j = 1$, and $m$ benchmark constraints, indexed by $i \in I = \{1,\dots,m\}$; $J = \{1,\dots,n\}$. A decision $z$ ranges over a convex set $Z \subseteq \mathbb R^N$. For each scenario $j$, $h_j:\mathbb R^N\to\mathbb R$ is the objective contribution and $g_{ij}:\mathbb R^N\to\mathbb R$ the $i$th outcome, all concave. The benchmark $Y_i$ has realizations $y_{ij}$. Write $(t)_+=\max(t,0)$.

The second-order dominance of a finitely distributed $X_i$ (realizations $x_{ij}$) over $Y_i$ on an interval $[a_i,b_i]$ reads

$$\sum_{j} p_j(\eta - x_{ij})_+ \le \sum_j p_j(\eta-y_{ij})_+ \quad\text{for all } \eta\in[a_i,b_i]. \tag{36}$$

The split-variable problem (38)–(41) is

$$\max \sum_{j=1}^n p_j h_j(z)\quad\text{s.t.}\quad \sum_{j} p_j(y_{ik}-x_{ij})_+ \le \sum_j p_j(y_{ik}-y_{ij})_+,\quad x_{ik}\le g_{ik}(z),\quad z\in Z,$$

for all $i\in I$, $k\in J$, over $z$ and $X=(x_{ij})\in\mathbb R^{mn}$. The Slater condition asks for $\tilde z \in \operatorname{relint} Z$ and $\tilde X$ satisfying the dominance constraints (39) with $\tilde x_{ik} < g_{ik}(\tilde z)$ for all $i,k$.

The utility set $V_i$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave, nondecreasing, piecewise linear with break points only at the $y_{ik}$, and zero on $[\max_k y_{ik},\infty)$. With $\theta_{ij}\ge 0$ multipliers for the splitting constraints $x_{ij}\le g_{ij}(z)$, the Lagrangian is

$$L(z,X,u,\theta) = \sum_{j=1}^n p_j\Big[h_j(z)+\sum_{i=1}^m\theta_{ij}g_{ij}(z)\Big]+\sum_{i=1}^m\sum_{j=1}^n p_j\big[u_i(x_{ij})-u_i(y_{ij})-\theta_{ij}x_{ij}\big]. \tag{42}$$

Multipliers $\mu_{ik}$ of the inequalities (39) generate the utility $u_i(t)=-\sum_k\mu_{ik}(y_{ik}-t)_+$ (46). The dual functional is $D(u,\theta)=\sup_{z\in Z,\,X}L(z,X,u,\theta)$ (47).

Formalization targets

Goal: Theorem 6

Under the Slater condition, $(\hat z,\hat X)$ optimal for (38)–(41) implies that there are $\hat u_i\in V_i$ and $\hat\theta\ge 0$ with

$$L(\hat z,\hat X,\hat u,\hat\theta)=\max_{(z,X)\in Z\times\mathbb R^{mn}}L(z,X,\hat u,\hat\theta),\qquad \sum_j p_j[\hat u_i(\hat x_{ij})-\hat u_i(y_{ij})]=0,\qquad \hat\theta_{ij}(\hat x_{ij}-g_{ij}(\hat z))=0;$$

conversely, these conditions together with feasibility imply optimality.

Milestones

1. Lemma 2 (p. 15): if $a_i\le y_{ij}\le b_i$, then (36) is equivalent to the $mn$ inequalities (37) at the realizations $\eta=y_{ik}$, and also to (36) on the whole line.
2. Eq. (46) (p. 17): for any $\mu$, the standard Lagrangian $\Lambda(z,X,\mu,\theta)$ equals $L(z,X,u,\theta)$ with $u$ given by (46).
3. p. 18: for $\mu_i\ge0$, the utility (46) lies in $V_i$.
4. pp. 16–17: under Slater, an optimal solution admits Kuhn–Tucker multipliers $\mu\ge0$, $\theta\ge0$ for (38)–(41) with complementarity.
5. p. 18: every $v\in V_i$ is of the form (46) with $\mu_i\ge0$.
6. Theorem 7 (p. 18), after the goal: the dual problem $\min\{D(u,\theta): u\in V_1\times\dots\times V_m,\ \theta\ge0\}$ has a solution and no duality gap.

Significance

Theorem 6 says that, for finitely many scenarios, the infinite-dimensional multiplier of the general theory (a concave utility in a cone of functions, Theorem 2 of the paper) can always be taken piecewise linear with kinks exactly at the benchmark's realizations. The multiplier space becomes finite-dimensional, $V_i$ is a polyhedral cone, and the dual problem of Theorem 7 is a finite-dimensional convex program. The paper's decomposition (49)–(51) of the dual functional and its numerical method in §6 rest on this. Lemma 2 is the standard reduction that makes dominance against a finitely distributed benchmark a finite set of polyhedral constraints, used throughout the later literature on dominance-constrained portfolio optimization.

The results are proved in the paper; none of them is formalized. The mission produces machine-checked statements of the finite-scenario theory, a Lean model of the utility set $V_i$ and of the correspondence between nonnegative multipliers and piecewise-linear utilities, and a Kuhn–Tucker theorem for concave programs with polyhedral constraints and a relative-interior Slater point.

Difficulty

The obvious route to Theorem 6 is to invoke a Kuhn–Tucker theorem. The available formal versions require every inequality constraint to hold strictly at the Slater point and range over all of $\mathbb R^N$. Neither fits: the dominance constraint at the smallest realization $y_{i,[1]}$ has right-hand side $0$ and a nonnegative left-hand side, so it can never hold strictly, and $Z$ may be lower-dimensional (a simplex), so only its relative interior is available. The polyhedral structure of (39) must be used, as in Rockafellar's Theorem 28.2. The second obstacle is the converse direction of the multiplier–utility correspondence: a utility in $V_i$ must be written as a nonnegative combination of the kinks $(y_{ik}-t)_+$, which requires handling repeated realizations and the one-sided slopes at each break point.

Formalization scope

• $\mathbb R^N$ is Fin N → ℝ; $X$, $\theta$, $\mu$ are Fin m → Fin n → ℝ; expectations are finite sums and positive parts are max t 0. No measure theory is used.
• Probabilities satisfy $p_j\ge0$, $\sum_jp_j=1$; $p_j=0$ is allowed, as on the page.
• Standing assumptions of p. 2 are explicit hypotheses: $Z$ convex and $h_j$, $g_{ij}$ concave on $\mathbb R^N$. Continuity is not stated, since finite concave functions on $\mathbb R^N$ are continuous.
• The relative interior is intrinsicInterior ℝ Z, not the topological interior. In the Slater condition only the splitting constraints are strict; the dominance constraints hold non-strictly.
• $V_i$ is defined by concavity, monotonicity, affinity on every interval whose interior contains no $y_{ik}$, and $u=0$ on $[\max_ky_{ik},\infty)$. This last clause is the page's $u(y_{i,[n]})=0$ combined with $V_i\subset\mathcal U_1([a_i,b_i])$. No positive slope is required, because the printed "$c>0$" in $\mathcal U_1$ is a misprint for $c\ge0$.
• "max" in (43) is an attained maximum over all of $Z\times\mathbb R^{mn}$, with no constraints on $X$. The dual functional (47) is an EReal supremum.
• Theorem 6 keeps the Slater condition as a hypothesis of the whole statement, as printed, although its converse part does not use it.
• A trivializing formalization is ruled out. $V_i$ is not defined as the set of functions of the form (46), which would make milestones 3 and 5 true by definition. Slater does not require strict dominance constraints, which would make it unsatisfiable. A sorry-free check confirms that the goal's hypotheses hold on an instance ($n=2$, $Z=[0,1]$).
• Reusable beyond this mission: the Kuhn–Tucker theorem with polyhedral constraints and relative-interior Slater point (milestone 4), and Lemma 2. Proofs of any item, and alternative proofs of the goal that avoid milestone 4, are welcome.
• The pure-dominance case is the earlier paper of Dentcheva–Ruszczyński (2003). The function $F_2$ and its expected-shortfall form are due to Ogryczak–Ruszczyński. The general Lagrange duality on the platform (ConvexOptimization.slater_strong_duality, Boyd–Vandenberghe §5.3.2) assumes a strict Slater point for every constraint and no set constraint, so it does not cover milestone 4.

Selected references

• D. Dentcheva, A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Math. Program., 2004 (cited here from the authors' revised manuscript, April 2003). https://doi.org/10.1007/s10107-003-0453-z
• D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14 (2003) 548–566. https://doi.org/10.1137/S1052623402420528
• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13 (2002) 60–78. https://doi.org/10.1137/S1052623400375075
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §28. https://doi.org/10.1515/9781400873173