All missions

Motivation

In budget-feasible procurement an auctioneer with a budget $B$ wants to buy services from $n$ strategic sellers. Each seller $i$ has a private cost $c_i\ge0$, the auctioneer has a public valuation $v$ over sets of sellers, and the mechanism must choose whom to pay and how much, so that sellers have no reason to misreport and the total payment never exceeds $B$. The model was introduced by Singer (FOCS 2010) and is used for crowdsourcing, influence maximization and data acquisition, where a buyer with a fixed budget faces sellers whose costs it cannot observe.

Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239v2, Operations Research 2025) show that deterministic clock auctions, which repeatedly lower personalized prices and let sellers drop out, achieve constant approximations for monotone submodular valuations. Their Appendix B asks whether an even simpler family suffices: posted-price mechanisms, which approach each seller once with a take-it-or-leave-it offer. This mission formalizes their answer for additive valuations, Theorem 13 (p. 25): no deterministic posted-price mechanism achieves an approximation better than $\sqrt n/2$.

Setting

There are $n$ sellers $N=\{0,\dots,n-1\}$, a budget $B>0$, private costs $c_i\ge0$, and a valuation $v:2^N\to\mathbb R_{\ge0}$. The valuation is additive if there are values $v_i\ge0$ with $v(S)=\sum_{i\in S}v_i$ for every $S\subseteq N$.

A deterministic posted-price mechanism knows $n$, $B$ and $v$, but not $c$. It approaches sellers one at a time. At each step it looks at the history of earlier offers (the seller, the price, and whether the seller accepted) and either stops or names a seller not yet approached and a price $p_i$. The seller accepts if $p_i\ge c_i$ and rejects otherwise, and is never approached again. The output $M(v,c)$ is the set of sellers who accepted; each of them is paid its price. The mechanism is budget feasible if for every additive $v$ and every cost profile $c\ge0$ the accepted prices sum to at most $B$.

For an instance, $\mathrm{OPT}$ is the largest value $v(O)$ of a set $O$ with $\sum_{i\in O}c_i\le B$. A mechanism is a $\rho$-approximation on a class if $\mathrm{OPT}\le\rho\,v(M(v,c))$ on every instance of the class.

In Lean the sellers are Fin n, a mechanism is M : (Finset (Fin n) → ℝ) → PostedPrice n with PostedPrice n a rule next : List (Fin n × ℝ × Bool) → Option (Fin n × ℝ) on histories, run (M v) c is its history on the costs c, and accepted and payment read off the output and the total payment.

Formalization targets

Goal: Theorem 13 (p. 25)

For every $n\ge1$, every $B>0$ and every budget-feasible deterministic posted-price mechanism $M$, there are an additive $v$, costs $c\ge0$ and a set $O$ with

$$\sum_{i\in O}c_i\le B,\qquad v(O)>0,\qquad \frac{\sqrt n}{2}\,v\big(M(v,c)\big)\le v(O).$$

This is $\mathrm{OPT}/v(M)\ge\sqrt n/2$ on some instance, written without division.

Milestones: the three cases of the proof (p. 25)

All three concern one valuation $v_0$: a high-value seller $b_h$ worth $\sqrt n$ and $n-1$ small sellers worth $1$ each, with $c_{b_h}=B$.

1. Case 1. If the first positive offer goes to a small seller $i$, before $b_h$ is approached, then on the costs $c_i=p_i$, $c_j=B$ otherwise, $v_0(M)\le1$ and $\frac{\sqrt n}2 v_0(M)<\sqrt n=v_0(\{b_h\})$.
2. Case 2. If every earlier offer is $0$ and $b_h$ is offered $B$, then on small costs $B/(n-1)$, $v_0(M)=\sqrt n$ and $\frac{\sqrt n}2 v_0(M)<n-1$ for $n\ge3$, the value of the budget-feasible set of small sellers.
3. Case 3. If every earlier offer is $0$ and $b_h$ is offered $p_h<B$, then on all costs $B$, $v_0(M)\le1$ and $\frac{\sqrt n}2 v_0(M)<\sqrt n$.

Significance

The theorem separates two families of simple mechanisms. Deterministic clock auctions achieve a constant approximation for monotone submodular valuations (Theorem 1 of the same paper, a $4.75$-approximation), while deterministic posted prices cannot achieve better than $\sqrt n/2$ even for additive valuations, the simplest class. Clock auctions are therefore not merely sufficient but needed among these simple formats: the ability to lower a price after a refusal is what the constant approximation rests on. The bound also explains why the paper's positive result for posted prices (Theorem 15, symmetric submodular valuations) must give up a logarithmic factor.

The result is proved in the paper; it has not been formalized. A formal version fixes what "deterministic posted-price mechanism" means, an adaptive rule on histories that never sees costs, and makes the adversary argument checkable: the hard instance depends on the mechanism, and the case analysis must be exhaustive over all such rules. The mission also provides a reusable model of sequential take-it-or-leave-it mechanisms with budget constraints.

Difficulty

The statement is a lower bound over all mechanisms, so the instance must be chosen after the mechanism. The mechanism is adaptive: which seller it approaches next and at what price can depend on every earlier answer. The proof handles this by noting that, on the hard family, every seller rejects a non-positive offer, so all instances share the run up to the first positive offer or the offer to $b_h$. Making that "common prefix" precise for an arbitrary history-dependent rule, and covering the mechanisms that fall outside the three printed cases (those that never approach $b_h$, or offer $b_h$ more than $B$), is the work of the formal proof. A naive attempt that fixes one instance for all mechanisms fails: a mechanism tailored to that instance is optimal on it.

Formalization scope

• Sellers are Fin n; valuations are functions Finset (Fin n) → ℝ, and additivity carries nonnegative weights. Costs are real and nonnegative.
• The budget satisfies $B>0$, an addition to §2's "a budget $B$"; with $B=0$ nothing can be bought.
• A mechanism may depend on the valuation (and on $n$ and $B$, which are fixed outside it) but not on costs. Prices are arbitrary reals. The run asks the rule for at most $n$ offers; a proposal of an already approached seller ends the run.
• Budget feasibility is a property of the mechanism on every additive instance, as defined on p. 24, not of a single run.
• $\mathrm{OPT}$ is never a supremum: the goal exhibits a budget-feasible set $O$ with $v(O)>0$. The condition $v(O)>0$ rules out the trivial instance with $\mathrm{OPT}=0$, where every bound holds.
• The Case 2 cost is $B/(n-1)$; the page prints $1/(n-1)$, which is budget feasible for the small sellers only when $B\ge1$.
• The cases' hypotheses ("before $b_h$", "price $0$") are read off the run on the profile with all costs $B$; "price $0$" is rendered as "price at most $0$".
• Out of scope: running time, truthfulness (posted-price mechanisms are truthful by construction), and randomized mechanisms.

Contributions welcome: proofs of the three cases, the "common prefix" lemma for runs on cost profiles that agree on every seller approached, and the assembly of the goal.

Selected references

• E. Balkanski, P. Garimidi, V. Gkatzelis, D. Schoepflin, X. Tan, Deterministic Budget-Feasible Clock Auctions, arXiv:2107.09239v2, 2021; Operations Research, 2025. https://arxiv.org/abs/2107.09239v2
• Y. Singer, Budget Feasible Mechanisms, FOCS 2010. https://doi.org/10.1109/FOCS.2010.78

Motivation

Optimal control problems governed by partial differential equations (PDEs) often carry uncertainty in their data, for example a random source term. When the state must stay below a threshold, there are several ways to impose the constraint: with high probability (chance constraints), almost surely, or for every value in a fixed uncertainty set (robust constraints). C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive first-order optimality conditions for all three models for the same elliptic model problem. This mission covers the robust model of §3.2 (pp. 23–25). Its Karush–Kuhn–Tucker (KKT) system has a Radon measure as multiplier, and it is related to the semi-infinite programming view of the same problem.

Robust state constraints are also the limiting case of the almost-sure model: by Lemma 3.4 of the paper (p. 19), an almost-sure constraint and the constraint for every parameter in the support of the distribution coincide when the constraint function is lower semicontinuous in the parameter. The robust multipliers live in $C(\bar D\times\Xi)^*$, which is a space of measures, whereas the almost-sure multipliers of §3.1 contain singular functionals with no such representation.

Setting

Let $D\subseteq\mathbb R^d$, $d\in\{1,2,3\}$, be open, bounded and of class S: there are $\gamma\in(0,1)$ and $r_0>0$ such that $\operatorname{meas}(B_r(x)\setminus D)\ge\gamma\operatorname{meas}(B_r(x))$ for all $x\in\partial D$ and $0<r<r_0$. Let $\Xi\subset\mathbb R^m$ be compact, let $f_0,\varphi_1,\dots,\varphi_m\in L^2(D)$, and set $f(x,z)=f_0(x)+\sum_{i=1}^m z_i\varphi_i(x)$ (Assumption 1.1, eq. (3)). The solution operator $A^{-1}:L^2(D)\to C(\bar D)$ maps $F$ to the unique weak solution $y\in H^1_0(D)\cap C(\bar D)$ of $-\Delta y=F$ in $D$, $y=0$ on $\partial D$.

For a control $u\in L^2(D)$, a cost $F:L^2(D)\to\mathbb R$ and a threshold $\alpha\in\mathbb R$, the robust problem (63) is

$$\min_{u\in L^2(D)}F(u)\quad\text{s.t.}\quad -\Delta\hat y(\cdot,z)=u+f(\cdot,z)\ \text{in }D,\quad \hat y(\cdot,z)=0\ \text{on }\partial D,\quad \hat y(x,z)\le\alpha\ \ \forall (x,z)\in D\times\Xi.$$

The state is $\hat{\mathcal S}(u)\in C(\bar D\times\Xi)$, $[\hat{\mathcal S}(u)](x,z)=[A^{-1}(u+f(\cdot,z))](x)$, and $\hat{\mathcal G}(u)=\hat{\mathcal S}(u)-\alpha$. The cone is $\hat{\mathcal K}=\{y\in C(\bar D\times\Xi):y\le0\}$ and its polar cone is $\hat{\mathcal K}^-=\{y^*\in C(\bar D\times\Xi)^*:\langle y^*,y\rangle\le0\ \forall y\in\hat{\mathcal K}\}$. The linear part of the state is $[\hat{\mathcal A}^{-1}\hat{\mathcal B}h](x,z)=[A^{-1}h](x)$. The active set is $M(u)=\{(x,z)\in\bar D\times\Xi:[\hat{\mathcal S}(u)](x,z)=\max_{\bar D\times\Xi}\hat{\mathcal S}(u)\}$.

Formalization targets

Goal: Lemma 3.14 refined to (66), pp. 23–24

Let $F$ be convex and continuously Fréchet differentiable, and assume the constraint qualification $0\in\operatorname{int}\{\hat{\mathcal G}(L^2(D))-\hat{\mathcal K}\}$. Then $u^*$ is a solution of (63) if and only if there is a nonnegative finite Borel measure $\mu^*$ on $\bar D\times\Xi$ with, for $y^*=\hat{\mathcal S}(u^*)$,

$$\langle DF(u^*),h\rangle+\int_{\bar D\times\Xi}[A^{-1}h](x)\,d\mu^*(x,z)=0\quad\forall h\in L^2(D),$$ $$y^*\le\alpha\ \text{on }\bar D\times\Xi,\qquad\int_{\bar D\times\Xi}(y^*-\alpha)\,d\mu^*=0.$$

The page derives (66) from the abstract system (65) of Lemma 3.14 (necessity). Sufficiency is the converse direction of Lemma 3.14, since a nonnegative measure defines a multiplier in $\hat{\mathcal K}^-$ by integration. Both directions are part of the goal.

Milestones

1. Lemma 3.13: unique solvability of (63b)–(63c) in $C(\bar D\times\Xi)$ with the bound (64).
2. Lemma 3.14: the abstract KKT system (65) with $\lambda^*\in C(\bar D\times\Xi)^*$.
3. The identification $C(\bar D\times\Xi)^*\cong\mathcal M(\bar D\times\Xi)$ (p. 23): every $\lambda^*$ is integration against a signed measure.
4. Nonnegativity (p. 24): $\lambda^*\in\hat{\mathcal K}^-$ gives a nonnegative $\mu^*$.
5. Lemma 3.15: (66) is equivalent to the scalar-multiplier form (67): $\lambda^*\ge0$ and a probability measure $\tilde\mu$ on $M(u^*)$ with $\langle DF(u^*),h\rangle+\lambda^*\int[A^{-1}h](x)\,d\tilde\mu=0$, $\max y^*\le\alpha$, $\lambda^*(\max y^*-\alpha)=0$.
6. Lemma 3.16: the convex-hull condition (68) is equivalent to the existence of such a $\tilde\mu$.
7. Lemma 3.4: for lower semicontinuous $h$, $h(\xi)\le0$ almost surely if and only if $h\le0$ on the support of the law of $\xi$.

Significance

The goal gives the robust problem a KKT system whose multiplier is a nonnegative measure on $\bar D\times\Xi$ that is carried by the points where the constraint is active. Lemmas 3.15 and 3.16 turn this into a scalar multiplier times a probability measure on the active set, and into a convex-hull condition. These are the forms used by semi-infinite programming algorithms and by discretizations that approximate the measure by finitely many atoms. Together with Lemma 3.4, they say when the KKT system of the almost-sure model (§3.1, with its singular multipliers) can be replaced by the measure-valued system of the robust model.

All statements of the mission are proved in the paper, some by reference: Lemma 3.14's proof refers to the argument of Lemma 3.7, and Lemma 3.16 relies on Phelps's barycenter theorem. None of them is formalized. A formal development would also check two points that the page leaves implicit. Lemma 3.15's proof divides by the total mass of $\mu^*$ and does not treat $\mu^*=0$. Condition (68) is printed per direction $h$, while (67a) needs one measure for all $h$.

Difficulty

The necessity direction of the goal needs a Lagrange multiplier theorem in a Banach space whose constraint cone $\hat{\mathcal K}$ has nonempty interior. The multiplier is a priori only an element of $C(\bar D\times\Xi)^*$, and the Riesz–Markov–Kakutani theorem on the compact space $\bar D\times\Xi$ turns it into a measure. The state $\hat{\mathcal S}(u)$ must also be shown to lie in $C(\bar D\times\Xi)$. Continuity of each slice in $x$ is the regularity of Lemma 1.2 (continuity of $H^1_0$ solutions up to the boundary for class-S domains, from Kinderlehrer–Stampacchia), and joint continuity needs the bound (64), uniform in $z$. Working pointwise in $z$ does not give these: a family of continuous slices need not be jointly continuous without an estimate that is uniform in the parameter.

Formalization scope

$\bar D$ and $\Xi$ are subtypes of Euclidean spaces with CompactSpace instances, so $C(\bar D\times\Xi)$ carries its sup norm. Measures on $\bar D\times\Xi$ are Borel measures; on this compact metric space every finite Borel measure is regular, so "regular Borel (Radon) measure" is IsFiniteMeasure, and nonnegativity (66c) is built into Lean's Measure type. The solution operator is a hypothesis: a bounded linear map $L^2(D)\to C(\bar D)$ such that $A^{-1}F$ is, for every $F$, the weak solution in $H^1_0(D)\cap C(\bar D)$, encoded with the published weak-derivative definitions HunterPDE.Shared.WeakDeriv. The page's "$\le0$ in $D\times\Xi$" is encoded on $\bar D\times\Xi$, the same condition for continuous functions. "Solution" means global minimizer over the feasible set. $L^2(D)^*$ is identified with $L^2(D)$ through the Riesz map. In Lemma 3.16 the clco of (68) is the norm closure of the convex hull, which equals the weak closure.

Added hypotheses: $D$ and $\Xi$ nonempty in Lemmas 3.15 and 3.16 (no probability measure exists on an empty set). Pinned reading: (68) is posed as one inclusion $0\in DF(u^*)+\lambda^*\,\overline{\operatorname{co}}\{u_x:(x,z)\in M(u^*)\}$ in $L^2(D)$, where $u_x$ represents $h\mapsto[A^{-1}h](x)$. The page derives (68) from exactly this inclusion. The closed hull is kept because the page's remark that "co" suffices is not proved in infinite dimension.

Several trivializing formalizations are ruled out. The state operator is tied to the PDE and is never an arbitrary map into $C(\bar D\times\Xi)$. The multiplier carries its sign (a nonnegative measure, or $\lambda^*\in\hat{\mathcal K}^-$) together with complementarity. Optimality is global minimality, not a stationarity condition. All integrands are continuous functions on a compact space against finite measures, so no integral takes a junk value.

A complete development needs elliptic regularity in $C(\bar D)$ for class-S domains, a Banach-space Lagrange multiplier theorem under a Robinson-type constraint qualification, the Riesz–Markov–Kakutani theorem for $C(K)^*$ with signed measures (the platform's FamousTheorems.riesz_markov_kakutani covers positive functionals on $C_c$), and barycenters of probability measures on compact convex sets. The last three are reusable beyond this mission. Contributions of proofs for any of them are welcome.

Selected references

• C. Geiersbach, R. Henrion, Optimality conditions in control problems with random state constraints in probabilistic or almost-sure form, arXiv:2306.03965v2, 2024; Math. Oper. Res., 2025. https://arxiv.org/abs/2306.03965
• F. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309
• D. Kinderlehrer, G. Stampacchia, An Introduction to Variational Inequalities and Their Applications, Academic Press, 1980 (SIAM reprint 2000). https://doi.org/10.1137/1.9780898719451
• R. R. Phelps, Lectures on Choquet's Theorem, 2nd ed., Lecture Notes in Mathematics 1757, Springer, 2001. https://doi.org/10.1007/b76887
• H. W. Alt, Lineare Funktionalanalysis, Springer, 2012. https://doi.org/10.1007/978-3-662-08386-4

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