Operations Research

Motivation

A portfolio manager who observes a covariate today, say a vector of macroeconomic indicators $x_0$, wants an allocation that performs well on the returns $Y$ that follow such a covariate. With finitely many historical pairs $(\hat x_i,\hat y_i)$ the conditional law of $Y$ given $X=x_0$ is poorly estimated: usually no sample has covariate exactly $x_0$, and few have covariates near it. Distributionally robust optimization hedges against this estimation error by optimizing against the worst distribution in a ball around the empirical one. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451, Operations Research, 2025) study this problem with an optimal transport ball and a conditional objective. Before giving tractable reformulations they identify the regimes in which the robust problem is degenerate. This mission covers one of those regimes, a transport budget large enough to empty a fiber of positive radius.

Setting

Let $\mathcal X$ and $\mathcal Y$ be Polish spaces (covariates and returns) and let $(\hat x_i,\hat y_i)\in\mathcal X\times\mathcal Y$, $i\in[N]$, be the data, with empirical distribution $\hat{\mathbb P}=N^{-1}\sum_i\delta_{(\hat x_i,\hat y_i)}$. Ground costs $\mathbb D_{\mathcal X}$ and $\mathbb D_{\mathcal Y}$ combine into the separable cost $\mathbb D((x,y),(x',y'))=\mathbb D_{\mathcal X}(x,x')+\mathbb D_{\mathcal Y}(y,y')$. The optimal transport cost $\mathbb W(\mathbb Q,\hat{\mathbb P})$ is the least expected cost $\mathbb E_\pi[\mathbb D]$ over couplings $\pi$ of $\mathbb Q$ and $\hat{\mathbb P}$, and the ambiguity set is the ball

$$\mathbb B_\rho=\{\mathbb Q\in\mathcal M(\mathcal X\times\mathcal Y):\mathbb W(\mathbb Q,\hat{\mathbb P})\le\rho\}.$$

The conditioning event is the fiber $\mathcal N_\gamma(x_0)\times\mathcal Y$, with $\mathcal N_\gamma(x_0)=\{x:\mathbb D_{\mathcal X}(x,x_0)\le\gamma\}$ and fiber radius $\gamma>0$. For a loss $\ell(y)$ (the loss of a fixed portfolio at return $y$) the worst-case conditional expected loss is

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X\in\mathcal N_\gamma(x_0))>0}\ \mathbb E_{\mathbb Q}\big[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)\big],$$

problem (12) of the paper, where the strict inequality avoids conditioning on null sets. The threshold

$$\rho_{\max}(x_0,\gamma)=\inf\{\mathbb W(\mathbb Q,\hat{\mathbb P}):\mathbb Q(X\in\mathcal N_\gamma(x_0))=0\}$$

is the least budget that empties the fiber. With $\mathcal I_1=\{i:\hat x_i\in\mathcal N_\gamma(x_0)\}$ and $d_i$ the cost from $\hat x_i$ to the boundary $\partial\mathcal N_\gamma(x_0)$, the paper computes it in closed form. Throughout, the paper's Assumption 2.4 holds: the costs are symmetric, nonnegative and continuous, and $\mathbb D$ vanishes exactly on the diagonal; projections onto $\mathcal N_\gamma(x_0)$ are unique; and every boundary point of $\mathcal N_\gamma(x_0)$ has points outside it at arbitrarily small cost.

Formalization targets

Goal: Proposition 4.2

For $\gamma>0$ and $\rho>\rho_{\max}(x_0,\gamma)$, and every loss $\ell$,

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X\in\mathcal N_\gamma(x_0))>0}\mathbb E_{\mathbb Q}\big[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)\big]=\sup_{y\in\mathcal Y}\ell(y).$$

Milestones

1. The decomposition (24): $\mathbb Q\in\mathbb B_\rho$ iff $\mathbb Q=N^{-1}\sum_i\pi_i$ with $N^{-1}\sum_i\mathbb E_{\pi_i}[\mathbb D_{\mathcal X}(X,\hat x_i)+\mathbb D_{\mathcal Y}(Y,\hat y_i)]\le\rho$.
2. Proposition 4.1: $\rho_{\max}(x_0,\gamma)=N^{-1}\sum_{i\in\mathcal I_1}d_i$.
3. A conditional expectation of $\ell(Y)$ never exceeds $\sup_y\ell(y)$.
4. For every $y_0$, some $\mathbb Q'\in\mathbb B_\rho$ with positive fiber mass has conditional expected loss $\ell(y_0)$.

Significance

Proposition 4.2 is a negative result with a practical consequence: when the budget $\rho$ exceeds $\rho_{\max}$, the robust conditional loss equals the worst loss over the whole return space and ignores the data. The modeler must therefore keep $\rho<\rho_{\max}$, and Proposition 4.1 makes that threshold computable from the samples. In that regime the paper replaces the strict constraint by a positive mass requirement (Proposition 4.3) and derives a finite-dimensional dual (Theorem 4.4); those results are separate missions of this series.

The results are proved in the paper; none is formalized. The mission formalizes them in Lean 4 on top of Mathlib, using a published optimal transport cost and a published extended-real integral. The decomposition (24) is reusable for every argument about empirical optimal transport balls with finitely many atoms. The formal statement of Proposition 4.1 makes explicit a regularity condition on the boundary that the paper's proof uses but does not state.

Difficulty

The upper bound is elementary. The lower bound needs, for each $y_0$, a feasible distribution whose conditional law on the fiber is concentrated at $y_0$. The construction printed on p. 46 keeps a positive mass of a sample inside the fiber, so its conditional expectation mixes $\ell(y_0)$ with a sample loss; that construction has to be corrected. Proposition 4.1 needs a matching lower bound on the cost of every fiber-emptying coupling, and an exit cost from the fiber that equals the boundary distance $d_i$. For a general continuous $\mathbb D_{\mathcal X}$ this fails. The decomposition (24) needs an optimal coupling to exist, which on Polish spaces with a lower semicontinuous cost is Villani's existence theorem. Mathlib does not have that theorem.

Formalization scope

• $\mathcal X,\mathcal Y$ are Polish Borel spaces; $[N]$ is Fin N with $N>0$; repeated samples are allowed.
• $\mathbb W$ is RWPI.SqrtLasso.transportCost, an infimum over couplings with a $[0,\infty]$-valued cost; the paper's "min" is not built into the definition.
• Expectations are $\int\ell^+-\int\ell^-$ in EReal (ModelRiskOT.Duality.extIntegral), never a Bochner integral, which would assign $0$ to a non-integrable loss. Both sides of the goal are extended reals; $\sup_y\ell(y)$ may be $+\infty$.
• The loss at a fixed portfolio $(\alpha,\beta)$ is an arbitrary function $L:\mathcal Y\to\mathbb R$, with no measurability or boundedness assumed.
• The conditional expectation is $\mathbb Q(S)^{-1}\cdot\mathbb E_{\mathbb Q}[\ell\,\mathbb 1_S]$ and is evaluated only at measures with $\mathbb Q(S)>0$. The supremum ranges exactly over probability measures in the ball with positive fiber mass.
• The radius enters as ENNReal.ofReal ρ; the hypothesis $\rho_{\max}<\rho$ forces $\rho>0$, and (24) carries $0\le\rho$.
• $\kappa_i$ and $d_i$ are real infima; $\partial$ is the topological frontier in $\mathcal X$.
• Assumption 2.4 is a structure hypothesis on every theorem. Proposition 4.1 additionally carries BoundaryRegular, which is not in the paper: the boundary is nonempty, the exit cost of a sample inside the fiber equals $d_i$, and $d_i=\kappa_i$ for samples outside. It mentions only $\mathbb D_{\mathcal X}$ and the samples and holds when $\mathbb D_{\mathcal X}$ is a norm distance. The goal does not carry it.
• The goal's hypothesis is $\rho>\rho_{\max}$ with $\rho_{\max}$ as defined (an infimum over measures), not its closed form, so Proposition 4.1 is not built into the goal.

Trivializing formalizations are ruled out: no conditional expectation is evaluated at fiber mass zero, the expectation is not a Bochner integral, $\rho<0$ cannot enter through ofReal, and the supremum is over the ball with positive fiber mass, not over all measures.

Needed infrastructure: finitely supported measures and their couplings, convexity of $\mathbb W(\cdot,\hat{\mathbb P})$, and for (24) the existence of optimal couplings on Polish spaces. These are reusable well beyond this paper, and contributions toward them are welcome.

Selected references

• V. A. Nguyen, F. Zhang, S. Wang, J. Blanchet, E. Delage, Y. Ye, Robustifying conditional portfolio decisions via optimal transport, Operations Research, 2025; arXiv:2103.16451v3. https://arxiv.org/abs/2103.16451
• C. Villani, Optimal Transport: Old and New, Springer, 2009 (Theorem 4.1, existence of optimal couplings). https://doi.org/10.1007/978-3-540-71050-9
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research, 2019. https://doi.org/10.1287/moor.2018.0936

Motivation

A retailer that operates several physical stores can show a customer who finds nothing she likes in her store the products that other stores carry, for example on an in-store screen or a magic mirror, and ship the chosen product from the other store. The customer then buys at a utility discount: shipping takes time and the product cannot be tried on. Liu, Chen, Liu and Wan (2025) compare two ways of making such recommendations. Under simultaneous recommendation (SMR) all products of all stores are shown at once; under sequential recommendation (SQR) the customer first sees the products of her own store and is shown the other stores' products only if she buys nothing. The SQR choice model is the impatient-customer multinomial logit (MNL) model of Gao et al. (2021) applied store by store.

Under SMR the seller can do no better than letting every store offer the single-store optimal assortment (Theorem 1 of the paper, the subject of mission I of this series). Under SQR the seller can do better: the assortment of one store becomes a second-chance offer to the customers of every other store. The SQR problem with general discounts is NP-hard (Proposition 3 of the paper). This mission formalizes the structural result that makes the problem tractable when the discounts depend only on the store a customer visits.

Setting

A seller runs $m\ge2$ stores and sells $n$ products. A fraction $\lambda_i\ge0$ of the customers visits store $i$, with $\sum_i\lambda_i=1$. Product $k$ has revenue $r_k$, with $r_1>r_2>\dots>r_n>0$, and attraction value $v_k>0$; not buying has attraction $1$. A profile $\mathbf S=(S_1,\dots,S_m)$ lists the assortment of each store, and $\bar S=S_1\cup\dots\cup S_m$. A customer of store $i$ who buys product $k$ from store $j$ pays a utility discount $c_{ij}^k\ge0$, with $c_{ii}^k=0$, and $c_i^k(\mathbf S)$ is the smallest such discount over the stores that offer $k$. Under SQR the probability that a customer of store $i$ buys product $k$ is

$$p^Q_{ik}(\mathbf S)=\frac{v_k}{1+V(S_i)}\ \ (k\in S_i),\qquad p^Q_{ik}(\mathbf S)=\frac{v_k e^{-c_i^k(\mathbf S)}}{\big(1+V(S_i)\big)\big(1+V(S_i)+\sum_{l\in\bar S\setminus S_i}v_le^{-c_i^l(\mathbf S)}\big)}\ \ (k\in\bar S\setminus S_i),$$

and $0$ otherwise, where $V(S)=\sum_{k\in S}v_k$ and $W(S)=\sum_{k\in S}r_kv_k$. The seller maximizes the expected revenue

$$R(\mathbf S)=\sum_{i=1}^m\lambda_i\sum_{k=1}^n r_k\,p^Q_{ik}(\mathbf S)\qquad\text{(SQR)}.$$

The discounts are universally homogeneous if $c_{ij}^k=c>0$ for all $i\ne j$, and store-wise homogeneous if $c_{ij}^k=c_i>0$ for all $i\ne j$: the discount depends only on the store the customer visits. The single-store problem is $R^*=\max_S W(S)/(1+V(S))$ (3). An assortment is revenue-ordered if it equals $\{1,\dots,k\}$ for some $k\in[n]$, and $\tilde S$ denotes the smallest revenue-ordered optimal solution of (3).

Formalization targets

Goal: Theorem 4 (p. 17)

If the discounts are store-wise homogeneous, $\lambda_m=\min\{\lambda_1,\dots,\lambda_m\}$ and $c_1\le c_2\le\dots\le c_m$, then some optimal solution of (SQR) satisfies

$$S_1^*\subseteq S_2^*\subseteq\dots\subseteq S_{m-1}^*\subseteq\tilde S\subseteq S_m^*,$$

with every $S_i^*$ revenue-ordered.

Milestones

1. Existence of $\tilde S$ (p. 11): a smallest revenue-ordered optimal solution of (3) exists.
2. Lemma B.3 (p. 36): a three-store, four-product comparison of three explicit profiles.
3. Proposition B.1 (p. 35): if $\lambda_m$ is minimal and $c_m$ maximal, some optimal solution has $S_i^*\subseteq S_m^*$ for all $i$.
4. Lemma B.2 (p. 35): the one-store problem (8) with a fixed second-step set has an optimum that is revenue-ordered within that set.
5. Claim in the proof of Lemma B.1 (p. 38): a unique optimum of (8) shrinks as the discount factor grows.
6. Lemma B.1 (p. 35): under the hypotheses of Theorem 4, some optimal solution is nested, $S_1^*\subseteq\dots\subseteq S_m^*$.
7. Lemma B.4 (p. 39): $f(x)=\sum_i(a_i+b_ix)/(d_i+x)$ is quasi-convex on $x\ge0$ when $a_i/b_i$ decreases and $d_i$ increases.
8. (B.4) and (B.5) (pp. 40–41): for a nested profile whose last store misses product $k$, adding $k$ or truncating the last store does not lose revenue.
9. Proposition B.2 (p. 35): some optimal solution is nested and all revenue-ordered.
10. Step 3, Cases 1 and 2 (p. 43): moving stores $k+1,\dots,m-1$ to $\tilde S$, or growing store $m$ towards $\tilde S$, does not lose revenue.
11. Theorem 3 (p. 16) and Theorem 2 (p. 15): the universally homogeneous $m$-store and two-store versions.

Significance

Theorem 4 reduces the SQR problem with store-wise homogeneous discounts from a search over $2^{mn}$ profiles to a search over nested chains of prefixes, of which there are polynomially many for fixed $m$. It also gives an operational rule: the store with the lowest demand and the largest discount for its customers carries the widest assortment, wider than the single-store optimum $\tilde S$, and every other store carries a prefix that fits inside $\tilde S$. Example 2 of the paper (p. 18) shows that when the two orderings point in opposite directions an optimal solution need not be revenue-ordered, so both hypotheses carry weight.

The result is proved in the paper's Online and Additional Supplements. None of it is machine-checked. A formal development would also settle two places where the printed proof is incomplete: the proof of Proposition B.2 ends with "If we continue the analysis, one can show…", and it applies Lemma B.4 with some coefficients $a_i=0$ and a reordered index, outside the lemma's stated hypotheses.

Difficulty

The revenue of one store depends on the assortments of all others through $\bar S\setminus S_i$, and the objective is a sum of ratios of ratios. The classical argument for MNL assortment problems, that a product with revenue above the current optimum should be added, does not transfer: adding a product to store $i$ raises store $i$'s first-step revenue but also changes the second-step offer to every other store's customers, and removing it from store $i$ moves it into the second step. A local exchange that improves one store can hurt another, so revenue-ordering has to be established jointly with the nesting, and the order of the stores (by $\lambda_i$ and by $c_i$) determines which exchanges are safe.

Formalization scope

Products are Fin n and the paper's product $k$ is index $k-1$; stores are Fin (M + 2), so $m\ge2$ and stores $m-1$, $m$ are the last two indices. Assortments are Finset (Fin n). The attraction values $v_k$ are the primitive data. The factor $e^{-c_i^k(\mathbf S)}$ is the largest $e^{-c_{ij}^k}$ over the stores offering $k$, and $0$ when none does. The choice probabilities (2) and the objective (SQR) are the model; the Gumbel derivation of (2) (Proposition 1, from Gao et al. 2021) is not formalized. Store-wise homogeneity is a predicate on a general discount array, not a separate model.

The standing assumptions of §3 are explicit hypotheses everywhere: $\lambda_i\ge0$, $\sum_i\lambda_i=1$, $r_1>\dots>r_n$, $v_k>0$, $c_{ii}^k=0$. Two hypotheses are pinned and disclosed: $r_k>0$ (revenues are prices; Lemma B.3 is false with a negative revenue), and $n\ge1$ wherever revenue-ordered sets appear, since $\{1,\dots,k\}$ with $k\in[n]$ is nonempty. Lemma B.3 takes nonnegative revenues and attraction values, because the proof of Proposition B.1 applies it to proxy products that may be empty.

"Optimal" means a global maximizer of (SQR) over all profiles, ties allowed. $\tilde S$ enters as the hypothesis that a given set is the smallest revenue-ordered optimum of (3); the first milestone shows the hypothesis can be met, so the goal is not vacuous. A formalization in which $\tilde S$ is an arbitrary optimum, the discount factor ignores which store offers a product, or $m$ is fixed to $2$ would be a different theorem and is ruled out. The inequalities (B.4), (B.5) and those of Step 3 are stated for every profile of the stated shape rather than only for an optimal one, since for an optimal profile they would hold trivially.

A complete development needs finite-sum manipulations of MNL ratios, a reusable lemma that the single-store MNL problem has a revenue-ordered optimum, and quasi-convexity of sums of linear-fractional functions (Lemma B.4, a pure real-analysis statement of independent use). Contributions of any milestone, of alternative proofs of Theorem 4, and of proofs of the companion Theorems 2 and 3 are welcome.

Selected references

• Y. Liu, X. A. Chen, Y. Liu, Z. Wan, Simultaneous vs. Sequential: Optimal Assortment Recommendation in Multistore Retailing, Manufacturing & Service Operations Management, 2025. https://doi.org/10.1287/msom.2024.0761 (formalized from the authors' manuscript of 2024-09-17 with its Online and Additional Supplements).
• P. Gao, Y. Ma, N. Chen, G. Gallego, A. Li, P. Rusmevichientong, H. Topaloglu, Assortment optimization and pricing under the multinomial logit model with impatient customers: Sequential recommendation and selection, Operations Research 69(5):1509–1532, 2021. https://pubsonline.informs.org/journal/opre
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147

Motivation

Retail chains increasingly let a customer who visits one store buy a product that only another store carries, delivered from that store or picked up later. Liu, Chen, Liu and Wan (MSOM 2025, DOI 10.1287/msom.2024.0761) study how a seller operating several stores should choose assortments when customers can substitute across stores at a utility cost, and compare two ways of presenting the other stores' products: simultaneous recommendation (SMR), where they are shown together with the visited store's assortment, and sequential recommendation (SQR), where they are shown only after the customer declines everything in the visited store.

For fixed prices, the paper shows that under SMR the best a chain can do is to offer the single-store optimal assortment everywhere (its Theorem 1). Section 8 asks whether this survives when the seller also sets prices, store by store. This mission formalizes the answer, Theorem 6: under SMR with joint pricing, offering every product in every store at the classical single-store constant adjusted markup prices is optimal. It also formalizes the paper's Proposition 9, which transfers this solution to SQR with a factor-½ revenue guarantee.

The single-store ingredient is older. For the multinomial logit (MNL) model with product-specific price sensitivities, the optimal prices share a common markup adjusted by the reciprocal sensitivity; this goes back to work on MNL multi-product pricing such as Li and Huh (2011) and is stated in this form by Wang (2012), whom the paper cites.

Setting

There are $m$ stores $i\in[m]$ and $n$ products $k\in\mathcal N=[n]$. A fraction $\lambda_i\ge0$ of customers visits store $i$, with $\sum_i\lambda_i=1$. The seller chooses an assortment profile $\mathbf S=(S_1,\dots,S_m)$ with $S_i\subseteq\mathcal N$, writes $\bar S=S_1\cup\dots\cup S_m$, and chooses real prices $\mathbf P=(p_{ik})$, the price of product $k$ in store $i$; production costs are zero.

A customer visiting store $i$ who buys product $k$ in store $j$ at that store's price has utility $\alpha_{ik}-\beta_{ik}p_{jk}-c^k_{ij}$ plus an independent standard Gumbel term, where $\alpha_{ik}>0$ is the intrinsic utility, $\beta_{ik}>0$ the price sensitivity, and $c^k_{ij}\ge0$ the utility discount for buying from another store, with $c^k_{ii}=0$. Write $v_{ik}=\exp(\alpha_{ik}-\beta_{ik}p_{ik})$. For $k\in\bar S\setminus S_i$, the customer buys from a store $l=l(i,k)$ that offers $k$ and maximizes $\alpha_{ik}-\beta_{ik}p_{jk}-c^k_{ij}$ over the stores $j$ offering $k$; then $\tilde v_{ik}(\mathbf S)=\exp(\alpha_{ik}-\beta_{ik}p_{lk}-c^k_{il})$ and $\tilde p_{ik}(\mathbf S)=p_{lk}$. The no-purchase option has weight $1$.

The SMR joint problem (13) maximizes

$$R^M(\mathbf S,\mathbf P)=\sum_{i=1}^m\lambda_i\cdot\frac{\sum_{k\in S_i}p_{ik}v_{ik}+\sum_{k\in\bar S\setminus S_i}\tilde p_{ik}(\mathbf S)\tilde v_{ik}(\mathbf S)}{1+\sum_{k\in S_i}v_{ik}+\sum_{k\in\bar S\setminus S_i}\tilde v_{ik}(\mathbf S)},$$

and the SQR joint problem (15) maximizes

$$R^Q(\mathbf S,\mathbf P)=\sum_{i=1}^m\lambda_i\left(\frac{\sum_{k\in S_i}p_{ik}v_{ik}}{1+\sum_{k\in S_i}v_{ik}}+\frac{\sum_{k\in\bar S\setminus S_i}\tilde p_{ik}\tilde v_{ik}}{(1+\sum_{k\in S_i}v_{ik})(1+\sum_{k\in S_i}v_{ik}+\sum_{k\in\bar S\setminus S_i}\tilde v_{ik})}\right).$$

The single-store problem (14) maximizes $\sum_{k\in S}p_k e^{\alpha_k-\beta_kp_k}/(1+\sum_{k\in S}e^{\alpha_k-\beta_kp_k})$ over $S\subseteq\mathcal N$ and real $(p_k)$. Finally $\theta^*_i$ is the unique solution of

$$\theta_i=\sum_{k\in\mathcal N}e^{\hat\alpha_{ik}-\beta_{ik}\theta_i},\qquad\hat\alpha_{ik}=\alpha_{ik}-\log\beta_{ik}-1.$$

Formalization targets

Goal: Theorem 6

$$R^M(\mathbf S,\mathbf P)\ \le\ R^M\bigl((\mathcal N,\dots,\mathcal N),\ (\theta^*_i+1/\beta_{ik})_{i,k}\bigr)\quad\text{for all }\mathbf S,\ \mathbf P\in\mathbb R^{m\times n}\text{ and every best-store rule }l.$$

No uniqueness is claimed.

Milestones

1. The markup equation has a unique solution $\theta^*_i$ (p. 28).
2. The single-store problem (14) has optimal value $\theta^*$, attained by the full set at prices $\theta^*+1/\beta_k$ (p. 28, citing Wang 2012).
3. In the proof of Theorem 6 (Online Supplement, p. 47): store $i$'s revenue in (13) is at most the objective of (14) at $S=\bar S$, $p_k=p_{ik}$ on $S_i$ and $p_k=(\alpha_{ik}-\log\tilde v_{ik})/\beta_{ik}$ off $S_i$, and these prices dominate $\tilde p_{ik}$.
4. Hence store $i$'s revenue in (13) is at most $\theta^*_i$.
5. Proposition 9 (p. 29): $R^Q(\mathbf S,\mathbf P)\le 2R^Q(\mathbf S^*,\mathbf P^*)$ for the solution of Theorem 6.

Significance

Theorem 6 says that, under simultaneous recommendation, cross-store substitution creates no value that a coordinated price-and-assortment policy can extract: the multistore problem decouples into independent single-store pricing problems, each solved by offering everything at a constant adjusted markup. Together with Theorem 1 it places SMR as a clean benchmark against which SQR is compared, and Proposition 9 turns the benchmark into a guaranteed policy for SQR, where the joint problem has no known closed-form solution.

None of these results has a machine-checked proof. The mission's main new formal content is the single-store MNL pricing theorem with heterogeneous price sensitivities (milestone 2), which is cited, not proved, in the paper and is not on the platform; it is reusable for any MNL pricing model. Formalizing the store-wise reduction also makes explicit what the printed argument leaves implicit: the bound holds for every tie-breaking in the best-store rule, and for arbitrary real prices.

Difficulty

The multistore objective (13) is not a sum of independent store problems: store $j$'s prices enter store $i$'s revenue through $\tilde p_{ik}$ and $\tilde v_{ik}$, and the selection $l$ is itself an $\arg\max$ that changes with the prices, so the objective is discontinuous in $\mathbf P$. Direct first-order analysis of (13) is therefore not available. The single-store problem (14) is not concave in the prices either, so its optimum cannot be read off from a stationarity condition alone: one needs a global bound valid for every real price vector and every assortment, including negative prices and empty assortments.

Formalization scope

Stores are Fin m, products Fin n (the paper's product $k$ is index $k-1$), assortments Finset (Fin n), prices real-valued functions. $\bar S$ is the finite union of the $S_i$. The best-store rule $l$ is a function Fin m → Fin n → Fin m constrained by a predicate (it must offer $k$ and maximize the customer's utility among the stores offering $k$); every statement holds for every such $l$, and the right-hand side at the full profile, where $\bar S\setminus S_i=\emptyset$, does not depend on its rule. $\theta^*_i$ enters as a hypothesis "θ solves the markup equation", never as a chosen term; its existence and uniqueness is milestone 1.

Standing assumptions carried as explicit hypotheses: $\lambda_i\ge0$, $\sum_i\lambda_i=1$, $\alpha_{ik}>0$ and $\beta_{ik}>0$ (the page's $\mathbb R^+$), $c^k_{ij}\ge0$, $c^k_{ii}=0$. Prices range over all of $\mathbb R$. Optimality is a universal upper bound over all profiles, prices and tie-breaking rules, never a supremum or an $\arg\max$. Proposition 9's "optimal solution to problem (13)" is the solution constructed in Theorem 6.

The choice model (13)–(15) is taken as given; the derivation of the MNL probabilities from Gumbel utilities is not formalized. A formalization in which the selection $l$ is unconstrained, in which $\tilde v_{ik}$ uses store $l$'s price sensitivity instead of the customer's, or in which the optimum is a supremum of a possibly unbounded set would change the theorem and is ruled out by the definitions.

A complete development needs only Mathlib's real analysis (exponential, logarithm, finite sums); no new library is required. The single-store pricing optimum (milestone 2) is reusable for any MNL pricing model, and contributions of a general MNL pricing library are welcome.

Selected references

• Y. Liu, X. A. Chen, Y. Liu, Z. Wan, Simultaneous vs. Sequential: Optimal Assortment Recommendation in Multistore Retailing, Manufacturing & Service Operations Management, 2025. https://doi.org/10.1287/msom.2024.0761
• R. Wang, Capacitated assortment and price optimization under the multinomial logit model, Operations Research Letters 40(6), 2012. https://doi.org/10.1016/j.orl.2012.08.003
• H. Li, W. T. Huh, Pricing multiple products with the multinomial logit and nested logit models: concavity and implications, Manufacturing & Service Operations Management 13(4), 2011. https://doi.org/10.1287/msom.1110.0344
• P. Gao, Y. Ma, N. Chen, G. Gallego, A. Li, P. Rusmevichientong, H. Topaloglu, Assortment optimization and pricing under the multinomial logit model with impatient customers: Sequential recommendation and selection, Operations Research 69(5), 2021. https://doi.org/10.1287/opre.2021.2127

Motivation

A retailer with several physical stores often carries a different selection in each one. A customer who walks into a store and finds nothing she likes may still buy a product stocked elsewhere in the chain, paying in delivery cost or waiting time for it. Liu, Chen, Liu and Wan (MSOM 2025, DOI 10.1287/msom.2024.0761) compare two ways of showing those other products. Under simultaneous recommendation (SMR) the customer sees the store's own assortment and the rest of the chain's products at once. Under sequential recommendation (SQR) she first sees only the store's assortment and is shown the other stores' products only after declining all of them.

The paper shows that sequential recommendation earns more than simultaneous recommendation, but that choosing the best SQR assortments is NP-hard. A natural first heuristic ignores the cross-store interaction: each store simply carries the assortment that would be optimal if it were alone. This mission formalizes the paper's guarantee for that heuristic: it earns at least half the optimal sequential revenue, and half is the best possible constant. The guarantee is proved in the heterogeneous case of the paper's §7.1, where a product may be valued differently in different stores (a flagship store downtown and an outlet store, for example).

Setting

There are $m$ stores and $n$ products. A fraction $\lambda_i\ge0$ of the customers first visits store $i$, with $\sum_{i=1}^m\lambda_i=1$. Product $k$ earns revenue $r_k$, and the products are numbered so that $r_1>r_2>\dots>r_n>0$. In store $i$, product $k$ has attraction value $v_{ik}=\exp(u_{ik})>0$, where $u_{ik}$ is its mean utility; not buying has attraction value $1$. A customer who first visits store $i$ but buys product $k$ from store $j$ suffers a utility discount $c^k_{ij}\ge0$, with $c^k_{ii}=0$.

A decision is a profile $\boldsymbol S=(S_1,\dots,S_m)$ of assortments $S_i\subseteq\{1,\dots,n\}$; write $\bar S=S_1\cup\dots\cup S_m$. A product $k\in\bar S\setminus S_i$ reaches a store-$i$ customer through the cheapest store that offers it, with discount $c^k_i(\boldsymbol S)=\min_{j:\,k\in S_j}c^k_{ij}$. Under the multinomial logit model with sequential recommendation, a customer who first visits store $i$ buys product $k$ with probability

$$p^Q_{ik}(\boldsymbol S)=\begin{cases}\dfrac{v_{ik}}{1+\sum_{l\in S_i}v_{il}} & k\in S_i,\\[3mm]\dfrac{v_{ik}e^{-c^k_i(\boldsymbol S)}}{\bigl(1+\sum_{l\in S_i}v_{il}\bigr)\bigl(1+\sum_{l\in S_i}v_{il}+\sum_{l\in\bar S\setminus S_i}v_{il}e^{-c^l_i(\boldsymbol S)}\bigr)} & k\in\bar S\setminus S_i,\\[3mm]0&\text{otherwise,}\end{cases}$$

and the seller's expected revenue is

$$R(\boldsymbol S)=\sum_{i=1}^m\lambda_i\sum_{k=1}^nr_k\,p^Q_{ik}(\boldsymbol S).\qquad\text{(SQR-heter)}$$

Its maximum over all profiles is $R^*_Q$.

The single-store problem of store $i$ is

$$R^*_i=\max_{S}\frac{\sum_{k\in S}r_kv_{ik}}{1+\sum_{k\in S}v_{ik}}.$$

An assortment is revenue-ordered if it is $\{1,2,\dots,k\}$ for some $k\in\{1,\dots,n\}$. Some revenue-ordered assortment is optimal for the single-store problem; $\tilde S_i$ denotes the smallest such one. The heuristic offers $\tilde S_i$ in store $i$ for every $i$, and its revenue is $R^H_Q=R(\tilde S_1,\dots,\tilde S_m)$, cross-selling between stores included.

Formalization targets

Goal: Proposition 7

$$R^H_Q\ \ge\ \tfrac12R^*_Q,$$

and the factor $\tfrac12$ is tight: for every $\delta>0$ there is an instance with two stores and two products on which $R^H_Q<(\tfrac12+\delta)R^*_Q$.

Milestones

1. Lemma D.1. Scaling every attraction value by a factor $\epsilon_i\in(0,1)$ does not increase the optimal MNL revenue.
2. First inequality. For every profile, $R(\boldsymbol T)\ge\sum_i\lambda_i\frac{\sum_{k\in T_i}r_kv_{ik}}{1+\sum_{k\in T_i}v_{ik}}$; at the heuristic profile this is $R^H_Q\ge\sum_i\lambda_iR^*_i$.
3. Second and third inequalities. For every profile $\boldsymbol S$, $R(\boldsymbol S)\le2\sum_i\lambda_iR^*_i$.
4. Tightness instance. With $\lambda=(1,0)$, $r=(1+\frac1\epsilon,1)$, $v_{i\cdot}=(\epsilon,\frac1\epsilon)$ and no discounts, $\tilde S_i=\{1\}$, the heuristic earns exactly $1$ and the profile $(\{1\},\{2\})$ earns $1+\frac1{(1+\epsilon)(1+\epsilon+\epsilon^2)}$.

Significance

The guarantee says that the simplest decentralized policy, in which every store optimizes as if alone, cannot lose more than half of what the best sequential recommendation earns, whatever the store-specific valuations and the cross-store discounts. Read from the other side, the same bound with its tight instance says that sequential cross-selling can at most double the revenue of operating the stores separately, and that a doubling is approached. Since the exact SQR problem is NP-hard (the paper's Proposition 3), a constant-factor guarantee for a policy computable store by store is the kind of statement a practitioner can act on; the paper's numerical study (its Appendix G) finds the heuristic much closer to optimal on synthetic data than the worst case.

Proposition 7 is proved in the paper; nothing in it has been machine-checked. The mission formalizes the model, the proposition with both parts, and the three steps of its proof. Lemma D.1, the monotonicity of the optimal MNL revenue in the attraction values, is a standard fact of assortment optimization that is stated here for a single MNL model and is reusable beyond this mission.

Difficulty

The heuristic profile and the optimal profile are unrelated: the optimal one may stock in store $i$ products that store $i$'s own optimum omits, precisely to sell them to other stores' customers in the second stage. A comparison store by store therefore fails, because the optimum's revenue in store $i$ depends on every other store's assortment through $\bar S$ and the discounts $c^k_i(\boldsymbol S)$. The second-stage revenue is a product of two MNL fractions over different assortments with discounted attraction values, and it has to be bounded by the single-store optimum with undiscounted values; this is where Lemma D.1 is needed, and the lemma itself does not follow from comparing a fixed assortment, since the optimal assortment changes with the attraction values. For the tightness part, the answer depends on the tie rule that defines $\tilde S_i$: in the instance, store 2 has two optimal single-store assortments, and only the smallest one makes the bound tight.

Formalization scope

Lean 4 with Mathlib. Products are Fin n (the paper's product $k$ is index $k-1$) and stores are Fin m; assortments are Finset (Fin n) and profiles are Fin m → Finset (Fin n). Attraction values $v_{ik}$ are the primitive data, not utilities. The discount factor $e^{-c^k_i(\boldsymbol S)}$ is the largest $e^{-c^k_{ij}}$ over the offering stores, and $0$ when no store offers $k$ (the paper's $c=\infty$). The single-store revenue is the published ChoiceCDLP.MNL.mnlObjective v r 1 S. The model is the choice probabilities (10) and the objective (SQR-heter), taken as given; the paper's derivation of (10) from Gumbel utilities is not formalized.

The standing assumptions $\lambda_i\ge0$, $\sum_i\lambda_i=1$, $r_1>\dots>r_n$, $v_{ik}>0$, $c^k_{ij}\ge0$ and $c^k_{ii}=0$ are explicit hypotheses of every theorem. One hypothesis is pinned beyond the page: $r_k>0$. The paper's revenues are prices and its proof drops a second-stage revenue term that is nonnegative only for nonnegative revenues, but the sign is never stated. The paper's tightness claim ("an instance where the equality holds") is realized only in the limit $\epsilon\to0$, so the goal states it in the form "for every $\delta>0$, some instance has $R^H_Q<(\frac12+\delta)R^*_Q$".

"Optimal" means a maximizer over all assortments or profiles, ties allowed, and $R^*_Q$ is never formed as a term: the bound is stated as $\frac12R(\boldsymbol S)\le R^H_Q$ for every profile $\boldsymbol S$. $\tilde S_i$ is a predicate (revenue-ordered, optimal, and of least cardinality among the revenue-ordered optima). An encoding in which $\tilde S_i$ can never exist would make the bound vacuous, so the tightness part asserts that $\tilde S_i$ exists on its instance. The tightness part also must use the paper's tie rule, not an arbitrary single-store optimum, since with the other optimum the instance is not tight.

Welcome contributions: proofs of Lemma D.1 and of the two halves of the bound, the exact evaluation of the tightness instance, and a general Lean library for single-store MNL assortment optimization (existence of revenue-ordered optima, monotonicity in attraction values) that the other missions of this series can reuse.

Selected references

• Y. Liu, X. A. Chen, Y. Liu, Z. Wan, Simultaneous vs. Sequential: Optimal Assortment Recommendation in Multistore Retailing, Manufacturing & Service Operations Management, 2025. https://doi.org/10.1287/msom.2024.0761 (formalized from the authors' manuscript of 2024-09-17 with its Online Supplement).
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Gao, Y. Ma, N. Chen, G. Gallego, A. Li, P. Rusmevichientong, H. Topaloglu, Assortment Optimization and Pricing Under the Multinomial Logit Model with Impatient Customers: Sequential Recommendation and Selection, Operations Research 69(5):1509–1532, 2021. https://doi.org/10.1287/opre.2021.2127

Motivation

Lambda Value-at-Risk ($\Lambda$VaR), introduced by Frittelli, Maggis and Peri (Mathematical Finance 24(3), 2014), generalizes the Value-at-Risk used in banking and insurance regulation: instead of one fixed confidence level, the level $\Lambda(x)$ may depend on the size $x$ of the loss. It has since been studied for its properties, representation and characterization (Bellini and Peri, SIAM J. Financial Math. 13(1), 2022; Han et al. 2025; see the references of arXiv:2511.00717v1).

Regulators and risk managers rarely know the loss distribution exactly. A standard way to account for this ambiguity is to evaluate the risk measure under every model in a neighbourhood of a reference model $\mathbb P$ and report the worst case. Neighbourhoods defined by a $\phi$-divergence (Kullback–Leibler, chi-squared, $\alpha$-divergences) are the most common choice in distributionally robust optimization (Ben-Tal et al. 2013). P. Liu and A. Schied, Lambda Value-at-Risk under ambiguity and risk sharing, arXiv:2511.00717v1 (2025), define $\Lambda$VaR with respect to a capacity. They show that for increasing $\Lambda$ the worst case over a $\phi$-divergence ball is again a $\Lambda$VaR, under an explicitly distorted reference probability. This mission formalizes that result.

Setting

Let $(\Omega,\mathcal F)$ be a measurable space. A capacity is a set function $w:\mathcal F\to[0,1]$ that is increasing ($A\subseteq B\Rightarrow w(A)\le w(B)$) with $w(\emptyset)=0$ and $w(\Omega)=1$; every probability measure is one. Let $\mathcal H_I$ be the set of increasing functions $\Lambda:\mathbb R\to(0,1)$. For a capacity $w$ and a random variable $X$,

$$\Lambda\mathrm{VaR}^w(X)=\inf\{x\in\mathbb R: w(X>x)\le\Lambda(x)\},\qquad \Lambda\mathrm{VaR}^{+,w}(X)=\sup\{x\in\mathbb R: w(X>x)\ge\Lambda(x)\},$$

with $\inf\emptyset=\infty$ and $\sup\emptyset=-\infty$. A constant $\Lambda\equiv\alpha$ gives the Choquet quantile $\mathrm{VaR}^w_\alpha$. For a class $W$ of capacities, $\overline w=\sup_{w\in W}w$ and $\underline w=\inf_{w\in W}w$ are its setwise envelopes; for a class $\mathcal P$ of probability measures they are written $\overline{\mathbb Q}$ and $\underline{\mathbb Q}$.

Fix a probability measure $\mathbb P$ and a convex $\phi:[0,\infty)\to\mathbb R\cup\{\infty\}$ with $\phi(1)=0$ and $\phi(0)=\lim_{x\downarrow0}\phi(x)$. For a probability measure $\mathbb Q\ll\mathbb P$, $D_\phi(\mathbb Q\|\mathbb P)=\mathbb E^{\mathbb P}[\phi(\mathrm d\mathbb Q/\mathrm d\mathbb P)]$, and for $\delta>0$ the $\phi$-divergence ball is $\mathcal P_\phi(\mathbb P,\delta)=\{\mathbb Q\ll\mathbb P: D_\phi(\mathbb Q\|\mathbb P)\le\delta\}$. The distortion $g_{\phi,\delta}:[0,1]\to[0,1]$ is $g_{\phi,\delta}(0)=0$, $g_{\phi,\delta}(1)=1$ and

$$g_{\phi,\delta}(x)=\sup\{t\in[x,1]: x\phi(t/x)+(1-x)\phi((1-t)/(1-x))\le\delta\},\qquad x\in(0,1).$$

Formalization targets

Goal: Theorem 2 (p. 12)

For $\delta>0$, $\Lambda\in\mathcal H_I$, $\alpha\in(0,1)$ and every random variable $X$,

$$\sup_{\mathbb Q\in\mathcal P_\phi(\mathbb P,\delta)}\Lambda\mathrm{VaR}^{\mathbb Q}(X)=\Lambda\mathrm{VaR}^{g_{\phi,\delta}\circ\mathbb P}(X),\qquad \sup_{\mathbb Q\in\mathcal P_\phi(\mathbb P,\delta)}\mathrm{VaR}^{\mathbb Q}_\alpha(X)=\mathrm{VaR}^{g_{\phi,\delta}\circ\mathbb P}_\alpha(X).$$

If moreover $\phi$ is finite, strictly convex and $\phi(x)/x\to\infty$, then

$$\sup_{\mathbb Q\in\mathcal P_\phi(\mathbb P,\delta)}\Lambda\mathrm{VaR}^{\mathbb Q}=(g^{-1}_{\phi,\delta}\circ\Lambda)\mathrm{VaR}^{\mathbb P},\qquad \sup_{\mathbb Q\in\mathcal P_\phi(\mathbb P,\delta)}\mathrm{VaR}^{\mathbb Q}_\alpha=\mathrm{VaR}^{\mathbb P}_{g^{-1}_{\phi,\delta}(\alpha)},$$ $$\lim_{\delta\downarrow0}\sup_{\mathbb Q\in\mathcal P_\phi(\mathbb P,\delta)}\Lambda\mathrm{VaR}^{\mathbb Q}(X)=\lim_{\delta\downarrow0}(g^{-1}_{\phi,\delta}\circ\Lambda)\mathrm{VaR}^{\mathbb P}(X)=\Lambda\mathrm{VaR}^{+,\mathbb P}(X).$$

Milestones

1. Proposition 2 (p. 8): for a nonempty class $W$ of capacities and $\Lambda\in\mathcal H_I$, $\sup_{w\in W}\Lambda\mathrm{VaR}^w=\Lambda\mathrm{VaR}^{\overline w}$ and $\inf_{w\in W}\Lambda\mathrm{VaR}^{+,w}=\Lambda\mathrm{VaR}^{+,\underline w}$.
2. Corollary 1 (p. 8): the same for a class of probability measures, together with the fact that $\overline{\mathbb Q}$ and $\underline{\mathbb Q}$ are capacities.
3. Proposition 5, formula (p. 11): $\sup_{\mathbb Q\in\mathcal P_\phi(\mathbb P,\delta)}\mathbb Q(A)=g_{\phi,\delta}(\mathbb P(A))$ for every $A\in\mathcal F$.
4. Proposition 5, properties (pp. 11–12): under the extra hypotheses on $\phi$, $x\phi(1/x)+(1-x)\phi(0)=\delta$ has a unique root $x_\delta\in(0,1)$, $g_{\phi,\delta}$ is continuous and strictly increasing on $[0,x_\delta]$ and equal to $1$ on $[x_\delta,1]$, and $g_{\phi,\delta}(x)>x$ with $g_{\phi,\delta}(x)\downarrow x$ as $\delta\downarrow0$.

Significance

The theorem reduces a supremum over an infinite-dimensional set of models to a single $\Lambda$VaR under the reference model with a transformed level function $g^{-1}_{\phi,\delta}\circ\Lambda$. Robust $\Lambda$VaR therefore inherits the computational and statistical tools available for $\Lambda$VaR, and the worst-case VaR at level $\alpha$ is the ordinary VaR at the explicit level $g^{-1}_{\phi,\delta}(\alpha)$. The limit statement shows an asymmetry: as the ambiguity vanishes, the robust value converges to the upper version $\Lambda\mathrm{VaR}^{+,\mathbb P}$, not to $\Lambda\mathrm{VaR}^{\mathbb P}$; the two differ when the distribution function of $X$ has a flat piece where it meets $\Lambda$.

The result is proved in the paper (2025) and, to our knowledge, nothing of it is machine-checked. The platform has no capacity, no Choquet quantile, no $\Lambda$VaR, and no $\phi$-divergence over general (non-discrete) probability spaces; the mission supplies all of these, and the formula for the upper probability of a $\phi$-divergence ball (Proposition 5) is a reusable fact about divergence balls in its own right.

Difficulty

Proposition 2 is an order-theoretic exchange of a supremum with an infimum; it fails for decreasing $\Lambda$ (Example 1 of the paper), so monotonicity of $\Lambda$ must be used at the right place, and the values $\pm\infty$ have to be handled. Proposition 5 asks for the exact value of a supremum over an infinite-dimensional ball of measures, for a $\phi$ that may take the value $+\infty$ and may be negative; the upper bound must hold for every density in the ball, not only for the simple ones, and the integrability conventions of $D_\phi$ matter. The second part of Proposition 5 is real analysis of the perspective function $x\phi(t/x)$, and continuity of $g_{\phi,\delta}$ at the endpoints $0$ and $x_\delta$ does not follow from continuity of $\phi$ alone. In the limit $\delta\downarrow0$ the natural guess $\Lambda\mathrm{VaR}^{\mathbb P}$ is wrong: the limit is $\Lambda\mathrm{VaR}^{+,\mathbb P}$, so any argument that treats the robust value as a perturbation of $\Lambda\mathrm{VaR}^{\mathbb P}$ fails at flat pieces of the distribution function.

Formalization scope

All definitions live in the namespace LambdaVaRAmb.Robust. A random variable is a measurable function $\Omega\to\mathbb R$; statements quantify over all of them, which covers every domain $\mathcal X$ the paper allows. Set functions are Set Ω → ℝ and the capacity axioms are imposed on measurable sets. $\Lambda$VaR, $\Lambda$VaR$^+$, the suprema over the ball and the limits as $\delta\to0^+$ are taken in EReal, so $\pm\infty$ are genuine values. $\phi$ is ℝ → EReal (only its values on $[0,\infty)$ matter); convexity uses $0\cdot\infty=0$. $D_\phi$ is the integral of the positive part of $\phi(\mathrm d\mathbb Q/\mathrm d\mathbb P)$ minus that of the negative part; members of the ball are probability measures. $g^{-1}_{\phi,\delta}(t)$ is defined as $\sup\{x\in[0,1]: g_{\phi,\delta}(x)\le t\}$, which is the inverse of $g_{\phi,\delta}$ on $(0,1)$ under the hypotheses where the paper uses it.

Implicit hypotheses made explicit: the classes $W$ and $\mathcal P$ in Proposition 2 and Corollary 1 are nonempty; "$\phi:[0,\infty)\to\mathbb R$" in the second parts is the hypothesis that $\phi$ is finite on $[0,\infty)$; "$x_\delta$ being the solution" is posed as existence and uniqueness.

The trivializing readings are ruled out: suprema over the ball and $\Lambda$VaR values are never real sSup/sInf (which would collapse to $0$ on empty or unbounded sets); the envelopes are real suprema only over nonempty classes of values in $[0,1]$; the ball always contains $\mathbb P$, so it is not empty; $g_{\phi,\delta}$ is the paper's supremum, not a closed form for a particular $\phi$.

Needed infrastructure, all reusable beyond this mission: capacities and Choquet-type quantiles; $\phi$-divergences for general measures via Radon–Nikodym derivatives; conditional Jensen for extended-valued convex functions; perspective functions. Contributions of any of these, and proofs of the milestones in any order, are welcome.

Selected references

• P. Liu and A. Schied, Lambda Value-at-Risk under ambiguity and risk sharing, arXiv preprint, 2025. https://arxiv.org/abs/2511.00717v1
• M. Frittelli, M. Maggis and I. Peri, Risk measures on 𝒫(ℝ) and Value at Risk with probability/loss function, Mathematical Finance 24(3), 442–463, 2014.
• F. Bellini and I. Peri, An axiomatization of Λ-quantiles, SIAM Journal on Financial Mathematics 13(1), 26–38, 2022.
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg and G. Rennen, Robust solutions of optimization problems affected by uncertain probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• C. P. Chambers, Ordinal aggregation and quantiles, Journal of Economic Theory 137(1), 416–431, 2007 (Choquet quantiles).

Motivation

Small third-party sellers on e-commerce marketplaces (Amazon, JD.com, Alibaba) typically have little capital and limited credit history, so they finance procurement through short-term credit. The traditional source is trade credit: the supplier ships the goods and is paid after the sales. Since about 2011 the platforms themselves lend to their sellers (the Amazon Lending Program, Ant Group's micro-loans, JD Small Loan), a form of finance called platform financing. The usual argument for platform loans is that platforms have cheap capital and rich data. Huang, Lai, Wang and Xiao (SSRN 4014045; published in Management Science, 2024, doi:10.1287/mnsc.2022.00201) remove both advantages: supplier and platform have the same capital cost and the same information. They ask whether a platform loan can still help the seller and the supplier, and at which interest rates.

The paper builds on the literature comparing supply-chain finance with bank finance, for example Buzacott and Zhang (2004) on asset-based financing and Kouvelis and Zhao (2012) on supplier versus bank financing of a newsvendor. The new feature is a third lender, the platform, which also collects a share of the revenue.

Setting

A supplier produces at unit cost $c>0$. A seller with no capital procures $q\ge 0$ units and sells all of them on a platform at the market-clearing price $p=\tilde a-q$. The market size $\tilde a$ is uniform on $[a-\delta,a+\delta]$, where $\delta>0$ measures uncertainty. The platform keeps the share $\varphi\in[0,1)$ of revenue, and the seller receives $(1-\varphi)pq$. Supplier and platform both have capital cost equal to the risk-free rate $r_f\ge 0$. The paper assumes $(1-\varphi)a>c(1+r_f)$, so selling is profitable in expectation, and that the smallest market size $a-\delta$ keeps the price positive.

The seller has limited liability: if her revenue falls short of what she owes, she hands over all of it. If she owes $W$ per unit, her expected profit is

$$\Pi_s(W,q)=\mathbb E\big[((1-\varphi)(\tilde a-q)q-Wq)^+\big].$$

• Trade credit. The supplier sets a deferred wholesale price $w$, so $W=w$. He collects $\min\{(1-\varphi)(\tilde a-q)q,\,wq\}$ and pays production cost $cq(1+r_f)$.
• Platform financing at rate $r$. The supplier sets an upfront price $w$ and earns $(w-c)q(1+r_f)$. The seller borrows $wq$ from the platform and owes $W=w(1+r)$ per unit.

Each scheme is a two-stage Stackelberg game: the supplier chooses $w$, then the seller, having observed $w$, chooses $q$. Its subgame-perfect equilibrium gives the profits $\Pi^T_s,\Pi^T_m$ (seller and supplier under trade credit) and $\Pi^P_s,\Pi^P_m$ (under platform financing).

Formalization targets

Goal: Proposition 6 (p. 18)

The paper defines two piecewise threshold functions of $\delta$. They are built from the thresholds $\delta_1,\delta_2,\delta_3$ and the rates $r_1,\dots,r_4$, all explicit in $a,\delta,\varphi,c,r_f$:

$$\hat r_1(\delta)=\begin{cases}r_f&\delta\le\delta_2\\ r_1&\delta_2<\delta\le\delta_3\\ r_2&\delta>\delta_3\end{cases}\qquad \hat r_2(\delta)=\begin{cases}r_f&\delta\le\delta_2\\ r_3&\delta_2<\delta\le\delta_1\\ r_4&\delta>\delta_1.\end{cases}$$

The goal states that $\hat r_1(\delta)\le\hat r_2(\delta)$ and that, for every pair of equilibria of the two games,

$$r<\hat r_1\Rightarrow \Pi^P_s>\Pi^T_s,\ \Pi^P_m>\Pi^T_m;\qquad \hat r_1<r<\hat r_2\Rightarrow \Pi^P_s\le\Pi^T_s,\ \Pi^P_m>\Pi^T_m;\qquad r>\hat r_2\Rightarrow \Pi^P_s\le\Pi^T_s,\ \Pi^P_m\le\Pi^T_m .$$

Milestones

1. Lemmas 1–2: the seller's unique best response.
2. Propositions 1–2: existence and uniqueness of the equilibrium in each game, with explicit prices and quantities.
3. The equilibrium profits displayed in the proofs (pp. 32–33, 35).
4. Proposition 3: the comparison of unit costs and order quantities.
5. Propositions 4 and 5: the seller's and the supplier's profit comparisons.

Significance

The theorem says that a platform loan never benefits the seller while hurting the supplier. The outcome "win for the seller, loss for the supplier" does not occur. Whenever the platform's rate is low enough to help the seller, it also helps the supplier. Combined with Proposition 3, it identifies the mechanisms that make a platform loan attractive even without a cost-of-capital or information advantage: an interest subsidy at low uncertainty, risk mitigation at moderate uncertainty, and risk isolation at high uncertainty, where $\hat r_1$ exceeds $r_f$. The thresholds are explicit, so the result tells a platform the range of rates at which its lending creates value for both supply-chain parties.

The paper's proofs are long case analyses on closed-form radicals. Several displayed formulas in the manuscript contain printing errors (listed below), and some comparisons are justified as "it can be verified". A machine-checked development would certify the closed forms and the threshold algebra and settle the boundary cases. None of these results is formalized in Mathlib or in the Prove2Me library as of October 2026.

Difficulty

The equilibrium is not given by first-order conditions alone. Under limited liability the seller's objective is not concave in $q$: it has a no-default regime and a default regime, and the maximizer jumps between them at $w=(1-\varphi)(a-2\delta)$. The supplier's problem under trade credit is therefore a comparison of two local optima: one quadratic, one a cubic in $w$ with a radical maximizer. The winner switches at $\delta_1$, which involves $5\sqrt{10}-14$. The comparisons of Propositions 3–6 then require sign analyses of differences of nested radicals across up to five regimes, ordered by $\delta_1,\delta_2,\delta_3,\delta_r$ and $(1-\varphi)a-c(1+r_f)$ over $1-\varphi$.

Equating first-order conditions is not enough: equilibrium uniqueness requires excluding the off-path behaviour of the seller and handling the supplier's indifference at $\delta=\delta_1$ and $\delta=\delta_r$.

Formalization scope

• Expectation. $\mathbb E$ over $\tilde a$ is the normalized interval integral $\frac1{2\delta}\int_{a-\delta}^{a+\delta}$. All integrands are continuous.

• Equilibrium. A strategy profile is a price $w$ together with an order rule $q(\cdot)$ defined at every price. A subgame-perfect equilibrium requires two things:

  • for every $w$, $q(w)\ge 0$ maximizes $\Pi_s$ over $q\ge0$;
  • the supplier's price maximizes his payoff over all real prices.

  Two tie-breaks are part of the definition, both the paper's own conventions:

  • the seller orders $0$ when no order is profitable (proofs of Propositions 1–2);
  • the supplier's price is the least maximizer, which assigns $\delta=\delta_1$ and $\delta=\delta_r$ to the low-price branch as the paper does.

• Goals quantify over equilibria. The closed forms enter only through the milestones. A statement taking the closed forms as hypotheses, or proving only $\hat r_1\le\hat r_2$, is not this theorem.

• Standing assumptions.

  • $0<\delta<a$. The pin $\delta<a$ formalizes "the smallest market size keeps the price positive". It is load-bearing: $\hat r_1\le\hat r_2$ fails for some $\delta>a$.
  • $0\le\varphi<1$ and $c>0$.
  • $r_f\ge0$ and $(1-\varphi)a>c(1+r_f)$.
  • For platform financing, $r>-1$ and $c(1+r)<(a+\delta)(1-\varphi)$ (the paper's conditions (ii)–(iii), p. 36).

• Corrected slips, each disclosed in its item:

  • $r_3$ uses $(2ac+8c\delta)$ under the root, not the printed $(2ac+8\delta)$;
  • Proposition 1's $\delta>\delta_1$ branch uses the proof's form $w^T=(1-\varphi)(a-\delta(S-2))$, $q^T=\delta(S-1)/3$;
  • the supplier's trade-credit profit for $\delta>\delta_1$ is $\delta K/27$, where the printed display has flipped signs;
  • Proposition 3(c) uses the strict endpoint.

• Boundary. Propositions 3–4 exclude the rate $r=\hat r_1(\delta)$ from their "otherwise" clause only for $\delta_2<\delta\le\delta_3$, where $r=r_1$ makes $\delta=\delta_r$ and the paper's statement and proof disagree; for other $\delta$ the boundary rate is kept, as on the page.

A complete development needs the following:

• calculus of the uniform expectation of piecewise polynomials;
• the seller's best response;
• the two supplier optimizations;
• the algebra of the thresholds.

The best-response analysis under limited liability is reusable for other newsvendor-type financing models. Contributions of any milestone, of lemmas on the threshold order, and of alternative proofs are welcome.

Selected references

• R. Huang, G. Lai, X. Wang, W. Xiao, Lending to Third-party Sellers with Platform Loan, SSRN manuscript 4014045 (the source of every page and label cited here). https://ssrn.com/abstract=4014045 — published as Platform Financing vs. Trade Credit for Lending to Third-Party Sellers, Management Science, 2024. https://doi.org/10.1287/mnsc.2022.00201
• J. A. Buzacott, R. Q. Zhang, Inventory management with asset-based financing, Management Science 50(9), 1274–1292, 2004. https://doi.org/10.1287/mnsc.1040.0278
• P. Kouvelis, W. Zhao, Financing the newsvendor: supplier vs. bank, and the structure of optimal trade credit contracts, Operations Research 60(3), 566–580, 2012. https://doi.org/10.1287/opre.1120.1040
• B. Jing, X. Chen, G. Cai, Equilibrium financing in a distribution channel with capital constraint, Production and Operations Management 21(6), 1090–1101, 2012. https://doi.org/10.1111/j.1937-5956.2012.01328.x