All missions

Why reference effects make pricing dynamic

Consumers judge a price against a reference price, an internal benchmark formed from the prices they have seen before. A price below the reference is perceived as a gain and raises demand; a price above it is perceived as a loss and lowers demand. Because today's price moves tomorrow's reference price, a seller who maximises the revenue of each period separately ignores how it erodes or builds future demand. This makes pricing a dynamic program, studied for a single product with linear demand by Popescu and Wu (Operations Research 2007) and Chen, Hu and Hu (Management Science 2017), among others.

Guo, Jiang and Shen (SSRN 4189049, published in Manufacturing & Service Operations Management, 2025) treat several substitutable products under multinomial-logit (MNL) demand. The dynamic program then has a continuous state of dimension $n$, and computing the optimal policy is impractical even for moderate $n$. The myopic policy, which maximises the current period's revenue only, is easy to compute. This mission formalizes the paper's bound on how much revenue the myopic policy can lose (Proposition 2).

Setting

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

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

the market share is $q_i(\mathbf p,\mathbf r)=e^{u_i}/(1+\sum_{k\in N}e^{u_k})$, and the single-period revenue is $\Pi(\mathbf p,\mathbf r)=\sum_{i\in N}p_iq_i(\mathbf p,\mathbf r)$.

Prices and reference prices lie in the admissible box $\mathcal P^n=[0,p_H]^n$ with a price ceiling $p_H>0$. The reference price follows exponential smoothing with memory $\alpha\in[0,1]$: $\mathbf r^{t+1}=\alpha\mathbf r^t+(1-\alpha)\mathbf p^t$. Revenue is discounted by $\beta\in[0,1)$.

• The optimal value $V^\star(\mathbf r^0)$ is the supremum of $\sum_{t\ge0}\beta^t\Pi(\mathbf p^t,\mathbf r^t)$ over all price sequences in $\mathcal P^n$.
• A myopic policy $\mathbf p^m$ picks, for each $\mathbf r\in\mathcal P^n$, a maximiser of $\Pi(\cdot,\mathbf r)$ over $\mathcal P^n$. Its value $V^m(\mathbf r^0)=\sum_{t\ge0}\beta^t\Pi(\mathbf p^m(\mathbf r^t),\mathbf r^t)$ is taken along $\mathbf r^{t+1}=\alpha\mathbf r^t+(1-\alpha)\mathbf p^m(\mathbf r^t)$.
• The ceiling condition: $p_H\ge\hat p_H$, where $\hat p_H$ is the root of the scalar equation (9) of the paper, $p=\chi+\sum_i\frac{1}{b_i+c_i^+}\exp(a_i-b_ip+(b_i+c_i^+)\chi-1)$ with $\chi=\max_i 1/(b_i+\min\{c_i^+,c_i^-\})$. It makes the ceiling non-binding for the single-period problem, and the paper assumes it throughout §3–§4.

Formalization targets

Goal: Proposition 2 (optimality gap)

With $\omega=\max_{i\in N}\{c_i^+/(b_i+c_i^+),\ c_i^-/(b_i+c_i^-)\}$, for every $\mathbf r^0\in\mathcal P^n$ and every myopic policy,

$$0\le V^\star(\mathbf r^0)-V^m(\mathbf r^0)\le\frac{\beta(1-\alpha)}{(1-\alpha\beta)(1-\beta)}\cdot\omega\,p_H .$$

Milestones

1. The Bellman equation (6), p. 9: $V^\star(\mathbf r^0)=\max_{\mathbf p\in\mathcal P^n}\{\Pi(\mathbf p,\mathbf r^0)+\beta V^\star(\alpha\mathbf r^0+(1-\alpha)\mathbf p)\}$, with the maximum attained.
2. The left inequality $V^m(\mathbf r^0)\le V^\star(\mathbf r^0)$, stated in §4.1, p. 17.
3. Proposition 1.1, p. 10: if $\alpha<1$, $\beta>0$ and $\max_ic_i^+>0$, then $V^\star(\mathbf r^0)$ is non-decreasing in $p_H$ and $\lim_{p_H\to\infty}V^\star(\mathbf r^0)=\infty$. It explains why the gap is linear in $p_H$ and why a ceiling is needed at all.

Significance

The bound is uniform in the initial reference price and has an explicit constant. It vanishes in three regimes: $\alpha=1$ (the reference price never moves), $\beta=0$ (only the present counts) and $\omega=0$ (no reference effect). It quantifies how much the intertemporal structure costs a seller who ignores it. The myopic policy is computable by a one-dimensional root search (Theorem 1 of the paper), while the optimal policy suffers from the curse of dimensionality, so the bound is what makes the myopic policy a usable benchmark.

The paper proves Proposition 2 in its online supplement (Appendix C.1), which is not part of the source file used for this mission. To our knowledge, none of these results has a machine-checked proof. Formalizing them yields a verified Bellman equation for a deterministic dynamic program with a continuous multidimensional state and a nonsmooth, nonconcave reward.

Difficulty

The left inequality only uses the fact that the myopic price sequence is admissible. The right inequality is the content. Comparing the two value functions period by period fails: in a given period the optimal policy may earn less than the myopic one, and its later advantage comes from having moved the reference price. The two policies also generate different reference paths, so their revenues are evaluated at different states, and the sensitivity of the revenue to the reference price enters only through the constant $\omega$. The revenue is not concave in prices or in reference prices, and the kinks at $p_i=r_i$ make it nonsmooth. The Bellman equation itself needs the optimal value to be well behaved enough in $\mathbf r$ for the one-step maximum to be attained.

Formalization scope

Products are indexed by Fin n (product $i$ is Lean index $i-1$), and vectors are Fin n → ℝ. The shares are defined directly by the logit formula; the Gumbel random-utility derivation is motivation only. The standing assumptions $b>0$, $c^\pm\ge0$, $\alpha\in[0,1]$, $\beta\in[0,1)$ and $p_H>0$ are hypotheses of every theorem. The goal also assumes the ceiling condition $p_H\ge\hat p_H$, as a standing assumption of §2.4. That condition is stated as the existence of a root of (9) at most $p_H$. The Bellman equation omits the ceiling condition (it holds without it). Proposition 1.1 varies $p_H$, so it does not take the condition.

• $V^\star$ is optValue, the supremum over all admissible price sequences, built as an instance of the published deterministic dynamic program KarlinDP.Deterministic.optimalReturn (Karlin 1955). The paper writes $V^\star$ as a maximum over stationary policies and uses it through (6); milestone 1 is the theorem that connects the two.
• The bound holds for every myopic selection, because single-period maximisers can tie.
• $\omega$ and $\chi$ are maxima over $N$, written ⨆ i, which is $0$ when $n=0$ (then $V^\star=V^m=0$).

Lean's real supremum is $0$ on an unbounded family and its tsum is $0$ on a non-summable series. Neither default is reached here: with $\beta<1$ and $p_H>0$ the family is nonempty and bounded by $p_H/(1-\beta)$, and every series is summable. So the goal cannot hold vacuously through a junk value. In particular, $V^\star$ may not be replaced by an arbitrary solution of (6), and the constant may not be weakened, for example by replacing $\omega$ with $1$.

Needed infrastructure: continuity of the MNL revenue, the Bellman equation for a discounted deterministic program on a compact action set, and bounds on the myopic value $\Pi^m(\mathbf r)=\max_{\mathbf p\in\mathcal P^n}\Pi(\mathbf p,\mathbf r)$ as a function of $\mathbf r$. The first two are reusable beyond this mission. Contributions toward any milestone are welcome.

Selected references

• M. A. Guo, H. Jiang, Z.-J. M. Shen, Multi-Product Dynamic Pricing with Reference Effects Under Logit Demand, SSRN 4189049 (version of 2024-05-25); Manufacturing & Service Operations Management, 2025. 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):413–429, 2007. https://doi.org/10.1287/opre.1070.0393
• X. Chen, P. Hu, Z. Hu, Efficient algorithms for the dynamic pricing problem with reference price effect, Management Science 63(12):4389–4408, 2017. https://doi.org/10.1287/mnsc.2016.2554
• S. Karlin, The structure of dynamic programming models, Naval Research Logistics Quarterly 2(4):285–294, 1955. https://doi.org/10.1002/nav.3800020408
• D. McFadden, Conditional logit analysis of qualitative choice behavior, in Frontiers in Econometrics, 105–142, 1974.

Motivation

Financial networks are webs of liabilities: firm $u$ owes firm $v$ an amount $c_{(u,v)}$, and every firm holds some external assets. When firms cannot pay in full, how much money actually moves through the network depends on how each firm splits its available funds among its creditors. The classical clearing model of Eisenberg and Noe (2001) fixes this split by a proportional rule. Flow allocation games, introduced by Bertschinger, Hoefer and Schmand (arXiv:1908.01714, Mathematics of Operations Research, 2025), make it strategic: every firm chooses how to allocate whatever it receives, and the resulting payments are the clearing state of the chosen strategies.

Because money that circulates comes back, the total amount of flow in such a network is driven by cycles, and cycles require several firms to cooperate. The natural solution concept is therefore the strong equilibrium, which is stable against joint deviations of coalitions. The paper shows that in unit-ranking games a strong equilibrium maximizing total flow always exists (Theorem 9, price of stability $1$). This mission concerns the other side: how much total flow can the worst strong equilibrium lose, and which structural parameter of the network controls the loss.

Setting

A flow allocation game $\Gamma=(G,(b_v)_{v\in V},(c_e)_{e\in E})$ consists of a finite directed graph $G=(V,E)$ (parallel edges allowed), a fixed supply $b_v\in\mathbb N_0$ at each node and a capacity $c_e\in\mathbb N_0$ on each edge. Every node is a player. $E^+(v)$ and $E^-(v)$ denote the outgoing and incoming edges of $v$, and $c_v^+=\sum_{e\in E^+(v)}c_e$.

In a unit-ranking game, player $v$ chooses for each edge $e\in E^+(v)$ a non-decreasing function $a_e:\mathbb N_0\to\mathbb N_0$ with $a_e(y)\le c_e$ and $\sum_{e\in E^+(v)}a_e(y)=\min\{c_v^+,y\}$: given a total supply $y$, it forwards all of it until its outgoing edges are full, one unit at a time according to a ranking of unit capacities. A flow $f$ is feasible for a profile $\mathbf a$ if $f_{(v,w)}=a_{(v,w)}(f_v)$ with $f_v=b_v+\sum_{e\in E^-(v)}f_e$. The clearing state $\hat f$ is the coordinatewise largest feasible flow; player $v$'s utility is $u_v(\mathbf a)=\sum_{e\in E^+(v)}\hat f_e$, and the total flow is

$$\mathrm{Flow}(\mathbf a)=\sum_{e\in E}\hat f_e .$$

A profile is a strong equilibrium if no non-empty coalition $C\subseteq V$ can jointly switch to other unit-ranking strategies so that every member of $C$ strictly gains.

The circulation network $G'$ adds an auxiliary node $s$ with edges $(v,s)$ of unbounded capacity and $(s,v)$ of capacity $b_v$ for every $v$. An optimal circulation $f^*$ of $G'$ maximizes $\sum_{e\in E'}f^*_e$. A decomposition $\mathcal C(f^*)=\{C_1,\dots,C_k\}$ of $f^*$ into cycles of unit flow is a list of simple directed cycles of $G'$ that uses each edge exactly as often as $f^*$ has units on it. The parameter of this mission is

$$d=\min_{f^*,\ \mathcal C(f^*)}\ \max_{C_i\in\mathcal C(f^*)}|C_i| ,$$

the smallest possible size of the longest cycle, over all decompositions of all optimal circulations; sizes count auxiliary edges.

Formalization targets

Goal: Theorem 16 (p. 30)

In unit-ranking games, the price of anarchy for strong equilibria in terms of Flow is at most $d$: for every strong equilibrium $\mathbf a$ and every unit-ranking profile $\mathbf a'$,

$$\mathrm{Flow}(\mathbf a')\le d\cdot\mathrm{Flow}(\mathbf a).$$

The statement fixes no constant beyond the structural parameter $d$ and holds for all capacities and supplies.

Milestones (proof of Theorem 16, p. 30)

1. An optimal circulation yields the optimal total flow, and

$$\mathrm{Flow}(\mathbf a^*)=\sum_{C_i\in\mathcal C(f^*)}|C_i|-2\sum_{v}b_v\le\sum_{C_i\in\mathcal C(f^*)}d .$$

2. In a strong equilibrium every simple cycle of $G$ contains an edge with $\hat f_e=c_e$.
3. $\mathrm{Flow}(\mathbf a)$ is at least the number of cycles of $\mathcal C(f^*)$ that avoid $s$.

Companions

• Theorem 16 for games without fixed supplies ($b\equiv0$), the setting of Propositions 15 and 17.
• Proposition 17 (p. 30). For every $d\ge2$ there is a unit-ranking game with parameter $d$ and a strong equilibrium $\mathbf a$ with $\mathrm{Flow}(\mathbf a)>0$ and $(d-1)\,\mathrm{Flow}(\mathbf a)\le\mathrm{Flow}(\mathbf a^*)$.

Significance

The bound identifies the length of the circulating cycles as the quantity that governs the efficiency of coalition-stable payment behaviour. In networks whose optimal circulation decomposes into short cycles, such as bilateral or triangular netting of liabilities, every strong equilibrium clears at least a $1/d$ fraction of the optimal total payments; Proposition 17 shows that long cycles genuinely cost efficiency, so the bound is tight up to one. For pure Nash equilibria no such bound exists (Proposition 15, the price of anarchy is unbounded), so the result separates coalitional from unilateral stability.

The results are proved on paper; none of them is machine-checked. A formalization adds a precise account of the model (clearing state as a supremum of feasible flows, unit-ranking strategies as functions on $\mathbb N_0$, cycle decompositions of the circulation network) and checks a proof whose last step, as printed, needs repair. The printed last display, $\mathrm{Flow}(\mathbf a)\ge\sum_{C_i\in\mathcal C(f^*)}1$, does not hold for cycles passing through the auxiliary node $s$: with a single node $v$, $b_v=1$ and no outgoing edges, $\mathcal C(f^*)=\{(s,v,s)\}$ but $\mathrm{Flow}(\mathbf a)=0$. The theorem itself is not contradicted by this example, and the printed argument is complete for games without fixed supplies. The cycles through the auxiliary node need a separate count, which is part of the work this mission asks for.

Difficulty

The upper bound compares an arbitrary strong equilibrium with an optimum that may look nothing like it. The obvious approach, counting the units of each optimal cycle that also carry equilibrium flow, fails: the clearing state is a fixed point of all strategies at once, so whether a unit reaches an edge depends on decisions all around the network, and the equilibrium may route its flow along entirely different cycles. A single player cannot complete a cycle on its own, which is why the Nash price of anarchy is unbounded; any argument has to use coalitional deviations, and a deviation changes the clearing state globally, so its effect on each member's utility must be controlled through the fixed point.

The second difficulty is the auxiliary node. A cycle of the optimal decomposition that passes through $s$ contains a node that is not a player, so no coalition of players can claim it, and the unit of flow it represents may sit on an auxiliary edge that $\mathrm{Flow}$ does not count. These cycles are exactly where the printed argument stops short.

Formalization scope

Supplies, capacities, strategies and flows are natural numbers, as the paper prescribes for unit-ranking games. The graph is a finite type of nodes $V$ and a finite type of edges $E$ with tail and head maps, so parallel edges and loops are allowed. The clearing state is the coordinatewise sSup of the feasible flows. Coalitions are non-empty, and deviations range over unit-ranking profiles. Optimal circulations are optimal among integral circulations. Cycles of $G'$ are lists of edges with pairwise distinct start nodes, and decompositions are lists of cycles counted with multiplicity. Nodes of $G'$ are Option V, with none the node $s$.

The price of anarchy is stated multiplicatively, $\mathrm{Flow}(\mathbf a')\le d\cdot\mathrm{Flow}(\mathbf a)$, with no division, so a zero-flow equilibrium cannot satisfy the goal vacuously through a junk quotient. The parameter $d$ enters as a hypothesis, "some decomposition of some optimal circulation has all cycles of size at most $d$", which is equivalent to the bound for the min-max $d$ and avoids an infimum that would be $0$ on an empty set. In Proposition 17 the strong equilibrium is required to have positive flow, since otherwise the lower bound would hold trivially.

Not formalized: the complexity results of the paper, the bounds for other quality measures (Proposition 18) and for Nash equilibria (Proposition 15). A complete development needs the integral version of the lattice theorem for feasible flows (Theorem 2), the existence of a Flow-optimal profile from the proof of Theorem 9, and integral cycle decomposition of circulations; the last two are reusable beyond this mission. Contributions are welcome on each milestone, on a separate count for cycles through $s$, and on the explicit construction of Proposition 17.

Selected references

• N. Bertschinger, M. Hoefer, D. Schmand, Flow Allocation Games, Mathematics of Operations Research, 2025; preprint arXiv:1908.01714v3, 2023. https://arxiv.org/abs/1908.01714
• L. Eisenberg, T. H. Noe, Systemic Risk in Financial Systems, Management Science 47(2), 236–249, 2001. https://doi.org/10.1287/mnsc.47.2.236.9835

Why measure sensitivity by optimal transport

Global sensitivity analysis asks how much the uncertainty in an output $Y$ of a model or a data set is explained by an input $X$. A large family of indices has the form "expected discrepancy between the marginal law of $Y$ and its conditional law given $X$": the variance-based index of Sobol' and Wagner, the $L^1$ density-based index, Kuiper and Cramér–von Mises indices. Borgonovo, Figalli, Plischke and Savaré (Management Science 2025, doi:10.1287/mnsc.2023.01796) take the discrepancy to be an optimal-transport cost. The resulting indices apply to multivariate outputs, need no density, and include as special cases the numerator of Wiesel's Wasserstein correlation coefficient (Wiesel 2022, arXiv:2207.14079).

A sensitivity index is meant to measure information: how much knowing $X$, or a coarsening of $X$, tells about $Y$. Two properties make this reading legitimate. Coarser information must never be worth more than finer information, and an index computed from increasingly fine observations of $X$ must approach the value for the limiting information. This mission formalizes both properties for the optimal-transport indices, Theorems 8 and 9 of the paper. Theorem 9 is also the last step of the paper's consistency proof for its partition estimator (Theorem 21).

Setting

Let $(\Omega,\mathcal B,\mathbb P)$ be a probability space, $\mathsf X$ and $\mathsf Y$ Polish spaces with Borel σ-algebras $\mathscr B(\mathsf X)$, $\mathscr B(\mathsf Y)$, and $X:\Omega\to\mathsf X$, $Y:\Omega\to\mathsf Y$ measurable maps. Write $\mu$ and $\nu$ for the laws of $X$ and $Y$.

A cost is a continuous function $\mathsf k:\mathsf Y\times\mathsf Y\to[0,+\infty]$ with $\mathsf k(y,y')=0$ exactly when $y=y'$. The optimal-transport cost between probability measures $\nu,\nu'$ on $\mathsf Y$ is

$$K(\nu,\nu')=\inf_{\pi\in\Pi(\nu,\nu')}\iint\mathsf k(y,y')\,d\pi(y,y'),$$

where $\Pi(\nu,\nu')$ is the set of probability measures on $\mathsf Y\times\mathsf Y$ with marginals $\nu$ and $\nu'$.

For a σ-algebra $\mathcal F\subseteq\mathscr B(\mathsf X)$, representing partial information on $X$, a version of the conditional distribution of $Y$ given $(X,\mathcal F)$ is a family $(\nu^{\mathcal F}_x)_{x\in\mathsf X}$ of probability measures on $\mathsf Y$ with $x\mapsto\nu^{\mathcal F}_x(B)$ $\mathcal F$-measurable and

$$\mathbb P(X\in A,\ Y\in B)=\int_A\nu^{\mathcal F}_x(B)\,d\mu(x)\qquad(A\in\mathcal F,\ B\in\mathscr B(\mathsf Y)).$$

The OT-based sensitivity measure (Definition 1) is

$$\xi^K(Y,X\mid\mathcal F)=\int_{\mathsf X}K(\nu,\nu^{\mathcal F}_x)\,d\mu(x)\in[0,+\infty],$$

written $\xi^K(Y,X)$ when $\mathcal F=\mathscr B(\mathsf X)$. For a Borel map $g:\mathsf X\to\mathsf U$ into a Polish space, $U=g\circ X$ is a new random variable and $\xi^K(Y,U)$ is defined in the same way on $\mathsf U$; $\sigma(g)$ is the σ-algebra generated by $g$.

Formalization targets

Goal: continuity along increasing σ-algebras (Theorem 9)

For an increasing sequence $\mathcal F^1\subseteq\mathcal F^2\subseteq\cdots$ of sub-σ-algebras of $\mathscr B(\mathsf X)$ with join $\mathcal F=\bigvee_n\mathcal F^n$,

$$\lim_{n\to\infty}\xi^K(Y,X\mid\mathcal F^n)=\xi^K(Y,X\mid\mathcal F)\quad\text{in }[0,+\infty].$$

Milestones

• (66) and (68): the conditional law given coarser information is a mixture of the conditional laws given $X$, against the disintegration of $\mu$.
• Jensen step: $K\big(\nu,\int\eta_x\,d\rho(x)\big)\le\int K(\nu,\eta_x)\,d\rho(x)$.
• Theorem 8: $\xi^K(Y,X)\ge\xi^K(Y,X\mid\mathcal F)$ (23); $\xi^K(Y,X)\ge\xi^K(Y,U)=\xi^K(Y,X\mid\sigma(g))$ (24); equality $\xi^K(Y,X)=\xi^K(Y,U)$ when $g$ is injective almost everywhere.
• Relative monotonicity: $\xi^K(Y,X\mid\mathcal G)\le\xi^K(Y,X\mid\mathcal F)$ for $\mathcal G\subseteq\mathcal F$.
• Almost-sure weak convergence of the conditional laws $\nu^n_x\to\nu^\infty_x$ for $\mu$-a.e. $x$.
• Lower semicontinuity of $K(\nu,\cdot)$ under weak convergence.

Significance

The results. Theorem 8 is the formal statement that the OT indices value information monotonically: a transformation $g(X)$ of an input, such as a discretization or an aggregation of features, can only lose explanatory power, and loses none when $g$ is injective. Theorem 9 makes the indices continuous in the information: refining a partition of the input space, as an estimator does when the sample grows, recovers the index of the limiting σ-algebra. The paper relies on Theorem 9 to prove that its given-data estimator is consistent, and on Theorem 8 to justify its interpretation of the indices as values of information.

The formalization. The proofs are on pp. 35–36 of the authors' manuscript. As far as we know, none of these statements has been machine-checked. Formalizing them requires conditional distributions relative to arbitrary sub-σ-algebras, the convexity of optimal-transport costs under mixtures, and their lower semicontinuity under weak convergence, which are general facts of optimal transport that the platform does not yet have.

Difficulty

The monotonicity in Theorem 8 is a Jensen inequality, but it is applied to a function of a measure, $K(\nu,\cdot)$, along a mixture indexed by a disintegration, so the step needs a measurable choice of near-optimal couplings. Without such a choice the averaged coupling is not defined.

For Theorem 9, the inequality $\limsup\le$ follows from monotonicity, and $\liminf\ge$ is the substance. The natural first idea, Lévy's upward theorem applied to $\mathbb E[\varphi(Y)\mid X,\mathcal F^n]$, gives convergence for one test function at a time and outside a null set that depends on $\varphi$. Weak convergence of the conditional laws for almost every $x$ is a statement about all test functions at once. Even with it, $K(\nu,\cdot)$ is only lower semicontinuous, not continuous, and the cost $\mathsf k$ may be unbounded and take the value $+\infty$. No integrability hypothesis is available: the theorem holds without assuming $\mathbb M^K[Y]<\infty$, including when the limit is $+\infty$.

Formalization scope

• $\mathsf X$, $\mathsf Y$, $\mathsf U$ are Polish spaces with Borel σ-algebras; the paper's supports in $\mathbb R^{n_X}$, $\mathbb R^{n_Y}$ are such spaces.
• $X$, $Y$, $g$ are measurable, and $\mathbb P$ is a probability measure.
• Costs, $K$, $\mathbb M^K$ and $\xi^K$ take values in $[0,+\infty]$ (ℝ≥0∞); integrals are lower Lebesgue integrals.
• $K$ is the published platform definition RWPI.SqrtLasso.transportCost. Its first argument is the marginal $\nu$ and its second the conditional law.
• Conditional distributions are characterized by the defining property above (IsCondDistrib), never constructed. Every statement holds for every version, and versions for different $n$ need not be compatible.
• The join $\bigvee_n\mathcal F^n$ is the supremum of σ-algebras (⨆ n, Fs n), and the sequence is indexed from $0$.
• Weak convergence is tested against all bounded continuous real functions.
• "Injective almost everywhere" means injective on a measurable set of full $\mu$-measure.

The goal is a Tendsto in $[0,+\infty]$, not a one-sided bound. In particular, a proof of only $\limsup\le$ (monotonicity) or of the statement under a finiteness hypothesis on $\mathbb M^K[Y]$ does not close it. $\xi^K(Y,U)$ uses the conditional distribution of $Y$ given the random variable $U$ on $\mathsf U$, not that given $(X,\sigma(g))$; their equality is part of (24).

Two readings are disclosed corrections. Theorem 9's "sub-σ-algebras in $\mathcal F$" is read as sub-σ-algebras of $\mathscr B(\mathsf X)$. The comparison of two sub-σ-algebras $\mathcal G\subseteq\mathcal F$, used in the proof of Theorem 9 but stated in Theorem 8 only for $\mathcal F=\mathscr B(\mathsf X)$, is posed as its own milestone.

Reusable infrastructure includes the following, and contributions of any of them are welcome:

• existence and uniqueness of conditional distributions given a sub-σ-algebra;
• mixture convexity and lower semicontinuity of optimal-transport costs;
• almost-sure weak convergence of conditional laws along a filtration.

Selected references

• E. Borgonovo, A. Figalli, E. Plischke, G. Savaré, Global Sensitivity Analysis via Optimal Transport, Management Science, 2025 (authors' manuscript of 7 March 2024). https://doi.org/10.1287/mnsc.2023.01796
• J. Wiesel, Measuring association with Wasserstein distances, arXiv preprint, 2022. https://arxiv.org/abs/2207.14079
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
• L. Schwartz, Radon Measures on Arbitrary Topological Spaces and Cylindrical Measures, Oxford University Press, 1973.
• I. M. Sobol', Sensitivity estimates for nonlinear mathematical models, Mathematical Modeling and Computational Experiment, 1993.

Motivation

Optimal auction theory in the tradition of Myerson (1981) assumes that the seller knows the distribution of the buyers' valuations. In practice that distribution is estimated, misspecified, or simply unknown. Prior-independent mechanism design asks for a mechanism that performs well across a whole class of distributions, without being tuned to any one of them. A natural yardstick is regret: the gap between the revenue the seller would extract if she knew the valuations, namely the highest valuation, and the revenue her mechanism actually collects. The seller chooses a mechanism to minimize the worst case of this gap over all distributions Nature may pick.

For a single buyer, Bergemann and Schlag (2008) showed that the minimax regret over valuations supported on $[0,1]$ is $1/e$, attained by a posted price drawn at random with CDF $\log v + 1$ on $[1/e, 1]$. Whether a comparably explicit answer exists for $n$ buyers, and whether the familiar second-price auction remains optimal among all dominant-strategy mechanisms, was open. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478v5, Operations Research 2025) answer both questions for i.i.d. valuations. This mission formalizes that answer: their Theorem 1.

Setting

A seller has one indivisible item and $n \ge 1$ buyers with valuations $v = (v_1, \dots, v_n) \in [0,1]^n$. A mechanism $m = (x, p)$ assigns to every valuation profile allocation probabilities $x_i(v) \in [0,1]$ and expected payments $p_i(v)$. It is dominant-strategy incentive compatible (DSIC), written $m \in \mathcal M$, if for all $i$, all $v$ and every misreport $\hat v_i$:

$$v_i x_i(v) - p_i(v) \ge 0 \;\;\text{(IR)}, \qquad v_i x_i(v) - p_i(v) \ge v_i x_i(\hat v_i, v_{-i}) - p_i(\hat v_i, v_{-i}) \;\;\text{(IC)}, \qquad \textstyle\sum_i x_i(v) \le 1 \;\;\text{(AC)}.$$

For a joint distribution $F$ of $v$, the regret is

$$\mathrm{Regret}(m, F) = \mathbb E_{v \sim F}\Big[\max(v) - \sum_{i=1}^n p_i(v)\Big],$$

and the minimax regret over a class $\mathcal F$ of distributions is $\mathcal R^*_n(\mathcal F) = \inf_{m \in \mathcal M} \sup_{F \in \mathcal F} \mathrm{Regret}(m, F)$. Here $\mathcal F_{\mathrm{iid}}$ is the class of product laws $G^{\otimes n}$ whose marginal $G$ is supported on $[0,1]$.

A second-price auction with random reserve $\mathrm{SPA}(\Phi)$ draws a reserve price $q$ from a distribution $\Phi$. The highest bidder wins if her bid is at least $q$ and pays $\max(v^{(2)}, q)$, where $v^{(1)} \ge v^{(2)}$ are the two highest valuations. Otherwise nothing is sold.

Two explicit functions enter the answer. For $r \in (0,1)$, let

$$\mathrm{rEq}_n(r) = (1-r)^{n-1} + \log r + \sum_{k=1}^{n-1} \frac{(1-r)^k}{k},$$

and, for $r < v \le 1$,

$$\Phi^*_n(v) = \Big(\frac{v}{v-r}\Big)^{n-1}\log\Big(\frac vr\Big) - \sum_{k=1}^{n-1} \frac1k \Big(\frac{v}{v-r}\Big)^{n-1-k},$$

with $\Phi^*_n = 0$ below $r$ and $1$ above $1$. The isorevenue marginal $F^*_n(v) = 1 - r/v$ on $[r, 1)$, $F^*_n(1) = 1$, is the law under which every posted price in $[r,1]$ earns the same revenue $r$.

Formalization targets

Goal: Theorem 1

Let $r^*_n$ be the root of $\mathrm{rEq}_n$ in $(0, 1/n)$; it is the only root in $(0,1)$. A reserve distribution on $[r^*_n, 1]$ with CDF $\Phi^*_n$ exists. The auction $\mathrm{SPA}(\Phi^*_n)$ is DSIC and minimax-regret optimal, and

$$\mathcal R^*_n(\mathcal F_{\mathrm{iid}}) = (1-r^*_n)^{n-1} - \int_{r^*_n}^1 \Big(1 - \frac{r^*_n}{v}\Big)^{n-1} dv.$$

The Lean goal states the location and uniqueness of the root, the existence of the reserve law, the DSIC property, the upper bound for $\mathrm{SPA}(\Phi^*_n)$ against every i.i.d. law, the matching lower bound for every DSIC mechanism, and the literal identity for $\mathcal R^*_n(\mathcal F_{\mathrm{iid}})$.

Milestones

1. Lemma B-1 (p. App-4): an integration-by-parts identity for $\int h\,dG$, split at $r^*$.
2. Proposition 1 (p. 16): the regret of $\mathrm{SPA}(\Phi)$, for $\Phi$ with a density on $[r^*, 1]$, in terms of the order-statistic CDFs; joint and i.i.d. forms.
3. Proposition A-3 (p. App-2): the root $r^*_n$; $\Phi^*_n$ equals a power series, solves the ODE $(\Phi^*)' + \frac{(n-1)r^*_n}{v(v-r^*_n)}\Phi^* = \frac1v$, and satisfies $\Phi^*_n(r^*_n) = 0$ and $\Phi^*_n(1) = 1$; the regret at the candidate saddle point equals the value.
4. Step 1 of the proof of Theorem 1 (p. 17): against $\mathrm{SPA}(\Phi^*_n)$, the i.i.d. isorevenue law is a worst case.
5. Step 2 (p. 17): against the i.i.d. isorevenue law, $\mathrm{SPA}(\Phi^*_n)$ has the least regret among all DSIC mechanisms.

A companion item states Corollary 1 (p. 14): for $n = 1$, $r^*_1 = 1/e$, $\Phi^*_1(v) = \log v + 1$ on $[1/e, 1]$, and the minimax regret is $1/e$.

Significance

The theorem gives, for every number of buyers, a closed-form description of the minimax-regret optimal mechanism among all DSIC mechanisms, together with its value. The optimum is a familiar format, a second-price auction, but its reserve price must be randomized. The same saddle point is the starting point for the paper's results on affiliated and arbitrary joint valuations, which are separate missions of this series.

The result is proved on paper. To our knowledge none of it has been formalized. A complete development would supply machine-checked versions of several tools that recur in robust mechanism design: DSIC mechanisms with randomized allocations, the regret functional, order-statistic CDFs of product measures, Myerson-type revenue characterizations under distributions with atoms, and saddle-point arguments for inf–sup problems over mechanisms and distributions.

Difficulty

The upper bound (Step 1) is a pointwise optimization once the regret of $\mathrm{SPA}(\Phi)$ is written through the CDFs of the order statistics. Writing it that way already requires integration by parts against arbitrary distributions on $[0,1]$, which may have atoms.

The lower bound (Step 2) is the hard direction. One must show that no DSIC mechanism beats $\mathrm{SPA}(\Phi^*_n)$ against the isorevenue law. The standard route through Myerson's virtual values does not apply directly: the isorevenue law is a mixture of a density and a point mass at $1$, so the revenue of a general DSIC mechanism has to be characterized from first principles. That characterization starts from the payment identity for dominant-strategy mechanisms. The closed forms also involve a transcendental root $r^*_n$ and a logarithmic ODE solution, so the monotonicity and boundary facts about $\Phi^*_n$ (it is a CDF, $\Phi^*_n(1) = 1$) need real analysis rather than numerics.

Formalization scope

Buyers are indexed by Fin n, valuations are functions Fin n → ℝ, and distributions are measures on that space. (IR), (IC) and (AC) are imposed for valuations in $[0,1]^n$, which is all the seller considers. Two conditions are added to DSIC so that the expectation in the regret is meaningful: the allocation and payment rules are measurable, and payments are bounded on the cube. The second-price auction breaks ties in favour of the lowest index; the revenue does not depend on the rule. A reserve law or an isorevenue law is described by a hypothesis on its CDF. $\Phi^*_n$ is defined piecewise, so its closed form is never evaluated at the singular point $v = r^*_n$, and "$\Phi^*_n(r^*_n) = 0$" is stated as a one-sided limit. The minimax regret is a real infimum over the nonempty class of DSIC mechanisms of real suprema of bounded families. Uniqueness of $r^*_n$ is stated on $(0,1)$, which is what the paper's proof establishes.

Trivializing formalizations are ruled out explicitly. The regret is not a Bochner integral of a possibly non-integrable payment, which Lean would set to $0$. The mechanism class is not restricted to second-price auctions. The value is the explicit integral, not a sSup. The root's location in $(0, 1/n)$ is part of the claim.

Contributions are welcome at every level. These include the DSIC property of $\mathrm{SPA}(\Phi)$, order-statistic CDFs of product measures, Lemma B-1 and Proposition 1, the analytic facts about $\mathrm{rEq}_n$ and $\Phi^*_n$, the payment identity for DSIC mechanisms with randomized allocations, and the revenue bound of Step 2. The analytic and mechanism-design infrastructure is reusable beyond this paper.

Selected references

• J. Anunrojwong, S. R. Balseiro, O. Besbes, On the Robustness of Second-Price Auctions in Prior-Independent Mechanism Design, arXiv:2204.10478v5, 2024; Operations Research, 2025. https://arxiv.org/abs/2204.10478
• D. Bergemann, K. Schlag, Pricing without Priors, Journal of the European Economic Association 6(2–3), 2008. https://doi.org/10.1162/JEEA.2008.6.2-3.560
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58

Motivation

Social media influencers earn money by endorsing products to their followers. An influencer who endorses only products that fit her organic content keeps her audience; one who accepts every sponsorship offer earns more per follower today but loses part of her audience and grows more slowly. Practitioners describe this as the choice between growing and monetizing, and the marketing literature documents both sides of it: followers unsubscribe after poorly fitting sponsored posts (Cheng and Zhang 2022), and small influencers have deeper engagement than large ones (Bentley et al., J. Global Marketing 34(3), 2021, cited in the paper).

Nistor, Selove and Villas-Boas (Management Science, Articles in Advance 2024) turn this trade-off into a deterministic continuous-time control problem. Awareness of the influencer spreads by word of mouth as in the Bass (1969) diffusion model, and the influencer's authenticity is the control. The paper's first main result, Proposition 1, characterizes the optimal policy completely: depending on two explicit conditions, the influencer is always authentic, always inauthentic, or authentic until her awareness reaches a threshold and inauthentic forever after. This mission formalizes Proposition 1 and the lemmas of §3.3 that lead to it.

Setting

Time is $t\in[0,\infty)$ and the mass of potential followers is one. The influencer's awareness $A_t\in[0,1]$ is the fraction of potential followers who know her, starting from $0<A_0<1$. At each time she is authentic or inauthentic. Following Table 1 of the paper, with parameters $0<\gamma<1$ and $\varphi>1$ (the reduced-form parameters of §3.1, which aggregate the offer arrival rate, the share of good-fit offers and the followers' tolerance of bad-fit posts):

• an authentic influencer has $F_t=A_t$ followers and instantaneous profit $\pi_t=A_t$;
• an inauthentic influencer has $F_t=\gamma A_t$ followers and instantaneous profit $\pi_t=\gamma\varphi A_t$.

Awareness grows according to the equation of motion (1),

$$\frac{dA_t}{dt}=\beta F_t(1-A_t),\qquad\beta>0,$$

so it grows at rate $\beta A_t(1-A_t)$ when she is authentic and $\gamma\beta A_t(1-A_t)$ when she is inauthentic. With discount rate $r>0$ the influencer maximizes the discounted profit (2),

$$V_t=\int_t^\infty e^{-r(u-t)}\pi_u\,du ,$$

and $V(A)$ is the value of starting at awareness $A$ and following the optimal policy.

Two closed-form objects enter the main result. The value of always being inauthentic from awareness $A$ is (Lemma 3)

$$\underline V(A)=\int_0^\infty \frac{e^{-rs}\gamma\varphi}{1+\frac{1-A}{A}e^{-\gamma\beta s}}\,ds ,$$

and its derivative is (3)

$$m(A)=\frac{d\underline V(A)}{dA}=\int_0^\infty \frac{e^{-(\gamma\beta+r)s}\gamma\varphi}{\big[A+(1-A)e^{-\gamma\beta s}\big]^2}\,ds .$$

Condition 1 (with footnote 4) holds if $\gamma\beta\ge r$ or $\big[\frac{\beta-\gamma\beta}{r-\gamma\beta}\big]\gamma\varphi>\gamma\varphi-1$.

Formalization targets

Goal: Proposition 1

For $0<\gamma<1$, $\varphi>1$, $\beta>0$, $r>0$:

1. if $\gamma\varphi\le1$, always being authentic is optimal from every $A_0\in(0,1)$;
2. if $\gamma\varphi>1$ and Condition 1 fails, always being inauthentic is optimal from every $A_0\in(0,1)$;
3. if $\gamma\varphi>1$ and Condition 1 holds, there is $A^*\in(0,1)$ with

$$m(A^*)=\frac{\gamma\varphi-1}{(1-\gamma)\beta(1-A^*)},$$

and for all sufficiently small $A_0$ the policy "authentic while $A_t<A^*$, inauthentic once $A_t\ge A^*$" is optimal.

Milestones

In the paper's order: Lemma 1 (corrected) bounds the growth of $V$ above awareness $\tfrac12$; Lemma 2 (corrected) shows that permanent inauthenticity is optimal at large awareness; Lemma 3 gives $\underline V$ in closed form; (3) identifies $m$ as its derivative; (4) computes the limit of $m$ at zero awareness,

$$\lim_{A\to0^+}m(A)=\frac{\gamma\varphi}{r-\gamma\beta}\ \ (\gamma\beta<r),\qquad m(A)\to+\infty\ \ (\gamma\beta\ge r),$$

which is where Condition 1 comes from.

Significance

Proposition 1 is the benchmark of the paper: each of the six model extensions of §4 (celebrities, follower turnover, partial authenticity, viral content, two segments, commitment) is read against it. Its third clause explains an observed pattern in influencer marketing, that small influencers post fitting content and large ones accept most sponsorships, as an optimal policy rather than a change in preferences, and Condition 1 makes explicit when growth potential outweighs current profits; the paper notes it always holds when $\beta>r$. The numerical example of §3.5 (Table 2) places the switch at about 73% awareness.

The proofs are in an online appendix and have not been machine-checked. Formalizing them requires an optimality argument against every measurable switching pattern, not only threshold policies. The mission also records two corrections: Lemma 1 and Lemma 2 are false as printed when $\gamma\varphi>1$ (explicit counterexamples are in the milestone statements), and they are stated here with the constant $\gamma\varphi/r$ that the paper's own argument gives.

Difficulty

The natural argument compares, at each instant, the extra profit from inauthenticity, $(\gamma\varphi-1)A_t$, with the value of the extra growth from authenticity, $(1-\gamma)\beta A_t(1-A_t)V'(A_t)$. This requires knowing the value function $V$, its differentiability, and the Bellman equation it satisfies, none of which is given; replacing $V$ by $\underline V$ is only justified along the part of the trajectory after the switch. The comparison must also hold against every measurable switching pattern, under which awareness solves (1) only almost everywhere. Clause 3 additionally needs the threshold equation to have a single crossing and the optimal trajectory to cross it exactly once. Optimality of a constant policy cannot be read off from instantaneous profits alone when $\gamma\varphi>1$: the instantaneously better choice (inauthenticity) can be the wrong one for a small influencer.

Formalization scope

• Policies are measurable sets $S\subseteq\mathbb R$ of times at which the influencer is inauthentic; constant policies are $\emptyset$ and $\mathbb R$.
• Admissible paths are continuous on $[0,\infty)$, start at $A_0$, take values in $[0,1]$, and solve (1) in integral (Carathéodory) form, because a measurable control makes $dA/dt$ exist only almost everywhere. The $[0,1]$ clause is implied by the equation and makes every profit stream bounded.
• Discounted profit is (2) at $t=0$, an integral over $(0,\infty)$; the paper's shift $s=u-t$ is notation. The value function $V$ of Lemma 1 is the real supremum over admissible pairs, nonempty and bounded above by $\gamma\varphi/r$ at every $A_0\in[0,1]$.
• Optimality is against every admissible pair from the same $A_0$, and every goal clause produces the optimal pair existentially. The threshold policy is the set $\{t\ge0: A_t\ge A^*\}$ of the same path it drives; a free switching time would not express a feedback rule.
• Standing assumptions. $0<\gamma<1$, $\varphi>1$, $\beta>0$, $0<A_0<1$ (§3.1–3.2); $r>0$ is the reading of "discount rate"; $\gamma\varphi>1$ is assumed in every milestone ("for the remainder of the paper", p. 5) but not in the goal, whose first clause is $\gamma\varphi\le1$. Condition 1 is the disjunction of footnote 4. Lemma 1 and Lemma 2 carry the corrected constant $\gamma\varphi/r$.

A trivializing formalization is ruled out: optimality is never assumed, the competitor class contains the constant policies' logistic paths, the threshold $A^*$ must solve the equation of (3) inside $(0,1)$, and measurability of policies keeps every profit integral meaningful. The microfoundations of §3.1 ($\mu$, $\theta$, $\omega$, $\hat U$, $c$) do not enter any statement.

The development needs Carathéodory solutions of a scalar ODE with a measurable switching coefficient, comparison and uniqueness for such solutions, differentiation under an improper integral, and a verification argument for a one-dimensional deterministic control problem with bang-bang control. The last two are reusable for other continuous-time marketing and diffusion models. Proofs of any milestone are welcome, as are proofs of the logistic closed form underlying Lemma 3.

Selected references

• C. Nistor, M. Selove, J. M. Villas-Boas, Influencer Authenticity: To Grow or to Monetize, Management Science, Articles in Advance, 2024. https://doi.org/10.1287/mnsc.2023.03479
• F. M. Bass, A new product growth for model consumer durables, Management Science 15(5):215–227, 1969. https://doi.org/10.1287/mnsc.15.5.215
• M. Cheng, S. Zhang, Reputation burning: Analyzing the impact of brand sponsorship on social influencers, preprint, 2022. https://doi.org/10.2139/ssrn.4071188

Motivation

A portfolio manager who observes today's value $x_0$ of a covariate (a market signal, a macroeconomic indicator) wants to choose a portfolio that performs well conditionally on that observation: the relevant risk is $\mathbb E[\ell(Y,\alpha,\beta)\mid X=x_0]$ of the asset return $Y$, not its unconditional mean. With finitely many historical pairs $(\hat x_i,\hat y_i)$, the empirical conditional distribution at a new $x_0$ is usually empty or rests on one or two samples, so estimating it directly is unreliable. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451v3, Operations Research 2025) hedge it with distributionally robust optimization: they take the worst case of the conditional expectation over all joint laws of $(X,Y)$ within an optimal-transport ball around the empirical measure that still put a prescribed amount of mass on the conditioning event.

The objective is a ratio of two linear functionals of the law, so the standard strong-duality theorems for Wasserstein distributionally robust optimization (Mohajerin Esfahani and Kuhn, 2018; Blanchet and Murthy, 2019; Gao and Kleywegt, 2023) do not apply directly. This mission formalizes the paper's answer in the singular case where the conditioning event is the single point $\{x_0\}$ and the event must keep mass at least $\varepsilon>0$.

Setting

Let $\mathcal X$ (covariates) and $\mathcal Y$ (returns) be spaces with ground costs $\mathbb D_{\mathcal X}$, $\mathbb D_{\mathcal Y}$, combined into the separable cost $\mathbb D((x,y),(x',y'))=\mathbb D_{\mathcal X}(x,x')+\mathbb D_{\mathcal Y}(y,y')$. The data are $N$ samples $(\hat x_i,\hat y_i)$, $i\in[N]$, with empirical measure $\hat{\mathbb P}=N^{-1}\sum_i\delta_{(\hat x_i,\hat y_i)}$.

• The optimal transport cost between laws $\mathbb Q_1,\mathbb Q_2$ is $\mathbb W(\mathbb Q_1,\mathbb Q_2)=\inf\{\mathbb E_\pi[\mathbb D(\xi_1,\xi_2)]:\pi\in\Pi(\mathbb Q_1,\mathbb Q_2)\}$, the infimum over couplings.
• The ambiguity set is $\mathbb B_\rho=\{\mathbb Q:\ \mathbb W(\mathbb Q,\hat{\mathbb P})\le\rho\}$ for a radius $\rho\ge0$.
• The fiber of radius $\gamma$ is $\mathcal N_\gamma(x_0)\times\mathcal Y$ with $\mathcal N_\gamma(x_0)=\{x:\mathbb D_{\mathcal X}(x,x_0)\le\gamma\}$; here $\gamma=0$, so the fiber is $\{x_0\}\times\mathcal Y$.
• The minimum radius $\rho_{\min}(x_0,\gamma,\varepsilon)=\inf\{\mathbb W(\mathbb Q,\hat{\mathbb P}):\mathbb Q(X\in\mathcal N_\gamma(x_0))\ge\varepsilon\}$ is the smallest radius at which some law in the ball meets the mass requirement.
• Assumption 2.4 of the paper: the costs are symmetric, non-negative and continuous, $\mathbb D$ vanishes exactly on the diagonal, each $\hat x_i$ has a unique projection onto $\mathcal N_\gamma(x_0)$ with cost $\kappa_i$, and boundary points of $\mathcal N_\gamma(x_0)$ can be left at arbitrarily small cost.

For a loss $\ell(y)=\ell(y,\alpha,\beta)$ at a fixed decision, the object of study is the worst-case conditional expected loss

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X=x_0)\ge\varepsilon}\ \mathbb E_{\mathbb Q}[\ell(Y)\mid X=x_0],\qquad \mathbb E_{\mathbb Q}[\ell(Y)\mid X=x_0]=\frac{\mathbb E_{\mathbb Q}[\ell(Y)\mathbb 1_{\{x_0\}}(X)]}{\mathbb Q(X=x_0)} .$$

Formalization targets

Goal: Theorem 3.2 (p. 15)

For $\varepsilon\in(0,1]$ and $\rho>\rho_{\min}(x_0,0,\varepsilon)$,

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X=x_0)\ge\varepsilon}\mathbb E_{\mathbb Q}[\ell(Y)\mid X=x_0] =\inf_{\lambda_1\ge0,\ \lambda_2\in\mathbb R}\Big\{\rho\lambda_1+\varepsilon\lambda_2+\frac1N\sum_{i\in[N]}\Big(\sup_{y\in\mathcal Y}\big\{\varepsilon^{-1}\ell(y)-[\mathbb D_{\mathcal X}(x_0,\hat x_i)+\mathbb D_{\mathcal Y}(y,\hat y_i)]\lambda_1-\lambda_2\big\}\Big)^+\Big\}.$$

The loss is arbitrary (measurable, real-valued), and both sides may be $+\infty$.

Milestones

1. Representation (24) (p. 47): $\mathbb Q\in\mathbb B_\rho$ iff $\mathbb Q=N^{-1}\sum_i\pi_i$ for probability measures $\pi_i$ with $N^{-1}\sum_i\mathbb E_{\pi_i}[\mathbb D(\cdot,(\hat x_i,\hat y_i))]\le\rho$.
2. Proposition 2.5 (p. 11): $\rho_{\min}$ is the value of the fractional knapsack program $\min\{N^{-1}\sum_i\kappa_i\upsilon_i:\upsilon\in[0,1]^N,\sum_i\upsilon_i\ge N\varepsilon\}$, and the problem is feasible iff $\rho\ge\rho_{\min}$.
3. Lemma A.4 (p. 36): in a linear-fractional program over $[0,1]^N$, the constraint $\sum_i\upsilon_i\ge\varepsilon N$ may be replaced by $\sum_i\upsilon_i=\varepsilon N$.
4. Proposition A.5 (p. 36): the worst case equals a supremum over weights $\upsilon$ with $\sum_i\upsilon_i=N\varepsilon$ and over laws $\mu_0^i$ on $\mathcal Y$ of the linear objective $(N\varepsilon)^{-1}\sum_i\upsilon_i\mathbb E_{\mu_0^i}[\ell]$ under one transport budget.
5. Inner duality (p. 41): for fixed strictly feasible weights, the inner supremum over $(\mu_0^i)$ equals its moment-problem dual over $\lambda_1\ge0$ and $\theta\in\mathbb R^N$.

Significance

Theorem 3.2 reduces an infinite-dimensional, fractional worst-case problem to a two-multiplier convex program whose only infinite-dimensional pieces are $N$ suprema over $\mathcal Y$. For piecewise-linear losses and norm costs the paper turns this into the conic programs of Propositions 3.3–3.4, which are what make the robust conditional portfolio model solvable in practice. It also compares the formulation with the trimming approach of Esteban-Pérez and Morales (Mathematical Programming, 2022), whose adversary may only pick laws with fiber mass exactly $\varepsilon$; Proposition A.5 shows that, at $\gamma=0$, the more powerful adversary allowed $\mathbb Q(X=x_0)\ge\varepsilon$ attains the same value.

The result is proved in the paper; nothing here is open mathematics. None of it is formalized. A complete development would add to the platform a first conditional (fractional) distributionally robust duality, a decomposition of optimal-transport balls around empirical measures (milestone 1, reusable by every finite-sample Wasserstein result), and a moment-problem duality with one budget constraint (milestone 5).

Difficulty

The ratio objective is the obstacle: neither the numerator nor the denominator alone determines the worst case, and a law that is optimal for the numerator may violate the mass constraint. The step "fix the fiber mass at $\varepsilon$" (Proposition A.5) is where the obvious argument fails: an optimal law may put more than $\varepsilon$ on $\{x_0\}$, and reducing that mass requires moving sample points off $x_0$ at vanishing transport cost, which needs points of $\mathcal X$ arbitrarily close to $x_0$. Milestone 1 needs the existence of optimal couplings, which Mathlib lacks. Milestone 5 is an infinite-dimensional Lagrangian duality whose Slater point degenerates on the boundary of the weight set, so the final interchange of supremum and infimum must avoid that boundary.

Formalization scope

$\mathcal X$ and $\mathcal Y$ are Polish spaces with their Borel σ-algebras; samples are indexed by Fin N with $N\ge1$, repeats allowed. The optimal transport cost is the published RWPI.SqrtLasso.transportCost (an infimum of lower integrals of the $[0,\infty]$-valued cost; attainment is not built in), and every expectation of the loss is the published ModelRiskOT.Duality.extIntegral, $\int\ell^+-\int\ell^-$ in $[-\infty,\infty]$. Worst-case values and duals are EReal suprema and infima. The loss is a measurable L : Y → ℝ standing for $\ell(\cdot,\alpha,\beta)$ at an arbitrary decision.

Hypotheses beyond the page, all disclosed in the statements:

• Assumption 2.4 is a hypothesis of every statement, as the paper makes it "throughout".
• NotIsolated: for every $r>0$ there is $x\ne x_0$ with $\mathbb D_{\mathcal X}(x,x_0)\le r$. This is Assumption 2.4(iii) at $\gamma=0$ read with the ambient boundary of $\{x_0\}$, as the paper's remark on p. 11 does; with the topological frontier in $\mathcal X$, (iii) is vacuous at an isolated $x_0$, and Theorem 3.2 is then false.
• Measurability of the loss, used because the dual side integrates $\ell$ against arbitrary laws on $\mathcal Y$.
• Milestone 5 requires the strict budget inequality $\sum_i\upsilon_i\mathbb D_{\mathcal X}(x_0,\hat x_i)<N\rho$; the page's Slater argument covers only that case.

Trivializing formalizations are ruled out: conditional expectations are only taken at laws with fiber mass at least $\varepsilon>0$ (never at mass $0$, where a real division would return $0$); expectations are never Bochner integrals, which would be $0$ for a non-integrable loss; the radius enters through ENNReal.ofReal ρ only where $\rho\ge0$ or $\rho>\rho_{\min}$ forces $\rho>0$; and every supremum ranges over exactly the paper's feasible set.

Needed infrastructure: existence of optimal couplings on Polish spaces (Villani, Theorem 4.1), a Lagrangian duality for moment problems, and Mathlib's Sion minimax theorem for the interchange. Contributions to any of these, and proofs of the milestones in any order, 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, 2024. https://arxiv.org/abs/2103.16451
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44, 2019. https://doi.org/10.1287/moor.2018.0936
• R. Gao, A. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, Mathematics of Operations Research 48, 2023. https://doi.org/10.1287/moor.2022.1275
• A. Esteban-Pérez, J. M. Morales, Distributionally robust stochastic programs with side information based on trimmings, Mathematical Programming, 2022.
• A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, Kluwer, 2001, pp. 135–165.
• M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8, 1958, pp. 171–176.
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9