Operations Research

Convex Optimization Optimization Probability·Captain: mikedeng1

Wait-and-Judge Scenario Optimization 1: For Convex Programs, Seeing s_N Support Constraints Gives P^N{V(x_N) > ε(s_N)} ≤ γ, the Value of the Variational Problem (10)Research Paper

Motivation

Many decision problems in control, finance and engineering must hold against an uncertain parameter $\delta$ whose distribution is unknown, while samples of $\delta$ (measurements, historical records, simulations) are available. The scenario approach replaces the uncertain constraint by the constraints of the $N$ observed samples and solves the resulting convex program. The open question is then how robust its solution is: with what probability does a new, unseen $\delta$ violate it?

The classical answer, due to Calafiore and Campi (doi:10.1007/s10107-003-0499-y, 2005; doi:10.1109/TAC.2006.875041, 2006) and sharpened by Campi and Garatti (doi:10.1137/07069821X, 2008), is an a-priori bound: it depends only on $N$ and the dimension $d$ , and it is tight for the worst problems. It is conservative for the many problems whose solution is determined by far fewer than $d$ samples. Campi and Garatti's wait-and-judge theorem (doi:10.1007/s10107-016-1056-9, Math. Program. 2018) replaces it by an a-posteriori certificate: after solving, count the samples that actually determine the solution and certify the solution at a level that depends on that count.

Timeline:

2005–2006, Calafiore and Campi: a convex scenario program in $\mathbb R^d$ has at most $d$ support constraints; first sample-size bounds.
2008, Campi and Garatti: the exact bound $\mathbb P^N\{V(x^*_N)>\epsilon\}\le\sum_{i=0}^{d-1}\binom Ni\epsilon^i(1-\epsilon)^{N-i}$ , with equality for fully-supported problems.
2018, Campi and Garatti: the wait-and-judge bound, Theorem 1 below, with the 2008 bound as a corollary.

Setting

The decision variable is $x\in\mathbb R^d$ . A problem consists of a cost vector $c\in\mathbb R^d$ , a convex domain $\mathcal X\subseteq\mathbb R^d$ , convex constraint sets $\mathcal X_\delta\subseteq\mathbb R^d$ indexed by $\delta$ in a probability space $(\Delta,\mathcal F,\mathbb P)$ , and convex tie-break functions $t_1,\dots,t_p$ . Given an i.i.d. sample $\delta^{(1)},\dots,\delta^{(N)}$ with $N>d$ , the scenario program is

\min_{x\in\mathcal X}\ c^{\mathsf T}x\quad\text{subject to}\quad x\in\bigcap_{i=1}^N\mathcal X_{\delta^{(i)}}.

Ties are broken by minimising $t_1$ among the minimisers, then $t_2$ , and so on; the resulting solution is $x^*_N$ .

The violation of a point is $V(x)=\mathbb P\{\delta\in\Delta: x\notin\mathcal X_\delta\}$ .
A constraint is a support constraint if removing it changes the solution; $s^*_N$ is their number.
Assumption 1: for every $m$ and every sample of size $m$ , the program with those $m$ constraints has a unique tie-broken solution.
Assumption 2 (non-degeneracy): for every $m$ , with probability one, keeping only the support constraints does not change the solution.

The variational problem (10) is: for a function $\epsilon:\{0,\dots,d\}\to[0,1]$ ,

\gamma^*=\inf_{\xi\in C^d[0,1]}\xi(1)\quad\text{s.t.}\quad\frac1{k!}\frac{\mathrm d^k}{\mathrm dt^k}\xi(t)\ge\binom Nk t^{N-k}\,\mathbf 1_{[0,1-\epsilon(k))}(t),\ \ t\in[0,1],\ k=0,\dots,d.

Formalization targets

Goal: Theorem 1 (p. 10)

For every $[0,1]$ -valued $\epsilon(k)$ , under Assumptions 1 and 2,

\mathbb P^N\{V(x^*_N)>\epsilon(s^*_N)\}\ \le\ \gamma^*.

The level $\epsilon$ is evaluated at the observed number of support constraints. The goal fixes no particular $\epsilon$ , which keeps it stable under any later choice of levels.

Milestones (the proof of Theorem 1, Sect. 5.1)

$s^*_m\le d$ for every sample (quoted from [7]).
(14): $\mathbb P^N\{V(x^*_N)>\epsilon(k)\wedge s^*_N=k\}=\binom Nk\,\mathbb P^N\{A\}$ , where $A$ adds "the first $k$ constraints are of support".
$A=B$ up to a null set, where $B$ concerns the program on the first $k$ samples.
(16): $\mathbb P^N\{A\}=\int_{(\epsilon(k),1]}(1-v)^{N-k}\,\mathrm dF_k(v)$ , with $F_k(v)=\mathbb P^k\{V(x^*_k)\le v\wedge s^*_k=k\}$ .
(17): $\mathbb P^N\{V(x^*_N)>\epsilon(s^*_N)\}=\sum_{k=0}^d\binom Nk\int_{(\epsilon(k),1]}(1-v)^{N-k}\,\mathrm dF_k(v)$ .
(18): $\sum_{k=0}^{\min\{m,d\}}\binom mk\int_{[0,1]}(1-v)^{m-k}\,\mathrm dF_k(v)=1$ for every $m$ .
Weak duality between the truncated moment problem (20) and its dual (21), giving (22).
(23): $\frac1{k!}\frac{\mathrm d^k}{\mathrm dt^k}t^m=\binom mk t^{m-k}$ for $m\ge k$ , and $0$ otherwise.
(24): the infimum of $p(1)$ over polynomials feasible for (10) equals $\gamma^*$ .

Companions

Theorem 2 (p. 11): for $\beta\in(0,1)$ and $\epsilon(k)=1-t(k)$ , with $t(k)$ the unique root in $(0,1)$ of $\frac{\beta}{N+1}\sum_{m=k}^N\binom mk t^{m-k}-\binom Nk t^{N-k}=0$ , the probability is at most $\beta$ .
The root lemma of Sect. 5.3, including its sign and divergence claims.
$\gamma^*\le\sum_{i<d}\binom Ni\epsilon^i(1-\epsilon)^{N-i}$ for constant $\epsilon$ (Sect. 5.2).
Corollary 1, the 2008 bound.

Significance

Theorem 1 turns the number of support constraints, which is observed after solving, into a confidence statement that holds uniformly over all convex problems and all distributions. With Theorem 2's choice of $\epsilon(k)$ , a user who finds $k\ll d$ support constraints obtains a level $\epsilon(k)$ comparable to that of a $k$ -dimensional problem, which is far below the a-priori level for dimension $d$ . The classical bound (2) is recovered as Corollary 1, so Theorem 1 contains the earlier theory.

The result is proved in the paper. As far as is known, it has no machine-checked proof. A formalization produces:

a formal account of scenario programs with lexicographic tie-break and of support constraints in the "changes the solution" sense;
the exchangeability argument (14) on product measures;
the representation (17) of a tail probability through generalized distribution functions;
a weak-duality argument for a generalized moment problem. The 2008 bound itself is posed on the platform as an open problem under other hypotheses; Corollary 1 states it under this paper's assumptions.

Difficulty

The obvious approach bounds the probability for each value of $s^*_N$ separately by a binomial tail, then sums. This fails: the event $s^*_N=k$ is not known in advance, and summing the individual bounds over $k$ loses the uniformity that makes the result useful. The paper instead characterises every convex problem by the $(d+1)$ -tuple $(F_0,\dots,F_d)$ . It then maximises (17) over all tuples satisfying the infinitely many moment conditions (18), which is a generalized moment problem in $d+1$ measures, and solves it by duality.

Two steps carry most of the work. One is the almost-sure identity $A=B$ , which depends on the precise interplay of Assumptions 1 and 2 with the tie-break. The other is passing from the polynomial dual problems to the variational problem (10), which needs a density argument in $C^d[0,1]$ . The bound $s^*_N\le d$ itself is quoted from the earlier literature; it needs a Helly-type argument adapted to the lexicographic tie-break.

Formalization scope

Spaces. The decision space is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, and samples are Fin N → Δ, indexed from $0$ . $\mathbb P$ is a probability measure and $\mathbb P^N$ is the product measure.
Tie-break. The tie-broken solution is the lexicographic minimiser of $(c^{\mathsf T}x,t_1(x),\dots,t_p(x))$ and depends only on the feasible set, which is what makes the exchangeability step valid. A support constraint is one whose removal changes this solution; this is not the platform's earlier "removal lowers the cost" notion.
Assumptions. Assumption 1 is required for every sample, Assumption 2 almost surely.
Measurability. The paper takes measurability for granted (footnote 1). Here it is two explicit hypotheses: the relation $\{(x,\delta):x\in\mathcal X_\delta\}$ is measurable, and every solution map $\omega\mapsto x^*_m(\omega)$ is measurable. No event is assumed measurable directly.
$F_k$ . $F_k$ is the finite measure on $\mathbb R$ given by the law of $V(x^*_k)$ on the event $\{s^*_k=k\}$ ; it is not normalised.
Problem (10). $C^d[0,1]$ is ContDiffOn ℝ d on $[0,1]$ , with derivatives taken within $[0,1]$ . $\gamma^*$ is a real infimum over a set that is nonempty ( $\xi(t)=t^N$ ) and bounded below by $0$ .
Probabilities are compared with real quantities through ENNReal.ofReal.
Theorem 2 is stated for every $\epsilon$ whose values $1-\epsilon(k)$ are roots of (11) in $(0,1)$ , which by its first part is the paper's $\epsilon$ .
Added hypothesis. The constant- $\epsilon$ companion assumes $d\ge1$ : at $d=0$ , $\epsilon=0$ its inequality is false.

Ruled-out trivializations:

The solution is never a free function of the sample.
The goal does not mention $F_k$ , moments or polynomials.
Assumption 1 is not weakened to almost surely.
$N>d$ is kept on Theorems 1, 2 and Corollary 1.
The indicators keep the paper's open and closed ends: $[0,1-\epsilon(k))$ in (10), $(\epsilon(k),1]$ in (16)–(21).

Contributions welcome:

the support-constraint bound under lexicographic tie-break, which is reusable for any convex scenario result;
the exchangeability lemma on Measure.pi;
the duality and density lemmas, which are pure analysis.

Selected references

M. C. Campi, S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming 167 (2018). https://doi.org/10.1007/s10107-016-1056-9
G. C. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102 (2005). https://doi.org/10.1007/s10107-003-0499-y
G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51 (2006). https://doi.org/10.1109/TAC.2006.875041
M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19 (2008). https://doi.org/10.1137/07069821X

12 thms2 active usersReviewed

Completed

Algorithmic Game Theory Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts VIII: In the Two-Location Base-Stock Model the Linear Transfers (39)–(41) Make the Optimal Base Stocks the Unique Nash EquilibriumTextbook

Motivation

In a supply chain with stock at two locations, a supplier holds inventory that replenishes a retailer, and the retailer serves customers. Each firm sets its own inventory level to minimize its own cost. The retailer bears only part of the cost of customer backorders, and the supplier bears none of the retailer's holding cost, so their incentives differ. The resulting equilibrium generally differs from the policy that minimizes total cost. Cachon and Zipkin (Management Science 45(7), 1999) studied this game and proposed linear transfer payments that align the firms' incentives. In the chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003, doi:10.1016/S0927-0507(03)11006-7), Cachon re-derives that analysis, adds a parameter $\lambda$ that divides the retail-level costs between the firms, and answers two questions the original paper left open: whether the contracts allow an arbitrary division of cost, and whether the optimal policy is the unique equilibrium under the contracts. This mission formalizes the second answer, together with the analysis of the decentralized game and of the optimal policy that it rests on (§6.8 of the 2003 chapter, read in the author's January 2003 draft).

Setting

Two firms, a retailer $r$ and a supplier $s$ , each use a base stock policy: firm $i$ keeps its inventory position equal to its base stock level $s_i \in \mathbb R$ . A negative supplier base stock means planned backorders. Let $D_r$ and $D_s$ be the demands during the retailer's and the supplier's lead times. They are nonnegative with finite means $\mu_r$ , $\mu_s$ , and their distribution functions $F_r$ , $F_s$ are continuous, zero at $0$ , strictly increasing on $[0,\infty)$ and differentiable on $(0,\infty)$ . Holding costs are $h_r$ and $h_s$ , with $0 < h_s < h_r$ . Each backorder at the retailer costs the retailer $\beta_r > 0$ and the supplier $\beta_s > 0$ per unit time. Write $\beta = \beta_r + \beta_s$ .

At retailer inventory level $y$ the expected on-hand stock is $I_r(y) = E[(y-D_r)^+]$ and the expected backorders are $B_r(y) = E[(D_r-y)^+]$ . The retail-level cost rates are $c_r(y) = h_rI_r(y) + \beta_rB_r(y)$ , $c_s(y) = \beta_sB_r(y)$ and $c(y) = c_r(y) + c_s(y)$ . Because the supplier may stock out, the retailer's actual inventory level is $s_r - (D_s - s_s)^+$ , and every retail-level quantity is averaged accordingly:

g(s_r,s_s) = E\big[g(s_r - (D_s-s_s)^+)\big] = F_s(s_s)g(s_r) + \int_{s_s}^\infty g(s_r+s_s-x)f_s(x)\,dx .

With the supplier's inventory $I_s(y) = E[(y-D_s)^+]$ and backorders $B_s(y) = \mu_s - y + I_s(y)$ , the firms' costs and the chain's cost are

\pi_r(s_r,s_s) = c_r(s_r,s_s), \qquad \pi_s(s_r,s_s) = h_sI_s(s_s) + c_s(s_r,s_s), \qquad \Pi = \pi_r + \pi_s .

A pair $\{s_r^o, s_s^o\}$ minimizing $\Pi$ is an optimal policy. A Nash equilibrium is a pair from which neither firm can lower its own cost by a unilateral change of its base stock.

Under a linear transfer the supplier pays the retailer $t_II_r(s_r,s_s) + t_B^rB_r(s_r,s_s) + t_B^sB_s(s_s)$ (a negative amount is a payment the other way). The Cachon–Zipkin contracts with parameter $\lambda \in (0,1]$ are

t_I = (1-\lambda)h_r, \qquad t_B^r = \beta_r - \lambda\beta, \qquad t_B^s = \lambda h_s\frac{F_s(s_s^o)}{1-F_s(s_s^o)} .

Formalization targets

Goal: the contracts coordinate, uniquely

If $\{s_r^o, s_s^o\}$ is optimal with $s_s^o > 0$ and $\lambda \in (0,1]$ , then under the contracts

\pi_r = \lambda c(s_r,s_s) - t_B^sB_s(s_s), \qquad \pi_s = (h_s+t_B^s)I_s(s_s) + (1-\lambda)c(s_r,s_s) + t_B^s(\mu_s - s_s),

$\{s_r^o, s_s^o\}$ is a Nash equilibrium, and it is the only one. The goal contains no numerical constants. It holds for every demand distribution in the class and every $\lambda$ in the range.

Milestones

In the uncontracted game, every retailer best response exceeds $\hat s_r > 0$ , where $F_r(\hat s_r) = \beta_r/(h_r+\beta_r)$ , and every supplier best response is positive (pp. 79–80).
In the uncontracted game, for every $s_s$ the retailer's optimal base stock is below the chain's; consequently the competition penalty $(\Pi(s^*) - \Pi(s^o))/\Pi(s^o)$ is positive at every equilibrium $s^*$ (pp. 80–81).
The partial derivatives (35)–(36) of $\Pi$ , and every optimum with $s_s > 0$ satisfies $c'(s_r) = h_s$ , i.e. $F_r(s_r) = (h_s+\beta)/(h_r+\beta)$ (37) (p. 83).
Optima with $s_s \le 0$ have $s_r + s_s = \bar s$ , where $\Pr(D_r + D_s \le \bar s) = \beta/(h_r+\beta)$ (38) (p. 83).
The cost identities (42)–(43) under the contracts (p. 84).
Under the contracts the retailer's best response decreases in $s_s$ , and the supplier's marginal cost along it has the closed form printed on p. 84.

Significance

The goal says that a contract built from quantities both firms can measure, namely the retailer's inventory and backorders and the supplier's backorders, makes the system-optimal policy the only equilibrium. The firms therefore reach the optimum without coordinating on an equilibrium. The parameter $\lambda$ splits the retail-level costs between the firms in any proportion up to $\lambda = 1$ . Milestone 2 shows the contract is needed: without transfers, decentralization is always strictly suboptimal when the supplier is charged for retail backorders. The transfers $t_I$ and $t_B^r$ are those of the single-location model (§6.7), even though the retailer's target fractile changes from $\beta/(\beta+h_r)$ to $(\beta+h_s)/(\beta+h_r)$ .

The results are proved in the source and in Cachon and Zipkin (1999), with informal derivative arguments. No machine-checked version is known. Formalizing them requires differentiating expectations of piecewise-linear convex functions of a random lead-time shortfall. The page's argument also assumes densities, which the formal statements avoid, and contains several printing slips (see below). These would be settled by a complete development.

Difficulty

The firms' costs are compositions: a convex single-location cost evaluated at the random level $s_r - (D_s - s_s)^+$ , which is concave in $s_s$ . The supplier's cost is therefore not obviously convex in $s_s$ ; its convexity at $s_r = s_r^o$ depends on the value of $t_B^s$ and on $c'(s_r^o) = h_s$ . Uniqueness is the hard part. Under the contracts the retailer's best response $s_r(s_s)$ decreases, but the supplier's marginal cost along that best response, $F_s(s_s)(h_s - (1-\lambda)c'(s_r(s_s)) + t_B^s) - t_B^s$ , is not monotone in general when $\lambda$ is small, contrary to a literal reading of p. 84. A uniqueness argument has to show that it has at most one zero, not that it increases.

Formalization scope

Demand laws are probability measures on $\mathbb R$ with no mass below $0$ , finite means, and continuous distribution functions, zero at $0$ , strictly increasing on $[0,\infty)$ and differentiable on $(0,\infty)$ . These are the section's standing assumptions, together with $0 < h_s < h_r$ and $\beta_r, \beta_s > 0$ (footnote 34 excludes the zero cases). Expectations are Lebesgue integrals: $I_r$ , $B_r$ , $I_s$ and the two-location averages are defined by expectation, and the page's integral forms are consequences. Integrals against $f_s(x)\,dx$ are written against the law of $D_s$ , so no density hypothesis is made. Base stocks range over all of $\mathbb R$ , and "optimal" means minimizing $\Pi$ over $\mathbb R^2$ ; the existence of an optimum is a hypothesis, as on p. 77. Derivatives are stated with HasDerivAt. Independence of $D_r$ and $D_s$ , implicit on the page, enters only through the convolution of their laws in (38).

The contracted costs are defined from the firms' original costs and the transfer payment. Defining them by the closed forms (42)–(43) would make the identities trivial and is ruled out.

Corrected slips: (42) is stated with $\lambda c(s_r,s_s)$ where the page prints $\lambda\Pi(s_r,s_s)$ (the difference $\lambda h_sI_s(s_s)$ does not depend on $s_r$ ). The retailer's single-location fractile on p. 79 is stated as $\beta_r/(h_r+\beta_r)$ , not the printed $\beta/(h_r+\beta)$ . The garbled display after (43) and the $f_s$ / $F_s$ slip in the best-response derivative are not reproduced. Not included: the contraction condition (34), the case split for the optimal policy (p. 84), the case $s_s^o \le 0$ , and the alternative schemes of §6.8.5 (Lee–Whang, Chen). Contributions of those, or of a reusable library for derivatives of $E[g(s - (D-t)^+)]$ , are welcome. The platform's Clark–Scarf items (InventoryControl_clarkScarf, ClarkScarf.Serial.*) concern periodic-review echelon policies and are not reused.

Selected references

G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, vol. 11, North-Holland, 2003, §6.8. https://doi.org/10.1016/S0927-0507(03)11006-7
G. P. Cachon and P. H. Zipkin, Competitive and cooperative inventory policies in a two-stage supply chain, Management Science 45(7), 936–953, 1999. https://doi.org/10.1287/mnsc.45.7.936
F. Chen and Y.-S. Zheng, Lower bounds for multi-echelon stochastic inventory systems, Management Science 40(11), 1426–1443, 1994. https://doi.org/10.1287/mnsc.40.11.1426
A. Federgruen and P. Zipkin, Computational issues in an infinite-horizon, multiechelon inventory model, Operations Research 32(4), 818–836, 1984. https://doi.org/10.1287/opre.32.4.818

10 thms2 active usersReviewed

Discrete Geometry Linear Optimization Number Theory·Captain: mikedeng1

Integer Programming with a Fixed Number of Variables 1: If B(p,r) ⊂ τK ⊂ B(p,R) with R/r ≤ c₁ and τK Misses the Lattice, Fewer Than 1 + c₁c₂√n Lattice Hyperplanes H + kbₙ Meet B(p,R)Research Paper

Motivation

The integer linear programming feasibility problem asks, for an integer $m\times n$ matrix $A$ and $b\in\mathbb Z^m$ , whether some $x\in\mathbb Z^n$ satisfies $Ax\le b$ . It is NP-complete, so no algorithm polynomial in the length of the data is expected. H. W. Lenstra, Jr. (Math. Oper. Res. 8 (1983) 538–548) showed that the picture changes when the number of variables $n$ is fixed: the problem is then solvable in polynomial time. The proof is a short argument from the geometry of numbers, and it became the starting point of lattice methods in integer programming, including Kannan's improved algorithm and the later flatness-based branching schemes.

Lenstra's introduction (p. 538) describes the idea as transforming the problem into an equivalent one in which "either the existence of a vector $x \in \mathbb Z^n$ satisfying $Ax \le b$ is obvious; or it is known that the last coordinate of any such $x$ belongs to an interval whose length is bounded by a constant only depending on $n$ ." This mission formalizes the geometric statement behind that dichotomy, §1 of the paper.

Timeline. For $n = 2$ , Hirschberg and Wong and Kannan gave polynomial algorithms in special cases, and Scarf treated the case $n=2$ completely; the case of general fixed $n$ was conjectured by Hirschberg–Wong and Scarf (as recounted on p. 538). Lenstra's paper (received 1981, published 1983) settled the conjecture. Its lattice reduction step uses the algorithm of Lenstra, Lenstra and Lovász (1982). Kannan (1987) later reduced the dependence on $n$ to $n^{O(n)}$ .

Setting

Work in $\mathbb R^n$ with the Euclidean length $|\cdot|$ , and write $B(p,z)=\{x\in\mathbb R^n : |x-p|\le z\}$ for the closed ball with centre $p$ and radius $z>0$ .

A lattice is $L=\sum_{i=1}^n \mathbb Z b_i$ for a basis $b_1,\dots,b_n$ of $\mathbb R^n$ . Its determinant $d(L)=|\det(b_1,\dots,b_n)|$ (the $b_i$ as columns) is the volume of the parallelepiped $\sum_i[0,1)\,b_i$ and does not depend on the basis. Hadamard's inequality (6) says $d(L)\le\prod_i|b_i|$ . A basis is reduced in Lenstra's sense if, for a constant $c_2$ depending only on $n$ ,

\prod_{i=1}^n |b_i| \le c_2\cdot d(L). \tag{7}

Singling out $b_n$ , let $H=\sum_{i=1}^{n-1}\mathbb R b_i$ be the hyperplane spanned by the other vectors, $L'=\sum_{i=1}^{n-1}\mathbb Z b_i$ the lattice inside it, and $h$ the distance of $b_n$ to $H$ . Then $L\subset\bigcup_{k\in\mathbb Z}(H+kb_n)$ : the lattice lies on a family of parallel hyperplanes $H + kb_n$ at successive distance $h$ .

In the paper, $K=\{x : Ax\le b\}$ is bounded with positive volume, and a linear map $\tau$ makes it "round":

B(p,r)\subset\tau K\subset B(p,R)\quad(3),\qquad R/r\le c_1\quad(4),

with $c_1$ depending only on $n$ . Then $K\cap\mathbb Z^n=\emptyset$ if and only if $\tau K\cap L=\emptyset$ for $L=\tau\mathbb Z^n$ , a lattice with basis $b_i=\tau(e_i)$ .

Formalization targets

Goal (§1, p. 541)

Let $b_1,\dots,b_n$ be a basis with (7), numbered so that $|b_n|=\max_i|b_i|$ , and let $\tau K$ satisfy (3) and (4). Then

\tau K\cap L\neq\emptyset\quad\text{or}\quad t-1<c_1c_2\sqrt n,

where $t$ is the number of hyperplanes $H+kb_n$ , $k\in\mathbb Z$ , that meet $B(p,R)$ (finiteness included).

Milestones, in the order the paper uses them

LEMMA (8), p. 540: every $x$ has $y\in L$ with $|x-y|^2\le\frac14(|b_1|^2+\cdots+|b_n|^2)$ .
(10), p. 540: if $|b_n|$ is maximal, $|x-y|\le\frac12\sqrt n\,|b_n|$ .
(11), p. 540: $d(L)=h\cdot d(L')$ .
(12), pp. 540–541: under (7), $c_2^{-1}|b_n|\le h\le|b_n|$ .
p. 541: if $B(p,r)\subset\tau K$ and $\tau K\cap L=\emptyset$ , then $r<\frac12\sqrt n\,|b_n|$ .
p. 541: if precisely $t$ hyperplanes $H+kb_n$ meet $B(p,R)$ , then $t-1\le 2R/h$ .

The goal leaves $c_1$ and $c_2$ free, so it remains valid for any reduction algorithm and any rounding procedure; the companion mission (Integer Programming with a Fixed Number of Variables 2) supplies $c_1 = 2n^{3/2}$ , and the LLL algorithm supplies $c_2=2^{n(n-1)/4}$ .

Significance

The result. The goal is the branching step of Lenstra's algorithm. It says that a lattice-point-free convex body that is well rounded is "flat" in the lattice direction dual to $H$ : only boundedly many lattice hyperplanes meet it. The search for a lattice point in dimension $n$ therefore reduces to fewer than $1+c_1c_2\sqrt n$ searches in dimension $n-1$ , which with $n$ fixed gives polynomial running time. Sharper forms of the same dichotomy, such as Kannan's bounds, are the basis of later lattice-based integer programming algorithms.

Formalizing it. The results are classical and proved on paper; to our knowledge none of the statements of §1 is machine-checked. Hadamard's inequality (6) is in Mathlib (Orientation.abs_volumeForm_apply_le). The published platform theorem KannanLattice.Core.exists_lattice_point_near_projection (Kannan 1987, Proposition 4.2) proves a stronger form of (8) and (10), with Gram–Schmidt lengths in place of $|b_i|$ ; for $L=\mathbb Z^n$ , (10) is the published QFS.exists_lattice_mem_closedBall. What remains is the "base times height" identity (11) relating a full-rank determinant to the distance of a vector from a hyperplane, the spacing bound (12), the count of hyperplanes meeting a ball, and their assembly. This is one of the two geometric ingredients of Lenstra's polynomial algorithm; the algorithm itself and its running time are not formalized.

Difficulty

The argument is short on paper, and each step is "clear" there. The work lies in connecting three descriptions of the same geometry that Mathlib keeps apart: the determinant of a coordinate matrix ( $d(L)$ ), the metric distance of a point to a subspace ( $h$ ), and the $(n-1)$ -dimensional volume of $L'$ . Identity (11) needs exactly this bridge, and (12) needs Hadamard's inequality for the lower-dimensional lattice $L'$ inside a hyperplane of $\mathbb R^n$ , not for a full-rank matrix. Bounding the number of hyperplanes meeting a ball needs the normal direction of $H$ and the fact that the hyperplanes are $h$ apart along it. A tempting shortcut is to define $h$ as the length of the last Gram–Schmidt vector and $d(L)$ as the product of Gram–Schmidt lengths: that turns (11) into a tautology and is ruled out below.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so norms are Euclidean and balls round; $B(p,z)$ is Metric.closedBall p z with $z>0$ as a hypothesis where the paper writes a ball.
Where $b_n$ is singled out, $n=k+1$ , the basis is b : Fin (k+1) → ℝⁿ, $b_n$ = b (Fin.last k) and $b_1,\dots,b_{n-1}$ = b ∘ Fin.castSucc. "Basis for $L$ " is linear independence of the $n$ vectors over $\mathbb R$ , and $L$ is the published KannanLattice.Core.lattice b, the $\mathbb Z$ -span.
$d(L)$ is the paper's definition, $|\det|$ of the column matrix (latDet). $h$ is Metric.infDist from $b_n$ to the span $H$ . $d(L')$ , for which the paper writes no formula, is the published KannanLattice.Core.latticeDet (the product of Gram–Schmidt lengths of $b_1,\dots,b_{n-1}$ , the $(n-1)$ -volume of their parallelepiped).
The hyperplanes $H+kb_n$ meeting $B(p,R)$ are indexed by the set of integers hitIndices b p R; $t$ is its cardinality, its finiteness is part of every conclusion (the cardinality of an infinite set is $0$ in Lean), and $t-1$ is computed in $\mathbb R$ .
The constants "only depending on $n$ ", $c_1$ and $c_2$ , are arbitrary real numbers. The reducedness (7) is a hypothesis, and so is the maximality $|b_i|\le|b_n|$ , which enters (10), the radius bound and the goal only.
$\tau K$ is an arbitrary set $X\subseteq\mathbb R^n$ satisfying (3); §1 never uses that $K$ is a polyhedron or the map $\tau$ , and every lattice is $\tau\mathbb Z^n$ for $\tau(e_i)=b_i$ . The paper's "for some $p\in\tau K$ " follows from (3).
The identity (11) is stated without (7), which the paper assumes in the surrounding sentence but does not use.
Ruled out: defining $d(L)$ or $h$ through Gram–Schmidt lengths (which makes (11) bookkeeping), dropping finiteness of the hyperplane count, and replacing the dichotomy "some lattice point lies in $\tau K$ " by a statement about one computed lattice point.

Welcome contributions: the bridge between Matrix.det of a basis and products of Gram–Schmidt lengths (reusable for any lattice development), Hadamard's inequality for a family of fewer than $n$ vectors, and the count of lattice hyperplanes meeting a ball.

Selected references

H. W. Lenstra, Jr., Integer Programming with a Fixed Number of Variables, Mathematics of Operations Research 8(4) (1983) 538–548. https://doi.org/10.1287/moor.8.4.538
A. K. Lenstra, H. W. Lenstra, Jr., L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen 261 (1982) 515–534. https://doi.org/10.1007/BF01457454
R. Kannan, Minkowski's convex body theorem and integer programming, Mathematics of Operations Research 12(3) (1987) 415–440. https://doi.org/10.1287/moor.12.3.415

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Optimization·Captain: mikedeng1

Supply Chain Coordination with Contracts V: With Market-Clearing Prices the Best Wholesale Price Earns θ/(2(1 + θ)) or θ/8, Below the (1 + θ)/8 a Full-Refund Buy-Back AttainsTextbook

Motivation

A supplier that sells through many competing retailers usually worries that competition among them pushes orders too high, because each retailer ignores the demand it takes from the others. Deneckere, Marvel and Peck (1997) identified the opposite failure. When the retail price is set by the market after demand is realized, retailers who hold too much stock in a weak market bid the price down, and anticipating this, perfectly competitive retailers order too little. The supplier then needs a contract that raises orders, and the classical justification for resale price maintenance (a price floor imposed on retailers) comes out of this model. G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents the model in §6.5.2 as a closed-form example. In it the supplier's best wholesale price contract is computed explicitly and compared with two contracts that recover the monopoly profit: resale price maintenance and a full-refund buy-back.

This mission is volume V of a series that formalizes the section capstones of that chapter, read in the author's 3rd draft (January 2003), pp. 53–58.

Setting

Fix $\theta>1$ . Industry demand is low or high, each with probability $1/2$ . If the retailers hold a total stock $q$ , the market clearing price is

p_l(q)=(1-q)^+\ \text{(low state)},\qquad p_h(q)=\Big(1-\frac q\theta\Big)^+\ \text{(high state)}.

Leftover inventory has no salvage value, and the supplier's production cost is zero.

Monopolist benchmark. A single firm orders a stock $Q$ , observes the state, and sells $x_l\le Q$ (low) or $x_h\le Q$ (high) at the market clearing price. Its expected profit is $\tfrac12p_l(x_l)x_l+\tfrac12p_h(x_h)x_h$ , and $\Pi^o$ is the maximum of this.
Wholesale price contract. The supplier charges $w$ per unit. A continuum of retailers orders before demand is known and sells everything at the market clearing price. Their aggregate expected profit is

\pi(q)=\tfrac12p_l(q)q+\tfrac12p_h(q)q-wq .

Perfect competition means the retailers keep ordering until expected profit is zero. The competitive order is the $q>0$ with $\pi(q)=0$ and $\pi>0$ on $(0,q)$ . The supplier earns $wq$ .

Resale price maintenance $(\bar p,w)$ : retailers may not sell below $\bar p$ . When the clearing price would fall below $\bar p$ , only the demand at $\bar p$ is sold, allocated in proportion to stock.
Buy-back $(w,b)$ : the supplier pays $b$ per unsold unit. The market price then cannot fall below $b$ , and retailers sell at most $1-b$ units (low) and $\theta(1-b)$ units (high).

The page's notation $q_1(w)=\frac{2\theta}{1+\theta}(1-w)$ , $q_2(w)=\theta(1-2w)$ , $\pi_s(w)$ and $w^*(\theta)$ is kept in Lean under the names q1, q2, supplierProfit, wStar.

Formalization targets

Goal (pp. 55, 57)

With

\pi_s^*=\begin{cases}\dfrac{\theta}{2(1+\theta)}&\theta\le3,\\[4pt]\dfrac\theta8&\theta>3,\end{cases}

the goal states four things:

$\pi_s^*$ is the greatest supplier profit $wq$ over all wholesale prices and their competitive orders.
$w^*(\theta)$ attains it.
The monopolist's maximum is $\Pi^o=(1+\theta)/8$ , and $\pi_s^*<\Pi^o$ .
Under the buy-back $b=w=1/2$ the competitive order is $\theta/2$ and the supplier earns exactly $\Pi^o$ .

Milestones

$\Pi^o=(1+\theta)/8$ (p. 54).
The competitive order is $q_1(w)$ if $w\ge\tfrac12-\tfrac1{2\theta}$ and $q_2(w)$ otherwise, for $0\le w<1$ (p. 55).
$w^*(\theta)$ maximizes $\pi_s$ on $[0,1)$ , with the value $\pi_s^*$ (p. 55).
The orders and market clearing prices at $w^*(\theta)$ (p. 55).
Under resale price maintenance with $\bar p=1/2$ and total stock $\theta/2$ , $\pi_r(t)=q(t)\big(\frac{1+\theta}{4\theta}-w\big)$ (p. 56).
Under $(\bar p,\bar w)$ the competitive order is $\theta/2$ and the supplier earns $\Pi^o$ (p. 57).
Under the buy-back $b=1/2$ the retailers' profit is $q\big(\frac34-w-\frac q{2\theta}\big)$ for $1/2<q<\theta/2$ (p. 57).
$1/2>(1+\theta)/(4\theta)$ (p. 57).

Significance

The goal shows that in this model a wholesale price contract always falls short of the integrated profit, whatever $\theta$ . It also shows where the shortfall comes from: at the optimal wholesale price the low-state market price falls below the monopoly price $1/2$ (milestone 4). Restoring the monopoly profit therefore requires a mechanism that holds the low-state price at $1/2$ . Resale price maintenance and a full-refund buy-back both do this, so the section gives a closed-form efficiency argument for vertical restraints that are often treated as anticompetitive. The section also contrasts the buy-back with revenue sharing, which coordinates the single newsvendor (§6.2) but not this model.

The results are proved on the printed pages by elementary algebra. None of them has a machine-checked proof, and nothing on Prove2Me covers this model. The mission produces checked versions of the case analysis, including the $\theta=3$ tie and the two regimes of the competitive order. It also adds a reusable encoding of "perfect competition" as the first zero of aggregate expected profit.

Difficulty

Every statement reduces to one-variable inequalities, but the case structure is easy to get wrong.

The retailers' profit is piecewise (prices hit zero at $q=1$ in the low state and at $q=\theta$ in the high state). The competitive order lies on either side of $q=1$ depending on $w$ .
The supplier's profit $\pi_s$ is piecewise in $w$ , and its second branch peaks at $w=1/4$ only when $\theta>2$ .
The global optimum switches at $\theta=3$ , where both prices are optimal.
A statement "the competitive order is $q_1(w)$ " needs the order to exist, to be unique, and to have positive profit everywhere below it. Exhibiting a root is not enough.
The buy-back profit is identically zero for $q\ge\theta/2$ when $b=w=1/2$ . Only the "first zero" reading of perfect competition pins the order at $\theta/2$ .

Formalization scope

All quantities are real numbers and $\theta>1$ throughout. The continuum of retailers enters only through the total order. No measure space of retailers is formalized, and footnote 26's multiplicity of individual equilibria is not stated. The sales rules under resale price maintenance (proportional allocation) and under the buy-back (price floor $b$ ) are written into the contract definitions, as the page describes them in words. The theorems use only $\bar p=b=1/2$ .

The formulas $q_1$ , $q_2$ , $\pi_s$ and $w^*$ are definitions transcribed from the page. That they are the competitive order and the optimum is the content of the theorems. Defining $\Pi^o$ or the competitive order by its closed form would trivialize the mission, so the competitive order is defined only by the zero-profit property and $\Pi^o$ as a greatest element of the monopolist's feasible profits. The goal is stated over all real wholesale prices, so it also rules out profitable prices outside $[0,1)$ . Uniqueness of $w^*(\theta)$ is not asserted at $\theta=3$ .

The chapter's standing assumptions used here are risk neutrality and full information, together with the model paragraph of pp. 53–54 (two equally likely states, zero salvage value, zero production cost). No platform definition is referenced: no published item formalizes this model.

Selected references

G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves, T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, §6.5.2 (3rd draft, January 2003, pp. 53–58). https://doi.org/10.1016/S0927-0507(03)11006-7
R. Deneckere, H. P. Marvel, J. Peck, Demand Uncertainty and Price Maintenance: Markdowns as Destructive Competition, American Economic Review 87(4), 619–641, 1997. https://www.jstor.org/stable/2951366
R. Deneckere, H. P. Marvel, J. Peck, Demand Uncertainty, Inventories, and Resale Price Maintenance, Quarterly Journal of Economics 111(3), 885–913, 1996. https://doi.org/10.2307/2946675

11 thms2 active usersReviewed

Discrete Geometry Linear Optimization·Captain: mikedeng1

On Linear Characterizations of Combinatorial Optimization Problems III: Zero-One and Integer-Programming-Type Problems Have Small Facial DescriptionsResearch Paper

Motivation

Many discrete optimization problems can be described by linear inequalities, even when their feasible solutions are integer vectors. A linear description lets one study the geometry of the feasible set and connect combinatorial methods with linear programming. The number of inequalities may be large, so a more basic question is whether each inequality needs coefficients of manageable size. Karp and Papadimitriou separated this coefficient-size issue from the number and computational recognizability of the inequalities in their study of facial descriptions Karp and Papadimitriou, MIT/LCS/TM-154, pp. 3–7.

Their Lemma 1 identifies two common families for which small coefficients suffice: zero-one problems and problems given by an integer linear system. This result establishes a geometric premise used by the paper's later complexity discussion. It says nothing by itself about finding the inequalities efficiently or recognizing whether a proposed inequality belongs to a description. Those computational conditions belong to the paper's subsequent theorems Karp and Papadimitriou, pp. 5–8.

Setting

A combinatorial optimization problem here consists of a set $L$ of binary strings, a dimension $n(z)$ for each $z\in L$ , and a set $S(z)$ of feasible nonnegative integer vectors of that dimension. The geometric object is the rational convex hull $\mathrm{CH}(S(z))\subseteq\mathbb Q^{n(z)}$ . The paper calls the rationals $R$ in its notation. The values of $n$ and $S$ outside $L$ carry no meaning. A feasible set may be empty; its convex hull is then empty as well Karp and Papadimitriou, Definition 1 and footnote, p. 3.

A facial description $F$ is a collection of triples $\langle z,f,g\rangle$ , where $z\in L$ , $f\in\mathbb Z^{n(z)}$ , and $g\in\mathbb Z$ . For every rational vector $x$ and every $z\in L$ , membership in $\mathrm{CH}(S(z))$ must be equivalent to satisfying all inequalities $f\cdot x\le g$ indexed by triples of $F$ with first component $z$ . A facial description is small when one polynomial in $|z|+n(z)$ bounds the binary size of every coefficient of every triple in the collection. The collection itself need not be small Karp and Papadimitriou, pp. 4–5.

A zero-one problem has only vectors with entries zero or one in each $S(z)$ . An integer-programming-type problem gives an integral matrix $A(z)$ and right-hand side $b(z)$ and takes $S(z)$ to be all nonnegative integer vectors satisfying $A(z)x\le b(z)$ . The dimensions of these data depend on $z$ . Their total binary coefficient size is controlled by the length of the encoded input Karp and Papadimitriou, pp. 5–6.

Formalization targets

Lemma 1

The mission goal is the complete statement for both classes:

\forall C,\quad \bigl(\operatorname{ZeroOne}(C)\lor\operatorname{IPType}(C)\bigr) \Longrightarrow \exists F,\quad \operatorname{FacialDescription}(C,F)\land\operatorname{Small}(C,F).

The milestone list records three claims used in the paper's proof. In a zero-one hull, every vertex is a zero-one vector and there are no nonzero rays. For integer hulls, the cited vertex-size result gives a uniform polynomial bound on the coordinates of vertices. Finally, the Cramer's-rule calculation bounds an integral normal $f$ and intercept $g$ by $(2nx)^n$ when the geometric data have coordinates bounded by $x$ Karp and Papadimitriou, pp. 5–7.

Significance

Lemma 1 permits descriptions of the whole hull, including lower-dimensional hulls that require equations and unbounded integer hulls that have recession directions. It gives a coefficient bound for every input with one polynomial, rather than a polynomial chosen separately for each instance. This is the premise needed when the paper treats a facial description as a language of short encodable inequalities. The later assertion that an NP-recognizable small facial description places the decision problem in co-NP has a distinct hypothesis and is handled by the first mission of this series Karp and Papadimitriou, Theorem 1, pp. 7–8.

The mathematical result is known; the mission asks for a Lean proof of its precise rational, input-indexed version. The local declarations are proof obligations and do not yet carry verified proofs. Existing platform work includes a rational integer-hull definition reused here, a related open theorem of Cook–Gerards–Schrijver–Tardos that bounds normal coefficients under different hypotheses, and proved real-carrier versions of Meyer's polyhedrality and finite-generation results. The related open theorem does not supply Lemma 1: it has neither this zero-one case nor the bound on the intercept $g$ . The real-carrier theorems supply neither the input-size bound nor the paper's rational convention.

Difficulty

The zero-one case has bounded coordinates, but a complete description must also handle an empty hull and a hull contained in a proper affine subspace. Bounding only the facet inequalities of a full-dimensional nonempty polytope does not describe those cases. The integer-programming case adds unbounded directions, and the paper's printed identification of extreme rays with rows of $A$ is false. A faithful treatment must bound suitable recession directions and then obtain a uniform coefficient bound for the inequalities describing the hull Karp and Papadimitriou, pp. 5–7.

Formalization scope

The Lean model uses List Bool for inputs, Fin (n z) → ℤ for feasible vectors, and Fin (n z) → ℚ for the convex hull. The published CookSensitivity.ChvatalRank.polyhedron and integerHull definitions provide the general rational integer-programming substrate. This mission adds only the paper's input-indexed problem, facial description, smallness condition, and two named problem classes. The three language-recognition requirements in the paper's Definition 1 are omitted because Lemma 1 never uses them; the resulting theorem applies to every such geometric problem, including every c.o.p. in the paper's narrower definition.

The polynomial bound is represented by $(|z|+n(z))^k+k$ with a single natural exponent $k$ chosen before every input and inequality. For an integer-programming-type input, the sum $s(A,b)=\sum_a\lceil\log_2(1+|a|)\rceil$ over all entries of $A$ and $b$ must be at most $|z|$ . This makes the paper's phrase “ $z$ specifies $A$ and $b$ ” an explicit binary-size condition. The cited vertex milestone bounds coordinates in terms of $s$ alone, as the page states: a zero column gives a line direction rather than a vertex. Its statement follows the paper's unrestricted $Ax\le b$ formulation; the IP-type goal additionally imposes $x\ge0$ . The paper calls $b$ an $n$ -vector, but it has one entry per row of $A$ and is an $m$ -vector here. The Cramer's-rule milestone allows rows of size $2x$ , as vertex differences can reach that size.

Empty feasible sets, dimension zero, lower-dimensional hulls, and unbounded IP hulls remain in the goal. A description restricted to full-dimensional facets, or a smallness exponent chosen separately for each input, would not meet it. A complete development needs rational convex hulls, integer-hull geometry, finite descriptions of rational polyhedra, bounds on vertices and recession generators, and finite-dimensional determinant estimates. The rational integer-hull definitions and the coefficient estimates are reusable beyond this mission; contributions that establish the three listed milestones or the remaining geometric steps are in scope.

Selected references

Richard M. Karp and Christos H. Papadimitriou, On Linear Characterizations of Combinatorial Optimization Problems, MIT/LCS/TM-154, February 1980, pp. 3–7. Report scan. Later published in SIAM Journal on Computing 11 (1982), 620–632, DOI.

6 thms2 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts III: With Effort-Dependent Demand, Buy-Backs, Quantity Flexibility and Revenue Sharing Under-Reward Effort, While a Quantity Discount Gives λΠ(q, e°)Textbook

Why effort breaks the standard coordinating contracts

A supplier selling through a retailer earns more when the retailer works harder at selling. Examples are a better shelf position, more knowledgeable sales staff, local advertising and keeping the display in order. These activities cost the retailer, raise demand, and usually cannot be observed or verified by the supplier, so no contract can be written on them directly. Chapter 6 of the Handbook of Operations Research and Management Science, Vol. 11: Supply Chain Management (G. P. Cachon, Supply Chain Coordination with Contracts, 2003) surveys contracts that align a retailer's decisions with the interest of the whole supply chain. Its §6.4 asks which of these contracts survive when the retailer also chooses such an unverifiable effort level.

The question goes back to the marketing literature on retail effort (Chu and Desai 1995, Desai and Srinivasan 1995, Desiraju and Moorthy 1997, Lal 1990, Lariviere and Padmanabhan 1997). It was taken up for newsvendor contracts by Taylor (2000), who showed that a sales rebate combined with a buy back restores coordination, and by Krishnan, Kapuscinski and Butz (2001), who let effort be chosen after demand is observed. This mission is the third in a series that formalizes the chapter's section capstones. It covers §6.4.1.

The newsvendor with effort-dependent demand

One supplier sells to one retailer for a single selling season. Before the season the retailer chooses an order quantity $q \ge 0$ and an effort level $e \ge 0$ . Effort costs him $g(e)$ , where $g(0) = 0$ , $g' > 0$ and $g'' > 0$ . Demand $D$ given effort $e$ has distribution function $F(\cdot \mid e)$ on $[0, \infty)$ , with $F(0 \mid e) = 0$ and $F(\cdot \mid e)$ strictly increasing. Demand is stochastically increasing in effort: $\partial F(y \mid e)/\partial e < 0$ for $y > 0$ . Units sell at the retail price $p$ and cost $c < p$ to produce. Goodwill costs, the salvage value and the retailer's own unit cost are zero. Expected sales and the integrated channel's profit are

S(q, e) = \mathbb E[\min(q, D)] = q - \int_0^q F(y \mid e)\,dy, \qquad \Pi(q, e) = pS(q, e) - cq - g(e).

Let $(q^o, e^o)$ maximize $\Pi$ . A contract fixes the transfer the retailer pays the supplier, as a function of what the supplier can verify: the order and, for some contracts, sales or leftover units, but never effort. The contracts compared are the buy back $\{w_b, b\}$ , quantity flexibility $\{w_q, \delta\}$ , revenue sharing $\{w_r, \phi\}$ , the sales rebate $\{w_s, r, t\}$ and the quantity discount $w_d(q)$ . Under each, the retailer's profit $\pi_r(q, e)$ is his revenue $pS(q, e)$ less the transfer and $g(e)$ .

Formalization targets

Goal

The goal combines the section's negative and positive results.

Buy backs distort effort (Eq. (19)). For every $b > 0$ , $q > 0$ and $e > 0$ ,

\frac{\partial \pi_r(q, e, w_b, b)}{\partial e} < \frac{\partial \Pi(q, e)}{\partial e}.

The quantity discount aligns effort and splits profit. With

w_d(q) = (1 - \lambda)p\,\frac{S(q, e^o)}{q} + \lambda c - (1 - \lambda)\frac{g(e^o)}{q}, \qquad \lambda \in [0, 1],

the following hold for every $q > 0$ . The retailer earns $\pi_r(q, e^o) = \lambda\Pi(q, e^o)$ and the supplier earns $(1 - \lambda)\Pi(q, e^o)$ . The retailer's marginal profit of effort equals the channel's. His optimal efforts are the channel's. 3. The optimal order. If $(q^o, e^o)$ maximizes $\Pi$ , both firms' profits at effort $e^o$ are maximized by $q^o$ .

Milestones

The milestones follow the section's own claims: the integral form of $S$ (p. 41); the first-order condition (18) for the chain-optimal effort; (19); the analogous strict inequalities for quantity flexibility ( $\delta > 0$ ) and revenue sharing ( $\phi < 1$ ), and the reverse inequality for the sales rebate ( $r > 0$ , $q > t$ ); the two displays of $\pi_r$ under the quantity discount; and the fact that $S(q, e)/q$ decreases in $q$ .

Significance

The result separates two jobs a contract does. To coordinate the order quantity, buy backs, quantity flexibility and revenue sharing all shield the retailer from part of the demand risk or take part of his revenue. The same shield dulls his incentive to raise demand, so each one leads him to under-invest in effort. The sales rebate pushes the other way, toward too much effort. The quantity discount works because the retailer keeps every unit of realized revenue and bears all of his own effort cost. The schedule then prices the order against expected revenue at the optimal effort, so the order is coordinated without touching the effort incentive. Because $\pi_r(q, e^o) = \lambda\Pi(q, e^o)$ with $\lambda$ free in $[0, 1]$ , any split of the channel's optimal profit is attainable. The chapter extends this observation to retailers that also set price (p. 43).

The section's claims are proved on the page only in outline; several are introduced with "it can be shown". To our knowledge none has a machine-checked proof. Formalizing them requires differentiating expected sales in a parameter of the demand law. That step recurs throughout stochastic inventory and pricing models.

Difficulty

Most of the algebra is short. The substance is in the derivatives. $\partial S(q, e)/\partial e = -\int_0^q \partial F(y \mid e)/\partial e\,dy$ is a differentiation under the integral sign. The strict inequalities need this integral to be strictly negative. That in turn needs $\partial F/\partial e$ to be integrable and negative on a set of positive length, which is why $q > 0$ (and $q > t \ge 0$ for the sales rebate) matters.

The natural reading "the quantity discount makes $(q^o, e^o)$ the retailer's joint optimum" is not what the page shows, and it fails in general. The page gives two partial statements: for each fixed $q$ the retailer's effort incentive is the chain's, and at $e = e^o$ his best order is $q^o$ . Since $\pi_r(q, e) = \Pi(q, e) - (1 - \lambda)\Pi(q, e^o)$ , the retailer can gain by moving $q$ and $e$ together when $\lambda$ is small. The goal states exactly the two partial claims.

Formalization scope

The Lean namespace is CachonCoord.EffortNewsvendor. A structure Model collects the data: $p$ and $c$ with $0 \le c < p$ ; a family of demand laws indexed by effort (probability measures on $[0, \infty)$ with finite mean, no atom at $0$ , strictly increasing distribution function); the effort derivative $\partial F(y \mid e)/\partial e$ , negative for $y > 0$ , $e > 0$ ; and $g$ with $g(0) = 0$ and positive first and second derivatives for $e > 0$ . $S$ is defined as an expectation, and its integral form is a milestone. Derivative claims are HasDerivAt statements at interior efforts $e > 0$ . The inequalities assert that both derivatives exist.

The following hypotheses are standing assumptions or disclosed additions:

the chapter's model paragraph (p. 7) and the zeros $g_r = g_s = v = c_r = 0$ of p. 41;
as regularity, differentiation of $e \mapsto \int_a^b F(y \mid e)\,dy$ under the integral sign, with interval-integrable $\partial F/\partial e$ ;
$0 \le c$ (a production cost);
$w_q > 0$ and $\delta \le 1$ for quantity flexibility (the contract's range, p. 24);
$t \ge 0$ for the sales rebate threshold;
$q > 0$ wherever $w_d$ , which divides by $q$ , is used.

Revenue sharing and the sales rebate use §6.2's profit functions (pp. 21, 27) with this section's zeros, less $g(e)$ .

The page prints the last term of $w_d$ as $+(1 - \lambda)g(e^o)/q$ . With that sign the page's own displays $\pi_r(q, e^o) = \lambda\Pi(q, e^o)$ and $\pi_r(q, e)$ fail by $2(1 - \lambda)g(e^o)$ . The formalization uses $-(1 - \lambda)g(e^o)/q$ , under which both hold. $w_d$ is the explicit printed schedule with this correction. It is not defined as "a schedule with $\pi_r = \lambda\Pi$ ", which would make the goal empty.

Not covered: the price-and-effort schedule at the bottom of p. 43, for which the page gives no argument. The cachon-2005 revenue-sharing effort results (RevShareCoord.Effort.*, deterministic revenue $R(q, e)$ ) are a different model and are not referenced. Proofs of any milestone, and a reusable library for differentiating newsvendor expectations in a parameter, are welcome.

Selected references

G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, Ch. 6. https://doi.org/10.1016/S0927-0507(03)11006-7 (read in the author's 3rd draft, January 2003).
T. A. Taylor, Supply Chain Coordination under Channel Rebates with Sales Effort Effects, Management Science 48(8), 2002, 992–1007. https://doi.org/10.1287/mnsc.48.8.992.168
H. Krishnan, R. Kapuscinski, D. A. Butz, Coordinating Contracts for Decentralized Supply Chains with Retailer Promotional Effort, Management Science 50(1), 2004, 48–63. https://doi.org/10.1287/mnsc.1030.0154
G. P. Cachon, M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, Management Science 51(1), 2005, 30–44. https://doi.org/10.1287/mnsc.1040.0215

11 thms2 active usersReviewed

Completed

Optimization·Captain: mikedeng1

Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments VI: Revenue-Ordered Offer Sets Grow with Capacity Left and Shrink with Time LeftResearch Paper

Motivation

In airline and hotel revenue management a firm sells a fixed stock of a perishable resource (seats on a flight leg, rooms on a night) over a finite selling horizon, and in each period decides which fare classes to open. Customers do not buy a fixed fare: they choose among the fares on offer, or leave. Talluri and van Ryzin (Management Science, 2004) formulated this single-leg, choice-based problem as a dynamic program over the time remaining and the units remaining.

Practical revenue management systems rarely offer arbitrary sets of fares. They use nested controls: fares are opened from the most expensive downwards, so the open set is always "every fare above some threshold". Whether restricting to such revenue-ordered offer sets is natural depends on how the optimal threshold moves as the state changes. For mixtures of multinomial logit models, Rusmevichientong, Shmoys, Tong and Topaloglu (Production and Operations Management, 2014, Theorem 6) showed that the best revenue-ordered threshold moves monotonically in both the remaining capacity and the remaining time.

Berbeglia and Joret (arXiv:1606.01371v3, §5, Theorem 5.1) extend these two monotonicity properties to every regular discrete choice model, the class that contains essentially every model used in revenue management, including all random utility models. This mission formalizes that result.

Setting

A finite nonempty set $\mathcal C$ of products is sold. For a choice set $S\subseteq\mathcal C$ and a product $x$ , $\mathcal P(x,S)$ is the probability that a customer offered $S$ buys $x$ ; the no-purchase probability is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ . The system $\mathcal P$ is regular when (i) all these probabilities are nonnegative, (ii) $\mathcal P(x,S)=0$ for $x\notin S$ , (iii) $\sum_{x\in S}\mathcal P(x,S)\le 1$ , and (iv) $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$ , for every $x\in S$ and for the no-purchase option $x=0$ .

Each product $x$ has a revenue $r(x)>0$ . Let $r_1<r_2<\cdots<r_k$ be the distinct revenues. For $\ell\in[k]=\{1,\dots,k\}$ the revenue-ordered assortment is $S_\ell=\{x\in\mathcal C:r(x)\ge r_\ell\}$ ; a larger index $\ell$ gives a smaller set, $S_1=\mathcal C$ .

In the multi-period model one customer arrives per period. With $t$ periods remaining and $q$ units left, the firm offers some $S_\ell$ . The values of the revenue-ordered dynamic program are

\mathcal J_t(q,\ell)=\sum_{x\in S_\ell}\mathcal P(x,S_\ell)\bigl(r(x)+\mathcal J_{t-1}(q-1)\bigr)+\mathcal P(0,S_\ell)\,\mathcal J_{t-1}(q)\qquad(t,q>0),

$\mathcal J_t(q,\ell)=0$ when $t=0$ or $q=0$ , and $\mathcal J_t(q)=\max_{\ell\in[k]}\mathcal J_t(q,\ell)$ . The optimal revenue-ordered index is the smallest maximiser,

\ell^*_t(q)=\min\{\ell\in[k]:\mathcal J_t(q,\ell)=\mathcal J_t(q)\},

and $\Delta\mathcal J_t(q)=\mathcal J_t(q)-\mathcal J_t(q-1)$ is the marginal value of capacity.

Formalization targets

Goal: Theorem 5.1

For every $t\ge 1$ and $q\ge 1$ ,

\ell^*_t(q)\le\ell^*_t(q-1)\ \text{ if } q\ge 2,\qquad \ell^*_t(q)\ge\ell^*_{t-1}(q)\ \text{ if } t\ge 2 .

More units left give a weakly larger optimal offer set; more periods left give a weakly smaller one. The paper states the theorem for $t\in[T]$ , $q\in[Q]$ ; the horizon and the capacity only bound $t$ and $q$ , so the goal is stated for all $t,q\ge 1$ .

Milestones

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'$ .
Lemma .1 (p. 35): with $\mathcal L^*(\delta)$ the set of indices $\ell$ maximising $\sum_{x\in S_\ell}\mathcal P(x,S_\ell)(r(x)+\delta)$ , if $\delta_1+r_k\ge 0$ and $\delta_1\le\delta_2$ then $\min\mathcal L^*(\delta_2)\le\min\mathcal L^*(\delta_1)$ .
Equation (16) (p. 36): $\mathcal J_t(q)=\max_{\ell}\sum_{x\in S_\ell}\mathcal P(x,S_\ell)(r(x)-\Delta\mathcal J_{t-1}(q))+\mathcal J_{t-1}(q)$ .
Equations (17)–(18) (p. 36): $\ell^*_t(q)=\min\mathcal L^*(-\Delta\mathcal J_{t-1}(q))$ .
Marginal value at most $r_k$ (p. 36): $\Delta\mathcal J_t(q)\le r_k$ .
Marginal value non-increasing in capacity (p. 36, citing Talluri–van Ryzin, Lemma 4): $\Delta\mathcal J_t(q+1)\le\Delta\mathcal J_t(q)$ .
Marginal value non-decreasing in time (p. 37, citing Talluri–van Ryzin, Lemma 5): $\Delta\mathcal J_t(q)\le\Delta\mathcal J_{t+1}(q)$ .

Milestones 5–7 are asserted or cited in the paper, not proved there; milestones 6–7 are stated for this restricted dynamic program, which is the one the paper applies them to.

Significance

The theorem says that a firm restricted to revenue-ordered offer sets can implement its policy as a nested booking control: as seats sell out, the threshold fare can only rise, and as departure approaches with seats in hand, it can only fall. This is the structure that standard revenue management systems already assume, and Rusmevichientong et al. point out that such monotonicity can be used to implement them. The paper's contribution is that the property depends only on regularity of the choice model, not on its multinomial-logit form.

Formalizing it adds a machine-checked statement of the single-leg choice-based dynamic program over a general choice model, a precise account of the tie-breaking rule (the smallest maximiser), and machine-checked versions of the two marginal-value monotonicity facts that the paper cites from Talluri and van Ryzin rather than proves. To our knowledge none of these statements has been formalized in any proof assistant; the paper's proofs are informal.

Difficulty

The paper's proof is short, but two of its steps are not proved there. The marginal-value inequalities are imported from Talluri and van Ryzin, whose dynamic program optimises over all offer sets; here only the $k$ revenue-ordered sets are available and the empty set is not, so those proofs have to be redone for this program, and the bound $\Delta\mathcal J\le r_k$ is needed to keep each stage's shifted problem well behaved. The claim $\Delta\mathcal J\le r_k$ itself is justified on the page only by an informal sentence.

The second subtlety is tie-breaking. The monotonicity is about the smallest optimal index. Several indices can be optimal at once, and the comparison of Lemma .1 transfers optimality of one index from one shift to another only through Lemma 2.1, that is, through the no-purchase case of the regularity axiom. Without that case the statement fails.

Formalization scope

Products form a finite nonempty type C; choice probabilities are P : C → Finset C → ℝ, defined on all pairs. The no-purchase option is not a product: its probability is the derived quantity noPurchase P S = 1 − ∑_{x∈S} P x S.
IsChoiceSystem P is axioms (i)–(iii); IsRegular P adds axiom (iv) for products and for the no-purchase option. Milestones 5–7 assume only axioms (i)–(iii), as the paper says suffices; Lemma .1, (16), (18) and the goal assume regularity and $r>0$ .
Revenue levels use the paper's 1-based index: level r ℓ is $r_\ell$ for $1\le\ell\le k$ , topRevenue r is $r_k$ , and roSet r ℓ is $S_\ell$ as a Finset. The paper's sorting of products ( $S_\ell=\{1,\dots,j(\ell)\}$ ) is notation only and is not used.
The dynamic program is defined by structural recursion on $t$ ; there is no stochastic process. Maxima over $[k]$ are Finset.sup', and the minima defining $\ell^*_t(q)$ and $\min\mathcal L^*(\delta)$ are Finset.min' over sets proved nonempty.
$\Delta\mathcal J_t(q)$ is used only for $q\ge 1$ ; milestones are stated with $t+1$ , $q+1$ in place of the paper's $t-1$ , $q-1$ to avoid natural-number subtraction, which the goal keeps under its hypotheses $q\ge 2$ , $t\ge 2$ .

Formalizations that would trivialize the statement are ruled out: the dynamic program maximises over the $k$ revenue-ordered sets only, never over all subsets (that is Talluri and van Ryzin's program); $\ell^*$ is the smallest maximiser, never the largest; and $T$ , $Q$ , $k$ and the choice model are arbitrary, never fixed.

The definitions (regular choice model, revenue-ordered assortments, the restricted dynamic program) are reusable for other results on nested policies. Proofs of the cited Talluri–van Ryzin lemmas for this program are especially welcome, as they are the part the paper leaves to the literature.

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.01371
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

14 thms2 active usersReviewed

Completed

Graph Theory Linear Optimization Optimization·Captain: mikedeng1

Finding Minimum-Cost Circulations by Successive Approximation I: The Generic Refine Subroutine Stops Within 3n(n − 1) + 3nm + 3n²(m + n) Update Operations at an ε-Optimal CirculationResearch Paper

Motivation

Minimum-cost circulation asks how to route flow around a directed network without accumulating flow at any vertex, while minimizing the total cost of the routed units. It is a basic network optimization problem: lower-bound and demand constraints in many flow models can be converted into circulation form. Goldberg and Tarjan's 1987 technical report develops a successive-approximation approach in which a local repair subroutine, refine, improves an approximately optimal circulation. The report was followed by a 1990 journal article; all theorem numbers and page citations in this mission refer to the 1987 report.

The mission isolates the generic form of refine, where an implementation may choose any applicable update at each step. Its question is whether every such choice sequence finishes after a controlled number of operations and returns a circulation with a stronger optimality certificate. The related Goldberg–Tarjan maximum-flow algorithm uses push and relabel operations with distance labels; here the labels are real-valued prices tied to arc costs. The authors' cycle-canceling work uses the same circulation network model and supplies published definitions reused in this development.

Setting

A circulation network has a finite vertex set $V$ and a symmetric set $E$ of directed arcs: whenever $(v,w)$ is an arc, so is $(w,v)$ . Let $n=|V|$ and $m=|E|$ , counting both orientations. Each arc has a real capacity $u(v,w)$ and cost $c(v,w)$ , with $c(v,w)=-c(w,v)$ . A pseudoflow $f$ respects capacities and the paired-arc relation $f(v,w)=-f(w,v)$ . Its excess $e_f(v)$ is the sum of flow entering $v$ . A circulation is a pseudoflow with zero excess everywhere. The already published CycleCanceling.MinMean.Network supplies this network, its circulation predicate, and residual capacity $u_f(v,w)=u(v,w)-f(v,w)$ . An arc is residual when this capacity is positive.

A price function $p:V\to\mathbb R$ changes an arc's reduced cost to $c_p(v,w)=c(v,w)-p(v)+p(w)$ . A pseudoflow is $\varepsilon$ -optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$ . A vertex is active when its excess is positive. An admissible arc is a residual arc of negative reduced cost. Refine takes an input circulation that is $2\varepsilon$ -optimal, saturates every arc whose reduced cost is negative, and then repeatedly applies an available update. A push sends flow from an active vertex along an admissible arc. A relabel raises the price of an active vertex with no outgoing admissible arc to the largest value permitted by $\varepsilon$ -optimality. These rules are Figures 4 and 5, printed pages 18–19.

Formalization targets

The supporting targets are the paper's progress and correctness results, its price bound, and the three operation counts. For any generic refine run from a $2\varepsilon$ -optimal circulation, Lemma 5.8 bounds each vertex's price increase by $3n\varepsilon$ . Lemmas 5.9–5.11 bound the numbers $R,S,T$ of relabelings, saturating pushes, and nonsaturating pushes:

R\leq 3n(n-1),\qquad S\leq 3nm,\qquad T\leq 3n^2(m+n).

The goal combines the resulting bound on the number $K$ of updates with progress and correctness:

K\leq 3n(n-1)+3nm+3n^2(m+n).

If the final state has an active vertex, another update exists. If no update applies, the final pseudoflow is a circulation and is $\varepsilon$ -optimal with respect to its final prices. This is the explicit operation-count content behind the generic subroutine's analysis in Section 5. It does not claim a bound for a particular data structure or a complete minimum-cost algorithm.

Significance

The theorem gives an order-independent finite bound: the choice of which applicable push or relabel to perform cannot cause generic refine to run forever or stop with an active vertex. Its output is a circulation whose approximate-optimality tolerance has been halved. That output can serve as the next input in the successive-approximation framework. For integral costs, the report's Theorem 2.3 later turns a sufficiently small tolerance into exact minimum cost; that outer-loop result is outside this mission.

This mission specifies the generic cost-scaling state machine in Lean and poses its quantitative analysis as open formalization targets. The shared network and circulation definitions from the published Goldberg–Tarjan 1989 series are available, and a related generic maximum-flow theorem in the 1988 series has a machine-checked proof. Those results do not prove refine's price-based bounds. Contributions that establish the paper's progress, price, or counting statements for this state machine, and reusable facts about finite residual networks, advance the open goal.

Difficulty

A push respects a capacity, but it can create activity at another vertex; a relabel changes which arcs are admissible. Thus checking a single update does not bound an arbitrary sequence. The price bound also depends on the circulation and prices supplied at entry, not merely on the current pseudoflow being $\varepsilon$ -optimal. Finally, a vertex with no admissible outgoing arc may appear to be stuck when the relabel minimum is over an empty set. Feasibility of the original circulation network is needed to establish that an active vertex still has a genuine next update. The operation bound requires accounting for the three update types across every possible choice sequence.

Formalization scope

Vertices form a finite type, and capacities, costs, flows, and prices are real-valued functions. The network has symmetric ordered arcs and antisymmetric costs. There is no separate nonnegativity assumption on capacities; feasibility is supplied by the input circulation. The new $\varepsilon$ is positive, so the entry circulation is $2\varepsilon$ -optimal before Figure 4 halves the error parameter. The run starts from the resulting saturated pseudoflow and records one applicable push or relabel per index $k<K$ . Counts classify those actual steps by the selected arc's residual capacity after a push. Termination is the negation of the paper's loop guard, not a definition that assumes zero excess.

The reduced-cost sign is $c-p(v)+p(w)$ , and relabel raises $p(v)$ . This differs from the published 1989 epsilon-optimality definition, so only its network model is imported. The relabel relation requires an attained minimum over a nonempty set of outgoing residual arcs; it assigns no default value to an empty minimum. Loops may occur in the reused network model, but cost antisymmetry makes their reduced cost zero, so they cannot be push arcs. The explicit constants are the report's $3n\varepsilon$ , $3n(n-1)$ , $3nm$ , and $3n^2(m+n)$ ; the goal sums the last three. The report's RAM-model $O(\cdot)$ running times are outside the formal statements. A definition that makes termination equivalent to conservation or assigns an arbitrary relabel price at an empty set would miss the target.

Selected references

Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987. Technical report.
Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI. The report above supplies this mission's numbering.
Andrew V. Goldberg and Robert E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4), 1988. DOI.
Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, Journal of the ACM 36(4), 1989. DOI.

10 thms2 active usersReviewed

Graph Theory Optimization·Captain: mikedeng1

Send-and-Split Method for Minimum-Concave-Cost Network Flows I: A Minimum-Cost Flow Exists iff Every Simple Circulation Has Nonnegative Cost, and Then an Extreme One Exists (Theorem 1)Research Paper

Why minimum-concave-cost flows

Many network design and production–distribution problems have economies of scale: shipping twice as much along an arc costs less than twice as much, because of fixed charges, set-up costs or volume discounts. Modelled as network flows, such problems ask for a flow of least cost when each arc cost is a concave function of the flow on the arc. Classical instances include the uncapacitated lot-sizing problem, the fixed-charge transportation problem, and the Steiner tree problem in graphs. Unlike linear costs, concave costs make the problem NP-hard in general, and the usual linear-programming arguments do not apply directly.

Erickson, Monma and Veinott (Math. Oper. Res. 12 (1987) 634–664) give the send-and-split method, a dynamic program that solves such problems in time exponential only in the number of demand nodes. Before the method can run, two questions must be settled: when does a minimum-cost flow exist at all, and can the arc costs be shifted so that they are nonnegative on flows? Theorem 1 of the paper answers both. This mission formalizes Theorem 1.

Timeline. Hirsch and Hoffman (1961) showed that a concave function bounded below on a polyhedron's extreme rays attains its minimum at a vertex; Rockafellar's Convex Analysis (1970, pp. 61, 343) gives the polyhedral form. Edmonds and Karp (1972) showed how to choose node potentials making linear arc costs nonnegative. Theorem 1 (1987) extends both to additive concave costs on uncapacitated networks.

Setting

A graph $G = (N, A)$ has $n$ nodes and a set $A$ of ordered pairs of distinct nodes, the arcs. A demand vector $r \in \mathbb{R}^n$ assigns a demand $r_i$ to each node (negative demands are supplies). A preflow is a nonnegative matrix $x = (x_{ij})$ carried by the arcs, and a flow for $r$ is a preflow with

\sum_{(j,i)\in A} x_{ji} - \sum_{(i,k)\in A} x_{ik} = r_i \qquad (i \in N),

inflow minus outflow equal to demand. A circulation is a flow for $r = 0$ .

The flow cost is $c(x) = \sum_{(i,j)\in A} c_{ij}(x_{ij})$ , where each $c_{ij}$ is concave on $[0,\infty)$ and $c_{ij}(0) = 0$ . A minimum-cost flow for $r$ is a flow whose cost is at most that of every flow for $r$ .

A preflow induces the subgraph of arcs with nonzero flow. An extreme flow is a flow whose induced subgraph is a forest (in the undirected sense; two antiparallel arcs form a cycle). A simple circuit is a directed cycle through at least two distinct nodes, with arc set $C$ ; a simple circulation is a circulation whose induced subgraph is a simple circuit. The slope at infinity $\dot c_{ij}(\infty) \in [-\infty, \infty)$ is the limit of the right derivative of $c_{ij}$ .

Two nodes are in the same strong component if chains (directed walks) join them both ways; a component is a sink if no chain leaves it. The augmented graph $\underline{G}$ appends a node $\nu$ and an arc $(i,\nu)$ for exactly one node $i$ of each sink component. Its arc costs $\underline{c}$ are $\dot c_{ij}(\infty)$ on arcs inside strong components and arbitrary real numbers elsewhere; $\underline{\pi}_i$ is the infimum of the costs of chains from $i$ to $\nu$ . For $\pi \in \mathbb{R}^n$ , the altered costs are $c^\pi_{ij}(y) = c_{ij}(y) - (\pi_i - \pi_j) y$ .

Formalization targets

Goal: Theorem 1

The following are equivalent:

\begin{aligned} &1^\circ\ \text{there is a minimum-cost flow for some demand vector;}\\ &2^\circ\ \text{the null circulation is a minimum-cost circulation;}\\ &3^\circ\ \text{for every } r \text{ with a flow, some minimum-cost flow for } r \text{ is extreme;}\\ &4^\circ\ c(y) \ge 0 \text{ for every simple circulation } y;\\ &5^\circ\ \textstyle\sum_{(i,j)\in C} \dot c_{ij}(\infty) \ge 0 \text{ for every simple circuit with arc set } C;\\ &6^\circ\ \text{there is a minimum-cost chain from each node of } \underline{G} \text{ to } \nu \text{ under } \underline{c}. \end{aligned}

If moreover $r$ admits a flow and $\underline{c}_{ij} z \le c_{ij}(z)$ on arcs joining distinct strong components, where $z = \sum_i r_i^+$ , they are equivalent to

7^\circ\quad \exists \pi\ \ c^\pi_{ij}(x_{ij}) \ge 0 \text{ for all arcs } (i,j) \text{ and all flows } x \text{ for } r,

and $\pi = \underline{\pi}$ is real and satisfies $7^\circ$ .

Milestones

The milestones are the statements the paper's proof rests on: the Hirsch–Hoffman extension (p. 638), $c^\pi(x) = c(x) + \sum_i \pi_i r_i$ , the bounds $\tfrac12 c(2x) + \tfrac12 c(2\theta y) \le c(x+\theta y) \le c(x) + c(\theta y)$ , the circuit-wise form of 4° ⇔ 5°, uniqueness of the extreme circulation, $x_{ij} \le z$ between strong components, and the two inequalities giving $7^\circ$ (all p. 639).

Significance

Theorem 1 decides existence of an optimum from the costs alone: conditions 4° and 5° do not mention the demand vector, so one test settles every demand pattern at once, and 3° guarantees the optimum may be sought among extreme (forest) flows, which is what the send-and-split recursion enumerates. Condition 6° is checkable by a shortest-chain computation, and 7° supplies node potentials that convert the instance into an equivalent one with nonnegative arc costs, the standing assumption of the paper's Theorem 2 and of its running-time analysis. For linear costs the theorem reduces to the familiar statement that a minimum-cost flow exists iff no simple circuit has negative cost.

The result is proved in the paper; it has not been machine-checked. The formalization adds a precise model of extreme flows over arcs (so that antiparallel arcs form a cycle), a treatment of slopes that may equal $-\infty$ , and the Hirsch–Hoffman extension specialized to network polyhedra, which the paper cites rather than proves. Related platform items cover the linear, capacitated case: CycleCanceling.MinMean.minCost_iff_no_negative_cycle and CycleCanceling.MinMean.minCost_iff_exists_price (Goldberg–Tarjan), and LinearOptimization.positive_directed_cycle_of_circulation and LinearOptimization.network_basic_iff_tree on a different arc encoding.

Difficulty

The first idea, to argue as for linear costs by cancelling negative cycles, fails because concave costs are not additive along cycle decompositions: the cost of a flow is not the sum of the costs of its cycle and path components, and a circuit can be harmless at small flow and arbitrarily negative at large flow. Existence therefore depends on the asymptotic slopes $\dot c_{ij}(\infty)$ , which may be $-\infty$ , rather than on any finite cost evaluation. The implication from bounded rays to an attained minimum (Hirsch–Hoffman) requires identifying the vertices of the flow polyhedron with forest flows and its extreme rays with simple circulations. The potential step 6° ⇒ 7° needs a cost bound on arcs between strong components, where the concave cost is only controlled up to the total positive demand $z$ .

Formalization scope

Nodes are Fin n; a graph is ArcGraph n, a Finset (Fin n × Fin n) of arcs without loops. Preflows are real matrices vanishing off the arcs; arc costs are functions $\mathbb{R} \to \mathbb{R}$ , concave on Set.Ici 0 with value $0$ at $0$ (the paper's "without further mention" assumption, made a hypothesis). The augmented graph has nodes Option (Fin n), with none the node $\nu$ ; chain costs, $\dot c_{ij}(\infty)$ and $\underline{\pi}$ are EReal-valued.

The explicit readings of loose phrases are:

"minimum-cost flow" is a flow whose cost is at most that of every flow for the same demands (attained, never an infimum);
"bounded below on each half-line" is $\exists M\ \forall \theta \ge 0,\ M \le c(x+\theta y)$ ;
$\dot c_{ij}(\infty)$ is the infimum over $t > 0$ of the right derivative at $t$ , equal to the limit by concavity;
"chain" is a directed walk; "minimum-cost chain" is a chain of real cost at most every chain's cost;
6° quantifies over every admissible choice of the appended arcs and of the finite costs $\underline{c}$ ;
in the 7° part, "flows $x$ " are flows for the given $r$ , and the existence of such a flow is an added hypothesis: without it 7° is vacuous while 4° can fail;
" $\underline{\pi}$ satisfies 7°" uses the real values of $\underline{\pi}$ , which the theorem asserts are real.

A formalization in which extreme flows are forests of a simple graph built from the support, in which chains are simple paths, or in which a chain of cost $-\infty$ counts as a minimum would make 3°, 6° or the equivalence trivially or falsely true; all three are ruled out by the definitions. The running-time remarks, the computation paragraph and the linear-cost remark after the proof are not formalized. Contributions are welcome on the polyhedral side (vertices and extreme rays of $\{x \ge 0 : \text{conservation}\}$ ), on right derivatives of concave functions at infinity, and on walk costs with negative cycles; all are reusable beyond this mission.

Selected references

R. E. Erickson, C. L. Monma, A. F. Veinott, Jr., Send-and-Split Method for Minimum-Concave-Cost Network Flows, Mathematics of Operations Research 12(4), 1987, 634–664. https://doi.org/10.1287/moor.12.4.634
W. M. Hirsch, A. J. Hoffman, Extreme varieties, concave functions, and the fixed charge problem, Communications on Pure and Applied Mathematics 14, 1961, 355–369. https://doi.org/10.1002/cpa.3160140312
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, Journal of the ACM 19(2), 1972, 248–264. https://doi.org/10.1145/321694.321699

11 thms2 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts I: The Newsvendor Quantity-Flexibility Contract (w_q(δ), δ) Gives the Retailer at Least Π(q°) at δ = 0, the Supplier at Least Π(q°) at δ = 1Textbook

Why contracts in a newsvendor supply chain

A supplier sells to a retailer who must order before a single selling season with random demand. Each firm maximizes its own expected profit, and with the simplest contract, a fixed wholesale price per unit, the retailer orders too little: he bears all the risk of unsold stock but earns only part of the margin on each sale. The supply chain as a whole then earns less than it could. A contract is said to coordinate the supply chain if the chain-optimal actions are an equilibrium of the two firms' game. Which contracts coordinate, and how they divide the chain's profit, is the subject of a large literature in operations management. G. P. Cachon's survey chapter in the Handbooks in Operations Research and Management Science (Cachon 2003) gives its standard account. This mission formalizes §6.2 of that chapter, Coordinating the newsvendor, read in the author's 3rd draft (January 2003).

Timeline of the contracts treated in §6.2:

Pasternack (1985) shows that buy-back (returns) contracts coordinate the newsvendor.
Tsay (1999) and Tsay and Lovejoy (1999) study quantity flexibility contracts, in which the supplier refunds unsold units up to a fraction δ of the order.
Cachon and Lariviere (2005, working paper 2000) analyze revenue sharing and show it is equivalent to buy back in the newsvendor.
Taylor (2002) studies sales rebates. Moorthy (1987) and Kolay and Shaffer (2002) treat quantity discounts.

Setting

Demand $D \ge 0$ has distribution function $F$ , with $\bar F = 1 - F$ and mean $\mu = E[D]$ . The retail price is $p$ . The supplier's unit production cost is $c_s$ and the retailer's unit cost is $c_r$ , with $c = c_s + c_r < p$ . Unmet demand costs the retailer a goodwill penalty $g_r$ per unit and the supplier $g_s$ , with $g = g_s + g_r$ . Each unsold unit is worth $v < c$ to the retailer.

Expected sales are $S(q) = E[\min(q, D)]$ , leftover inventory is $I(q) = E[(q - D)^+]$ and lost sales are $L(q) = E[(D - q)^+]$ . If $T$ is the expected payment from the retailer to the supplier, the firms earn

\pi_r(q) = (p - v + g_r)S(q) - (c_r - v)q - g_r\mu - T, \qquad \pi_s(q) = g_sS(q) - c_sq - g_s\mu + T,

and the chain earns $\Pi(q) = (p - v + g)S(q) - (c - v)q - g\mu$ . Let $q^o$ be a maximizer of $\Pi$ , with $\Pi(q^o) > 0$ .

Under the quantity flexibility contract $(w_q, \delta)$ the retailer pays $w_q$ per unit ordered and is refunded $w_q + c_r - v$ for each unsold unit, up to $\delta q$ units:

T_q(q, w_q, \delta) = w_qq - (w_q + c_r - v)\int_{(1-\delta)q}^q F(y)\,dy.

The wholesale price that makes $q^o$ satisfy the retailer's first-order condition is

w_q(\delta) = \frac{(p - v + g_r)\,\bar F(q^o)}{\bar F(q^o) + (1-\delta)F((1-\delta)q^o)} - c_r + v.

Formalization targets

Goal: the quantity flexibility contract can split the profit in any way

With $\pi_r(q, w_q(\delta), \delta)$ and $\pi_s(q, w_q(\delta), \delta)$ the firms' profits under $(w_q(\delta), \delta)$ :

\pi_r(q^o, w_q(0), 0) = \Pi(q^o) + g_s\big(\mu - S(q^o) + \bar F(q^o)q^o\big) \ge \Pi(q^o),

\pi_s(q^o, w_q(1), 1) = \Pi(q^o) + \mu g_r \ge \Pi(q^o),

and for every $a \in [0, \Pi(q^o)]$ some $\delta \in [0,1]$ gives the retailer $a$ and the supplier $\Pi(q^o) - a$ (§6.2.5, p. 25).

Milestones, in attack order

$S(q) = q - \int_0^q F$ , $I(q) = q - S(q)$ , $L(q) = \mu - S(q)$ (p. 10).
The unique maximizer $q^o$ of $\Pi$ satisfies $\bar F(q^o) = (c - v)/(p - v + g)$ (Eq. (2), p. 11).
$w_q(0) = (p - v + g_r)\bar F(q^o) + v - c_r$ and $w_q(1) = p + g_r - c_r$ . Also, $w_q$ is increasing on $[0,1]$ , which gives $v - c_r \le w_q(\delta) \le p + g_r - c_r$ (p. 24).
$q^o$ maximizes the retailer's profit under $(w_q(\delta), \delta)$ (Eq. (11), p. 24).
The supplier's first-order condition holds at $q^o$ (p. 25).
The δ = 0 identity and the δ = 1 identity (p. 25).

Companion results of §6.2

Revenue sharing $\{w_r,\phi\}$ equals the buy back $w_b = w_r + (1-\phi)p$ , $b = (1-\phi)(p - v)$ for every demand realization (p. 22).
The sales rebate contract: first-order condition (12), price (13), the retailer's profit and its monotonicity in the threshold (p. 27), and failure under voluntary compliance (p. 28).
The quantity discount gives the retailer $\pi_r = \lambda(\Pi(q) + g\mu) - g_r\mu$ , so $q^o$ is optimal for both firms (p. 29).
Under the wholesale price contract, the retailer's profit increases in the induced quantity (p. 14).

Significance

The goal is what makes quantity flexibility a complete coordinating family. Retailer optimality (milestone 4) says $q^o$ can be implemented. The allocation statement says that bargaining power can then be expressed through the single parameter δ without losing efficiency. Together with the supplier's first-order condition, these are the facts that matter in practice: forced compliance suffices for coordination, and the choice of δ is purely distributional. The companions put §6.2's other contracts on the same footing. Revenue sharing and buy back are equivalent. Sales rebates coordinate only with forced compliance. Quantity discounts coordinate with a bounded retailer share.

All of these results are stated in the source. Related results are Proved on the platform in Snyder and Shen's chapter (SupplyChainTheory.*), including the chain-optimal fractile and retailer optimality under quantity flexibility. This mission states them locally because Snyder and Shen's contract data impose stronger restrictions on salvage value than Cachon's model. The efficiency formula $(k+1)^{-(1+1/k)}(k+2)$ for the power distribution on p. 14 is already posed as the Open item RevShareCoord.Wholesale.alpha_family_efficiency and is not posed again.

Difficulty

Each identity is elementary algebra once $S$ , its derivative and the integrals of $F$ are under control. That is where the work lies. Expected sales are defined as an expectation, so $S(q) = q - \int_0^q F$ is a theorem to prove, not a definition to unfold.

Differentiating $\int_{(1-\delta)q}^q F$ needs continuity of $F$ at two points. The sales rebate transfer is piecewise and has a kink at the threshold, so derivatives must be taken on the right side of it.

The allocation clause rests on continuity of δ ↦ π_r(q^o, w_q(δ), δ). The obvious argument, "the profits are continuous in δ", hides two facts. First, the denominator of $w_q(\delta)$ stays positive on $[0,1]$ . Second, $F((1-\delta)q^o)$ moves continuously, which fails for a demand law with atoms. Both must be derived from the model, not assumed.

Formalization scope

The local ContractData follows Cachon's $v<c_s+c_r$ and $c_s+c_r<p$ . Its $r$ is Cachon's price $p$ , and its $p_s,p_r$ are the goodwill penalties $g_s,g_r$ . The penalties are nonnegative costs. Net salvage may be negative and may exceed $c_r$ ; both possibilities were excluded by the related published model.

A demand law is a probability measure on ℝ with no mass on $(-\infty, 0)$ , finite mean and no atoms (so $F$ is continuous). $F$ is strictly increasing on $[0, \infty)$ as long as $F < 1$ . Its derivative is specified on the positive interior of that active support. This reading admits the bounded-support power law the chapter itself uses on p. 14, whose cdf has a corner at the support endpoint. Derivative conclusions use HasDerivAt.

Optimality is IsMaxOn … Set.univ over real quantities; the optimum is positive under the model assumptions. $\Pi(q^o) > 0$ is a hypothesis wherever an optimum is named, following p. 11.

Cachon's sales rebate $r$ is rebate in Lean.

Three printed slips are corrected, and the milestone quotes keep the print:

p. 24 writes $w$ for $w_q$ in $T_q$ .
p. 25 mixes $q$ and $q^o$ in the δ = 0 and δ = 1 displays.
p. 28 has a spurious $-v$ in $w_s(r) - r$ .

Two encodings are ruled out. $w_q(\delta)$ is the explicit formula, never "the solution of (11)". The supplier's profit is the model's own function, not $\Pi$ minus the retailer's profit, so no clause holds by definition.

The local definition file CachonCoord.Newsvendor.Contracts contains the model, its expected profits, the contract transfers, the sales rebate price $w_s(r)$ , the quantity discount schedule, and realized profits and payments. Lemmas about $S$ , $\int F$ and continuity of contract prices are reusable across the series. The sales rebate existence-of-threshold argument and the normal-distribution counterexample of p. 25 are outside this mission.

Selected references

G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves, T. de Kok (eds.), Handbooks in OR & MS Vol. 11, North-Holland, 2003 (3rd draft, Jan. 2003). https://doi.org/10.1016/S0927-0507(03)11006-7
B. A. Pasternack, Optimal pricing and return policies for perishable commodities, Marketing Science 4(2), 1985. https://doi.org/10.1287/mksc.4.2.166
A. A. Tsay, The quantity flexibility contract and supplier–customer incentives, Management Science 45(10), 1999. https://doi.org/10.1287/mnsc.45.10.1339
G. P. Cachon, M. A. Lariviere, Supply chain coordination with revenue-sharing contracts: strengths and limitations, Management Science 51(1), 2005. https://doi.org/10.1287/mnsc.1040.0215
T. A. Taylor, Supply chain coordination under channel rebates with sales effort effects, Management Science 48(8), 2002. https://doi.org/10.1287/mnsc.48.8.992.168
L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Ch. 14. https://doi.org/10.1002/9781119584445

9 thms2 active usersReviewed

Completed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments III: The Three Revenue-Ordered Approximation Bounds Are TightResearch Paper

Motivation

A retailer or an airline chooses which products to offer, and customers choose among what is offered, or buy nothing. Choosing the offer set that maximizes expected revenue is the assortment problem, central to revenue management (Talluri and van Ryzin, 2004). It is NP-hard even for simple mixtures of logit models, so practice relies on heuristics. The most common one is the revenue-ordered assortments strategy: offer the products whose price is above a threshold, and pick the best threshold.

Berbeglia and Joret (arXiv:1606.01371) analyse this heuristic under every regular choice model, the broad class in which enlarging the offer set never raises the probability of choosing any given alternative, including not buying. They prove three approximation guarantees, then show that none of the three can be improved. This mission formalizes that last result, Theorem 3.4.

Timeline:

Talluri and van Ryzin (2004) showed that revenue-ordered assortments are optimal under the multinomial logit model.
Rusmevichientong, Shmoys, Tong and Topaloglu (2014) showed the problem NP-hard under a mixture of two logit models, and proved that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit.
Aouad, Farias, Levi and Segev (2018) proved an $\Omega(1/\ln(r_k/r_1))$ guarantee under random utility models, and that the assortment problem there is NP-hard to approximate within $\Omega(1/n^{1-\epsilon})$ and $\Omega(1/\log^{1-\epsilon}(r_k/r_1))$ .
Berbeglia and Joret (2016–2020, Algorithmica) proved the guarantees $1/k$ , $1/\sum_{i}(r_i-r_{i-1})/r_i\ge1/(1+\ln(r_k/r_1))$ and a purchase-probability bound under any regular model, and an instance on which all three, in their sum forms, are attained in the limit.

Setting

The products form a finite set $\mathcal C$ . 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 buys $x$ . The no-purchase probability is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ . The model is regular if

$\mathcal P(x,S)\ge0$ for $x\in\mathcal C\cup\{0\}$ ;
$\mathcal P(x,S)=0$ for $x\notin S$ ;
$\sum_{x\in S}\mathcal P(x,S)\le1$ ;
$\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$ .

Each product has a revenue $r(x)>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 revenues, with $r_0:=0$ , and $S_i=\{x: r(x)\ge r_i\}$ . The heuristic earns

\mathrm{RO}=\max_{i\in[k]}\mathrm{rev}(S_i).

For an optimal $S^*$ let $N_i=\sum_{x\in S^*,\,r(x)\ge r_i}\mathcal P(x,S^*)$ , $N_{k+1}=0$ , and $\ell$ the largest index with $N_\ell>0$ . Section 3 of the paper proves

(A) $\mathrm{OPT}\le k\cdot\mathrm{RO}$ (Theorem 3.1);
(B) $\mathrm{OPT}\le D_r\cdot\mathrm{RO}$ , with $D_r=\sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\le 1+\ln(r_k/r_1)$ (Theorem 3.2);
(C) $\mathrm{OPT}\le D_N(S^*)\cdot\mathrm{RO}$ , with $D_N(S^*)=\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\le 1+\ln(N_1/N_\ell)$ (Theorem 3.3).

Formalization targets

Goal: Theorem 3.4

For every $k\ge1$ and every $\delta>0$ there are a finite nonempty product set, a regular $\mathcal P$ , revenues $r>0$ with exactly $k$ distinct values, and an optimal $S^*$ with $N_1>0$ , such that

k\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_r\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_N(S^*)\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT}.

So none of the bounds (A), (B), (C) stays true when multiplied by $1+\delta$ , for any number $k$ of distinct revenues.

The tight instance (milestones)

The paper's witness has products $(i,j)$ with $i\in[k]$ and $j\in[i]$ . Product $(i,j)$ has revenue $\varepsilon^{-j}$ , and $\mathcal P((i,j),S)=\varepsilon^i$ when $(i,j)\in S$ and $(i,1),\dots,(i,j-1)\notin S$ , and $0$ otherwise, for $0<\varepsilon\le\tfrac12$ . The milestones follow the proof on pp. 10–11:

the axiom (iii) bound;
(7);
(8);
(9);
regularity;
the distinct revenues $r_i=\varepsilon^{-i}$ ;
$\mathrm{RO}=\mathrm{rev}(\mathcal C)<1/(1-\varepsilon)$ ;
$\mathrm{OPT}=k$ , attained by $\{(i,i)\}$ ;
the limits $\mathrm{OPT}/\mathrm{RO}\to k$ and $D_r\to k$ ;
$N_i=\varepsilon^i+\dots+\varepsilon^k$ and $D_N\to k$ as $\varepsilon\to0^+$ .

Significance

With Theorems 3.1–3.3, Theorem 3.4 closes the analysis: in terms of the parameters $k$ , $D_r$ and $D_N$ , revenue-ordered assortments are understood exactly under regular choice. It complements the hardness results of Aouad et al., which already show that no efficient strategy can do much better than (A) and (B) in general; Theorem 3.4 shows that the analysis of this particular heuristic is exact. The instance is also a concrete regular choice model in which the optimal offer set is far from every nested one.

On the formal side, the mission produces a reusable formal definition of regular discrete choice models, revenue-ordered assortments and the three bound quantities. These are shared, under other sub-namespaces, with the companion missions on Theorems 3.2 and 3.3. The result is proved in the paper. As far as is known it has not been machine-checked anywhere; the remaining work is formalizing the paper's proof, including the steps it leaves to the reader.

Difficulty

The proof is a construction, and the paper verifies most of it in a sentence each. The work lies in those sentences:

the regularity of the instance at the no-purchase option, (9), which needs the row decomposition (8);
the claim that $\{(i,i)\}$ is optimal among all $2^{k(k+1)/2}$ offer sets, asserted without proof;
the claim that the full set is the best threshold set;
the evaluation of $D_N(S^*)$ , which needs $\ell=k$ .

The naive witness, one instance per bound, does not help: the goal asks for one instance with exactly $k$ revenues on which all three bounds are nearly attained, for every $k$ .

Formalization scope

Products are an arbitrary finite type C. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S. Offer sets are Finset C.
IsRegular carries axioms (i)–(iv), with (i) and (iv) stated both for products and for the no-purchase option. Regularity at $x=0$ is essential: without it the guarantees fail.
$\mathrm{OPT}$ is Finset.sup' over all subsets, including $\emptyset$ . $\mathrm{RO}$ is Finset.sup' over the $k$ threshold sets only, and needs Nonempty C.
The distinct revenues are the sorted image of r, indexed by Fin k from $0$ : the Lean index $i$ is the paper's $i+1$ , and $r_0=0$ is a separate case. $\ell$ lives in WithBot (Fin k).
Bounds are multiplicative ( $\mathrm{OPT}\le D\cdot\mathrm{RO}$ ); there is no ratio $\mathrm{RO}/\mathrm{OPT}$ in the goal. Limits are along 𝓝[>] 0.
The tight instance keeps the paper's 1-based pairs $(i,j)$ as a subtype of Fin (k+1) × Fin (k+1). Its regularity is a theorem to prove, never a field assumed.

Ruled out:

a fixed $k$ , since "for every $k$ " is the content;
tightness of the logarithmic forms $1/(1+\ln(r_k/r_1))$ and $1/(1+\ln\nu)$ , which this instance does not show (there $1+\ln(r_k/r_1)\to\infty$ while $\mathrm{OPT}/\mathrm{RO}\to k$ ), so only the sum forms are claimed tight;
an instance whose regularity is assumed;
a heuristic maximizing over all subsets.

Contributions welcome: proofs of the milestones, especially (8), (9) and the optimality of $\{(i,i)\}$ , and general lemmas on sorted distinct values of a finite function.

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; published in Algorithmica, 2020. https://arxiv.org/abs/1606.01371
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
A. Aouad, V. Farias, R. Levi and D. Segev, The Approximability of Assortment Optimization Under Ranking Preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1724

15 thms2 active usersReviewed

Completed

Optimization Theoretical Computer Science·Captain: mikedeng1

Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments II: Revenue-Ordered Assortments Earn OPT/(1 + ln ν), ν the Optimum's Purchase RatioResearch Paper

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

$\mathcal P(x,S)\ge0$ for products and for $x=0$ ;
$\mathcal P(x,S)=0$ for $x\notin S$ ;
$\sum_{x\in S}\mathcal P(x,S)\le1$ ;
$\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

9 thms2 active usersReviewed

Completed

Combinatorics Probability Theoretical Computer Science·Captain: mikedeng1

Online Stochastic Matching: Beating 1-1/e 2: The Suggested Matching Algorithm Achieves 1 − 1/e with High Probability, and This Is Tight Even in ExpectationResearch Paper

Motivation

Online bipartite matching models decisions that must be made as requests arrive: an advertiser can be assigned to a compatible request once, and an assignment cannot be revised when later requests reveal a better alternative. Display advertising is the motivating example in Feldman, Mehta, Mirrokni, and Muthukrishnan's 2009 preprint: an ad server knows which advertisers accept each kind of impression and has estimates of how frequently those kinds will arrive. The question is how much this advance distributional information helps when decisions still have to be immediate.

This mission studies the paper's first offline-guided algorithm. It computes a maximum matching for the expected traffic and follows that matching during the actual random run. The paper shows that this natural policy reaches the familiar $1-1/e$ performance level and that its own analysis cannot be improved for this policy, even if performance is averaged over runs. The result sets the baseline for the paper's later two-suggested-matchings algorithm, which improves on that level under its stated assumptions. Feldman et al., §§1 and 4.1

Setting

An instance consists of a finite advertiser set $A$ , a finite impression-type set $I$ , and allowed edges $E\subseteq A\times I$ . For each type $i$ , the nonnegative integer $e_i$ is its expected number of arrivals. There are $n=\sum_{i\in I}e_i>0$ arrivals. Each arrival independently has type $i$ with probability $e_i/n$ . A type with $e_i=0$ remains in the graph but has zero arrival probability. On an arrival of type $i$ , an online algorithm may assign it to an adjacent advertiser that has not been assigned before, or may leave it unassigned. The hindsight optimum, $\mathrm{OPT}(\omega)$ , is the largest matching in the realization graph with one vertex for every arrival position, including separate vertices for repeated types. Feldman et al., §2, pp. 3–4

The suggested matching algorithm first selects any maximum integral flow in the expected-instance network. Each advertiser has capacity one, and each type $i$ has capacity $e_i$ . Equivalently, the selected edges form a maximum degree-capped bipartite matching $M\subseteq E$ . Let $A^*$ be the advertisers covered by $M$ . When type $i$ arrives, the algorithm chooses each advertiser joined to $i$ by a selected edge with probability $1/e_i$ ; any remaining probability chooses no advertiser. It assigns the chosen advertiser if available and otherwise makes no assignment. Its number of assignments is $\mathrm{ALG}(\omega)$ . This rule includes the algorithm's random choice in addition to the random arrival types. Feldman et al., §4.1, p. 5

The canonical residual cut of $M$ places each advertiser and impression type on the source side if it is reachable from the source by residual edges. Write $A_T$ for advertisers on the sink side and $I_S$ for types on the source side. These sets describe the comparison between the expected-instance matching and the optimum of a realized run. The mission also uses occupancy: after $n$ independent uniform throws into $n$ bins, count how many bins in a fixed subset receive at least one ball. Feldman et al., §§2.1 and 4.1

Formalization targets

Theorem 4's general-instance guarantee is expressed in the additive form established by its analysis. For every $\varepsilon>0$ , there are $\delta>0$ and $N$ , uniform across all finite instances, all maximum integral flows, and all valid ways of realizing the algorithm's random choice, such that $n\ge N$ implies

\Pr\!\left[\mathrm{ALG}(\omega)\ge(1-e^{-1})\mathrm{OPT}(\omega)-\varepsilon n\right] \ge 1-e^{-\delta n}.

The complete bipartite family gives the tightness target. When $A=I=\{0,\ldots,n-1\}$ and every $e_i=1$ , every maximum expected-instance matching is perfect. For every run, $\mathrm{OPT}=n$ , and

\mathbb E[\mathrm{ALG}] =n\left(1-\left(1-\frac1n\right)^n\right), \qquad \lim_{n\to\infty}\frac{\mathbb E[\mathrm{ALG}]}{n}=1-e^{-1}.

The milestone list follows the paper's Fact 1 and the named passages “Bounding ALG,” “Bounding OPT,” and “Tightness of the Analysis” in §4.1. The cut identity $|A^*|=|A_T|+\sum_{i\in I_S}e_i$ is a separate deterministic milestone. Feldman et al., Theorem 4 and §4.1, pp. 5–6

Significance

The result establishes exactly what this one-matching policy achieves under integer-frequency independent arrivals. It gives a guarantee for the actual number of assignments relative to the best assignment made with hindsight, and a family on which the limiting expected ratio equals the guarantee. That tight family explains why the paper introduces a second suggested matching rather than seeking a stronger bound for the same policy. Feldman et al., §4

The mathematical theorem is proved in the paper; the mission asks for its machine-checked formalization. The development would also provide reusable finite models of repeated-type realizations, integral degree-capped bipartite matchings, uniform occupancy, and residual reachability cuts. No machine-checked proof of these mission items is being claimed by this draft.

Difficulty

The expected-instance matching is selected before the arrivals, but the hindsight optimum can exploit the actual multiplicities of every type. Counting only the ads selected online does not compare the algorithm with that hindsight optimum. Also, a type may have several selected advertisers when $e_i>1$ , so replacing the algorithm's random choice by a deterministic designated ad would change its law. The cut and concentration statements have to apply uniformly to every maximum integral flow, including flows chosen by different tie-breaking rules. Feldman et al., §4.1, pp. 5–6

Formalization scope

Advertisers and types are finite Lean types. The edge relation is a finite set, and $e_i$ and $n$ are natural numbers with $n=\sum_i e_i>0$ . An integral maximum flow is represented by a maximum cardinality edge set with advertiser degree at most one and type- $i$ degree at most $e_i$ . The theorem quantifies over every such set. This is the unit-advertiser, integer-type-capacity flow used in §4.1, without a separate real-valued flow object. The canonical cut is defined through residual reachability. The hindsight optimum maximizes over matchings of the realized graph, with each arrival position distinct.

The run uses $n$ independent uniform draws from $\sum_i\{0,\ldots,e_i-1\}$ . A valid labelling assigns each selected advertiser at type $i$ to a distinct copy. The drawn copy determines the type and, if labelled, the ad selected by the algorithm. This gives type probability $e_i/n$ , conditional ad probability $1/e_i$ on selected edges, and the remaining “no ad” probability. Counts, probabilities, and expectations use finite sums, so there is no integrability convention. Since $n>0$ , the run sample space is nonempty; no value of $\mathrm{ALG}/\mathrm{OPT}$ at $\mathrm{OPT}=0$ is needed. The complete-graph family has $n\ge1$ .

The paper writes $1-e^{-\Omega(n)}$ in both bounding passages. The Lean statements spell this out as $\forall\varepsilon>0,\ \exists\delta>0,\ \exists N,\ \forall$ instances with $n\ge N$ , with $\delta,N$ preceding the instance. Theorem 4's ratio language is represented by the additive estimate its proof yields; a vanishing ratio error requires a separate lower bound on $\mathrm{OPT}/n$ . The exact finite- $n$ expectation and its limit make “tight, even in expectation” precise. The printed Fact 1 exponent is $\varepsilon n/2$ , while its Appendix A proof yields $\varepsilon^2n/2$ ; the formalized concentration statement uses the proved exponent and the milestone retains the printed wording. Neither a ratio with a zero denominator nor a labelling that changes the algorithm's choice law is accepted as a shortcut.

Contributions toward the occupancy bound, the residual cut identity, the realized matching bound, and the complete-graph expectation are welcome. The finite occupancy and matching interfaces are intended for reuse beyond this specific algorithm.

Selected references

Jon Feldman, Aranyak Mehta, Vahab Mirrokni, and S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, arXiv:0905.4100v1, 2009; FOCS 2009. Preprint

10 thms2 active usersReviewed

Completed

Combinatorics Linear Optimization·Captain: mikedeng1

Solving Large-Scale Zero-One Linear Programming Problems: A Minimal Cover Inequality Cuts Off x̄ iff the Knapsack Problem (2.12) Has Optimal Value Less Than OneResearch Paper

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

8 thms2 active usersReviewed

Dynamical Systems Stochastic Systems·Captain: mikedeng1

Stability and Instability of Fluid Models for Reentrant Lines 3: In Every Reentrant Line the Last-Buffer-First-Served Fluid Model Is StableResearch Paper

Motivation

A manufacturing line can send the same job through several stations and return it to a station it visited earlier. Semiconductor fabrication is one example. Such a reentrant line has several customer classes at one server, and the server must choose which class to work on. A station may have enough capacity on average yet the line can still accumulate an unbounded queue under an unfortunate service rule. Dai and Weiss use deterministic fluid models to study this question: fluid represents large queues, and its motion exposes the long-run effect of the service rule. Their paper proves that two simple buffer priority disciplines have stable fluid models for every reentrant line satisfying the usual station load condition. This mission concerns Last-Buffer-First-Served, abbreviated LBFS. Dai and Weiss (1996).

The distinction between fluid and stochastic queue stability matters. Dai and Weiss cite an earlier theorem connecting stable fluid models to stable queueing disciplines under the stochastic assumptions of their introduction. The target here is their fluid theorem, Theorem 4.4, rather than a separate formalization of that stochastic implication. Dai and Weiss (1996), pp. 115, 119, 124.

Setting

There are $K$ classes, numbered in route order, and $I$ stations. Every unit of fluid enters class $1$ at rate one. On completing service in class $k$ , it becomes class $k+1$ ; after class $K$ , it leaves. The station serving class $k$ is $\sigma(k)$ . Different classes may share a station. The constituency of station $i$ is $C_i=\{k:\sigma(k)=i\}$ , and class $k$ has positive mean service requirement $m_k$ , so its service rate is $\mu_k=1/m_k$ . The nominal workload at station $i$ is $\rho_i=\sum_{k\in C_i}m_k$ . The paper assumes $\rho_i<1$ at every station. Dai and Weiss (1996), pp. 115–117.

For time $t\ge0$ , $Q_k(t)$ is the amount of fluid in class $k$ , and $T_k(t)$ is the cumulative server time spent on that class. The flow equations say that class content equals its initial content plus completed service from the preceding class minus its own completed service. The first class receives the external unit-rate flow. Each $Q_k$ remains nonnegative, each $T_k$ starts at zero and is nondecreasing, and the cumulative idle time of every station is nondecreasing. A priority rule adds a condition on when a server may reserve capacity for lower-ranked classes. These are the fluid equations of Definition 1.2 and §4. Dai and Weiss (1996), pp. 118, 122–123.

A priority ranking $\pi$ assigns a distinct rank to every class, with smaller rank meaning higher priority. For class $k$ , let $H_k$ contain the classes at the same station whose rank is at least as high as $k$ 's. In a preemptive-resume priority fluid model, capacity unused by $H_k$ may increase only when the fluid workload in $H_k$ is zero. Under LBFS, $\pi(k)=K+1-k$ : a class later in the route has higher priority. Priority is compared within each station, even though the ranking is written globally. Dai and Weiss (1996), pp. 122–123, Definition 4.1.

Formalization targets

Theorem 4.4 asks for stability of the LBFS fluid model for every reentrant line with positive service requirements and $\rho_i<1$ :

\exists\delta>0\;\forall (Q,T),\quad \bigl[(Q,T)\text{ is an LBFS fluid solution and }|Q(0)|=1\bigr] \Longrightarrow \forall t\ge\delta,\;Q(t)=0,

where $|Q(0)|=\sum_{k=1}^K Q_k(0)$ . The same $\delta$ must work for every solution and every normalized initial configuration. This is exactly the fluid stability definition used by the paper. Dai and Weiss (1996), pp. 118–119, 124.

The milestones follow the paper's own intermediate statements. Lemma 2.2 treats a nonnegative absolutely continuous function whose derivative is negative whenever the function is positive. Proposition 4.2 identifies flow-rate relations at a regular point under a buffer priority rule. The proof of Theorem 4.4 records a uniform negative drift for total content and the explicit emptying time

\delta=\frac{|Q(0)|}{\widehat\lambda-1},\qquad \widehat\lambda=\frac{1}{\max_{1\le i\le I}\rho_i}>1.

The explicit time is stated for every initial fluid amount; normalization to one belongs only to the final stability theorem. Dai and Weiss (1996), pp. 120, 123–125.

Significance

The theorem gives a uniform finite clearing time for the LBFS fluid model whenever each station's nominal workload is below its capacity. It applies to any number of stations, any finite route, and any assignment of route stages to stations. This is stronger than checking a particular factory layout. The conclusion concerns every fluid solution, which matters because the defining equations need not determine a unique path. Dai and Weiss (1996), pp. 118–119, 124–125.

Formalizing the result requires a reusable interface for reentrant lines, service allocation, station workloads, and the priority complementarity condition, plus separate statements for the extinction criterion and priority flow rates. The theorem is proved in the 1996 paper; the remaining work in this mission is a machine-checked Lean proof of its fluid-model statement and of the listed milestones. The stochastic queueing theorem cited by Dai and Weiss is outside this mission's scope.

Difficulty

The load inequalities $\rho_i<1$ compare average work with available server time, but by themselves they do not specify which class receives service at an instant. Under other service rules, reentrant lines can amplify queued fluid despite every station being nominally underloaded; the same paper gives such an example. A formal proof therefore has to use the precise LBFS priority condition, not only the flow equations and the load inequalities. The regular-time argument must then yield a single bound valid across every possible fluid path. Dai and Weiss (1996), §§4–5.

Formalization scope

Lean represents classes and stations by finite index types. Their indices start at zero: Lean class $k-1$ corresponds to paper class $k$ , and LBFS is Fin.revPerm. The paths $Q$ and $T$ are functions on all real times, while the fluid equations and conclusions are imposed only for $t\ge0$ . The external arrival rate is one, as in the paper's normalization. The conditions that station idle capacity and priority-set unused capacity increase only when their relevant content is zero are expressed by constancy on each interval where that content stays positive. Service and fluid paths are not given extra continuity hypotheses; the fluid equations and monotonicity conditions provide the regularity used in the paper. Dai and Weiss (1996), pp. 116–119, 122–123.

The service requirements $m_k>0$ are explicit so $\mu_k=1/m_k$ has its intended value. The drift and emptying-time milestones explicitly assume $K>0$ , since their formula divides by the maximum station workload. The main theorem retains the universal quantification over lines; when $K=0$ , its normalization $|Q(0)|=1$ is impossible. A faithful solution predicate must include the priority condition (4.4), whose omission would change Theorem 4.4 into a false claim about all work-conserving policies. The definition layer, elementary real-analysis extinction lemma, and priority flow-rate relations are useful beyond this single stability theorem. Dai and Weiss (1996), pp. 117–125.

Selected references

J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. DOI: 10.1287/moor.21.1.115.

8 thms2 active usersReviewed

Dynamical Systems Stochastic Systems·Captain: mikedeng1

Stability and Instability of Fluid Models for Reentrant Lines 2: In Every Reentrant Line the First-Buffer-First-Served Fluid Model Is StableResearch Paper

Why priority rules in reentrant lines matter

Semiconductor wafer fabrication is the standard example of a reentrant line: every wafer follows the same long route through a set of machines, and visits several machines many times. Each visit is a separate processing step, and a machine with work waiting from several steps must choose which step to serve. Kumar (1993) proposed studying such lines through their buffer priority rules, and Lu and Kumar (1991) showed that a priority rule can make a line unstable even though every machine has spare capacity. The question is therefore not academic: a scheduling rule that looks reasonable can let queues grow without bound.

Dai (1995) reduced the positive Harris recurrence of a multiclass queueing network to the stability of a deterministic fluid model, and Dai and Weiss (1996) used this reduction to prove stability results for several reentrant lines. This mission formalizes their Theorem 4.3: under the First-Buffer-First-Served (FBFS) discipline, the fluid model of every reentrant line is stable whenever each station's nominal workload is below one. Kumar (1993) had proved the analogous statement for discrete deterministic systems.

Timeline:

1991. Lu and Kumar exhibit a two-station reentrant line that is unstable under a static priority rule with every workload below one.
1993. Kumar proves stability of FBFS and LBFS for discrete deterministic reentrant lines.
1995. Dai shows that stability of the fluid model implies positive Harris recurrence of the stochastic network.
1996. Dai and Weiss prove that the FBFS and LBFS fluid models of every reentrant line are stable (Theorems 4.3 and 4.4), and with Dai's theorem obtain stability of the stochastic networks.

Setting

A reentrant line has $I$ stations and $K$ classes. All fluid follows one route: it enters as class $1$ , becomes class $k+1$ when class $k$ is completed, and leaves after class $K$ . Class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$ , and $\mu_k = 1/m_k$ . The constituency of station $i$ is $C_i = \{k : \sigma(k) = i\}$ , and its nominal workload is $\rho_i = \sum_{k\in C_i} m_k$ . The exogenous arrival rate is $1$ . The standing assumption of the paper is

\rho_i < 1 \qquad (i = 1,\dots,I). \tag{1.7}

A fluid model solution is a pair of paths $Q(t) = (Q_k(t))_k$ , the fluid levels, and $T(t) = (T_k(t))_k$ , the cumulative service time given to each class, such that for $t \ge 0$ :

Q_k(t) = Q_k(0) + \mu_{k-1}T_{k-1}(t) - \mu_k T_k(t), \qquad Q_k(t) \ge 0,

with $\mu_0T_0(t) = t$ ; each $T_k$ starts at $0$ and is nondecreasing; and the idle time $U_i(t) = t - \sum_{k\in C_i}T_k(t)$ of each station is nondecreasing.

A buffer priority discipline is a permutation $\pi$ of the classes; a class $k$ has priority over a class $l$ at the same station when $\pi(k) < \pi(l)$ . Write $H_k = \{l \in C_{\sigma(k)} : \pi(l) \le \pi(k)\}$ , $T_k^+ = \sum_{l\in H_k}T_l$ , $U_k^+(t) = t - T_k^+(t)$ and $W_k^+ = \sum_{l\in H_k} m_l Q_l$ . Under preemptive resume, $U_k^+$ may increase only at times when $W_k^+ = 0$ (condition (4.4)): a station never idles toward the classes of priority at least that of $k$ while any of them holds fluid. FBFS is $\pi(k) = k$ , so earlier steps of the route have priority.

The fluid model is stable (Definition 1.3) if there is a time $\delta > 0$ such that every solution with $|Q(0)| = \sum_k Q_k(0) = 1$ has $Q(t) = 0$ for all $t \ge \delta$ .

Formalization targets

Goal: Theorem 4.3

For every reentrant line with $m_k > 0$ and (1.7),

\text{the fluid model (1.8)–(1.12), (4.4) with } \pi(k) = k \text{ is stable.}

The goal asserts existence of an emptying time; it does not fix the value.

Milestones

Lemma 2.2 (i): a nonnegative function has zero derivative wherever it vanishes and is differentiable.
Lemma 2.2 (ii): an absolutely continuous nonnegative $g$ whose derivative is at most $-\varepsilon$ wherever $g > 0$ vanishes from $g(0)/\varepsilon$ on, and is nonincreasing.
Proposition 4.2: at a regular time of a priority fluid model, an empty buffer has equal in- and out-flow rates, and at each station the highest-priority nonempty class satisfies $\sum_{k\in H_{k_0}} m_kd_k = 1$ while lower-priority classes have zero out-flow.
Inductive step (proof of Theorem 4.3): once buffers $1,\dots,k-1$ stay empty from $t_{k-1}$ on, buffer $k$ is empty from $t_k = t_{k-1} + Q_k(t_{k-1})m_k/(1 - \sum_{l\in H_k} m_l)$ on.
Emptying time (proof of Theorem 4.3): every solution with $|Q(0)| = 1$ is empty from

\delta = \sum_{k=1}^K m_k\frac{\prod_{l=1}^{k-1}(1-\sum_{j\in H_l\setminus\{l\}}m_j)}{\prod_{l=1}^{k}(1-\sum_{j\in H_l}m_j)}

on, which gives the goal with an explicit constant.

Significance

Combined with Dai's theorem (Theorem 1.1 of the paper), Theorem 4.3 gives positive Harris recurrence of every multiclass reentrant line operated under FBFS, under the distributional assumptions of that theorem, whenever (1.7) holds. Since Lu–Kumar-type examples show that priority rules can destabilize a network with spare capacity, a rule that is provably stable on every reentrant line is a meaningful guarantee. FBFS, together with LBFS, is the basic positive case against which the instability examples in the same paper (Theorem 5.1) are compared.

Formalizing the result adds a machine-checked version of the fluid model with priority constraints, stated for an arbitrary line rather than a fixed network, and a checked explicit emptying time. The result is proved in the paper; no machine-checked proof is known. The rate identities of Proposition 4.2 and the extinction lemma are reused by the LBFS mission of this series.

Difficulty

The fluid model gives the paths only as nondecreasing functions subject to equations; nothing says they are differentiable. Every argument about rates holds only at regular times, and the conclusion must be integrated back through absolute continuity, which itself must be derived from the monotonicity conditions. The priority condition (4.4) is an "increases only when empty" condition; turning it into the rate identity (4.6) at a regular point requires continuity of the fluid levels and a careful local argument. The induction over classes needs uniform control of every earlier buffer for all later times, not only at one instant, so a pointwise reading of "buffer $k-1$ is empty" is not enough. Finally, the explicit constant $\delta$ requires bounding the content of buffer $k$ at time $t_{k-1}$ by the total content, which may have grown since time $0$ .

Formalization scope

Classes and stations are Fin K and Fin I, 0-based: the paper's class $k$ is Lean index $k-1$ .
Paths are total functions ℝ → Fin K → ℝ; every equation is imposed on $t \ge 0$ only, and derivatives are taken at $t > 0$ .
Conditions (1.13) and (4.4) are in interval form (ConstantWhile): the idle process is constant on every interval of $[0,\infty)$ on which the content stays positive. This is equivalent to the paper's Stieltjes integral form for continuous paths.
Lipschitz continuity of the paths is not assumed; it follows from the monotonicity conditions.
$m_k > 0$ is an explicit hypothesis; the paper takes it for granted.
Priorities are Equiv.Perm (Fin K), FBFS is the identity; $|Q(0)|$ is $\sum_k Q_k(0)$ .
In Lemma 2.2 (ii) the printed strict " $\dot g(t) < -\varepsilon$ " is relaxed to " $\le -\varepsilon$ ", as every application requires; absolute continuity is dropped from Lemma 2.2 (i), where it is not needed. Both changes strengthen the lemma.
In the inductive step, "stay empty for $t > t_{k-1}$ " is read as $t \ge t_{k-1}$ , and the case $Q_k(t_{k-1}) = 0$ is included.
The stochastic network is not formalized; only the fluid model is.

A trivializing formalization is ruled out: the goal uses the priority fluid model, not the work-conserving one alone (which would claim that every work-conserving fluid model is stable, false by Theorem 5.1), and a sorry-free witness shows that the FBFS solution predicate has solutions with $|Q(0)| = 1$ , so stability is not vacuous.

Contributions welcome: the extinction lemma for absolutely continuous functions, the derivation of Lipschitz continuity from (1.10)–(1.12), and the rate identities of Proposition 4.2 are reusable beyond this mission.

Selected references

J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1) (1996) 115–134. https://doi.org/10.1287/moor.21.1.115
J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1) (1995) 49–77. https://doi.org/10.1214/aoap/1177004828
P. R. Kumar, Re-entrant lines, Queueing Systems 13 (1993) 87–110. https://doi.org/10.1007/BF01149327
S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Transactions on Automatic Control 36(12) (1991) 1406–1416. https://doi.org/10.1109/9.106159

8 thms2 active usersReviewed

Completed

Optimal Transport Optimization Probability·Captain: mikedeng1

Quantifying Distributional Model Risk via Optimal Transport 3: A Worst-Case Transport Plan Exists in a Locally Compact Normed Space under Growth Conditions on c and fResearch Paper

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

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$ .
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.
§5 display (p. 26): $I=\sup\{I(\pi):\pi\in\Phi'_{\mu,\delta}\}$ .
Proposition 9 (p. 26): on a Polish space, (P-Compactness) and (P-USC) give a primal optimizer.
Corollary 1, Step 1 (p. 28): (A1)–(A4) and $\lambda^*>0$ give (P-Compactness).
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

18 thms2 active usersReviewed

Completed

Optimal Transport Optimization Probability·Captain: mikedeng1

Quantifying Distributional Model Risk via Optimal Transport 2: The Worst-Case Probability of a Closed Set A Equals the Baseline Probability of Its Inflation {x : c(x, A) ≤ 1/λ*}Research Paper

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

Coupling form (§2.2, p. 5, for $f = 1_A$ ): $I = \sup\{\pi(S \times A) : \pi \in \Phi_{\mu,\delta}\}$ .
Indicator supremum (pp. 8–9): $\sup_{y}\{1_A(y) - \lambda c(x,y)\} = (1 - \lambda c(x,A))^+$ for $\lambda \ge 0$ .
(13) (p. 9): $I$ equals the infimum in (13).
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$ .
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$ .
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).

11 thms2 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Scheduling Deteriorating Jobs on a Single Processor I: Under Linear Deterioration, Sequencing by Increasing E(X_i)/α_i Minimizes the Expected MakespanResearch Paper

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

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.
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).

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.

6 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers I: Under a Lagrangian Saddle Point, ADMM Residuals Vanish and Objective Values ConvergeTextbook

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:

(3.10) holds along the iteration: $0\in\partial g(z^{k+1})+B^Ty^{k+1}$ (§3.3, p. 18);
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);
(A.3) $p^\star-p^{k+1}\le y^{\star T}r^{k+1}$ ;
(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))$ ;
(3.11) $p^k-p^\star\le-(y^k)^Tr^k+(x^k-x^\star)^Ts^k$ ;
the monotonicity step $(y^{k+1}-y^k)^T(B(z^{k+1}-z^k))\le0$ for $k\ge1$ (p. 110);
(A.6) $V^k-V^{k+1}\ge\rho\|r^{k+1}-B(z^{k+1}-z^k)\|_2^2$ ;
(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$ ;
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$ ;
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

13 thms2 active usersReviewed

Completed

Linear Optimization Optimization·Captain: mikedeng1

On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems 4: For Symmetric Cost and Right-Hand-Side Uncertainty, the Adaptability Gap Is at Most FourResearch Paper

Motivation

Two-stage optimization separates a decision made before uncertainty is observed from one made after a scenario is known. A fully adaptive policy can choose a different second-stage decision in each scenario, while a static robust solution commits to a single second-stage decision that works in every scenario. Static solutions can be simpler to implement, but their worst-case cost may be higher. Bertsimas and Goyal ask how large this cost difference can be when both the right-hand sides of the constraints and the second-stage prices vary. Their Theorem 5.1 gives a factor of four when the paired uncertainty set is symmetric and nonnegative, even when both stages contain integer variables.

The distinction matters in planning problems where one policy is fixed in advance and another could respond to realized demand or prices. A uniform bound lets a planner assess the cost of the static restriction without solving every adaptive policy exactly. The source is the authors' manuscript; all page and result numbers in this mission refer to that manuscript, not to the journal pagination.

Setting

Fix matrices $A\in\mathbb R^{m\times n_1}$ and $B\in\mathbb R^{m\times n_2}$ . A scenario $\omega\in\Omega$ supplies a right-hand side $b(\omega)\in\mathbb R_+^m$ and a second-stage cost vector $d(\omega)\in\mathbb R_+^{n_2}$ . The first-stage cost vector is $c\in\mathbb R_+^{n_1}$ . For a set $I$ of designated integer coordinates, write $D_I$ for the nonnegative real vectors whose coordinates in $I$ are integers. After relabelling, this is the paper's $\mathbb R_+^{n-p}\times\mathbb Z_+^p$ .

In the robust problem $\Pi_{\mathrm{Rob}}(b,d)$ , one first-stage decision $x\in D_{I_1}$ and one second-stage decision $y\in D_{I_2}$ must satisfy $Ax+By\ge b(\omega)$ for every scenario. Their cost is $c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty$ . In the adaptive problem $\Pi_{\mathrm{Adapt}}(b,d)$ , $x$ is still chosen once, but $y(\omega)\in D_{I_2}$ may depend on the scenario. Its constraints are $Ax+By(\omega)\ge b(\omega)$ for every $\omega$ , and its cost is $c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty(\omega)$ . The optimal values $z_{\mathrm{Rob}}(b,d)$ and $z_{\mathrm{Adapt}}(b,d)$ are infima over feasible decisions in these respective problems; these are models (1.5)–(1.6).

The paired uncertainty set is $I_{(b,d)}(\Omega)=\{(b(\omega),d(\omega)): \omega\in\Omega\}$ . It is symmetric when it contains a point $u^0$ such that $u^0+z$ belongs to the set exactly when $u^0-z$ does, for every displacement $z$ . The point $u^0$ is itself a scenario realization. The smallest coordinatewise bounding hypercube has lower and upper corners $(b^l,d^l)$ and $(b^h,d^h)$ ; its center is $((b^l+b^h)/2,(d^l+d^h)/2)$ . These are Definition 1.2 and displays (2.5)–(2.7).

Formalization targets

The adaptability gap

The goal is Theorem 5.1:

z_{\mathrm{Rob}}(b,d)\le 4z_{\mathrm{Adapt}}(b,d).

The factor applies to every nonnegative symmetric paired uncertainty set and to both continuous and mixed-integer decisions. The theorem does not require an optimal adaptive policy to attain its infimum. The milestones record the source's geometric Lemma 2.3 and the estimates labelled (5.1)–(5.4), which supply the center-scenario cost and feasibility statements with the explicit factor four. They are stated for arbitrary feasible adaptive policies so the conclusion also covers nonattained infima.

Significance

The result bounds the price of committing to a single second-stage decision, despite uncertainty in both the constraints and the objective. In this setting the comparison is independent of the number of scenarios and of the dimensions $m,n_1,n_2$ . The paper also considers right-hand-side-only uncertainty, positive sets, and hypercubes; this mission isolates its symmetric paired-uncertainty result §5.1.

The theorem is proved in the paper. The remaining formalization work is a machine-checked development of the model, the bounding-hypercube geometry, the cost inequalities, and the passage from arbitrary feasible policies to the optimal values. The resulting definitions of mixed-integer domains, robust and adaptive feasibility, and extended-real optimal values can also support the other results in this paper's mission series. The theorem statements here are open proof targets, with no machine-checked proofs claimed.

Difficulty

The worst-case maximizer of $d(\omega)^Ty(\omega)$ can vary with $\omega$ , and an adaptive policy can choose a different integer vector in every scenario. Selecting one of those vectors as a static decision therefore gives no immediate cost or feasibility guarantee. The point of symmetry is a realizable scenario, but it must control both components of every other paired scenario. Without nonnegative data, doubling the center-scenario decision may fail to cover a positive right-hand side, and the cost comparison can fail as well. Integer coordinates also constrain which scalings preserve the decision domain; the exact factor in the theorem is compatible with doubling, unlike arbitrary fractional rescalings.

Formalization scope

Vectors are real functions on finite index types, matrices use Mathlib's matrix-vector product, and inequalities are componentwise. The scenario set is the range of $\omega\mapsto(b(\omega),d(\omega))$ , with a product-space symmetry predicate. No probability measure or measurability structure is used in these worst-case problems. Both stages may have integer coordinates designated by sets $I_1,I_2$ ; no continuous-only second-stage restriction is imposed.

Optimal values and worst-case costs use extended real numbers. An infeasible problem has value $+\infty$ ; a real infimum over an empty feasible set would incorrectly return a default zero. Symmetry includes a center belonging to the scenario range, so the scenario set is nonempty. Combined with nonnegative coordinates, symmetry bounds every scenario coordinate and makes the bounding-hypercube endpoints meaningful. The hypotheses retain $c\ge0$ , $b(\omega)\ge0$ , and $d(\omega)\ge0$ , which the source uses in its factor-four estimate. A statement restricted to continuous recourse, an assumed optimal adaptive policy, or a zero-valued infeasible problem would not express this target.

The source prints $\mathbb Z_+^{n_2}$ in (1.5)–(1.6), although the model's second-stage integer count is $p_2$ ; the domain here follows the surrounding $p_2$ convention. Lemma 2.3 is stated here for nonnegative sets, the regime needed for its second inequality. Its coordinatewise suprema and infima agree with the printed maxima and minima in this bounded symmetric setting. Contributions to the shared domain and geometry lemmas, the mixed-integer scaling fact, and the optimal-value comparison are all useful to the goal.

Selected references

Dimitris Bertsimas and Vineet Goyal, On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems, authors' manuscript of Mathematics of Operations Research, 2010. DOI: 10.1287/moor.1090.0440.

9 thms2 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 2: Every Convex Bipartite Order Has a Realizer of Size 3Research Paper

Motivation

The single-machine scheduling problem $1|\mathrm{prec}|\sum w_j C_j$ asks for an order in which to process $n$ jobs, each with a processing time and a weight, on one machine, respecting a partial order of precedence constraints, so that the weighted sum of completion times is as small as possible. It is NP-hard, and the best known approximation ratio for general precedence constraints is $2$ . Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) relate the problem to the dimension theory of partial orders: their Theorem 3.2 states that when the precedence constraints are given together with a realizer of size $k$ , the problem has a $(2 - 2/k)$ -approximation algorithm. Small realizers of structured precedence orders therefore translate directly into better approximation ratios.

This mission formalizes one such structural result, Lemma 4.1 of the paper: every convex bipartite order has a realizer of size $3$ . Convex bipartite orders form a class of precedence constraints that lies strictly between strong bipartite orders and general bipartite orders (Möhring, 1989). Combined with Theorem 3.2, the lemma gives a $4/3$ -approximation for $1|\mathrm{prec}|\sum w_j C_j$ on this class. According to the authors, the bound $\dim \le 3$ for convex bipartite orders had not been known before.

Setting

A poset is a set $N$ with a reflexive, antisymmetric, transitive relation $P$ . Two elements $x, y$ are incomparable, written $x \parallel y$ , when neither $(x,y) \in P$ nor $(y,x) \in P$ ; the set of incomparable pairs is $\mathrm{inc}(P)$ . A linear extension of $P$ is a linear order $L$ on $N$ with $P \subseteq L$ . A linear order $L$ reverses the pair $(x,y)$ when $y < x$ in $L$ . A realizer of size $t$ is a family $L_1, \dots, L_t$ of linear extensions of $P$ such that every incomparable pair $(x,y)$ is reversed by at least one $L_i$ . The dimension $\dim(P)$ is the least $t$ for which a realizer of size $t$ exists.

A convex bipartite order has jobs $N = J^- \cup J^+$ split into minus jobs $J^- = \{j_1, \dots, j_a\}$ and plus jobs $J^+ = \{j_{a+1}, \dots, j_n\}$ . Each plus job $j_k$ carries two indices $1 \le l(k) \le r(k) \le a$ , and a minus job $j_i$ precedes $j_k$ exactly when $l(k) \le i \le r(k)$ . There are no other precedences: the predecessors of each plus job form a nonempty interval of consecutive minus jobs.

For the Appendix construction, the incomparable pairs are sorted into three sets $E_1, E_2, E_3$ according to the kinds of the two jobs, the order of their indices and, for a pair (plus job $j_i$ , minus job $j_j$ ), whether $j_j$ precedes some plus job of larger index than $i$ . The sets $\bar E_m = E_m \cup P$ describe what the $m$ -th linear order of the realizer must contain.

Formalization targets

Goal: Lemma 4.1

\text{For every convex bipartite order } (N, P):\quad \exists\, L_1, L_2, L_3 \text{ linear extensions of } P \text{ with } \forall (x,y) \in \mathrm{inc}(P)\ \exists m:\ y <_{L_m} x .

Equivalently, $\dim(P) \le 3$ . The goal holds for every numbering of the jobs and every choice of interval ends $l, r$ .

Milestones

Lemma A.1. $E_1, E_2, E_3$ partition $\mathrm{inc}(P)$ , and for each $m$ , $(x,y) \in E_m$ implies $(y,x) \notin E_m$ .
Lemma A.2. Under the Appendix's numbering of the plus jobs ( $i < j$ implies $l(i) \le l(j)$ ), each $\bar E_m$ is contained in a linear order on $N$ .

Significance

The result. Lemma 4.1 places convex bipartite orders among the classes of precedence constraints for which $1|\mathrm{prec}|\sum w_j C_j$ has an approximation ratio strictly below $2$ , namely $4/3$ through Theorem 3.2 of the paper. The bound is tight: a bipartite order has dimension $2$ exactly when it is a strong bipartite order (Möhring), so the bound $3$ cannot be lowered for the class of convex bipartite orders. Since $\dim(P) = 3$ also gives $\chi(G_P) = 3$ for the graph of incomparable pairs, a $3$ -realizer yields an optimal colouring of that graph.

Formalizing it. The result is proved in the paper, with a short case analysis in the Appendix. No machine-checked proof is known to exist. Mathlib has no dimension theory of posets: realizers, reversals of incomparable pairs and the construction of linear extensions containing a given acyclic relation have to be set up here. The definitions of realizer and linear extension are stated for an arbitrary relation and can be reused for other dimension bounds (interval orders, semiorders, the other missions of this series).

Difficulty

The three relations $\bar E_m$ are not partial orders. $\bar E_2$ , for instance, is not transitive: with two minus jobs and one plus job $j_3$ with $l(3) = r(3) = 2$ , the pairs $(j_1, j_2) \in E_2$ and $(j_2, j_3) \in P$ are present but $(j_1, j_3)$ lies in $E_1$ . The step that requires work is to show that each $\bar E_m$ has no cycle, so that it extends to a linear order. For $\bar E_2$ this depends on the convexity of the predecessor intervals and on the numbering of the plus jobs by their left ends: it is not a consequence of bipartiteness alone. The goal itself carries no numbering assumption, so any proof must also account for renumbering the plus jobs.

Formalization scope

All declarations live in the namespace SingleMachinePrec.ConvexBipartite.

Relations. A relation on $N$ is a predicate N → N → Prop. Linear orders use Mathlib's unbundled class IsLinearOrder. A linear extension of $P$ is a linear order $L$ with $P \subseteq L$ ; $L$ reverses $(x,y)$ when $L\,y\,x$ and $y \ne x$ . A realizer of size $t$ is a function Fin t → N → N → Prop, so repeated members are allowed, as in the paper's multisets.
Convex bipartite orders. The jobs are the type Fin a ⊕ Fin b: Sum.inl i is the minus job $j_{i+1}$ , Sum.inr k the plus job $j_{a+k+1}$ , with indices starting at $0$ . The interval ends are maps l r : Fin b → Fin a with l k ≤ r k, and $P$ is equality together with the pairs (minus $i$ , plus $k$ ) with $l(k) \le i \le r(k)$ . A file-level instance records that $P$ is a partial order. Any convex bipartite order in the paper's sense is one of these after naming its jobs. The cases $a = 0$ and $b = 0$ are allowed.
$E_1, E_2, E_3$ . Each set is defined as "incomparable and satisfies the paper's case condition". In the plus–minus clauses, " $k > i$ " compares plus indices, because $k$ exceeds the index of a plus job.
Lemma A.2. " $\bar E_m$ is an extension of $P$ " is formalized as "there is a linear order containing $\bar E_m$ ", which is what the paper's proof establishes (absence of cycles) and what its final paragraph uses. Reading it as " $\bar E_m$ is a partial order" would make the lemma false (see Difficulty). The Appendix's numbering assumption is the hypothesis Monotone l of this milestone only.
Algorithmic wording not formalized. The paper states Lemma 4.1 as "a realizer of size 3 can be computed in polynomial time". What is formalized is the existence of the realizer; the running time is not.

A trivializing formalization would let the members of the realizer be arbitrary relations, which makes reversing every pair free. Here every member must be a linear order containing $P$ .

Contributions welcome: proofs of the two milestones and of the goal; a general lemma that a relation whose transitive closure is antisymmetric extends to a linear order on a finite type; and the renumbering argument that removes the numbering assumption.

Selected references

C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992.
R. H. Möhring, Computationally tractable classes of ordered sets, in I. Rival (ed.), Algorithms and Order, NATO ASI Series 255, Kluwer, 1989, pp. 105–193.
W. T. Trotter, Combinatorics and Partially Ordered Sets: Dimension Theory, Johns Hopkins University Press, 1992.

7 thms2 active usersReviewed

Completed

Algebraic Geometry Differential Geometry Linear Optimization+1·Captain: mikedeng1

Log-Barrier Interior Point Methods Are Not Strongly Polynomial 2: The Total Curvature of the Central Path of LW_r(t) Exceeds (2^(r−2) − 1)π/2 − ε for All Large tResearch Paper

Motivation: curvature of the central path as a complexity measure

Path-following interior point methods solve a linear program by tracking its central path, a smooth curve that runs through the interior of the feasible set and ends at an optimal solution. Their number of iterations is polynomial in the bit size of the input, and whether some interior point method is strongly polynomial (bounded by a polynomial in the number of variables and constraints alone) is open. Bayer and Lagarias called the central path "a fundamental mathematical object underlying Karmarkar's algorithm". Dedieu and Shub proposed its total curvature as an informal complexity measure: a path that turns little should be easy to follow with straight steps. Several results bound that curvature:

2005. Dedieu and Shub conjecture that the total curvature of the central path is bounded linearly in the dimension. Dedieu, Malajovich and Shub prove an $O(n)$ bound on average over the regions of a hyperplane arrangement. De Loera, Sturmfels and Vinzant later obtain the same averaged bound with matroid methods (arXiv:1012.3978).
2008–2009. Deza, Terlaky and Zinchenko build redundant Klee–Minty cubes and "snakes" with curvature $\Omega(m)$ for $m$ inequalities, which refutes the dimension version. They then conjecture the continuous analogue of the Hirsch conjecture: the total curvature is bounded linearly in the number of constraints.
2014–2017. Allamigeon, Benchimol, Gaubert and Joswig disprove that conjecture with a family of linear programs whose central paths have curvature exponential in the number of constraints. The bound first appeared in arXiv:1405.4161 and was given an elementary tropical proof in arXiv:1708.01544v2, Theorem 25, which is the result of this mission.

Setting

A linear program in slack form has a real $m\times n$ matrix $A$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ and $N:=n+m$ :

\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. } Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .

For $\mu>0$ the point of the central path $(x^\mu,w^\mu,s^\mu,y^\mu)\in\mathbb R^{2N}$ is the unique solution of

Ax+w=b,\quad s-A^\top y=c,\quad x_js_j=\mu,\quad w_iy_i=\mu,\quad x,w,s,y>0. \tag{1}

The primal central path is $\mu\mapsto(x^\mu,w^\mu)\in\mathbb R^N$ .

For $r\ge1$ and $t>0$ , the program $\mathbf{LW}_r(t)$ minimizes $x_1$ over $x\in\mathbb R^{2r}$ subject to

x_1\le t^2,\quad x_2\le t,\quad x_{2j+1}\le t\,x_{2j-1},\quad x_{2j+1}\le t\,x_{2j},\quad x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ \ (1\le j<r),\quad x\ge0 .

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$ , $m=3r-1$ , $N=5r-1$ .

For points $U,V,W$ of Euclidean space with $U\ne V\ne W$ , the turning angle $\angle UVW\in[0,\pi]$ is the angle between the vectors $V-U$ and $W-V$ . For a curve $\sigma$ parameterized over $I\subseteq\mathbb R$ , the total curvature is

\kappa(\sigma,I)=\sup\Big\{\sum_{k=1}^{p-1}\angle\,\sigma(\mu_{k-1})\sigma(\mu_k)\sigma(\mu_{k+1})\ :\ \mu_0<\dots<\mu_p\ \text{in } I\Big\}\in[0,+\infty].

The milestones also use the field $\mathbb K$ of absolutely convergent generalized real Puiseux series $\sum_{\alpha\in\mathbb R}a_\alpha t^\alpha$ . Such a series can be evaluated at large real $t$ , and it has a valuation $\mathrm{val}\in\mathbb T=\mathbb R\cup\{-\infty\}$ , its leading exponent. Read over $\mathbb K$ , $\mathbf{LW}_r$ is one linear program. The valuation of its central path at $\mu=t^\lambda$ is the tropical central path $\mathcal C^{\mathrm{trop}}(\lambda)\in\mathbb R^{2N}$ , a piecewise-linear curve with an explicit recursive description (Propositions 20–21 of the paper).

Formalization targets

Goal: Theorem 25

For every $r\ge1$ and $\epsilon>0$ there is $t_0$ such that for all $t>t_0$ ,

\kappa\big(\mu\mapsto(x^\mu,w^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon\quad\text{and}\quad\kappa\big(\mu\mapsto(x^\mu,w^\mu,s^\mu,y^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon

for the central path of $\mathbf{LW}^=_r(t)$ . Here $t_0$ may depend on $r$ and $\epsilon$ . Both the primal and the primal-dual curves are part of the goal, as in the paper.

Milestones, in the order of the paper's argument

Lemma 22: for non-null $\mathbf x,\mathbf y\in\mathbb K^d$ , the angle $\angle\mathbf x(t)\mathbf y(t)$ has a limit, which is $\pi/2$ when the arg maxes of $\mathrm{val}\,\mathbf x$ and $\mathrm{val}\,\mathbf y$ are disjoint.
Lemma 23: the turning angle $\angle\mathbf U(t)\mathbf V(t)\mathbf W(t)\to\pi/2$ when $\max\mathrm{val}\,\mathbf U<\max\mathrm{val}\,\mathbf V<\max\mathrm{val}\,\mathbf W$ and the arg maxes of $\mathrm{val}\,\mathbf V$ and $\mathrm{val}\,\mathbf W$ are disjoint.
Proposition 24: $\liminf_{t}\kappa(\mathcal C_t,[t^{\lambda_0},t^{\lambda_p}])\ge\sum_{k=1}^{p-1}\angle^*\mathcal C^{\mathrm{trop}}(\lambda_{k-1})\mathcal C^{\mathrm{trop}}(\lambda_k)\mathcal C^{\mathrm{trop}}(\lambda_{k+1})$ , where $\angle^*$ is the weak tropical angle ( $\pi/2$ under the conditions of Lemma 23, else $0$ ).
Table 1: the coordinates of the tropical central path of $\mathbf{LW}_r$ at $\lambda=(4k+2c)/2^j$ .
Claims in the proof of Theorem 25 (p. 23): on $[0,2]$ the dual coordinates of $\mathcal C^{\mathrm{trop}}$ are at most $\max(0,\lambda-1)$ . At $\lambda_k=4k/2^{r-1}$ the largest coordinate is $r-1+(2k+2)/2^{r-1}$ , attained only by $w_{3(r-1)}$ or $w_{3(r-1)+1}$ . Hence $\angle^*=\pi/2$ at each interior subdivision point.

Significance

The theorem shows that the total curvature of the central path is not bounded by any polynomial in the number of constraints: $\mathbf{LW}_r$ has $3r+1$ constraints and curvature at least about $2^{r-2}\pi/2$ . This settles the conjecture of Deza, Terlaky and Zinchenko in the negative. It also shows that the averaged upper bounds of Dedieu–Malajovich–Shub and De Loera–Sturmfels–Vinzant cannot hold for every region. A companion mission of this series formalizes the paper's second main result, an exponential lower bound on the number of iterations of log-barrier path-following methods on the same family.

The result is proved on paper. As far as is known, it has not been formalized in any proof assistant, and Mathlib has no notion of the total curvature of a curve, of Puiseux-series evaluation and valuation, or of the tropical central path. Formalizing the theorem would give a machine-checked reference point for a much-cited negative result in interior point theory. The Lean definitions of total curvature and of the turning angle are general and reusable.

Difficulty

The total curvature is a supremum over inscribed polygons, and a lower bound needs explicit polygons whose angles can be estimated for every large $t$ . The central path of $\mathbf{LW}^=_r(t)$ has no closed form, so its points cannot be written down at given parameters $\mu$ . Numerical evidence at a fixed $t$ says nothing uniform in $r$ . The natural first idea, to compute the path's angles directly from system (1) for a fixed instance, gives no handle on how the number of turns grows with $r$ . What is needed is control of the path's geometry uniformly over the whole scale of $t$ , with $2^{r-2}$ turns located at once, and the threshold $t_0$ is not explicit.

Formalization scope

Vectors in which angles are measured are EuclideanSpace ℝ (Fin d). The turning angle is InnerProductGeometry.angle (V - U) (W - V), not Mathlib's vertex angle ∠ U V W, which is $\pi$ minus it. A degenerate triple ( $U=V$ or $V=W$ ) contributes angle $0$ . Total curvature is an EReal-valued supremum over strictly increasing parameter sequences in the parameter set, and the goal uses the set $(0,\infty)$ . The primal and primal-dual curves are the vectors $(x,w)\in\mathbb R^{5r-1}$ and $(x,w,s,y)\in\mathbb R^{2(5r-1)}$ . System (1) is the published Vanderbei central-path system with objective $-c$ . The goal quantifies over every curve solving (1) for all $\mu>0$ . Existence and uniqueness of that curve is the referenced platform statement VanderbeiLP.CentralPath.central_path_exists_unique and is not posed again. Indices are the paper's, 1-based, mapped to Fin by subtracting one. Powers $2^{r-2}$ use integer exponents of the real number $2$ .

A trivializing formalization is ruled out explicitly: the curvature is a supremum in EReal (a real sSup of an unbounded set would be $0$ ), the turning angle is not the vertex angle, and degenerate polygons cannot add spurious right angles.

Lemmas 22–24 are stated over a model of $\mathbb K$ by coefficient functions with the paper's support and absolute-convergence conditions. Equalities, products and order in $\mathbb K$ are expressed through evaluation at all sufficiently large $t$ , which is how the paper characterizes them. Table 1 and the claims of the proof are stated for the explicit tropical central path of $\mathbf{LW}_r$ given by Propositions 20–21 (milestones of the companion mission), written as a definition here. One repair: the paper's "uniquely attained" claim fails at $r=2$ , $k=0$ , where $w_1=w_4=2$ . It is stated with that case excluded, which the proof does not use.

Welcome contributions: a general theory of total curvature of curves (monotonicity under refinement, behaviour under limits), asymptotics of evaluated Puiseux series, and the comparison between the central path over $\mathbb K$ and its real specializations.

Selected references

X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-Barrier Interior Point Methods Are Not Strongly Polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; preprint v2 (cited throughout) arXiv:1708.01544, doi:10.1137/17M1142132.
X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Long and winding central paths, preprint, 2014. arXiv:1405.4161
J. A. De Loera, B. Sturmfels, C. Vinzant, The central curve in linear programming, Found. Comput. Math. 12(4), 2012. arXiv:1012.3978
J.-P. Dedieu, G. Malajovich, M. Shub, On the curvature of the central path of linear programming theory, Found. Comput. Math. 5(2), 2005.
J.-P. Dedieu, M. Shub, Newton flow and interior point methods in linear programming, Int. J. Bifurcation and Chaos 15(3), 2005.
A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Springer, 2009.
L. van den Dries, P. Speissegger, The real field with convergent generalized power series, Trans. Amer. Math. Soc. 350(11), 1998.

18 thms2 active usersReviewed

Completed

Analysis·Captain: mikedeng1

Regret in Decision Making under Uncertainty 2: With u(x, y) = x + f(x − y) and f Decreasingly Concave, the Same Decision Maker Takes a Fair Long-Odds Bet and Buys Fair InsuranceResearch Paper

Motivation

Expected utility theory explains a single attitude toward risk by the curvature of a utility function of final wealth: a concave utility makes a decision maker risk averse, a convex one risk seeking. Several well documented patterns of behaviour do not fit this picture. The same people buy insurance against small-probability losses and buy lottery tickets with small-probability gains (Friedman and Savage, 1948, doi:10.1086/256692); subjects who are risk averse for gains are risk seeking for the mirrored losses, the reflection effect; and subjects who are indifferent between full insurance and bearing a risk reject half-price insurance that pays only half the time, probabilistic insurance (Kahneman and Tversky, 1979, doi:10.2307/1914185).

David E. Bell's 1982 paper Regret in Decision Making under Uncertainty (doi:10.1287/opre.30.5.961) proposes that a decision maker cares not only about what she obtains but also about what she would have obtained had she chosen differently. Its first part (the companion mission of this series) derives the representation $u(x,y)=\alpha v(x)+f(v(x)-v(y))$ ; its Section 2 shows that the single additive form with linear $v$ explains all of the patterns above at once, provided the regret function $f$ is decreasingly concave. Regret theory, developed at the same time by Loomes and Sugden (1982, doi:10.2307/2232669), remains one of the standard alternatives to expected utility in decision analysis and behavioural economics.

Setting

A decision maker chooses between two alternatives $a$ and $b$ . Uncertainty is described by finitely many states $i$ with probabilities $\pi_i$ ; in state $i$ alternative $a$ gives final assets $a_i$ and $b$ gives $b_i$ . Choosing $a$ means forgoing $b$ , and an outcome is valued by the regret utility

u(x,y)=x+f(x-y),

where $x$ is the final assets received, $y$ the assets the foregone alternative would have given in the same state, and $f:\mathbb R\to\mathbb R$ the regret function. The expected utility of selecting $a$ when $b$ is foregone is

\mathrm{EU}_\pi(a\,|\,b)=\sum_i \pi_i\,u(a_i,b_i),

and $a$ is strictly preferred to $b$ when $\mathrm{EU}_\pi(b\,|\,a)<\mathrm{EU}_\pi(a\,|\,b)$ (the paper's inequality (1)); $a$ and $b$ are indifferent when the two expected utilities are equal.

The comparisons are given by three payoff tables. Table II: a horse wins with probability $p$ ; betting $\$ p $gives$ 1-p $if it wins and$ -p $if it loses, not betting gives$ 0 $. Table III: a car is damaged with probability$ p $at a cost of$ 1 $; insuring gives$ -p $in both states, not insuring gives$ -1 $or$ 0 $. Table IV: an accident has probability$ q $; self insurance gives$ -1 $or$ 0 $, full insurance$ -p $always, and probabilistic insurance, which charges half the premium and pays with probability one half given an accident, gives$ -p $,$ -1 $or$ -p/2$.

The regret function $f$ is decreasingly concave if it is twice differentiable with strictly increasing second derivative $f''$ . Section 3 also uses $g(r)=r+f(r)-f(-r)$ and the negative exponential $f(r)=1-e^{-\gamma r}$ , $\gamma>0$ .

Formalization targets

Goal: coexistence of insurance and gambling

If $f$ is decreasingly concave and $0<p<\tfrac12$ , then the bet of Table II is strictly preferred to not betting and insuring in Table III is strictly preferred to not insuring:

p\,[f(1-p)-f(p-1)]>(1-p)\,[f(p)-f(-p)].

Both comparisons have equal expected values, so the statement is a pure regret effect. The goal fixes no constants and assumes nothing about $f$ beyond decreasing concavity; it is the weakest hypothesis the page offers.

Milestones

Display (5): the bet is preferred iff the inequality above; display (6): insurance is preferred iff the same inequality, so the two preferences coincide.
The inequality holds for $0<p<\tfrac12$ whenever $(f(x)-f(-x))/x$ is strictly increasing on $x>0$ ; and that ratio is strictly increasing whenever $f''(x)>f''(-x)$ for $x>0$ .
The reflection effect (Sec. 2(ii)): $x_2$ for sure is indifferent to the lottery $(p:x_1;\,1-p:x_3)$ iff $-x_2$ for sure is indifferent to $(p:-x_1;\,1-p:-x_3)$ .
Probabilistic insurance (Sec. 2(iii)): display (9) characterises indifference between full and self insurance; under (9) and $0\le q<1$ ,

f(p/2)-f(-p/2)<\tfrac12\,[f(p)-f(-p)]\qquad(11)

holds iff full insurance is strictly preferred to probabilistic insurance, iff probabilistic insurance is strictly preferred to self insurance; and (11) follows from the same ratio condition. 5. The negative exponential (Sec. 3): $f$ concave, $g$ convex on $r\ge0$ , $g(r)/r$ strictly increasing on $r>0$ , and $f$ decreasingly concave.

Significance

The goal is the paper's central behavioural claim: one regret function explains why the same decision maker gambles on long odds and buys insurance at fair prices, behaviour that a single concave or convex utility of wealth cannot produce. The milestones show that the reflection effect and the rejection of probabilistic insurance follow from the same model, and two of them reduce to the same inequality on the odd part $f(x)-f(-x)$ of the regret function. The negative exponential example shows the hypotheses are met by a concrete, commonly used function, so the explanation is not vacuous.

The results are proved in the paper by short calculations, and none of them has been machine-checked before. The mission produces a formal statement of the regret model of Section 2 with its payoff tables, which pins down several points the printed text leaves loose: the meaning of "decreasingly concave", the domain on which "increasing" and "convex" are meant, and three misprinted intermediate displays.

Difficulty

The comparisons (5), (6), (9) and the reflection identity are algebraic once the payoff tables are expanded; the work is in expanding them correctly, since the foregone argument of $u$ changes with the alternative selected and three printed expansions are wrong. The substance lies in the analytic step: passing from a pointwise condition on $f''$ to strict monotonicity of $(f(x)-f(-x))/x$ on $(0,\infty)$ , with strict inequalities throughout and through a quotient that is undefined at $0$ . The naive reading of the page's condition, " $f''(x)>f''(-x)$ for all $x$ ", is unsatisfiable and cannot be used as a hypothesis.

Formalization scope

All quantities are real numbers. The utility is regretU f x y = x + f (x - y), i.e. form (4) with $v(x)=x$ exactly; the page assumes $v$ only "approximately linear" but computes every display with $v(x)=x$ . A comparison is a finite state space Fin n with a real weight vector; the theorems instantiate it with $(p,1-p)$ for Tables II–III and with $(q/2,q/2,1-q)$ for Table IV, the accident state split by whether the insurer pays. Strict preference is strict inequality of expected regret utilities; indifference is equality.

Conventions and corrections, each disclosed in the item concerned:

"Decreasingly concave" is not defined in the paper; it is read as Differentiable ℝ f, Differentiable ℝ (deriv f) and StrictMono (deriv (deriv f)). The page's presumption that $f$ is increasing and concave is not assumed.
"Increasing" is read strictly, because the conclusions (5), (6), (11) are strict, and on $x>0$ , because $(f(x)-f(-x))/x$ is undefined at $0$ and even.
" $f''(x)>f''(-x)$ for all $x$ " is read for $x>0$ .
The convexity of $g$ in the exponential example is stated on $r\ge0$ : $g(r)=r+2\sinh(\gamma r)$ is concave for $r<0$ , as the paper itself notes on p. 977.
Misprints corrected: the last bracket of the second reflection equality on p. 973; $f(p/2)$ for $f(-p/2)$ in the expansion before (10) and in the probabilistic-versus-self display on p. 975, which also lacks a factor $q$ . The normalisation $f(0)=0$ is not needed.
The equivalences (5), (6), (9) and the reflection identity hold for every real probability and are stated without a range; the goal keeps $0<p<\tfrac12$ and the probabilistic-insurance statement keeps $0\le q<1$ .

The goal cannot be satisfied vacuously: the negative exponential milestone exhibits a decreasingly concave $f$ , and the conclusion is a strict preference between two alternatives of equal expected value. Section 2(iv) (preference reversals) is not formalized: its printed rewriting of (12) in terms of $h$ drops a linear term and its conclusion is unquantified ("for sufficiently small units of money").

Contributions welcome: proofs of the algebraic reductions, the slope argument for $(f(x)-f(-x))/x$ , and the convexity facts for $\sinh$ ; the latter two are reusable beyond this mission.

Selected references

D. E. Bell, Regret in Decision Making under Uncertainty, Operations Research 30(5), 961–981, 1982. doi:10.1287/opre.30.5.961
D. Kahneman and A. Tversky, Prospect Theory: An Analysis of Decision under Risk, Econometrica 47(2), 263–291, 1979. doi:10.2307/1914185
G. Loomes and R. Sugden, Regret Theory: An Alternative Theory of Rational Choice under Uncertainty, The Economic Journal 92(368), 805–824, 1982. doi:10.2307/2232669
M. Friedman and L. J. Savage, The Utility Analysis of Choices Involving Risk, Journal of Political Economy 56(4), 279–304, 1948. doi:10.1086/256692

12 thms2 active usersReviewed

Combinatorics Probability Theoretical Computer Science·Captain: mikedeng1

Online Stochastic Matching: Beating 1-1/e 1: When OPT = Ω(n), the Two Suggested Matchings Algorithm Achieves ALG/OPT ≥ (1 − 2/e²)/(4/3 − 2/(3e)) − ε ≈ 0.670 with Probability 1 − e^(−Ω(n))Research Paper

Motivation

Online bipartite matching models a platform that must commit each arriving request to a resource immediately. The motivating application of Feldman, Mehta, Mirrokni and Muthukrishnan is display advertising: an ad server knows from past traffic how many impressions of each type (web page, audience segment) to expect, sells them to advertisers in advance, and must assign each impression to an interested advertiser the moment a user loads the page. The goal is to fill as many contracted impressions as possible.

When arrivals are chosen by an adversary, the best ratio an online algorithm can guarantee is $1 - 1/e \approx 0.632$ , achieved by the RANKING algorithm of Karp, Vazirani and Vazirani (STOC 1990). The ad server, however, is not facing an adversary: it has a forecast. The i.i.d. model captures this: the graph and the distribution of impression types are known in advance, and the impressions are independent draws. The paper asks whether this knowledge allows an online algorithm to beat $1 - 1/e$ , and answers yes.

Timeline.

1990: Karp, Vazirani and Vazirani give RANKING, with ratio $1 - 1/e$ for adversarial arrivals, and show this is optimal in that model.
2005: Mehta, Saberi, Vazirani and Vazirani obtain $1 - 1/e$ for the budgeted AdWords generalization.
2009: Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) show that in the i.i.d. model the two suggested matchings algorithm achieves about $0.670$ with high probability when OPT is linear in $n$ , the first ratio above $1 - 1/e$ for this model, and that no online algorithm reaches $26/27$ in expectation.

Setting

An instance is a bipartite graph $G = (A, I, E)$ with a finite set $A$ of advertisers, a finite set $I$ of impression types, and edges $E \subseteq A \times I$ recording which advertisers want which types. The mission treats the case analysed throughout §4.2 of the paper, in which one impression of each type is expected ( $e_i = 1$ ). So $n = |I|$ impressions arrive one at a time, with types $\omega(0), \dots, \omega(n-1)$ drawn independently and uniformly from $I$ . On arrival an impression must be assigned at once and irrevocably to a still unassigned advertiser adjacent to its type, or discarded. $\mathrm{ALG}(\omega)$ is the number of impressions an algorithm assigns. $\mathrm{OPT}(\omega)$ is the size of a maximum matching of the realization graph, which has one node per arrival $t$ , joined to every advertiser $a$ with $(a, \omega(t)) \in E$ .

The two suggested matchings (TSM) algorithm works offline first. Its boosted flow graph $G_f$ has a source arc of capacity $2$ into every advertiser, a unit-capacity arc along every edge of $E$ , and an arc of capacity $2$ from every type to a sink. The algorithm takes the edge set $E_f$ of an integral maximum flow. Every vertex then has at most two edges of $E_f$ , so $E_f$ splits into vertex-disjoint paths and cycles. The algorithm colours each component blue and red:

on cycles, the colours alternate;
on odd paths, the colours alternate, with more blue than red;
on even paths between advertisers, the colours alternate;
on even paths between types, the first two edges are blue, then the colours alternate, ending in blue.

Online, the first arrival of type $i$ tries the advertiser along $i$ 's blue edge, the second tries the one along its red edge, and later arrivals are discarded. A tried advertiser that is already taken is not reassigned. The advertisers fall into four classes by their coloured edges: $A_{BR}$ (one blue, one red), $A_{BB}$ (two blue), $A_B$ (one blue only) and $A_R$ (one red only).

Formalization targets

Goal: Theorem 5, first sentence, $e_i = 1$

Let

\alpha = \frac{1 - 2/e^2}{4/3 - 2/(3e)} \approx 0.67029 .

The goal has three parts. First, every maximum flow edge set admits a colouring that follows the rules. Second, for every $\varepsilon > 0$ and $c > 0$ there are $\delta > 0$ and $N$ such that, for every instance with $n \ge N$ , every maximum flow edge set and every rule-following colouring,

\Pr_\omega\big[\ \mathrm{OPT} \ge c\,n \implies \mathrm{ALG} \ge (\alpha - \varepsilon)\,\mathrm{OPT}\ \big] \;\ge\; 1 - e^{-\delta n}.

Third, $\alpha > 1 - 1/e$ .

Milestones

Facts 1 and 2: concentration for two balls-in-bins statistics.
The note of §4.2.1: each type has no coloured edge, one blue edge, or one blue and one red edge.
Equation (1): $|E_f| = 2|A_{BR}| + 2|A_{BB}| + |A_B| + |A_R|$ .
Equation (2): with high probability, $\mathrm{ALG} \ge (1 - 1/e^2)|A_{BB}| + (1 - 2/e^2)|A_{BR}| + (1 - 3/(2e))(|A_B| + |A_R|) - 4\varepsilon n$ .
Equation (3): $|E_f| = 2(|A_T| + |I_S|) + |E_\delta|$ for the surgered residual cut $(S,T)$ of $G_f$ .
Equation (4): with high probability, $\mathrm{OPT} \le |A_{BR}| + |A_{BB}| + \tfrac12(|A_B| + |A_R|) + (\tfrac12 - \tfrac1e)|E_\delta| + \varepsilon n$ .
Lemma 1: $|E_\delta| \le \tfrac23|A_{BR}| + \tfrac43|A_{BB}| + |A_B| + \tfrac13|A_R|$ .

Significance

The theorem separates the i.i.d. model from the adversarial one: knowing the distribution is worth a constant factor above $1 - 1/e$ . The suggested matching algorithm of the same paper (Theorem 4) shows that following a single offline matching gets exactly $1 - 1/e$ , so the second, red matching is what crosses the barrier. The paper's question started a line of work on the i.i.d. and random-order models, with later improvements to the constant by other authors under further assumptions.

The result has a written proof but, as far as the platform record shows, no machine-checked one. The mission formalizes the paper's own argument: the flow-and-colouring construction, the balls-in-bins concentration facts, the cut-based bound on OPT and the combinatorial Lemma 1. It also fixes two slips in the printed statements (see Formalization scope). The pieces are reusable beyond this paper. The occupancy concentration (Fact 1) and the satisfied-sequences bound (Fact 2) recur in analyses of online algorithms with stochastic input. The degree-capped flow encoding and its path/cycle decomposition are standard tools for 2-matchings.

Difficulty

The upper bound on OPT is the delicate part. A cut of the flow graph bounds the maximum matching of the realization graph only after a second surgery that depends on the random arrivals. Its size must then be compared with the colour classes, which are defined by a different structure (the components of $E_f$ ). Lemma 1 bridges the two, and it depends on the exact colouring rules: a colouring that only satisfies local degree conditions can put red edges at both ends of an even advertiser path, which breaks the inequality $|A_B| \ge |A_R|$ behind (2). On the probabilistic side, the advertisers of $A_{BR}$ share impression types with each other, so the success events are dependent, and Fact 2 needs a bounded-differences argument in which one ball affects up to $d$ sequences.

Formalization scope

All declarations live in the namespace OnlineStochMatching.TSM. Advertisers and types are finite types A I : Type, and $E$ is a Finset (A × I). Probabilities are counting ratios $\#\{\omega : \mathrm{Fin}\ n \to I \mid P\,\omega\}/|I|^n$ , so there are no measurability side conditions. OPT is a maximum over the finite, nonempty set of partial injective assignments. An integral flow of $G_f$ is its set of saturated middle edges, i.e. a subset of $E$ with at most two edges per vertex; $E_f$ is such a set of maximum cardinality. A colouring is given by a listing of the components of $E_f$ as vertex sequences. Every theorem quantifies over every maximum $E_f$ and every colouring the rules allow, since the paper fixes neither.

The paper's asymptotic phrases are replaced by explicit quantifiers that come from its own proofs:

"with probability $1 - e^{-\Omega(n)}$ " and "with high probability" (Theorem 5, (2), (4)) become: $\exists\, \delta > 0,\ \exists\, N$ , chosen before the instance, with probability at least $1 - e^{-\delta n}$ for all $n \ge N$ ;
"as long as OPT $= \Omega(n)$ " becomes the event $\mathrm{OPT} \ge c\,n$ for an arbitrary $c > 0$ fixed before $\delta$ and $N$ ;
the $O(1)$ term in the bound on $|A^*_\delta|$ (p. 8) is absorbed into $\varepsilon n$ for $n \ge N$ .

Corrections to the printed statements:

Theorem 5 prints $\mathrm{ALG}/\mathrm{OPT} - \epsilon \ge \alpha$ ; the proof concludes $\mathrm{ALG}/\mathrm{OPT} + \epsilon \ge \alpha$ , so the goal states $\mathrm{ALG} \ge (\alpha - \varepsilon)\mathrm{OPT}$ ;
Fact 1 prints the failure probability $2e^{-\epsilon n/2}$ ; its proof gives $2e^{-\epsilon^2 n/2}$ , which is used;
Fact 2 states two hypotheses its proof uses: the bins of a sequence are distinct, and $c^2 < n$ .

The ratio is multiplied out, so no division by OPT occurs. A colouring condition that is unsatisfiable, or a flow set that is not maximum, would make the goal vacuous or false; part (a) of the goal rules out the first, and every statement requires maximality. Not included: the reduction to general integer $e_i$ (§4.2.4), the tightness sentence of Theorem 5 (§4.2.5), and footnote 7's variant of the algorithm.

Useful infrastructure: bounded-differences (McDiarmid/Azuma) inequalities for functions of i.i.d. uniform variables, which exist on the platform as separate theorems; path/cycle decomposition of graphs of maximum degree two; and max-flow min-cut for unit-capacity bipartite networks. Contributions are welcome on Facts 1 and 2 independently of the combinatorics, and on Lemma 1 and equations (1) and (3), which are deterministic.

Selected references

J. Feldman, A. Mehta, V. Mirrokni, S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, FOCS 2009; arXiv:0905.4100v1. https://arxiv.org/abs/0905.4100
R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and generalized online matching, FOCS 2005; J. ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321

13 thms2 active usersReviewed

Operations Research

Missions

Wait-and-Judge Scenario Optimization 1: For Convex Programs, Seeing s_N Support Constraints Gives P^N{V(x_N) > ε(s_N)} ≤ γ, the Value of the Variational Problem (10)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 10)

Milestones (the proof of Theorem 1, Sect. 5.1)

Companions

Significance

Difficulty

Formalization scope

Selected references

Supply Chain Coordination with Contracts VIII: In the Two-Location Base-Stock Model the Linear Transfers (39)–(41) Make the Optimal Base Stocks the Unique Nash EquilibriumTextbook

Motivation

Setting

Formalization targets

Goal: the contracts coordinate, uniquely

Milestones

Significance

Difficulty

Formalization scope

Selected references

Integer Programming with a Fixed Number of Variables 1: If B(p,r) ⊂ τK ⊂ B(p,R) with R/r ≤ c₁ and τK Misses the Lattice, Fewer Than 1 + c₁c₂√n Lattice Hyperplanes H + kbₙ Meet B(p,R)Research Paper

Motivation

Setting

Formalization targets

Goal (§1, p. 541)

Milestones, in the order the paper uses them

Significance

Difficulty

Formalization scope

Selected references

Supply Chain Coordination with Contracts V: With Market-Clearing Prices the Best Wholesale Price Earns θ/(2(1 + θ)) or θ/8, Below the (1 + θ)/8 a Full-Refund Buy-Back AttainsTextbook

Motivation

Setting

Formalization targets

Goal (pp. 55, 57)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On Linear Characterizations of Combinatorial Optimization Problems III: Zero-One and Integer-Programming-Type Problems Have Small Facial DescriptionsResearch Paper

Motivation

Setting

Formalization targets

Lemma 1

Significance

Difficulty

Formalization scope

Selected references

Supply Chain Coordination with Contracts III: With Effort-Dependent Demand, Buy-Backs, Quantity Flexibility and Revenue Sharing Under-Reward Effort, While a Quantity Discount Gives λΠ(q, e°)Textbook

Why effort breaks the standard coordinating contracts

The newsvendor with effort-dependent demand

Formalization targets

Goal

Milestones

Significance

Difficulty

Formalization scope

Selected references

Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments VI: Revenue-Ordered Offer Sets Grow with Capacity Left and Shrink with Time LeftResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Finding Minimum-Cost Circulations by Successive Approximation I: The Generic Refine Subroutine Stops Within 3n(n − 1) + 3nm + 3n²(m + n) Update Operations at an ε-Optimal CirculationResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references