Operations Research

Motivation

Online retailers, search engines and streaming services show products on a sequence of pages, and most consumers look at only the first few. Which products are seen therefore depends on where they are placed. Gallego, Li, Truong and Wang (Operations Research, 2020) call the problem of placing products on pages to maximize expected revenue product framing. They show that it is NP-hard even with two pages and the multinomial logit model, and they give simple algorithms with constant-factor guarantees.

This mission concerns their second guarantee. In their basic model every consumer chooses with the same choice model, whatever the number of pages she views. In practice the number of pages viewed is itself informative: consumers who browse many pages may be keener buyers. Section 6 of the paper lets the choice model depend on the number of pages viewed and proposes the TRUNC algorithm for this setting. The guarantee is that TRUNC earns at least one third of the optimal expected revenue.

Setting

There are $n$ products with revenues $r_i\ge 0$ and $m$ virtual pages, each holding at most $p$ products; write $[k]=\{1,\dots,k\}$. A framing places each product on at most one page, with at most $p$ products per page. A consumer views a random number $X\in[m]$ of pages, with law $\lambda(x)=\mathbb P[X=x]$, tail $\Lambda(x)=\mathbb P[X\ge x]$ and failure rate $h(x)=\lambda(x)/\Lambda(x)$. Her consideration set is the set of products on pages $1,\dots,X$.

A consumer who views $x$ pages is of type $x$ and buys product $i$ from consideration set $S$ with probability $P_x(i,S)$, where $P_x(i,S)\ge 0$, $P_x(i,S)=0$ for $i\notin S$, and $\sum_{i\in S}P_x(i,S)\le 1$. The revenue of $S$ for type $x$ and the best capacitated revenue are

$$R_x(S)=\sum_{i\in S}r_iP_x(i,S),\qquad U(x)=\max_{S\subseteq[n],\ |S|\le xp}R_x(S).$$

A framing $f$ earns $\sum_{x\in[m]}\lambda(x)R_x(C_f(x))$, where $C_f(x)$ is the set of products on pages $1,\dots,x$. Its maximum over all framings is $V^{OPT}$. The assumptions are:

• B1: $R_x(S)\le R_y(S)$ whenever $x\le y$ and $|S|\le xp$;
• B2: $U(x)/x$ is nonincreasing in $x$;
• B3: problem (9) defining $U$ can be solved, here exactly;
• B4: $X$ has an increasing failure rate (IFR), i.e. $h$ is nondecreasing (Shaked and Shanthikumar 2007).

TRUNC($y$), for $y\in[m]$, picks an optimal assortment $S(y)$ for $U(y)$ and places it, in any arrangement, on pages $1,\dots,y$, leaving the remaining pages blank. TRUNC takes the best of these $m$ framings; its revenue is $V^{TRUNC}$.

The analysis passes through the bound-revealing program (10): minimize $\max_{x\in[m]}U(x)\Lambda(x)$ over nondecreasing $U\ge 0$ with $U(x)/x$ nonincreasing and over tails $1=\Lambda(1)\ge\cdots\ge\Lambda(m)\ge 0$ with $\Lambda(x+1)\Lambda(x-1)\le\Lambda(x)^2$, subject to $\sum_x\lambda(x)U(x)=1$.

Formalization targets

Goal: Theorem 4

Under Assumptions B1–B4, for every choice of optimal assortments and every arrangement on the pages,

$$V^{TRUNC}\;\ge\;\frac13\,V^{OPT}.$$

Milestones

In the order the proof uses them:

1. Upper bound (§6, p. 13): $V^{OPT}\le\mathbf E[U(X)]=\sum_x\lambda(x)U(x)$.
2. Lower bound (§6.1, p. 14): every run of TRUNC($y$) earns at least $U(y)\Lambda(y)$.
3. Lemma 8: for an IFR tail with $\Lambda>0$, $g(x)=x\Lambda(x)$ is weakly unimodal, and its largest maximizer is $\min\{x: h(x)>1/(x+1)\}$.
4. Proposition 5, Lemma 9, Proposition 6, Proposition 7: the structure of every optimal solution of (10) with $\Lambda>0$. With $y$ the largest maximizer of $U(x)\Lambda(x)$:
   • $U(x)/x$ is constant for $x\ge y$;
   • $y$ also maximizes $x\Lambda(x)$;
   • $U(x)\Lambda(x)$ is constant for $x\le y$;
   • $h$ is constant on $[y,m-1]$.
5. Value of (10) (A.4, p. 42): every feasible point of (10) has $\max_xU(x)\Lambda(x)\ge 1/3$.

Significance

The theorem shows that framing under type-dependent choice admits a constant-factor approximation using only $m$ calls to an assortment oracle, although the framing problem itself is NP-hard. The constant does not depend on the number of products, pages or page capacity. The bound-revealing program (10) is a self-contained extremal problem about log-concave tails and is reusable wherever a revenue curve with decreasing average returns meets an IFR horizon. The numerical value of (10) decreases with $m$ ($2/3$ at $m=2$, about $0.36$ at $m=40$), so the constant $1/3$ is approached only as the number of pages grows.

The result is proved in the paper. No part of it has a machine-checked proof: the platform has no item on product framing, discrete failure rates or program (10). A complete development would give a machine-checked proof of the approximation ratio. It would also give a checked treatment of the perturbation arguments of Appendix A.4, which the paper presents briefly.

Difficulty

Two steps are elementary: the upper bound (a consumer of type $x$ never sees more than $xp$ products) and the lower bound (every consumer of type $x\ge y$ sees all of $S(y)$).

The difficulty lies in the extremal problem (10). It is not convex: the IFR constraint is a log-concavity condition, and the objective is a maximum of products $U(x)\Lambda(x)$. A direct bound such as $\max_xU(x)\Lambda(x)\ge\sum_x\lambda(x)U(x)/m$ gives a constant that decays with $m$. The uniform constant comes from showing that the extremal tail is geometric beyond the maximizing page and that the extremal $U$ is pinned down on both sides of it. The paper reaches this structure through optimality conditions, so a formal proof must also establish that (10) attains its minimum, or must avoid that step.

Formalization scope

Products are Fin n. Pages are the natural numbers $1,\dots,m$, as in the paper, with $m\ge 1$ and $p\ge 1$. A framing is f : Fin n → ℕ: product $i$ is on page f i when $1\le f(i)\le m$, and f i = 0 means it is not displayed. The law $\lambda$ and the functions of (10) are functions on $\mathbb N$ of which only the values on $[m]$ are used, and $\Lambda(m+1)=0$.

$V^{OPT}$ and $U$ are maxima over finite nonempty families, and $V^{TRUNC}$ is a Finset.sup' over $y\in[m]$. TRUNC is a predicate on its outputs, not a function, and the goal is quantified over every family of runs. Assumption B3 is used with $\epsilon=0$, as everywhere in the paper. IFR is required only where the failure rate is defined ($\Lambda>0$), so laws whose support ends before page $m$ are allowed. Nonnegative revenues $r_i\ge 0$ are assumed; the lower bound of milestone 2 needs them.

No trivializing reading. The goal is not stated for one particular filling heuristic, or for some run only, and $V^{TRUNC}$ is the revenue of the framings themselves, not the lower bound $U(y)\Lambda(y)$.

Page numbers refer to the authors' accepted manuscript of the Operations Research article, which differ from the journal typesetting. The development needs only Mathlib (finite sums and maxima over Finset). Program (10) and Lemma 8 are independent of the framing model. Contributions are welcome at every milestone: Lemma 8 and the bound for (10) are the most self-contained.

Selected references

• G. Gallego, A. Li, V.-A. Truong, X. Wang, Approximation Algorithms for Product Framing and Pricing, Operations Research, 2020. https://doi.org/10.1287/opre.2019.1875
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

A chance-constrained program chooses a decision $x$ so that a random vector $\xi$ falls outside a decision-dependent safety set $\mathcal S(x)$ with probability at most $\epsilon$. Chance constraints are a standard model for reliability requirements in power systems, supply chains and transportation, where a plan must survive random demand or supply with high probability. In practice the distribution of $\xi$ is known only through samples $\xi_1, \dots, \xi_N$, and the sample average approximation (SAA) that replaces it by the empirical distribution $\mathbb P_N$ is sensitive to the particular sample.

Distributionally robust chance constraints regularize SAA by requiring the probability bound for every distribution within Wasserstein distance $\theta$ of $\mathbb P_N$. Chen, Kuhn and Wiesemann (arXiv:1809.00210) and Xie (doi:10.1007/s10107-019-01445-5) showed that, for safety sets defined by linear inequalities, the resulting program (DR-CCP) is a mixed-integer linear program with a big-M constant. These big-M formulations are hard for solvers to close when $\theta$ is small. Ho-Nguyen, Kılınç-Karzan, Küçükyavuz and Lee (doi:10.1007/s10107-020-01605-y) connect the formulation to the mixing sets of SAA and to robust 0–1 programming, and derive a smaller and tighter formulation that is still exact.

Setting

The random vector lives in $\mathbb R^K$ with an arbitrary norm $\|\cdot\|$; in the formalization it is a finite-dimensional real normed space $E$. The dual norm of a linear functional $b$ is $\|b\|_* = \sup_{\|\xi\| \le 1} b^\top \xi$. The decision $x$ ranges over a set $\mathcal X \subseteq \mathbb R^L$.

The 1-Wasserstein distance between distributions $\mathbb P, \mathbb P'$ is the infimum of $\mathbb E\|\xi - \xi'\|$ over couplings of $\mathbb P$ and $\mathbb P'$. The ambiguity set $\mathcal F_N(\theta)$ is the set of distributions within distance $\theta$ of $\mathbb P_N = \frac1N \sum_{i} \delta_{\xi_i}$. The feasible region of (DR-CCP) is

$$\mathcal X_{\mathrm{DR}}(\mathcal S) = \Big\{x \in \mathcal X : \sup_{\mathbb P \in \mathcal F_N(\theta)} \mathbb P[\xi \notin \mathcal S(x)] \le \epsilon\Big\}.$$

Throughout, $\epsilon \in (0,1)$ and $\theta > 0$ are fixed.

The paper studies joint chance constraints with right-hand side uncertainty: for $p \in [P]$ there are $a_p \in \mathbb R^L$, $b_p$ and $d_p \in \mathbb R$, and

$$\mathcal S(x) = \{\xi : b_p^\top \xi + d_p - a_p^\top x > 0,\ p \in [P]\}.$$

Write $g_{i,p}(x) = (b_p^\top\xi_i + d_p - a_p^\top x)/\|b_p\|_*$ and $k = \lfloor \epsilon N \rfloor$. Let $q_p$ be the $(k+1)$-th largest value among $\{-b_p^\top\xi_i\}_{i\in[N]}$, and let $[N]_p = \{i : -b_p^\top \xi_i > q_p\}$.

The big-M formulation (5) of Chen et al. uses binaries $z \in \{0,1\}^N$, slacks $r \ge 0$ and a scalar $t \ge 0$ with

$$\epsilon t \ge \theta + \tfrac1N \textstyle\sum_i r_i,\qquad M(1 - z_i) \ge t - r_i,\qquad g_{i,p}(x) + M z_i \ge t - r_i.$$

The paper's improved formulation (20) keeps the first two families, adds the knapsack constraint $\sum_i z_i \le k$, replaces $M$ in the third family by $h_{i,p} = (-b_p^\top\xi_i - q_p)/\|b_p\|_*$, imposes it only for $i \in [N]_p$, and adds $(-q_p + d_p - a_p^\top x)/\|b_p\|_* \ge t$ for every $p$.

Formalization targets

Goal: Theorem 3 (p. 655)

$$\mathcal X_{\mathrm{DR}}(\mathcal S) = \{x \in \mathcal X : \exists\,(z, r, t) \text{ satisfying (20b)–(20d)}\}.$$

The goal states equality of feasible sets of $x$. Because the objective $c^\top x$ depends on $x$ alone, this is the paper's "exact reformulation".

Milestones, in attack order

1. (4b), p. 646: $\operatorname{dist}(\xi, \mathcal S(x)) = \max\{0, \min_p (b_p^\top\xi + d_p - a_p^\top x)/\|b_p\|_*\}$, where $\operatorname{dist}(\xi, \mathcal S) = \inf\{\|\xi - \xi'\| : \xi' \notin \mathcal S\}$ is (1).
2. (3), p. 645: for open $\mathcal S(x)$, $\mathcal X_{\mathrm{DR}}(\mathcal S)$ is the set of $x \in \mathcal X$ admitting $t \ge 0$, $r \ge 0$ with $\operatorname{dist}(\xi_i, \mathcal S(x)) \ge t - r_i$ and $\epsilon t \ge \theta + \frac1N\sum_i r_i$.
3. (6), p. 646: $\mathcal X_{\mathrm{DR}}(\mathcal S) = \{x \in \mathcal X : \text{(5b)–(5e)}\}$.
4. Theorem 1, p. 648: adding $\sum_i z_i \le k$ and $g_{i,p}(x) + M z_i \ge 0$ to (5) keeps it exact.
5. Theorem 2, p. 651: replacing $M$ in (5e) by $h_{i,p}$, with the knapsack constraint, keeps it exact.
6. Lemma 1, p. 653: for $x \in \mathcal X_{\mathrm{DR}}(\mathcal S)$, $t$ may be taken equal to the $(k+1)$-th smallest of the distances $\operatorname{dist}(\xi_i, \mathcal S(x))$.
7. Proposition 1, p. 654: for $x \in \mathcal X_{\mathrm{DR}}(\mathcal S)$, some solution of (17) also satisfies $(-q_p + d_p - a_p^\top x)/\|b_p\|_* - t \ge 0$ for every $p$.

Milestones 2 and 3 are results of Chen, Kuhn and Wiesemann that this paper cites and uses, not results it proves.

Significance

Theorem 3 says that the scenario-wise big-M rows of the Wasserstein chance constraint can be replaced by at most $\lfloor\epsilon N\rfloor$ rows per $p$, with coefficients computed from the data. Remark 2 of the paper counts at least $((1-\epsilon)N - 1)P$ fewer rows than (17). The reduced form exposes a robust 0–1 substructure, and the paper adapts Atamtürk's valid inequalities for it. Its computational study reports order-of-magnitude speed-ups on stochastic transportation problems.

The results are proved on paper; none is machine-checked. The formalization would give a verified chain from the Wasserstein worst-case probability to a finite mixed-integer system. Milestone (3), the dual reformulation, is reusable for any distributionally robust chance constraint over a 1-Wasserstein ball around an empirical distribution, and (4b) for any polyhedral safety set. A second formalization layer would verify the order-statistic arguments (Lemma 1, Proposition 1) used throughout the quantile-strengthening literature.

Difficulty

The deterministic parts — Theorems 1–3 given (3) and (4b) — are finite case analyses on $z_i \in \{0,1\}$, but each step relies on order statistics of the sample with ties. Lemma 1 rests on the paper's "without loss of generality, sort the distances", and a formal proof must handle ties and the floor $\lfloor\epsilon N\rfloor$ exactly. The paper's proof of Theorem 2 argues "at optimality"; for a statement about feasible sets that argument has to be replaced by an explicit choice of $z$.

The hard step is (3). It exchanges a supremum over all Borel probability measures in a Wasserstein ball for a scalar system. The naive attempt, which perturbs $\mathbb P_N$ by moving mass from the samples to the nearest unsafe points, proves only one inclusion. The other needs strong duality for worst-case probabilities over transport balls, together with attainment of the dual infimum, which uses $\theta > 0$.

Formalization scope

• The ξ-space is a type E with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] and its Borel σ-algebra. The norm is arbitrary, not the sup norm of Fin K → ℝ.
• Each $b_p$ is a continuous linear functional (StrongDual ℝ E), so $\|b_p\|_*$ is its operator norm.
• Decisions are Fin L → ℝ, with $a_p^\top x$ written a p ⬝ᵥ x. Indices are 0-based.
• The worst-case probability is the published ModelRiskOT.WorstProb.worstProb with cost $\|u - v\|$, valued in $[0,\infty]$, around the published WassersteinDRO.Duality.empiricalDistribution.
• The distance (1) is Metric.infDist.
• Binaries are reals with $z_i \in \{0,1\}$.
• Order statistics sort the multiset of values, so ties count with multiplicity.

Standing assumptions and pins in every statement:

• $N \ge 1$, $\epsilon \in (0,1)$ and $\theta > 0$ (p. 645);
• $P \ge 1$ and $b_p \neq 0$, which (4) needs;
• for every statement involving $M$, one bound $|b_p^\top\xi_i + d_p - a_p^\top x|/\|b_p\|_* \le M$ over $x \in \mathcal X$ and all $i, p$. This is Remark 1's (10), taken uniform in $i$. It replaces the compactness of $\mathcal X$ assumed on p. 642, which is not assumed;
• for the general-$\mathcal S$ milestone (3), $\mathcal S(x)$ open with nonempty complement.

In (17b), the printed "(5b)–(5d) and (5c)" is read as "(5b)–(5d) and (8c)", following the proof of Theorem 2 and (20b).

Several trivializing formalizations are ruled out:

• an empty or degenerate ball: $N \ge 1$ makes $\mathbb P_N$ a probability measure inside its own ball;
• a junk distance: the unsafe set is nonempty under the pins, so infDist never sees the empty set;
• a junk order statistic: the rank $k$ is below $N$;
• a fixed norm;
• a relaxation of $z$ to $[0,1]$, which is a different theorem.

Welcome contributions:

• the 1-Wasserstein duality for indicator losses on empirical distributions;
• order-statistic lemmas for the multiset sort;
• the distance from a point to the complement of an open polyhedron in a normed space.

Selected references

• N. Ho-Nguyen, F. Kılınç-Karzan, S. Küçükyavuz, D. Lee, Distributionally robust chance-constrained programs with right-hand side uncertainty under Wasserstein ambiguity, Mathematical Programming Ser. B 196 (2022) 641–672. https://doi.org/10.1007/s10107-020-01605-y
• Z. Chen, D. Kuhn, W. Wiesemann, Data-driven chance constrained programs over Wasserstein balls, Operations Research (2024); preprint 2018. https://arxiv.org/abs/1809.00210
• W. Xie, On distributionally robust chance constrained programs with Wasserstein distance, Mathematical Programming 186 (2021) 115–155. https://doi.org/10.1007/s10107-019-01445-5
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44 (2019) 565–600. https://doi.org/10.1287/moor.2018.0936
• A. Atamtürk, Strong formulations of robust mixed 0–1 programming, Mathematical Programming 108 (2006) 235–250. https://doi.org/10.1007/s10107-006-0709-5

Why radius sensitivity matters

A distributionally robust decision evaluates a rule against every data distribution within a specified transport budget of a baseline law. The budget is a modeling choice: increasing it expresses more uncertainty about the data. A robust objective value can increase with that budget, but the value alone does not describe how the adverse distribution changes. For a fixed linear decision, Blanchet, Murthy, and Zhang identify the worst-case distribution and ask what happens to each observation as the budget increases. Their Theorem 7 gives a sample-wise answer in a small-radius regime: adverse observations move along straight lines, and their distance from the original observations grows monotonically.

This matters when a robust solution is interpreted through its adverse scenarios. The result says that two nearby ambiguity budgets do not produce unrelated worst-case data sets. They produce a coherent family of transported observations whose directions are determined by the sign of the loss derivative. The theorem is a structural property of an optimal-transport ambiguity set, beyond a bound on its optimal value. It appears in a paper that also develops dual formulas and iterative optimization schemes for the same model Blanchet, Murthy, and Zhang, 2022.

Model and notation

Let $X$ take values in $\mathbb R^d$ with baseline law $P_0$. A decision $\beta$ belongs to a convex set $B\subseteq\mathbb R^d$ and incurs loss $\ell(\beta^\top X)$. At each source point $x$, a positive-definite matrix $A(x)$ defines the transport cost

$$c(x,x')=(x-x')^\top A(x)(x-x').$$

The matrix may depend on $x$, so movement can be cheaper in different directions and at different observations. The model requires lower semicontinuity of $c$ and almost-sure lower and upper spectral bounds for $A(x)$. A distribution $P$ is within the ambiguity ball of radius $\delta>0$ when it can be coupled with $P_0$ at expected cost at most $\delta$. The worst-case objective is the supremum of $E_P[\ell(\beta^\top X)]$ over that ball. In Lean, the equivalent coupling formulation records a joint law $\pi$ with first marginal $P_0$, second marginal $P$, and cost at most $\delta$.

The paper reduces the worst-case calculation to a dual objective $f_\delta(\beta,\lambda)$, where $\lambda\ge0$ prices the transport budget. Its pointwise term $\ell_{\rm rob}(\beta,\lambda;x)$ is the supremum over a scalar $\gamma$ of the function $F(\gamma,\beta,\lambda;x)$ in display (7). The set of maximizing scalars is $\Gamma^*(\beta,\lambda;x)$. A scalar maximizer $G_\delta(x)$ produces a transported observation

$$X^*_\delta=x+\sqrt\delta\,G_\delta(x)A(x)^{-1}\beta.$$

Assumptions 2–4 require a convex loss with controlled growth, a fourth moment of $P_0$, bounded second derivatives of the loss, a nondegenerate loss derivative, and compactness of $B$. The statement here also uses Assumption 5, local strong convexity with a positive-probability nondegeneracy condition. The paper’s proof of Theorem 7 uses that condition through its small-radius strong-convexity result Theorems 4 and 7.

Formalization targets

For each fixed $\beta\in B\setminus\{0\}$, the goal asserts that there is a common threshold $\delta_1>0$ and a family $G_\delta$ such that the law of $X^*_\delta$ is the unique worst-case distribution for every $0<\delta<\delta_1$. For any pair $0<\delta<\delta'<\delta_1$, it asserts, $P_0$-almost surely,

$$\begin{aligned} 0&<\sqrt\delta\,G_\delta<\sqrt{\delta'}\,G_{\delta'} &&\text{if }\ell'(\beta^\top X)>0,\\ \sqrt{\delta'}\,G_{\delta'}&<\sqrt\delta\,G_\delta<0 &&\text{if }\ell'(\beta^\top X)<0,\\ G_\delta&=0 &&\text{if }\ell'(\beta^\top X)=0. \end{aligned}$$

Consequently,

$$\|X^*_\delta-X\|\le\|X^*_{\delta'}-X\|.$$

The goal keeps the uniqueness and primal attainment clauses together with these comparisons. The milestones follow the paper’s prerequisites: the optimizer and curvature bounds of Proposition 9, the unique worst-case law of Theorem 6(e), uniqueness of the dual minimizer at small radius, and the sign of the pointwise maximizer. Each has its own statement so solvers can use it elsewhere.

What the result establishes

The theorem gives a consistent interpretation of changes in the ambiguity radius. If the loss increases locally in the decision direction, an adverse observation moves farther in that direction; if the loss decreases, it moves farther in the opposite direction; at a stationary score it stays put. The corresponding displacement norm is monotone for each radius pair, almost surely. This is stronger than monotonicity of the worst-case objective value: it describes the geometry of a family of optimizers, not only their values.

The paper proves the result in §5.4. The work of this mission is to formalize its hypotheses, optimality claims, and sample-wise inequalities in Lean. The published ModelRiskOT.Duality coupling definitions already give a reusable primal interface; this mission adds the state-dependent quadratic cost, the scalar dual model, its small-radius regions, and the comparative-statics statements. The proof obligations remain open in this draft. Their formalization would also make the dual optimizer bounds and the deterministic transport representation reusable in later optimal-transport DRO developments.

Where the mathematical difficulty sits

The worst-case value being monotone in $\delta$ does not force a particular worst-case distribution, or each observation in one, to move monotonically. The theorem needs a unique worst-case law and a coherent choice of pointwise maximizers as $\delta$ varies. The scalar maximizer depends on both the radius and the dual price, while the optimal dual price itself changes with the radius. The paper’s small-radius conditions keep this joint variation controlled. Without uniqueness, two optimal laws could differ even at the same radius, and a sample-wise comparison would have no fixed object to compare.

The result also involves several layers of almost-sure reasoning. Spectral bounds on $A(x)$ hold only outside a null set; the relevant maximizer and its transported law must be measurable enough to define pushforwards and expectations. These conditions must be carried through the theorem without silently replacing an almost-sure claim by a pointwise one.

Formalization scope

Vectors use EuclideanSpace ℝ (Fin d), and the baseline is a Borel probability measure. The decision set is convex and compact and is explicitly nonempty. Assumption 1 gives positive definiteness of $A(x)$ everywhere, lower semicontinuity of the cost, and almost-sure uniform spectral bounds. The loss satisfies Assumptions 2–5. The fourth moment in Assumption 2 and the bounds on $\ell''$ control the integrals used by the dual theory. A positive ambiguity radius is required whenever its square root appears.

The dual terms $\ell_{\rm rob}$ and $f_\delta$ use extended-real values, since the pointwise supremum can be infinite. The worst-case value is a supremum over feasible couplings, with signed loss integrated using the published extended-real integral. A graph coupling witnesses attainment, and every optimal coupling must have the same second marginal. This ties the family $G_\delta$ to the actual worst-case distribution rather than an arbitrary monotone scalar field. Almost-everywhere measurability of $G_\delta$ and the transport map is part of the conclusion.

The radius $\delta$ varies inside the goal. The threshold $\delta_1$ is chosen before any radius pair, and the comparisons are stated almost surely for each pair. The paper prints Theorem 7 under Assumptions 1–4 while referring to $\delta_1$ and invoking Theorem 4, which uses Assumption 5; this mission includes Assumption 5 explicitly. It also reads the singleton clause of Theorem 6(e) almost surely, because its threshold is an essential supremum, and uses a non-strict lower curvature bound in Proposition 9(b), as its proof permits. Contributions on the small-radius dual theory, measurable maximizers, primal attainment, and the radius comparisons are all within scope.

Selected references

• J. Blanchet, K. Murthy, and F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Mathematics of Operations Research 47(2), 2022. arXiv:1810.02403v3.
• J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2), 2019. arXiv:1604.01446v2.

Motivation

A buyer can reduce production cost by using a supplier whose operations carry a risk of a responsibility violation. That choice can also bring a direct penalty and cause customers to leave. Guo, Lee, and Swinney study how the cost saving, consumer demand, and violation risk jointly determine the buyer’s sourcing decision in a transparent supply chain. Their model distinguishes customers who value responsible production from those who do not, making it possible to ask when the buyer uses a responsible supplier, a risky supplier, or both. The question concerns supplier selection when the buyer knows each supplier’s responsibility type and customers can react to a violation. Guo, Lee, and Swinney (2016) give the model and its four strategy regions.

Setting

A single buyer sells to a market whose total size is normalized to one. A responsible supplier has marginal cost $c_R$ and no responsibility violation in the model. A risky supplier has lower marginal cost $c_{NR}<c_R$ and a violation occurs with probability $\phi\in[0,1]$. Write $\Delta=c_R-c_{NR}$ for the responsible supplier’s cost premium. A violation costs the buyer a fixed amount $c_{VP}$.

Every consumer has baseline willingness to pay $v$. A fraction $\theta\in[0,1]$ is socially conscious and has additional willingness to pay $r$ for a responsibly sourced product. Upon a violation, a fraction $\alpha\in[0,1]$ of this group exits the market. The remaining fraction $1-\theta$ has no responsible-sourcing premium and does not exit for that reason. These symbols and ranges follow the paper’s Section 3; the theorem adds no sign restriction to $v$, $r$, or $c_{VP}$.

The buyer chooses among four sourcing strategies. Low-cost sourcing (LC) uses the risky supplier for the whole market. Dual sourcing (DS) serves socially conscious consumers with responsible units and other consumers with risky units. Responsible niche sourcing (RN) serves only socially conscious consumers with responsible units. Responsible mass market sourcing (RM) serves everyone with responsible units. With $\Pi^s$ denoting strategy $s$’s expected profit, Table 2 gives

$$\begin{aligned} \Pi^{LC}&=(1-\alpha\phi)\theta(v-c_{NR})+(1-\theta)(v-c_{NR})-\phi c_{VP},\\ \Pi^{DS}&=(1-\alpha\phi)\theta(v+r-c_R)+(1-\theta)(v-c_{NR})-\phi c_{VP},\\ \Pi^{RN}&=\theta(v+r-c_R),\\ \Pi^{RM}&=v-c_R. \end{aligned}$$

A strategy is optimal when its profit is at least the profit of each of the four strategies. This definition allows ties. In the statements below, $[x]^+=\max(x,0)$, as defined immediately before Proposition 1. Section 4 and Table 2 are the sources for these formulas.

Formalization targets

Proposition 1: sufficient conditions for each strategy

The goal is all four clauses of Proposition 1, p. 2729, as printed. For LC, the sufficient conditions are

$$r<\Delta,\qquad \phi[\alpha\theta(v-c_{NR})+c_{VP}]<\Delta-[\theta r-(1-\theta)(v-c_R)]^+.$$

For DS, they are

$$r>\Delta,\qquad \phi[\alpha\theta(v+r-c_{NR})+c_{VP}]<\Delta(1-\theta)+\theta r-[\theta r-(1-\theta)(v-c_R)]^+.$$

For RN, the threshold is $r>(v-c_R)(1-\theta)/\theta$; for RM it is $r<(v-c_R)(1-\theta)/\theta$. Each of these last two clauses also requires that neither LC nor DS be optimal. They are stated for $\theta>0$, since their displayed quotient is undefined at zero. The six milestones record the pairwise strategy comparisons stated in the appendix proof, in its order: LC with DS, RM, and RN; RN with RM; and DS with RN and RM. Proposition 1 and its appendix proof supply these targets.

Significance

The proposition partitions the buyer’s decision into explicit sufficient regions. It identifies when the low cost of risky sourcing outweighs expected violation costs, when serving both segments separately pays, and when responsible sourcing should serve only the conscious segment or the full market. The four profits also provide the base for the paper’s later comparative statics on sourcing quantities, penalties, and transparency. Those later propositions are outside this mission; their exact treatment of strategy ties and sourcing quantities warrants a separate development. Guo, Lee, and Swinney (2016) establish these results in the published article.

The mathematical result is proved in that article. The formalization task is to give its parameter ranges, four profits, and optimality claims a machine-checkable statement, then prove the pairwise comparisons and the four-clause goal. The draft statements compile locally, but their proofs are open. The resulting model and comparisons can support later formalizations of the article’s other propositions.

Difficulty

The four choices must be compared under a single, consistent profit table. A comparison with one competitor does not establish optimality among all four, and the positive-part term in Proposition 1 compresses two distinct comparisons into one threshold. Boundary cases also matter: a strict “preferred to” comparison can disappear when its profit difference is zero, even though weak optimality remains meaningful. The printed sufficient condition in part (ii) uses $c_{NR}$ inside the violation term, while the appendix’s DS comparisons use $c_R$. Both statements must retain their respective printed forms; treating them as the same expression would change the source claim.

Formalization scope

Lean represents the eight parameters by real fields of one record and the four strategies by a finite inductive type. The range assumptions are $0\leq\theta,\alpha,\phi\leq1$ and $c_{NR}<c_R$. The cost premium is defined from the two costs. The theorem compares exactly the four Table 2 profits; the Section 3–4 derivation of prices and quantities from the underlying selling game is outside this mission. An optimal strategy is weakly best against all four strategies, including itself. A model with fewer competitors or profits that differ from Table 2 would not capture the proposition.

The clauses containing division by $\theta$ require $\theta>0$. The appendix’s strict LC–DS equivalence additionally requires $\theta>0$ and $\alpha\phi<1$; otherwise equal profits can defeat its “if and only if” wording. Proposition 1 itself retains the full standing ranges. No positivity of $v$, $r$, or $c_{VP}$ is assumed. Part (ii) retains the printed $c_{NR}$, which makes its hypothesis stronger than the corresponding appendix conditions with $c_R$. Its conclusion remains valid under the standing ranges. These conventions are visible in the statements and can be checked independently of the paper’s informal derivation.

The development needs only real arithmetic, finite case analysis, the four profit definitions, and the maximum of a real number with zero. The parameter record and strategy comparison interface are reusable for later propositions in the same paper. Contributions that prove the exact milestone statements, establish the goal, or clarify behavior at ties are within scope.

Selected references

• Guo, R., H. L. Lee, and R. Swinney, Responsible Sourcing in Supply Chains, Management Science 62(9):2722–2744, 2016. DOI: 10.1287/mnsc.2015.2256.

Motivation

In classical optimal transport, a transport plan that minimizes the total cost is characterized through its support: an optimal plan is $c$-cyclically monotone, meaning that no finite collection of its transported particles can be re-paired more cheaply (Villani, Optimal Transport, Old and New, 2009, Ch. 4–5). This pointwise criterion is how most structural results in optimal transport are proved: it is what turns a global minimization over measures into a statement about finitely many points.

The martingale transport problem adds a constraint motivated by mathematical finance: the plan must be the law of a one-step martingale $(X, Y)$ with given marginals $X\sim\mu$, $Y\sim\nu$. Its value gives model-independent bounds on the price of an exotic option whose payoff is the cost function, given the prices of all vanilla options at two dates (Beiglböck, Henry-Labordère, Penkner, Model-independent bounds for option prices, Finance Stoch. 2013). Because the martingale constraint ties together all points with the same first coordinate, the classical re-pairing argument does not carry over: swapping two destinations generally destroys the martingale property.

M. Beiglböck and N. Juillet (On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 2016; arXiv:1208.1509v2) prove a martingale replacement for $c$-cyclical monotonicity, the variational lemma (Lemma 1.11). It is the tool from which they derive the left-monotone structure of optimal plans, the uniqueness of the left-curtain coupling as optimizer for costs $h(y-x)$ with $h'$ strictly convex, and the support bounds for optimizers. This mission is the first of a series formalizing that paper.

Setting

All measures live on $\mathbb R$ or $\mathbb R\times\mathbb R$ with their Borel $\sigma$-algebras. Two probability measures $\mu,\nu$ on $\mathbb R$ with finite first moment are in convex order, $\mu\preceq_C\nu$, if $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi:\mathbb R\to\mathbb R$.

A transport plan is a measure $\pi$ on $\mathbb R^2$ with first marginal $\mu$ and second marginal $\nu$. It is a martingale transport plan, $\pi\in\Pi_M(\mu,\nu)$, if under $\pi$ the conditional mean of $y$ given $x$ equals $x$; equivalently,

$$\int\rho(x)\,(y-x)\,d\pi(x,y)=0\quad\text{for every bounded Borel }\rho .$$

A cost is a Borel function $c:\mathbb R^2\to\mathbb R$ satisfying the sufficient integrability condition $c(x,y)\ge a(x)+b(y)$ with $a\in L^1(\mu)$, $b\in L^1(\nu)$; then the cost of a plan, $\int c\,d\pi$, is well defined in $(-\infty,+\infty]$. A plan $\pi\in\Pi_M(\mu,\nu)$ is optimal if $\int c\,d\pi\le\int c\,d\pi'$ for every $\pi'\in\Pi_M(\mu,\nu)$, and it leads to finite costs if $\int c\,d\pi<+\infty$.

A measure $\alpha'$ on $\mathbb R^2$ is a competitor of $\alpha$ (Definition 1.10) if it has the same two marginals as $\alpha$ and the same conditional barycentres: $\int y\,d\alpha_x(y)=\int y\,d\alpha'_x(y)$ for almost every $x$, where $(\alpha_x)$, $(\alpha'_x)$ are disintegrations with respect to the first marginal. A competitor redistributes the mass of $\alpha$ in a way that a martingale plan could absorb: replacing a piece $\alpha$ of a martingale plan by $\alpha'$ keeps both marginals and the martingale property.

Formalization targets

Goal: the variational lemma (Lemma 1.11, p. 8)

Let $\mu\preceq_C\nu$ be probability measures, $c$ a Borel cost satisfying the sufficient integrability condition, and $\pi\in\Pi_M(\mu,\nu)$ optimal with $\int c\,d\pi<+\infty$. Then there is a Borel set $\Gamma\subseteq\mathbb R^2$ with $\pi(\Gamma)=1$ such that

$$\int c\,d\alpha\le\int c\,d\alpha'\quad\text{for every finitely supported }\alpha\text{ with }\operatorname{spt}\alpha\subseteq\Gamma\text{ and every competitor }\alpha'\text{ of }\alpha .$$

The set $\Gamma$ is chosen once, before $\alpha$; the quantifier order is the content.

Milestones

The milestones are the steps of the paper's proof (§3, pp. 16–19), in attack order:

1. Theorem 3.1 (p. 17), Kellerer's duality in the form of Beiglböck–Goldstern–Maresch–Schachermayer: for a Polish probability space $(Z,\zeta)$ and a Borel $M\subseteq Z^n$, either $M\subseteq\bigcup_i M_i$ with $\zeta(\operatorname{proj}^iM_i)=0$, or some measure $\gamma$ with $\gamma(M)>0$ has all marginals $\le\zeta$.
2. The set $M\subseteq(\mathbb R^2)^n$ of $n$-tuples carrying a non-optimal finite measure is Borel (p. 17).
3. In case (1), a Borel $\Gamma_n$ of full $\pi$-measure supports no improvable $\alpha$ with $|\operatorname{spt}\alpha|\le n$ (p. 18).
4. Every finitely supported $\alpha$ has a cost-minimizing competitor (p. 18).
5. If $\omega\le\pi$ and a competitor $\omega'$ is cheaper than $\omega$, then $\pi-\omega+\omega'$ is a cheaper martingale plan (p. 18).
6. For an optimal $\pi$ of finite cost, case (2) cannot occur (pp. 18–19).
7. $\Gamma=\bigcap_n\Gamma_n$ is as required (p. 17).

Significance

The result. The variational lemma converts optimality of a martingale plan, a property of a measure, into a condition on finite configurations of points in its support. In the paper it is applied, together with a lemma on accumulation points of sections (Lemma 3.2), to show that optimizers for costs $h(y-x)$ with $h'$ strictly convex are left-monotone, which by the paper's Theorem 1.5 identifies them as the left-curtain coupling; it also yields the bound $|\operatorname{spt}\pi_x|\le k$ of Theorem 7.1 and the two-graph structure of the optimizers for $\pm|y-x|$. Later missions of this series use it as a milestone. Its converse, under continuity assumptions, is the separate Lemma A.2 of the paper's appendix.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization needs a usable form of Kellerer's duality for multi-marginal problems, which is not in Mathlib, and the bookkeeping that finite rearrangements of a martingale plan stay in $\Pi_M(\mu,\nu)$. Both are reusable well beyond this paper: Kellerer's theorem underlies the analogous results for classical, multi-marginal and martingale transport.

Difficulty

The classical proof of $c$-cyclical monotonicity perturbs an optimal plan by moving a small amount of mass around a finite cycle of its support points. For martingale plans this fails: the perturbation must preserve the conditional barycentre of every $x$, and mass sitting at isolated points of a non-atomic plan cannot be moved without moving mass at uncountably many other points. The proof therefore cannot argue point by point. It works with whole families of bad configurations at once, which requires the measure-theoretic duality of Kellerer (resting on Choquet's capacitability theorem) and a measurable choice of an optimal competitor for each configuration. Proving that the set of bad configurations is Borel, and that a positive-mass family of them can be glued into a cheaper competitor $\omega'$ of a piece $\omega\le\pi$, is the technical core.

Formalization scope

The Lean development uses Mathlib's Measure ℝ and Measure (ℝ × ℝ). Costs and integrals that may be infinite take values in EReal, through the published definition ModelRiskOT.Duality.extIntegral ($\int f^+-\int f^-$, with $(+\infty)-(+\infty)=-\infty$); no Bochner integral of a possibly non-integrable function is compared. Martingale plans and competitors are encoded through test functions $\rho(x)$ (the paper's characterization (4), p. 10) instead of disintegrations. A finitely supported finite measure is written $\sum_{s\in S}w_s\delta_s$ with $S$ a finite set and weights $w_s\ge0$; this covers every such measure, and masses are taken finite. $(\mathbb R^2)^n$ is Fin n → ℝ × ℝ.

Committed conventions and disclosed additions:

• the goal's hypothesis "leads to finite costs" is $\int c\,d\pi<+\infty$; without it, a cost under which every plan has infinite cost makes optimality empty;
• Theorem 3.1 is stated for Borel $M$, the case proved in the cited source and the only case the paper uses; $\zeta(\operatorname{proj}^iM_i)=0$ is the outer measure, since the projections need not be Borel;
• in milestone 3, $\Gamma_n$ is a Borel subset of the paper's $\mathbb R^2\setminus N$ of full measure, because $N$ need not be Borel;
• milestone 4 states, for the uniform measure $\alpha_p$ on the points of an $n$-tuple $p$, both that an optimal competitor $\alpha'_p$ exists and that it can be chosen measurably in $p$ (p. 18), with Mathlib's σ-algebra on the space of measures.

A formalization in which $\Gamma$ is empty or $\pi$-null, or in which $\Gamma$ is allowed to depend on $\alpha$, is trivial and is ruled out by the statement: $\pi(\Gamma^c)=0$ and $\exists\Gamma\,\forall\alpha$. The competitor $\alpha'$ ranges over all measures, not only finitely supported ones.

Welcome contributions: a general form of Kellerer's duality theorem (milestone 1), the Borel-measurability of the bad set, and the gluing step of milestone 6.

Selected references

• M. Beiglböck, N. Juillet, On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 42–106, 2016. arXiv:1208.1509, doi:10.1214/14-AOP966
• M. Beiglböck, M. Goldstern, G. Maresch, W. Schachermayer, Optimal and better transport plans, J. Funct. Anal. 256(6), 1907–1927, 2009. doi:10.1016/j.jfa.2009.01.013
• H. G. Kellerer, Duality theorems for marginal problems, Z. Wahrsch. Verw. Gebiete 67(4), 399–432, 1984. doi:10.1007/BF00532047
• M. Beiglböck, P. Henry-Labordère, F. Penkner, Model-independent bounds for option prices — a mass transport approach, Finance Stoch. 17(3), 477–501, 2013. doi:10.1007/s00780-013-0205-8
• C. Villani, Optimal Transport, Old and New, Springer, 2009. doi:10.1007/978-3-540-71050-9

Product framing in online retail

An online retailer does not show its catalogue at once. Products are arranged on a sequence of pages, and a consumer looks at the first few pages and then chooses among what she has seen, or leaves. Where a product is placed therefore decides whether it is considered at all. Gallego, Li, Truong and Wang (Operations Research, 2020) call the placement decision product framing. They show that the optimal framing problem is NP-hard even with two pages and a multinomial logit choice model, and give polynomial-time framing algorithms with constant performance guarantees.

The paper builds on the assortment optimization literature, where a seller chooses one set of products to offer under a choice model, and on work in which consideration sets depend on how products are presented. Davis, Topaloglu and Williamson (2015) studied a sequential assortment problem in which products are added over time. Two of their results, on how per-product revenue behaves when products are removed, are the structural inputs of this mission. Aouad and Segev (2016) studied a variant with one product per page under the MNL model, in which every product must be displayed.

Setting

There are $n$ products $[n]=\{1,\dots,n\}$, and product $i$ earns unit revenue $r_i$. The products are placed on $m$ pages, each holding at most $p$ products, and a product may be left undisplayed. A consumer views the first $X$ pages, where $X\in[m]$ is random with law $\lambda(x)=\mathbb P[X=x]$ and tail $\Lambda(x)=\mathbb P[X\ge x]$, independent of the framing. Her consideration set is the set of products on pages $1,\dots,X$.

A choice model gives, for each consideration set $S\subseteq[n]$, purchase probabilities $P(i,S)\ge0$ with $P(i,S)=0$ for $i\notin S$ and $\sum_{i\in S}P(i,S)\le1$. The expected revenue of $S$ is $R(S)=\sum_{i\in S}r_iP(i,S)$. The optimal framing value is

$$V^{OPT}=\max_{\text{framings}}\ \sum_{x\in[m]}\lambda(x)\,R(\text{products on pages }1,\dots,x),$$

the maximum over all placements with at most $p$ products per page (problem (1)). The cardinality-constrained assortment problem is $G(c)=\max_{|S|\le c}R(S)$ (problem (2)), and $U(x)=G(x\cdot p)$ is the best revenue from a consumer who sees $x$ pages.

The analysis rests on three assumptions:

• A1: $P(i,S)\ge P(i,T)$ whenever $i\in S\subseteq T$, a property of every random utility model.
• A2: problem (2) can be solved, here exactly.
• A3: $X$ is new better than used in expectation (NBUE): $q(x)=\mathbb E[X-x+1\mid X\ge x]\le q(1)=\mathbb E[X]$ for all $x\in[m]$.

The algorithm NEST($y$), for $y\in[m]$, first takes an optimal solution $S(y)$ of (2) with bound $y\cdot p$. Then, for $x=y-1$ down to $1$, it chooses $S(x)\subseteq S(x+1)$ of size $\min(|S(x+1)|,xp)$ whose per-product revenue $R(S(x))/|S(x)|$ is at least that of $S(x+1)$. Page $x$ displays $S(x)\setminus S(x-1)$, and pages after $y$ stay blank. $V^{NEST(y)}$ is the expected revenue of this framing, and $V^{NEST}=\max_{y\in[m]}V^{NEST(y)}$.

Formalization targets

Goal: Theorem 3 (p. 10)

$$V^{NEST}\ \ge\ \frac{6}{\pi^2}\,V^{OPT}$$

The goal holds under A1, A2 with $\varepsilon=0$ and A3, for every run of NEST($y$), $y\in[m]$. Here $6/\pi^2\approx0.608$.

Milestones

The milestones are the numbered results the proof of Theorem 3 uses, in the order it uses them:

1. Theorem 2, the clairvoyant bound $V^{OPT}\le\mathbb E[U(X)]$.
2. Lemma 1, from Davis et al.: some product can be removed from any $S$ with $|S|\ge2$ without lowering $R(S)/|S|$.
3. The existence of a NEST($y$) run.
4. Proposition 1: $V^{NEST(y)}\ge\frac{U(y)}{y}\mathbb E[\min(X,y)]$.
5. Lemma 2, from Davis et al.: $U(x)/x$ is decreasing.
6. Propositions 2 and 3, on the bound-revealing program (5),

$$\gamma=\min_{U,\Lambda}\ \max_{x\in[m]}\frac{U(x)}{x}\,\mathbb E[\min(X,x)],$$

taken over NBUE tails $\Lambda$ and functions $U\ge0$ that are increasing with $U(x)/x$ decreasing and $\mathbb E[U(X)]=1$. Proposition 3 states $1/\gamma=\max_\Lambda\mathbb E[X/\mathbb E[\min(X,Y)\mid X]]$. 7. Lemma 7 and Corollaries 5–6, comparing NBUE $X$ with an exponential variable of the same mean. 8. The evaluation $\mathbb E[W/(\mu(1-e^{-W/\mu}))]=\pi^2/6$ for $W$ exponential with mean $\mu$. 9. The bound $\gamma\ge6/\pi^2$.

Significance

Theorem 3 gives a constant-factor guarantee for a problem that is NP-hard under the same assumptions. The constant does not depend on the choice model beyond A1, on the number of pages, or on the page capacity, and the paper shows it is tight relative to the upper bound $\mathbb E[U(X)]$ (Proposition 4, in the geometric limit). NEST needs only a cardinality-constrained assortment oracle, which exists in polynomial time for the MNL and nested logit models. The same bound-revealing program, problem (5), is reused in the paper for joint framing and pricing (Theorem 7).

The paper proves the result in full. No part of it has been machine-checked. The mission formalizes the model and states the guarantee and every intermediate result. The proofs combine finite combinatorics (Lemmas 1 and 2, Proposition 1) with a comparison of a discrete NBUE law against the exponential distribution, and that comparison is reusable for other approximation analyses with the same structure. The equality of the exponential integral with $\sum_k k^{-2}$ connects to Mathlib's hasSum_zeta_two.

Difficulty

The upper bound (Theorem 2) and the lower bound (Proposition 1) are each elementary. The difficulty is to compare them uniformly over all choice models and all NBUE page-count laws. The ratio of $\max_y\frac{U(y)}{y}\mathbb E[\min(X,y)]$ to $\mathbb E[U(X)]$ depends on the whole function $U$ and the whole law of $X$, and the worst case cannot be read off from any single instance. Replacing the instance by the program (5) removes the choice model. Bounding the program still requires an optimization over distributions, and its value is attained only in a limit (Proposition 4).

The comparison with the exponential law goes through the increasing convex order. Here $X$ is a discrete law on $\{1,\dots,m\}$ and the comparison variable is continuous. The function $h(x)=x/\mathbb E[\min(Z,x)]$ to which Lemma 7 is applied is increasing and convex only on $[0,\infty)$, so a formal argument has to track the domain.

Formalization scope

Theorem numbers and pages are those of the authors' accepted manuscript (49 pp.), which differ from the journal typesetting. The conventions are:

• Products are Fin n. Pages are the naturals $1,\dots,m$, kept 1-based, with $m,p\ge1$.
• A framing is a map Fin n → ℕ: page $0$ means "not displayed", and each page $1,\dots,m$ holds at most $p$ products. $V^{OPT}$ is the maximum over the finite, nonempty set of feasible framings.
• The law $\lambda$ is a function on $[1,m]$, and $\Lambda$, $\mathbb E[\min(X,x)]$ and $\mathbb E[X]$ are finite sums. A3 is the paper's own $q$-form, and a conditional expectation on a null event imposes nothing.
• The exponential law is Mathlib's expMeasure with rate $1/\mathbb E[X]$. The independence in Corollary 6 is encoded by iterated integrals.
• The revenues are assumed nonnegative ("unit profit or revenue"). Lemma 1 fails for negative revenues.
• A2 is taken with $\varepsilon=0$, as the paper does after p. 8, and polynomial time is not modelled.
• "Increasing" and "decreasing" are weak.

NEST makes arbitrary choices, so a run is a predicate on its output. Theorem 3 is stated for every family of runs, and a separate milestone shows that runs exist. The value $V^{NEST(y)}$ is the expected revenue of the framing the run actually displays, not the closed form $\sum_x\lambda(x)R(S(\min(x,y)))$, whose equality with it is part of the proof of Proposition 1. A formalization that quantified over some run, that defined $V^{NEST(y)}$ by that closed form, or that assumed Lemma 2 for $U$ would not be Theorem 3.

Program (5) is stated with its tail variable $\Lambda$ and law $\lambda(x)=\Lambda(x)-\Lambda(x+1)$, $\Lambda(m+1)=0$. The page's typos are corrected in the statements and recorded in the notes: "$\mathbb E[U(x)]=1$" in (5), and the right-hand side of Corollary 5. Proposition 2 is formalized in its existential reading: some optimal solution of (5) has constant $\frac{U(x)}{x}\mathbb E[\min(X,x)]$.

A complete development needs:

• finite assortment combinatorics;
• the finite program (5) and its compactness;
• the increasing convex order between a discrete NBUE law and the exponential, through integrated tails;
• the integral $\int_0^\infty ue^{-u}/(1-e^{-u})\,du=\pi^2/6$.

The exponential comparison and the integral are reusable beyond this mission. Proofs of any milestone are welcome, including alternative proofs of Lemmas 1 and 2 from A1.

Selected references

• G. Gallego, A. Li, V.-A. Truong, X. Wang, Approximation Algorithms for Product Framing and Pricing, Operations Research, 2020. https://doi.org/10.1287/opre.2019.1875
• J. M. Davis, H. Topaloglu, D. P. Williamson, Assortment optimization over time, Operations Research Letters 43(6), 608–611, 2015. https://doi.org/10.1016/j.orl.2015.08.007
• A. Aouad, D. Segev, Display optimization for vertically differentiated locations under multinomial logit choice preferences, working paper, 2016 (as cited in the paper; later published in Management Science).
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

A decision maker wants to choose $x$ in a compact set $X\subseteq\mathbb R^n$ to minimize an expected cost $c(x,\mathbb P^\star)=\mathbb E_{\mathbb P^\star}[\gamma(x,\xi)]$, but the distribution $\mathbb P^\star$ of $\xi$ is unknown; only independent samples $\xi_1,\dots,\xi_T$ are available. The standard remedy, minimizing the cost under the empirical distribution, is known to produce decisions whose realized cost exceeds the in-sample estimate: the "optimizer's curse" of decision analysis (Smith and Winkler, 2006) and overfitting in statistics. Distributionally robust optimization (DRO) replaces the empirical distribution by a worst case over a set of nearby distributions. Many such sets have been proposed, and the question of which one is best has no answer unless "best" is made precise.

Van Parys, Mohajerin Esfahani and Kuhn (arXiv:1704.04118v3, published in Management Science 67(6), 2021) give such a precise meaning. They ask for the least conservative data-driven decision rule whose out-of-sample disappointment decays exponentially at a prescribed rate $r$ under every possible data-generating distribution, and they prove that DRO over a relative-entropy ball of radius $r$ is that rule. This mission formalizes the prescription half of the result (Theorem 7 of the paper), in which decisions, not only cost estimates, are optimized. The prediction half (Theorem 4) is the subject of mission 1 of this series, and the extension to continuous state spaces (Theorem 10) is mission 3. All page and result numbers below refer to the arXiv version v3 (22 Dec 2019).

Setting

The random parameter takes values in a finite set $\Xi=\{1,\dots,d\}$. The model class is the probability simplex $\mathcal P=\{\mathbb P\in\mathbb R^d_+:\sum_i\mathbb P(i)=1\}$ with the topology inherited from $\mathbb R^d$. The cost $\gamma(x,i)$ is continuous in $x$ for each $i$, and $c(x,\mathbb P)=\sum_i\mathbb P(i)\gamma(x,i)$. From a sample path the decision maker forms the empirical distribution $\hat{\mathbb P}_T(i)=\frac1T\sum_{t=1}^T\mathbb 1_{\xi_t=i}$. When the samples are drawn independently from $\mathbb P$, the probability of an event about $\hat{\mathbb P}_T$ is written $\mathbb P^\infty(\cdot)$.

A data-driven predictor is a continuous function $\hat c:X\times\mathcal P\to\mathbb R$; $\hat c(x,\hat{\mathbb P}_T)$ estimates $c(x,\mathbb P^\star)$. A function $f:\mathcal P\to X$ is quasi-continuous if for every $\mathbb P$, every $\epsilon>0$ and every neighbourhood $U$ of $\mathbb P$ there is a non-empty open $V\subseteq U$ on which $\|f(\mathbb P)-f(\mathbb Q)\|\le\epsilon$ (the set $V$ need not contain $\mathbb P$). A data-driven prescriptor induced by $\hat c$ is a quasi-continuous $\hat x:\mathcal P\to X$ with $\hat x(\mathbb P')\in\arg\min_{x\in X}\hat c(x,\mathbb P')$ for every $\mathbb P'$. The family $\mathcal X$ consists of all such pairs $(\hat c,\hat x)$.

The prescription disappointment of a pair under a model $\mathbb P$ is

$$\mathbb P^\infty\big(c(\hat x(\hat{\mathbb P}_T),\mathbb P)>\hat c(\hat x(\hat{\mathbb P}_T),\hat{\mathbb P}_T)\big),$$

the probability that the true cost of the prescribed decision exceeds its in-sample estimate. Pairs are ordered by their in-sample optimal values: $(\hat c_1,\hat x_1)\preceq_{\mathcal X}(\hat c_2,\hat x_2)$ iff $\hat c_1(\hat x_1(\mathbb P'),\mathbb P')\le\hat c_2(\hat x_2(\mathbb P'),\mathbb P')$ for all $\mathbb P'$. Problem (6) of the paper is the vector optimization problem

$$\min_{(\hat c,\hat x)\in\mathcal X}{}^{\preceq_{\mathcal X}}\ (\hat c,\hat x)\quad\text{s.t.}\quad\limsup_{T\to\infty}\frac1T\log\mathbb P^\infty\big(c(\hat x(\hat{\mathbb P}_T),\mathbb P)>\hat c(\hat x(\hat{\mathbb P}_T),\hat{\mathbb P}_T)\big)\le-r\quad\forall\,\mathbb P\in\mathcal P,$$

and a pair is strongly optimal if it is feasible and $\preceq_{\mathcal X}$ every feasible pair.

The relative entropy is $I(\mathbb P',\mathbb P)=\sum_i\mathbb P'(i)\log(\mathbb P'(i)/\mathbb P(i))$, with $0\log(0/p)=0$ and $p'\log(p'/0)=+\infty$. The distributionally robust predictor and prescriptor are

$$\hat c_r(x,\mathbb P')=\sup_{\mathbb P\in\mathcal P}\{c(x,\mathbb P):I(\mathbb P',\mathbb P)\le r\},\qquad \hat x_r(\mathbb P')\in\arg\min_{x\in X}\hat c_r(x,\mathbb P'),$$

with $\hat x_r$ quasi-continuous (Definition 7). The estimator realization $\mathbb P'$ is the first argument of $I$, the reverse of the usual Kullback–Leibler ball.

Formalization targets

Goal: Theorem 7 (p. 20)

$$r>0\ \Longrightarrow\ (\hat c_r,\hat x_r)\ \text{is strongly optimal in (6), for every quasi-continuous selector }\hat x_r .$$

Milestones

1. Proof of Theorem 7, p. 21 (Bledsoe 1952): a quasi-continuous $\hat x:\mathcal P\to X$ is continuous on a dense subset of $\mathcal P$.
2. Proof of Theorem 7, p. 21 (Berge 1963): for $X$ compact and $\hat c$ continuous, $\mathbb P'\mapsto\hat c(\hat x(\mathbb P'),\mathbb P')$ is continuous for every arg-min selector $\hat x$.
3. Proposition 4, p. 20: for $r\ge0$ a quasi-continuous selector $\hat x_r$ exists.
4. Theorem 6, p. 20: for $r\ge0$, $(\hat c_r,\hat x_r)$ is feasible in (6).
5. Theorem 8, (21), p. 22: $\mathbb P^\infty\big(c(\hat x_r(\hat{\mathbb P}_T),\mathbb P)>\hat c_r(\hat x_r(\hat{\mathbb P}_T),\hat{\mathbb P}_T)\big)\le(T+1)^de^{-rT}$ for every $T\ge1$.

Context from mission 1

The proof of Theorem 7 also uses results posed as milestones of mission 1 of this series: the large deviation bounds of Theorem 1, (7a) and (7b) (p. 12); the continuity of $\hat c_r$ (Proposition 3, p. 16); the inclusion of the disappointment set in $\{I(\cdot,\mathbb P)>r\}$ from the proof of Theorem 3 (pp. 16–17); and the construction of a perturbed model $\mathbb P_2>0$ with $I(\mathbb P'_0,\mathbb P_2)<r$ from the proof of Theorem 4 ((14)–(16), pp. 17–18). They are not posed again here.

Significance

Theorem 7 says that no decision rule whose prescriptions disappoint with probability decaying at rate $r$ can report a smaller in-sample optimal value than relative-entropy DRO, at any realization of the data. It turns a modelling choice (which ambiguity set to use) into a consequence of a statistical requirement, and it identifies the radius $r$ of the ball with the decay rate of the out-of-sample disappointment. Theorem 8 complements this with a finite-sample bound that holds before any data are observed.

The theorem is proved in the paper, and its proof is short given the earlier results; there is no machine-checked version. A complete formalization adds a finite-alphabet Sanov theorem with the infinity convention of the relative entropy, an elementary theory of quasi-continuous functions on the simplex (density of continuity points, selection of quasi-continuous minimizers from an upper semicontinuous arg-min map), and Berge's maximum theorem in the form used here. The paper itself only sketches several steps (the construction of $\mathbb P_1,\mathbb P_2$ "exactly as in the proof of Theorem 4", and the proof of Theorem 8 is omitted).

Difficulty

Theorem 7 does not follow from the predictor result (Theorem 4). The order $\preceq_{\mathcal X}$ compares only the in-sample optimal values, so a competing pair may use a predictor that lies below $\hat c_r$ away from its own minimizers, and the pointwise comparison of predictors that settles Theorem 4 says nothing about such a pair. What the data can detect is governed by the large deviations of $\hat{\mathbb P}_T$, which only see sets with non-empty interior in $\mathcal P$, while the competitor's prescriptor need not be continuous. Without quasi-continuity of $\hat x$ the argument breaks: a selector that jumps to a cheaper decision only on a set with empty interior is invisible to the data, and the theorem is not claimed for such selectors. The existence half (Proposition 4) rests on a selection theorem for upper semicontinuous set-valued maps on Baire spaces (Matejdes 1987, Corollary 4), for which there is no Mathlib counterpart.

Formalization scope

Lean conventions:

• $\Xi$ is Fin d, and $\mathcal P$ is the subtype of stdSimplex ℝ (Fin d) with its subspace topology.
• $X$ is a compact subset of EuclideanSpace ℝ (Fin n), with decisions in the subtype ↥X and the Euclidean distance; $\gamma$ is continuous in $x$ for each $i$. These are the standing assumptions of §2 (p. 5).
• The relative entropy is valued in EReal, equal to $+\infty$ unless $\mathbb P(i)=0\Rightarrow\mathbb P'(i)=0$.
• $\mathbb P^\infty(\hat{\mathbb P}_T\in\mathcal D)$ is the finite sum over sample paths in $\Xi^T$ of $\prod_t\mathbb P(\xi_t)$. For $T=0$ every such event has probability $0$, and Theorem 8 is posed for $T\ge1$.
• The decay rate $\limsup\frac1T\log p_T\le-r$ is encoded without logarithms: for every $r'<r$, eventually $p_T\le e^{-r'T}$.
• $\hat x_r$ is a hypothesis-bound function, quasi-continuous and an arg-min selector of $\hat c_r$, never a chosen one.
• Proposition 4 additionally assumes $X\ne\emptyset$.

Ruled out:

• A rate written with Real.log would treat a probability that vanishes as having rate $0$.
• A real-valued relative entropy would give finite values where the paper has $+\infty$.
• Competing pairs without continuity of $\hat c$ or quasi-continuity of $\hat x$ make the theorem false.

Each of these makes the statement different from the paper's, and none is used.

Reusable infrastructure includes quasi-continuity (with the Bledsoe density theorem), Berge's maximum theorem for the minimum value, and finite-alphabet large deviations for empirical distributions. Contributions of any of these, or of the mission 1 milestones, are welcome.

Selected references

• B. P. G. Van Parys, P. Mohajerin Esfahani, D. Kuhn, From Data to Decisions: Distributionally Robust Optimization is Optimal, Management Science 67(6), 2021; preprint arXiv:1704.04118v3, 2019. https://arxiv.org/abs/1704.04118v3
• W. Bledsoe, Neighborly functions, Proceedings of the American Mathematical Society 3:114–115, 1952.
• C. Berge, Topological Spaces: Including a Treatment of Multi-Valued Functions, Vector Spaces, and Convexity, 1963, pp. 115–116.
• M. Matejdes, Sur les sélecteurs des multifonctions, Mathematica Slovaca 37(1):111–124, 1987.
• J. E. Smith, R. L. Winkler, The optimizer's curse: Skepticism and postdecision surprise in decision analysis, Management Science 52(3):311–322, 2006. https://doi.org/10.1287/mnsc.1050.0451