Operations Research

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

Motivation

A decision based on observed data can change when the data law differs from the one used to choose it. Distributionally robust optimization addresses this by evaluating each decision against a family of nearby probability laws. Optimal transport gives one way to define “nearby”: a candidate law is admissible when probability mass can be moved from the baseline law at a bounded expected cost. For a linear decision rule, the resulting worst-case expectation is usually harder to optimize than an ordinary sample-average loss. Blanchet, Murthy, and Zhang identify a dual objective whose variables are the decision vector and a scalar transport multiplier, then study its curvature near the multipliers that actually minimize it (Blanchet–Murthy–Zhang, 2022).

The paper proves that this dual objective is jointly strongly convex on a specified region for sufficiently small transport radius. This matters because ordinary convexity allows flat directions in the joint decision–multiplier space. The joint lower Hessian bound gives local curvature in every direction with one positive modulus that remains independent of the radius apart from the paper's explicit factor $\sqrt{\delta}$ (Theorem 4, p. 11).

Setting

Let $X\in\mathbb R^d$ have a baseline probability law $P_0$, and let a decision be a vector $\beta$ in a nonempty compact convex set $B\subseteq\mathbb R^d$. The loss of a possible outcome $x$ is $\ell(\beta^{\mathsf T}x)$ for a convex function $\ell:\mathbb R\to\mathbb R$. A state-dependent positive-definite matrix $A(x)$ sets the cost of moving mass from $x$ to $x'$:

$$c(x,x')=(x-x')^{\mathsf T}A(x)(x-x').$$

Assumption 1 requires this cost to be lower semicontinuous and the eigenvalues of $A(x)$ to lie between positive constants $\rho_{\min}$ and $\rho_{\max}$ for $P_0$-almost every $x$. Assumption 2 requires at most quadratic growth of $\ell$ and a finite fourth moment of $P_0$. The ambiguity radius $\delta$ is positive (Assumptions 1–2, pp. 9–10).

The paper's dual objective is an expectation under the known law $P_0$. Write $q_A(\beta,x)=\beta^{\mathsf T}A(x)^{-1}\beta$. For a scalar $\lambda\ge0$ and an auxiliary scalar $\gamma$, set

$$F(\gamma,\beta,\lambda;x) =\ell\bigl(\beta^{\mathsf T}x+\gamma\sqrt\delta\,q_A(\beta,x)\bigr) -\lambda\sqrt\delta\bigl(\gamma^2q_A(\beta,x)-1\bigr), \qquad f_\delta(\beta,\lambda)=\mathbb E_{P_0}\!\left[\sup_{\gamma\in\mathbb R}F(\gamma,\beta,\lambda;X)\right].$$

This value may be $+\infty$. Under the paper's duality conditions, minimizing $f_\delta(\beta,\lambda)$ over $\lambda\ge0$ gives the worst-case loss at $\beta$ (Theorem 1 and (7), p. 10).

Formalization targets

Assumption 3 bounds $\ell''$ above by $M>0$ and excludes an almost surely zero $\ell'(\beta^{\mathsf T}X)$ for each $\beta\in B$. Assumption 4 makes $B$ compact. Lemma 6 supplies positive constants $\underline L,\overline L$ bounding $\mathbb E_{P_0}[\ell'(\beta^{\mathsf T}X)^2]$ uniformly over $B$. With $R_\beta=\sup_{\beta\in B}\|\beta\|$, the constants $K_1,K_2$ are those of (28), and

$$\mathbb V_\delta=\{(\beta,\lambda):\beta\in B,\ \lambda\ge0,\ K_1\|\beta\|\le\lambda\le K_2\|\beta\|\}.$$

Theorem 3 first gives a bounded Hessian on $\mathbb V_\delta$ and a positive lower bound on its $\beta$ block when $0<\delta<\delta_0$, with the explicit $\delta_0$ from p. 36. The goal, Theorem 4, adds Assumption 5: $\ell$ is locally strongly convex and, at each $\beta\in B$, the loss derivative and the linear score are simultaneously separated from zero with positive probability. It asserts the joint bound

$$\exists\,\delta_1\in(0,\delta_0),\ \kappa_1>0\quad \forall\,\delta\in(0,\delta_1),\ \forall\,\theta\in\mathbb V_\delta:\quad \nabla^2 f_\delta(\theta)\succeq\sqrt\delta\,\kappa_1 I_{d+1}.$$

The order of the quantifiers is part of the target: $\kappa_1$ works for every sufficiently small $\delta$ (Theorems 3–4, p. 11).

Significance

The Hessian bound makes the joint dual parameters locally identifiable by curvature on a region that contains every dual optimizer. In the paper, this structure also underlies the analysis of algorithms and of how the optimizer changes with the transport radius (Proposition 1, p. 11; §3 and §5.4). Theorem 4 is already proved in the paper; this mission asks for its machine-checked formalization, together with the stated bounds on multipliers, the maximizing scalar, and the intermediate curvature results. The general optimal-transport integral used here already has a published Prove2Me definition from Blanchet and Murthy's earlier model-risk work. The new definitions specify this paper's Mahalanobis model, regions, and smoothness assumptions.

Difficulty

Convexity alone gives only a nonnegative Hessian; it cannot produce a strictly positive joint lower bound. Even curvature of $\ell$ does not by itself control directions that combine a change in $\beta$ with a change in $\lambda$. The inner supremum over $\gamma$ can become infinite outside its effective domain, while at $\beta=0$ its maximizer ceases to be unique. The theorem therefore needs a region where the dual objective is finite and differentiable and a probabilistic condition that prevents the relevant score and derivative from vanishing together. The target keeps the actual $\sqrt\delta$ scale instead of settling for a radius-dependent positive constant (§2.2.2 and Remark 4, pp. 10–12, 39).

Formalization scope

Lean uses EuclideanSpace ℝ (Fin d) for $\mathbb R^d$, a Borel probability measure for $P_0$, and EReal for $f_\delta$ and the inner supremum. The reused extended-real integral records the $+\infty$ and $-\infty$ cases; the Hessian is taken only where $f_\delta$ is finite on a neighborhood and its real representative is differentiable there. Quadratic Hessian forms use $\|v_\beta\|^2+v_\lambda^2$, since Lean's product norm is not the paper's Euclidean norm. The compact set $B$ is explicitly nonempty, and the positive ambiguity radius $\delta$ is quantified inside the goal so that $\delta_1$ and $\kappa_1$ are uniform in $\delta$. Theorem 3 additionally assumes $R_\beta>0$ for the proof's explicit formula for $\delta_0$: nonempty compact $B=\{0\}$ would make that formula zero. Assumption 5 already gives $R_\beta>0$ in the goal.

The goal retains Assumption 5's per-decision quantifiers. That assumption itself excludes $0\in B$: its strict score event is empty at $\beta=0$. Intermediate statements where the printed wording includes $\beta=0$ but the claim fails there state $\beta\ne0$ explicitly. Lemma 5 also states the differentiability and positive-multiplier conditions needed for its derivative and division. Proposition 9(b)'s printed strict curvature-margin inequality is corrected to the nonstrict inequality derived in its proof; its original wording is preserved in the milestone quotation. The claims are about the expectation $f_\delta$, with $\kappa_1$ independent of $\delta$, rather than a pointwise or merely convex substitute.

A complete development needs measurable extended-real integration, the matrix quadratic form and its inverse, almost-everywhere spectral bounds, differentiability under an expectation, and Hessian estimates for an optimized scalar. The transport integral, the assumptions and constants, and the multiplier bounds are intended as reusable interfaces for the companion missions. Contributions that close the listed lemmas or add the paper's omitted second-order kernel formula are within scope.

Selected references

• José Blanchet, Karthyek Murthy, and Fan Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Mathematics of Operations Research 47(2), 2022. arXiv:1810.02403v3; DOI:10.1287/moor.2021.1178.
• José Blanchet and Karthyek Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2), 2019. arXiv:1604.01446v2.

Motivation

A linear two-stage stochastic program chooses a first-stage decision $x$ before an uncertain parameter $\tilde\xi$ is revealed, and pays the optimal value $Q(x,\xi)$ of a second-stage linear program once the realization $\xi$ is known. Such programs are the basic model of planning under uncertainty in operations research, and their computational complexity determines which solution methods can be expected to work. In 2006, Dyer and Stougie argued that linear two-stage stochastic programs with fixed recourse are #P-hard even when the random data follow independent uniform distributions. Hanasusanto, Kuhn and Wiesemann showed that this proof is not correct and gave a corrected one, which also covers approximate evaluation to sufficiently high accuracy; their note also shows that, when the second-stage constraint matrix itself depends on $\xi$ (random recourse), even finding an approximately optimal decision is strongly NP-hard.

This mission formalizes that last result, Theorem 4 of the note. The previous missions of the series treat the hardness of evaluating the expected recourse with fixed and with random recourse.

Setting

The Integer Feasibility Problem. An instance is an integer matrix $A\in\mathbb Z^{m\times n}$ and an integer vector $b\in\mathbb Z^m$ such that the polytope $\{y\in\mathbb R^n:Ay\le b\}$ lies in the unit cube $[0,1]^n$. The question is whether some binary vector $y\in\{0,1\}^n$ satisfies $Ay\le b$. This problem is strongly NP-hard (Garey and Johnson).

The second-stage problem. For a decision $x\in\mathbb R$ and a realization $\xi\in[0,1]^n$, write $e$ for the all-ones vector and consider

$$\begin{aligned} Q(x,\xi)=\ \text{minimize}\ \ & e^\top y\\ \text{subject to}\ \ & y\in\mathbb R^n_+,\ \lambda\in\mathbb R^m_+,\ x\ge e^\top y,\\ & y_i\ge \xi_i+(b-A\xi)^\top\lambda,\quad y_i\ge(1-\xi_i)+(b-A\xi)^\top\lambda\qquad(i=1,\dots,n). \end{aligned}$$

The coefficient of $\lambda$ in each constraint depends on $\xi$, which is what makes the recourse random.

Problem (11). With $\tilde\xi$ uniformly distributed on $[0,1]^n$,

$$\text{minimize}\ \ x+\mathbb E\big[Q(x,\tilde\xi)\big]\quad\text{subject to}\ \ x\in\mathbb R .$$

The second stage is not feasible for every $x$ (the problem lacks relatively complete recourse), so a decision $x$ is feasible only if the second stage is feasible for every $\xi\in[0,1]^n$. Let $f^\star$ be the infimum of the objective over feasible decisions. A feasible $x$ is $\epsilon$-optimal if

$$\frac{\big|f^\star-\big(x+\mathbb E[Q(x,\tilde\xi)]\big)\big|}{\max\{|f^\star|,1\}}\le\epsilon .$$

The constant $\epsilon'$. Lemma 4 fixes $\epsilon'$ with $0\le\epsilon'<\tfrac12$ and $\epsilon'\sum_j|A_{ij}|<1$ for every row $i$.

Formalization targets

Goal: Theorem 4 as a reduction

For an instance with nonempty polytope, $n\ge1$, $\epsilon'$ as above, $0\le\epsilon<\epsilon'/(4n)$, and any $\epsilon$-optimal decision $x$ of (11),

$$\exists\,y\in\{0,1\}^n:\ Ay\le b\iff x>n-\frac{\epsilon'}{2}.$$

This is the mathematical content of "determining an $\epsilon$-optimal decision is strongly NP-hard whenever $\epsilon<\epsilon'/4n$": a single comparison of any approximate decision with a threshold answers the NP-hard question.

Milestones

1. Lemma 4. $Ay\le b$ has a binary solution iff it has a solution in $([0,\epsilon']\cup[1-\epsilon',1])^n$.
2. The second stage. If $A\xi\le b$, the second stage is feasible iff $\sum_i\max\{\xi_i,1-\xi_i\}\le x$, with value $\sum_i\max\{\xi_i,1-\xi_i\}$; otherwise it is feasible iff $x\ge0$, with value $0$. Optimal $y$ is unique in both cases.
3. The optimal decision. $x$ is feasible iff $x\ge x^\star$, and $x^\star$ is the unique optimal decision, where

$$x^\star=\max\Big\{\sum_{i=1}^n\max\{\xi_i,1-\xi_i\}:A\xi\le b\Big\}.$$

4. The dichotomy. The answer is affirmative iff $x^\star=n$, and negative iff $x^\star<n-\epsilon'$.
5. Accuracy of the decision. Every $\epsilon$-optimal $x$ satisfies $|x^\star-x|\le2n\epsilon$.

Significance

The result. Theorem 4 implies that, unless the problems in NP admit an efficient solution scheme, there is no fully polynomial-time approximation scheme for two-stage stochastic programs with random recourse, even with a one-dimensional first stage and a uniform distribution. Together with the #P-hardness results of the same note, it delimits what algorithms such as sample average approximation can guarantee once relatively complete recourse and fixed recourse are dropped.

Formalizing it. The theorem has a short published proof, but that proof leaves several conventions implicit: the index set of the constraint block, the meaning of first-stage feasibility, and the condition on $\epsilon'$ when $A$ has a zero row. A machine-checked version fixes each of them and verifies that the claimed formula for $x^\star$ is correct under the chosen reading. To our knowledge none of these statements has been formalized before. The objects are elementary (finite-dimensional linear programs, a set integral on the unit cube), and the second-stage solution and rounding lemma are reusable for related reductions from integer feasibility.

Difficulty

The individual steps are short; the difficulty is bookkeeping across three layers. The second stage is an optimisation over $(y,\lambda)$ whose feasibility depends on the sign pattern of $b-A\xi$; the first stage requires a supremum over a polytope to be attained (compactness), and the expected recourse to be the same integral for all feasible decisions (integrability of a piecewise-defined value function over the cube). The tempting shortcut, reading off feasibility from the value of $Q$, fails: an infeasible linear program has no meaningful value, and treating it as cost $0$ would make every decision look optimal. Similarly, an almost-sure notion of feasibility looks natural for a stochastic program but invalidates the formula for $x^\star$ whenever the polytope has measure zero, as it typically does for integer feasibility instances written with equalities.

Formalization scope

All objects live in SPHardness.IntFeas. Vectors are functions on Fin n and Fin m; $A$ and $b$ are integer and are cast to $\mathbb R$, and integrality is kept because Lemma 4 depends on it. The uniform law on $[0,1]^n$ is Lebesgue measure restricted to the cube (volume $1$); expectations are set integrals. The recourse value, $f^\star$ and $x^\star$ are sInf/sSup in $\mathbb R$, and second-stage feasibility, first-stage feasibility and $\epsilon$-optimality are separate predicates, so no statement depends on the junk value of an empty infimum.

Pinned readings and added conventions:

• The page writes the constraint block as "$\forall i=1,\dots,m$" and $x^\star$ with $\sum_{i=1}^m$, adding "$n=m=k$". Here the block ranges over $i=1,\dots,n$, $\xi\in[0,1]^n$, and $m$ (the number of rows of $A$) is arbitrary.
• First-stage feasibility is robust: feasible for every $\xi\in[0,1]^n$, not almost every $\xi$.
• $\epsilon'<\min_i\{(\sum_j|A_{ij}|)^{-1}\}$ is encoded as $\epsilon'\sum_j|A_{ij}|<1$ for every row, together with $0\le\epsilon'<\tfrac12$.
• Added hypotheses, all disclosed in the statements: the polytope $\{A\xi\le b\}$ is nonempty (the proof's own assumption), $n\ge1$, and $\epsilon\ge0$.

Strong NP-hardness, the FPTAS consequence, running times and encoding lengths are not formalized; the goal is the correctness of the reduction. A statement in which $x$ ranges over arbitrary reals satisfying a hypothesised identity, rather than over $\epsilon$-optimal decisions of the program (11) built from $(A,b)$, would be trivial and is ruled out: every object in the goal is defined from the instance.

Contributions welcome: proofs of the milestones, in particular measurability and integrability of the recourse function on the cube and attainment of $x^\star$, which are reusable for other piecewise-linear recourse functions.

Selected references

• G. A. Hanasusanto, D. Kuhn, W. Wiesemann, A comment on "computational complexity of stochastic programming problems", Mathematical Programming (2016); preprint Optimization Online 2015/03/4825 (version of October 6, 2015). https://optimization-online.org/wp-content/uploads/2015/03/4825.pdf, DOI https://doi.org/10.1007/s10107-015-0958-2
• M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Mathematical Programming 106 (2006) 423–432. https://doi.org/10.1007/s10107-005-0597-0
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• J. R. Birge, F. Louveaux, Introduction to Stochastic Programming, Springer, 1997 (2nd ed. 2011, https://doi.org/10.1007/978-1-4614-0237-4).

Motivation

The alternating direction method of multipliers (ADMM) is one of the standard splitting methods for problems of the form $\min_x\{g(Ax) + h(x)\}$, in which a nonsmooth term acts on a linear image of the variable. It is used in signal and image processing, statistical learning and matrix completion, and in many of these applications $g$ or $h$ is nonconvex: sparsity penalties such as $\ell_0$ or $\ell_p$ with $p<1$, rank constraints, or indicator functions of nonconvex sets. For convex problems the convergence theory of ADMM is classical; for nonconvex problems the questions of whether, and how fast, the iterates converge were open until the last decade.

R. I. Boţ and D.-K. Nguyen (arXiv:1801.01994v2, Math. Oper. Res. 45(2), 2020, DOI) analyse a proximal ADMM with variable metrics and its linearized variant in the nonconvex setting. Their first main result (Theorem 14, the subject of the companion mission of this series) shows that bounded iterates converge to a KKT point when a regularization of the augmented Lagrangian has the Kurdyka–Łojasiewicz property. This mission formalizes their second main result, Theorem 20: when that function has the Łojasiewicz property with exponent $\theta$, the iterates converge in finitely many steps, linearly, or sublinearly, according to the value of $\theta$.

Timeline. Łojasiewicz (1963) proved his gradient inequality for real-analytic functions; Attouch and Bolte (Math. Program. 2009) derived from its nonsmooth version the rates $\theta=0$ / $\theta\in(0,\frac12]$ / $\theta\in(\frac12,1)$ for the proximal point algorithm; Bolte, Sabach and Teboulle (Math. Program. 2014) gave a general KL-based convergence scheme (PALM); Li and Pong (SIAM J. Optim. 2015) proved convergence of a proximal ADMM under KL assumptions; Boţ and Nguyen (2018/2020) treated variable metrics, relaxation parameters $\rho\in(0,2)$, and the linearized variant, with explicit rates.

Setting

Let $g:\mathbb R^m\to\mathbb R\cup\{+\infty\}$ be proper and lower semicontinuous, $h:\mathbb R^n\to\mathbb R$ differentiable with $L$-Lipschitz gradient, and $A:\mathbb R^n\to\mathbb R^m$ linear. The augmented Lagrangian with parameter $r>0$ is

$$L_r(x,z,y) = g(z) + h(x) + \langle y, Ax - z\rangle + \frac r2\|Ax-z\|^2 .$$

Given positive semidefinite matrices $M_1^k$, $M_2^k$ and $\rho\in(0,2)$, Algorithm 1 produces $(x^k,z^k,y^k)_{k\ge0}$ from any starting point by: $z^{k+1}$ minimizes $L_r(x^k,z,y^k) + \frac12\|z-z^k\|^2_{M_2^k}$; $x^{k+1}$ minimizes $L_r(x,z^{k+1},y^k) + \frac12\|x-x^k\|^2_{M_1^k}$; and $y^{k+1} = y^k + \rho r(Ax^{k+1} - z^{k+1})$. Algorithm 2 replaces $h(x)$ in the $x$-step by $\langle x - x^k,\nabla h(x^k)\rangle$.

Assumption 2 requires $g$ and $h$ to be bounded below, $A$ to be surjective with $\lambda\|y\|^2\le\|A^*y\|^2$ ($\lambda>0$), $\|M_1^k\|\le\mu_1$, $\|M_2^k\|\le\mu_2$, $r\ge4T_0L>0$, and $2M_1^k + rA^*A\succeq(L + C'_{\mathbf M}/r)\,\mathrm{Id}$ for all $k$, where $T_0$ and $C'_{\mathbf M}$ are explicit functions of $\lambda,\rho,L,\mu_1$.

The analysis runs on the regularized augmented Lagrangian of Section 3

$$\mathcal F_r(x,z,y,x',y') = L_r(x,z,y) + 2T_1\|A^*(y-y')\|^2 + C_1\|x-x'\|^2,$$

with explicit constants $T_1$, $C_1$. Along a run, $\mathcal F_k = \mathcal F_r(x^k,z^k,y^k,x^{k-1},y^{k-1})$. If the run converges to $(\hat x,\hat z,\hat y)$, put $\hat u = (\hat x,\hat z,\hat y,\hat x,\hat y)$, $\mathcal F_* = \mathcal F_r(\hat u)$ and $\mathcal E_k = \mathcal F_k - \mathcal F_*$. $\mathcal F_r$ has the Łojasiewicz property at $\hat u$ with constant $C_L>0$ and exponent $\theta\in[0,1)$ if

$$|\mathcal F_r(u) - \mathcal F_*|^\theta \le C_L\operatorname{dist}(0,\partial\mathcal F_r(u))$$

for all $u$ near $\hat u$, where $\partial$ is the limiting subdifferential.

Formalization targets

Goal: Theorem 20 (p. 28)

Under Assumption 2, for a bounded run converging to $(\hat x,\hat z,\hat y)$ at which $\mathcal F_r$ has the Łojasiewicz property with exponent $\theta$:

$$\theta = 0:\quad (x^k,z^k,y^k) = (\hat x,\hat z,\hat y)\ \text{ for all large } k;$$ $$\theta\in(0,\tfrac12]:\quad \|x^k-\hat x\|,\ \|y^k-\hat y\|,\ \|z^k-\hat z\| \le \hat C\,\hat Q^k,\quad \hat Q\in[0,1);$$ $$\theta\in(\tfrac12,1):\quad \|x^k-\hat x\|,\ \|y^k-\hat y\| \le \hat C(k-1)^{-\frac{1-\theta}{2\theta-1}},\quad \|z^k-\hat z\|\le\hat C(k-2)^{-\frac{1-\theta}{2\theta-1}}.$$

All constants are existential and independent of $k$; the goal fixes only the shape of each rate.

Milestones

1. Lemma 15 (p. 23): a real sequence with $e_{k-l_0} - e_k \ge C_e e_k^{2\theta}$ decreases to $0$ in finite time, linearly, or as $(k - l_0 + 1)^{-1/(2\theta-1)}$.
2. Lemma 16 (p. 25): the descent inequality (80) under Assumption 2.
3. (83) (p. 25): $\mathcal F_{k+1} + \frac{C_1}4\|x^{k+1}-x^k\|^2 + \frac12\|z^{k+1}-z^k\|^2_{M_2^k} + \frac1{\rho r}\|y^{k+1}-y^k\|^2\le\mathcal F_k$.
4. The subgradient estimate of p. 26: an explicit $D^{k+1}\in\partial\mathcal F_r$ with $|||D^{k+1}|||\le C_{14}\|x^{k+1}-x^k\| + C_{15}\|y^{k+1}-y^k\| + C_{16}\|y^k-y^{k-1}\|$.
5. Lemma 17 (p. 26): $\mathcal E_{k-1} - \mathcal E_{k+1}\ge C_{19}\mathcal E_{k+1}^{2\theta}$.
6. Theorem 18 (p. 27): the three rates for $\mathcal E_k$.
7. Lemma 19 (p. 27): $\|x^k-\hat x\|$, $\|y^k-\hat y\|$, $\|z^k - \hat z\|$ bounded by $\max\{\sqrt{\mathcal E},\varphi(\mathcal E)\}$ with $\varphi(s) = \frac{C_L}{1-\theta}s^{1-\theta}$.

Significance

Theorem 20 is the quantitative half of the paper: it converts a local growth condition on one explicit function into convergence rates for the iterates of two practical nonconvex splitting methods. Since semi-algebraic functions satisfy the Łojasiewicz property with some exponent, the theorem applies to most of the sparsity- and rank-type models for which ADMM is used, and it explains when finite termination or linear convergence is to be expected. The intermediate results (Lemma 15 in particular) are the standard route from a Łojasiewicz inequality to rates and recur in the analysis of many first-order methods.

The result is proved in the paper; to our knowledge no part of it has a machine-checked proof. The mission produces a formal statement and proof of the rates, with every constant of the paper defined explicitly, and records where the paper's constants need recomputing: the constants $C_8$ and $C_{10}$ of Lemma 9 are reused on p. 26 for a regularization whose gradient is twice as large.

Difficulty

Lemma 15 is elementary but delicate: the recurrence has a lag $l_0$ and, for $\theta>\frac12$, a nonlinearity that a direct induction does not control, and the index bookkeeping determines the exponent. The rates for $\mathcal F_k$ require a bound on an explicit subgradient of $\mathcal F_r$, whose limiting subdifferential involves the nonsmooth $g$, so the calculus of limiting subgradients for a sum of a lower semicontinuous and a smooth function on a product space is needed. Transferring rates from $\mathcal F_k$ to the iterates needs a finite-length estimate with explicit constants, uniform in the tail. A tempting shortcut, applying the Łojasiewicz inequality directly to $L_r$, fails: $L_r$ does not decrease along the iterates; only the regularized $\mathcal F_r$ does.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin n); $g$ takes values in EReal and is proper and lower semicontinuous; $L_r$ and $\mathcal F_r$ take values in EReal. Points of $\mathbb R^n\times\mathbb R^m\times\mathbb R^m\times\mathbb R^n\times\mathbb R^m$ form a nested WithLp 2 product, so the norm and the inner product are the Euclidean ones of the paper. The limiting subdifferential is the published NonconvexSplitting.Shared.LimitingSubdiff. The two algorithms are the constructors of an inductive type; a run is a relation (any minimizer may be taken), and every statement holds for both. $\lambda_{\min}(AA^*)$ and $\sup_k\|M_i^k\|$ are replaced by arbitrary valid bounds. $\mathcal F_*$ is $\mathcal F_r(\hat u)$, which the paper shows equals $\lim_k\mathcal F_k$.

The Łojasiewicz hypothesis requires the inequality for every subgradient, so that $\operatorname{dist}(0,\emptyset) = +\infty$, and only at points with $\mathcal F_r(u)\ne\mathcal F_*$, the convention $0^0 = 0$; with Lean's $0^0 = 1$ the hypothesis would be unsatisfiable at $\theta = 0$, and a Łojasiewicz hypothesis that no function satisfies, an Assumption 2 that no data satisfy, or a rate whose constant depends on $k$ would each make the targets trivial. Assumption 2 together with the run predicate is satisfiable (checked on a one-dimensional instance), and all constants are quantified before $k$.

Labelled corrections: $\mathcal F_r$ uses $C_1$ as displayed on p. 25 (not $C_1/2$); $C_8 = 4C_1 + C_5$ and $C_{10} = C_7 + 8T_1\|A\|^2$ are recomputed for the Section 3 $\mathcal F_r$; Lemma 17 asks for $k_0\ge2$; Lemma 19 assumes $C_1>0$, since for $C_1 = 0$ the paper's $C_{20}$ is $+\infty$.

Needed infrastructure: calculus of the limiting subdifferential for the sum of a lower semicontinuous function and a $C^1$ function on a product space, the descent lemma, and real-power estimates for sequences. Lemma 15 is independent of ADMM and reusable. Proofs of individual milestones are welcome in any order.

Selected references

• R. I. Boţ, D.-K. Nguyen, The proximal alternating direction method of multipliers in the nonconvex setting: convergence analysis and rates, Math. Oper. Res. 45(2), 2020. https://arxiv.org/abs/1801.01994 (v2), https://doi.org/10.1287/moor.2019.1008
• H. Attouch, J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Math. Program. 116, 2009. https://doi.org/10.1007/s10107-007-0133-5
• J. Bolte, S. Sabach, M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Math. Program. 146, 2014. https://doi.org/10.1007/s10107-013-0701-9
• G. Li, T. K. Pong, Global convergence of splitting methods for nonconvex composite optimization, SIAM J. Optim. 25(4), 2015. https://doi.org/10.1137/140998135