Optimization

Motivation

A discrete moment problem asks for the largest expected payoff compatible with prescribed moments of an unknown probability distribution. A decision maker may know the first few moments of demand or loss while the full distribution remains uncertain. The optimization then asks which compatible distribution makes a chosen payoff largest. Chen, He, Jiang, Ryan, and Zhang study what happens when the distribution must also obey a shape constraint. Their preprint treats discrete log-concavity and increasing failure rate as two such constraints. This mission concerns the log-concave case.

The moment constraints alone define a convex polytope of probability vectors. Requiring log-concavity changes its geometry: the feasible region is generally nonconvex. This matters because familiar descriptions of extreme points of a moment polytope no longer describe the candidate worst-case distributions. The paper's Theorem 4.1 gives a finite structural description of the optimal extreme points despite that change. Its proof uses a general result about optimization over reverse convex constraints, Theorem 3.6, which is also included as a milestone. Both statements and their setting are taken from arXiv:1708.02079v1, pages 5–15.

Setting

Fix the finite sample space $\Omega=\{1,\ldots,n\}$. A distribution is a vector $x=(x_1,\ldots,x_n)$ of nonnegative masses. For each integer $i$ from $0$ through $m$, its prescribed moment is $q_i$, so $\sum_{j=1}^{n}j^i x_j=q_i$. The convention $q_0=1$ makes the masses sum to one. Given payoff coefficients $f_j$, the discrete moment problem maximizes $\sum_{j=1}^{n}f_jx_j$ over the distributions satisfying these equations.

A distribution is discrete log-concave when its positive masses form one consecutive integer interval $[k,\ell]$ and $x_{j-1}x_{j+1}\le x_j^2$ at every interior index $k<j<\ell$. In the paper's formulation (DMP-LC), the entries on $[k,\ell]$ are strictly positive and the other entries are zero; the feasible region is the union over all such supports. Its alternative formulation (DMP-LC′) replaces the chosen support with nonnegativity and a family of longer-range inequalities. Proposition 2.4 says that the two feasible regions coincide. The extreme points in this mission are those of the entire feasible region, including every possible support.

The paper also considers a general reverse convex program in $\mathbb R^n$: minimize a function $c(x)$ subject to $Ax=b$, $x\ge0$, and $f_p(x)\le0$ for $p=1,\ldots,P$. Here the reverse convex condition is relative to the nonnegative orthant: the forbidden set $\{x\ge0:f_p(x)>0\}$ is convex. Under the paper's continuity, quasiconcavity, differentiability, rank, and compactness assumptions, Theorem 3.6 counts the inequalities that are tight at an optimal extreme point.

Formalization targets

The goal is the corrected mathematical content of Theorem 4.1. If (DMP-LC) is feasible, an optimal extreme point exists. Every optimal extreme point $x^*$ has support $[k,\ell]$ and can be covered by at most $m$ geometric pieces. In symbols, there are weakly increasing breakpoints $k=b_0\le b_1\le\cdots\le b_m=\ell$ and positive parameters $\alpha_i,r_i$ such that

$$x_j^*=\alpha_i r_i^{j-b_{i-1}}\quad\text{for }b_{i-1}\le j\le b_i, \qquad x_j^*=0\quad\text{outside }[k,\ell].$$

The milestone path includes the equivalence of the two feasible formulations, compact-set extreme-point results, convexity of the forbidden power regions, the reverse convex tight-constraint count, and the two structural steps in the proof of Theorem 4.1. Theorem 3.6 asserts, in particular, that at each optimal extreme point of its $m$-row program,

$$n-m\le \#\{p:f_p(x^*)=0\}+\#\{j:x_j^*=0\}.$$

Significance

The conclusion replaces an unrestricted search over feasible probability vectors with a characterization of the candidates that can be optimal extreme points. It also identifies how the number of prescribed nonzero-order moments controls the number of geometric pieces. The count in Theorem 3.6 applies to the larger class of reverse convex programs described above; it is useful independently of this distributional example. These are results proved in the cited preprint, rather than open conjectures.

The formalization target is to give the known statements a machine-checked proof in Lean. The proposed items are statements with proof placeholders; they do not yet assert that a machine-checked proof exists. The finite moment notation, the log-concave feasible region, and the reverse convex feasible region are separate definition files so the general finite-dimensional objects can be reused. Contributions to the milestone theorems, the proof of the goal, and supporting lemmas are all in scope.

Difficulty

The log-concavity inequalities do not make the feasible region convex, so the standard convex-polytope description of optimal extreme points does not directly apply. In addition, the chosen support may move: a vector that is extreme within one fixed-support slice need not be extreme in the full union. Existence of an optimal solution alone gives no bound on the number of geometric pieces. The challenge is to obtain enough tight constraints at every optimal extreme point, then relate those equalities to its coordinates without assuming the desired shape in the definition of feasibility.

Formalization scope

Lean represents $\mathbb R^n$ as Fin n → ℝ; a Fin n index with value $j-1$ represents the paper's position $j$. The helper ext supplies the paper's one-based coordinates and returns zero outside $[1,n]$. Moments use the exact weights $w_j=j$. All feasible sets use real vectors, with nonnegativity or strict positivity stated where the paper requires it. The (DMP-LC) region is the union over supports satisfying (2b)–(2e); the goal uses extreme points of that whole set and a maximization objective. The reverse convex milestones use minimization, full row rank, and convexity of the forbidden sets inside the nonnegative orthant. Compactness and nonemptiness are explicit assumptions where the source invokes them.

Two corrections to the printed Theorem 4.1 are necessary. First, its bound $0<r_i<1$ is false. With $n=3$, $m=1$, $q_0=1$, $q_1=5/2$, and payoff $f=(1,0,0)$, the unique maximizing extreme point is approximately $(0.1162,0.2676,0.6162)$, whose geometric ratio is about $2.30$. The formal statement requires $r_i>0$. Second, the printed strict chain of breakpoints fails for short supports: with $n=3$, $m=2$, and moments $(q_0,q_1,q_2)=(1,2,4)$, the only feasible distribution is the point mass at $2$. Weak breakpoints express the paper's “at most $m$ pieces” conclusion. They allow degenerate pieces; $m=0$ is retained and forces a point mass. The proof's closed-range wording for tight equalities is read on interior indices, and the tight count uses $m+1$ moment rows. These choices and the paper's typographical slips are recorded with the items.

The feasible region does not encode geometric sequences, and extremeness is never taken only within one support or within its convex hull. The development needs Mathlib's finite sums, finite-dimensional topology, convex hulls, extreme points, matrix rank, continuity, quasiconcavity, and differentiation. The finite discrete moment definition and reverse convex feasible-set definition are intended for reuse beyond this paper.

Selected references

• X. Chen, S. He, B. Jiang, C. T. Ryan, and T. Zhang, The Discrete Moment Problem with Nonconvex Shape Constraints, preprint arXiv:1708.02079v1, 2017; published in Operations Research, 2021. Pinned preprint.

Motivation

A medical visit, a hotel stay or a bank onboarding is not one transaction but a service process: a sequence of steps (check-in, waiting, examination, payment), each delivered by the provider and each experienced by the customer. Practitioners design such processes with descriptive tools such as customer-journey maps and service blueprints, which list the steps and their touchpoints but do not say how much effort each step deserves. Two features make this allocation non-obvious. First, customers judge the experience as a whole, and the experiences at different steps are correlated: a long wait colours the examination that follows. Second, effort changes not only the average quality of a step but also its variability, and the direction depends on the step: at a routine step (check-in) more effort makes the outcome more predictable, while at a non-routine step (a diagnostic procedure) it may make it less so.

Bellos and Kavadias (Management Science, 2020) give a model in which the optimal effort per step has a closed form, and characterise when the efforts at two steps move together (are complementary) or in opposite directions (are substitutable) in response to a change in one step's characteristics. The answer depends on the two step types and on one entry of the inverse of the correlation matrix, not on the correlation itself. This mission formalizes that characterisation.

Setting

There are $n$ steps $i \in \mathcal J = \{1,\dots,n\}$. The provider chooses an effort $\delta_i \in [0,1]$ at every step and one price $\pi$.

• Functional value. Step $i$ delivers $V_i = \delta_i V^H_i + (1-\delta_i)V^L_i$ with $V^H_i > V^L_i \ge 0$. Steps reinforce each other through technical couplings $\beta_{j,i} \in [0,1)$ ($j \ne i$), $\beta_{i,i} = 1$, $\sum_{i\ne j}\beta_{j,i} < 1$, and the functional value at step $i$ is $\mathcal V_i = \sum_j \beta_{j,i}V_j$.
• Variability. The experiential value at step $i$ has standard deviation $\sigma_i = \delta_i\sigma^H_i + (1-\delta_i)\sigma^L_i$ with $\sigma^H_i, \sigma^L_i \ge 0$. The step is routine if $\sigma^H_i < \sigma^L_i$ and non-routine if $\sigma^H_i > \sigma^L_i$.
• Correlation. The experiences at steps $i$ and $j$ have correlation $\rho_{i,j} \in (-1,1)$, collected in a symmetric positive definite correlation matrix $\mathbf P$ with unit diagonal.
• Utility. Customers with risk aversion $r > 0$ obtain the mean-variance net utility

$$\mathcal U(\delta,\pi) = \sum_{i=1}^n \mathcal V_i - \frac r2\Big(\sum_{i=1}^n\sigma_i^2 + 2\sum\sum_{i<j}\rho_{i,j}\sigma_i\sigma_j\Big) - \pi.$$

• Design problem. With unit costs $c_i \in (\sum_{j\ne i}\beta_{j,i}, 1)$ and a reservation profit $\pi_0 \ge 0$, the provider maximizes $\mathcal U(\delta,\pi)$ subject to $\pi - \sum_i V_ic_i \ge \pi_0$ and $0 \le \delta_i \le 1$. An optimal effort $\delta^*$ is the effort of an optimal design.

The paper's analysis assumes that each $V^H_i - V^L_i$ lies in an explicit interval $(\underline{\Delta V}_i, \overline{\Delta V}_i)$ built from the other parameters, the cofactors of $\mathbf P$ and $|\mathbf P|$ (the interior condition), and for its comparative statics it sets the technical couplings between distinct steps to zero.

Formalization targets

Goal: Proposition 3

Fix a step $i$. Under the interior condition and without technical coupling, the effort at step $i$ satisfies

$$\frac{\partial\delta^*_i}{\partial c_i} < 0,\qquad \frac{\partial\delta^*_i}{\partial V^H_i} > 0,\qquad \operatorname{sgn}\frac{\partial\delta^*_i}{\partial\sigma^H_i} = -\operatorname{sgn}(\sigma^H_i - \sigma^L_i),$$

and for every $j \ne i$ the effort at step $j$ responds to $c_i$, $V^H_i$ and $\sigma^H_i$ in the same directions if and only if

$$\Big(\operatorname{sgn}[\sigma^H_i-\sigma^L_i] = \operatorname{sgn}[\sigma^H_j-\sigma^L_j] \text{ and } [\mathbf P^{-1}]_{i,j} > 0\Big) \text{ or } \Big(\operatorname{sgn}[\sigma^H_i-\sigma^L_i] \ne \operatorname{sgn}[\sigma^H_j-\sigma^L_j] \text{ and } [\mathbf P^{-1}]_{i,j} < 0\Big),$$

and in the opposite directions otherwise (when $[\mathbf P^{-1}]_{i,j} \ne 0$). The derivatives are of the optimizer of the design problem, in one parameter at a time.

Milestones

1. For a given effort the optimal price is $\tilde\pi(\delta) = \pi_0 + \sum_i V_ic_i$, so the problem reduces to maximizing $\tilde{\mathcal U}(\delta) = \mathcal U(\delta,\tilde\pi(\delta))$ over $[0,1]^n$.
2. The Hessian of $\tilde{\mathcal U}$ has entries $-r(\sigma^H_i-\sigma^L_i)(\sigma^H_j-\sigma^L_j)\rho_{i,j}$ and leading minors $|\boldsymbol H_k| = (-1)^kr^k\prod_{j\le k}(\sigma^H_j-\sigma^L_j)^2|\mathbf P[1:k;1:k]|$; $\tilde{\mathcal U}$ is strictly concave.
3. The gradient of $\tilde{\mathcal U}$, and the unique solution $\hat\delta$ of the first-order conditions.
4. The slope $\partial\hat\delta_i/\partial(V^H_i-V^L_i) > 0$ and the thresholds: $\hat\delta_i \le 0$ iff $V^H_i - V^L_i \le \underline{\Delta V}_i$, $\hat\delta_i \ge 1$ iff $V^H_i - V^L_i \ge \overline{\Delta V}_i$.
5. Proposition 1: under the interior condition the optimal effort is unique and equals

$$\delta^*_i = \hat\delta_i = \sum_{j=1}^n\frac{\big(1-(c_j-\sum_{m\ne j}\beta_{j,m})\big)(V^H_j-V^L_j)}{r(\sigma^H_i-\sigma^L_i)(\sigma^H_j-\sigma^L_j)}[\mathbf P^{-1}]_{i,j} - \frac{\sigma^L_i}{\sigma^H_i-\sigma^L_i}.$$

6. The explicit partial derivatives of $\delta^*$ in $c_j$, $V^H_j$, $\sigma^H_j$, own-step and cross-step, and the own-step half of Proposition 3.

Significance

The result. Proposition 3 says that a change at one step propagates to every other step through the inverse correlation matrix. An entry $[\mathbf P^{-1}]_{i,j}$ is, up to a negative factor, the partial correlation of steps $i$ and $j$ given all other steps. So two steps whose experiences are positively correlated can still have substitutable efforts once the rest of the process is accounted for, and two uncorrelated steps can have coupled efforts. Pairing a routine with a non-routine step reverses the direction. The paper's later results, on antedependent and autoregressive correlation structures and on the first versus the last step, use this characterisation as their starting point.

Formalizing it. The result is proved on paper. As far as is known, it has no machine-checked proof. Formalizing it means: a verified closed form for the maximizer of a box-constrained concave quadratic with a correlation-matrix Hessian; the identification of the optimizer with that closed form near the base point, so that the optimizer is differentiable there; and the sign analysis. Along the way the formalization corrects two printed slips: the auxiliary quantities $A$ and $B$ in the proof of Proposition 3 (as printed, the displayed identity for $\delta^*_i$ fails), and the printed "Otherwise", which is false when $[\mathbf P^{-1}]_{i,j} = 0$.

Difficulty

The sign algebra at the end is short. The work lies in the step before it: Proposition 3 differentiates the optimizer of a constrained problem, not a formula. To differentiate it one has to show that under the interior condition the optimizer exists, is unique, and coincides with $\hat\delta$ on a neighbourhood of the parameters in each direction of perturbation. This needs strict concavity from positive definiteness of $\mathbf P$, the identification of the interior condition (stated through cofactors of $\mathbf P$) with $\hat\delta \in (0,1)^n$, and the openness of that condition in the parameters. Differentiating $\hat\delta$ directly and reading off signs proves a statement about the closed form, not Proposition 3.

Formalization scope

Steps are Fin n, 0-based. All quantities are real. The utility $\mathcal U$ is defined by its mean-variance expression; no random variables appear. $\mathbf P$ is assumed symmetric, positive definite, with unit diagonal and off-diagonal entries in $(-1,1)$. The cofactor $(-1)^{i+j}|\mathbf P[-j;-i]|$ is Matrix.adjugate P i j. Two hypotheses are added to the page and disclosed: $r > 0$ (the model allows $r \ge 0$, but Proposition 1 divides by $r$) and $\sigma^H_i \ne \sigma^L_i$ (every step is routine or non-routine). Proposition 3 assumes $\beta_{j,i} = 0$ for $j \ne i$, the paper's own simplification for §4. A partial derivative is Lean's deriv of the optimal effort along one parameter, the others fixed ($V^L_i$ fixed when $V^H_i$ moves, $\sigma^L_i$ fixed when $\sigma^H_i$ moves). The optimal effort is a choice of maximizer of the §3.3 problem, with junk value $0$ when none exists.

Stating Proposition 3 for the closed form $\hat\delta$ instead of the optimizer of the design problem would trivialize it, and that formalization is ruled out. Likewise the interior condition is the page's interval on $V^H_i - V^L_i$, not the assumption $\hat\delta \in (0,1)^n$.

The development needs Mathlib's positive definite matrices, adjugates and determinants, strict concavity, and one-variable derivatives. Reusable by-products: strict concavity and the unique maximizer of a concave quadratic with Hessian $-rD\mathbf PD$; positivity of principal cofactors of a positive definite matrix. Contributions are welcome on any milestone, and alternative proofs of Proposition 1 by convex duality or KKT are welcome too.

Selected references

• I. Bellos and S. Kavadias, Service design for a holistic customer experience: a process framework, Management Science, 2020 (authors' manuscript). https://doi.org/10.1287/mnsc.2020.3609
• U. Karmarkar and R. Pitbladdo, Quality, class, and competition, Management Science 43(1), 27–39, 1997. https://doi.org/10.1287/mnsc.43.1.27
• A. Raveh, On the use of the inverse of the correlation matrix in multivariate data analysis, The American Statistician 39(1), 39–42, 1985. https://doi.org/10.2307/2683904

Motivation

A cloud provider buys servers in preset configurations, while its demand for processing and memory grows at different rates. Each server configuration supplies both resources, so adding capacity for one resource also changes the unused capacity of the other. Purchases incur a charge for the servers, a charge for making an expansion, and an ongoing cost for unused capacity. The choice between buying configurations together and staggering their purchases is therefore a cost decision even when demand is known. Arbabian, Chen, and Moinzadeh study this decision for two resources and two server configurations over a finite planning horizon. Their Proposition 1 identifies a threshold in the fixed cost of a joint expansion.

The result was stated in the authors' April 14, 2019 manuscript and published in Manufacturing & Service Operations Management in 2020. This mission uses the manuscript's theorem numbers and pages. The result is a known mathematical claim; the remaining work is to give its definitions and proof in Lean, with the source's policy classes and cost accounting represented explicitly.

Setting

There are two capacity attributes, indexed by $i\in\{1,2\}$, and two cluster types, indexed by $j\in\{1,2\}$. A unit of cluster $j$ supplies $a_{ij}>0$ units of attribute $i$. Demand for attribute $i$ increases at a nonnegative rate $d_i(t)$ over $[0,T]$, and $D_i(s,t)=\int_s^t d_i(u)\,du$ is its growth between $s$ and $t$. The provider starts with both attributes at their minimum desired excess capacity, normalized to zero. It must meet demand at every time and return both excess capacities to zero at the end of the horizon. Replenishment takes effect immediately. These are the base-model conventions in §3 of the manuscript.

A capacity expansion cycle begins and ends when both attributes are leveled. In a sequential cycle, one cluster type leads: it is bought one or more times, followed by one purchase of the other type. Each expansion costs $A>0$. In a simultaneous cycle, both types are bought at each expansion, whose fixed cost is $\beta A$ for $\beta\in[1,2]$. Cluster $j$ has unit purchase cost $c_j$, and unused attribute $i$ has holding rate $h_i>0$. If $E_i(t)$ is the excess capacity after the expansions at time $t$, total holding cost is $\sum_i h_i\int_0^T E_i(t)\,dt$. Total cost also includes all fixed and purchase costs. Sequential policies may have any positive number of cycles, any positive number of leading expansions within each cycle, and either leading type. For joint policies, the intervals between consecutive joint expansions form a partition of $[0,T]$.

Formalization targets

The main target is the unique fixed-cost threshold of Proposition 1. Write $V_{\mathrm{seq}}$ for the infimum of costs of all feasible sequential policies and $V_{\mathrm{sim}}(\beta)$ for the corresponding simultaneous infimum. The threshold $\bar\beta\in(1,2)$ satisfies, for every $\beta\in[1,2]$,

$$V_{\mathrm{sim}}(\beta)\le V_{\mathrm{seq}}\iff\beta\le\bar\beta, \qquad V_{\mathrm{sim}}(\beta)<V_{\mathrm{seq}}\iff\beta<\bar\beta.$$

This makes equality at $\bar\beta$ explicit, in line with the paragraph following Proposition 1. The milestone list records the source's sequential and simultaneous cost identities, the fixed-time holding comparison, the split comparison from the appendix, the two endpoint inequalities, and monotonicity in $\beta$. Equation (8), which fixes the final sequential expansion time inside a cycle, is another milestone because the authors use its uniqueness in their analysis.

Significance

The threshold gives a precise decision rule for the model: a lower relative joint expansion charge favors buying both types together; a higher charge favors staggered purchases. It compares optimized policies, whose cycle boundaries and expansion times may differ, rather than only two schedules held at the same times. The result therefore captures the interaction of the fixed charge and the time spent holding unused capacity. The paper also analyzes specialized one-cycle schedules under exponential demand; those results are separate from this mission's general comparison.

A completed Lean development would make the policy definitions, cost identities, and threshold claim machine checked. It would also provide reusable definitions for finite-horizon bundled capacity expansion, including a time-dependent excess-capacity trajectory and its integral holding cost. The manuscript supplies a mathematical proof, but this proposal's theorem files currently contain open sorry proofs. The mission invites proofs of its listed statements and the analytic facts needed to connect them, including existence of optimal schedules.

Difficulty

The straightforward comparison uses identical expansion times. That comparison identifies a holding-cost difference, but it does not compare the two optimized classes: the least-cost sequential schedule and the least-cost joint schedule may choose different times and different numbers of expansions. The paper's endpoint arguments also rely on strict inequalities for optimal costs. A strict inequality for every fixed schedule does not automatically become strict after taking an infimum. Showing that the relevant optima are attained, or supplying an equivalent uniform argument, is part of the formalization burden. The fixed expansion charge bounds how many expansions a near-optimal policy can afford, but the interval lengths remain continuous variables.

Formalization scope

Lean represents the attributes and cluster types by Fin 2, with index 0 corresponding to the paper's 1 and index 1 to its 2. The matrix entry a i j is capacity of attribute $i$ per unit of cluster $j$. Times, demand, quantities, and costs are real. Replenishment times are strictly increasing, and a purchase at time $t$ contributes to the right-continuous excess capacity at $t$. Policy validity requires no shortage and balance at cycle endpoints. The positive determinant $\alpha=a_{11}a_{22}-a_{12}a_{21}$ records the nondegenerate, attribute-intensive cluster configurations needed by the paper's division formulas. The optimal costs are real infima over full policy classes, with no attainment built into their definitions. Holding cost is computed from the integral of actual excess capacity; defining it by the displayed closed forms would erase the content of Lemmas 1 and 2.

The theorem assumes continuous demand rates and the strict demand-ratio guard $a_{12}d_2(t)<a_{22}d_1(t)$ and $a_{21}d_1(t)<a_{11}d_2(t)$ throughout $[0,T]$. The manuscript states Assumption 1 only for chosen leading intervals. Its Proposition 1 needs more: without the guard, taking $a=((2,1),(1,2))$, $A=100$, $c_j=0$, $h_i=1$, $d_2=1$, and $d_1=90$ on $[0,0.01)$ then $10/99$ permits one joint expansion at $\beta=2$ for at most 202 while every feasible sequential policy costs at least 300. Demand continuity supports the cost integrals; the strict guard makes every subinterval satisfy Assumption 1 strictly and keeps the appendix's sequential split feasible. Neither regularity nor this guard is claimed as a printed hypothesis of Proposition 1.

The appendix prints an extra $h_1$ outside the sum in its Case 2 holding-cost difference; the Lean milestone uses $\sum_i h_i(y-s)a_{i2}Q_2$, consistent with the preceding integrals. The paper also prints $[0,1]$ in its last monotonicity sentence, while its fixed-cost parameter is defined on $[1,2]$; the milestone uses the model's interval. Useful contributions include formal integration identities for these finite replenishment schedules, existence and finiteness of the policy optima, and the comparison claims in the milestones.

Selected references

• M. E. Arbabian, S. Chen, and K. Moinzadeh, Capacity Expansions with Bundled Supplies of Attributes: An Application to Server Procurement in Cloud Computing, Manufacturing & Service Operations Management, 2020. SSRN manuscript, April 14, 2019; published DOI.

Motivation

Restaurants that take orders online promise each customer a pickup time when the order is placed. A static quote promises every customer the same lead time $\delta$, the form in common use. Once the promise is fixed, the kitchen still decides when to start each order. Starting too early means the food waits and cools (an earliness cost). Starting too late breaks the promise (a tardiness cost). Farahani, Dawande and Janakiraman (SSRN 3557605; published in Operations Research, 2022, doi:10.1287/opre.2021.2203) model this as a single-server queue and propose simple threshold policies. To judge those policies against the unknown optimum they need lower bounds on the optimal long-run average cost, and their first such bound is the subject of this mission.

The bound uses a clairvoyant relaxation: a decision maker who knows every future arrival and service time can do no worse than one who does not. Relaxations of this kind are standard for finite-horizon stochastic dynamic programs, where the relaxed problem is deterministic and its expected value can be estimated by Monte Carlo simulation (Brown, Smith and Sun, 2010, doi:10.1287/opre.1090.0796). Brown and Haugh (2017, doi:10.1287/opre.2017.1631) extended them to discounted infinite-horizon problems. The queue here is an undiscounted infinite-horizon problem: the clairvoyant problem involves an infinitely long sample path, which cannot be simulated directly. Theorem 4 of the paper resolves this by showing that the clairvoyant cost per customer over any finite number of customers is already a valid lower bound.

Setting

A probability space carries inter-arrival times $T_1, T_2, \dots$ and service times $x_1, x_2, \dots$. The $T_n$ are identically distributed with mean $1/\lambda$, the $x_n$ are identically distributed with mean $1/\mu$, the whole family is mutually independent, and $\lambda < \mu$ (the queue is stable). Customer $n \ge 1$ arrives at

$$t_n = T_1 + \cdots + T_n$$

and is due at $d_n = t_n + \delta$, where $\delta \ge 0$ is the quote time. The arrival rate is $\lambda = 1/\mathbb E[T_1]$.

A schedule assigns to each customer $n$ a service start time $y_n$, which may depend on the sample path. It is FCFS-feasible if on every sample path

$$y_n \ge t_n, \qquad y_{n+1} \ge y_n + x_n \qquad (n \ge 1).$$

Customer $n$ departs at $D_n = y_n + x_n$ and pays $g(D_n - d_n)$, where

$$g(\xi) = c_e(-\xi)^+ + c_d(\xi)^+, \qquad c_e, c_d \ge 0.$$

The long-run average cost of a schedule is (the paper's form (4))

$$C(y) = \lambda \limsup_{N \to \infty} \mathbb E\Big[\frac1N \sum_{n=1}^N g(y_n + x_n - d_n)\Big].$$

The perfectly-clairvoyant cost of customers $i, \dots, j$ on a sample path $\omega$ (program (12)) is

$$\gamma_{i:j}(\omega) = \inf_y \sum_{n=i}^j g(y_n + x_n - d_n) \quad \text{s.t.} \quad y_n \ge t_n \ (i \le n \le j), \quad y_{n+1} \ge y_n + x_n \ (i \le n < j).$$

In Lean these are StaticQuote.Clairvoyant.Model with Standing, rate, arrival, due, g, IsFCFSSchedule, cost, IsSchedule and gamma.

Formalization targets

Goal: Theorem 4 (p. 18)

For every FCFS-feasible schedule $y$ and every $N \ge 1$,

$$C(y) \ \ge\ \lambda\, \mathbb E\Big[\frac{\gamma_{1:N}(\omega)}{N}\Big].$$

The paper writes the left side as $C^{\pi^*}$, the optimal cost. The statement here holds for every schedule, so it covers the optimum whenever one exists.

Milestones (in the order of the printed proof, pp. 18–19)

1. Sample-path bound: $\gamma_{1:M}(\omega)/M \le \sum_{n=1}^M g(D_n - d_n)/M$ on every path.
2. (14): $\limsup_M \lambda\, \mathbb E[\gamma_{1:M}/M] \le C(y)$.
3. Superadditivity: $\gamma_{1:2N}(\omega) \ge \gamma_{1:N}(\omega) + \gamma_{N+1:2N}(\omega)$.
4. Block stationarity: $\mathbb E[\gamma_{1:N}] = \mathbb E[\gamma_{N+1:2N}]$.
5. Doubling: $\mathbb E[\gamma_{1:2N}] \ge 2\,\mathbb E[\gamma_{1:N}]$.
6. Dyadic bound: $k \mapsto \mathbb E[\gamma_{1:2^kN}/2^kN]$ is non-decreasing and $\mathbb E[\gamma_{1:N}/N] \le \limsup_k \mathbb E[\gamma_{1:2^kN}/2^kN]$.
7. (15): $\mathbb E[\gamma_{1:N}/N] \le \limsup_M \mathbb E[\gamma_{1:M}/M]$.

Significance

The result. Theorem 4 turns an infinite-horizon lower bound into a finite computation: for any $N$, the deterministic clairvoyant problem over $N$ customers can be solved on simulated sample paths, and the sample mean, scaled by $\lambda$, estimates a lower bound on the optimal long-run cost. The paper uses this bound, with its refinements (Theorems 5 and 6), to certify the numerical quality of its threshold policies (§7). Without it, the only available benchmark is the asymptotic clairvoyant cost, which cannot be computed.

Formalizing it. The paper proves the theorem with an informal argument. No machine-checked proof of this bound, or of the sample-path GI/G/1 objects it needs, is known to exist. The mission produces a sample-path model of a single-server queue with due dates, a clairvoyant value defined as an extended-real infimum, and the measure-theoretic step that the clairvoyant cost of a block of customers has the same expectation as that of the first block.

Difficulty

Most steps are monotonicity of integrals and of $\limsup$. The substantive step is block stationarity (milestone 4). $\gamma_{N+1:2N}$ and $\gamma_{1:N}$ are not functions of the same random variables, and $\gamma_{N+1:2N}$ depends on the absolute arrival times $t_{N+1}, \dots, t_{2N}$, which carry the whole history $T_1, \dots, T_N$. The equality of expectations needs the clairvoyant value to be expressed as a function of relative arrival times and service times only. It also needs that function to be measurable (it is an infimum over uncountably many schedules) and the joint law of a block of an i.i.d. family to be invariant under shifting the block. The doubling argument then has to pass from horizons $2^kN$ to all horizons $M$, which in the extended reals needs no integrability.

Formalization scope

• Source. The statements follow the SSRN author version of 2021-08-05 (abstract 3557605), whose page and equation numbers are cited throughout; the published article's numbering is not used.
• Indices start at $1$: $t_n = T_1 + \cdots + T_n$; the coordinates $T_0, x_0$ are unused and carry no hypothesis. $N \ge 1$ in the goal, in the dyadic bound and in (15) (the paper's $\mathbb N$ starts at $1$; the ratios are $0/0$ at $N = 0$).
• Sample paths. The outcome $\omega$ is the full sample path of inter-arrival and service times; the page calls it "a sample path of inter-arrival times" on p. 18 and "of inter-arrival and service times" on p. 19.
• Policy class. The paper's admissible, FCFS and Loynes stable policy classes are not modelled. The Loynes class asks for $L^1$ convergence of the waiting times $W^\pi_n$. For a nondegenerate GI/G/1 queue these converge only in law, so the class may be empty, and an infimum over it would be vacuous. Every statement instead quantifies over all schedules that are FCFS-feasible on every sample path. That class contains every policy the paper considers, so the statements imply the paper's. No measurability or adaptedness of $y$ is required: the bound holds without it.
• Cost. $C(y)$ is defined by the per-customer form (4), not by the calendar-time form (1); the paper passes from (1) to (4) by citing Whitt (1991), and the proof of Theorem 4 uses (4) only.
• Extended reals. $\gamma$ is an infimum in $[0, \infty]$ (the page writes $\min$, which is attained but not proved to be). Costs, expectations (lower Lebesgue integrals) and $\limsup$s are in $[0, \infty]$. Each cost term is $\max(g, 0)$, which is exact because $g \ge 0$.
• Standing assumptions. The paper leaves some conditions implicit; they are made explicit: durations are nonnegative almost surely, $\delta, c_e, c_d \ge 0$, and "mean $1/\lambda$, mean $1/\mu$" means $0 < \mathbb E[T_1] < \infty$ and $0 < \mathbb E[x_1] < \infty$. Stability $\lambda < \mu$ ($\mathbb E[x_1] < \mathbb E[T_1]$) is kept as the paper's standing assumption although Theorem 4 does not use it. A one-point model ($T \equiv 1$, $x \equiv 1/2$, $\delta = c_e = c_d = 1$) satisfies all of them and has finite $\gamma_{1:N}$.
• Ruled out. A real-valued $\gamma$, cost, expectation or $\limsup$ (junk value $0$ on unbounded or non-integrable input); a policy class that may be empty; dropping the i.i.d. or independence hypotheses (milestone 4 and the goal fail without them); $N = 0$; and $\lambda$ as a free parameter (it is $1/\mathbb E[T_1]$).
• Infrastructure. A complete development needs measurability of the clairvoyant value, invariance of block laws for i.i.d. families, and the comparison of a $\limsup$ along a subsequence with the full $\limsup$ in $[0, \infty]$. The block-law invariance and the sample-path queue model can be reused in other missions. Proofs of any milestone, and lemmas towards milestone 4, are welcome.

Selected references

• M. H. Farahani, M. Dawande, G. Janakiraman, Order Now, Pickup in 30 Minutes: Managing Queues with Static Delivery Guarantees, SSRN 3557605, version of 2021-08-05; published in Operations Research, 2022. https://ssrn.com/abstract=3557605, https://doi.org/10.1287/opre.2021.2203
• D. B. Brown, J. E. Smith, P. Sun, Information relaxations and duality in stochastic dynamic programs, Operations Research 58(4), 785–801, 2010. https://doi.org/10.1287/opre.1090.0796
• D. B. Brown, M. B. Haugh, Information relaxation bounds for infinite horizon Markov decision processes, Operations Research 65(5), 1355–1379, 2017. https://doi.org/10.1287/opre.2017.1631
• R. M. Loynes, The stability of a queue with non-independent inter-arrival and service times, Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 497–520, 1962. https://doi.org/10.1017/S0305004100036094
• W. Whitt, A review of L = λW and extensions, Queueing Systems 9(3), 235–268, 1991. https://doi.org/10.1007/BF01158466

Motivation

Convex optimization often minimizes a function obtained by applying one convex function to the output of another map. The inner map may be vector valued, and its components need not be linear. To understand sensitivity, optimality conditions, and dual formulations for such a convex composite, one needs its Fenchel conjugate. Standard formulas for an affine inner map do not directly describe a nonlinear, partially defined map. Burke, Hoheisel, and Nguyen treat this setting in finite-dimensional Euclidean spaces and identify conditions under which the conjugate has an exact, attained representation over a polar cone (Burke–Hoheisel–Nguyen, pp. 3, 10).

The paper distinguishes monotonicity of the outer function along the particular epigraph of the inner map from monotonicity throughout the entire cone order. This matters when the outer function behaves well on the points the inner map can reach but does not satisfy a stronger global condition. Its Theorem 12 gives a conjugacy formula under a point-based condition on relative interiors; subsequent results use it to describe subgradients and additive composites (Burke–Hoheisel–Nguyen, pp. 8, 10–13). The mission isolates the conjugacy theorem and the source results that support it.

Setting

Let $E_1$ and $E_2$ be finite-dimensional real inner-product spaces. A closed convex cone $K\subseteq E_2$ defines the relation $u\le_K v$ when $v-u\in K$. Its polar cone is $K^\circ=\{v:\langle v,k\rangle\le0\text{ for all }k\in K\}$. A possibly partial map $F:E_1\to E_2^\bullet$, where $E_2^\bullet$ adjoins one formal value $+\infty^\bullet$, has an effective domain $D=\operatorname{dom}F$ on which its values lie in $E_2$. Its $K$-epigraph is

$$K\text{-epi}F=\{(x,y)\in E_1\times E_2:x\in D,\ y-F(x)\in K\}.$$

The map $F$ is $K$-convex when this set is convex. The paper assumes throughout §4 that $D$ is nonempty (Burke–Hoheisel–Nguyen, pp. 6, 10).

The outer function $g:E_2\to\mathbb R\cup\{+\infty\}$ belongs to $\Gamma(E_2)$: it is proper and convex but need not be lower semicontinuous. The composite $g\circ F$ equals $g(F(x))$ on $D$ and $+\infty$ outside $D$. The key monotonicity condition, numbered (7), is $g(F(x))\le g(y)$ whenever $(x,y)\in K\text{-epi}F$. It is restricted to the epigraph of $F$, unlike global $K$-increasingness (Burke–Hoheisel–Nguyen, pp. 6, 8).

For an extended-real function $f$, the Fenchel conjugate is $f^*(p)=\sup_x\{\langle p,x\rangle-f(x)\}$. The scalarization $\langle v,F\rangle$ takes value $\langle v,F(x)\rangle$ on $D$ and $+\infty$ elsewhere. Its conjugate and the conjugate $g^*$ are combined in the dual function

$$\eta(p)=\inf_{v\in-K^\circ}\bigl\{g^*(v)+\langle v,F\rangle^*(p)\bigr\}.$$

Here $\operatorname{ri}$ means interior relative to the affine hull, and $\operatorname{dom}f$ means the set where $f$ is finite (Burke–Hoheisel–Nguyen, pp. 4, 6, 10).

Formalization targets

The goal is Theorem 12(c). Suppose $K$ is a closed convex cone, $F$ is proper and $K$-convex, $g\in\Gamma(E_2)$ satisfies (7), and the Slater-type condition (10) holds:

$$F(\operatorname{ri}D)\cap\operatorname{ri}(\operatorname{dom}g-K)\ne\varnothing.$$

Then the formula has an actual minimizer at every $p\in E_1$ and the effective domain has an exact description:

$$(g\circ F)^*(p)=\min_{v\in-K^\circ}\bigl\{g^*(v)+\langle v,F\rangle^*(p)\bigr\},$$ $$\operatorname{dom}(g\circ F)^*=\{p:\exists v\in\operatorname{dom}g^*\cap(-K^\circ),\ \langle v,F\rangle^*(p)<+\infty\}.$$

The milestones follow results stated in the paper: Theorem 2 on conjugacy and infimal convolution; Lemma 6 on support functions; Lemma 4 on the relative interior of a $K$-epigraph; and parts (a) and (b) of Theorem 12, which establish a closure bound and properness with attainment for $\eta$ (Burke–Hoheisel–Nguyen, pp. 5–7, 10).

Significance

The theorem turns the conjugate of a nonlinear composite into a minimization over the negative polar cone. It also identifies exactly which dual arguments give a finite value. Attainment matters because later subgradient formulas can use a specific minimizing multiplier rather than only an approximating sequence. In this paper, Theorem 12 is followed by a subdifferential formula for $g\circ F$ and a formula for the additive composite $f+g\circ F$ (Burke–Hoheisel–Nguyen, pp. 10–13).

The mathematical theorem is proved in the source paper. The formalization task is to give its statement a machine-checkable meaning and then prove that statement from a reusable collection of facts about extended-real conjugacy, support functions, cones, and relative interiors. The imported definitions of conjugacy and closed convex cones already have published formal interfaces; the paper-specific definitions and theorems in this mission are draft statements and do not yet have machine-checked proofs.

Difficulty

The main obstruction is the interaction between closure and conjugacy of a sum. A direct interchange of a supremum over primal points and an infimum over cone multipliers does not itself establish equality or the existence of a minimizing multiplier. Theorem 2 supplies a finite-dimensional conjugacy rule under a relative-interior qualification, while Lemma 4 identifies the relative interior of the relevant epigraph. The source then needs to account for the extended-real values of a partial map and for an outer function that is convex but may not be lower semicontinuous (Burke–Hoheisel–Nguyen, pp. 5–6, 10–11).

Formalization scope

The Lean model uses finite-dimensional real inner-product spaces and EReal for extended-real values. The partial map $F$ is a pair $(D,F)$: $D$ is its domain, and values of the total representative $F$ outside $D$ are ignored. Properness of $F$ is the explicit hypothesis $D\ne\varnothing$. The effective domain of an extended-real function excludes $+\infty$; this corrects a printed $\le+\infty$ in the paper's definition. Conjugacy, epigraph convexity, $\Gamma_0$, closed convex cones, and polar cones reuse published definitions. The lower semicontinuous hull follows the paper's sequential-limit definition, and $\operatorname{ri}$ is Mathlib's intrinsic interior. Pairings on $E_1\times E_2$ are sums of the two component inner products.

The theorem keeps the infimum and minimizer inside $-K^\circ$, uses relative rather than ordinary interior in (10), and retains the properness and finite-dimensional hypotheses. These conventions prevent a vacuous or weaker encoding. Attainment is a separate existential statement, including the case where the minimum is $+\infty$. The printed $\Gamma_0(E_2)$ in Theorem 12(a)'s scalarization clause is read as $\Gamma_0(E_1)$ because each scalarization has domain $E_1$; the paper's Lemma 10 uses that same space. Theorem 2's closure identity is stated under the added hypothesis $\operatorname{dom}(\operatorname{cl}f)\cap\operatorname{dom}(\operatorname{cl}g)\ne\varnothing$. With the paper's definition of $\operatorname{cl}$ as the lower semicontinuous hull, the unconditional identity fails when $\operatorname{cl}f+\operatorname{cl}g\equiv+\infty$. The cited source theorem uses a closure that is identically $-\infty$ for improper functions.

The mission develops the definitions of effective domain, closure, infimal convolution, indicators and support functions, $K$-epigraphs, scalarizations, condition (7), and $\eta$. Contributions proving the listed milestones or building general lemmas for those definitions are in scope. Corollaries 14 and 16, the other corollaries of §4, and the applications of §5 are outside this mission (Burke–Hoheisel–Nguyen, pp. 11–27).

Selected references

• J. V. Burke, T. Hoheisel, and Q. V. Nguyen, A Study of Convex Convex-Composite Functions via Infimal Convolution with Applications, Mathematics of Operations Research (2021), read as arXiv:1907.08318v2.

Motivation

A buyer may be liable for social responsibility violations among suppliers that remain in its production network. Auditing can prevent a later penalty, but the buyer must pay for each audit and then choose what to do with a supplier that fails. Dropping a supplier can also remove other firms that depend on it, changing the buyer's eventual production profit. Zhang, Aydin, and Parker study this decision in a three-tier supply network and establish a structural rule for an optimal auditing policy in Theorem 3. The rule tells the buyer how dropping and rectification can be ordered without specifying which supplier to audit first.

Setting

There is one buyer in tier 0 and two possible tier-1 firms, $a$ and $b$. The tier-2 suppliers are divided into three disjoint sets: $S_a$, whose members supply only $a$; $S_b$, whose members supply only $b$; and $S_{ab}$, whose members supply both. A network is $g=(S^{(1)},S_a,S_b,S_{ab})$, where $S^{(1)}\subseteq\{a,b\}$ is the set of tier-1 firms still present. Its supplier set $S_g$ contains those tier-1 firms and the members of the three tier-2 sets. The set $D_g(i)$ of dependents of supplier $i$ includes $i$ itself. For a tier-1 firm, it includes its exclusive tier-2 suppliers. For a tier-2 supplier, it also includes a tier-1 firm if that supplier is the firm's sole remaining tier-2 source.

An auditing state $\gamma=(g,U_\gamma)$ records the current network and its finite set of unaudited suppliers, $U_\gamma\subseteq S_g$. The state is terminal when $U_\gamma=\varnothing$. The operator $\gamma\oplus i$ vets an unaudited supplier without changing the network. The operator $\gamma\ominus i$ drops $i$ and $D_g(i)$. If a tier-1 firm is dropped, its formerly shared tier-2 suppliers become exclusive to the other tier-1 firm. These transitions are the paper's footnotes 3 and 4 on page 10.

At a state, the buyer can proceed to production ($pp$), audit and rectify an unaudited supplier ($ar(i)$), or audit and drop one if it fails ($ad(i)$). An auditing policy $\xi$ chooses an admissible action at every state. Let $a\geq0$ be the audit cost, $r\geq0$ the rectification cost, $u\in(0,1)$ the chance that a supplier is noncompliant, $w\in(0,1]$ the chance that an uncorrected violation is exposed, and $z\geq0$ the penalty for an exposed violation. If the buyer proceeds to production, it receives production profit $\pi(g)$ less the expected penalty $\zeta(\gamma)=|U_\gamma|uwz$.

The optimal value $V^*(\gamma)$ is the maximum of the values of the admissible actions at $\gamma$, using the finite recursion (1)–(5) of §3.2. An optimal policy chooses a maximizing action at every state. The appendix also defines the value $V(\xi,\gamma)$ of a fixed policy and the restricted value $V_{ar}(\gamma)$ when only $pp$ and $ar$ are available.

Formalization targets

The main target is Theorem 3, page 19: some optimal policy first audits and drops any number of suppliers, perhaps none, and then enters a second subphase. In that second subphase it either rectifies all remaining unaudited suppliers, in any order, or proceeds directly to production. The choice is governed by the comparison

$$a+ur\leq uwz\quad\text{(rectify all)},\qquad a+ur\geq uwz\quad\text{(proceed to production)}.$$

The inequalities are non-strict: both choices are permitted at equality. The statement applies at every state of the auditing process. Once the policy rectifies a supplier, it rectifies another at the successor state whenever unaudited suppliers remain; no later audit-and-drop action follows. Every available rectification action is optimal during this subphase.

Two appendix results are the milestones. Proposition D.1, OA-11 says that, for each starting state, a buyer can postpone rectification actions until after dropping actions without lowering its value at that state. Proposition D.2, OA-13 identifies the optimal value and actions in the restricted rectify-or-produce problem. With $c_{rp}=\min\{uwz,a+ur\}$, its value formula is

$$V_{ar}(\gamma)=\pi(g)-c_{rp}|U_\gamma|.$$

Significance

Theorem 3 reduces the form of policies that need consideration: rectification need not be interleaved with later dropping, and the final choice between rectification and accepting exposure risk depends on one comparison of per-supplier costs. It does not resolve which suppliers to audit and drop, or when to leave that first subphase. Those decisions can still depend on the network and audit outcomes, as §5.1 explains.

The paper proves the structural result and its two appendix propositions. This mission asks for machine-checked proofs of those known statements, together with a reusable finite representation of network dependents, transitions, and Bellman values. The present draft statements compile with proof placeholders; they are not machine-checked proofs of the claims. The definitions also permit later work on other auditing rules over the same state space.

Difficulty

An audit-and-drop action can change the network and therefore production profit. Comparing it with an audit-and-rectify action is more involved than comparing their immediate costs: a dropped supplier can remove its dependents, and those losses affect all later decisions. The obvious choice of rectifying whenever $a+ur\leq uwz$ ignores the possibility that a later drop removes the rectified supplier anyway. The structural theorem must account for both successor states of an audit and still produce one policy that is optimal at every state.

Formalization scope

Tier-2 suppliers carry labels in an arbitrary type, while every individual network and unaudited set is finite. The tier-2 components of a network are pairwise disjoint. The Lean parameters explicitly require $a,r,z\geq0$, $0<u<1$, and $0<w\leq1$. The paper derives $\zeta$ from independent supplier outcomes; the formalization uses that derived formula, and its Bellman recursions already take the audit outcomes' expectations. The profit $\pi$ is any real-valued function of the current network. This is a disclosed generalization of the Cournot profit used earlier in the paper: §6.1 says the two-subphase result does not depend on the mode of competition, and (D.27) uses only that vetting leaves the network unchanged.

The value functions are defined by recursion on the number of unaudited suppliers. Their maxima are taken over exactly the admissible finite action set, and optimality is checked at every state. Transition functions are total, but the theorems use them only for unaudited suppliers. The action-value functions return zero for inadmissible supplier actions; the fixed-policy recursion returns the production value there. These values have no role for admissible policies. The formulation excludes an unattained policy supremum, a policy that is optimal only at a chosen initial state, or a special production-profit function. Contributions that establish the appendix propositions, the main structural theorem, or useful lemmas about the finite transitions and recursions fit this scope.

Selected references

• H. Zhang, G. Aydin, and R. P. Parker, Social Responsibility Auditing in Supply Chain Networks, Management Science, 2021, authors' accepted manuscript dated 26 February 2021, pp. 8–11, 19, OA-11–OA-13. DOI: 10.1287/mnsc.2020.3950.

Motivation

A constrained optimization problem often has an objective of the form $\varphi(x)=\vartheta(f(x))$: a smooth map $f$ describes the model, while an extended-real function $\vartheta$ gives the cost and can assign $+\infty$ to infeasible outputs. Such a description covers polyhedral constraints, quadratic penalties on pieces, and many nonsmooth composite objectives. Solvers need to know how the local first and second order behavior of $\varphi$ depends on the two parts of the model. The usual chain rules in Rockafellar and Wets, Variational Analysis use qualification conditions stronger than an error bound at the point of interest. Mohammadi, Mordukhovich, and Sarabi develop chain rules under a metric subregularity qualification condition (MSQC), including the second order result targeted here.

The paper was circulated as arXiv:1905.08837v2 in 2019 and published in Mathematics of Operations Research in 2022. This mission follows the pinned arXiv version, whose theorem and page numbering is used throughout. The result is known in mathematics; the open task here is its formalization in Lean. The paper also derives optimality conditions and statements about KKT systems from its second order analysis, but those later applications are outside this mission's target. Source: §§1, 5, 6, 8.

Setting

Fix finite dimensional Euclidean spaces $\mathbb R^n$ and $\mathbb R^m$. An extended-real function $\varphi:\mathbb R^n\to(-\infty,+\infty]$ has finite domain $\operatorname{dom}\varphi=\{x:\varphi(x)<+\infty\}$. Assigning $+\infty$ outside a feasible set lets an ordinary function and a constraint be treated together. A convex piecewise linear-quadratic function (PWLQ) $\vartheta$ has a finite collection of polyhedral convex pieces $\Omega_i$ whose union is its domain. On each piece its value is $\tfrac12\langle A_i y,y\rangle+\langle a_i,y\rangle+\alpha_i$, where $A_i$ is symmetric. The separate formulas must agree where pieces meet, because all describe the same function. Source: (2.9), p. 5.

A function $\varphi$ is fully subamenable at $\bar x$ when it agrees with $\vartheta\circ f$ on a neighborhood of $\bar x$, with $f$ twice differentiable at $\bar x$, $\vartheta$ convex PWLQ, and MSQC satisfied there. Write $\Omega=\{x:f(x)\in\operatorname{dom}\vartheta\}$. MSQC says that for some $\kappa\ge0$ and all $x$ near $\bar x$, $\operatorname{dist}(x,\Omega)\le\kappa\operatorname{dist}(f(x),\operatorname{dom}\vartheta)$. This controls how far a nearby point is from feasibility through its residual in the outer domain. It is the paper's condition (3.5), not metric regularity. Source: Definition 3.2 and (3.5), pp. 9–10; Definition 4.2, p. 16.

The subderivative $d\varphi(\bar x)(w)$ is a lower limit of first order difference quotients as positive time tends to zero and the direction tends to $w$. Given a limiting subgradient $\bar v\in\partial\varphi(\bar x)$, the second subderivative $d^2\varphi(\bar x,\bar v)(w)$ uses the quotient after subtracting the linear term $t\langle\bar v,w\rangle$ and dividing by $\tfrac12t^2$. Proper twice epi-differentiability means these quotients epi-converge to a second subderivative that never equals $-\infty$ and is finite somewhere. The paper gives an equivalent test using recovery directions for every positive null sequence; that test is used in Lean. Source: (2.11), (2.15), (2.16), pp. 6–7.

Formalization targets

Main theorem

For every $\bar v\in\partial\varphi(\bar x)$, a fully subamenable $\varphi$ is properly twice epi-differentiable at $\bar x$ for $\bar v$. With

$$\Lambda(\bar x,\bar v)=\{\lambda\in\partial\vartheta(f(\bar x)):\nabla f(\bar x)^*\lambda=\bar v\},$$

its second subderivative satisfies, for every $w\in\mathbb R^n$,

$$d^2\varphi(\bar x,\bar v)(w)=\max_{\lambda\in\Lambda(\bar x,\bar v)}\bigl\{d^2\vartheta(f(\bar x),\lambda)(\nabla f(\bar x)w)+\langle\lambda,\nabla^2f(\bar x)(w,w)\rangle\bigr\}.$$

The maximum is attained; a supremum alone is a weaker claim. This is Theorem 5.2 and (5.3), p. 22.

Supporting statements

The milestones are the paper's equality rules for first order subderivatives and subgradients (Theorems 3.4 and 3.6), its identification of critical directions with the finite domain of the second subderivative (Theorem 4.4), the PWLQ outer-function formula (4.8), the lower bound (4.10), and the parabolic limit formula (Lemma 5.1). Each names a separate mathematical claim needed to connect the composite model to the goal. Source: §§3–5.

Significance

Theorem 5.2 gives a data-level way to evaluate the second order behavior of a nonsmooth composite: the outer function contributes its own second subderivative, the inner map contributes its Hessian, and multipliers connect the two. Its properness and epi-differentiability clauses make the formula suitable for the paper's later no-gap second order optimality conditions and parametric analysis. Without those clauses, an equality of extended-real expressions alone would not establish the stability of the difference quotients. Source: Theorem 5.2 and §6.

A formal development of this result would add reusable definitions and lemmas for extended-real difference quotients, second-order tangent geometry, PWLQ functions, and local composite error bounds. The present draft contains statements and definitions that compile; it does not yet contain proofs of the open theorem items. The published limiting-subdifferential definition is reused, while the paper-specific local representation and multiplier set are defined here.

Difficulty

A first order expansion of $f$ does not settle the second order claim. Near a polyhedral boundary, the direction $w$ may be tangent while a fixed straight path $\bar x+tw$ leaves the domain; the second-order correction and the outer function's active piece matter. MSQC controls distance to feasibility but does not itself identify a feasible second-order path or a maximizing multiplier. The source therefore needs separate results about critical directions, PWLQ second subderivatives, parabolic limits, and dual attainment before the full formula can be stated with a maximum. Source: §§4–5, especially pp. 17–23.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin n) and EReal. The paper's codomain excludes $-\infty$; the relevant hypotheses enforce that exclusion, while the subderivatives themselves may take either infinite value. The finite domain is defined by exclusion of $+\infty$. A PWLQ representation records finite closed half-space intersections, symmetric operators, and the exact $\tfrac12$ quadratic coefficient. Twice differentiability includes differentiability near the base point and differentiability of the derivative at the point. The composite identity holds on a neighborhood rather than globally. MSQC uses the paper's local distance estimate with $\kappa\ge0$. Positive null sequences represent $t\downarrow0$; a filter lower limit represents the varying direction. The second quotient retains the paper's $\tfrac12t^2$ denominator.

The subdifferentials are the published analytic regular and limiting subdifferentials. Their use matches the paper's geometric subdifferentials at the lower semicontinuous functions in these statements. The goal computes the second subderivative from the lower-limit definition, rather than defining it by (5.3). Full subamenability retains MSQC and a genuine PWLQ representation; it is neither an empty-domain case nor a stronger metric-regularity special case. Contributions toward proofs of the milestone theorems, their needed tangent-set geometry, and the goal are in scope.

Selected references

• A. Mohammadi, B. S. Mordukhovich, M. E. Sarabi, Variational Analysis of Composite Models with Applications to Continuous Optimization, arXiv:1905.08837v2, 2019; published in Mathematics of Operations Research, 2022. https://arxiv.org/abs/1905.08837v2
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

Online and omni-channel retailers promise delivery within a fixed number of days, and carriers charge less for slower service. A retailer that receives orders over time can therefore wait, collect several orders into one package, and send it by a slower and cheaper service, as long as no order misses its promised date. Waiting saves the fixed cost of a shipment but uses up the slack of the orders already waiting. This trade-off between shipment consolidation and expedited delivery is the subject of L. Wei, R. Kapuscinski and S. Jasin, Shipping Consolidation across Two Warehouses with Delivery Deadline and Expedited Options for E-commerce and Omni-channel Retailers (Manufacturing & Service Operations Management, 2020; author's manuscript SSRN 2920899).

The paper treats one and two warehouses, with fixed and with volume-dependent shipping costs. Its first structural result concerns the simplest case, one warehouse and a fixed cost per package: the optimal policy waits while the most urgent order has enough slack and ships everything once the slack falls to a period-dependent threshold. This mission formalizes that result and the lemmas its proof rests on.

Setting

Time is discrete and counted backward: $t$ is the number of periods to go and period $1$ is the last. Each order must be delivered at most $d \ge 1$ periods after it arrives. The slack time of a pending order is the number of periods left until its deadline; slack $1$ means the order must leave now.

Shipping a package that must arrive within $p$ periods costs $F(p)$, the fixed shipping cost, which does not depend on the number of orders in the package. The paper assumes $F$ is non-increasing and convex (slower delivery is cheaper, with diminishing savings), and specifies it on $[1,\infty)$. In each period new orders arrive with probability $\alpha \in [0,1]$.

With one warehouse and fixed costs, the paper's Lemma 1 shows that it is optimal either to ship all pending orders together in one package or to ship none, at a cost depending only on the smallest slack $z$ among pending orders. The state is therefore $z \in \{1,\dots,d\}$, or $\infty$ when nothing is pending. The cost-to-go functions $V_t(z)$ and $V_t(\infty)$ satisfy the recursion (2)–(3): for $t > 1$ and $1 \le z \le d$,

$$V_t(z) = \min\{\,F(z) + V_t(\infty)\ \text{(ship)},\ \ V_{t-1}(z-1)\ \text{(do not ship)}\,\},$$ $$V_t(\infty) = \alpha V_{t-1}(d) + (1-\alpha) V_{t-1}(\infty),$$

with $V_1(z) = F(z)$ and $V_1(\infty) = 0$. Holding is infeasible at $z = 1$. Shipping is optimal at $(t,z)$ when the ship branch attains the minimum; holding is optimal when it is feasible and the do-not-ship branch attains the minimum. With ties both are optimal.

Formalization targets

Goal: Theorem 1 (p. 13)

For every period $t \ge 1$ there is an integer $\tau_t$ such that, for every slack $1 \le z \le d$,

$$z \le \tau_t \implies \text{shipping all pending orders is optimal}, \qquad z > \tau_t \implies \text{holding all pending orders is optimal}.$$

The threshold may depend on $t$, and no formula for it is asserted.

Milestones

1. Lemma E1 (Online Appendix, p. 1). For reals $a_1,\dots,a_n$ and $b_1 \ge \dots \ge b_n$,

$$\min_i (a_i + b_i) - \min_i a_i \ \ge\ b_n.$$

2. Unrolled cost-to-go (proof of Lemma 2, Online Appendix, p. 1). For $t \ge 1$ and $1 \le z \le d$,

$$V_t(z) = \min_{0 \le j \le k} \{F(z-j) + V_{t-j}(\infty)\}, \qquad k = \min\{t,z\} - 1.$$

3. Lemma 2 (p. 13). For $t \ge 1$ and $2 \le z \le d$,

$$V_t(z-1) - V_t(z) \ \ge\ F(z-1) - F(z).$$

4. The downward step (proof of Theorem 1, p. 13). For $t \ge 2$ and $3 \le z \le d$, if shipping is optimal at slack $z$, it is optimal at slack $z-1$.

Significance

Theorem 1 reduces the policy of a $T$-period stochastic control problem to one integer per period. The paper builds on it: Theorem 2 computes the long-run average cost of a constant threshold, Proposition 2 and Lemma 3 describe the best constant threshold, and the two-warehouse analysis of §5 and the heuristics of §7 start from this one-warehouse structure. Lemma 2 states that the cost-to-go reacts to a loss of slack at least as strongly as the current shipping cost does, which the paper calls counter-intuitive (p. 13); it is the property that makes the threshold exist.

The results are proved in the paper, with one gap: the proof of Lemma 2 is written out only for $t \ge d$, and the case $t < d$ is described as similar and omitted. A formal proof closes that case. To the best of our knowledge none of these results has a machine-checked proof.

Difficulty

The natural first idea is to argue that the cost-to-go $V_t(z)$ inherits convexity in $z$ from $F$ and then read off a threshold. That is not what is needed: the threshold needs a comparison between the slope of $V_t$ and the slope of $F$ (Lemma 2), and the paper notes (p. 13) that, without further structure, the difference $V_t(z-1) - V_t(z)$ can a priori be larger or smaller than $F(z-1) - F(z)$, because the optimal shipping periods for slacks $z-1$ and $z$ may differ. The recursion couples two indices, period and slack, through the no-order value $V_t(\infty)$, and its boundary cases ($z = 1$, where shipping is forced, and $t = 1$, the last period) behave differently from the interior. The paper's own argument covers only $t \ge d$; the regime $t < d$, in which the horizon ends before the most urgent order's deadline, is left to the reader.

Formalization scope

• Model. The model is the reduced recursion (2)–(3) itself, encoded as a recursive definition valuePair F α d t returning $(z \mapsto V_t(z), V_t(\infty))$. The reduction from the general dynamic program (1) over all slack vectors to (2)–(3) (Lemma 1) is not formalized; $z$ stands for the smallest slack among pending orders. All objects are deterministic; $\alpha$ enters only through (3).
• Conventions. Periods are counted down, $t \ge 1$. $V_1(\infty) = 0$ (from (1): nothing pending costs nothing in the last period). The boundary condition $V_{t-1}(0) = \infty$ is encoded as a forced shipment at $z = 1$. Every statement is restricted to $1 \le z \le d$, the domain of (2); values outside it, and at $t = 0$, are placeholders. $F : \mathbb R \to \mathbb R$ is real-valued, assumed convex and non-increasing on $[1,\infty)$, and evaluated only at integers $z \ge 1$; the paper's $F(0) = \infty$ is never read and is not encoded.
• Optimality. A decision is optimal when its branch of (2) attains the minimum; ties make both decisions optimal. Holding is optimal only if it is feasible ($t \ge 2$, $z \ge 2$).
• Ruling out a trivial goal. Shipping is always optimal at $z = 1$, so "there is a threshold below which shipping is optimal" holds with $\tau = 1$ for free; the goal also requires holding to be optimal at every slack above the threshold.
• Not formalized. Lemma 1, Proposition 1, Theorem 2 and the results that rest on it (Proposition 2, Lemma 3), the two-warehouse results of §5, the variable-cost model of §6, and the heuristic bounds of §7.
• Infrastructure. Only Finset.inf', ConvexOn and natural-number arithmetic are needed. Lemma E1 is a self-contained fact about finite minima and may be reusable. Alternative proofs of Lemma 2 that avoid the unrolled form are welcome.

Selected references

• L. Wei, R. Kapuscinski, S. Jasin, Shipping Consolidation across Two Warehouses with Delivery Deadline and Expedited Options for E-commerce and Omni-channel Retailers, Manufacturing & Service Operations Management, 2020. https://doi.org/10.1287/msom.2020.0903 — author's manuscript: https://ssrn.com/abstract=2920899

Motivation

The apparel industry is a large source of carbon emissions, water use and landfill waste, and much of that footprint comes from garments being discarded early. Fast-fashion retailers such as Zara and H&M combine two operational choices: they offer a very large number of styles each season, and they replenish the styles that turn out to be popular through quick response, i.e. production during the selling season at a higher unit cost. Their garments are also widely reported to be of low quality, which shortens their useful life and reduces the chance of reuse.

X. Long and J. Nasiry, Sustainability in the Fast Fashion Industry (SSRN 3486502; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2021.1054), give an operational explanation of low quality: it is driven by the firm's incentive to offer variety. The paper's headline (abstract, and the first sentence of its conclusion) is that when variety is chosen by the firm, quality falls as consumers become more sensitive to fashion or as introducing new styles gets cheaper. This mission formalizes that result and the chain of propositions leading to it.

Setting

A firm sells one season of a fashion product. Before the season it chooses a number of styles $m\ge 1$ (design cost $\beta m$), a common quality $u\ge 0$, and an inventory $q$ per style produced at unit cost $\tfrac k2u^2$. Styles are points on a circle of unit circumference (Salop's circular city). During the season, a trend $x$ uniform on the circle and a market size $n\sim U(0,\bar n)$ are realised. All $n$ consumers buy the style $t^*$ closest to the trend at their valuation

$$p=a+\theta u+\gamma\Big(\tfrac12-|t^*-x|\Big),$$

where $|t^*-x|$ is the arc distance, $a$ is a base value, and $\theta$ and $\gamma$ measure the sensitivity to quality and to fashion. Demand above $q$ is met by quick response at unit cost $\tfrac{k'}2u^2$ with $k'>k$; unsold units of the other styles are wasted.

The paper shows that equally spaced styles are optimal (Lemma 1), computes the expected price $a+\theta u+\gamma/2-\gamma/(4m)$ and the expected quick-response volume $(\bar n-q)^2/(2\bar n)$, and arrives at the firm's problem (1):

$$\max_{m\ge1,\ u\ge0,\ 0\le q\le\bar n}\ \mathbb E\Pi(m,u,q)=\Big(a+\theta u+\frac\gamma2-\frac{\gamma}{4m}\Big)\frac{\bar n}{2}-m\frac k2u^2q-\frac{k'}2u^2\frac{(\bar n-q)^2}{2\bar n}-\beta m .$$

An optimal solution $(m^*,u^*,q^*)$ is a feasible triple with the largest expected profit. The parameters satisfy $0<k<k'$ and $\theta,\gamma,\beta,\bar n>0$; $a$ is any real number.

Formalization targets

Goal: Proposition 4(ii)

For admissible parameters, problem (1) has an optimal solution, and

$$u^*\ \text{decreases in }\gamma,\qquad u^*\ \text{increases in }\beta,\qquad u^*\ \text{decreases in }\bar n,$$

where each comparison changes one parameter, keeps the others fixed, and holds between every optimal solution before the change and every optimal solution after it. Monotonicity is weak: on part of the parameter space the optimal quality does not move.

Milestones

In attack order:

1. the stochastic model reduces to (1): Lemma 1, the expected price, and the two uniform expectations (p. 10–11);
2. for fixed $m$: the optimal inventory $\hat q$ (p. 14), and Proposition 2, which gives the optimal quality $\hat u(m)$, the optimal inventory and the value of (1). For $m>k'/k$ these are $\hat u=\theta/k'$ and $\hat q=0$; for $m\le k'/k$ they are $\hat u=\theta k'/(mk(2k'-mk))$ and $\hat q=\bar n(1-mk/k')$. Proposition 2(iii) adds that $\hat u$ decreases in $m$ and $k'$;
3. the optimal variety: Proposition 3 locates $m^*$ in three ranges of $\gamma$. It is $1$, $\sqrt{\bar n\gamma/(8\beta)}$, or an interior root $m_E\in[1,k'/k]$, with explicit thresholds in $\gamma$ and $\beta$;
4. Proposition 4(i): $m^*$ increases in $\gamma$ and $\bar n$ and decreases in $\beta$ and $k'$.

Significance

The result separates two channels by which fashion sensitivity could affect quality. For a fixed number of styles, the optimal quality does not depend on $\gamma$, $\beta$ or $\bar n$ at all (p. 17). All of the effect therefore runs through variety: more styles mean more leftover inventory or more reliance on expensive quick response, and the firm cuts quality to lower the unit cost. Policy conclusions in the paper rest on this mechanism. The disposal-cost and production-tax analyses of §5 ask whether a regulator can reverse the quality decline, and the environmental-impact comparison (Corollary 3) compares fast fashion with a single-style firm.

The paper proves the result with Karush–Kuhn–Tucker conditions on a non-concave reduced problem, split into four regions of $\gamma$ and several cases in $\beta$. No machine-checked proof of any of its statements exists. A formal development would certify the region analysis, which the paper itself states with thresholds that are easy to mistype. It would also supply a reusable treatment of monotone comparative statics for every selection of a non-unique optimum. Two printed slips are already corrected in the statements: the expectation "$\mathbb E[(\bar n-q)^+]$" on p. 11 should read $\mathbb E[(n-q)^+]$, and the optimal-inventory display on p. 14 needs $u>0$.

Difficulty

The reduced profit $F(m)=\max_{u,q}\mathbb E\Pi$ is not concave in $m$: on $[1,k'/k]$ its second derivative changes sign, and the optimum can jump between $m=1$, an interior critical point $m_E$, and the region-III value $\sqrt{\bar n\gamma/(8\beta)}$. Differentiating an optimality condition, the implicit-function argument the paper uses for $m_E$, says nothing about these jumps or about ties. The goal is stated for every optimal solution, including the parameter values where two values of $m$ are optimal, so a proof needs an argument valid across jumps.

Formalization scope

Everything is real-valued. Parameters form a record with an admissibility predicate. Problem (1) is one explicit real function, and the feasible set is $m\ge1$, $u\ge0$, $0\le q\le\bar n$, with the number of styles $m$ a real number as in the paper's analysis. "Optimal" means a feasible maximiser over this set. "The optimal $x^*$" is read as the $x$-component of every optimal solution; "increases/decreases" are weak; parameter changes are strict and vary one record field ({ P with γ := γ₂ }). Ties at the thresholds of Proposition 3 are handled by asserting uniqueness of $m^*$ only off the thresholds. The circle is AddCircle (1 : ℝ), whose metric is the arc distance and whose Haar measure is the uniform probability; the uniform market size is an interval integral divided by $\bar n$. Lemma 1 is stated in the reduced form its proof uses: equal spacing minimises the expected nearest-style distance. The paper's standing assumption that the base value $a$ is high enough to make quick response always worth using does not enter (1) and is not a hypothesis.

The goal is a statement about every joint maximiser $(m,u,q)$ of the expected profit (1) over $m\ge1$, $u\ge0$, $0\le q\le\bar n$. It compares parameter values that differ in one coordinate only, and it asserts that an optimum exists. For a fixed number of styles the optimal quality does not depend on $\gamma$, $\beta$ or $\bar n$, so a formalization about the per-$m$ optimum would be trivially true; the content lies entirely in how the optimal variety responds.

A proof needs only real analysis: one-variable optimisation of quadratics, existence of a maximiser of a continuous coercive function, and an increasing-differences (Topkis-type) monotonicity argument. A proved abstract version of the latter is on the platform, Supermodularity.Monotonicity.argmax_mono_of_strictly_increasing_differences. Lemma 1 needs integration on AddCircle and a convexity inequality over arc lengths. Contributions of alternative proofs of Proposition 3, and of reusable lemmas on comparative statics of argmax sets, are welcome.

Selected references

• X. Long, J. Nasiry, Sustainability in the Fast Fashion Industry, Manufacturing & Service Operations Management 24(3), 2022; author's manuscript SSRN 3486502 (2021). https://ssrn.com/abstract=3486502, https://doi.org/10.1287/msom.2021.1054
• S. C. Salop, Monopolistic Competition with Outside Goods, Bell Journal of Economics 10(1), 141–156, 1979. https://doi.org/10.2307/3003323
• G. P. Cachon, R. Swinney, Purchasing, Pricing, and Quick Response in the Presence of Strategic Consumers, Management Science 55(3), 497–511, 2009. https://doi.org/10.1287/mnsc.1080.0948
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539