Optimization

Motivation

Two-stage optimization separates a decision made before uncertainty is observed from one made after a scenario is known. A fully adaptive policy can choose a different second-stage decision in each scenario, while a static robust solution commits to a single second-stage decision that works in every scenario. Static solutions can be simpler to implement, but their worst-case cost may be higher. Bertsimas and Goyal ask how large this cost difference can be when both the right-hand sides of the constraints and the second-stage prices vary. Their Theorem 5.1 gives a factor of four when the paired uncertainty set is symmetric and nonnegative, even when both stages contain integer variables.

The distinction matters in planning problems where one policy is fixed in advance and another could respond to realized demand or prices. A uniform bound lets a planner assess the cost of the static restriction without solving every adaptive policy exactly. The source is the authors' manuscript; all page and result numbers in this mission refer to that manuscript, not to the journal pagination.

Setting

Fix matrices $A\in\mathbb R^{m\times n_1}$ and $B\in\mathbb R^{m\times n_2}$. A scenario $\omega\in\Omega$ supplies a right-hand side $b(\omega)\in\mathbb R_+^m$ and a second-stage cost vector $d(\omega)\in\mathbb R_+^{n_2}$. The first-stage cost vector is $c\in\mathbb R_+^{n_1}$. For a set $I$ of designated integer coordinates, write $D_I$ for the nonnegative real vectors whose coordinates in $I$ are integers. After relabelling, this is the paper's $\mathbb R_+^{n-p}\times\mathbb Z_+^p$.

In the robust problem $\Pi_{\mathrm{Rob}}(b,d)$, one first-stage decision $x\in D_{I_1}$ and one second-stage decision $y\in D_{I_2}$ must satisfy $Ax+By\ge b(\omega)$ for every scenario. Their cost is $c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty$. In the adaptive problem $\Pi_{\mathrm{Adapt}}(b,d)$, $x$ is still chosen once, but $y(\omega)\in D_{I_2}$ may depend on the scenario. Its constraints are $Ax+By(\omega)\ge b(\omega)$ for every $\omega$, and its cost is $c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty(\omega)$. The optimal values $z_{\mathrm{Rob}}(b,d)$ and $z_{\mathrm{Adapt}}(b,d)$ are infima over feasible decisions in these respective problems; these are models (1.5)–(1.6).

The paired uncertainty set is $I_{(b,d)}(\Omega)=\{(b(\omega),d(\omega)): \omega\in\Omega\}$. It is symmetric when it contains a point $u^0$ such that $u^0+z$ belongs to the set exactly when $u^0-z$ does, for every displacement $z$. The point $u^0$ is itself a scenario realization. The smallest coordinatewise bounding hypercube has lower and upper corners $(b^l,d^l)$ and $(b^h,d^h)$; its center is $((b^l+b^h)/2,(d^l+d^h)/2)$. These are Definition 1.2 and displays (2.5)–(2.7).

Formalization targets

The adaptability gap

The goal is Theorem 5.1:

$$z_{\mathrm{Rob}}(b,d)\le 4z_{\mathrm{Adapt}}(b,d).$$

The factor applies to every nonnegative symmetric paired uncertainty set and to both continuous and mixed-integer decisions. The theorem does not require an optimal adaptive policy to attain its infimum. The milestones record the source's geometric Lemma 2.3 and the estimates labelled (5.1)–(5.4), which supply the center-scenario cost and feasibility statements with the explicit factor four. They are stated for arbitrary feasible adaptive policies so the conclusion also covers nonattained infima.

Significance

The result bounds the price of committing to a single second-stage decision, despite uncertainty in both the constraints and the objective. In this setting the comparison is independent of the number of scenarios and of the dimensions $m,n_1,n_2$. The paper also considers right-hand-side-only uncertainty, positive sets, and hypercubes; this mission isolates its symmetric paired-uncertainty result §5.1.

The theorem is proved in the paper. The remaining formalization work is a machine-checked development of the model, the bounding-hypercube geometry, the cost inequalities, and the passage from arbitrary feasible policies to the optimal values. The resulting definitions of mixed-integer domains, robust and adaptive feasibility, and extended-real optimal values can also support the other results in this paper's mission series. The theorem statements here are open proof targets, with no machine-checked proofs claimed.

Difficulty

The worst-case maximizer of $d(\omega)^Ty(\omega)$ can vary with $\omega$, and an adaptive policy can choose a different integer vector in every scenario. Selecting one of those vectors as a static decision therefore gives no immediate cost or feasibility guarantee. The point of symmetry is a realizable scenario, but it must control both components of every other paired scenario. Without nonnegative data, doubling the center-scenario decision may fail to cover a positive right-hand side, and the cost comparison can fail as well. Integer coordinates also constrain which scalings preserve the decision domain; the exact factor in the theorem is compatible with doubling, unlike arbitrary fractional rescalings.

Formalization scope

Vectors are real functions on finite index types, matrices use Mathlib's matrix-vector product, and inequalities are componentwise. The scenario set is the range of $\omega\mapsto(b(\omega),d(\omega))$, with a product-space symmetry predicate. No probability measure or measurability structure is used in these worst-case problems. Both stages may have integer coordinates designated by sets $I_1,I_2$; no continuous-only second-stage restriction is imposed.

Optimal values and worst-case costs use extended real numbers. An infeasible problem has value $+\infty$; a real infimum over an empty feasible set would incorrectly return a default zero. Symmetry includes a center belonging to the scenario range, so the scenario set is nonempty. Combined with nonnegative coordinates, symmetry bounds every scenario coordinate and makes the bounding-hypercube endpoints meaningful. The hypotheses retain $c\ge0$, $b(\omega)\ge0$, and $d(\omega)\ge0$, which the source uses in its factor-four estimate. A statement restricted to continuous recourse, an assumed optimal adaptive policy, or a zero-valued infeasible problem would not express this target.

The source prints $\mathbb Z_+^{n_2}$ in (1.5)–(1.6), although the model's second-stage integer count is $p_2$; the domain here follows the surrounding $p_2$ convention. Lemma 2.3 is stated here for nonnegative sets, the regime needed for its second inequality. Its coordinatewise suprema and infima agree with the printed maxima and minima in this bounded symmetric setting. Contributions to the shared domain and geometry lemmas, the mixed-integer scaling fact, and the optimal-value comparison are all useful to the goal.

Selected references

• Dimitris Bertsimas and Vineet Goyal, On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems, authors' manuscript of Mathematics of Operations Research, 2010. DOI: 10.1287/moor.1090.0440.

Motivation: curvature of the central path as a complexity measure

Path-following interior point methods solve a linear program by tracking its central path, a smooth curve that runs through the interior of the feasible set and ends at an optimal solution. Their number of iterations is polynomial in the bit size of the input, and whether some interior point method is strongly polynomial (bounded by a polynomial in the number of variables and constraints alone) is open. Bayer and Lagarias called the central path "a fundamental mathematical object underlying Karmarkar's algorithm". Dedieu and Shub proposed its total curvature as an informal complexity measure: a path that turns little should be easy to follow with straight steps. Several results bound that curvature:

• 2005. Dedieu and Shub conjecture that the total curvature of the central path is bounded linearly in the dimension. Dedieu, Malajovich and Shub prove an $O(n)$ bound on average over the regions of a hyperplane arrangement. De Loera, Sturmfels and Vinzant later obtain the same averaged bound with matroid methods (arXiv:1012.3978).
• 2008–2009. Deza, Terlaky and Zinchenko build redundant Klee–Minty cubes and "snakes" with curvature $\Omega(m)$ for $m$ inequalities, which refutes the dimension version. They then conjecture the continuous analogue of the Hirsch conjecture: the total curvature is bounded linearly in the number of constraints.
• 2014–2017. Allamigeon, Benchimol, Gaubert and Joswig disprove that conjecture with a family of linear programs whose central paths have curvature exponential in the number of constraints. The bound first appeared in arXiv:1405.4161 and was given an elementary tropical proof in arXiv:1708.01544v2, Theorem 25, which is the result of this mission.

Setting

A linear program in slack form has a real $m\times n$ matrix $A$, $b\in\mathbb R^m$, $c\in\mathbb R^n$ and $N:=n+m$:

$$\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. } Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .$$

For $\mu>0$ the point of the central path $(x^\mu,w^\mu,s^\mu,y^\mu)\in\mathbb R^{2N}$ is the unique solution of

$$Ax+w=b,\quad s-A^\top y=c,\quad x_js_j=\mu,\quad w_iy_i=\mu,\quad x,w,s,y>0. \tag{1}$$

The primal central path is $\mu\mapsto(x^\mu,w^\mu)\in\mathbb R^N$.

For $r\ge1$ and $t>0$, the program $\mathbf{LW}_r(t)$ minimizes $x_1$ over $x\in\mathbb R^{2r}$ subject to

$$x_1\le t^2,\quad x_2\le t,\quad x_{2j+1}\le t\,x_{2j-1},\quad x_{2j+1}\le t\,x_{2j},\quad x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ \ (1\le j<r),\quad x\ge0 .$$

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$, $m=3r-1$, $N=5r-1$.

For points $U,V,W$ of Euclidean space with $U\ne V\ne W$, the turning angle $\angle UVW\in[0,\pi]$ is the angle between the vectors $V-U$ and $W-V$. For a curve $\sigma$ parameterized over $I\subseteq\mathbb R$, the total curvature is

$$\kappa(\sigma,I)=\sup\Big\{\sum_{k=1}^{p-1}\angle\,\sigma(\mu_{k-1})\sigma(\mu_k)\sigma(\mu_{k+1})\ :\ \mu_0<\dots<\mu_p\ \text{in } I\Big\}\in[0,+\infty].$$

The milestones also use the field $\mathbb K$ of absolutely convergent generalized real Puiseux series $\sum_{\alpha\in\mathbb R}a_\alpha t^\alpha$. Such a series can be evaluated at large real $t$, and it has a valuation $\mathrm{val}\in\mathbb T=\mathbb R\cup\{-\infty\}$, its leading exponent. Read over $\mathbb K$, $\mathbf{LW}_r$ is one linear program. The valuation of its central path at $\mu=t^\lambda$ is the tropical central path $\mathcal C^{\mathrm{trop}}(\lambda)\in\mathbb R^{2N}$, a piecewise-linear curve with an explicit recursive description (Propositions 20–21 of the paper).

Formalization targets

Goal: Theorem 25

For every $r\ge1$ and $\epsilon>0$ there is $t_0$ such that for all $t>t_0$,

$$\kappa\big(\mu\mapsto(x^\mu,w^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon\quad\text{and}\quad\kappa\big(\mu\mapsto(x^\mu,w^\mu,s^\mu,y^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon$$

for the central path of $\mathbf{LW}^=_r(t)$. Here $t_0$ may depend on $r$ and $\epsilon$. Both the primal and the primal-dual curves are part of the goal, as in the paper.

Milestones, in the order of the paper's argument

1. Lemma 22: for non-null $\mathbf x,\mathbf y\in\mathbb K^d$, the angle $\angle\mathbf x(t)\mathbf y(t)$ has a limit, which is $\pi/2$ when the arg maxes of $\mathrm{val}\,\mathbf x$ and $\mathrm{val}\,\mathbf y$ are disjoint.
2. Lemma 23: the turning angle $\angle\mathbf U(t)\mathbf V(t)\mathbf W(t)\to\pi/2$ when $\max\mathrm{val}\,\mathbf U<\max\mathrm{val}\,\mathbf V<\max\mathrm{val}\,\mathbf W$ and the arg maxes of $\mathrm{val}\,\mathbf V$ and $\mathrm{val}\,\mathbf W$ are disjoint.
3. Proposition 24: $\liminf_{t}\kappa(\mathcal C_t,[t^{\lambda_0},t^{\lambda_p}])\ge\sum_{k=1}^{p-1}\angle^*\mathcal C^{\mathrm{trop}}(\lambda_{k-1})\mathcal C^{\mathrm{trop}}(\lambda_k)\mathcal C^{\mathrm{trop}}(\lambda_{k+1})$, where $\angle^*$ is the weak tropical angle ($\pi/2$ under the conditions of Lemma 23, else $0$).
4. Table 1: the coordinates of the tropical central path of $\mathbf{LW}_r$ at $\lambda=(4k+2c)/2^j$.
5. Claims in the proof of Theorem 25 (p. 23): on $[0,2]$ the dual coordinates of $\mathcal C^{\mathrm{trop}}$ are at most $\max(0,\lambda-1)$. At $\lambda_k=4k/2^{r-1}$ the largest coordinate is $r-1+(2k+2)/2^{r-1}$, attained only by $w_{3(r-1)}$ or $w_{3(r-1)+1}$. Hence $\angle^*=\pi/2$ at each interior subdivision point.

Significance

The theorem shows that the total curvature of the central path is not bounded by any polynomial in the number of constraints: $\mathbf{LW}_r$ has $3r+1$ constraints and curvature at least about $2^{r-2}\pi/2$. This settles the conjecture of Deza, Terlaky and Zinchenko in the negative. It also shows that the averaged upper bounds of Dedieu–Malajovich–Shub and De Loera–Sturmfels–Vinzant cannot hold for every region. A companion mission of this series formalizes the paper's second main result, an exponential lower bound on the number of iterations of log-barrier path-following methods on the same family.

The result is proved on paper. As far as is known, it has not been formalized in any proof assistant, and Mathlib has no notion of the total curvature of a curve, of Puiseux-series evaluation and valuation, or of the tropical central path. Formalizing the theorem would give a machine-checked reference point for a much-cited negative result in interior point theory. The Lean definitions of total curvature and of the turning angle are general and reusable.

Difficulty

The total curvature is a supremum over inscribed polygons, and a lower bound needs explicit polygons whose angles can be estimated for every large $t$. The central path of $\mathbf{LW}^=_r(t)$ has no closed form, so its points cannot be written down at given parameters $\mu$. Numerical evidence at a fixed $t$ says nothing uniform in $r$. The natural first idea, to compute the path's angles directly from system (1) for a fixed instance, gives no handle on how the number of turns grows with $r$. What is needed is control of the path's geometry uniformly over the whole scale of $t$, with $2^{r-2}$ turns located at once, and the threshold $t_0$ is not explicit.

Formalization scope

Vectors in which angles are measured are EuclideanSpace ℝ (Fin d). The turning angle is InnerProductGeometry.angle (V - U) (W - V), not Mathlib's vertex angle ∠ U V W, which is $\pi$ minus it. A degenerate triple ($U=V$ or $V=W$) contributes angle $0$. Total curvature is an EReal-valued supremum over strictly increasing parameter sequences in the parameter set, and the goal uses the set $(0,\infty)$. The primal and primal-dual curves are the vectors $(x,w)\in\mathbb R^{5r-1}$ and $(x,w,s,y)\in\mathbb R^{2(5r-1)}$. System (1) is the published Vanderbei central-path system with objective $-c$. The goal quantifies over every curve solving (1) for all $\mu>0$. Existence and uniqueness of that curve is the referenced platform statement VanderbeiLP.CentralPath.central_path_exists_unique and is not posed again. Indices are the paper's, 1-based, mapped to Fin by subtracting one. Powers $2^{r-2}$ use integer exponents of the real number $2$.

A trivializing formalization is ruled out explicitly: the curvature is a supremum in EReal (a real sSup of an unbounded set would be $0$), the turning angle is not the vertex angle, and degenerate polygons cannot add spurious right angles.

Lemmas 22–24 are stated over a model of $\mathbb K$ by coefficient functions with the paper's support and absolute-convergence conditions. Equalities, products and order in $\mathbb K$ are expressed through evaluation at all sufficiently large $t$, which is how the paper characterizes them. Table 1 and the claims of the proof are stated for the explicit tropical central path of $\mathbf{LW}_r$ given by Propositions 20–21 (milestones of the companion mission), written as a definition here. One repair: the paper's "uniquely attained" claim fails at $r=2$, $k=0$, where $w_1=w_4=2$. It is stated with that case excluded, which the proof does not use.

Welcome contributions: a general theory of total curvature of curves (monotonicity under refinement, behaviour under limits), asymptotics of evaluated Puiseux series, and the comparison between the central path over $\mathbb K$ and its real specializations.

Selected references

• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-Barrier Interior Point Methods Are Not Strongly Polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; preprint v2 (cited throughout) arXiv:1708.01544, doi:10.1137/17M1142132.
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Long and winding central paths, preprint, 2014. arXiv:1405.4161
• J. A. De Loera, B. Sturmfels, C. Vinzant, The central curve in linear programming, Found. Comput. Math. 12(4), 2012. arXiv:1012.3978
• J.-P. Dedieu, G. Malajovich, M. Shub, On the curvature of the central path of linear programming theory, Found. Comput. Math. 5(2), 2005.
• J.-P. Dedieu, M. Shub, Newton flow and interior point methods in linear programming, Int. J. Bifurcation and Chaos 15(3), 2005.
• A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Springer, 2009.
• L. van den Dries, P. Speissegger, The real field with convergent generalized power series, Trans. Amer. Math. Soc. 350(11), 1998.

Motivation

Assortment optimization asks a retailer which products to offer when customers substitute among them. The nested logit model groups products into nests and is one of the most used choice models in revenue management, because it relaxes the independence of irrelevant alternatives of the plain multinomial logit model while keeping choice probabilities in closed form. Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) study how the tractability of the assortment problem under this model depends on two features: whether the dissimilarity parameters of the nests are at most one, and whether a customer who selects a nest always buys there (fully-captured nests).

When the dissimilarity parameters are at most one and the nests are fully captured, offering the $j$ highest-revenue products in every nest is optimal (Theorem 4 of the paper). This mission concerns what survives when a dissimilarity parameter exceeds one, the regime the paper calls possibly synergistic products. Then the problem is NP-hard (Theorem 5), and the paper shows that the same nested-by-revenue assortments still achieve an explicit, data-dependent fraction of the optimal expected revenue.

Setting

There are nests $i \in M$ and products $j \in N = \{1, \dots, n\}$ in every nest. Product $j$ of nest $i$ has a revenue $r_{ij}$ and a preference weight $v_{ij} > 0$, ordered so that $r_{i1} \ge r_{i2} \ge \dots \ge r_{in}$. Nest $i$ has a dissimilarity parameter $\gamma_i > 0$, and $v_0 \ge 0$ is the weight of leaving without choosing a nest. Throughout this mission the nests are fully captured: the within-nest no-purchase weights $v_{i0}$ are zero. For an assortment $S_i \subseteq N$ in nest $i$,

$$V_i(S_i) = \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)}, \quad R_i(\emptyset) = 0,$$

and the expected revenue of $(S_1, \dots, S_m)$ is

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

Problem (2) maximizes $\Pi$; its optimal value is $Z^*$. The nested-by-revenue assortment $N_{ij} = \{1, \dots, j\}$ collects the $j$ highest-revenue products of nest $i$, with $N_{i0} = \emptyset$ and $N_+ = \{0, 1, \dots, n\}$.

Problem (2) is equivalent to the linear program (3): minimize $x$ subject to $v_0 x \ge \sum_i y_i$ and $y_i \ge V_i(S_i)^{\gamma_i}(R_i(S_i) - x)$ for every nest $i$ and every $S_i \subseteq N$. Problem (4) keeps the second family of constraints only for candidate assortments; here the candidates are $\{N_{ij} : j \in N_+\}$, which gives a linear program with $1 + m$ variables and $1 + m(1 + n)$ constraints. The performance factor of the nested-by-revenue assortments is

$$\alpha = \max_{i \in M,\ j = 2, \dots, n} \left\{ \frac{R_i(N_{i,j-1})}{R_i(N_{ij})} \wedge \left(\frac{R_i(N_{ij})}{R_i(N_{i,j-1})}\, \frac{V_i(N_{ij})^{\gamma_i}}{V_i(N_{i,j-1})^{\gamma_i}}\right) \right\}, \qquad a \wedge b = \min\{a, b\}. \tag{6}$$

Formalization targets

Goal: Theorem 7

Assume $v_{i0} = 0$ for every nest, $\gamma_i > 1$ for some nest, positive revenues and $n \ge 2$. If $(\hat x, \hat y)$ is an optimal solution of (4) over the nested-by-revenue assortments, then

$$(\alpha \hat x, \alpha \hat y) \ \text{is feasible for (3)}.$$

Combined with Theorem 1 of the paper this yields $Z^* \le \alpha\, \Pi(\hat S)$ for the assortment $\hat S$ read off the small linear program; that consequence is a companion item.

Milestones

1. Problem (3) is a relaxation of the fractional problem (7), in which $y_i$ dominates $\big(\sum_j v_{ij} z_{ij}\big)^{\gamma_i}\big[\sum_j r_{ij} v_{ij} z_{ij} / \sum_j v_{ij} z_{ij} - x\big]$ for all $z_i \in [0,1]^n$.
2. Lemma 6: the inner maximization (8) of (7) has a solution of the form $z_{i1} = \dots = z_{i,k-1} = 1$, $z_{ik} \in [0,1]$, $z_{i,k+1} = \dots = z_{in} = 0$.
3. $\hat y_i \ge 0$ and $\hat x \ge 0$.
4. The inequalities (20) and (22) with the coefficients $\alpha^1_{ik} = R_i(N_{i,k-1})/R_i(N_{ik})$ and $1 \vee \alpha^2_{ik}$.
5. $R_i(N_{ij}) \le R_i(N_{i,j-1})$, and Lemma 14: $\alpha \ge 1$ when some $\gamma_i > 1$.
6. The inequalities (24) and (25): $\alpha \hat y_i$ dominates the objective of (8) at $\alpha \hat x$ for every vector of Lemma 6's shape.

Two companion statements follow the goal: the bounds $\alpha \le \rho$ and $\alpha \le 2\kappa$ when revenues, respectively preference weights, within each nest differ by at most the factors $\rho$, $\kappa$; and the guarantee $Z^* \le \alpha\, \Pi(\hat S)$.

Significance

Because problem (2) is NP-hard once a dissimilarity parameter exceeds one (Theorem 5 of the paper), an exact polynomial algorithm is not expected, and a guarantee for a polynomial-size candidate family is the natural substitute. Theorem 7 gives one with an explicit factor computed from the data: $\alpha \le \rho$ when revenues within each nest are balanced, $\alpha \le 2\kappa$ when preference weights within each nest are balanced, and the nests may differ arbitrarily from one another. The same linear-programming argument (Theorem 1) is reused for partially-captured nests in §6 of the paper.

The result is proved in the paper (Appendix A.1); no machine-checked version is known. A formalization verifies an appendix argument that is stated with little detail, and fixes the conventions that the page leaves implicit, such as the value of the objective of (8) at $z_i = 0$ and the role of the standing assumption that some $\gamma_i$ exceeds one.

Difficulty

Theorem 7 is a feasibility statement for the exponentially many constraints of (3), one per subset of every nest, while optimality of $(\hat x, \hat y)$ only controls the $n + 1$ nested-by-revenue constraints per nest. The obvious approach, comparing each subset directly with a nested-by-revenue assortment, fails: when $\gamma_i > 1$ the nested-by-revenue assortments are not optimal within a nest, and the example of §4.1 shows that they can lose an unbounded factor. The constant $\alpha$ must absorb the gap between a fractional assortment and its two neighbouring nested-by-revenue assortments, which the dual-style solution $(\hat x, \hat y)$ of the small program does not see.

Formalization scope

Lean 4 with Mathlib. Nests form a finite type ι; products are Fin n, indexed from $0$, so $N_{ij}$ is nbr n j = {k | k < j} and product $k$ of the page is ⟨k - 1, _⟩. Powers are real powers (Real.rpow), and division is total ($x / 0 = 0$), which gives $R_i(\emptyset) = 0$ and value $0$ for the objective of (8) at $z_i = 0$.

Standing assumptions in every statement: $v_0 \ge 0$, $v_{i0} \ge 0$, $v_{ij} > 0$, $r_{ij} \ge 0$, $\gamma_i > 0$, revenues ordered within each nest (§1); $v_{i0} = 0$ for every nest and $\gamma_i > 1$ for some nest (§4, p. 16). Added and disclosed: $r_{ij} > 0$ wherever (6) appears, so that no denominator of (6) vanishes; $n \ge 2$, the nonempty range of (6); $v_0 > 0$ only in the guarantee $Z^* \le \alpha\,\Pi(\hat S)$, inherited from Theorem 1. The factor $\alpha$ enters as a real number with the hypothesis that it is the greatest element of the set of terms of (6). An optimal solution of (4) is a feasible pair whose $x$ is minimal among feasible pairs.

A trivializing formalization is ruled out: $\alpha$ is the maximum of (6), not an arbitrary upper bound, and the goal states feasibility for the full program (3) over every subset of every nest, not for (7) or for the candidate collection.

Needed infrastructure: maximization of a continuous function on $[0,1]^n$, the greedy solution of a continuous knapsack, monotonicity of weighted averages and elementary real-power calculus. These are reusable beyond this mission. Proofs of any milestone, of the companions, and of the §4.1 example 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. https://doi.org/10.1287/opre.2014.1256 (formalized from the revised manuscript of June 18, 2013).
• 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

Motivation

A portfolio manager who maximizes expected utility needs the distribution of asset returns, but in practice only estimates of its first two moments are available, and these estimates are themselves noisy. Distributionally robust optimization handles this by optimizing against the worst distribution in a set of plausible ones. Delage and Ye (Operations Research 58(3), 2010) proposed a set of distributions defined by confidence bounds on the mean and on the second-moment matrix, showed that the resulting problems are solvable in polynomial time for a large class of costs, and applied the framework to portfolio selection.

The set contains an upper bound on the covariance but no lower bound. Remark 1 of the paper says a lower bound "leads to important computational difficulties" and argues it should be unnecessary: for a concave utility, a less predictable market can only reduce expected utility, so the worst distribution should already have the largest covariance allowed. Proposition 3 in §5.2 turns this argument into a theorem for piecewise-linear concave utilities and unconstrained support. This mission formalizes Proposition 3 and the steps of its proof.

Setting

Let $n$ assets have a random return vector $\xi\in\mathbb R^n$, and let $x\in\mathbb R^n$ be a portfolio, so the return is $\xi^{\mathsf T}x$. A distribution of $\xi$ is a Borel probability measure on $\mathbb R^n$ with finite second moments. For symmetric matrices, $A\preceq B$ (the Loewner order) means $B-A$ is positive semidefinite.

Given a support set $S$, a centre $\mu_0$, a positive definite matrix $\Sigma_0\succ0$ and $\gamma_1\ge0$, $\gamma_2>0$, the distributional set of Assumption 3 is

$$\mathcal D_1(S,\mu_0,\Sigma_0,\gamma_1,\gamma_2)=\Big\{P\ :\ P(\xi\in S)=1,\ (\mathbb E[\xi]-\mu_0)^{\mathsf T}\Sigma_0^{-1}(\mathbb E[\xi]-\mu_0)\le\gamma_1,\ \mathbb E[(\xi-\mu_0)(\xi-\mu_0)^{\mathsf T}]\preceq\gamma_2\Sigma_0\Big\}.$$

The second constraint, (1b), is the covariance constraint.

The utility is piecewise linear concave, $u(y)=\min_{k\in\{1,\dots,K\}}a_ky+b_k$ with $K\ge1$ pieces, and the cost of a return is $-u$:

$$h(x,\xi)=\max_{k}\ \big(-a_k\,\xi^{\mathsf T}x-b_k\big).$$

With estimates $\hat\mu$, $\hat\Sigma\succ0$ of the mean and covariance, the inner problem of the robust portfolio problem with unconstrained support and an exactly known mean ($\gamma_1=0$) is

$$\max_{P\in\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,0,\gamma_2)}\ \mathbb E_P\big[h(x,\xi)\big].\tag{18}$$

The proof relates (18) to a semidefinite program in variables $\Lambda_k\in\mathbb R^{n\times n}$, $\lambda_k\in\mathbb R^n$, $\nu_k\in\mathbb R$:

$$\max\ \sum_k\big(-a_k\,x^{\mathsf T}\lambda_k-b_k\nu_k\big)\quad\text{s.t.}\quad \sum_k\Lambda_k\preceq\gamma_2\hat\Sigma+\hat\mu\hat\mu^{\mathsf T},\ \ \sum_k\lambda_k=\hat\mu,\ \ \sum_k\nu_k=1,\ \ \begin{bmatrix}\Lambda_k&\lambda_k\\\lambda_k^{\mathsf T}&\nu_k\end{bmatrix}\succeq0.\tag{19}$$

Formalization targets

Goal: Proposition 3

For every $\gamma_1\ge0$ (the mean-uncertainty radius of the robust portfolio problem (16); (18) is the case $\gamma_1=0$),

$$\exists\,P^*\in\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2):\quad \mathbb E_{P^*}\big[(\xi-\hat\mu)(\xi-\hat\mu)^{\mathsf T}\big]=\gamma_2\hat\Sigma\quad\text{and}\quad \mathbb E_Q[h(x,\xi)]\le\mathbb E_{P^*}[h(x,\xi)]\ \ \forall\,Q\in\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2).$$

The worst-case expectation is attained, and at a distribution for which the covariance constraint holds with equality. The statement holds for every portfolio $x$, every $K\ge1$, every $a,b$, every $\hat\mu$, every $\hat\Sigma\succ0$, every $\gamma_1\ge0$ and every $\gamma_2>0$.

Milestones

1. Every value of (18) is dominated by the value of a feasible point of (19).
2. (19) has an optimal solution at which $\sum_k\Lambda_k=\gamma_2\hat\Sigma+\hat\mu\hat\mu^{\mathsf T}$.
3. If $\begin{bmatrix}\Lambda&\lambda\\\lambda^{\mathsf T}&\nu\end{bmatrix}\succeq0$ and $\nu>0$, a random vector with mean $\lambda/\nu$ and second moment $\Lambda/\nu$ exists.
4. The mixture $\sum_k\nu_kP_k$ of such vectors, built from a tight feasible point with all $\nu_k>0$, lies in $\mathcal D_1$ and has second moment $\gamma_2\hat\Sigma$ about $\hat\mu$.
5. The expected cost under that mixture is at least the objective value of (19) at the point.
6. (18) and (19) have the same attained optimal value.

Significance

The proposition justifies a modelling decision of the whole paper: for portfolio problems with piecewise-linear concave utility, adding a lower bound $\gamma_3\Sigma_0\preceq\mathbb E[(\xi-\mu_0)(\xi-\mu_0)^{\mathsf T}]$ (display (2)) to the distributional set cannot change the robust decision, so the computational difficulty that lower bound would cause is avoided at no loss. It also shows that, under these assumptions and with $\gamma_2=1$, the paper's semidefinite formulation solves the known-moment portfolio problem of Popescu (2007) in polynomial time (Remark 4). The worst case is explicit: a finite mixture of distributions with prescribed first and second moments, read off an optimal solution of (19).

The result is proved in the paper; no machine-checked version is known. Formalizing it requires a moment-problem argument (from a distribution to a feasible point of an SDP) and its converse (from an SDP solution to a distribution), both of which are reusable for other moment-based distributionally robust results. The proposition concerns the robust portfolio problem with $\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2)$; the paper's proof writes out only $\gamma_1=0$ "for simplicity of our derivations". The goal states the proposition for every $\gamma_1\ge0$; the milestones follow the written proof and are stated for $\gamma_1=0$.

Difficulty

The obvious argument, "a concave utility prefers less spread, so the adversary maximizes spread", does not prove anything by itself: increasing the second-moment matrix of a given distribution in the Loewner order does not determine its law, and the expected cost depends on the whole law, not on the moments. The proof goes through the semidefinite program (19). Two steps carry the weight. First, every distribution in $\mathcal D_1$ must be mapped to a feasible point of (19) with no smaller value, although the cost is only piecewise affine in $\xi$. Second, an optimal point of (19) must be turned back into a distribution in $\mathcal D_1$; this needs the existence of random vectors with prescribed first and second moments, and care with blocks where $\nu_k=0$, which the paper sets aside "without loss of generality" although such a block can carry a nonzero $\Lambda_k$ that the mixture would lose.

Formalization scope

• Vectors are Fin n → ℝ; all Euclidean quantities are dot products, never the sup norm. Matrices are Matrix (Fin n) (Fin n) ℝ; $A\preceq B$ is (B - A).PosSemidef; $\Sigma_0^{-1}$ is Mathlib's matrix inverse, used only with $\Sigma_0\succ0$.
• A distribution is a Measure (Fin n → ℝ) that is a probability measure and whose coordinates are in $L^2$ (MemLp _ 2). This makes every mean, second moment and expected cost a genuine integral; without it a non-integrable expectation would evaluate to $0$.
• $P(\xi\in S)=1$ is an almost-everywhere statement; the goal uses $S=\mathbb R^n$ ("infinite support constraint"). The convexity of $S$, $\mu_0\in\operatorname{int}S$ and the separation oracle of Assumption 3 concern the paper's algorithms and are not part of the set.
• The maximum of (18) is never a real supremum: the goal asserts a maximizer that dominates every member of the set. The cost uses a finite maximum over $K\ge1$ pieces ([NeZero K]).
• Standing hypotheses: $\hat\Sigma\succ0$ (Assumption 3's $\Sigma_0\succ0$, and endnote 1), $\gamma_2>0$ (§3), $\gamma_1\ge0$ (Assumption 3) in the goal; the milestones fix $\gamma_1=0$ as the proof does. The portfolio $x$ ranges over all of $\mathbb R^n$; the simplex constraint (16b) plays no role in the inner problem, so dropping it only strengthens the statements.
• The objective of (19) has the sign of the proof's final computation (p. 21), $\sum_k(-a_kx^{\mathsf T}\lambda_k-b_k\nu_k)$; display (19a) on p. 19 prints the opposite signs, a misprint.
• Ruling out trivial readings: the goal requires both membership in $\mathcal D_1$ with tight covariance and domination of every member of $\mathcal D_1$. A distribution with covariance $\gamma_2\hat\Sigma$ alone, or a maximizer alone, would not suffice. The goal does not claim that every maximizer is tight; for $K=1$ the cost is linear and every member of $\mathcal D_1$ is a maximizer.
• Infrastructure needed: existence of distributions with prescribed mean and covariance (for instance multivariate Gaussians, or degenerate laws on a subspace), finite mixtures of measures and their moments, Schur complements of positive semidefinite block matrices, and compactness of the feasible set of (19). Proofs of the milestones in any order are welcome.

The source is the authors' draft of 20 February 2008 of the Operations Research paper; every page, display and label in this mission refers to that draft.

Selected references

• E. Delage and Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3):595–612, 2010 (authors' draft of 20 February 2008 used here). https://doi.org/10.1287/opre.1090.0741
• I. Popescu, Robust mean-covariance solutions for stochastic optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• Y. Nesterov and A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

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

Motivation

Fashion and consumer-electronics retailers sell a product at full price early in a season and mark down what is left. Consumers learn the pattern, and some of them wait for the markdown. Such strategic consumers lower the revenue of the full-price period, and the retailer's stocking decision affects how deep the markdown is expected to be. Quick response — a second, more expensive replenishment placed after demand is observed — is usually valued as a way to match supply with exogenous demand (Fisher and Raman 1996; Cachon and Terwiesch, Matching Supply with Demand, 2005). Cachon and Swinney ask how strategic waiting changes that value.

The source is the authors' working paper of April 2007, revised November 25, 2007, not the 2009 Management Science version, whose numbering and wording may differ. Its answer: with strategic consumers the retailer stocks less (Theorem 1), and under an explicit cost condition, quick response is worth more to a retailer facing strategic consumers than to one facing only myopic consumers (Theorem 3).

Setting

A retailer sells over two periods. It sells at the exogenous full price $p$ in period 1 and at a markdown price $s\in[0,p]$ chosen at the start of period 2. Leftover units are worth $0$. First-period demand $D\ge0$ has density $f$ and distribution function $F$, and $f$ satisfies the monotone scaled likelihood ratio (MSLR) property: for every $\lambda\in(0,1]$, $x\mapsto f(\lambda x)/f(x)$ is monotonic on the support of $f$.

The market has three segments:

• myopic consumers, $(1-\alpha)D$ of them, with value $v_M$, who only buy in period 1;
• strategic consumers, $\alpha D$ of them, with value $v_M$ in period 1 and second-period values uniform on $[\underline v,\bar v]$;
• an unlimited pool of bargain hunters with value $v_B$, who only buy on sale.

The standing assumptions are $\bar v\le p$ and $\underline v\ge v_M-p+v_B$. Let $\bar G(s)$ be the fraction of strategic values above $s$.

By a threshold argument (Lemma 1), strategic consumers with value below some $\hat v$ buy at $p$ and the rest wait. A fraction $\xi=1-\bar G(\hat v)\alpha$ of demand then buys in period 1, and the inventory left for period 2 is $I=(q-\xi D)^+$. The period-2 revenue $R(s,I)$ counts the waiting strategic consumers with value at least $s$ and, if $s\le v_B$, the bargain hunters, up to the inventory $I$. The retailer's expected profit at unit cost $c$ is

$$\pi(q,\hat v)=\mathbb E\Big[p\min(q,\xi D)-cq+\sup_{0\le s\le p}R(s,I)\Big].$$

With quick response, units ordered before the season cost $c_1$ and units ordered after observing $D$ cost $c_2$, with $c_1\le c_2\le p$. The second order covers all first-period demand and may add stock for the sale. The resulting profit is $\pi_r(q,\hat v)$.

In the sale period, waiting strategic consumers are rationed: they effectively face the inventory $\theta I$, where $\theta\in[0,1]$ measures their place in the queue. A strategic consumer with value $\hat v$ who waits gains, in expectation,

$$\psi(\hat v)=(\hat v-v_B)\Pr(D<D_l\text{ and a unit is received}),$$

where $D_l$ is the demand level below which the retailer clears stock at $s_l=v_B$. A rational expectations equilibrium $(q^*,v^*)$ is a pair in which $q^*$ maximizes $\pi(\cdot,v^*)$ and $v^*$ is a best response of consumers who correctly expect $q^*$. The superscript $m$ denotes the benchmark with only myopic consumers ($\alpha=0$): $\pi^m$ and $\pi^m_r$ are the optimal myopic profits without and with quick response.

Formalization targets

Goal: Theorem 3

Assume MSLR and no rationing, $0<\alpha\le1$, $v_B<c_1<p$, $c_1\le c_2\le p$, and condition (6):

$$\frac{v_M-p}{\bar v-v_B}\ \ge\ \frac{c_2-c_1}{c_2-v_B}.$$

Let $(q^*,v^*)$ be any equilibrium without quick response, $(q_r^*,v_r^*)$ any equilibrium with it, and $\pi^m$, $\pi_r^m$ the myopic optima. Then

$$\pi_r(q_r^*,v_r^*)-\pi(q^*,v^*)\ \ge\ \pi_r^m-\pi^m .$$

Milestones

The milestones follow the paper's path:

• the threshold structure (Lemma 1);
• the optimal sale price (Lemma 2) and quasi-concavity of $\pi$ with first-order condition (2) (Lemma 3);
• the fill probability and the limits of the best response (Lemma 4);
• existence and the comparison $q^*\le q^m$, $\pi^*\le\pi^m$ (Theorem 1), with the myopic newsvendor $F(q^m)=(p-c)/(p-v_B)$;
• the quick-response analogues (Lemma 5, Theorem 2 (i)), with the myopic fractile $F(q^m_r)=(c_2-c_1)/(c_2-v_B)$;
• the statement that under (6) every equilibrium with quick response has $v^*_r=\bar v$ (Theorem 2, last sentence).

Corollary 1 is the percentage form, $\Delta/\pi^*\ge\Delta_m/\pi^m$.

Significance

Theorem 3 identifies a second channel through which quick response creates value. Beyond matching supply to demand, it lets the retailer keep its initial stock low enough that a deep markdown becomes unlikely, so strategic consumers buy at full price. Under (6), all of them do. Quick response thus reduces strategic waiting without withholding availability, unlike the inventory-signalling remedies in the literature, and the theorem quantifies when this effect dominates.

The results are proved in the working paper, partly in a technical appendix. No machine-checked version of them, or of the underlying markdown game, is known. A formalization pins down several statements that the paper states loosely:

• the uniqueness claims of Lemmas 2 and 5;
• the case condition of Lemma 4 (i), which is false as printed;
• the sign in display (5);
• the boundary cases of the threshold lemma.

It also produces reusable components: the newsvendor with salvage and the reactive-capacity fractile under a general density, and a rational-expectations equilibrium predicate for a retailer–consumer game.

Difficulty

The profit $\pi(\cdot,\hat v)$ is not concave: with strategic consumers it is concave–convex (Figure 4 of the paper). The newsvendor argument therefore does not give a unique optimal order, and Lemma 3's quasi-concavity rests on MSLR in a short appendix step.

Existence (Theorem 1) needs a fixed point of the map $q\mapsto$ best response, but the consumer best response is a correspondence, not a function, so the printed intermediate-value argument does not apply directly. Theorem 3 needs a statement about every equilibrium with quick response, while Theorem 2's proof only exhibits one. Ruling out an equilibrium with $v_r^*<\bar v$ requires comparing the derivative (4) of $\pi_r$ with the myopic derivative along the whole demand distribution.

Formalization scope

Lean represents prices, quantities and valuations as reals, demand by a density $f:\mathbb R\to\mathbb R$ on $[0,\infty)$, and expectations as Lebesgue integrals against $f$. The model carries the standing assumptions of §3 as fields, plus the following additions and corrections, each disclosed in the item notes:

• $v_B>0$: $D_l$ divides by $s_l=v_B$.
• $p<v_M$, strengthening $v_M\ge p$: Lemma 4 (ii) and Theorem 2's last claim need it.
• A finite mean: $\pi_r$ contains $\mathbb E[p\xi D]$.
• The paper's "$\theta_c\le\theta$" (p. 15) is replaced by the no-rationing condition $s_l\bar G(\hat v)\le\theta s_m\bar G(s_m)$ for every belief, which is exactly $D_l\le D_\theta$. The printed condition agrees with it only when $s_m=\hat v$.
• Lemma 4 (i) is stated with the corrected case split.
• Lemmas 2 and 5 claim uniqueness only off the tie points.
• $c<p$ is the reading of the "$p-c>0$" step in the proof of Theorem 1.
• In the quick-response profit, $\xi D$ replaces the $D$ that the proof of Theorem 2 prints.

Optimal revenues are suprema over all prices $s\in[0,p]$ (and $q_2\ge0$ with quick response). "Optimal order" means a maximizer over all $q\ge0$, never a stationary point, and the myopic benchmarks are the same functions at $\alpha=0$. Defining the optimal revenue by Lemma 2's closed form would make Lemma 2 and the first-order conditions definitional; it is not done.

The fill rate is $\min\{(1-\xi)x,\theta I\}/((1-\xi)x)$, set to $1$ when no strategic consumer waits. With Lean's $0/0=0$ instead, $\bar v$ would be a best response to every order and Theorem 2's last claim would be trivial.

A complete development needs:

• differentiation under the integral for piecewise-smooth integrands;
• quasi-concavity from a single-crossing derivative;
• a fixed-point argument for the equilibrium correspondence;
• the newsvendor and reactive-capacity fractiles.

The last two are reusable beyond this mission. Proofs of any milestone, alternative existence arguments, and sorry-free proofs of the newsvendor items are welcome. The comparison "$q_r^*\le q^*$, $\pi_r^*\ge\pi^*$" of Theorem 2 and §8's numerical study are outside the scope.

Selected references

• G. P. Cachon, R. Swinney, Purchasing, Pricing, and Quick Response in the Presence of Strategic Consumers, working paper, revised November 25, 2007; published in Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0948
• M. L. Fisher, A. Raman, Reducing the Cost of Demand Uncertainty Through Accurate Response to Early Sales, Operations Research 44(1), 1996. https://doi.org/10.1287/opre.44.1.87
• J. F. Muth, Rational Expectations and the Theory of Price Movements, Econometrica 29(3), 1961. https://doi.org/10.2307/1909635