All missions

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

Remote driving, or tele-driving, separates the driver from the vehicle: a human sitting in a control centre drives a car over a network link and can switch to another car as soon as a trip ends. Commercial pilots of this model exist for car delivery and ride-hailing, and it gives a platform a new design choice. A conventional ride-hailing fleet has one driver per car. A tele-driven fleet can run more cars than drivers.

Benjaafar, Wang and Yang model this choice as a queueing system and ask how the service level depends on the number of drivers when the number of vehicles is fixed (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687). Idle vehicles still matter even when nobody is driving them: they are spread over the service region, so the car nearest a new request is closer, and trips (pick-up plus ride) finish faster. A driver count below the vehicle count therefore trades fewer servers for shorter service times. This mission formalizes the paper's first main result, Theorem 1.A, which says when that trade can strictly improve service. The mission follows the 2023 SSRN working paper (version of 1 June 2023) and its numbering.

Setting

A platform has $m$ vehicles and $n \le m$ remote drivers. Trip requests arrive as a Poisson process of rate $\lambda > 0$. A request that finds all $n$ drivers busy is lost. While $q$ customers are in service, each trip ends at the exponential rate $\mu(m, q)$, a function of a real $q \in [1, m]$. The paper's standing assumptions on this rate are:

• Assumption 1: $\mu(m,q)$ is strictly increasing in $m$ and decreasing in $q$, strictly concave in $q$, tends to $1/s$ as $m \to \infty$ (where $s > 0$ is the expected trip time between two uniform locations), and $\mu(m,m)$ does not depend on $m$;
• Assumption 2: there is $\bar m > 0$ such that for $m \ge \bar m$ the trip-completion rate $q\mu(m,q)$ first increases and then decreases in $q$.

The number of customers in service is a birth–death chain with birth rate $\lambda$ and death rate $q\mu(m,q)$, truncated at $n$. With

$$\rho(q) = \frac{\lambda}{q\,\mu(m,q)},$$

its stationary law is $\pi_{m,n}(q) = \prod_{k=1}^{q}\rho(k) \big/ \big[1 + \sum_{i=1}^{n}\prod_{k=1}^{i}\rho(k)\big]$ for $0 \le q \le n$. The service level, the long-run fraction of requests served, is

$$SL(m,n) = 1 - \pi_{m,n}(n).$$

The paper restricts throughout to $m \ge \bar m$ and $\lambda > \max\{1/s, \max_{q \le \bar m} q\mu(\bar m, q)\}$. It splits fleet sizes into three regimes by thresholds $\gamma_1(\lambda) < \gamma_2(\lambda)$. In the supply-limited regime $m < \gamma_1(\lambda)$, demand exceeds the trip-completion rate in every state: $\rho(q) > 1$ for all $q \in [1, m]$.

Formalization targets

Goal: Theorem 1.A

For $m < \gamma_1(\lambda)$, if

$$\lambda\, SL(m,m) > m\,\mu(m,m), \qquad (5)$$

then there is a threshold $1 \le \tilde n_1 \le m - 1$ such that $SL(m,n)$ is strictly increasing in $n$ for $n \le \tilde n_1$ and strictly decreasing for $n > \tilde n_1$, with $SL(m,\tilde n_1) \ge SL(m,\tilde n_1 + 1)$. If (5) fails, $SL(m,n)$ is non-decreasing in $n$ on $\{1,\dots,m\}$.

Milestones

1. Lemma 3 (first sentence): $\rho$ is strictly convex and $1/\rho$ strictly concave on $[1,m]$.
2. Lemma 4: for $1 \le n \le m$, $\pi_{m,n-1}(n-1) > \pi_{m,n}(n)$ holds if and only if $\pi_{m,n-1}(n-1) > \frac{\rho(n)-1}{\rho(n)}$, if and only if $\pi_{m,n}(n) > \frac{\rho(n)-1}{\rho(n)}$.
3. App. C.1, dichotomy: the blocking probability $\pi_{m,n}(n)$ is strictly decreasing on $\{1,\dots,m\}$, or strictly decreasing up to some $\tilde n_1$ and strictly increasing from $\tilde n_1 + 1$.
4. App. C.1, Condition (5): $\pi_{m,m}(m) > \pi_{m,m-1}(m-1)$ if and only if (5) holds.

Significance

Theorem 1.A says that removing drivers from a fleet can strictly raise the fraction of demand served, and Condition (5) says exactly when. The condition compares the average trip-completion rate $\lambda SL(m,m)$ with the completion rate $m\mu(m,m)$ when every vehicle is occupied. In a standard multi-server loss system, where $q\mu(m,q) = q\mu$, the condition never holds and more servers always help. The result makes the optimal driver count a well-posed line search over a unimodal function, and the companion Theorems 1.B and 1.C of the paper (intermediate and supply-rich regimes) rest on the same recursion.

The paper's proofs are short but leave gaps a formal proof must close. To our knowledge no part of the paper has been machine-checked. The mission produces a complete formal statement of the model and of the theorem, under the paper's own assumptions, together with the lemmas the published argument passes through. Milestones 2–4 hold in every regime, so they also serve the proof of Theorem 1.B.

Difficulty

Two steps resist the obvious argument. First, the blocking probability $\pi_{m,n}(n)$ is not a monotone function of anything simple: each driver count truncates the birth–death chain at a different state, so the comparison between $n-1$ and $n$ drivers is a comparison of two different stationary laws. Second, the published argument for the first step of the dichotomy appeals to "$\rho(1) > \rho(2)$ by Assumption 2", which Assumption 2 does not imply. A correct proof must handle the case where the blocking probability increases already from one driver to two. Strict convexity of $\rho$ must also be proved without derivatives, because the formal rate $\mu$ is only assumed concave, not differentiable.

Formalization scope

All objects live in the namespace TeleDriving.ScarceFleet. The rate is a function mu : ℕ → ℝ → ℝ, meaningful for real $q \in [1, m]$. $\rho$, the products $\prod_{k\le i}\rho(k)$, $\pi_{m,n}(q)$ and $SL(m,n)$ are explicit definitions following (1)–(3). The committed conventions are:

• Positivity of $\mu$ on $[1,m]$ and $s > 0$, implicit on the page, are part of Assumption 1.
• "Decreasing in $q$" is non-strict.
• "First increases then decreases" means a turning point $\hat q \in (1, m)$, with strict increase on $[1,\hat q]$ and strict decrease on $[\hat q, m]$.
• Assumptions 1–2 and the size restriction of p. 13 are hypotheses of every theorem.
• The regime $m < \gamma_1(\lambda)$ is encoded by its characterization in Lemma 3(i), $\rho(q) > 1$ on $[1, m]$, because $\gamma_1(\lambda)$ is a real root in $m$ that an integer fleet size almost never equals.
• Driver counts range over $\{1,\dots,m\}$; monotonicity is stated on that set.
• The junction $SL(m,\tilde n_1) \ge SL(m,\tilde n_1+1)$ is non-strict, as the proof gives it.

The threshold is bounded, $1 \le \tilde n_1 \le m - 1$, and no hypothesis on the shape of $\pi$ or $SL$ is assumed. A threshold $\tilde n_1 = m$ or an assumed monotonicity would make the theorem trivial. The dichotomy milestone carries no regime hypothesis, because the argument of App. C.1 does not use one.

Useful infrastructure, reusable beyond this mission, includes: mediant inequalities for $\frac{a+c}{b+d}$ with $b, d > 0$; the fact that the product of a positive linear function and a positive, antitone, strictly concave function is strictly concave; and the induction pattern that turns a one-step recursion test into global unimodality. Proofs of any milestone, alternative arguments, and proofs that dispense with the regime hypothesis are all welcome.

Selected references

• S. Benjaafar, Z. Wang, X. Yang, Human in the Loop Automation: Ride-Hailing with Remote (Tele-)Drivers, SSRN working paper 4130757, version of 1 June 2023. https://ssrn.com/abstract=4130757
• S. Benjaafar, Z. Wang, X. Yang, Human in the Loop Automation: Ride-Hailing with Remote (Tele-)Drivers, Management Science, 2024. https://doi.org/10.1287/mnsc.2022.01687
• O. Besbes, F. Castro, I. Lobel, Spatial Capacity Planning, Operations Research 70(2), 2022. https://doi.org/10.1287/opre.2021.2112
• J. Cheah, J. M. Smith, Generalized M/G/C/C state dependent queueing models and pedestrian traffic flows, Queueing Systems 15, 1994. https://doi.org/10.1007/BF01189240

Motivation

Decision theory under uncertainty distinguishes risk, where probabilities are known, from ambiguity, where they are not. Ellsberg's (1961) urn experiments showed that people's choices between bets on the same kind of event depend on where the uncertainty comes from: a bet on a known urn is preferred to the matching bet on an unknown urn. Tversky and Fox (1995) found that basketball fans prefer bets on basketball games to bets with matched objective chances. Models of ambiguity therefore have to let attitudes depend on the source of uncertainty.

Baillon, Bleichrodt, Li and Wakker (Source Theory: A Tractable and Positive Ambiguity Theory, Management Science 71(10), 2025) take sources to be algebras of events and propose source theory: within each source the agent behaves as if events carry probabilities, transformed by a source-dependent weighting function, while different sources may be weighted differently. The behavior within one source is probabilistic sophistication in the sense of Machina and Schmeidler (1992), restricted to that source. This mission formalizes the paper's first main result, Theorem 1: a characterization of when a single source admits such a probability, entirely in terms of two ambiguity attitudes that are measured in experiments.

Setting

A state space $S$ carries an algebra $\mathcal E$ of events, and $\Gamma$ is a set of outcomes. An act is a finite-valued map $x : S \to \Gamma$ whose level sets are events; it is from an algebra $\mathcal A$ if its level sets lie in $\mathcal A$. The binary act $\gamma E \beta$ pays $\gamma$ on $E$ and $\beta$ on $E^c$. The agent has a preference $\succcurlyeq$ on acts.

Structural Assumption 1 (p. 8771) requires that $\succcurlyeq$ is a weak order represented on binary acts by biseparable utility: there are a utility $U : \Gamma \to \mathbb R$ and a weighting function $W$ on events ($W(\emptyset)=0$, $W(S)=1$, monotone) such that for $\gamma \succcurlyeq \beta$ the act $\gamma E\beta$ is valued $W(E)U(\gamma)+(1-W(E))U(\beta)$. It further requires three nonindifferent outcomes, convex rangedness of $W$ (between two nested events every intermediate weight is attained by a nested event), strong monotonicity, cumulative dominance and the Archimedean axiom. Events are ranked by $W$: $A \succcurlyeq B$ means $W(A) \ge W(B)$.

A source $\mathcal S$ is a subalgebra of $\mathcal E$ on which $W$ is convex ranged. It is uniform (source theory holds for it, Definition 1) if there is a finitely additive probability measure $P$ on $\mathcal S$ such that for all acts $x, y$ from $\mathcal S$

$$\bigl[\forall \alpha\in\Gamma:\ P(x\succcurlyeq\alpha)\ge P(y\succcurlyeq\alpha)\bigr]\ \Longrightarrow\ x\succcurlyeq y. \tag{2}$$

Two attitudes compare sources $\mathcal A$ and $\mathcal C$. $\mathcal C$ is preferred to $\mathcal A$ (Definition 2) if for all $A_1\in\mathcal A$, $C_1\in\mathcal C$,

$$W(A_1)=W(C_1)\ \Longrightarrow\ W(A_1^c)\le W(C_1^c). \tag{6}$$

$\mathcal A$ is more insensitive than $\mathcal C$ with insensitivity region $[B,D]$ (Definition 4) if for all ordered threefold partitions $(C_1,C_2,C_3)$ of $S$ from $\mathcal C$ and $(A_1,A_2,A_3)$ from $\mathcal A$,

$$W(A_1)=W(C_1)\ \&\ W(A_3^c)=W(C_3^c)\le W(D)\ \Rightarrow\ W(A_2)\ge W(C_2), \tag{8}$$ $$W(B)\le W(A_1)=W(C_1)\ \&\ W(A_3^c)=W(C_3^c)\ \Rightarrow\ W(A_2^c)\le W(C_2^c). \tag{9}$$

The region is regular for $\mathcal S$ if every fourfold partition $(E_1,\dots,E_4)$ of $S$ from $\mathcal S$ has a cell with $E_j \succcurlyeq B$ and $E_j^c \preccurlyeq D$.

Formalization targets

Goal: Theorem 1 (p. 8774)

For a source $\mathcal S$ under Assumption 1,

$$\mathcal S \text{ is uniform}\iff \mathcal S \text{ is preferred to itself, and } \exists\, B,D\in\mathcal E:\ [B,D] \text{ regular for } \mathcal S,\ \mathcal S \text{ more insensitive than itself w.r.t. } [B,D].$$

Milestones (in proof order)

1. Necessity (App. B, p. 8779): a uniform source is preferred to itself and more insensitive than itself with the maximal region $[\emptyset, S]$.
2. Lemma A.1 (p. 8779): (6) is equivalent to its weak-premise form (7), $W(A_1)\ge W(C_1)\Rightarrow W(A_1^c)\le W(C_1^c)$.
3. Lemma A.2 (p. 8779): (8) and (9) are equivalent to their weak-premise forms (A.1) and (A.2).
4. (B.1) (p. 8780): in a source preferred to itself, $A\succcurlyeq C \iff A^c\preccurlyeq C^c$.
5. Lemma B.1 (p. 8780): under statement (ii), for $E\cap H=F\cap H=\emptyset$ in $\mathcal S$, $E\succcurlyeq F\iff E\cup H\succcurlyeq F\cup H$.
6. The representing probability (p. 8780): under statement (ii), a unique probability measure on $\mathcal S$ represents event preference on $\mathcal S$.
7. The aside (p. 8780): a representing probability $P$ gives $W = w\circ P$ on $\mathcal S$ for a continuous, strictly increasing $w$ with $w(0)=0$, $w(1)=1$.
8. Uniqueness (p. 8774): the probability measure of a uniform source is uniquely determined.

Significance

Theorem 1 gives source theory a behavioral foundation: whether a source admits an a-neutral probability measure can be read off from comparisons of bets on its own events, without assuming expected utility for risk. Uniformity is what makes the paper's quantitative tools available. Once a source is uniform, its weighting function factors as $W = w_{\mathcal S}\circ P_{\mathcal S}$, and Theorems 2–4 of the paper compare sources through the pmatcher between their source functions; Theorem 4 uses Theorem 1 as a step. The uniqueness of $P_{\mathcal S}$ (milestone 8) is what makes the source function well defined.

The result is proved in the paper; nothing in it is formalized anywhere to our knowledge. The proof relies on a classical representation theorem for qualitative probability (Krantz, Luce, Suppes and Tversky, 1971, Theorem 5.2.2), which is not in Mathlib either. A complete development would give Lean a first framework of Savage-style acts, biseparable utility and comparative probability, which other decision-theory missions could reuse.

Difficulty

The necessity half rests on the probability $P$ of a uniform source representing event preference strictly, which needs strong monotonicity and the range of $P$ on a convex-ranged source. The sufficiency half is the hard one. From the two attitude conditions alone one has to derive de Finetti's additivity (Lemma B.1). Its proof is a case analysis that uses regularity of the region to guarantee that one of the cells is a genuine middle event. One then needs a representation theorem for qualitative probabilities on an algebra, with uniqueness, in the finitely additive setting. Dropping regularity is not an option: without it the region $B=S$, $D=\emptyset$ makes insensitivity nearly empty, and source preference alone does not imply uniformity (the paper's Example 1). The obvious route through countably additive measure theory is not available either, because the probabilities are only finitely additive.

Formalization scope

All statements share one module, SourceTheory.Uniform.Model. It holds acts (IsActFrom), binary acts (bet), null events, convex rangedness, Assumption1 (a structure with one field per clause of Assumption 1), sources (IsSource), finitely additive probabilities (IsProbOn), uniformity (IsUniformWith, IsUniform), IsPreferredTo (Definition 2), IsMoreInsensitive (Definition 4) and IsRegularRegion. Its text is shared verbatim by the four missions on this paper. The conventions are:

• Events are the members of an algebra $\mathcal E$ (endnote 1 licenses any algebra; the power set is a special case). Every quantified event lies in $\mathcal E$ or in the source, so the values of $W$ off $\mathcal E$ never matter.
• Event preference is $W$-order, as Assumption 1 prescribes. The preference forms (15)–(17), (A.3)–(A.5) therefore coincide with the $W$-forms.
• Assumption 1's "W is convex ranged for every source" is split. Convex rangedness on all events is part of Assumption1, and each source carries its own via IsSource. Reading it over every subalgebra would make Assumption 1 unsatisfiable, because $\{\emptyset,S\}$ has no event of weight $1/2$.
• Twofold partitions are $(A_1,A_1^c)$. Threefold and fourfold partitions are ordered and may have empty cells.
• Probability measures on a source are finitely additive, real valued and nonnegative, with total mass 1.
• In the goal, the boundary events $B, D$ are arbitrary events, and "equally preferred/insensitive to itself" is one copy of each condition: for $\mathcal A=\mathcal C=\mathcal S$ both directions coincide.

Statement (ii) carries an existential region, and it must be regular. A version without regularity, or with uniformity replaced by "$W=w\circ P$ for some $P$", would be a different and weaker theorem.

Needed infrastructure: comparative-probability representation (Krantz et al. 1971, Theorem 5.2.2, or a direct construction via convex rangedness), finitely additive measures on set algebras, and the range of a finitely additive probability that represents a convex-ranged weighting. Proofs of the milestones, of the representation theorem as a reusable lemma, and sanity models of Assumption 1 (for instance an expected-utility agent on $[0,1)$ with Lebesgue measure) are all welcome.

Selected references

• A. Baillon, H. Bleichrodt, C. Li, P. P. Wakker, Source Theory: A Tractable and Positive Ambiguity Theory, Management Science 71(10):8767–8782, 2025. https://doi.org/10.1287/mnsc.2023.03307
• D. Ellsberg, Risk, Ambiguity, and the Savage Axioms, Quarterly Journal of Economics 75(4):643–669, 1961. https://doi.org/10.2307/1884324
• I. Gilboa, Expected Utility with Purely Subjective Non-Additive Probabilities, Journal of Mathematical Economics 16(1):65–88, 1987. https://doi.org/10.1016/0304-4068(87)90022-X
• D. H. Krantz, R. D. Luce, P. Suppes, A. Tversky, Foundations of Measurement, Vol. I, Academic Press, New York, 1971 (cited in the paper for Theorem 5.2.2).
• M. J. Machina, D. Schmeidler, A More Robust Definition of Subjective Probability, Econometrica 60(4):745–780, 1992. https://doi.org/10.2307/2951565
• A. Tversky, C. R. Fox, Weighing Risk and Uncertainty, Psychological Review 102(2):269–283, 1995. https://doi.org/10.1037/0033-295X.102.2.269

Motivation

The European Union's General Data Protection Regulation (GDPR, in force since 2018) shifted control over personal data from firms to consumers: data may be collected and processed only with the consumer's consent, and consent may be given for some uses and withheld for others. Online retailers use consumer data in two opposite ways. Saved shopping carts, stored addresses and location sharing make shopping more convenient for the consumer; the same data can also be monetized against the consumer, through targeted advertising, data sales or other exploitation. Whether giving consumers control over these uses helps them, and what it costs firms and society, is a question for regulators and for operations managers of e-commerce platforms alike.

F. Xu, X. Wang and F. Zhang, Consumer Privacy in Online Retail Supply Chains (Management Science, forthcoming), build a stylized model in which both uses of data appear and the consumers' disclosure decisions are taken under rational expectations. This mission formalizes the paper's single-firm result: when one vertically integrated e-commerce firm sells directly to consumers, the GDPR always raises the firm's profit and social welfare, but it raises consumer surplus only when the product's valuation is below an explicit threshold. A companion mission treats the supplier–retailer chain of the same paper, where the GDPR can hurt all three parties.

Setting

A unit mass of consumers values one product at $v>0$. A consumer's inconvenience cost $\theta$ is uniform on $[0,1]$. The data quality is $\delta\in(0,1)$, and monetizing data at intensity $r\ge0$ costs the firm $cr^2$ with $c>0$. Write

$$\mathcal Z = 2c+\delta,\qquad \mathcal M = 4c^2(1-\delta)+c\delta(4-3\delta)+\delta^2,\qquad \mathcal F = 4c^2(1-\delta)+4c\delta(1-\delta)+\delta^2 .$$

The firm first decides whether to collect data ($\ell\in\{0,1\}$), then sets a price $p\in\mathbb R$. Production is free. A buyer who hides her data gets $v-p-\theta$. A buyer who discloses gets $v-p-(1-\delta)\theta-r\delta$: the data scale her inconvenience down by the factor $1-\delta$, and the firm extracts $r\delta$ from her. Without collection only hiding is available. A consumer buys iff her best buying utility is nonnegative.

Two data policies are compared.

• In the $\mathbb R$ mode (retailer-controlled, before the GDPR), the firm chooses $r$ after the data are collected, to maximize $r\delta s-cr^2$ given the mass $s$ of disclosing consumers. Consumers anticipate $s$; a rational expectations equilibrium (REE) is a pair $(s,r)$ in which $r$ is the firm's best response to $s$ and $s$ is the mass of consumers who disclose given $r$.
• In the $\mathbb C$ mode (consumer-controlled, the GDPR), consumers allow the convenience use and block exploitation, so $r=0$ and every buyer discloses.

The firm's profit is $p\cdot(\text{demand})+r\delta s-cr^2$. Consumer surplus is the integral over $\theta\in[0,1]$ of each consumer's realized utility (zero for non-buyers), and social welfare is profit plus consumer surplus. A subgame-perfect equilibrium (SPE) is a profile with an REE response after every $(\ell,p)$, an optimal price over $\mathbb R$ after each $\ell$, and an optimal $\ell$.

Formalization targets

Goal: Theorem 1 (p. 17)

Let $\tau = \dfrac{2\mathcal M\sqrt{1-\delta}}{\mathcal Z\sqrt{\mathcal F}}$. SPEs exist under both policies, and for every SPE of the $\mathbb R$ mode and every SPE of the $\mathbb C$ mode,

$$v<\tau\ \Rightarrow\ CS_{\mathbb R}<CS_{\mathbb C},\qquad v>\tau\ \Rightarrow\ CS_{\mathbb C}<CS_{\mathbb R},\qquad \pi_{\mathbb R}<\pi_{\mathbb C},\qquad W_{\mathbb R}<W_{\mathbb C}.$$

Milestones

1. The optimal monetization intensity $r(s)=\delta s/(2c)$ (§4.1, p. 11).
2. The REE at each price, display (2) (p. 13), with the saturated branch: $s=2c(v-p)/(2c(1-\delta)+\delta)$, $r=\delta(v-p)/(2c(1-\delta)+\delta)$ when $(v-p)\mathcal Z\le 2c(1-\delta)+\delta$, and $s=2c/\mathcal Z$, $r=\delta/\mathcal Z$ otherwise.
3. Lemma 1 (p. 13): the hide-and-buy, disclose-and-buy and no-purchase intervals.
4. Proposition 1 (p. 14): the $\mathbb R$-mode equilibrium; the firm collects, and $(r^*,p^*,\mathcal T_1(p^*))$ switches form at $v=2\mathcal M/\mathcal Z^2$.
5. Proposition 2 (p. 16): the $\mathbb C$-mode equilibrium; the firm collects, and $(\tilde p^*,\mathcal T_2(\tilde p^*))$ switches form at $v=2(1-\delta)$.
6. The equilibrium consumer surplus in both modes (proof of Theorem 1, p. ec23).
7. The equilibrium profit in both modes (proof of Theorem 1, p. ec23).

Significance

The theorem separates two effects of the GDPR on consumers. The direct privacy effect removes the exploitation loss $r\delta$ of every discloser. The indirect pricing effect works the other way: without the exploitation revenue the firm no longer discounts the price to attract disclosers, and once the market under the GDPR is fully covered the firm raises the price sharply. The threshold $\tau$ says exactly where the second effect overtakes the first. The result that profit and welfare rise regardless of $v$ shows that in a single-firm market the GDPR is never welfare-reducing; the supply-chain mission shows that this conclusion fails once a supplier sets a wholesale price, which is the paper's main policy message.

The paper's proofs (e-companion, Appendix C, pp. ec21–ec24) work with closed forms and leave several steps to "it can be verified". A formal proof checks the reduction from the game to those closed forms: existence and uniqueness of the REE at every price including the saturated range, global optimality of the prices over all of $\mathbb R$, and the collection decision against the full no-collection subgame. To our knowledge no part of this paper has been machine-checked.

Difficulty

The obvious argument plugs the printed formula $r(p)=\delta(v-p)/(2c(1-\delta)+\delta)$ into the profit (3) and maximizes. That formula solves the REE condition only while the market is not saturated; on the saturated range the REE intensity is the constant $\delta/\mathcal Z$, and the profit is a different function of $p$. The firm's problem is therefore a maximization of a piecewise function with a kink at full coverage, and the price comparison has to cover prices above $v$ (no sales) and the subgame without collection.

The consumer-surplus comparison involves two piecewise quadratics with different breakpoints, $2(1-\delta)<2\mathcal M/\mathcal Z^2$, and their single crossing at $\tau$ lies in the middle region where one mode is saturated and the other is not. Strictness of the profit and welfare comparisons needs the identity $\mathcal M-(1-\delta)\mathcal Z^2=c\delta^2+\delta^3>0$ and its relatives.

Formalization scope

All objects are real numbers; $c>0$, $0<\delta<1$ and $v>0$ are hypotheses of every statement. The paper does not state $v>0$; at $v\le0$ nothing is sold, every outcome is $0$, and every strict claim fails, so $v>0$ is a disclosed standing assumption.

Sets of consumers are measured by Lebesgue measure on $[0,1]$ ((volume S).toReal); consumer surplus is the interval integral $\int_0^1\max\{0,u(\theta)\}\,d\theta$. Indifferent consumers buy and disclose (a null set). The REE uses an IsMaxOn condition over $r\ge0$ and the disclosing quantity defined from utilities; neither $r(s)$ nor $\mathcal T_1$ is hard-coded. The firm's profit is defined from the REE response, not from the paper's (3). A strategy profile specifies a price for both collection decisions and an REE response at every $(\ell,p)$ with $p\in\mathbb R$; the comparisons in the goal are between on-path outcomes of such profiles.

The goal is not a comparison of printed closed forms: those are milestones 6–7. It asserts existence of an SPE in each mode, so "every equilibrium" is not vacuous; no price range is restricted and no off-path action is omitted.

Display (2) is stated in its corrected two-branch form for $p\le v$; Lemma 1 is stated for $p\le v$, with $r(p)$ the REE intensity at $p$. The paper's Table 1 (p. 12) misprints the purchase condition of disclosers and is not used.

A complete development needs volumes of intervals, the REE fixed point, maximization of concave piecewise quadratics over $\mathbb R$, and square-root threshold algebra. No probability or limits are involved. The consumer-stage definitions are shared verbatim with the supply-chain mission and may later be merged. Proofs of any milestone, and of auxiliary lemmas such as $2(1-\delta)\le 2\mathcal M/\mathcal Z^2$, are welcome.

Selected references

• F. Xu, X. Wang, F. Zhang, Consumer Privacy in Online Retail Supply Chains, Management Science, forthcoming; author manuscript, version of November 2024. https://doi.org/10.1287/mnsc.2022.01819
• European Union, Regulation (EU) 2016/679 (General Data Protection Regulation), 2016. https://eur-lex.europa.eu/eli/reg/2016/679/oj

Motivation

Large online retailers such as Amazon run two businesses on one storefront. They sell products themselves, and they host a marketplace on which third-party sellers sell, paying the platform a percentage of their revenue. A retailer that also runs the marketplace can decide which products to sell itself, and it controls which offer most consumers see. Competition authorities have asked whether this dual role lets the platform appropriate third-party sellers' business, and empirical work (Zhu and Liu, 2018) finds that Amazon enters only a small, high-performing subset of marketplace products.

Hervas-Drane and Shelegia (Retailer-Led Marketplaces, Management Science, 2025) give a model in which these choices can be computed. Its main result, Proposition 2, says which products the platform sells itself when its assortment is limited. This mission formalizes that proposition together with the pricing and entry results it rests on.

Setting

There is a unit mass of products. Each product is an independent market indexed by its consumers' valuation $v$. Valuations are distributed according to a probability measure $\mu$ on $[c,\infty)$ with CDF $G(v)=\mu((-\infty,v])$. Every unit costs $c>0$ to supply. Each market has a unit mass of unit-demand consumers, who buy at a price $p$ only if $p\le v$.

The monopolist retailer $M$ sets an ad valorem fee $f\in[0,1]$ on the third-party seller's revenue. He can steer a share $\lambda$ of consumers (the inattentive ones) to the seller of his choice; the remaining $1-\lambda$ buy from the cheapest offer, with ties going to $M$. He has capacity $k\in[0,1]$: he can supply at most a fraction $k$ of all products.

The game has three stages. In Stage 1 $M$ sets $f$. In Stage 2 each product's third-party seller $T$ decides whether to enter, and then $M$ chooses which products to enter. In Stage 3, in each market both present firms price sequentially: $T$ quotes first, then $M$ quotes and steers. The solution concept is subgame perfect equilibrium.

Proposition 1 solves Stage 3. A product supplied by $M$ alone (SBM) earns him $\pi_M^{SBM}=v-c$. A product supplied by $T$ alone (SBT) earns her $(1-f)v-c$ and earns him the fee $\pi_M^{SBT}=fv$. When both supply it (SBMT), $T$ charges

$$\bar p_T=\frac{\lambda v+c(1-\lambda)}{1-f(1-\lambda)},$$

and $M$ earns $\pi_M^{SBMT}=\lambda(v-c)+(1-\lambda)f\bar p_T$. Lemma 1 says $T$ enters exactly the products $v\ge v_T=c/(1-f)$, the marketplace products. An allocation of $M$ is any measurable set $A$ of products with $\mu(A)\le k$. His total profit is the SBM profit on $A$ below $v_T$, plus the SBMT profit on $A$ above $v_T$, plus the fee on marketplace products outside $A$.

Formalization targets

Goal: Proposition 2

Assume $\lambda\ge\tfrac12$ (Assumption 1) and $f<1$. Let $\Delta\pi(v)=\pi_M^{SBMT}(v)-\pi_M^{SBT}(v)$ and

$$v^*=\frac{c\lambda}{(1-f)^2(\lambda-f(1-\lambda))},\qquad \underline k=1-G(v^*).$$

Then:

• Mode I. If $k\le\underline k$, the optimal allocation is unique up to $\mu$-null sets and equals $[v_K,\infty)$ with $1-G(v_K)=k$ (empty if $k=0$).
• Mode II. If $k>\underline k$, it is $[v_L,v_T)\cup[v_H,\infty)$, where

$$\pi_M^{SBM}(v_L)=\Delta\pi(v_H),\qquad (1-G(v_H))+(G(v_T)-G(v_L))=k.$$

Milestones

1. Proposition 1, its three supply configurations: the SBM monopoly price, the SBT equilibrium, and the SBMT subgame perfect equilibrium, which is unique for $0<\lambda<1$ and $v(1-f)>c$.
2. Lemma 1 with (1) and Property 1: the entry threshold $v_T$.
3. The closed form of $\Delta\pi$, its positivity above $v_T$, and its monotonicity in $v$ and in $f$.
4. (A.2): $\Delta\pi(v^*)=\pi_M^{SBM}(v_T)$, and $v^*\ge v_T$.
5. The $(v_L,v_H)$ system has a unique solution when $k>\underline k$.

Significance

Proposition 2 is the step that the rest of the paper builds on. Display (4) writes the monopolist's profit as a function of the fee by plugging in the thresholds $v_L$, $v_T$, $v_H$, $v_K$ of Proposition 2. The optimal fee (Lemma 2, Proposition 3) and the policy comparisons of §6 (a pure-retailer response, fee regulation, steering bans) are all statements about that function. The two modes are also the paper's empirical prediction. A platform with little capacity, effective steering and a high fee competes only in the top marketplace products. With more capacity it also takes products no third party sells.

The paper proves Proposition 2 in Appendix A. The proof is an informal capacity-allocation argument. No machine-checked version exists. A formal proof has to turn the argument about entering the products of highest marginal profitability first into a statement about all measurable allocations of mass at most $k$. It must also prove uniqueness up to null sets, and handle the corners $k=0$, $k=1$ and $f=0$ that the prose passes over.

Difficulty

The obvious argument ranks products by the marginal profitability of entry and fills capacity from the top. Two facts make this harder than it looks. First, the ranking is not monotone in $v$. Below $v_T$ the gain is $v-c$; above $v_T$ it is $\Delta\pi(v)$, which starts again from $0$ at $v_T$. So the optimal set is an upper level set of a piecewise function, and in Mode II it has two components. Second, the claim is about every measurable set of mass at most $k$, not about thresholds. Optimality needs an exchange argument against arbitrary sets, and uniqueness needs the level sets of the gain to be $\mu$-null. Locating the thresholds also needs continuity and strict monotonicity of $G$, which come from the density and the full-support hypothesis.

Proposition 1 has its own subtlety. At $p_T=\bar p_T$ the monopolist is indifferent between matching $T$'s price and charging $v$. $T$'s best price exists only if $M$'s strategy breaks this tie in $T$'s favour, so the equilibrium has to be stated for strategies defined at every price of $T$.

Formalization scope

Products form a probability measure μ : Measure ℝ. The standing hypotheses are:

• $\mu((-\infty,c))=0$, $\mu\ll$ Lebesgue (the density $g$), and Integrable (fun v => v) μ, which the paper never states but which is needed for profits to be finite;
• $\mu$ charges every nonempty open interval of $[c,\infty)$, the reading of $G^{-1}$ in (3);
• $c>0$, $f\in[0,1)$, $\lambda\in[\tfrac12,1]$, $k\in[0,1]$.

The foreclosed corner $f=1$ ($v_T=\infty$) is not covered. Marketplace products are encoded as $\{v: c\le v(1-f)\}$. Optimal allocations quantify over all measurable sets of mass at most $k$, and uniqueness is up to $\mu$-null sets. Restricting allocations to intervals or to unions of two intervals would assume the conclusion, and the formalization does not do it.

In Proposition 1, $M$'s strategy is a function of $T$'s price that is a best response at every price, and $T$'s price is optimal against it. Uniqueness of the SBMT outcome is stated only for $0<\lambda<1$ and $v(1-f)>c$, where it holds. Lemma 1's duopoly clause likewise needs $0<\lambda<1$.

Two definition files carry the model:

• Model: $G$, the marketplace set, the Proposition 1 payoffs, $\Delta\pi$, $v^*$, $\underline k$, allocations and profit;
• PricingGame: the three pricing games and their equilibria.

The bathtub-type lemma behind Proposition 2 is reusable beyond this mission: among measurable sets of mass at most $k$, an upper level set of a weight maximizes its integral. Contributions of that lemma, of the milestones, and of alternative proofs are welcome.

Selected references

• A. Hervas-Drane, S. Shelegia, Retailer-Led Marketplaces, Management Science, Articles in Advance, 2025. https://doi.org/10.1287/mnsc.2023.00315
• F. Zhu, Q. Liu, Competing with Complementors: An Empirical Look at Amazon.com, Strategic Management Journal 39:2618–2642, 2018. https://doi.org/10.1002/smj.2932
• A. Hervas-Drane, S. Shelegia, Price Competition with a Stake in Your Rival, International Journal of Industrial Organization 84:102862, 2022 (the simultaneous-pricing variant of the pricing game). https://doi.org/10.1016/j.ijindorg.2022.102862

Motivation

Consumers judge a price against a reference price, an internal benchmark formed from the prices they have seen before. A price above the reference is perceived as a loss and depresses demand; a price below it is perceived as a gain and stimulates it. Because today's prices shape tomorrow's reference prices, a seller facing reference effects solves a dynamic problem even when demand is otherwise stationary. The single-product theory is classical: Popescu and Wu (2007) showed, for a broad class of demand models, that loss-averse consumers make optimal and myopic price paths converge monotonically, and Hu, Chen and Hu (2016) studied the cyclic behaviour that gain-seeking consumers can induce under linear demand.

Retailers sell many substitutable products, and the standard model of substitution is the multinomial logit (MNL). Guo, Jiang and Shen (2025) combine the two: each product has its own reference price and its own asymmetric sensitivities to gains and losses, and consumers choose among the products by MNL. This mission formalizes the paper's first set of results, on the myopic pricing policy, which maximises the current period's revenue at the current reference prices and ignores the effect on the future. Myopic pricing is both a widely used heuristic and the benchmark against which the optimal policy is measured later in the paper.

Setting

There are $n$ products $N=\{1,\dots,n\}$. Product $i$ has an intrinsic utility $a_i\in\mathbb R$, a price sensitivity $b_i>0$, and reference sensitivities $c_i^+\ge0$ (to gains) and $c_i^-\ge0$ (to losses). At price vector $p$ and reference price vector $r$ the deterministic utility of product $i$ is

$$u_i(p,r)=a_i-b_ip_i+c_i^+(r_i-p_i)_+-c_i^-(p_i-r_i)_+ ,$$

the market share of product $i$ is $q_i(p,r)=e^{u_i}/(1+\sum_k e^{u_k})$, and the single-period revenue is $\Pi(p,r)=\sum_i p_i\,q_i(p,r)$. Product $i$ is loss-averse if $c_i^+<c_i^-$, loss-neutral if $c_i^+=c_i^-$, and gain-seeking if $c_i^+>c_i^-$; the three sets are $N_l,N_n,N_g$.

Prices and reference prices lie in the box $\mathcal P^n=[0,p_H]^n$ with ceiling $p_H>0$. A myopic policy $p^m$ assigns to each $r\in\mathcal P^n$ a maximiser of $\Pi(\cdot,r)$ over $\mathcal P^n$; the maximum value is the optimal single-period revenue $\Pi^m(r)$. Reference prices follow exponential smoothing with memory $\alpha\in[0,1]$:

$$r^{t+1}=\alpha r^t+(1-\alpha)\,p^m(r^t),$$

and $\{p^m(r^t)\}_{t\ge0}$ is the myopic price path. A policy has a steady state if $p^m(r)=r$ for some $r\in\mathcal P^n$.

The paper assumes throughout that $p_H\ge\hat p_H$, where $\hat p_H$ is the unique root of the scalar equation (9), $p=\chi+\sum_i \frac{1}{b_i+c_i^+}e^{a_i-b_ip+(b_i+c_i^+)\chi-1}$ with $\chi=\max_i 1/(b_i+\min\{c_i^+,c_i^-\})$. This ceiling assumption makes the ceiling non-binding for the myopic problem.

Formalization targets

Goal: Theorem 3, long-run behaviour of the myopic policy

For every myopic policy $p^m$ and every $r^0\in\mathcal P^n$:

$$N_g=\emptyset\ \Longrightarrow\ p^m(r^t)\to L\in\mathcal P^n,\ \text{and } p^m(L)=L \text{ when } \alpha<1;$$ $$N_g\neq\emptyset\ \Longrightarrow\ p^m(r)\neq r\ \ \forall r\in\mathcal P^n,\ \text{and the path does not converge when } \alpha<1 .$$

Milestones

1. Proposition 1.2 (p. 10): (9) has a unique root $\hat p_H$, and for $p_H\ge\hat p_H$ the maximisers of $\Pi(\cdot,r)$ over $\mathcal P^n$ are its maximisers over $\mathbb R^n$.
2. Theorem 2 (p. 13): every myopic price is $\Pi^m(r)$ plus an explicit constant that depends on the product's type and on where $r_i$ lies relative to thresholds such as $\Pi^m(r)+Z_i$, $Z_i=\frac{\log(b_i+c_i^+)-\log(b_i+c_i^-)}{c_i^+-c_i^-}$.
3. Theorem 1 (p. 12): $\Pi^m(r)$ is the unique root of the scalar equation (13).
4. Corollary 1 (p. 12): the right-hand side of (13) is non-increasing in $\Pi$.
5. §3.1, p. 13: $\Pi^m(r)$ is non-decreasing in $r$.
6. Corollary 2 (p. 16): if every product is loss-neutral, the myopic policy has a unique steady state $p_i^{m\star}=\Pi^{m\star}+1/(b_i+c_i)$, with $\Pi^{m\star}$ the unique root of (18), and the price paths of all products move synchronously.

Significance

Theorem 3 separates two regimes by consumer type alone. With loss-averse and loss-neutral consumers a seller who reprices myopically settles at a stable price vector; with even one gain-seeking product no price vector is self-reproducing, and myopic prices keep oscillating. Theorems 1 and 2 are the structural results behind this: they reduce a non-concave, non-smooth $n$-dimensional optimisation to one scalar equation with a monotone right-hand side, which is also how the myopic policy is computed in practice. The same structure is used later in the paper to bound the gap between myopic and optimal revenue.

All results are proved in the paper; the proofs are in its online supplement (Appendices B.1–B.5), which is not part of the source file used here. None of the results is formalized. The work in this mission is the first machine-checked treatment of MNL pricing with reference effects: global optimality of a candidate maximiser for a non-concave revenue, the analysis of a scalar root equation with piecewise definitions, and the dynamics of a map that is continuous without gain-seeking products and discontinuous with them.

Difficulty

The obvious route to Theorem 2, setting the gradient of $\Pi(\cdot,r)$ to zero, fails twice. The revenue has kinks at $p_i=r_i$, so a maximiser may sit at a kink where no gradient exists; this is the middle branch $p_i^m=r_i$ for loss-averse products. And the revenue is not concave in prices: for a gain-seeking product the first-order conditions have several solutions, and a global maximiser must be singled out among them. The usual reformulation of MNL pricing in market-share variables, which restores concavity without reference effects, does not survive the kinks.

For Theorem 3 the difficulty is dynamic. Without gain-seeking products the myopic map is continuous, but the flat middle branch of (14) makes it non-contracting, so the standard contraction arguments do not apply, and the limit depends on the starting point. With a gain-seeking product the map jumps at the threshold $\Pi^m+Z_i$, so continuity-based arguments about the limit of the path are unavailable.

Formalization scope

Products are indexed by Fin n (0-based); vectors are Fin n → ℝ with the product topology and the coordinatewise order. The standing hypotheses $b_i>0$, $c_i^\pm\ge0$, $\alpha\in[0,1]$, $p_H>0$ and the ceiling assumption (as "some root of (9) is at most $p_H$") appear as hypotheses of every theorem that needs them; Corollary 1 needs only $b>0$, $c^\pm\ge0$. The market shares (3) are defined directly, without the Gumbel derivation. $\chi$ is an indexed supremum over Fin n (zero when $n=0$). The three sums of (13) are written as one sum whose term is chosen by product type.

Maximisers need not be unique, so a myopic policy is any selection of maximisers, and every statement holds for all selections; $\Pi^m(r)$ is the revenue of an arbitrary maximiser. "The unique solution" is split into "is a solution" and "every solution equals it". The following deviations are disclosed in the items: at the threshold $r_i=\Pi^m+Z_i$ of (16) both prices are maximisers, so only "one of the two" is claimed there; the fixed-point property of the limit in Theorem 3, and every limit claim of Corollary 2, require $\alpha<1$, since at $\alpha=1$ the price path is the constant $p^m(r^0)$; the non-convergence clause in Theorem 3.2 is an addition to the literal "no steady state". "Monotone decreasing" (Corollary 1) and "monotone increasing" (Corollary 2, §3.1) are read non-strictly.

A trivializing formalization is ruled out: Theorem 3.2 quantifies over every reference price in the box and every myopic selection, Theorem 3.1 asserts convergence from every initial reference price rather than the existence of some fixed point, and Theorems 1–3 keep the ceiling assumption, without which the maximiser can sit on the boundary and (14)–(16) fail.

A complete development needs: continuity and compactness facts for the MNL revenue on a box; optimality conditions for the kinked, non-concave revenue; one-variable analysis of the piecewise-exponential right-hand side of (13); and convergence results for monotone or continuous recursions in $\mathbb R^n$. The MNL and reference-price infrastructure is reusable by the five other missions of this series. Contributions to any milestone, and alternative proofs, are welcome.

Selected references

• M. A. Guo, H. Jiang, Z.-J. M. Shen, Multi-Product Dynamic Pricing with Reference Effects Under Logit Demand, Manufacturing & Service Operations Management, 2025; source used: SSRN 4189049, version of 2024-05-25. https://ssrn.com/abstract=4189049, https://doi.org/10.1287/msom.2024.0801
• I. Popescu, Y. Wu, Dynamic Pricing Strategies with Reference Effects, Operations Research 55(3), 2007. https://doi.org/10.1287/opre.1070.0393
• Z. Hu, X. Chen, P. Hu, Dynamic Pricing with Gain-Seeking Reference Price Effects, Operations Research 64(1), 2016. https://doi.org/10.1287/opre.2015.1446
• D. McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in Frontiers in Econometrics, Academic Press, 1974.