Optimization

Motivation

Genetic algorithms with local search ("memetic" or hybrid genetic algorithms) are among the most effective heuristics for vehicle routing. Their recurring weakness is premature convergence: selection and local improvement both favour good individuals, so the population fills with near-copies of a few solutions and the search stalls. Vidal, Crainic, Gendreau, Lahrichi and Rei addressed this in their hybrid genetic search with adaptive diversity control (HGSADC) for multi-depot and periodic vehicle routing (CIRRELT-2010-34, 2010; journal version Operations Research 60(3), 2012). Instead of judging an individual by its cost alone, HGSADC ranks it by a Biased Fitness that mixes its cost rank with its rank in contribution to population diversity, and it uses that score to decide which individuals survive.

Trading cost for diversity raises an obvious worry: a very good but unoriginal solution could be discarded. The paper answers it with its only stated result, an elitism property (Section 4.6, an unnumbered Proposition with a three-sentence proof): the best individuals by cost are never discarded, as long as they are not clones. The HGSADC framework has since become the basis of state-of-the-art codes for many routing variants, and this guarantee is the one formal statement on which its population management rests.

Setting

HGSADC keeps two subpopulations (feasible and infeasible) and manages each separately. Everything below concerns one subpopulation; no routing object is involved.

A population is a finite set $P$ of individuals, with $\mathit{nbIndiv} = |P|$. Each individual $I$ has a penalized cost $c(I)\in\mathbb R$, its fitness (lower is better); a distance $\delta(I_1,I_2)$ to every other individual; and a diversity contribution $\Delta_P(I)$, which in the paper is the mean distance from $I$ to its $n_{close}$ nearest neighbours in $P$ (higher is better).

The normalized ranks of $I$ relative to the current population are

$$\mathit{fit}_P(I)=\frac{\#\{J\in P:\ c(J)<c(I)\}}{|P|-1},\qquad \mathit{dc}_P(I)=\frac{\#\{J\in P:\ \Delta_P(I)<\Delta_P(J)\}}{|P|-1},$$

so that the best individual has rank $0$ and the worst rank $1$. For an integer parameter $\mathit{nbElit}$, the Biased Fitness is (equation (7))

$$BF_P(I)=\mathit{fit}_P(I)+\Bigl(1-\frac{\mathit{nbElit}}{|P|-1}\Bigr)\times \mathit{dc}_P(I).$$

An individual $I$ is a clone in $P$ if some other $J\in P$ has $\delta(J,I)=0$ or $c(J)=c(I)$. With $\mathit{best}$ the current best solution, $X(P)$ is the set of individuals of $P$, other than $\mathit{best}$, that have a clone.

Survivor selection. When a subpopulation reaches $\mu+\lambda$ individuals, $\lambda$ of them are discarded one at a time: if $X\neq\emptyset$, an individual of maximum $BF$ in $X$ is removed; otherwise an individual of maximum $BF$ in the whole population. After each removal the distances, $X$, the ranks and $BF$ are recomputed on the remaining population. An individual is among the $\mathit{nbElit}$ best of $P$ in terms of fitness when fewer than $\mathit{nbElit}$ members of $P$ have strictly smaller cost.

Formalization targets

Goal: Section 4.6, Proposition

For every run of the survivor-selection procedure that removes $\lambda$ individuals from $P$ and ends at $P'$, with $\mathit{nbElit}+\lambda\le|P|$:

$$J\in P,\quad J\notin X(P),\quad \#\{K\in P: c(K)<c(J)\}<\mathit{nbElit}\ \Longrightarrow\ J\in P'.$$

Milestones: the three sentences of the proof (p. 17)

1. If $X(P)=\emptyset$, the individual $W$ with the worst fitness has $\mathit{fit}_P(W)=1$ and $BF_P(W)\ge 1$.
2. An individual $J$ among the $\mathit{nbElit}$ best has

$$BF_P(J)\le\frac{\mathit{nbElit}-1}{|P|-1}+1-\frac{\mathit{nbElit}}{|P|-1}<1.$$

3. One removal step does not remove an individual $J\notin X(P)$ among the $\mathit{nbElit}$ best.

Significance

The result. The Proposition explains what the parameter $\mathit{nbElit}$ means: it is the number of top individuals whose survival is guaranteed from one generation to the next, whatever their diversity contribution. It lets the algorithm designer push for diversity through $BF$ without risking the loss of the best solutions, and it is what makes the "removal zone" $BF\ge 1$ of the paper's Figure 4 a meaningful picture. The same Biased Fitness and survivor rule are reused in later HGS variants, so the guarantee transfers to them.

Formalizing it. The proof in the paper is three sentences long, but it leaves several things implicit: what happens with ties in cost or diversity, why "the" worst individual has rank exactly $1$, why the coefficient of $\mathit{dc}$ is nonnegative, and why the one-step argument survives $\lambda$ successive removals with everything recomputed. A machine-checked version settles each of these. To our knowledge no formalization of this or any other population-management guarantee for genetic algorithms exists.

Difficulty

The arithmetic of each step is elementary. The difficulty is in reading the statement correctly. "The individual with the worst fitness has rank 1" fails when costs tie; it holds only in the branch $X=\emptyset$, where equal costs are excluded because two individuals with equal cost are both clones and at most one of them is the best solution. The inequality $BF\ge 1$ needs $\mathit{nbElit}\le|P|-1$, which the Proposition does not state: it follows from the population sizes ($\mu+\lambda$ reduced to $\mu$, with $\mathit{nbElit}=el\times\mu$, $el\in[0,1]$, Table 1). Without it the Proposition is false: if $\mathit{nbElit}\ge|P|$ and $X=\emptyset$, some elite individual must be removed. Finally, the one-step argument must be iterated: the population, its ranks and $X$ change after each removal, and one must check that the hypotheses on $J$ persist.

Formalization scope

Individuals are elements of an arbitrary type $\alpha$ with decidable equality; populations are Finset α. Costs, distances and diversity contributions are real-valued, and $\Delta$ is an arbitrary function of (population, individual), which includes the paper's equation (5); the goal is therefore stated for every diversity measure. Explicit readings of loose phrases:

• "normalized ranks … where the best individual has rank 0 and the worst has rank 1": the number of strictly better individuals divided by $|P|-1$, in $\mathbb R$ (competition ranking; tied individuals share the better rank);
• "the nbElit best individuals … in terms of fitness": fewer than $\mathit{nbElit}$ members with strictly smaller cost;
• "Update the distance measures and X, and repeat": $X$, ranks and $BF$ are recomputed on the current population at each of the $\lambda$ steps;
• ties in "maximum Biased Fitness" are broken arbitrarily, and the goal quantifies over every run;
• the population-size condition $\mathit{nbElit}+\lambda\le|P|$ is an explicit hypothesis, taken from Section 4.6 and Table 1;
• the best solution $\mathit{best}$ is a parameter, not required to lie in $P$ (for the infeasible subpopulation it is the incumbent feasible solution); $J$ may itself be $\mathit{best}$.

A formalization that freezes the initial Biased Fitness, that takes the ranks as arbitrary functions into $[0,1]$, that states the existence of one good run, or whose size hypothesis cannot be met, would not be this Proposition. The supporting definition file contains the ranks, the Biased Fitness, clones, $X$, a removal step and a run of $\lambda$ steps; no further library is needed beyond Finset cardinalities. Proofs of the three milestones and of the goal are welcome, as is a formalization of the paper's Hamming distance (6) and diversity contribution (5) as an instance of $\Delta$.

Selected references

• T. Vidal, T. G. Crainic, M. Gendreau, N. Lahrichi, W. Rei, A Hybrid Genetic Algorithm for Multi-Depot and Periodic Vehicle Routing Problems, technical report CIRRELT-2010-34, July 2010. https://www.cirrelt.ca/documentstravail/cirrelt-2010-34.pdf (the version cited throughout; Section 4.6, pp. 16–17).
• T. Vidal, T. G. Crainic, M. Gendreau, N. Lahrichi, W. Rei, A Hybrid Genetic Algorithm for Multidepot and Periodic Vehicle Routing Problems, Operations Research 60(3):611–624, 2012. https://doi.org/10.1287/opre.1120.1048
• C. Prins, A simple and effective evolutionary algorithm for the vehicle routing problem, Computers & Operations Research 31(12):1985–2002, 2004. https://doi.org/10.1016/S0305-0548(03)00158-8
• K. Sörensen, M. Sevaux, MA|PM: memetic algorithms with population management, Computers & Operations Research 33(5):1214–1225, 2006. https://doi.org/10.1016/j.cor.2004.09.011

Motivation

Single-leg capacity allocation under customer choice is the basic dynamic problem of revenue management: a firm holds a fixed stock of a perishable resource (seats on a flight leg, rooms on a night), and in every period of a finite selling horizon it decides which products (fare classes) to offer to the arriving customer. Talluri and van Ryzin (Management Science, 2004) showed that under a multinomial logit (MNL) choice model with known parameters, the optimal assortment in every period is revenue-ordered and shrinks as capacity becomes scarcer ("nesting by fare order"), which is what justifies the protection levels and bid prices used in practice.

The MNL parameters are estimated from data and are never known exactly. Rusmevichientong and Topaloglu (Operations Research, 2012) study the robust version, in which an adversary picks the parameters of each period from an uncertainty set after seeing the offered assortment, following the robust Markov decision process framework of Iyengar (Mathematics of Operations Research, 2005). Their Section 4 shows that the structure of the known-parameter problem survives: the value function is concave in capacity, the optimal assortment is a revenue threshold set, and it grows with remaining capacity and, when uncertainty does not shrink, over time. This mission formalizes those results.

Setting

There are $n$ products $\mathcal A = \{1,\dots,n\}$ with revenues $r_1,\dots,r_n$. An MNL parameter vector is $v = (v_0, v_1, \dots, v_n) \in \mathbb R^{n+1}_{++}$; offered the assortment $S \subseteq \mathcal A$, a customer buys product $i \in S$ with probability

$$\phi_i(S,v) = \frac{v_i}{v_0 + \sum_{\ell\in S} v_\ell},$$

and nothing with probability $1 - \sum_{i\in S}\phi_i(S,v)$. The expected revenue is $f(S,v) = \sum_{i\in S} r_i \phi_i(S,v)$.

Static problem (Section 3). For a compact nonempty uncertainty set $\mathcal V \subseteq \mathbb R^{n+1}_{++}$,

$$Z^*(\mathcal V) = \max_{S\subseteq\mathcal A}\ \min_{v\in\mathcal V} f(S,v),$$

and $S^*(\mathcal V)$ is an optimal assortment of smallest cardinality.

Dynamic problem (Section 4). Periods $t = 1,\dots,T$ each bring one customer, whose parameter vector lies in a compact nonempty $\mathcal V_t \subseteq \mathbb R^{n+1}_{++}$. A purchase consumes one unit of capacity. The value function $J_t(x)$, the maximum worst-case revenue from period $t$ on with $x$ units of capacity, satisfies

$$J_t(x) = \max_{S_t\subseteq\mathcal A}\ \min_{v_t\in\mathcal V_t}\Big\{\sum_{i\in S_t}\phi_i(S_t,v_t)\big(r_i + J_{t+1}(x-1)\big) + \Big(1-\sum_{i\in S_t}\phi_i(S_t,v_t)\Big)J_{t+1}(x)\Big\}$$

for $x \ge 1$, with $J_t(0) = 0$ and $J_{T+1} \equiv 0$. The marginal value of capacity is $\Delta J_t(x) = J_t(x) - J_t(x-1)$, and $S^*_t(x)$ is a maximizer of the right-hand side of smallest cardinality.

Formalization targets

Goal: Theorem 4.3 (p. 17)

For every $1 \le t \le T$ and $x \ge 1$, and, in the second part, every $1 \le t \le T-1$ with $\mathcal V_t \subseteq \mathcal V_{t+1}$:

$$S^*_t(x) \subseteq S^*_t(x+1), \qquad \mathcal V_t \subseteq \mathcal V_{t+1} \implies S^*_t(x) \subseteq S^*_{t+1}(x).$$

Milestones

1. (Dynamic Robust), second line (p. 16): $J_t(x) = \max_{S}\min_{v\in\mathcal V_t}\sum_{i\in S}\phi_i(S,v)\,(r_i - \Delta J_{t+1}(x)) + J_{t+1}(x)$.
2. Proof of Theorem 4.2 (pp. 16–17): $S^*_t(x)$ is the static $S^*(\mathcal V_t)$ for revenues $r_i - \Delta J_{t+1}(x)$, and $J_t(x) - J_{t+1}(x)$ is the corresponding $Z^*(\mathcal V_t)$.
3. Theorem 3.2 (p. 7): $S^*(\mathcal V) = \{i : r_i > Z^*(\mathcal V)\}$.
4. Theorem 3.7 (p. 10): for $\delta \ge 0$, $S^*(\mathcal V)$ is contained in the robust assortment for revenues $r + \delta$.
5. Corollary 3.5 (p. 9): $\mathcal V \subseteq \mathcal V' \implies Z^*(\mathcal V') \le Z^*(\mathcal V)$ and $S^*(\mathcal V) \subseteq S^*(\mathcal V')$.
6. Theorem 4.1, first inequality (p. 16): $\Delta J_t(x+1) \le \Delta J_t(x)$.
7. Theorem 4.1, second inequality (p. 16): $\Delta J_{t+1}(x) \le \Delta J_t(x)$.
8. Theorem 4.2 (p. 16): $S^*_t(x) = \{i : r_i > J_t(x) - J_{t+1}(x-1)\}$.

Significance

The result. Theorems 4.1–4.3 say that robustness costs nothing structurally: the robust policy is still a nested threshold policy, so it can be implemented with the protection levels or bid-price controls already in use, and it can be computed by examining at most $n$ revenue-ordered assortments per state instead of $2^n$. Theorem 4.3 gives the operational content: with less inventory, offer fewer, higher-revenue products; nearer the end of the season (when the uncertainty sets are nested), offer more.

Formalizing it. The results are proved in the paper; none of them has a machine-checked proof. A formalization produces a checked robust finite-horizon dynamic program over finite action sets with compact adversary sets, the reduction of each Bellman step to a static max–min problem with shifted revenues, and checked concavity and time-monotonicity arguments that are reusable for other single-resource problems. The known-parameter analogues for general regular choice models and for the Markov chain choice model are separate drafts on the platform (RevenueOrdered.Nesting.*, MarkovChainChoice.SingleResource.*); they have no uncertainty set and are not used here.

Difficulty

The obvious route to concavity, an induction on $t$ in which $J_t$ is a maximum of concave functions, fails: a maximum of concave functions is not concave, and here each candidate assortment is evaluated by a minimum over $\mathcal V_t$, and the worst-case parameter vector changes with the capacity level, so the known-parameter argument cannot be reused term by term. Any induction on $t$ also has to handle the boundary $x = 0$, where the Bellman equation does not apply and only $J_t(0) = 0$ is given. Every step involving a minimum must use that the minimum over a compact set is attained, and translating a minimum by a constant must be justified rather than assumed.

Formalization scope

• Representation. Products are Fin n (Lean index $i$ is product $i+1$). A parameter vector is p : ℝ × (Fin n → ℝ) with p.1 $= v_0$. $f(S,v)$ is the published ChoiceCDLP.MNL.mnlObjective. Minima over uncertainty sets are real infima (sInf), equal to the attained minima under the standing hypotheses; maxima are Finset.sup' over all $2^n$ assortments.
• Standing assumptions. Every V t, $1 \le t \le T$, is compact, nonempty and contained in $\mathbb R^{n+1}_{++}$ (IsUncertaintySeq); the static results assume the same of V. The paper writes "$\mathcal V \subset \mathbb R^n_{++}$" in Theorem 3.2 and Corollary 3.5; this is read as $\mathbb R^{n+1}_{++}$, compact.
• Revenues are arbitrary reals. The paper orders $r_1 \ge \dots \ge r_n > 0$ "without loss of generality"; no proof uses it, and the dynamic reduction applies Theorem 3.2 to $r_i - \Delta J_{t+1}(x)$, which may be negative. Dropping it strengthens every statement.
• The value function is defined by the recursion. The max–min policy formulation (p. 15) and Iyengar's theorem that it satisfies the Bellman equation are not formalized. $J_t(x)$ is defined for every $x \in \mathbb N$; the initial capacity $C$ never enters the recursion, so the paper's $J_t$ on $\{0,\dots,C\}$ is the restriction.
• Capacity $x \ge 1$. Theorem 4.1 is printed "for any $x \in \{0,1,\dots,C\}$", which includes the undefined $\Delta J_t(0)$; Theorems 4.2 and 4.3 say "for any $x$", but $S^*_t(0)$ is not defined by the Bellman equation. All statements assume $x \ge 1$.
• Tie-break. $S^*(\mathcal V)$ and $S^*_t(x)$ are predicates ("$S$ is an optimal assortment of smallest cardinality"), not choice functions; Theorems 3.2 and 4.2 are stated as "↔ $S$ is the threshold set", which also asserts the threshold set is optimal. Without the tie-break Theorems 4.2 and 4.3 are false, since a product with revenue exactly at the threshold can be added.
• Ruled out. Defining $J$ as a maximum over revenue-ordered assortments, or through the threshold formula, would make Theorem 4.2 definitional; $J$ is defined with the minimum inside a maximum over all subsets.
• Restatements. Theorems 3.2, 3.7 and Corollary 3.5 restate, in RobustMNL.Dynamic, the companion mission on Section 3 of the same paper, identically up to namespace.
• Source. The source is the authors' manuscript of 20 September 2011 of the Operations Research 2012 article; its printed page numbers equal the PDF's.
• Welcome contributions. Lemmas on attained minima of continuous functions on compact sets of positive parameter vectors, the translation of a max–min by a constant, and the bound $\sum_{i\in S}\phi_i(S,v) \le 1$ are reusable across all three missions of this paper.

Selected references

• P. Rusmevichientong, H. Topaloglu, Robust Assortment Optimization in Revenue Management Under the Multinomial Logit Choice Model, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1063
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2), 2005. https://doi.org/10.1287/moor.1040.0129

Motivation

Assortment optimization is the problem a retailer faces in deciding which subset of its products to put in front of customers. Under the multinomial logit (MNL) choice model each product carries a preference weight, and a customer facing an offered set buys each product with probability proportional to its weight, or buys nothing. The optimal assortment under known weights is classical: it is one of the revenue-ordered sets (Talluri and van Ryzin, 2004). In practice the weights are estimated from data and are uncertain.

Rusmevichientong and Topaloglu (2012) study a robust version: the seller knows only that the weights lie in an uncertainty set, and maximizes the worst-case expected revenue over that set. They also treat the case where the offered set is limited in size, as when a display window or a web page holds only a fixed number of items. Under known weights the size-constrained MNL problem is solvable in polynomial time (Rusmevichientong, Shen and Shmoys, 2010); for a general uncertainty set the robust size-constrained problem has no comparable structure. This mission formalizes the result showing that, for a rectangular uncertainty set, the robust size-constrained problem is exactly a known-weights problem at an explicit parameter vector.

Setting

There are $n$ products $\mathcal A=\{1,\dots,n\}$ with revenues $r_1,\dots,r_n$. A parameter vector $v=(v_0,v_1,\dots,v_n)\in\mathbb R^{n+1}_{++}$ gives the no-purchase weight $v_0$ and the preference weight $v_i$ of each product. When the seller offers an assortment $S\subseteq\mathcal A$, a customer buys product $i\in S$ with probability $v_i/(v_0+\sum_{\ell\in S}v_\ell)$, and the expected revenue is

$$f(S,v)=\frac{\sum_{i\in S} r_i v_i}{v_0+\sum_{i\in S} v_i}.$$

An uncertainty set $\mathcal V\subseteq\mathbb R^{n+1}_{++}$ is a compact set of parameter vectors. The worst-case revenue of $S$ is $\min_{v\in\mathcal V} f(S,v)$. For a size limit $K\in\mathbb N$, the size-constrained robust problem is

$$Y^*(\mathcal V)=\max_{S\subseteq\mathcal A:\ |S|\le K}\ \min_{v\in\mathcal V} f(S,v),$$

and with no size limit its value is $Z^*(\mathcal V)=\max_{S\subseteq\mathcal A}\min_{v\in\mathcal V} f(S,v)$. A rectangular uncertainty set is a product of intervals

$$\mathcal V=\prod_{i=0}^n [l_i,u_i],\qquad 0<l_i\le u_i ,$$

in which each weight, including the no-purchase weight $v_0\in[l_0,u_0]$, varies independently over its own range.

Formalization targets

Goal: Theorem 3.8 (p. 11)

For every rectangular $\mathcal V=\prod_{i=0}^n[l_i,u_i]\subseteq\mathbb R^{n+1}_{++}$, every vector of revenues and every $K\in\mathbb N$,

$$Y^*(\mathcal V)=\max_{S\subseteq\mathcal A:\ |S|\le K}\ \frac{\sum_{i\in S} l_i r_i}{u_0+\sum_{i\in S} l_i} =\max_{S\subseteq\mathcal A:\ |S|\le K} f\big(S,(u_0,l_1,\dots,l_n)\big).$$

Milestones (proof of Theorem 3.8, p. 12)

1. Parametric form of $Y^*$, for every compact nonempty $\mathcal V\subseteq\mathbb R^{n+1}_{++}$:

$$Y^*(\mathcal V)=\max\Big\{\lambda:\ \max_{S:\,|S|\le K}\ \min_{v\in\mathcal V}\ \frac{1}{v_0}\sum_{i\in S}v_i(r_i-\lambda)\ge\lambda\Big\}.$$

2. Rectangular reduction, for every real $\lambda$:

$$\max_{S:\,|S|\le K}\ \min_{v\in\mathcal V}\ \frac{1}{v_0}\sum_{i\in S}v_i(r_i-\lambda)=\max_{S:\,|S|\le K}\ \frac{1}{u_0}\sum_{i\in S}l_i(r_i-\lambda).$$

3. Parametric form at known weights:

$$\max_{S:\,|S|\le K} f\big(S,(u_0,l_1,\dots,l_n)\big)=\max\Big\{\lambda:\ \max_{S:\,|S|\le K}\ \frac{1}{u_0}\sum_{i\in S}l_i(r_i-\lambda)\ge\lambda\Big\}.$$

Further result (Example 3.4, p. 8)

The unconstrained case: $Z^*(\mathcal V)=\max_{S\subseteq\mathcal A} f\big(S,(u_0,l_1,\dots,l_n)\big)$ for rectangular $\mathcal V$, which the paper establishes by a separate argument.

Significance

The result. Theorem 3.8 converts a max–min problem over a continuum of parameter vectors into a single deterministic size-constrained MNL problem with weights $(u_0,l_1,\dots,l_n)$: the largest no-purchase weight and the smallest product weights. The size-constrained MNL problem with known weights has efficient algorithms, so the robust problem inherits them. The theorem also identifies the worst-case customer explicitly, which means robustness against a box costs nothing computationally beyond a known-weights solve. The parametric description of $Y^*$ in Milestone 1 holds for every compact uncertainty set and is the starting point for other uncertainty sets.

Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission produces a Lean formalization of the size-constrained robust MNL problem built on the published MNL objective ChoiceCDLP.MNL.mnlObjective, the parametric (Dinkelbach-type) characterization of a max–min ratio problem with attainment, and the box reduction. The definitions are shared in convention with the companion missions on the same paper (the revenue-ordered structure of the unconstrained robust problem and the dynamic robust problem).

Difficulty

The direct approach — for each assortment $S$, find the worst parameter vector in the box and compare — does not work as stated: for a fixed $S$ containing a product whose revenue is below the target ratio, the minimizing no-purchase weight is $l_0$, not $u_0$, so the per-assortment worst case is not attained at $(u_0,l_1,\dots,l_n)$. The identity holds only after maximizing over assortments of size at most $K$, and the size constraint interacts with which products can be discarded. A second point is that the ratio $f(S,v)$ is not linear in $v$, so its minimum over the box is not determined coordinate by coordinate from the signs of the revenues alone, and every "max" in the statements asserts attainment, which has to be established, not assumed.

Formalization scope

The source is the authors' manuscript of 20 Sep 2011 of the Operations Research 2012 article; its printed page numbers equal the PDF's.

Representation. Products are Fin n (Lean index $i$ is the paper's product $i+1$). A parameter vector is p : ℝ × (Fin n → ℝ) with p.1 $=v_0$. The revenue $f(S,v)$ is the published ChoiceCDLP.MNL.mnlObjective p.2 r p.1 S. Every minimum over $\mathcal V$ is a real sInf of the image; every maximum over assortments is a Finset.sup' over all subsets of size at most $K$ (a nonempty family, since it contains $\emptyset$). Every "$\max\{\lambda:\dots\}$" is stated as IsGreatest, which asserts attainment. The rectangular set is Set.Icc l₀ u₀ ×ˢ Set.Icc l u. $K$ is any natural number, with no lower or upper bound.

Hypotheses.

• Milestone 1 assumes the paper's standing assumption: $\mathcal V$ compact, nonempty, and inside $\mathbb R^{n+1}_{++}$. Nonemptiness is implicit in the paper's $\min_{v\in\mathcal V}$.
• The box results assume $0<l_0$, $0<l_i$ (the paper's $[l_i,u_i]\subset\mathbb R_{++}$) and $l_0\le u_0$, $l_i\le u_i$, the reading of "the interval $[l_i,u_i]$ represents the range of the likely values"; without them the box would be empty.
• Revenues are arbitrary reals. The paper's ordering $r_1\ge\dots\ge r_n>0$ (p. 5, "without loss of generality") is used by no proof and is dropped; the statements are strengthened accordingly.
• The paper writes "$\mathcal V\subset\mathbb R^{n+1}_{++}$"; it is read as inclusion.
• Example 3.4's chain ends with $f(S^*_h,h)$, which equals $\max_S f(S,h)$ by definition of $S^*_h$; the Lean statement keeps the first equality.

Trivializations ruled out. $Y^*$ is defined through the worst case over the whole box and the maximum over all assortments of size at most $K$, never through the vertex $(u_0,l_1,\dots,l_n)$ or a restricted family of sets, so the goal is not definitional. The box hypotheses make $\mathcal V$ nonempty, so no sInf is evaluated on an empty set.

Contributions welcome. Proofs of the four milestones and the goal; lemmas on attainment of sInf of a continuous function over a compact set used for the inner minimum; a reusable parametric characterization of $\max_S \min_v$ of ratios with positive denominators.

Selected references

• P. Rusmevichientong, H. Topaloglu, Robust Assortment Optimization in Revenue Management Under the Multinomial Logit Choice Model, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1063
• P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic Assortment Optimization with a Multinomial Logit Choice Model and Capacity Constraint, Operations Research 58(6), 2010. https://doi.org/10.1287/opre.1090.0800
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• W. Dinkelbach, On Nonlinear Fractional Programming, Management Science 13(7), 1967. https://doi.org/10.1287/mnsc.13.7.492

Motivation

Assortment optimization asks which subset of products a firm should offer when customers choose among the offered products, or leave without buying. It underlies shelf-space planning in retail, the choice of which fare classes to keep open in airline revenue management, and the selection of items shown on a web page. The multinomial logit (MNL) model is the standard choice model in this literature: when the model parameters are known, the optimal assortment is revenue-ordered, that is, it consists of the products with the highest revenues (Talluri and van Ryzin, 2004; Gallego et al., 2004; Liu and van Ryzin, 2008), so only $n$ candidate assortments need to be compared instead of $2^n$.

In practice the parameters of the choice model are estimated from limited data. Rusmevichientong and Topaloglu (Operations Research, 2012) take a robust view: the parameters are only known to lie in an uncertainty set, and the firm maximizes its worst-case expected revenue. Their main structural result is that the revenue-ordered structure survives this uncertainty, whatever the uncertainty set. This mission formalizes that result and the comparative statics the paper derives from it.

Setting

There are $n$ products, $\mathcal A = \{1, \dots, n\}$, and product $i$ earns revenue $r_i$. A customer's choice is governed by a parameter vector $v = (v_0, v_1, \dots, v_n) \in \mathbb R^{n+1}_{++}$ (all components strictly positive): $v_0$ is the weight of the no-purchase option and $v_i$ the preference weight of product $i$. When the assortment $S \subseteq \mathcal A$ is offered, the customer buys product $i \in S$ with probability

$$\phi_i(S, v) = \frac{v_i}{v_0 + \sum_{\ell \in S} v_\ell},$$

and buys nothing with the remaining probability. The expected revenue of $S$ is

$$f(S, v) = \sum_{i\in S} r_i\,\phi_i(S, v) = \frac{\sum_{i\in S} r_i v_i}{v_0 + \sum_{i\in S} v_i}.$$

The parameters are unknown and lie in an uncertainty set $\mathcal V \subseteq \mathbb R^{n+1}_{++}$, which is compact and nonempty. The Robust Logit problem maximizes the worst-case expected revenue:

$$Z^*(\mathcal V) = \max_{S \subseteq \mathcal A}\ \min_{v \in \mathcal V} f(S, v).$$

Among the optimal assortments, $S^*(\mathcal V)$ is one with the smallest cardinality. For a single parameter vector $v$, write $S^*_v = S^*(\{v\})$ and $Z^*_v = Z^*(\{v\})$; this is the classical problem with known parameters. Finally, for $\delta \ge 0$, $Z^*_\delta(\mathcal V)$ and $S^*_\delta(\mathcal V)$ are the same quantities when every revenue $r_i$ is replaced by $r_i + \delta$.

Formalization targets

Goal: Theorem 3.2 (revenue-ordered assortments are robust)

$$S^*(\mathcal V) = \{\, i \in \mathcal A : r_i > Z^*(\mathcal V) \,\}.$$

Equivalently: an assortment is optimal with smallest cardinality if and only if it is the set of products whose revenue strictly exceeds the optimal worst-case revenue. When $r_1 \ge \dots \ge r_n$ this set is $\{1, \dots, i\}$ for some $i$.

Milestones

1. The identity in the proof of Lemma 3.1 (p. 6): for $i \notin A$, $f(A\cup\{i\}, v)$ is the convex combination of $r_i$ and $f(A, v)$ with weights $v_i/(v_0+v_i+\sum_{\ell\in A}v_\ell)$ and $(v_0+\sum_{\ell\in A}v_\ell)/(v_0+v_i+\sum_{\ell\in A}v_\ell)$.
2. Lemma 3.1 (p. 6): for $i \notin A$, the statements $r_i > f(A,v)$, $f(A\cup\{i\},v) > f(A,v)$ and $r_i > f(A\cup\{i\},v)$ are equivalent.
3. Corollary 3.5 (p. 9): if $\mathcal V \subseteq \mathcal V'$, then $Z^*(\mathcal V') \le Z^*(\mathcal V)$ and $S^*(\mathcal V) \subseteq S^*(\mathcal V')$.
4. Theorem 3.6 (p. 10): $S^*(\mathcal V) = \bigcup_{v\in\mathcal V} S^*_v$.
5. The sandwich in the proof of Theorem 3.7 (p. 11): $Z^*(\mathcal V) \le Z^*_\delta(\mathcal V) \le \delta + Z^*(\mathcal V)$ for $\delta \ge 0$.
6. Theorem 3.7 (p. 10): $S^*(\mathcal V) \subseteq S^*_\delta(\mathcal V)$ for $\delta \ge 0$.

Milestones 3–6 are consequences of the goal on the same definitions.

Significance

Theorem 3.2 reduces the robust problem, a max–min over $2^n$ assortments and a possibly infinite parameter set, to at most $n+1$ revenue-ordered candidates, each requiring one worst-case evaluation $\min_{v\in\mathcal V} f(S, v)$. Applied to a singleton $\mathcal V = \{v\}$ it also reproves the classical revenue-ordered optimality under known MNL parameters, together with the exact tie-breaking description. Corollary 3.5 and Theorem 3.6 say that more uncertainty calls for a larger assortment, and that the robust assortment is the largest assortment optimal for some parameter in $\mathcal V$; Theorem 3.7 compares assortments when all revenues shift by a constant, which the paper uses in Section 4 to show that robust dynamic assortments grow with remaining capacity and over time.

The results are proved in the paper; none of them has a machine-checked proof on Prove2Me. The platform has ChoiceCDLP.MNL.top_ranked_optimal (from Liu and van Ryzin, 2008), a statement about top-ranked offer sets for known MNL weights, which is a different statement without uncertainty or tie-breaking. A formal development here gives a checked version of the robust structure theorem stated for arbitrary real revenues, the generality in which the dynamic part of the paper uses it.

Difficulty

The obvious argument fails at the max–min. For known parameters, Lemma 3.1 immediately shows that a product should be added exactly when its revenue beats the current expected revenue; but under uncertainty the minimizing parameter vector changes with the assortment, so one cannot compare $f(S, v)$ and $f(S \cup \{i\}, v)$ at a single worst-case $v$. The argument has to establish a strict improvement uniformly over $\mathcal V$ and then pass to the minimum, which is where compactness enters: a pointwise strict inequality survives the minimum only because it is attained. The tie-breaking rule is equally essential: a product with $r_i = Z^*(\mathcal V)$ can be added to an optimal assortment without changing its worst-case value, so without the smallest-cardinality rule the characterization is false.

Formalization scope

Products are Fin n, so Lean index $i$ stands for the paper's product $i+1$. A parameter vector is p : ℝ × (Fin n → ℝ) with p.1 $= v_0$ and p.2 i the weight of product $i$; IsPos p expresses $v \in \mathbb R^{n+1}_{++}$. The expected revenue $f(S, v)$ is the published definition ChoiceCDLP.MNL.mnlObjective. The worst case $\min_{v\in\mathcal V} f(S,v)$ is a real infimum (sInf), and $Z^*(\mathcal V)$ is a maximum over all subsets of products. $S^*(\mathcal V)$ is encoded as the predicate IsSmallestOptimal V r S (optimal, and of cardinality at most that of every optimal assortment), not as a choice function, so every statement about $S^*(\mathcal V)$ is asserted for every optimal assortment of smallest cardinality. $Z^*_\delta$ and $S^*_\delta$ are the same objects for the revenue vector $r + \delta$, which is exact since $\sum_{i\in S}(r_i+\delta)\phi_i(S,v)$ is $f(S,v)$ at those revenues.

Standing assumptions and departures from the page:

• Every theorem assumes $\mathcal V$ compact, nonempty and contained in $\mathbb R^{n+1}_{++}$, the standing assumption of Sec. 3 (p. 6). Theorem 3.2, Corollary 3.5 and Theorem 3.6 write "$\mathcal V \subset \mathbb R^n_{++}$"; this is read as the compact $\mathcal V \subseteq \mathbb R^{n+1}_{++}$ of p. 6, since the parameter vector has $n+1$ components and the proofs use compactness.
• Revenues are arbitrary real numbers. The paper's ordering $r_1 \ge \dots \ge r_n > 0$ (p. 5, "without loss of generality") is used by none of the proofs, and Sec. 4 applies Theorem 3.2 to revenues that may be negative. This is a strengthening.
• The goal is stated as an equivalence: an assortment is optimal of smallest cardinality iff it equals $\{i : r_i > Z^*(\mathcal V)\}$. The backward direction asserts that the threshold set is optimal, so the statement cannot hold vacuously. Defining $Z^*$ as a maximum over revenue-ordered prefixes only, or defining $S^*(\mathcal V)$ through the threshold, would make the goal true by definition; both are ruled out by the definitions above.

The infimum is meaningful only under the standing assumptions (on an empty set it is $0$), which is why they appear as hypotheses of every statement. A complete development needs continuity of $v \mapsto f(S,v)$ on positive vectors and attainment of minima on compact sets, both available in Mathlib, and finite maxima over Finset (Finset (Fin n)). The lemmas about $f$ (milestones 1–2) are reusable for any MNL model. Proofs of any milestone, and alternative proofs of the goal, are welcome.

The source is the authors' manuscript of 20 Sep 2011 of the Operations Research 2012 article; its printed page numbers equal the PDF's page numbers, and all page citations refer to it.

Selected references

• P. Rusmevichientong, H. Topaloglu, Robust Assortment Optimization in Revenue Management Under the Multinomial Logit Choice Model, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1063
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2), 2008. https://doi.org/10.1287/msom.1070.0172
• G. Gallego, G. Iyengar, R. Phillips, A. Dubey, Managing Flexible Products on a Network, CORC Technical Report TR-2004-01, Columbia University, 2004.

Motivation

MAX-2SAT asks for an assignment of Boolean variables that maximizes the total weight of satisfied clauses, each clause being a disjunction of two literals. It is one of the basic constraint satisfaction problems of approximation theory, and its approximability has been studied alongside MAX-CUT since semidefinite programming entered the field.

Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 37(1), 2007) show that, assuming the Unique Games Conjecture, it is NP-hard to approximate MAX-2SAT within any factor greater than

$$\beta = \min_{\pi/2 \le \theta \le \pi} \frac{2 + (2/\pi)\theta}{3 - \cos\theta} \approx 0.943$$

(their Theorem 3), and that their reduction produces balanced instances, in which every variable carries as much weight positively as negatively. Their Theorem 4 shows that for this balanced restriction the bound is tight: a Goemans–Williamson style semidefinite relaxation followed by random-hyperplane rounding approximates Balanced-MAX-2SAT within any factor smaller than $\beta$. This mission formalizes Theorem 4.

Timeline.

• 1995: Goemans and Williamson give the 0.878 algorithm for MAX-CUT and a 0.878 algorithm for MAX-2SAT by semidefinite programming and random-hyperplane rounding (J. ACM 42(6)).
• 2007: Khot, Kindler, Mossel and O'Donnell prove UGC-hardness at $\beta$ for MAX-2SAT, and show $\beta$ is achievable for balanced instances (Theorem 4).
• 2007: Austrin shows that, under the Unique Games Conjecture, general MAX-2SAT is hard to approximate beyond about 0.9401, strictly below $\beta$, so balanced instances are not the hardest ones (STOC 2007); for the balanced version $\beta$ remains the threshold.

Setting

Treat the bit TRUE as $-1$ and FALSE as $1$ (the paper's §7.2 convention). An assignment of the variables $x_0,\dots,x_{n-1}$ is a point $x \in \{-1,1\}^n$. A literal is $y = r_i x_i$ with a sign $r_i \in \{-1,1\}$ ($r_i = -1$ for the negated variable $\neg x_i$); it is true when $y = -1$. A weighted MAX-2SAT instance is a finite list of clauses $C = (y \vee z)$ with $y = r_ix_i$, $z = r_jx_j$ (the two variables may coincide), with nonnegative weights $w_C$. The satisfied weight of $x$ is

$$\mathrm{sat}(x) = \sum_C w_C\,[\,y = -1 \text{ or } z = -1\,], \qquad \mathrm{OPT} = \max_{x\in\{-1,1\}^n} \mathrm{sat}(x).$$

An instance is balanced (Definition 12) if for each variable $i$, the expected satisfied weight when $x_i = 1$ and the other variables are uniform equals the expected satisfied weight when $x_i = -1$ and the others are uniform.

The semidefinite relaxation replaces each $x_i$ by a unit vector $v_i \in \mathbb R^d$ and the balanced objective by

$$\mathrm{SDPobj}(v) = \sum_{C = (r_ix_i\vee r_jx_j)} w_C\Bigl(\tfrac34 - \tfrac14\,(r_iv_i)\cdot(r_jv_j)\Bigr),$$

with optimal value $\mathrm{SDP} = \sup \mathrm{SDPobj}(v)$ over unit-vector families in every dimension. Hyperplane rounding draws a standard Gaussian vector $g \in \mathbb R^d$ and sets $x_i = \operatorname{sgn}(g\cdot v_i)$.

Formalization targets

Goal: Theorem 4 (p. 12), as the guarantee of the algorithm

For every balanced instance with nonnegative weights, every $\varepsilon \ge 0$, every unit-vector family $v$ with $\mathrm{SDPobj}(v) \ge \mathrm{SDP} - \varepsilon$, and every standard Gaussian vector $g$,

$$\mathbb E\bigl[\mathrm{sat}(\operatorname{sgn}(g\cdot v_i))_i\bigr] \;\ge\; \beta\,(\mathrm{OPT} - \varepsilon),$$

with the satisfied weight integrable. The constant is Theorem 3's exact minimum $\beta$, not its decimal rounding.

Milestones (proof of Theorem 4, pp. 21–22)

1. Arithmetization: $[\,y\vee z\,] = \tfrac34 - \tfrac14 y - \tfrac14 z - \tfrac14 yz$ on $\{-1,1\}^2$.
2. Balanced $\iff$ the linear terms cancel: $\mathrm{sat}(x) = \sum_C w_C(\tfrac34 - \tfrac14 yz)$ for all $x$.
3. Relaxation: $\mathrm{OPT} \le \mathrm{SDP}$ for balanced instances.
4. Hyperplane identity $\mathbb E[x_ix_j] = 1 - \tfrac2\pi\arccos(v_i\cdot v_j)$, already proved on the platform as Grothendieck's identity (in the equivalent form $\tfrac2\pi\arcsin$).
5. Per-clause bound: $\tfrac34 - \tfrac14(1 - \tfrac2\pi\arccos t) \ge \beta(\tfrac34 - \tfrac14 t)$ for all $t\in[-1,1]$.

Significance

The result. Together with Theorem 3, Theorem 4 pins the approximability of Balanced-MAX-2SAT at exactly $\beta$ under the Unique Games Conjecture: the constant arising from the Majority Is Stablest analysis of the hardness reduction coincides with the constant of a semidefinite rounding algorithm. It also explains why the hardness reduction for MAX-2SAT cannot give more than $\beta$ without abandoning balanced instances.

Formalizing it. The theorem is proved in the paper; no machine-checked proof is known to exist. A formal proof produces a verified approximation guarantee for a randomized rounding scheme that holds for every near-optimal vector solution, and a reusable layer for weighted 2-CSPs on $\{-1,1\}^n$: arithmetization, balancedness, the vector relaxation and its rounding. The hyperplane identity is already available on the platform, so the remaining work is combinatorial and analytic rather than probabilistic.

Difficulty

The naive approach, rounding the full arithmetized objective $\tfrac34 - \tfrac14 y - \tfrac14 z - \tfrac14 yz$, fails: the relaxation of a linear term $r_ix_i$ has no vector counterpart that random-hyperplane rounding treats correctly, and for unbalanced instances the achievable ratio is different. The whole argument rests on balancedness making the linear terms vanish identically, and the equivalence between Definition 12 (a statement about conditional expectations) and the cancellation of linear coefficients must be established with care, including clauses whose two literals involve the same variable.

The second difficulty is the constant. $\beta$ is defined as a minimum over $\theta\in[\pi/2,\pi]$ only, while the per-clause comparison is needed for all inner products $t\in[-1,1]$, that is for all $\theta\in[0,\pi]$. Showing that the ratio $\frac{2 + (2/\pi)\theta}{3-\cos\theta}$ does not drop below $\beta$ on $[0,\pi/2]$ is a genuine one-variable inequality, not a definitional unfolding. Finally, the expectation must be computed for a genuine Gaussian vector, with the sign convention at $0$ handled almost surely.

Formalization scope

• Assignments are Fin n → Bool read through pm true = -1, pm false = 1; a literal is (i, r) : Fin n × Bool with r = true for $\neg x_i$. The two literals of a clause may involve the same variable.
• An instance is a structure with m clauses, a clause map, and real weights with a nonnegativity field (Definition 10's "nonnegative weight function").
• Balancedness is Definition 12, stated as equality of the sums of satisfied weight over the two halves $\{x_i = 1\}$ and $\{x_i = -1\}$ of the cube; the common factor $2^{-(n-1)}$ is dropped.
• OPT is a maximum over the $2^n$ assignments. SDP is a real supremum over unit-vector families Fin n → Fin d → ℝ in every dimension $d$; the set is nonempty and bounded above by the total weight.
• beta is the infimum of the image of $[\pi/2,\pi]$, i.e. Theorem 3's attained minimum. Defining it over $[0,\pi]$ instead would make milestone 5 definitional and is ruled out.
• The Gaussian vector is the platform predicate IsStandardGaussianVector (measurable, independent coordinates of law $N(0,1)$ on an arbitrary probability space); the expectation is a Bochner integral and its integrability is part of the conclusion. The rounding outputs FALSE on the null event $g\cdot v_i = 0$.
• Not formalized: polynomial running time. The paper obtains an $(\mathrm{SDP}-\varepsilon)$-optimal solution in polynomial time by citing Goemans–Williamson; the goal quantifies over every such solution. "Within any factor smaller than $\beta$" follows by taking $\varepsilon$ small, because $\mathrm{OPT} \ge \tfrac12\sum_C w_C$.
• The goal cannot be met trivially: the vector family is universally quantified (not chosen inside the statement), the expectation is over a genuine Gaussian, and the instance ranges over all balanced weighted instances (a nontrivial balanced instance such as $(x_1\vee x_2)\wedge(\neg x_1\vee\neg x_2)$ exists).

Welcome contributions: proofs of the milestones, a bridge from Real.sign (used by the platform's Grothendieck identity) to the $\{-1,1\}$-valued rounding, and the one-variable analysis behind the per-clause bound.

Selected references

• S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal Inapproximability Results for MAX-CUT and Other 2-Variable CSPs?, SIAM J. Comput. 37(1), 2007. https://doi.org/10.1137/S0097539705447372
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42(6), 1995. https://doi.org/10.1145/227683.227684
• P. Austrin, Balanced Max 2-Sat might not be the hardest, STOC 2007. https://doi.org/10.1145/1250790.1250818
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018, Lemma 3.6.6 (Grothendieck's identity). https://doi.org/10.1017/9781108231596

Motivation

Risk-averse optimization replaces the expected cost $\mathbb E[X]$ of a random outcome by a risk function $\rho(X)$ that also penalizes dispersion: mean–deviation, mean–semideviation, conditional value-at-risk (CVaR) and their combinations are the standard examples in stochastic programming and portfolio selection. A decision maker who uses $\rho$ should not prefer an outcome that every risk-averse expected-utility maximizer rejects. For costs, the order that expresses this agreement among risk-averse agents is the increasing convex order: $X_2$ is worse than $X_1$ if $\mathbb E[u(X_2)]\ge\mathbb E[u(X_1)]$ for every increasing convex disutility $u$. It is the counterpart, for costs, of second-order stochastic dominance.

Whether a given mean–risk model is consistent with stochastic dominance was settled model by model: Ogryczak and Ruszczyński for mean–semideviation models (Eur. J. Oper. Res. 1999, Math. Program. 2001, SIAM J. Optim. 2002) and Pflug for CVaR (2000). Ruszczyński and Shapiro (Math. Oper. Res. 31, 2006) gave a single criterion, Theorem 5.1, which contains these results as special cases: among risk functions that depend only on the distribution of the outcome, consistency with the increasing convex order is equivalent to two structural properties, monotonicity and risk aversion.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $p\in[1,\infty)$. The space of outcomes is $\mathcal X=\mathcal L_p(\Omega,\mathcal F,P)$, the real random variables with $\mathbb E|X|^p<\infty$. An outcome is a cost: smaller is better. A risk function is a map $\rho:\mathcal X\to\mathbb R$.

• The cdf of $X$ is $F_X(t)=P(X\le t)$. $\rho$ is distribution invariant (Definition 5.2) if $F_{X_1}=F_{X_2}$ implies $\rho(X_1)=\rho(X_2)$.
• $\rho$ satisfies (A2) (monotonicity) if $X\le Y$ almost surely implies $\rho(X)\le\rho(Y)$.
• $\rho$ is risk averse (Definition 5.1) if for every $\sigma$-algebra $\mathcal G\subset\mathcal F$ and every $X\in\mathcal X$,

$$\rho(X)\ \ge\ \rho\big(\mathbb E[X\mid\mathcal G]\big),$$

for every version of the conditional expectation.

• For random variables $X_1,X_2$, the usual stochastic order $X_2\succeq_{\mathrm{st}}X_1$ holds if $\mathbb E[u(X_2)]\ge\mathbb E[u(X_1)]$ for every nondecreasing $u:\mathbb R\to\mathbb R$ for which both expectations exist; the increasing convex order $X_2\succeq_{\mathrm{icx}}X_1$ is the same with $u$ ranging over the increasing convex functions.
• $\rho$ is consistent with an order $\succeq$ if $X_2\succeq X_1$ implies $\rho(X_2)\ge\rho(X_1)$ for all $X_1,X_2\in\mathcal X$.

The paper places one more standing assumption on §5.2: the space is rich enough to carry a uniform random variable, a measurable $U:\Omega\to\mathbb R$ with $P(U\le t)=t$ for all $t\in[0,1]$.

In Lean these are IsUniformRV, cdfOf, cdfInv, DistInvariant, A2, RiskAverse, StLE, ConsistentSt and ConsistentIcx in the namespace ConvexRiskFn.Order; the increasing convex order is the published StochasticOrders.MonotoneConvex.IcxOrder P P X₁ X₂, read as $X_1\preceq_{\mathrm{icx}}X_2$.

Formalization targets

Goal: Theorem 5.1 (p. 446)

Under the standing assumptions, for every distribution-invariant $\rho:\mathcal X\to\mathbb R$,

$$\rho\ \text{consistent with}\ \succeq_{\mathrm{icx}}\quad\Longleftrightarrow\quad \rho\ \text{satisfies (A2) and is risk averse}.$$

No convexity, translation equivariance or positive homogeneity of $\rho$ is assumed.

Milestones

1. The usual stochastic order and the cdf (§5.2, p. 445): $X_2\succeq_{\mathrm{st}}X_1$ iff $F_{X_2}(t)\le F_{X_1}(t)$ for all $t$.
2. The quantile coupling (proof of Lemma 5.1, p. 446): $F_X^{-1}(U)$ has the law of $X$, and $F_{X_2}\le F_{X_1}$ gives $F_{X_1}^{-1}(U)\le F_{X_2}^{-1}(U)$ almost surely.
3. Lemma 5.1 (p. 445): a distribution-invariant $\rho$ is consistent with $\succeq_{\mathrm{st}}$ iff it satisfies (A2).
4. Conditional expectation is icx-smaller (proof of Theorem 5.1, p. 446): $\mathbb E[X\mid\mathcal G]\in\mathcal X$ and $\mathbb E[X\mid\mathcal G]\preceq_{\mathrm{icx}}X$.
5. Strassen's coupling on $\Omega$ (proof of Theorem 5.1, p. 446): if $X_1\preceq_{\mathrm{icx}}X_2$, there are $\widehat X_1\overset{D}{\sim}X_1$, $\widehat X_2\overset{D}{\sim}X_2$ on the same $\Omega$ with $\widehat X_1\le\mathbb E[\widehat X_2\mid\widehat X_1]$ a.s.

Significance

Theorem 5.1 reduces a property quantified over all pairs of ordered distributions to two properties that can be checked on the risk function directly. Monotonicity is usually immediate, and risk aversion follows for the main examples from the dual representation of the risk function (the paper verifies it for mean–semideviation and for CVaR-based models in §5.1). The theorem then yields at once the consistency of these models with the increasing convex order, which was previously proved case by case. It also explains the failures: a law-invariant risk function that violates (A2), such as mean–deviation for $p>1$ under the paper's condition $(*)$, cannot be consistent with any increasing integral stochastic order.

The result has a complete published proof. What the mission adds is a machine-checked version of it on the paper's own space $\mathcal L_p(\Omega,\mathcal F,P)$, together with reusable pieces of stochastic-order theory: the cdf characterization of the usual stochastic order, the quantile coupling, conditional Jensen in increasing-convex form, and Strassen's martingale coupling realized on a given space carrying a uniform random variable. Mathlib has conditional Jensen for convex functions (ConvexOn.map_condExp_le_univ) but not the stochastic orders, the quantile coupling or Strassen's theorem. Strassen's theorem for laws on $\mathbb R^n$, with a coupling on some probability space, is posed separately on Prove2Me but not proved.

Difficulty

The forward direction is short given milestone 4. The reverse direction is where the work is. Consistency compares $\rho(X_1)$ and $\rho(X_2)$ for random variables that are related only through their laws: $X_1\preceq_{\mathrm{icx}}X_2$ says nothing about $X_1(\omega)$ versus $X_2(\omega)$, so neither (A2) nor risk aversion applies to the pair as given. The argument has to replace the pair by another pair, with the same laws, on the same space $\Omega$, related by a conditional expectation; only then can monotonicity and risk aversion be chained. Producing that pair is Strassen's theorem, a nonconstructive existence result about martingale couplings, and it has to be realized on the given $\Omega$, not on a product space built for the purpose, because $\rho$ is defined only on $\mathcal L_p(\Omega,\mathcal F,P)$. That is the role of the uniform random variable, and transporting the coupling onto $\Omega$ through it is a separate measure-theoretic step. The first-order analogue, Lemma 5.1, needs the same kind of transfer, through quantile functions, whose values at $0$ and $1$ must be handled.

Formalization scope

• $\mathcal L_p$ is encoded by functions $\Omega\to\mathbb R$ satisfying MemLp X p P with 1 ≤ p and p ≠ ⊤, not by almost-everywhere classes. $\rho$ is a function (Ω → ℝ) → ℝ; every definition quantifies only over MemLp arguments, so its values elsewhere play no role. $\rho$ is real valued, as in Definition 5.2.
• The order in (A2) is the almost-sure order, the order of $\mathcal L_p$ (p. 434).
• "For which the expectations exist" is integrability of $u\circ X_1$ and $u\circ X_2$, as in the published increasing convex order.
• Risk aversion quantifies over every sub-$\sigma$-algebra $\mathcal G\subseteq\mathcal F$ and every $\mathcal G$-measurable version of Mathlib's conditional expectation P[X|m].
• The uniform random variable and $p\in[1,\infty)$ appear as hypotheses of the goal, of Lemma 5.1 and of milestone 5, exactly where the paper's standing assumptions of §5.2 apply. Milestones 1 and 4 do not need them.
• The quantile $F^{-1}(t)=\inf\{s:F(s)\ge t\}$ is a real infimum, which is $0$ where the paper's value is $\pm\infty$ ($t\notin(0,1)$); milestone 2 is therefore stated almost surely.
• The goal mentions neither quantiles, nor $U$ beyond its existence, nor any coupling. A statement that assumed convexity of $\rho$, dropped distribution invariance, restricted to bounded or pointwise-ordered outcomes, or replaced risk aversion by the single $\sigma$-algebra $\{\emptyset,\Omega\}$ would be a different and weaker theorem and does not count.

Needed infrastructure: equality in law from equality of cdfs, the quantile transform, conditional Jensen's inequality (in Mathlib) turned into the increasing convex order, and Strassen's theorem in dimension one with the transfer of a coupling to a space carrying a uniform random variable. The last two are reusable well beyond this mission. Proofs of any milestone, and of supporting lemmas such as the cdf characterization of equality in law, are welcome.

Selected references

• A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
• A. Müller, D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002 (Theorem 1.2.8, Corollary 1.5.21). https://www.wiley.com/en-us/Comparison+Methods+for+Stochastic+Models+and+Risks-p-9780471494461
• V. Strassen, The existence of probability measures with given marginals, Annals of Mathematical Statistics 36(2):423–439, 1965. https://doi.org/10.1214/aoms/1177700153
• D. Blackwell, Equivalent comparisons of experiments, Annals of Mathematical Statistics 24(2):265–272, 1953. https://doi.org/10.1214/aoms/1177729032
• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean–risk models, SIAM Journal on Optimization 13(1):60–78, 2002. https://doi.org/10.1137/S1052623400375075
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

Conic quadratic optimization — linear optimization over products of quadratic (second-order, Lorentz) cones — covers robust linear programming, portfolio problems with risk constraints, norm minimization and many engineering design problems. Andersen, Roos and Terlaky describe the primal-dual interior-point method implemented in the MOSEK optimizer for this problem class (Math. Program. 95 (2003)). Their algorithm does not solve the primal and dual problems directly. It solves the homogeneous model, an embedding that has a solution whether or not the original problem is feasible, and from which either an optimal pair or a certificate of infeasibility is read off.

The convergence argument of such a method rests on one algebraic property of its search direction: a step along the Newton direction reduces the infeasibility of the homogeneous model and its complementarity gap at the same rate. For linear programming this is classical (Xu, Hung and Ye, 1996; Andersen and Andersen, 2000). This mission formalizes the conic quadratic version, Lemma 4.1 of the paper, in which the diagonal complementarity products of linear programming are replaced by arrow-head matrices.

Setting

The cone is a product $K = K^1\times\cdots\times K^k$. Each factor $K^i\subseteq\mathbb R^{n^i}$ is one of three kinds:

• the half-line $\mathbb R_+ = \{x\in\mathbb R : x\ge0\}$, with $n^i = 1$;
• the quadratic cone $K^q = \{x\in\mathbb R^{n} : x_1^2\ge\|x_{2:n}\|^2,\ x_1\ge0\}$, with $n^i\ge1$;
• the rotated quadratic cone $K^r = \{x\in\mathbb R^{n} : 2x_1x_2\ge\|x_{3:n}\|^2,\ x_1,x_2\ge0\}$, with $n^i\ge2$.

Vectors are partitioned by cones, $x = (x^1;\dots;x^k)$, and $x^Ts = \sum_i (x^i)^Ts^i$. To each cone is attached a symmetric orthogonal matrix $T^i$: the identity for $\mathbb R_+$ and $K^q$, and for $K^r$ the identity with its leading $2\times2$ block replaced by $\frac{1}{\sqrt2}\begin{bmatrix}1&1\\1&-1\end{bmatrix}$. For $v\in\mathbb R^d$ the arrow-head matrix is

$$\operatorname{mat}(v) = \begin{bmatrix} v_1 & v_{2:d}^T\\ v_{2:d} & v_1 I\end{bmatrix}.$$

At a point $(x,s)$ put $X^i = \operatorname{mat}(T^ix^i)$, $S^i = \operatorname{mat}(T^is^i)$, and let $X$, $S$, $T$ be block diagonal with blocks $X^i$, $S^i$, $T^i$. Let $e^i$ be the first unit vector of $\mathbb R^{n^i}$ and $e = (e^1;\dots;e^k)$.

The data are $A\in\mathbb R^{m\times n}$, $b\in\mathbb R^m$, $c\in\mathbb R^n$. A current point is $(x^{(0)},\tau^{(0)},y^{(0)},s^{(0)},\kappa^{(0)})$, with

$$\mu^{(0)} = \frac{(x^{(0)})^Ts^{(0)} + \tau^{(0)}\kappa^{(0)}}{k+1}.$$

For a centering parameter $\gamma\in[0,1]$ the Newton direction $(d_x,d_\tau,d_y,d_s,d_\kappa)$ solves the linear system (22):

$$\begin{aligned} A d_x - b d_\tau &= (\gamma-1)(Ax^{(0)} - b\tau^{(0)}),\\ A^Td_y + d_s - c d_\tau &= (\gamma-1)(A^Ty^{(0)} + s^{(0)} - c\tau^{(0)}),\\ -c^Td_x + b^Td_y - d_\kappa &= (\gamma-1)(-c^Tx^{(0)} + b^Ty^{(0)} - \kappa^{(0)}),\\ X^{(0)}Td_s + S^{(0)}Td_x &= -X^{(0)}S^{(0)}e + \gamma\mu^{(0)}e,\\ \tau^{(0)}d_\kappa + \kappa^{(0)}d_\tau &= -\tau^{(0)}\kappa^{(0)} + \gamma\mu^{(0)}. \end{aligned}$$

The new point is $(x^{(1)},\tau^{(1)},y^{(1)},s^{(1)},\kappa^{(1)}) = (x^{(0)},\tau^{(0)},y^{(0)},s^{(0)},\kappa^{(0)}) + \alpha(d_x,d_\tau,d_y,d_s,d_\kappa)$ for a step size $\alpha\in[0,1]$ (23).

Formalization targets

Goal: Lemma 4.1 (p. 13)

Under (22) and (23),

$$\begin{aligned} Ax^{(1)} - b\tau^{(1)} &= (1-\alpha(1-\gamma))(Ax^{(0)} - b\tau^{(0)}),\\ A^Ty^{(1)} + s^{(1)} - c\tau^{(1)} &= (1-\alpha(1-\gamma))(A^Ty^{(0)} + s^{(0)} - c\tau^{(0)}),\\ -c^Tx^{(1)} + b^Ty^{(1)} - \kappa^{(1)} &= (1-\alpha(1-\gamma))(-c^Tx^{(0)} + b^Ty^{(0)} - \kappa^{(0)}),\\ d_x^Td_s + d_\tau d_\kappa &= 0,\\ (x^{(1)})^Ts^{(1)} + \tau^{(1)}\kappa^{(1)} &= (1-\alpha(1-\gamma))\big((x^{(0)})^Ts^{(0)} + \tau^{(0)}\kappa^{(0)}\big). \end{aligned}$$

Milestones

1. (25), p. 13: with $\eta = 1-\gamma$, the shifted point $\eta(x^{(0)},\tau^{(0)},y^{(0)},s^{(0)},\kappa^{(0)}) + d$ satisfies the three linear equations of the homogeneous model.
2. (26), p. 13: $0 = (\eta x^{(0)}+d_x)^T(\eta s^{(0)}+d_s) + (\eta\tau^{(0)}+d_\tau)(\eta\kappa^{(0)}+d_\kappa)$, and its expansion in powers of $\eta$.
3. (61), p. 36: $e^TXSe = \sum_i (T^ix^i)^TT^is^i = x^Ts$ for all $x$, $s$.
4. p. 14, first equality: $(x^{(0)})^Td_s + (s^{(0)})^Td_x = e^T(X^{(0)}Td_s + S^{(0)}Td_x)$, for all vectors.
5. p. 14, the chain's value: $(x^{(0)})^Td_s + (s^{(0)})^Td_x + \tau^{(0)}d_\kappa + \kappa^{(0)}d_\tau = (\gamma-1)\mu^{(0)}(k+1)$.
6. p. 14, orthogonality: $d_x^Td_s + d_\tau d_\kappa = 0$.

Significance

Lemma 4.1 is what makes the homogeneous algorithm analyzable. Because the three residuals and the gap shrink by the same factor $1-\alpha(1-\gamma)$, their ratios are invariant along the iterates, and a step with $\gamma<1$ and $\alpha>0$ makes measurable progress toward a solution of the homogeneous model. The paper notes (p. 14) that all properties stated in Lemma 4.1 hold for the Nesterov–Todd-scaled direction (27) as well, the direction actually implemented, for which polynomial complexity is shown by Monteiro and Tsuchiya (2000).

The result is proved on the page; it is not open. As far as the platform's catalogue shows, it has not been formalized. Machine-checked versions exist only for linear-programming analogues, with diagonal complementarity products in place of arrow-head matrices. The formalization adds two things. First, it fixes three printed slips: the third line of (22) prints $\kappa$ for $\kappa^{(0)}$; the fourth identity of (24) prints $d_x^Td_s^T$; and the proof's evaluation on p. 14 ends with $(\gamma-1)\mu^{(0)}k$ where $(\gamma-1)\mu^{(0)}(k+1)$ is correct, since $e^Te = k$ and the $\tau\kappa$ equation contributes the extra $\mu^{(0)}$. Second, the arrow-head identities (61) and the p. 14 equality are reusable for missions on the complementarity conditions (Lemma 3.1) and the scaled directions of the same paper.

Difficulty

The first three identities of (24) are linear and follow from the first three lines of (22) alone. The content is in the last two. They need an inner-product identity that turns the fourth line of (22), a statement about arrow-head matrix products, into a statement about the scalar quantity $(x^{(0)})^Td_s + (s^{(0)})^Td_x$. The naive reading treats $X^{(0)}Td_s$ as an abstract linear image of $d_s$ and loses exactly this link. What is needed is that the first row of $\operatorname{mat}(v)$ is $v^T$, that $\operatorname{mat}(u)\operatorname{mat}(v)e_1$ has first entry $u^Tv$, and that every $T^i$ is symmetric and orthogonal. The last fails for the rotated cone when $n^i<2$, so the dimension conventions are not decoration. The bookkeeping constant $e^Te = k$ must also be tracked correctly; the page itself gets it wrong.

Formalization scope

• Representation. Blocks are indexed by Fin k; block $i$ is Fin (n i) → ℝ, and indices are 0-based (the paper's $v_1$ is v 0). $A$ is given by its column blocks $A^i$, so $Ax = \sum_iA^ix^i$, $(A^Ty)^i = (A^i)^Ty$ and $c^Tx = \sum_i (c^i)^Tx^i$. The second line of (22) and of (24), and the fourth line of (22), are stated block by block; this is equivalent because $X$, $S$, $T$ are block diagonal.
• Definitions. The shared module ConicQuadIPM.Complementarity.Setting provides the cone kinds, $T^i$ (Tmat), $\operatorname{mat}(v)$ (arrow), $e^i$ (e1) and the predicate WellFormed; this mission's ConicQuadIPM.NewtonStep.Setting adds $\mu^{(0)}$ (mu0) and the system (22) (NewtonSystem). WellFormed is the paper's implicit dimension convention ($n^i = 1$, $\ge1$, $\ge2$ for the three kinds).
• Hypotheses. Every theorem assumes WellFormed. This is a disclosed addition: the paper never states the dimensions, and without them a block of dimension $0$ breaks $e^Te = k$. The ranges $\alpha\in[0,1]$ and $\gamma\in[0,1]$ are kept as on the page, although the identities hold for all real values. No interiority or cone membership of the current point is assumed, because Lemma 4.1 does not use any. The $\kappa$ of (22)'s third line is $\kappa^{(0)}$.
• No trivialization. The fourth line of (22) must stay in terms of arrow and Tmat. Replacing $X^{(0)}Td_s$ by an abstract linear map, or by $(x^{(0)})^Td_s$ directly, would turn milestone 4 into a definition and empty the goal. Milestone 5 states the corrected constant $k+1$; the printed $k$ is false whenever $\gamma\ne1$ and $\mu^{(0)}\ne0$.
• Reusable parts. The arrow-head lemmas (first row of $\operatorname{mat}(v)$, $e_1^T\operatorname{mat}(u)\operatorname{mat}(v)e_1 = u^Tv$, symmetry and orthogonality of $T^i$) are useful beyond this mission. Contributions of these as separate lemmas are welcome.

Selected references

• E. D. Andersen, C. Roos, T. Terlaky, On implementing a primal-dual interior-point method for conic quadratic optimization, Mathematical Programming 95 (2003) 249–277; cited from the authors' preprint of 18 December 2000. https://doi.org/10.1007/s10107-002-0349-3
• X. Xu, P.-F. Hung, Y. Ye, A simplified homogeneous and self-dual linear programming algorithm and its implementation, Annals of Operations Research 62 (1996) 151–171. https://doi.org/10.1007/BF02206815
• E. D. Andersen, K. D. Andersen, The MOSEK interior point optimizer for linear programming: an implementation of the homogeneous algorithm, in High Performance Optimization, Kluwer (2000) 197–232. https://doi.org/10.1007/978-1-4757-3216-0_8
• R. D. C. Monteiro, T. Tsuchiya, Polynomial convergence of primal-dual algorithms for the second-order cone program based on the MZ-family of directions, Mathematical Programming 88 (2000) 61–83. https://doi.org/10.1007/PL00011378