The OR Formalization Drive

Why ADMM convergence matters

The alternating direction method of multipliers (ADMM) is one of the most widely used algorithms for large-scale convex optimization in statistics, machine learning and signal processing. Its appeal is decomposition: a problem whose objective splits into two parts, coupled only by a linear constraint, is solved by alternately minimizing over each part and updating a dual variable. Each subproblem is often a proximity operator, a projection or a small linear system, so ADMM turns problems such as the lasso, sparse inverse covariance selection and consensus fitting across many machines into sequences of simple steps. The survey of Boyd, Parikh, Chu, Peleato and Eckstein (DOI 10.1561/2200000016) made the method standard, and every algorithm in its later chapters is justified by one convergence result, stated in §3.2.1 and proved in Appendix A. This mission formalizes that result and the inequalities behind it.

The method goes back to Gabay and Mercier (1976). Eckstein and Bertsekas (1992) proved convergence through the theory of maximal monotone operators, by identifying ADMM with Douglas–Rachford splitting applied to the dual problem. The proof in Appendix A of the survey is different: it is a direct Lyapunov argument in finite dimensions that uses only convexity and elementary algebra.

Setting

Let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ and $g:\mathbb R^m\to\mathbb R\cup\{+\infty\}$, let $A\in\mathbb R^{p\times n}$, $B\in\mathbb R^{p\times m}$ and $c\in\mathbb R^p$. The problem is

$$\text{minimize } f(x)+g(z)\quad\text{subject to } Ax+Bz=c, \tag{3.1}$$

with optimal value $p^\star=\inf\{f(x)+g(z)\mid Ax+Bz=c\}$. The augmented Lagrangian with parameter $\rho\ge0$ is

$$L_\rho(x,z,y)=f(x)+g(z)+y^T(Ax+Bz-c)+\tfrac{\rho}{2}\|Ax+Bz-c\|_2^2,$$

and $L_0$ is the ordinary Lagrangian. For $\rho>0$, ADMM generates iterates by

$$x^{k+1}\in\operatorname*{argmin}_x L_\rho(x,z^k,y^k),\quad z^{k+1}\in\operatorname*{argmin}_z L_\rho(x^{k+1},z,y^k),\quad y^{k+1}=y^k+\rho(Ax^{k+1}+Bz^{k+1}-c).$$

The state is $(z^k,y^k)$; $x^0$ plays no role. The primal residual is $r^k=Ax^k+Bz^k-c$, the dual residual is $s^k=\rho A^TB(z^k-z^{k-1})$, and $p^k=f(x^k)+g(z^k)$.

Two assumptions are made. Assumption 1: $f$ and $g$ are closed, proper and convex. Assumption 2: $L_0$ has a saddle point $(x^\star,z^\star,y^\star)$, i.e. $L_0(x^\star,z^\star,y)\le L_0(x^\star,z^\star,y^\star)\le L_0(x,z,y^\star)$ for all $x,z,y$. Nothing is assumed about the ranks of $A$ and $B$. The convergence proof uses the Lyapunov function

$$V^k=\tfrac1\rho\|y^k-y^\star\|_2^2+\rho\|B(z^k-z^\star)\|_2^2 .$$

Formalization targets

Goal: residual and objective convergence (§3.2.1, p. 17; Appendix A, p. 106)

Under Assumptions 1 and 2 and for $\rho>0$, every ADMM run satisfies

$$r^k\to0,\qquad f(x^k)+g(z^k)\to p^\star,\qquad s^k\to0\qquad(k\to\infty).$$

The statement fixes no rate and no constant. It does not claim convergence of $x^k$ or $z^k$, which fails in general (p. 17).

Milestones

In the order of Appendix A:

1. (3.10) holds along the iteration: $0\in\partial g(z^{k+1})+B^Ty^{k+1}$ (§3.3, p. 18);
2. the dual residual inclusion $\rho A^TB(z^{k+1}-z^k)\in\partial f(x^{k+1})+A^Ty^{k+1}$ (§3.3, p. 18);
3. (A.3) $p^\star-p^{k+1}\le y^{\star T}r^{k+1}$;
4. (A.2) $p^{k+1}-p^\star\le-(y^{k+1})^Tr^{k+1}-\rho(B(z^{k+1}-z^k))^T(-r^{k+1}+B(z^{k+1}-z^\star))$;
5. (3.11) $p^k-p^\star\le-(y^k)^Tr^k+(x^k-x^\star)^Ts^k$;
6. the monotonicity step $(y^{k+1}-y^k)^T(B(z^{k+1}-z^k))\le0$ for $k\ge1$ (p. 110);
7. (A.6) $V^k-V^{k+1}\ge\rho\|r^{k+1}-B(z^{k+1}-z^k)\|_2^2$;
8. (A.1) $V^{k+1}\le V^k-\rho\|r^{k+1}\|_2^2-\rho\|B(z^{k+1}-z^k)\|_2^2$ for $k\ge1$;
9. the summed bound $\rho\sum_{k\ge1}(\|r^{k+1}\|_2^2+\|B(z^{k+1}-z^k)\|_2^2)\le V^1$, with $r^k\to0$ and $B(z^{k+1}-z^k)\to0$;
10. the stopping-rule bound $p^k-p^\star\le-(y^k)^Tr^k+d\|s^k\|_2\le\|y^k\|_2\|r^k\|_2+d\|s^k\|_2$ when $\|x^k-x^\star\|_2\le d$ (§3.3.1, p. 19).

Significance

The theorem is what licenses every specialized ADMM of the survey (lasso, basis pursuit, covariance selection, consensus and sharing, distributed model fitting): each of these chapters only computes the subproblem solutions, and correctness of the overall method is inherited from §3.2.1. Inequality (3.11) and its corollary in §3.3.1 justify the primal/dual residual stopping criterion (3.12) used in practice: small residuals certify small suboptimality.

The result itself is classical and proved; it is not open. To our knowledge no machine-checked proof of convex two-block ADMM convergence exists in Lean's Mathlib. Formalizing it produces a reusable development of the augmented Lagrangian method with explicit domain handling for extended-valued convex functions, and checks a proof whose index bookkeeping the printed text leaves loose (the monotonicity step and (A.1) need $k\ge1$, see below).

Difficulty

The obvious argument, "the subproblem optimality conditions plus the saddle point give a decreasing quantity", works only once the right Lyapunov function is found and the cross term $-2\rho\, r^{(k+1)T}B(z^{k+1}-z^k)$ is controlled. That term has no sign from the optimality conditions of a single iteration, and at the first iteration, where $z^0$ is an arbitrary starting point, the decrease (A.1) can genuinely fail. A second obstacle is that $x^k$ and $z^k$ need not converge or even be bounded when $A$ or $B$ is rank deficient, so objective convergence cannot pass through limits of the primal iterates; it has to come from the two-sided bounds (A.2) and (A.3). Finally, the subdifferential sum rule used to linearize each subproblem must be handled for functions taking the value $+\infty$.

Formalization scope

• Vectors are EuclideanSpace ℝ (Fin n); matrices act through Matrix.toEuclideanLin; the problem data are bundled in a structure Problem n m p.
• An extended-valued $f$ is encoded by its effective domain $C_f$ and its real values on $C_f$. Assumption 1 is: $C_f$ nonempty, $f$ convex on $C_f$, epigraph over $C_f$ closed. All minimizations, and the saddle-point inequality in $(x,z)$, range over the domains; this is equivalent to the book's formulation with $+\infty$.
• $p^\star$ is the infimum over feasible points of the domains, not $f(x^\star)+g(z^\star)$ by definition.
• The run is a hypothesis. An ADMM run is any triple of sequences satisfying (3.2)–(3.4) exactly. The book asserts on p. 16 that Assumption 1 makes the subproblems solvable; this is false in general ($f(x)=e^{x_1}$, $A=[0\ 1]$), so no statement constructs iterates. A formalization that defined the iterates by choice, or required $Ax^k+Bz^k=c$ of a run, would trivialize the residual claim and is ruled out.
• Indices: $k\in\mathbb N$ starts at the book's $k=0$. Statements about $x^k$, $r^k$, $s^k$, $p^k$ are for $k\ge1$ (written with $k+1$). The monotonicity step and (A.1) are stated for $k\ge1$; the book states (A.1) without a range, and at $k=0$ with an arbitrary $z^0$ it can fail. The summed bound accordingly starts at $k=1$ and is bounded by $V^1$ instead of $V^0$; it is stated as a bound on every partial sum.
• Subdifferentials (milestones 1–2) use the published ShorNonsmooth.Subdiff.subdifferential relative to the domain.
• The dual-variable convergence $y^k\to y^\star$ listed in §3.2.1 is not proved in the book and is not a target.

A complete development needs the subdifferential of a convex function plus a differentiable quadratic, the first-order characterization of a constrained minimizer, and elementary limits; all of this is reusable for the later missions of the series, which take ADMM runs as given. Proofs of individual milestones are welcome independently.

Selected references

• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011, pp. 1–122. https://doi.org/10.1561/2200000016
• D. Gabay, B. Mercier, A dual algorithm for the solution of nonlinear variational problems via finite element approximation, Computers & Mathematics with Applications 2(1), 1976, pp. 17–40. https://doi.org/10.1016/0898-1221(76)90003-1
• J. Eckstein, D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, Mathematical Programming 55, 1992, pp. 293–318. https://doi.org/10.1007/BF01581204
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

In classical single-machine stochastic scheduling, $N$ jobs with independent random processing requirements $X_i$ are processed one after another, and the makespan (the completion time of the last job) is the same for every schedule that never idles: it is $X_1+\dots+X_N$. Research therefore concentrated on weighted flow times and rewards. Browne and Yechiali (Operations Research 38(3), 1990, 495–498) studied jobs that deteriorate while they wait: the longer a job is delayed, the more processing it needs. Such models arose in the control of queueing and communication systems (Browne 1988; Browne and Yechiali 1989) and in inventory issuing, where stored items lose quality at item-specific rates. Under deterioration the actual processing times depend on the order, so the makespan, and its expectation, become functions of the schedule, and the basic question is which order minimizes the expected makespan.

Setting

There are $N$ jobs, all available at time $0$, and a single processor. Job $i$ has an initial processing requirement $X_i$, a random variable on a probability space $(\Omega,\mathcal F,P)$: the time needed to complete job $i$ if it is processed first. Under linear deterioration, a job whose processing is delayed until time $t$ needs

$$Y_i(t) = X_i + \alpha_i t,$$

where $\alpha_i>0$ is its deterministic growth rate. A job stops deteriorating once it is put on the processor.

Only nonpreemptive strategies without idling are allowed, so a policy is a permutation $\pi$ of $\{1,\dots,N\}$, with $\pi(i)=j$ meaning that job $j$ is the $i$-th processed. The completion times follow the model: $S_0(\pi)=0$, and the job in position $k$ starts at $S_{k-1}(\pi)$ and takes $Y_{\pi(k)}(S_{k-1}(\pi))$, so

$$S_k(\pi) = S_{k-1}(\pi) + X_{\pi(k)} + \alpha_{\pi(k)} S_{k-1}(\pi), \qquad k = 1,\dots,N.$$

The makespan is $S_N(\pi)$ and the expected makespan is $\mathrm E\,S_N(\pi)$. In Lean these are completionTime X α π k ω, makespan X α π ω and expectedMakespan P X α π in the namespace DeterioratingJobs.Makespan.

The paper's Lemma 1 concerns, for real numbers $\mu_i$ and $\gamma_i$, the sum (1)

$$F_{\mu,\gamma}(\pi) = \sum_{i=1}^{N} \mu_{\pi(i)} \prod_{r=i+1}^{N} \gamma_{\pi(r)},$$

the Lean lemma1Sum μ γ π (empty product $=1$).

Formalization targets

Goal: the expected-makespan index rule (§1, p. 496)

If the $X_i$ are integrable, $\alpha_i>0$, and $\pi$ schedules the jobs by increasing values of $\mathrm E(X_i)/\alpha_i$, then

$$\mathrm E\,S_N(\pi) \le \mathrm E\,S_N(\sigma) \qquad\text{for every permutation } \sigma .$$

Milestones

1. Lemma 1 (p. 495). If $\gamma_i>1$ for all $i$, the sum (1) is minimized over all permutations by any permutation ordered by increasing $\mu_i/[\gamma_i-1]$, and maximized by any permutation ordered by decreasing values.
2. Eq. (2) (p. 496). For every $\pi$ and $j\le N$,

$$S_j(\pi) = \sum_{i=1}^{j} X_{\pi(i)} \prod_{r=i+1}^{j} \bigl(1+\alpha_{\pi(r)}\bigr).$$

3. The expected makespan in the form (1) (p. 496, after (2)).

$$\mathrm E\,S_N(\pi) = \sum_{i=1}^{N} \mathrm E(X_{\pi(i)}) \prod_{r=i+1}^{N}\bigl(1+\alpha_{\pi(r)}\bigr) = F_{\mathrm E X,\,1+\alpha}(\pi).$$

Significance

The result is an index rule: each job receives a number computed from its own data, $\mathrm E(X_i)/\alpha_i$, and sorting by that number is optimal. It needs only the means of the initial requirements, not their distributions, and it holds without independence. The same reduction to Lemma 1 gives the paper's other index rules: the variance of the makespan under independent requirements, the Poisson-shock model (5), Lévy-type growth (6) and setup/detach times (7). In inventory issuing, it says which stored item to issue first when items lose value at item-specific linear rates. Lemma 1 itself, which the paper attributes to Rau (1971) and relates to optimal search, is a general statement about ordering products of factors along a sequence.

The result is proved in the paper by an appeal to Lemma 1, whose proof is given there as one sentence ("direct upon an interchange argument"). None of these statements has a machine-checked proof on Prove2Me or in Mathlib. This mission produces a formal model of linear deterioration on a single machine, a formal proof of the interchange lemma with ties handled, and the formal index rule.

Difficulty

The algebra of one adjacent interchange is short. The work is in passing from that local comparison to optimality over all $N!$ permutations, with ties allowed: the paper speaks of "the permutation ordered by increasing values", but with equal indices several permutations qualify, and each of them must be shown optimal. The natural route, "an optimal permutation exists and must be sorted", needs care, because a sorted permutation is not unique and the swap that improves an unsorted permutation may only weakly improve it. On the probabilistic side, the expectation of the makespan must be reduced to the expectations of the $X_i$; the makespan is a polynomial in the $X_i$ with deterministic coefficients, so this is linearity of the integral, but integrability has to be carried through the recursion.

Formalization scope

• Jobs are Fin N (0-based: Lean job i is the paper's job $i+1$); a policy is π : Equiv.Perm (Fin N) with π k the job in position k, as in the paper's $\pi(i)=j$. $N=0$ is allowed.
• The probability space is (Ω, P) with [IsProbabilityMeasure P]; $X_i$ is Ω → ℝ; expectations are Bochner integrals, and every theorem about them assumes each $X_i$ integrable. The growth rates are deterministic reals.
• Completion times are defined by the model recursion $S_{k}=S_{k-1}+Y_{\pi(k)}(S_{k-1})$, never by the closed form (2), so that (2) is a theorem about the model.
• Explicit readings of loose phrases: "the permutation ordered by increasing values of $v_i$" means any permutation with $k\mapsto v_{\pi(k)}$ non-strictly increasing (Monotone), and "decreasing" means Antitone; "is minimized" means $\le$ against every permutation; "expected" means the integral of an integrable random variable.
• Added hypotheses: $\alpha_i>0$ in the goal (the paper divides by $\alpha_i$ without stating it) and $\gamma_i>1$ in Lemma 1 (the paper applies it only with $\gamma_i = 1+\alpha_i$ or $(1+\alpha_i)^2$; for $\gamma_i<1$ the ordering reverses).
• Omitted assumptions: positivity of the $X_i$ and their independence. The goal holds without them, so the formal statement is slightly more general than the paper's.
• Trivializing formalizations are excluded: defining $S$ by formula (2) would make milestone 2 a definition unfolding; a strictly increasing ordering would make the goal vacuous whenever two indices tie; ordering $\pi^{-1}$ instead of $\pi$ states a different theorem; dropping integrability makes all expectations $0$; allowing $\alpha_i=0$ makes $\mathrm E(X_i)/\alpha_i=0$ a meaningless index.
• Not formalized here: the variance result (3), the Poisson model (5), the Lévy model (6), Proposition 1, setup times (7), exponential growth (9), and the NP-hardness conjecture. Proposition 2 (weighted expected completion time) is the companion mission Scheduling Deteriorating Jobs on a Single Processor II.
• Related platform items, none of which states these results: PalmQueueing.Ordering.interchange_permutations (interchange permutations of a GI/GI/1 queue) and the additive, non-deteriorating completion-time models MooreLateJobs.Shared.completionTime and NumStochOpt.ListScheduling.Makespan.

Contributions welcome: proofs of the milestones, a reusable "sorted permutation minimizes a sum of products" lemma, and the variance index (3) as an extension.

Selected references

• S. Browne, U. Yechiali, Scheduling Deteriorating Jobs on a Single Processor, Operations Research 38(3), 1990, 495–498. https://doi.org/10.1287/opre.38.3.495
• J. G. Rau, Minimizing a Function of Permutations of n Integers, Operations Research 19(1), 1971, 237–240. https://doi.org/10.1287/opre.19.1.237
• F. P. Kelly, A Remark on Search and Sequencing Problems, Mathematics of Operations Research 7(1), 1982, 154–157. https://doi.org/10.1287/moor.7.1.154
• R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.

Motivation

A probability model $\mu$ for a risk quantity, such as the reserve process of an insurer or the path of a queue, is usually chosen for tractability or fitted to limited data, and the true law of the system is unknown. Distributional model risk asks how large a probability of interest could be if the true law were any model "close" to $\mu$. When closeness is measured by an optimal transport cost rather than a likelihood ratio, the competing models may put mass where $\mu$ puts none, which is the situation for rare events such as ruin or buffer overflow: the event of interest often lies outside the support of the baseline.

Blanchet and Murthy (arXiv:1604.01446, Mathematics of Operations Research 44(2), 2019) prove strong duality for worst-case expectations over an optimal-transport ball on a general Polish space, with a lower semicontinuous cost. Their §2.4 specializes the duality to worst-case probabilities of a closed set and obtains a closed-form answer: the worst-case probability of $A$ is the baseline probability of an inflated version of $A$. This mission formalizes that result, Theorem 3 of the paper, together with the numbered statements its proof uses.

Setting

Let $S$ be a Polish space with its Borel $\sigma$-algebra, $P(S)$ its probability measures, and $\mu \in P(S)$ the baseline. A cost $c : S \times S \to \mathbb R_+$ satisfies Assumption (A1): it is nonnegative, lower semicontinuous, and $c(x,y) = 0$ if and only if $x = y$.

For $\mu_1, \mu_2 \in P(S)$, a coupling of $\mu_1$ and $\mu_2$ is a probability measure $\pi$ on $S \times S$ with marginals $\mu_1$ and $\mu_2$; $\Pi(\mu_1,\mu_2)$ is the set of couplings, and the optimal transport cost is

$$d_c(\mu_1,\mu_2) = \inf\Big\{\int c\,d\pi : \pi \in \Pi(\mu_1,\mu_2)\Big\}.$$

For a budget $\delta > 0$, the primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S \times S$ with first marginal $\mu$ and $\int c\,d\pi \le \delta$.

Fix a nonempty closed set $A \subseteq S$ and let $c(x,A) = \inf\{c(x,y) : y \in A\}$ be the cheapest cost of moving unit mass from $x$ into $A$. The worst-case probability is

$$I = \sup\{P(A) : d_c(\mu,P) \le \delta\}. \tag{12}$$

Its dual is the univariate problem

$$\inf_{\lambda \ge 0}\Big\{\lambda\delta + E_\mu\big[(1 - \lambda c(X,A))^+\big]\Big\}, \tag{13}$$

and for a minimizer $\lambda^* \in [0,\infty)$ of (13) the paper defines

$$\underline c = \int_{\{c(x,A) < 1/\lambda^*\}} c(x,A)\,d\mu(x), \qquad \overline c = \int_{\{c(x,A) \le 1/\lambda^*\}} c(x,A)\,d\mu(x). \tag{14}$$

Formalization targets

Goal: Theorem 3 (p. 10)

If $\lambda^* \in [0,\infty)$ attains the infimum in (13) and $\underline c = \overline c$, then

$$\sup\{P(A) : d_c(\mu,P) \le \delta\} = \mu\{x : c(x,A) \le 1/\lambda^*\}. \tag{15}$$

Milestones, in the order the proof uses them

1. Coupling form (§2.2, p. 5, for $f = 1_A$): $I = \sup\{\pi(S \times A) : \pi \in \Phi_{\mu,\delta}\}$.
2. Indicator supremum (pp. 8–9): $\sup_{y}\{1_A(y) - \lambda c(x,y)\} = (1 - \lambda c(x,A))^+$ for $\lambda \ge 0$.
3. (13) (p. 9): $I$ equals the infimum in (13).
4. Remark 4, (11) for $f = 1_A$ (p. 8): an $\varepsilon$-optimal plan $\pi_\varepsilon$ satisfies $\int(\varphi_{\lambda^*}(x) - (1_A(y) - \lambda^* c(x,y)))\,d\pi_\varepsilon \le \varepsilon$ and, for $\lambda^* > 0$, $(\delta - \varepsilon/\lambda^*)^+ \le \int c\,d\pi_\varepsilon \le \delta$.
5. Lemma 4 (p. 11): plans $\pi_n \in \Phi_{\mu,\delta}$, $n > 1$, with $\pi_n(C_n) \ge 1 - 1/n$, no cost outside the set $C_n$ of §2.4.1, and $\pi_n(S \times A) \ge I - 2/n$.
6. Lemma 2 (p. 10): $\underline c \le \delta \le \overline c$ if $\lambda^* > 0$ attains (13); $\delta \ge \overline c = \underline c$ if $\lambda^* = 0$ does.

Significance

Theorem 3 converts a supremum over an infinite-dimensional ball of probability measures into a single probability under the baseline: $\mu$ of the set of points that can reach $A$ at cost at most $1/\lambda^*$, where $1/\lambda^*$ is determined by $\delta$ through the one-dimensional function $u \mapsto \int_{\{c(x,A) \le u\}} c(x,A)\,d\mu$. For the cost $c = d$ of a metric this is the baseline probability of the $1/\lambda^*$-neighbourhood of $A$. The paper uses it to compute worst-case ruin probabilities for the Cramér–Lundberg model around a Brownian approximation (§3, §6.1), where $S$ is a path space; the result applies there because nothing in it uses local compactness of $S$.

The result is proved in the paper. As far as the platform's corpus shows, neither it nor the strong duality behind it has been formalized. A formal development produces, beyond Theorem 3: a reusable definition of optimal transport costs with lower semicontinuous costs on Polish spaces; the coupling reformulation of the transport ball, which rests on the existence of optimal transport plans (Villani, Optimal Transport, Theorem 4.1), not in Mathlib; and an $\varepsilon$-optimal-plan argument that avoids assuming a primal optimizer exists.

Difficulty

The heuristic derivation on pp. 9–10 constructs an optimal transport plan that moves each $x$ with $c(x,A) \le 1/\lambda^*$ to a nearest point of $A$ and leaves the others in place. It needs a nearest point to exist and to be selectable measurably, which fails for general closed $A$ in a non-locally-compact space, and it needs a primal optimizer, which need not exist. Theorem 3 assumes neither, so the construction is not a proof. A second point is the boundary level $c(x,A) = 1/\lambda^*$: when $\mu$ charges it, as for atomic baselines, the identity (15) can fail (for $\mu$ a point mass at distance $1$ from $A$ and $\delta < 1$, the worst case is $\delta$, not $1$), and the hypothesis $\underline c = \overline c$ is exactly what excludes this. Measurability is a second obstacle: $x \mapsto c(x,A)$ is an infimum of a lower semicontinuous function over $A$ and in general only universally measurable, so integrals of it are taken against the completion of $\mu$.

Formalization scope

All objects live in the namespace ModelRiskOT.WorstProb. $S$ carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]; $\mu$ is a Measure S with IsProbabilityMeasure; the cost is a real-valued c : S → S → ℝ with (A1) bundled as a structure (nonnegativity, lower semicontinuity on $S \times S$, and $c(x,y) = 0 \iff x = y$). Committed conventions:

• Values in $[0,\infty]$. $d_c$, $I$, the objective of (13), $\underline c$ and $\overline c$ are ℝ≥0∞; integrals are lower Lebesgue integrals and the positive part $(\cdot)^+$ is ENNReal.ofReal. For the universally measurable functions and sets that occur, lower integrals and outer measures agree with the completion of $\mu$, which is the paper's reading (p. 4). No Bochner integral is used.
• The threshold $1/\lambda^*$ is written in multiplied form: $c(x,A) \le 1/\lambda^*$ is $\lambda^* c(x,A) \le 1$, and likewise for the strict inequality and for the sets $C_n$. For $\lambda^* > 0$ this is the printed condition; at $\lambda^* = 0$ it is the whole space, the paper's convention $1/0 = \infty$.
• $d_c$ fixes both marginals; $\Phi_{\mu,\delta}$ fixes only the first.
• $c(x,A)$ is a real infimum over the subtype $A$; every statement assumes $A$ nonempty.
• "$\lambda^*$ attains the infimum in (13)" is $\lambda^* \ge 0$ and $g(\lambda^*) \le g(\lambda)$ for all $\lambda \ge 0$.
• Inequalities $X \ge I - t$ are written $I \le X + t$ in $[0,\infty]$; sequences "$n > 1$" are indexed by $n \in \mathbb N$ with $1 < n$.

A formalization in which the transport ball fixes only the first marginal would contain every probability measure and give $I = 1$ for every nonempty $A$; the definitions here fix both marginals of the couplings in $d_c$, and the hypothesis $\underline c = \overline c$ is kept as stated rather than replaced by continuity of $u \mapsto \int_{\{c(x,A) \le u\}} c(x,A)\,d\mu$.

A complete development needs the existence of optimal couplings for lower semicontinuous costs (tightness and Prokhorov's theorem, available in Mathlib), the strong duality of the paper's Theorem 1 specialized to indicators (milestone 3; a separate mission in this series formalizes Theorem 1 in general), and universal measurability of $c(\cdot,A)$ through projections of Borel sets. The transport-cost definitions and the coupling reformulation are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs that derive (13) from the general strong duality once that is published.

Selected references

• J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, arXiv:1604.01446v2, 2017; Mathematics of Operations Research 44(2):565–600, 2019. https://arxiv.org/abs/1604.01446, https://doi.org/10.1287/moor.2018.0936
• C. Villani, Optimal Transport: Old and New, Grundlehren der mathematischen Wissenschaften 338, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
• R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, arXiv:1604.02199, 2016. https://arxiv.org/abs/1604.02199
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171:115–166, 2018. https://doi.org/10.1007/s10107-017-1172-1
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (universal measurability, Ch. 7).

Motivation

In distributionally robust modelling, a baseline probability model $\mu$ on a space $S$ is distrusted, and the analyst reports the largest expected loss over every model within a budget of $\mu$. Blanchet and Murthy (arXiv:1604.01446; Math. Oper. Res. 44(2), 2019, doi:10.1287/moor.2018.0936) measure the budget with an optimal transport cost and prove strong duality for the resulting worst-case expectation on an arbitrary Polish space, with a lower semicontinuous cost and an upper semicontinuous performance function. Duality computes the worst-case value. A risk manager also wants the worst-case model: a distribution that attains the value, whose structure explains which perturbation of $\mu$ is most harmful.

Such a model need not exist. Unlike the Kantorovich problem, where the set of couplings with two fixed marginals is weakly compact, the feasible set here fixes only one marginal and is not compact in general. Section 5 of the paper gives an example on $\mathbb R$ where the supremum is not attained, then gives abstract conditions under which it is (Proposition 9), and growth conditions on a locally compact normed space that imply them (Corollary 1). Related existence results in $\mathbb R^d$ were obtained by Gao and Kleywegt (arXiv:1604.02199, 2016) and, for empirical baselines and norm costs, by Mohajerin Esfahani and Kuhn (arXiv:1505.05116, 2018).

Setting

Let $S$ be a Polish space with its Borel $\sigma$-algebra, $\mu$ a probability measure on $S$, $\delta>0$ a budget, $c:S\times S\to[0,\infty)$ a cost and $f:S\to\mathbb R$ a performance function. The standing assumptions are:

• (A1) $c$ is lower semicontinuous and $c(x,y)=0$ iff $x=y$;
• (A2) $f$ is upper semicontinuous and $\mu$-integrable.

The primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S\times S$ with first marginal $\mu$ and $\int c\,d\pi\le\delta$ (transport plans out of $\mu$ of cost at most $\delta$). The primal objective is $I(\pi)=\int f(y)\,d\pi(x,y)$ and the primal value is $I=\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}$. The dual feasible set $\Lambda_{c,f}$ consists of pairs $(\lambda,\varphi)$ with $\lambda\ge0$, $\varphi:S\to[-\infty,\infty]$ universally measurable and $\varphi(x)+\lambda c(x,y)\ge f(y)$ for all $x,y$. The dual objective is $J(\lambda,\varphi)=\lambda\delta+\int\varphi\,d\mu$ and the dual value is $J=\inf J(\lambda,\varphi)$. For $\lambda\ge0$ put $\varphi_\lambda(x)=\sup_y\{f(y)-\lambda c(x,y)\}$.

Section 5 assumes throughout that $(\lambda^*,\varphi_{\lambda^*})\in\Lambda_{c,f}$ is a dual optimal pair with $I=J=J(\lambda^*,\varphi_{\lambda^*})<\infty$. Write $\Phi'_{\mu,\delta}$ for the plans in $\Phi_{\mu,\delta}$ concentrated on $\{f(x)\le f(y)\}$.

(P-Compactness): for every $\varepsilon>0$ there are a compact $K_\varepsilon$ with $\mu(K_\varepsilon)>1-\varepsilon$ and $\gamma>0$ such that $\{(x,y)\in K_\varepsilon\times S: f(y)-\lambda^*c(x,y)\ge\varphi_{\lambda^*}(x)-\gamma\}$ has compact closure. (P-USC): $\limsup_n I(\pi_n)\le I(\pi^*)$ whenever $\pi_n\in\Phi'_{\mu,\delta}$ converge weakly to $\pi^*\in\Phi_{\mu,\delta}$.

On a normed space $E$: (A3) $c(x,y)\ge g(\|x-y\|)$ for $\|x-y\|>C$, with $g$ nondecreasing and $g(t)\uparrow\infty$. (A4) $(f(y)-f(x))/(1+h(\|x-y\|))\le K$ for an increasing $h$ with $h(t)\uparrow\infty$; and for every $\varepsilon>0$, $f(y)-f(x)\le\varepsilon(1+c(x,y))$ once $\|x-y\|>C_\varepsilon$.

Formalization targets

Goal: Corollary 1 (p. 27)

Let $E$ be a real normed space that is locally compact, and let $c,f$ satisfy (A1)–(A4). Under the standing assumption, if $\lambda^*>0$ there is $\pi^*\in\Phi_{\mu,\delta}$ with

$$I(\pi^*)=I=J=J(\lambda^*,\varphi_{\lambda^*}).$$

Milestones

1. Remark 4, (10)–(11) (p. 8): for $\pi\in\Phi_{\mu,\delta}$, $I-I(\pi)$ is the sum of two nonnegative gaps, $\int(\varphi_{\lambda^*}(x)-f(y)+\lambda^*c(x,y))\,d\pi$ and $\lambda^*(\delta-\int c\,d\pi)$; so an $\varepsilon$-optimal plan has both gaps at most $\varepsilon$.
2. Lemma 17 (p. 43): every plan in $\Phi_{\mu,\delta}$ can be replaced by one in $\Phi'_{\mu,\delta}$ with at least the same value.
3. §5 display (p. 26): $I=\sup\{I(\pi):\pi\in\Phi'_{\mu,\delta}\}$.
4. Proposition 9 (p. 26): on a Polish space, (P-Compactness) and (P-USC) give a primal optimizer.
5. Corollary 1, Step 1 (p. 28): (A1)–(A4) and $\lambda^*>0$ give (P-Compactness).
6. Corollary 1, Step 2 (pp. 28–29): (A1), (A2), (A4) and $I<\infty$ give (P-USC):

$$\limsup_n\int f(y)\,d\pi_n\le\int f(y)\,d\pi^*.$$

Significance

The result. An attained worst case turns duality into a structural statement. By Theorem 1(b) of the paper, an optimizer moves mass from $x$ only to maximizers of $f(y)-\lambda^*c(x,y)$ and, when $\lambda^*>0$, uses the full budget. When those maximizers are unique (Remark 8: $c$ convex in $y$, $f$ concave) the worst-case model is unique and is the image of $\mu$ under a transport map. That map is what stress tests and robust estimators are built from. Without existence, these statements describe an object that may not be there.

Formalizing it. The paper's proofs are complete; nothing here is open. No machine-checked version of this result is known: the worst-case optimal transport literature, including the strong duality of this paper, is unformalized. The mission produces the transport objects of §2 in a form that keeps the paper's generality (Polish space, lower semicontinuous real cost, universally measurable dual variables, the $\infty-\infty$ convention), a tightness argument for nearly optimal one-marginal plans, and an upper semicontinuity argument for unbounded upper semicontinuous integrands under uniform integrability.

Difficulty

The obvious argument takes a maximizing sequence and extracts a weak limit. Both steps fail without more structure. First, $\Phi_{\mu,\delta}$ is not tight: only the first marginal is fixed, and a sequence may push mass to infinity at bounded cost. That is exactly what happens in Example 2 (p. 26), where $\lambda^*=0$ and the value $1$ is approached but never reached. Tightness has to come from the dual: nearly optimal plans concentrate near maximizers of $f(y)-\lambda^*c(x,y)$, and (A3)–(A4) with $\lambda^*>0$ confine those maximizers. Second, $f$ is only upper semicontinuous and unbounded, so weak convergence alone does not give $\limsup\int f\,d\pi_n\le\int f\,d\pi^*$. A uniform integrability bound is needed, and it uses the restriction to $\Phi'_{\mu,\delta}$ in an essential way. A third, Lean-specific difficulty is measure-theoretic: $\varphi_{\lambda^*}$ is only universally measurable, and the gaps of Remark 4 are integrals against completions.

Formalization scope

All declarations sit in the namespace ModelRiskOT.PrimalOpt. Values of $I(\pi)$, $I$, $J(\lambda,\varphi)$, $J$ and $\varphi_\lambda$ are in EReal. $I(\pi)$ is $\int f^+(y)\,d\pi-\int f^-(y)\,d\pi$ with lower integrals, and Mathlib's $\top-\top=\bot$ realises the paper's reading of the supremum (footnote 2, p. 5). Integrals of nonnegative or extended-real functions are lower integrals (lintegral), never Bochner integrals. Universal measurability is the published BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. Weak convergence is the topology of ProbabilityMeasure (S × S). Measures on $S\times S$ use the product $\sigma$-algebra.

The following readings are fixed:

• The standing assumption of §5 ($(\lambda^*,\varphi_{\lambda^*})\in\Lambda_{c,f}$, $I=J$, $J=J(\lambda^*,\varphi_{\lambda^*})$, finiteness) consists of hypotheses of Proposition 9 and Corollary 1. $I=J$ is Theorem 1(a), the goal of the companion mission on strong duality, and is not assumed proved here.
• In (P-Compactness) the constant $\gamma$ may depend on $\varepsilon$.
• "Increasing" in (A4) is strict.
• Remark 4's second conclusion in (11) is also stated as $\lambda^*(\delta-\int c\,d\pi)\le\varepsilon$, which covers $\lambda^*=0$.
• Lemma 17's last inequality is stated for every plan, which is equivalent under the EReal convention.
• Corollary 1's space is a real normed space with LocallyCompactSpace. It also carries PolishSpace, which is redundant, since a locally compact real normed space is finite-dimensional.

The goal cannot be satisfied by a junk value: $I$ and $J$ are EReal suprema and infima, not real sSup, and the hypothesis $\lambda^*>0$ is kept because Example 2 shows the conclusion fails without it. A sorry-free check that $c(x,y)=(x-y)^2$, $f(y)=y$ on $\mathbb R$ satisfy (A1), (A3) and (A4) accompanies the drafts.

A complete development needs Prokhorov's theorem (in Mathlib), a Fatou lemma for weakly converging measures with a lower semicontinuous integrand, an upper semicontinuity theorem for uniformly integrable upper semicontinuous integrands, and the change of variables $\int\varphi(x)\,d\pi=\int\varphi\,d\mu$ for universally measurable $\varphi$. The last three are reusable well beyond this mission. Proofs of any milestone, and these general lemmas as separate contributions, are welcome.

Selected references

• J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2):565–600, 2019. arXiv:1604.01446v2, doi:10.1287/moor.2018.0936
• R. Gao and A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, 2016. arXiv:1604.02199
• P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171:115–166, 2018. arXiv:1505.05116
• A. M. Zapała, Unbounded mappings and weak convergence of measures, Statist. Probab. Lett. 78(6):698–706, 2008. doi:10.1016/j.spl.2007.09.033
• C. Villani, Optimal Transport: Old and New, Springer, 2009. doi:10.1007/978-3-540-71050-9

Motivation

Large zero–one linear programs can contain constraints involving only a small fraction of their variables. Crowder, Johnson and Padberg study how to extract useful inequalities from one such row while solving the larger program. Their computational method identifies a violated inequality at a current linear programming solution, adds it, and resolves the relaxation. The mathematical question behind that step is whether a minimal cover inequality can be found by a separate optimization problem. The authors answer it in Section 2.3 of their 1983 paper, after developing cover and configuration inequalities in Section 2.2. Crowder, Johnson and Padberg (1983)

The target is a known result from that paper. It is a precise statement about a finite knapsack row and a point in the unit cube, independent of the paper's implementation and numerical experiments. The paper also discusses $(1,k)$-configurations and lifting, which turn the identified inequalities into valid cuts involving additional row variables. Those statements supply the mission's milestones and make the separation result useful in its original setting. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4

Setting

Fix a finite index set $K$, positive rational coefficients $a_j$ for $j\in K$, and a rational right-hand side $a_0$. A zero–one solution is a vector with each $x_j\in\{0,1\}$ satisfying the single row

$$\sum_{j\in K}a_jx_j\le a_0. \tag{2.5}$$

The model uses the support set $x=\{j:x_j=1\}$ for such a vector. A set $S\subseteq K$ is a minimal cover when its total coefficient exceeds $a_0$, but removing any one member makes the total at most $a_0$:

$$\sum_{j\in S}a_j>a_0, \qquad \sum_{j\in S}a_j-a_k\le a_0\quad(k\in S). \tag{2.6}$$

It yields the cover inequality $\sum_{j\in S}x_j\le |S|-1$ for every feasible zero–one vector. The right-hand side is interpreted as a real number, so the expression also has its usual meaning when $S$ is empty.

A $(1,k)$-configuration consists of $S^*\subseteq K$, $t\notin S^*$ and an integer $2\le k\le |S^*|$. The set $S^*$ itself fits the row, while $Q\cup\{t\}$ is a minimal cover for every $k$-element subset $Q$ of $S^*$. For any $k\le r\le |S^*|$ and $r$-element $T\subseteq S^*$, its inequality is $(r-k+1)x_t+\sum_{j\in T}x_j\le r$. Crowder, Johnson and Padberg (1983), pp. 810–811

For a point $\bar x\in[0,1]^K$, the separation problem asks for a cover $s\subseteq K$ minimizing $\sum_{j\in s}(1-\bar x_j)$, subject to the strict condition $\sum_{j\in s}a_j>a_0$. This is problem (2.12). The set of attainable values is finite, but it is empty if the row has no cover. An optimal value $z$ is therefore asserted only when a least attainable value exists.

Formalization targets

Cover separation

The goal is the paper's Section 2.3 equivalence:

$$\left(\exists S\subseteq K\text{ minimal}: \sum_{j\in S}\bar x_j>|S|-1\right) \quad\Longleftrightarrow\quad z<1,$$

where $z$ is the attained optimum of (2.12). A cover inequality cuts off $\bar x$ precisely when its left-hand side exceeds $|S|-1$. If there is no cover, (2.12) has no optimal value; the theorem does not assign it an artificial value. Crowder, Johnson and Padberg (1983), pp. 812–813

Valid inequalities and lifting

The milestones state the validity of (2.7) and every inequality in (2.9), the two assertions used in the separation equivalence, and the relaxed lifting claims of Section 2.4. For lifting, $z_k$ is the maximum integer objective value in (2.10), $\bar z_k$ is the maximum in its linear relaxation, and $z_k^*=\lfloor\bar z_k\rfloor$. The claims are $z_k\le z_k^*$ and validity after adding variable $k$ with coefficient $f_k=f_0-z_k^*$. They concern attained optima, as the paper's “maximum” language requires. Crowder, Johnson and Padberg (1983), pp. 811, 814

Significance

The equivalence turns a geometric question about which cover inequality excludes $\bar x$ into a finite optimization test with a numerical threshold of one. It identifies when a minimal cover cut exists for a row, while the validity milestones certify that the inequalities can be added without removing zero–one feasible points. The lifting claims explain how an inequality first written on a subset of variables remains valid as further variables enter it. These are the mathematical guarantees used by the paper's cutting plane procedure. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4

The paper proves the separation equivalence and states the surrounding validity claims. This mission records their exact statements in Lean; its theorem proofs remain open. A complete development would add machine-checked proofs for the finite cover argument, configuration inequalities, and lifting validity. The resulting definitions of feasible supports, attained optimization values and intermediate inequality validity can also be reused in other finite knapsack formalizations.

Difficulty

Checking all subsets of $K$ directly grows rapidly with the row size. A separation result must relate a minimum over all covers to an inequality indexed by a minimal cover, while accounting for objective coefficients that may be zero when $\bar x_j=1$. The same boundary matters for lifting: the zero–one maximum is compared with a continuous relaxation, and rounding is justified by the integer coefficients of the current inequality. If the lifting problem is infeasible, neither maximum exists. Crowder, Johnson and Padberg (1983), pp. 812–814

Formalization scope

Lean uses an arbitrary finite index type for $K$, replacing the paper's indices $1,\ldots,n$. A zero–one vector is a finite support set. Row coefficients and $a_0$ are rational, as on p. 810; the point $\bar x$ and separation values are real. The target asks only that $\bar x$ lie in the unit cube. Although the paper obtains it as an optimum of the full LP relaxation (2.11), that additional property is not used in the row-level equivalence. No sign condition is imposed on $a_0$.

The strict knapsack condition in (2.12) is retained. “Chops off” means strict violation of (2.7). “Optimal value” means membership and leastness in the attainable value set; for lifting it means membership and greatestness. Thus rows with no cover or infeasible lifting subproblem do not acquire a default zero optimum. The size expressions $|S|-1$ and $r-k+1$ are evaluated in the reals, so natural-number truncation cannot change them. Integer lifting coefficients and the floor of the relaxed optimum express the paper's “truncating to its integer part”; the feasible relaxed problem includes the zero vector, so this agrees with truncation toward zero there.

Validity during an intermediate lifting step ranges over feasible zero–one vectors supported in the current set $S$. After adding $k$, it ranges over support in $S\cup\{k\}$. The final inequality covers the whole row when that set is $K$. The development must preserve the full quantifier over every $k$-subset in (2.8) and every $r$ and $T$ in (2.9); restricting these would weaken the paper's claim. Contributions proving the named milestones, adding concrete examples, or developing general finite optimization lemmas are in scope. The facet assertions attributed to Padberg are outside the target. A related lifted-cover facet statement already appears on the platform as NemhauserWolsey.partitioned_cover_lifting_defines_facet; its conventions and claim differ from this mission's validity results.

Selected references

• H. Crowder, E. L. Johnson and M. Padberg, Solving Large-Scale Zero-One Linear Programming Problems, Operations Research 31(5), 803–834, 1983. DOI: 10.1287/opre.31.5.803

Motivation

A retailer that can display only some of its products must choose an assortment: the set of products offered to an arriving customer. Customers substitute: whether a given product is bought depends on what else is on the shelf. The assortment problem asks for the offer set that maximises expected revenue under a model of this substitution behaviour. It is a core problem of revenue management (Talluri and van Ryzin, Management Science 2004), and it is NP-hard already for a mixture of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, POMS 2014).

The heuristic used most widely in practice is revenue-ordered assortments: sort the products by price and offer, for some threshold, every product priced at least that threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin 2004) but not in general. Berbeglia and Joret (arXiv:1606.01371v3, 2019; Algorithmica 2020) give a tight analysis of its approximation ratio for every regular discrete choice model, a class that includes all random utility models. They prove three incomparable guarantees. This mission formalizes the third, Theorem 3.3, whose ratio depends on the purchase behaviour of an optimal assortment rather than on the prices. Companion missions in this series cover the price-ratio bound (Theorem 3.2) and the tightness of all three bounds (Theorem 3.4).

Setting

Let $\mathcal C$ be a finite nonempty set of products. A system of choice probabilities gives, for every offer set $S\subseteq\mathcal C$ and product $x$, the probability $\mathcal P(x,S)$ that a customer offered $S$ buys $x$. Buying nothing is the option $0$, with $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular when

1. $\mathcal P(x,S)\ge0$ for products and for $x=0$;
2. $\mathcal P(x,S)=0$ for $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$ and $x\in S\cup\{0\}$.

Axiom 4 at $x=0$ says that enlarging the offer set never makes buying nothing more likely.

Prices are a function $r:\mathcal C\to\mathbb R_{>0}$. Offering $S$ earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\mathrm{rev}(S)$. Let $r_1<\dots<r_k$ be the distinct values of $r$, and let $S_i=\{x:r(x)\ge r_i\}$ for $i\in[k]$. The revenue-ordered strategy earns

$$\mathrm{RO}=\max_{1\le i\le k}\mathrm{rev}(S_i).$$

For an assortment $S^*$, the purchase profile is

$$N_i=\sum_{x\in S^*,\ r(x)\ge r_i}\mathcal P(x,S^*)\qquad(i\in[k]),\qquad N_{k+1}:=0,$$

the probability that a customer offered $S^*$ buys something priced at least $r_i$. It is non-increasing in $i$.

Formalization targets

Goal: Theorem 3.3 (p. 9)

Let $S^*$ be optimal, $\mathrm{rev}(S^*)=\mathrm{OPT}$, suppose $N_1>0$, and let $\ell\in[k]$ be maximum with $N_\ell>0$. Then

$$\mathrm{OPT}\le\Big(\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\Big)\mathrm{RO} \qquad\text{and}\qquad \sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\le1+\ln\nu,\quad\nu=\frac{N_1}{N_\ell}.$$

The first inequality is the paper's sum-form factor, the bound that Theorem 3.4 shows to be tight. The second is the closed form $1/(1+\ln\nu)$.

Milestones (in proof order)

• Lemma 2.1 (p. 6): $\sum_{x\in S}\mathcal P(x,S)\le\sum_{x\in S'}\mathcal P(x,S')$ for $S\subseteq S'$.
• First observation of the proof (p. 9): $N_i\le\sum_{x\in S_i}\mathcal P(x,S_i)$ and $N_ir_i\le\sum_{x\in S_i}\mathcal P(x,S_i)r_i$.
• Inequality (6) (p. 9): $N_ir_i\le\mathrm{RO}$ for every $i\in[k]$.
• Revenue identity (p. 9): $\mathrm{rev}(S^*)=\sum_{i=1}^{\ell}(N_i-N_{i+1})r_i=\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}N_ir_i$.
• Logarithmic step (p. 9, the comparison $1/\sum\ge1/(1+\ln\nu)$ in Theorem 3.3, used in the last inequality of the proof): for $N_1\ge\dots\ge N_\ell>0$ and $N_{\ell+1}=0$, $\sum_{i=1}^{\ell}(N_i-N_{i+1})/N_i\le1+\ln(N_1/N_\ell)$. The paper states this step without proof.

Significance

Theorem 3.3 gives a guarantee that is independent of prices. The bound $1+\ln(r_k/r_1)$ of Theorem 3.2 grows when prices are spread out. The bound $1+\ln\nu$ is small whenever an optimal assortment sells its expensive products with probability comparable to its overall purchase probability. In §4 the paper combines it with a reduction from unit-demand pricing to derive, for example, the $1/(1+\ln m)$ guarantee of uniform pricing for the unit-demand min-pricing problem (Corollary 4.8, originally due to Aggarwal et al.). Together with Theorems 3.1 and 3.2, it describes the performance of the most common assortment heuristic over the whole class of regular models, with no parametric assumption on customer behaviour.

The theorem is proved on paper. To our knowledge it has no machine-checked proof, and no regular choice model has been formalized on the platform. This mission produces the regular model as a reusable definition, a statement of Theorem 3.3 in which every hypothesis is explicit, and formal versions of the proof's identities and inequalities. The logarithmic step is asserted without proof in the source, so a formal proof of it completes the paper's argument.

Difficulty

Each step is elementary. The difficulty is bookkeeping. The revenue of $S^*$ has to be regrouped by distinct price levels rather than by products: several products may share a price, and $k$ counts values. The regrouping uses an Abel-type rearrangement with the boundary convention $N_{k+1}=0$. Comparing $N_i$ with the purchase probability of $S_i$ needs regularity twice. First, axiom 4 for products passes from $S^*$ to $S^*\cap S_i$. Then the no-purchase case passes from $S^*\cap S_i$ to $S_i$. A proof that uses axiom 4 only for products fails at the second step, and the claim is false without it.

Formalization scope

• Products form a finite type C with [Fintype C] [DecidableEq C]. The goal adds [Nonempty C], the paper's $k\ge1$. Offer sets are Finset C, and $\mathcal P$ is P : C → Finset C → ℝ. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S. IsRegular P carries axioms 1–4, including both no-purchase cases.
• $\mathrm{OPT}$ is Finset.sup' over all subsets. $\mathrm{RO}$ is Finset.sup' over the indices $1,\dots,k$ of the threshold sets only.
• Indices are 1-based natural numbers. level r i is $r_i$ for $1\le i\le k$. purchaseProfile P r S i is $N_i$ for $1\le i\le k$ and $0$ otherwise, which builds in $N_{k+1}=0$.
• Optimality is the hypothesis $\mathrm{rev}(S^*)=\mathrm{OPT}$. The index $\ell$ is a variable with hypotheses $1\le\ell\le k$, $N_\ell>0$, and $N_i\not>0$ for $\ell<i\le k$. $N_1>0$ is kept as in the paper.
• The approximation factor is stated in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$, never as a ratio. Both the sum form and the logarithmic form are stated. $\ln$ is Real.log, applied to $\nu\ge1$.
• The milestones other than the goal are stated for an arbitrary $S^*$, because the proof does not use optimality there.

The following statements are trivial or false and are not this mission: a maximum over all subsets in place of $\mathrm{RO}$; regularity without its no-purchase case; a purchase profile taken from a non-optimal set while $\mathrm{rev}(S^*)$ is still called the optimum; the logarithmic form alone; a specific choice model (MNL, Markov chain) in place of an arbitrary regular $\mathcal P$.

A complete development needs finite sums regrouped by the values of a function and an elementary logarithm inequality. The regular choice model and the revenue-ordered sets are shared with the other missions of this series and are reusable for any analysis of assortment heuristics. Proofs of any milestone are welcome. So are alternative arguments for the logarithmic step and a proof that $N$ is non-increasing.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82, 2020. https://arxiv.org/abs/1606.01371v3
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191