Missions · Prove2Me

Completed

Combinatorics Operations Research Probability+1·Captain: mikedeng1

An Optimal Algorithm for On-line Bipartite Matching 2: No Randomized On-line Algorithm Guarantees an Expected Matching Larger Than n(1 − 1/e) + o(n)Research Paper

Motivation

An online matching algorithm must commit to each assignment when a request arrives, before it sees later requests. This limitation arises whenever waiting for the full instance is impossible: an available resource can be assigned to a current request or saved for an unknown future request. The quality of the assignment is measured by how many requests can be matched. The central question is how much the lack of future information costs, even when an algorithm uses randomness. Karp, U. Vazirani, and V. Vazirani studied this question for bipartite graphs and proved an asymptotic ceiling of $1-1/e$ for the expected fraction matched by any randomized online rule on graphs with a perfect matching (Karp, Vazirani, and Vazirani, 1990).

The paper also analyzes RANKING and gives a matching asymptotic guarantee from below. This mission concerns the separate upper-bound result: the existence of hard instances for every algorithm. The upper bound matters independently of any particular proposed rule. It says that improving an algorithm's decisions cannot remove the worst-case loss due to decisions made before all columns are revealed. Its quantifiers make the adversarial model precise: the graph is selected with knowledge of the algorithm, before that algorithm's random choices are made.

Setting

There are $n$ boys, represented by rows, and $n$ girls, represented by columns. A bipartite graph $G\subseteq[n]\times[n]$ records which boy and girl pairs may be matched. The graph is assumed to contain a perfect matching: some bijection between the two sides uses only edges of $G$ . This assumption supplies an offline benchmark of $n$ matches. Without it, a graph with no edges would make every upper bound on matching size empty of content.

Girls arrive one at a time. On arrival, the algorithm learns the edges incident to that girl, chooses an as-yet-unmatched adjacent boy, or declines to match her. A choice cannot later be changed. The paper labels columns so that they arrive in the order $n,n-1,\ldots,1$ . A deterministic algorithm can base its action on the neighborhoods revealed so far. A randomized algorithm can additionally use internal random choices. Its performance $p(A)$ is the minimum, over a graph with a perfect matching and a preselected arrival order, of its expected number of matches; the expectation is over its own randomness (Karp, Vazirani, and Vazirani, 1990, p. 352).

The paper's hard family begins with the complete upper-triangular graph $T_n$ , where row $i$ is adjacent to column $j$ exactly when $i\le j$ . Its columns arrive from largest to smallest. Relabeling the rows by a permutation $\pi$ gives an instance $T_\pi$ that still contains a perfect matching. The algorithm RANDOM takes an eligible boy uniformly whenever at least one is available. Write $V_{T_n}(n,\varnothing)$ for RANDOM's expected number of matches on $T_n$ , beginning with no matched rows (Karp, Vazirani, and Vazirani, 1990, p. 357).

Formalization targets

Main theorem

For every $\varepsilon>0$ , there is one threshold $N$ such that, for every $n\ge N$ and every randomized online algorithm $A$ on $n$ rows and columns, a graph $G$ with a perfect matching satisfies

\mathbb E_A[|M(G)|]\le (1-e^{-1}+\varepsilon)n.

The threshold is uniform over algorithms. The graph may depend on $A$ . This is the quantified upper-bound reading of Theorem 2's $p(A)\le n(1-1/e)+o(n)$ (Karp, Vazirani, and Vazirani, 1990, Theorem 2).

Milestone statements

Lemma 13 identifies the average size produced by any deterministic greedy algorithm on a uniformly permuted $T_n$ with RANDOM's expected size on $T_n$ . Lemma 14 bounds the worst-case performance of every randomized algorithm, including non-greedy algorithms, by that value. Lemma 16 identifies the value itself by the two-sided limit

\lim_{n\to\infty}\frac{V_{T_n}(n,\varnothing)}{n}=1-e^{-1}.

Together these statements give the finite-instance comparison and the asymptotic value named in the goal (Karp, Vazirani, and Vazirani, 1990, Lemmas 13, 14, 16).

Significance

Theorem 2 limits what any randomized online matching rule can guarantee under the paper's oblivious-adversary performance measure. Since the hard graph always admits a perfect matching, the gap from $n$ is caused by the order of information and the required irrevocable decisions. The statement applies to the entire algorithm class, rather than comparing two selected procedures. It therefore provides the ceiling against which the paper's lower guarantee for RANKING is measured.

Formalizing the result requires a reusable description of finite online algorithms, their visible histories, and expected matching size. It also requires a definition of uniform random choice from currently eligible rows with an explicit empty-choice case. The 1990 result is proved in the paper; the statements in this mission are targets for machine-checked proofs, not claims of an existing formal proof. The model can support later statements about other matching rules and hard-input distributions without changing the meaning of an online decision.

Difficulty

For a fixed graph, an algorithm can be designed around the graph's particular perfect matching, so one hard graph cannot simply be announced in advance for all deterministic algorithms. The theorem instead has to bound each randomized algorithm against a graph selected for that algorithm. Even then, checking the triangular graph against one rule does not establish a universal bound: different rules can respond differently to the same revealed neighborhoods. The crucial mathematical obstacle is a comparison across all such rules while preserving the restriction that future columns remain unseen. A further asymptotic step is needed to determine RANDOM's value on the triangular family, including both sides of the $o(n)$ claim in Lemma 16.

Formalization scope

Both sides are Fin n. An edge set is a subset of row-column pairs. The published perfect-matching predicate is reused: it asks for a bijection whose every selected pair is an edge. The paper's one-based column order $n,\ldots,1$ is represented by zero-based order $n-1,\ldots,0$ ; arrival number zero is the largest column. A deterministic rule receives only the neighborhoods of columns that have arrived, including the current column. A randomized rule is a probability mass function on the finite set of deterministic rules, allowing arbitrary correlations among its choices. The expected size is a finite sum over that mass function.

RANDOM is represented by the conditional-expectation recursion for uniform choice among eligible rows. If none is eligible, the column remains unmatched and there is no division by zero. For $n=0$ , the matching and RANDOM value are zero; the main theorem is eventual in $n$ and Lemma 16's value at zero does not affect the limit. Lemma 16 uses a two-sided limit. The paper's $o(n)$ in Theorem 2 is stated as $\forall\varepsilon>0,\exists N,\forall n\ge N$ with $N$ before the algorithm, so the error is uniform across algorithms. A hard graph must contain a perfect matching; dropping this condition would let the empty graph satisfy the inequality trivially.

Useful contributions include finite probabilistic averaging, the greedy comparison, analysis of the recursive RANDOM value, and a proof joining Lemmas 14 and 16 into the uniform goal. The history and matching-run definitions are reusable for other finite online bipartite matching statements. The two numbered claims inside the paper's proof of Lemma 13 and its later remarks are outside the mission's curated milestone list.

Selected references

Richard M. Karp, Umesh V. Vazirani, and Vijay V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, Proceedings of the 22nd Annual ACM Symposium on Theory of Computing, pp. 352–358, 1990. DOI: 10.1145/100216.100262.

9 thms3 active usersReviewed

Convex Optimization Operations Research Optimization+1·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 thms3 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts VI: With a Forecast Update, Buy-Back Terms with w₁ − w₂ + λc₂ = λc₁ Give the Retailer λΩ₁(q₁) and a Lower Period-2 Margin w₂ − c₂ < w₁ − c₁Textbook

Motivation

A newsvendor retailer who may order twice faces a tradeoff. Ordering late lets the retailer use a better demand forecast. Ordering early lets the supplier produce more cheaply, with longer procurement lead times and no overtime labor. Fisher and Raman (1996) document such forecast improvements between ordering epochs in fashion apparel. A decentralized supply chain must balance cheap early production against well-informed late production, and it is not obvious that a simple contract can induce both firms to strike the balance an integrated firm would choose.

This mission formalizes §6.6 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003), read in the author's January 2003 draft. The section builds on Donohue (2000), who studied the same two-mode production problem under forced compliance. The chapter's model lets the supplier operate under voluntary compliance: she may deliver less than the retailer orders, and she may produce more in period 1 than was ordered. The question is whether a buy back contract with one wholesale price per ordering epoch still coordinates the supply chain.

Setting

A demand signal $\xi \ge 0$ with density $g$ and distribution function $G$ is observed once before the selling season. Given $\xi$ , demand $D$ has distribution function $F(\cdot\,|\,\xi)$ , continuous and strictly increasing on $[0,\infty)$ . Demand is stochastically increasing in the signal: $F(x\,|\,\xi_h) < F(x\,|\,\xi_l)$ for $\xi_h > \xi_l$ . Expected sales are $S(q\,|\,\xi) = E[\min(q,D)\,|\,\xi]$ . Period 1 is before the signal and period 2 is after it. The retailer's total order is $q_1$ after period 1 and $q_2 \ge q_1$ after period 2. The supplier's unit production cost is $c_i$ in period $i$ , with $c_1 < c_2 < p$ , where $p$ is the retail price. Salvage values and goodwill costs are zero.

The supply chain's period-2 objective is

\Omega_2(q_2\,|\,q_1,\xi) = pS(q_2\,|\,\xi) - c_2 q_2 + c_2 q_1 ,

and $q_2(q_1,\xi)$ maximizes it over $q_2 \ge q_1$ . The supply chain's expected profit is $\Omega_1(q_1) = -c_1 q_1 + E[\Omega_2(q_2(q_1,\xi)\,|\,q_1,\xi)]$ .

Under the buy back contract $\{w_1, w_2, b\}$ the retailer pays $w_i$ per unit ordered in period $i$ , and the supplier refunds $b$ per unsold unit. The retailer's period-2 profit is $\pi_2(q_2\,|\,q_1,\xi) = (p-b)S(q_2\,|\,\xi) - (w_2-b)q_2 + w_2 q_1$ , and his period-1 profit is $\pi_1(q_1) = -w_1 q_1 + E[\pi_2(q_2(q_1,\xi)\,|\,q_1,\xi)]$ . The supplier's period-2 profit $\Pi_2$ and her period-1 profit $\Pi_1(x\,|\,q_1)$ , as functions of the stock $x$ she holds, are given in the mission's Profits definition.

Formalization targets

Goal: the buy back contract coordinates

For $\lambda \in [0,1]$ with

p - b = \lambda p,\qquad w_2 - b = \lambda c_2,\qquad w_1 - w_2 + \lambda c_2 = \lambda c_1,

the identities

\pi_2(q_2\,|\,q_1,\xi) = \lambda\big(\Omega_2(q_2\,|\,q_1,\xi) - c_2 q_1\big) + w_2 q_1,\qquad \pi_1(q_1) = \lambda\,\Omega_1(q_1)

hold, so the supply chain's optima in both periods are the retailer's optima (with equivalence for $\lambda > 0$ ). In addition,

w_2 - c_2 = w_1 - \big(\lambda c_1 + (1-\lambda)c_2\big) < w_1 - c_1 \quad (\lambda < 1).

Milestones

The structure of the period-2 problem, Eqs. (25)–(26): $q_2(\xi)$ solves $F(q_2(\xi)\,|\,\xi) = (p-c_2)/p$ and increases in $\xi$ , and the threshold $\xi(q_1)$ splits the signals into those that trigger a period-2 order and those that do not.
The retailer's period-2 identity (p. 65).
The supplier fills any period-2 order up to $q_2(q_1,\xi)$ , and for $\lambda < 1$ she does not fill a larger one (p. 65).
The retailer's period-1 identity (p. 66).
The first-order condition (27) for $q_1^o$ .
The supplier's period-2 profit increases in her stock below $q_1$ , so she produces at least the period-1 order (p. 66).
The supplier produces exactly the period-1 order (p. 67).
The margin comparison (p. 67).

Significance

The result shows that the buy back contract, which coordinates the single-period newsvendor, extends to a setting with a forecast update and two production modes, even when the supplier is free to under-deliver or to stockpile. Profit can be divided arbitrarily through $\lambda$ . Coordination also forces the supplier's margin on expensive late production below her margin on cheap early production, which contradicts the intuition that the better-informed late order should command a premium. Milestone 7 rules out stranded inventory: under the coordinating terms the supplier never stocks more than the retailer ordered in period 1.

These results are established on paper in Cachon's chapter. No machine-checked version is known. The identities are algebraic. The supplier's production result needs differentiation of an expectation over the signal across the moving threshold $\xi(x)$ .

Difficulty

The retailer's identities reduce to algebra once the contract terms are substituted, and the margin comparison is one line. The substantive steps are the derivative formulas (27) and $\partial \Pi_1(x\,|\,q_1)/\partial x = -c_1 + c_2(1 - G(\xi(x)))$ . The obvious move, differentiating inside the expectation term by term, fails because the period-2 optimum $\max(q_1, q_2(\xi))$ has a kink at $\xi = \xi(q_1)$ . The integrand switches between two regimes, and the switch point moves with $q_1$ . The supplier's period-1 profit is not differentiable at $x = q_1$ ; only its right derivative is negative at $q_1^o$ . Turning the page's derivative statements into the global claim that $x = q_1^o$ is her unique optimum needs a monotonicity argument on both sides of $q_1^o$ .

Formalization scope

The conditional law is a measurable family $\xi \mapsto D_\xi$ of probability measures on $\mathbb R$ supported on $[0,\infty)$ , each with a finite mean, a continuous distribution function, and a distribution function strictly increasing on $[0,\infty)$ . The signal has a measurable density $g \ge 0$ with $\int_0^\infty g = 1$ , and demand has a finite unconditional mean. These standing assumptions follow the chapter's p. 7 newsvendor model, together with the measurability needed for expectations over the signal. $0 < c_2 < p$ makes the critical ratio lie in $(0,1)$ . Expected sales reuse the platform definition SupplyChainTheory.expSales (from SupplyChainTheory_contracts).

The optimum $q_2(q_1,\xi)$ is a hypothesis-carried selection maximizing $\Omega_2$ over $q_2 \ge q_1$ . It is never an arbitrary function: a formalization that let $q_2(q_1,\xi)$ be unconstrained would make $\pi_1 = \lambda\Omega_1$ a statement about meaningless orders. The thresholds $\xi(q_1)$ enter as solutions of (26) whose existence is assumed where the page assumes it. Optimal order quantities are taken over $q_1 \ge 0$ and $q_2 \ge q_1$ . Derivatives are stated with HasDerivAt (or HasDerivWithinAt for the right derivative at a kink).

Three corrections of the print are disclosed in the item notes:

the strict margin inequality fails at $\lambda = 1$ ;
the p. 66 identity for $\Pi_2(x, q_1, q_2, \xi)$ is off by the constant $(1-\lambda)c_2q_1$ ;
"retailer optimal equals chain optimal" needs $\lambda > 0$ in the converse direction.

Contributions are welcome on all milestones. A lemma that differentiates $q \mapsto E[\max_{q_2 \ge q} \Omega_2]$ with a density-driven threshold would be reusable beyond this mission.

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
K. L. Donohue, Efficient Supply Contracts for Fashion Goods with Forecast Updating and Two Production Modes, Management Science 46(11), 1397–1411, 2000. https://doi.org/10.1287/mnsc.46.11.1397.12088
M. Fisher and A. Raman, Reducing the Cost of Demand Uncertainty Through Accurate Response to Early Sales, Operations Research 44(1), 87–99, 1996. https://doi.org/10.1287/opre.44.1.87

12 thms3 active usersReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 3: KNAPSACK Reduces to Single-Machine Total Weighted TardinessResearch Paper

Motivation

Minimizing total weighted tardiness on a single machine, written $n|1||\sum w_jT_j$ , is one of the basic problems of deterministic scheduling. A job that finishes after its due date is penalized in proportion to its lateness and its weight. Practitioners use this criterion to model penalty clauses and customer priority. In the theory it was a reference problem for branch-and-bound methods and dominance rules throughout the 1960s and 1970s.

Close relatives are easy: with equal weights and a common due date, shortest-processing-time order is optimal. Whether the weighted problem admits a polynomial algorithm was open until the report of Brucker, Lenstra and Rinnooy Kan in 1975. Their Theorem 4(d) shows that KNAPSACK reduces to it, so the problem is NP-hard. The unweighted case $n|1||\sum T_j$ is listed there as open (Section 5) and was settled only later by Du and Leung (1990).

Timeline:

1972: Karp proves KNAPSACK NP-complete (Karp 1972).
1975: Brucker, Lenstra and Rinnooy Kan, Mathematisch Centrum Report BW 43/75, Theorem 4(d), reduce KNAPSACK to $n|1||\sum w_jT_j$ (journal version: Annals of Discrete Mathematics 1, 1977).
1977: Lawler gives a pseudopolynomial algorithm for $n|1||\sum T_j$ and shows that $n|1||\sum w_jT_j$ is strongly NP-hard (Lawler 1977).
1990: Du and Leung prove $n|1||\sum T_j$ NP-hard (Du & Leung 1990).

Setting

A KNAPSACK instance consists of positive integers $a_1,\dots,a_t$ and $b$ . It is a yes-instance if some subset $S\subseteq T=\{1,\dots,t\}$ satisfies $\sum_{j\in S}a_j=b$ . Write $A=\sum_{j\in T}a_j$ and $a_*=\max_{j\in T}a_j$ .

An instance of $n|1||\sum w_jT_j$ consists of $n$ jobs. Job $j$ has a processing time $p_j$ , a weight $w_j$ and a due date $d_j$ , all nonnegative integers, and every job is available at time $0$ . A schedule gives each job a start time $B_j\in\mathbb N$ , and no two jobs may overlap on the machine. Job $j$ completes at $C_j=B_j+p_j$ and has tardiness $T_j=\max\{0,C_j-d_j\}$ . The instance with threshold $y$ is a yes-instance if some schedule satisfies $\sum_jw_jT_j\le y$ . A processing order $\pi=(\pi(1),\dots,\pi(n))$ determines the schedule without idle time, in which $C_{\pi(k)}=\sum_{i\le k}p_{\pi(i)}$ .

Reducibility (Section 2 of the paper) is polynomial-time many-one reducibility between the recognition versions. A polynomial-time Turing machine must map codes of KNAPSACK instances to codes of scheduling instances so that yes-instances map exactly to yes-instances.

The paper's construction has $n=t+t'$ jobs: for $j\in T$ , $p_j=\tau+a_j$ , $w_j=\tau+a_j+1$ , $d_j=t\tau+b$ ; for each of the $t'$ dummy jobs, $p_j=\tau$ , $w_j=\tau+1$ , $d_j=t\tau+b$ . The threshold is $y=\tfrac12t'(t'+1)\tau(\tau+1)+(t'+1)\tau(A-b)+t'$ , with $t'=\tfrac12(t+1)(A-b)+\tfrac12t(t+1)a_*^2$ and $\tau>2t'+A$ . The proof is phrased in terms of $c_\pi=C_{\pi(t)}-(t\tau+b)$ , the amount by which the $t$ -th job of the order misses the common due date.

Formalization targets

Goal: Theorem 4(d)

\text{KNAPSACK}\;\propto\;n|1||\textstyle\sum w_jT_j,

stated as CookPvsNP.PolyReducible SchedComplexity.OneMachine.knapsackLang wtLangMult. The scheduling side uses the multiplicity encoding of the paper's Remark (p. 23), in which a class of identical jobs is written once together with its cardinality.

The equivalence and its claims

Each milestone is a statement of the paper's proof (pp. 20–21) about the construction above, for every admissible $\tau$ :

removal of idle time: every schedule is matched or improved by the schedule without idle time of some processing order;
KNAPSACK has a solution iff some order has $C_{\pi(t)}=t\tau+b$ ; moreover $-b\le c_\pi\le A-b$ ;
identities and bounds (2)–(7) for the tail sums $\sum_{j>t}v_{\pi(j)}(C_{\pi(j)}-C_{\pi(t)})$ ;
claims (A) $c_\pi=0\Rightarrow\exists\pi'$ with $c_{\pi'}=0$ and $\sum w_jT_j\le y$ ; (B) $c_\pi>0\Rightarrow\sum w_jT_j>y$ ; (C) $c_\pi<0\Rightarrow\sum w_jT_j>y$ ;
the equivalence: KNAPSACK has a solution iff the constructed instance has a schedule with $\sum w_jT_j\le y$ .

Significance

The theorem places $n|1||\sum w_jT_j$ among the NP-hard problems, so (unless P = NP) the research on it has to aim at enumerative methods, pseudopolynomial algorithms or approximation, not at an exact polynomial algorithm. Together with the companion reductions of Theorem 4, it drew the boundary between easy and hard single-machine problems that the later classification of Lageweg, Lawler, Lenstra and Rinnooy Kan made systematic.

The result is proved in the paper, and Lawler's later strong NP-hardness proof supersedes it. No machine-checked proof is known to exist. A formal proof adds three things. It makes the paper's "it is easily seen" steps and the encoding argument of the Remark explicit. It produces a reusable single-machine tardiness model with processing orders. It also fixes a gap in the printed construction: the printed $t'$ need not be an integer.

Difficulty

The equivalence is not a local exchange argument. The threshold $y$ must separate orders with $c_\pi=0$ from all others, and the objective is a quadratic function of the order. The orders with $c_\pi=0$ can still differ in $\sum w_jT_j$ by the cross terms $\sum a_{\pi(j)}a_{\pi(k)}$ and by how the late jobs are arranged. The construction therefore needs a slack $t'$ that absorbs these terms, and a scale $\tau$ large enough that a nonzero $c_\pi$ always costs more than the slack. Keeping exact track of every constant, including $t'$ and $y$ , is where errors creep in.

Polynomiality is a second, separate difficulty. The construction has $\Theta(t^2a_*^2+tA)$ jobs, which is exponential in the binary length of the KNAPSACK input. The goal holds only for the encoding of the Remark, and a solver must also produce an explicit polynomial-time Turing machine.

Formalization scope

Jobs of the order-based statements are Fin n, numbered from $0$ ; a processing order is Equiv.Perm (Fin n) with π i the paper's $\pi(i+1)$ . posCompletion p π k is the paper's $C_{\pi(k)}$ for the 1-based position $k$ .
Start times are in $\mathbb N$ . Every criterion is regular and the paper determines schedules by processing orders, so integer start times lose nothing. Tardiness and $\sum w_jT_j$ are computed in $\mathbb Z$ ; the bounds with halves are stated over $\mathbb R$ exactly as printed.
Corrected gap: the printed $t'=\tfrac12(t+1)(A-b)+\tfrac12t(t+1)a_*^2$ is a half-integer when $(t+1)(A-b)$ is odd. The formalization uses its ceiling and computes $y$ from the same $t'$ .
$\tau$ is quantified over all integers with $\tau>2t'+A$ ; the positivity of the $a_j$ and $0<b<A$ are hypotheses, as the paper assumes them.
Explicit readings of the paper's loose phrases: "we may assume [no idle time]" becomes a theorem that the schedule without idle time of some order is at least as good as any schedule; "easily seen" becomes the equivalence with $C_{\pi(t)}=t\tau+b$ ; "for some $\pi$ " in (5) and (7) becomes a reordering that keeps the first $t$ positions, and so keeps $c_\pi$ ; "we may assume $0<b<A$ " is a hypothesis of the milestones but not of the goal, whose reduction must handle every KNAPSACK instance.
Reducibility is CookPvsNP.PolyReducible from the published CookPvsNP_defs. Codes use the alphabet BSym and the binary numerals encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). KNAPSACK is restricted to positive integers, so that encoding's subsetSumLang is not reused.
The goal must not be weakened to the bare equivalence: polynomial-time computability of the reduction is part of the statement. The one-copy-per-job encoding of the target is ruled out: the paper does not claim polynomiality for it, and the goal uses the multiplicity encoding instead.
Welcome contributions: proofs of the claims, a reusable lemma that idle time can be removed for regular criteria, and Turing-machine constructions for arithmetic on binary numerals, which the sibling missions of this series also need.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. https://ir.cwi.nl/pub/9725 , https://doi.org/10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
E. L. Lawler, A "pseudopolynomial" algorithm for sequencing jobs to minimize total tardiness, Annals of Discrete Mathematics 1 (1977) 331–342. https://doi.org/10.1016/S0167-5060(08)70742-8
J. Du, J. Y.-T. Leung, Minimizing total tardiness on one machine is NP-hard, Mathematics of Operations Research 15 (1990) 483–495. https://doi.org/10.1287/moor.15.3.483
S. Cook, The P versus NP problem, Clay Mathematics Institute problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

18 thms3 active usersReviewed

Completed

Discrete Geometry Linear Optimization Number Theory+1·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 thms3 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts VII: In the Single-Location Base-Stock Model the Transfers t_I = (1 − λ)h_r, t_B = β_r − λβ Make the Retailer's Cost λc(s_r)Textbook

Motivation

A retailer can keep too little inventory even when its own stocking decision is optimal. In the single-location model of Cachon, Supply Chain Coordination with Contracts (2003), the supplier suffers a cost when the retailer has backorders, but the retailer does not bear that part of the cost. The supplier and retailer therefore prefer different base-stock levels. Section 6.7 asks whether payments tied to expected inventory and backorders can make the retailer choose the level that minimizes their combined cost. The result also describes how the contract divides that cost between the firms.

The model concerns a continuing operation with repeated replenishment opportunities and backordered demand. A base-stock policy keeps the retailer's inventory position at a chosen level by replacing units as demand occurs. Cachon reduces the cost calculation for such a policy to the distribution of demand over one replenishment lead time. That reduction allows the coordination question to be stated with one real stock-level decision rather than a full inventory trajectory. The chapter presents this model as a building block for its two-location system in §6.8 Cachon (2003).

Setting

Let $D_r$ denote lead-time demand, the amount demanded while the retailer waits for replenishment. It is nonnegative and has a finite mean $\mu_r=\mathbb E[D_r]$ , distribution function $F_r$ , and density $f_r$ . At inventory level $s\in\mathbb R$ , expected inventory is $I_r(s)=\mathbb E[(s-D_r)^+]$ and expected backorders are $B_r(s)=\mathbb E[(D_r-s)^+]$ , where $x^+=\max(x,0)$ . The section assumes $F_r(0)=0$ and a strictly increasing differentiable $F_r$ on nonnegative levels. These assumptions place the optimum above zero.

The retailer pays holding cost $h_r I_r(s)$ and its own backorder cost $\beta_r B_r(s)$ . The supplier pays a further backorder cost $\beta_s B_r(s)$ . All three cost rates are positive. Thus $c_r(s)=h_r I_r(s)+\beta_r B_r(s)$ and $c_s(s)=\beta_s B_r(s)$ are the firms' costs, while $c(s)=c_r(s)+c_s(s)$ is the channel cost. Write $\beta=\beta_r+\beta_s$ . Because demand is backordered rather than lost, the section treats the sales rate as constant across the stock decisions and compares costs alone Cachon (2003), §6.7.1.

The proposed contract pays the retailer $t_I I_r(s)+t_B B_r(s)$ from the supplier, where $t_I$ and $t_B$ are transfer rates. A positive rate is a subsidy; a negative rate charges the retailer. For a parameter $\lambda\in(0,1]$ , the contract sets $t_I=(1-\lambda)h_r$ and $t_B=\beta_r-\lambda\beta$ . The retailer's contracted cost is its original cost minus this transfer; the supplier's contracted cost is its original cost plus it. The parameter $\lambda$ describes a family of printed contract rates and is not itself a payment term Cachon (2003), p. 74.

Formalization targets

The milestones establish the two expectation identities, the channel's cost formula and strict convexity, the channel's critical ratio, the retailer's lower uncontracted stock level, and the retailer's cost after the printed transfer. In the notation above, the channel optimum $s_r^\circ$ is unique and satisfies

F_r(s_r^\circ)=\frac{\beta}{h_r+\beta};

the uncontracted retailer has its own unique optimum $s_r^*$ with $s_r^*<s_r^\circ$ . Three further statements of §6.7.1 complete the section: the signs of the transfer rates over the family ( $t_I\ge0$ , with $t_I>0$ exactly for $\lambda<1$ , and $\{t_B:0<\lambda\le1\}=[-\beta_s,\beta_r)$ ); the decomposition

t_I I_r(y)+t_B B_r(y)=(t_I+t_B)I_r(y)+t_B(\mu_r-y);

and the equivalence with the newsvendor model: with lead-time demand as newsvendor demand, retail price $p=h_r+\beta_r$ and wholesale price $w=h_r$ , the newsvendor retailer's profit $pS(q)-wq$ , with expected sales $S(q)=\mathbb E[\min(q,D_r)]$ , equals $-c_r(q)+\beta_r\mu_r$ . The mission goal is the coordinating identity of Eq. (33), together with the unique optimality it implies:

c_r^\lambda(s)=\lambda c(s),\qquad c_s^\lambda(s)=(1-\lambda)c(s) \quad\text{for all }s\in\mathbb R\text{ and }0<\lambda\le1.

Consequently, the retailer's contracted cost has the same unique minimizer $s_r^\circ$ as the channel cost. At each stock level the retailer's contracted cost is strictly increasing in $\lambda$ , which is the page's statement that the retailer's share of the cost increases with $\lambda$ . The result does not prescribe one fixed allocation of cost: each $\lambda$ in the stated interval gives a contract with the same coordinated stock level and a different retailer share Cachon (2003), Eq. (33), p. 74.

Significance

The theorem identifies an explicit transfer that corrects an incentive gap created by the supplier's backorder cost. Without it, the retailer sets stock according to $\beta_r$ , while the channel's stock decision uses $\beta_r+\beta_s$ . Under the contract, the retailer bears the fraction $\lambda$ of total cost at every stock level, so its decision agrees with the integrated channel's decision. This conclusion connects a decentralized cost objective to the base-stock target used in the next section's two-location analysis Cachon (2003), §§6.7–6.8.

The chapter proves these claims informally; this mission asks for machine-checked Lean proofs of the expectation identities, convexity and optimality claims, and the contract identity. Its reusable output is the precise treatment of expected positive-part inventory and backorders under a demand law with finite mean. The local definitions may also support later formalizations of inventory contracts. Expected sales in the newsvendor comparison is the published SupplyChainTheory.expSales (definition SupplyChainTheory_contracts), referenced rather than redefined. The existing proved SupplyChainTheory.chain_optimal_fractile concerns a single-period newsvendor profit objective; its critical ratio is related mathematically but belongs to a different model and is not substituted for Eq. (31).

Difficulty

The algebra of the transfer rates is short, but the unique-optimum claim depends on more than algebra. It requires expected inventory and backorders to match the distribution formulas, the cost to have the required curvature at nonnegative levels, and the optimum to occur at a positive level. A formal statement that defines the retailer's contracted cost directly as $\lambda c$ would erase the coordinating claim. The negative-stock region also matters: since demand is nonnegative, expected inventory vanishes there and cost is affine rather than strictly convex. The formulation must keep strict convexity on the range where it holds while still identifying the unique optimum among all real stock levels.

Formalization scope

Lean represents $D_r$ by a probability measure on $\mathbb R$ supported on $[0,\infty)$ , with an explicit integrable first moment. The density is a measurable nonnegative function whose induced measure is the demand law; the cdf is continuous, strictly increasing on $[0,\infty)$ , equals zero at zero, and has that density as its derivative at positive levels. These are the section's distribution assumptions. The positive rates $h_r,\beta_r,\beta_s$ are fields of one model, and $I_r,B_r$ are defined by expectations. This rules out accidental zero values from nonintegrable real integrals. The cost functions are constructed from the expected inventory and backorders; the transfer is constructed from the two printed rates. The identities in Eqs. (28)–(33) are theorem targets, not definitions.

Stock levels are real, including negative levels, because the section does not explicitly restrict the decision set. The formal result states strict convexity on nonnegative levels and uniqueness of the cost minimizers over all real levels. The page's sentence that $t_I>0$ for all $\lambda\in(0,1]$ fails at $\lambda=1$ , where $t_I=0$ ; the formal statement asserts $t_I\ge0$ with strict positivity exactly for $\lambda<1$ . The contract range is exactly $0<\lambda\le1$ ; $\lambda=0$ would make every retailer stock level cost-equivalent. The transfer sign is positive from supplier to retailer, as on p. 73. Risk neutrality and full information are the chapter's standing conventions. The continuous-review state process, supplier capacity, and proof that a base-stock policy attains the displayed long-run average are not modeled; the mission formalizes the section's explicit lead-time-demand cost reduction. Contributions that establish integrability, distribution identities, strict convexity, and critical-ratio optimality are all needed for closure.

Selected references

Gérard P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, vol. 11, North-Holland, 2003; source used here: author's third draft, January 2003, §6.7. DOI.

12 thms3 active usersReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 2: KNAPSACK Reduces to Single-Machine Maximum Lateness, Weighted Number of Late Jobs, and Weighted Completion Time with DeadlinesResearch Paper

Motivation

Deterministic machine scheduling was one of the first application areas of the theory of NP-completeness. After Cook (1971) and Karp (1972) showed that a large family of combinatorial problems are polynomially equivalent, Brucker, Lenstra and Rinnooy Kan set out to locate the boundary between the polynomially solvable and the NP-complete scheduling problems. Their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, Report BW 43/75, 1975; journal version in Annals of Discrete Mathematics 1, 1977) introduced the four-field notation $n|m|\ell,\lambda|k$ that, in refined form, is still the standard classification of scheduling problems, and proved NP-completeness of the "easiest" hard problems by explicit reductions.

Single-machine problems with due dates sit right at that boundary. Minimizing the maximum lateness $L_{\max}$ is solved by Jackson's earliest-due-date rule (1955), and minimizing the number of late jobs by Moore's algorithm (1968). Theorem 4 of the report shows that small changes to these problems — one release date, job weights, or due dates turned into deadlines under a weighted completion-time objective — make them NP-complete, by reduction from KNAPSACK. This mission formalizes four of those reductions, parts (b), (c), (e) and (f) of Theorem 4.

Timeline, as far as this mission is concerned:

1955: Jackson — $n|1||L_{\max}$ is solved by sequencing in order of nondecreasing due dates.
1968: Moore — $n|1||\sum U_j$ (unit weights, no release dates) is solvable in polynomial time.
1972: Karp — KNAPSACK (in the subset-sum form used here) is NP-complete; Karp also notes the reduction to $n|1||\sum w_jU_j$ , which the report cites for part (e).
1975: Brucker, Lenstra and Rinnooy Kan — Theorem 4: KNAPSACK reduces to ten scheduling problems, including the four single-machine problems of this mission.

Setting

A single-machine instance consists of $n\ge1$ jobs $J_1,\dots,J_n$ . Job $J_j$ needs $p_{j1}$ units of processing on the machine $M_1$ , has a weight $w_j$ , a release date $r_j$ and a due date $d_j$ ; all data are nonnegative integers. A schedule assigns to each job a starting time $B_j\ge r_j$ such that the occupied intervals $[B_j,B_j+p_{j1})$ of distinct jobs are disjoint. Idle time is allowed; a job with $p_{j1}=0$ occupies an empty interval. The completion time is $C_j=B_j+p_{j1}$ , the lateness is $L_j=C_j-d_j$ (possibly negative), and $U_j$ is $0$ if $C_j\le d_j$ and $1$ otherwise. The criteria are

L_{\max}=\max_j L_j,\qquad \sum w_jC_j=\sum_{j=1}^n w_jC_j,\qquad \sum w_jU_j=\sum_{j=1}^n w_jU_j .

The problem class is written in the $\lambda$ field: by default every $r_j=0$ ; $r_n\ge0$ allows a nonzero release date for the last job $J_n$ only; $w_j=1$ fixes unit weights; $L_{\max}\le0$ admits only schedules that meet every due date. A problem is turned into a yes/no question by asking whether a schedule with value $\le y$ exists.

KNAPSACK (Theorem 2(b) of the report): given positive integers $a_1,\dots,a_t,b$ , is there a subset $S\subseteq T=\{1,\dots,t\}$ with $\sum_{j\in S}a_j=b$ ? Write $A=\sum_{j\in T}a_j$ .

A problem $P'$ is reducible to $P$ , $P'\propto P$ , if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ whose answer is the same.

Formalization targets

Goal: Theorem 4(b), (c), (e), (f)

\mathsf{KNAPSACK}\propto n|1|L_{\max}\le0|\textstyle\sum w_jC_j,\quad \mathsf{KNAPSACK}\propto n|1|r_n\ge0|L_{\max},

\mathsf{KNAPSACK}\propto n|1||\textstyle\sum w_jU_j,\quad \mathsf{KNAPSACK}\propto n|1|r_n\ge0,w_j=1|\textstyle\sum w_jU_j ,

as polynomial-time many-one reductions between languages of binary strings.

Milestones: the four yes-instance equivalences

For positive $a_1,\dots,a_t,b$ with $0<b<A$ , and the paper's constructions:

4(c): $n=t+1$ ; $r_j=0$ , $p_{j1}=a_j$ , $d_j=A+1$ for $j\in T$ ; $r_n=b$ , $p_{n1}=1$ , $d_n=b+1$ . KNAPSACK has a solution iff some schedule has $L_{\max}\le0$ .
4(f): the same instance with unit weights; KNAPSACK has a solution iff some schedule has $\sum U_j\le0$ .
4(e): $n=t$ ; $p_{j1}=w_j=a_j$ , $d_j=b$ . KNAPSACK has a solution iff some schedule has $\sum w_jU_j\le A-b$ .
4(b): $n=t+1$ ; $p_{j1}=w_j=a_j$ , $d_j=A+1$ for $j\in T$ ; $p_{n1}=1$ , $w_n=0$ , $d_n=b+1$ . KNAPSACK has a solution iff some schedule meeting all due dates has

\sum w_jC_j\le y=\sum_{j,k\in T,\ j\le k}a_ja_k+A-b .

Significance

The result. Combined with the NP-completeness of KNAPSACK, the four reductions show that the four problems are NP-hard (in the ordinary sense; they admit pseudo-polynomial algorithms). Part (c) shows that Jackson's rule cannot be extended to a single nonzero release date unless P = NP; part (f) does the same for Moore's algorithm; part (e) explains why weights are essential in the late-jobs problem; part (b) shows that deadlines turn the weighted completion-time problem, solved by Smith's ratio rule without them, into a hard one. These are entries of the complexity tables that every later scheduling classification builds on.

Formalizing it. The reductions are classical and proved on paper, in a few lines each: for (c), (e) and (f) the report gives only the construction and a figure. None of them has a machine-checked proof. A complete formalization supplies the explicit equivalence over all feasible schedules (including schedules with idle time and arbitrary processing order), the handling of the inputs the proof sets aside by "we may assume that $0<b<A$ ", and the polynomial-time computability of the constructions in a Turing-machine model.

Difficulty

Each equivalence has an easy direction: a subset $S$ with sum $b$ gives the schedule "jobs of $S$ , then $J_n$ , then the rest" (Figures 4 and 7 of the report). The other direction must rule out every feasible schedule, not only the idle-free ones in the displayed order. The report gives no argument for this direction in (c), (e) and (f), and for (b) only a computation for idle-free schedules of one shape. The equivalences are false outside $0<b<A$ in some cases (for (c), any $b>A$ makes every schedule on time), so the goal's reduction must treat those inputs separately.

The heavier part is polynomial-time computability: the reduction must be a function on strings, computed by a one-tape Turing machine within a polynomial number of steps, that parses a binary-coded KNAPSACK instance, computes $A$ and the threshold (for (b), a sum of $O(t^2)$ products), and writes the coded scheduling instance — and maps malformed strings outside the target language.

Formalization scope

Model. Jobs are Fin n (0-based; $J_n$ is the last index), with $n>0$ in each target language. Starting times are natural numbers: Section 3 computes them from processing orders on integer data, and since all criteria here are regular and release dates survive left shifts, real starting times give the same yes-instances. Feasibility requires disjoint occupied intervals, including empty intervals when $p_{j1}=0$ . Idle time is allowed. Lateness is an integer.
Problem classes are binding. $r_n\ge0$ means at least one job and release date $0$ for every job except the last; $L_{\max}\le0$ in (b) is a constraint on schedules, not the criterion. Instances outside the class are not in the target language.
Thresholds. $y\in\mathbb N$ in all four languages; for $L_{\max}$ this restricts to nonnegative thresholds, enough for the paper's $y=0$ . " $L_{\max}\le y$ " is stated as " $L_j\le y$ for all $j$ ".
Codes. An instance with threshold $y$ is the list $n$ , then $p_{j1},w_j,r_j,d_j$ per job, then $y$ , each number in binary.
Reducibility. "Reducible" (Section 2) is read as Karp reducibility, CookPvsNP.PolyReducible from the published definition CookPvsNP_defs. The alphabet and binary number codes are those of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann); its SUBSET SUM language is not reused because it admits zero sizes, while the paper's KNAPSACK is over positive integers.
Explicit readings of loose phrases. "We may assume that $0<b<A$ " becomes a hypothesis of each milestone and an obligation on the goal's reduction. "Cf. reduction (i) and Figure 4", "Cf. Karp [19] and Figure 7" and "The equivalence follows immediately" become the stated equivalences over all feasible schedules. Reduction (c) does not specify weights; the shared construction uses unit weights.
Not trivializable. The equivalences are stated for the paper's explicit constructions, not for an existentially chosen instance; the target languages enforce the problem class; and the goal demands polynomial-time computability, not only the equivalence.
Infrastructure. A Turing-machine library for arithmetic on binary codes (parsing, addition, multiplication, comparison) is reusable across all seven missions of this series and across every reduction posed in the same framework. Contributions of such general lemmas are welcome.

Parts (a), (d) and (g)–(j) of Theorem 4 are formalized in other missions of this series.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum, Report BW 43/75, Amsterdam, 1975; journal version: J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in: Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
S. A. Cook, The complexity of theorem-proving procedures, Proc. 3rd ACM STOC, 1971, 151–158. https://doi.org/10.1145/800157.805047
J. M. Moore, An n job, one machine sequencing algorithm for minimizing the number of late jobs, Management Science 15 (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102
J. R. Jackson, Scheduling a production line to minimize maximum tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.

11 thms3 active usersReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 1: PARTITION Reduces to Makespan and to Weighted Completion Time on Two Identical MachinesResearch Paper

Motivation

Deterministic machine scheduling asks how to process a set of jobs on a set of machines so that an overall criterion, such as the time at which the last job finishes, is as small as possible. In the early 1970s many such problems had efficient algorithms (Johnson's rule for the two-machine flow shop, Smith's ratio rule for a single machine, Lawler's rule under precedence constraints), while others resisted every attempt. The report of Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977) drew the line between the two groups systematically. It fixed the four-field notation $n|m|\ell,\lambda|k$ that the scheduling literature still uses, and it proved NP-completeness of the "easiest" hard problems by explicit reductions in the sense of Karp.

The first family of reductions in the report, Theorem 3, concerns the simplest machine environment beyond a single machine: two identical machines. It shows that already there, minimizing the makespan and minimizing the total weighted completion time are as hard as PARTITION. These two reductions are simplified versions of reductions given by Bruno, Coffman and Sethi (1974), reference [3] of the report.

Setting

PARTITION. Given positive integers $a_1,\dots,a_t$ , decide whether there is a subset $S$ of $T=\{1,\dots,t\}$ with

\sum_{j\in S}a_j=\sum_{j\in T-S}a_j .

Write $A=\sum_{j\in T}a_j$ for the total.

Two identical machines. There are $n$ jobs $J_1,\dots,J_n$ and two machines $M_1,M_2$ . Job $J_j$ has a processing time $p_j\in\mathbb N$ and a weight $w_j\in\mathbb N$ , and must be processed without interruption on one machine of its choice; all jobs are available at time $0$ . A schedule assigns to every job a machine and a starting time $B_j\in\mathbb N$ ; its completion time is $C_j=B_j+p_j$ . A schedule is feasible if no two jobs on the same machine are processed at the same time, i.e. the intervals $[B_j,B_j+p_j)$ on each machine are pairwise disjoint. Idle time is allowed. Two criteria are considered:

C_{\max}=\max_j C_j,\qquad \sum_j w_jC_j .

The problems $n|2|I|C_{\max}$ and $n|2|I|\sum w_jC_j$ ask for a feasible schedule minimizing the respective criterion.

Reducibility. Following Section 2 of the report, each problem is replaced by its recognition version: given an instance and a threshold $y$ , is there a feasible schedule with value $\le y$ ? A problem $P'$ is reducible to $P$ , written $P'\propto P$ , if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer. Instances are written as words over a finite alphabet, with every number in binary.

Formalization targets

Goal: Theorem 3

\text{PARTITION}\propto n|2|I|C_{\max}\qquad\text{and}\qquad \text{PARTITION}\propto n|2|I|\textstyle\sum w_jC_j .

Both reductions use the same instance shape: $n=t$ jobs with $p_j=a_j$ .

Milestones

Theorem 3(a), equivalence. With $p_j=a_j$ and $y=\tfrac12A$ : PARTITION has a solution iff some feasible schedule has $C_{\max}\le y$ .
Ordering independence. With $p_j=w_j=a_j$ , if $S$ is the set of jobs on $M_1$ and each machine works without idle time from $0$ , then $\sum w_jC_j=k(S)$ for every order of the jobs, where

k(S)=\sum_{j,k\in S,\,j\le k}a_ja_k+\sum_{j,k\in T-S,\,j\le k}a_ja_k ;

every feasible schedule with this assignment has value at least $k(S)$ . 3. The identity for $k(S)$ . With $c=\sum_{j\in S}a_j-\tfrac12A$ ,

k(S)=k(T)-\Big(\sum_{j\in S}a_j\Big)\Big(\sum_{j\in T-S}a_j\Big)=\sum_{j,k\in T,\,j\le k}a_ja_k-\big(\tfrac12A+c\big)\big(\tfrac12A-c\big)=y+c^2 .

Theorem 3(b), equivalence. With $p_j=w_j=a_j$ and $y=\sum_{j,k\in T,\,j\le k}a_ja_k-\tfrac14A^2$ : PARTITION has a solution iff some feasible schedule has $\sum w_jC_j\le y$ .

Significance

The result. Since PARTITION is NP-complete (Karp 1972), Theorem 3 shows that both problems are NP-hard with only two machines and a single operation per job; their recognition versions are NP-complete. Together with the single-machine and shop results in the rest of the report, it places the boundary of tractability in deterministic scheduling. The makespan problem $P2\|C_{\max}$ became a standard source problem for later hardness proofs and a standard target for pseudo-polynomial algorithms and approximation schemes. The weighted completion time result contrasts with the single-machine case, which Smith's ratio rule solves in polynomial time.

Formalizing it. The theorem is classical and fully proved on paper; the report prints the constructions and, for (b), a short calculation. To our knowledge no machine-checked proof exists. The mission produces (i) a precise model of nonpreemptive schedules on two identical machines with integer start times and idle time allowed, (ii) the two yes-instance equivalences with the paper's rational thresholds, (iii) the ordering-independence statement for $p_j=w_j$ behind part (b), and (iv) the polynomial-time computability of the reductions in a Turing machine model. Part (iv) is the formal content of "reducible" and is missing from the paper.

Difficulty

For part (a) the mathematics is short. The paper treats it as evident; a formal proof must still handle schedules with idle time and the case of odd $A$ , where $\tfrac12A$ is not an integer.

Part (b) rests on the claim that, when $p_j=w_j$ , the value $\sum w_jC_j$ does not depend on the order of the jobs on a machine. For a single machine without idle time this is a symmetric double sum. A recognition-problem proof also needs the converse direction: no schedule with idle time beats the non-idle one, so every feasible schedule with assignment $S$ has value at least $k(S)$ . The paper cites this rather than proving it.

The step the paper leaves out entirely is polynomiality. The constructions copy the input and compute $\tfrac12A$ or $\sum_{j\le k}a_ja_k-\tfrac14A^2$ , and in a one-tape Turing machine model with an explicit polynomial time bound this needs binary arithmetic (sums, products, a floor) carried out on the tape. It also needs a decoder that rejects malformed words and lists containing a zero. This is routine in principle but long in practice.

Formalization scope

Model. Jobs are Fin n and machines Fin 2 (machine 0 is $M_1$ ). Starting times are natural numbers. Section 3 of the report computes them from processing orders on nonnegative integer data, and both criteria are regular, so real starting times would give the same yes-instances. Processing times may be zero; a zero-length job occupies the empty interval. Schedules may contain idle time.
Criteria. " $C_{\max}\le y$ " is stated as $C_j\le y$ for every job, which equals $\max_jC_j\le y$ for $n\ge1$ and avoids a supremum. $\sum w_jC_j$ is a finite sum in $\mathbb N$ .
Languages. PARTITION is the set of binary codes of lists of positive integers that admit a partition; a code of a list with a zero entry is not in the language. A target word codes $n$ , the processing times (and weights, job by job), and a threshold $y\in\mathbb N$ . The number of machines is fixed by the class and not coded. Every coded instance is in the class, so the language admits nothing outside it.
Reducibility is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs (Cook's one-tape Turing machines, polynomial-time many-one reductions). The alphabet BSym and the binary code encNats are reused from the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). Its PARTITION language is not reused, because it allows zero sizes.
Thresholds. The milestones state the paper's thresholds $\tfrac12A$ and $\sum_{j\le k}a_ja_k-\tfrac14A^2$ as real numbers, exactly as printed. The goal's reduction must write a natural-number threshold; all schedule values are integers, so the floor of the printed threshold gives the same yes-instances.
Explicit readings. The equivalence of (a) is not printed; the report says on p. 14 that such equivalences are "trivial or clear" where not proved. "Only depends on the choice of $S$ " is stated as two facts: equality for non-idle schedules and a lower bound for all feasible schedules. "It is easily seen (cf. Figure 1)" is the three-step identity, one equality per printed step. $k(S)$ is defined by its closed form, and its link to schedules is a milestone.
Ruled out. A target language whose yes-instances are defined through PARTITION, an equivalence for some instance rather than the paper's construction, and a goal that drops polynomial-time computability would all make the goal vacuous or different. The statements here use the constructions as printed and Cook's reducibility.
Welcome contributions. Proofs of the four milestones; a library of polynomial-time Turing machine programs for binary arithmetic and list decoding over BSym, which every mission of this series needs and which is reusable for other reductions on the platform.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975. https://ir.cwi.nl/pub/9725/9725D.pdf
J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
J. Bruno, E. G. Coffman Jr., R. Sethi, Scheduling independent tasks to reduce mean finishing time, Communications of the ACM 17 (1974) 382–387. https://doi.org/10.1145/361011.361064
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. https://doi.org/10.1145/800157.805047
W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106

11 thms3 active usersReviewed

Completed

Operations Research 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 thms3 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts II: With Price-Dependent Demand the Price-Contingent Buy-Back Gives the Retailer λΠ(q, p), as Revenue Sharing Does, and Coordinates Price and QuantityTextbook

Motivation

A retailer who controls both inventory and price can respond to a supply contract in two ways. A contract that induces the right order quantity at a fixed price may change the retailer's incentive to raise or lower that price. For a one-season supply chain, Cachon's chapter compares familiar contracts under price-dependent demand and identifies a price-contingent buy-back, also called a price-discount contract, that aligns both decisions. The mission concerns §6.3 of the author's January 2003 third draft, on printed pages 33–38. Those page and equation numbers belong to the draft and may differ from the typeset chapter.

Setting

One risk-neutral supplier and one risk-neutral retailer have full information before a single selling season. The retailer chooses a nonnegative stocking quantity $q$ and a retail price $p$ from an admissible price set $P$ ; the price stays fixed during the season. Demand has a probability law $D_p$ that depends on $p$ . Write $F(y\mid p)$ for its distribution function, $S(q,p)=\mathbb E_p[\min(q,D)]$ for expected sales, and $\mu(p)=\mathbb E_p[D]$ for mean demand. Demand is nonnegative, has a finite mean and, in the chapter's regular setting, its distribution function increases with demand level and has a positive price derivative at positive demand levels. Higher prices thus lower demand in the stochastic order used by the chapter. The price set is nonempty and open so an admissible price optimum has an interior first-order condition.

The supplier's unit cost is $c_s$ , the retailer's unit procurement cost is $c_r$ , and $c=c_s+c_r$ is total unit cost. Their goodwill penalties for unmet demand are $g_s$ and $g_r$ , with $g=g_s+g_r$ . An unsold unit has salvage value $v$ at the retailer. The integrated channel's expected profit is

\Pi(q,p)=(p-v+g)S(q,p)-(c-v)q-g\mu(p).

A buy-back contract charges a wholesale price $w_b$ for each ordered unit and pays the retailer $b$ for each unsold unit. A revenue-sharing contract charges a wholesale price $w_r$ and gives the retailer a fraction $\phi$ of sales and salvage revenue. In this section the supplier offers the terms and the retailer chooses $(q,p)$ . The profit formulas use the chapter's convention that a positive transfer goes from retailer to supplier.

Formalization targets

The goal is the price-contingent buy-back on p. 35, with $\lambda\in[0,1]$ :

b(p)=(1-\lambda)(p-v+g)-g_s,\qquad w_b(p)=\lambda c_s+(1-\lambda)(p+g-c_r)-g_s.

In the chapter's zero-goodwill case, $g_r=g_s=0$ , every feasible $(q,p)$ then gives the retailer $\lambda\Pi(q,p)$ and the supplier $(1-\lambda)\Pi(q,p)$ . The same retailer profit is obtained from revenue sharing with $\phi=\lambda$ and $w_r=\lambda(c-v)-c_r+\lambda v$ . Thus every existing maximizer $(q^\circ,p^\circ)$ of the integrated profit maximizes each firm's profit under the contingent buy-back. At $\lambda=0$ the retailer is indifferent; at $\lambda=1$ the supplier is indifferent.

The milestones follow the chapter's printed claims in attack order:

the integrated price condition (14), p. 34;
the quantity-flexibility condition (15), p. 34: price coordination forces $w_q=v-c_r$ or $\delta=0$ ;
the fixed buy-back condition (16), p. 35: price coordination forces $b=-g_s$ and then $w_b=c_s-g_s$ ;
the linear price-contingent terms derived from (5)–(6), p. 35;
the p. 36 profit split $\pi_r=\lambda(\Pi+g\mu)-g_r\mu$ , $\pi_s=(1-\lambda)\Pi-(\lambda g-g_r)\mu$ , valid for all goodwill penalties as an identity;
the zero-goodwill revenue-sharing price claim following (17), p. 36 (the milestone quotes its restatement in §6.3.2, p. 38);
the price-contingent revenue-sharing parameters, p. 37;
the quantity discount $w_d(q)$ , pp. 37–38: with $g_s=0$ it does not distort the price, and given $p^\circ$ it makes $q^\circ$ optimal for both firms.

Significance

The result identifies a contract schedule under which the same quantity-price pair is best for the integrated channel and for the two firms' reported profit functions. It also explains the relation between a buy-back whose terms vary with the chosen price and a revenue-sharing arrangement. In the zero-goodwill setting, both allocate every realized choice's expected channel profit in fixed shares. The general-goodwill identity shows the additional mean-demand terms that matter when the retailer controls price.

The source presents these results analytically; this mission asks for Lean proofs of the stated price and profit relationships. A published Prove2Me definition already supplies expected sales and mean demand for a single demand law, and the model here applies those functions to each price's law. The earlier open theorem RevShareCoord.Single.price_quantity_coordination (from Cachon and Lariviere's revenue-sharing paper) treats deterministic revenue and a simpler cost convention. It is an overlap in theme, but its statement does not include price-indexed demand, salvage value, retailer cost or the contingent buy-back terms, so it is not posed again here. The new model can support further price-dependent contract comparisons in the chapter.

Difficulty

The obstacle is that matching the retailer's quantity incentive at a fixed price can change the retailer's price incentive. The buy-back rate required by the fixed-price coordination equations depends on $p$ ; a fixed buy-back contract therefore does not generally align both choices. Revenue sharing with goodwill penalties has a similar price dependence. The integrated profit need not be concave or unimodal in $(q,p)$ , so a price first-order condition by itself does not establish coordination. The chapter assumes a finite integrated optimum exists and treats the price condition as necessary, not sufficient.

Formalization scope

Lean represents price-dependent demand as a family of probability measures on $\mathbb R$ , one for each price in $P$ . Each admissible law is supported on nonnegative demand, has no atom at zero and has an integrable identity function, so $\mu(p)$ is a genuine finite expectation. Sales are defined by $\mathbb E_p[\min(q,D)]$ , using the published SupplyChainTheory_contracts definition; they are not defined by the equivalent CDF integral. The admissible decisions are exactly $q\ge0$ and $p\in P$ . Unit costs and goodwill penalties are nonnegative, each admissible price exceeds $c=c_s+c_r$ , and $v<c$ , as in the model of §6.2. The chapter's standing risk-neutrality and full-information conventions appear in the use of expected profit with the same demand laws available to both firms.

There is a material qualification. With price-dependent demand, $\mu(p)$ may change with $p$ . The printed first-order condition (14) and the p. 36 inference from $\pi_r=\lambda(\Pi+g\mu)-g_r\mu$ to a joint optimum omit that effect when goodwill penalties are positive. Price first-order and optimality statements here therefore use $g_r=g_s=0$ , a case explicitly discussed in the chapter; general-goodwill claims are limited to algebraic identities. The printed p. 36 equality of price derivatives under revenue sharing also misses its factor $\phi$ , which the formal statement restores. The contingent buy-back terms are defined by the chapter's linear formulas, not by a property that hard-codes coordination. The algebraic statement permits parameter values that may violate economic buy-back bounds such as $0\le b\le w_b$ ; those bounds need separate checks when selecting a contract.

Two first-order statements, (15) and (16), compare price derivatives; they take the derivative of expected sales in price as a hypothesis, and (15) also takes differentiation under the integral sign of $\int_{(1-\delta)q}^{q}F(y\mid p)\,dy$ as a disclosed regularity hypothesis. For the quantity discount, the statement claims what the page shows, undistorted prices for each $q$ and optimality of $q^\circ$ given $p^\circ$ , not joint optimality of $(q^\circ,p^\circ)$ for the retailer. The page's claim that revenue sharing with goodwill coordinates only with $\phi=g_r/g$ is not stated, for the mean-demand reason above.

A trivializing formalization is ruled out: no contract term is defined by the profit identity it should satisfy, the demand family cannot be replaced by a single law, and the optimal pair is a hypothesis about the integrated profit, not a chosen witness.

Reusable contributions include the price-indexed demand family, the expected-profit model with five contract types, and the price-maximizer statements. Proofs of the first-order milestones need Fermat's interior-extremum theorem on the open price set and, for (15), positivity of an interval integral; the identities need the expectation algebra of $S$ and $\mu$ , including $S(0,p)=0$ .

Selected references

Gérard P. Cachon, “Supply Chain Coordination with Contracts,” in Handbooks in Operations Research and Management Science, vol. 11, Supply Chain Management, North-Holland, 2003. DOI 10.1016/S0927-0507(03)11006-7. Formalization source: author's third draft, January 2003, §6.3, pp. 33–38.
Fernando Bernstein and Awi Federgruen, “Decentralized supply chains with competing retailers under demand uncertainty,” Management Science 51(1), 2005 (the price-discount sharing contract; cited in the draft as a 2000 working paper). DOI 10.1287/mnsc.1040.0230
Nicholas C. Petruzzi and Maqbool Dada, “Pricing and the newsvendor problem: a review with extensions,” Operations Research 47(2), 1999, 183–194. DOI 10.1287/opre.47.2.183

12 thms3 active usersReviewed

Completed

Graph Theory Linear Optimization Operations Research+1·Captain: mikedeng1

Finding Minimum-Cost Circulations by Successive Approximation II: For Real Costs, the Strongly Polynomial Loop Reaches a Minimum-Cost Circulation After at Most m⌈log₂(2n)⌉ RefinementsResearch Paper

Why minimum-cost circulation needs a real-cost iteration bound

A minimum-cost circulation is a way to send flow around a directed network while respecting capacities and paying a cost per unit on each arc. It is a basic form of network optimization: a minimum-cost flow with prescribed supplies and demands can be reduced to a circulation problem, and the circulation formulation exposes the residual arcs on which a flow can be improved. Goldberg and Tarjan's successive-approximation method relaxes exact optimality by an error parameter and repeatedly reduces that error. Its ordinary stopping rule for integer costs depends on the largest cost. For arbitrary real costs, including irrational costs, a decreasing positive error need never cross a fixed numerical cutoff. The strongly polynomial loop in their 1987 technical report, later published in Mathematics of Operations Research instead tests the smallest error parameter appropriate to the current circulation and stops when it is zero.

This mission formalizes the number of refinement calls made by that loop. It builds on the related Goldberg–Tarjan 1988 max-flow and 1989 minimum-mean cycle-canceling series: those develop different algorithms for network flow, while the published 1989 circulation and approximate-optimality definitions provide this mission's common network model. The result here concerns successive approximation and its fixed-arc progress measure.

Network and approximate optimality

The vertex set $V$ is finite, with $n=|V|$ , and $E$ is a symmetric set of directed arcs, with $m=|E|$ . Symmetry means that $(v,w)\in E$ brings $(w,v)\in E$ too. Each arc has a real capacity $u(v,w)$ and a real cost $c(v,w)$ ; costs obey $c(v,w)=-c(w,v)$ . A circulation $f$ obeys $f(v,w)\le u(v,w)$ , $f(v,w)=-f(w,v)$ , and conservation of flow at every vertex. Its total cost is half the sum of $c(v,w)f(v,w)$ over directed arcs, since each unordered edge appears twice. A minimum-cost circulation costs no more than any other circulation of the network.

The residual capacity is $u_f(v,w)=u(v,w)-f(v,w)$ . For a price function $p:V\to\mathbb R$ , the report writes the reduced cost as $c_p(v,w)=c(v,w)-p(v)+p(w)$ . A circulation is $\varepsilon$ -optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$ . It is $\varepsilon$ -optimal if some price function works, where $\varepsilon\ge0$ . The tight error $\varepsilon(f)$ is the least such error. A circulation is $\varepsilon$ -tight when it is $\varepsilon$ -optimal but fails to be $\varepsilon'$ -optimal at every $\varepsilon'<\varepsilon$ . This includes attainment at $\varepsilon$ .

An arc is $\varepsilon$ -fixed if all $\varepsilon$ -optimal circulations carry the same flow through it. Write $F_\varepsilon$ for the set of these arcs. Theorem 4.2 supplies an arc-fixing criterion from a large absolute reduced cost. Lemma 4.4 says that when a positive tight error falls by a factor of $2n$ , $F_\varepsilon$ becomes strictly larger. Both are numbered results on printed pages 16–17 of the source report's journal counterpart.

Formalization targets

The goal is the circulation-level form of Theorem 4.5. Begin with a circulation $f_0$ and a sequence $f_0,f_1,\ldots$ whose positive-error steps satisfy the contract of Figure 3: if $\varepsilon(f_k)>0$ , the next circulation is $\varepsilon(f_k)/2$ -optimal. With the report's standing $n\ge2$ and $m\ge n-1$ , the target is

\exists k\le m\left\lceil\log_2(2n)\right\rceil:\quad \varepsilon(f_k)=0\quad\text{and}\quad f_k\text{ is minimum-cost}.

The milestone list contains the already proved complementary-slackness characterization of minimum cost (Theorem 2.2), the cross-parameter arc-fixing result (Theorem 4.2), and strict growth of fixed arcs (Lemma 4.4). The report states Theorem 4.5 as $O(m\log n)$ iterations when each refinement decreases error by a constant factor. The target makes explicit the factor two used by the paper's refinements and the resulting finite count.

What the result establishes

The theorem gives a bound on the number of refinement calls that depends on the number of vertices and arcs, not on the magnitude, precision, or integrality of the costs. It gives an exact minimum-cost circulation rather than an arbitrary small-error approximation. This distinguishes the real-cost loop from an integer-cost stopping rule based on $1/n$ . The bound counts refinement calls only; the report analyzes the work within particular implementations separately.

The published 1989 definitions and the complementary-slackness theorem already have machine-checked status on the platform. Theorem 4.2, Lemma 4.4, and this iteration theorem are the open formalization targets. A complete development will connect the tight error to residual-cycle structure, establish that its infimum is attained for circulations, and prove that zero tight error implies minimum cost. The mission thereby makes the fixed-arc argument reusable for other circulation algorithms that lower an approximate-optimality parameter.

Why the bound needs more than repeated halving

Repeatedly dividing a positive real error by two gives errors approaching zero, but it does not by itself produce a finite step with zero error. The missing finite progress is structural: an arc must become fixed after enough reductions, and only finitely many arcs exist. Proving that fixedness is strict is delicate because it compares all circulations at two different error levels, not just two consecutive flows. Theorem 4.2 is the quantitative bridge between a price certificate for one flow and agreement of an arc across every sufficiently accurate flow. At the boundary $\varepsilon=0$ , the printed wording of Lemma 4.4 would require $F_0$ to be a proper subset of itself, so its positive-error regime must be made explicit.

Formalization scope

The Lean network uses CycleCanceling.MinMean.CircNetwork with a finite vertex type, a finite symmetric arc set, and real-valued capacities, costs, and flows. Off-arc values of these functions are irrelevant. The report assumes $m\ge n-1\ge1$ on printed page 5; the theorem binders express it as $n\ge2$ and $m\ge n-1$ . The arc count is for ordered arcs, exactly as the report defines $m$ . No integrality, rounding, or bounded-cost hypothesis is imposed. A feasible initial circulation is required because Figure 3 starts from one; infeasibility detection is outside this target.

The reused 1989 definitions write reduced cost as $c(v,w)+p(v)-p(w)$ . Substituting $-p$ for $p$ gives the report's $c(v,w)-p(v)+p(w)$ , so existential price certificates, $\varepsilon$ -optimality, and absolute reduced-cost conditions agree. The tight error is represented by a real infimum; proving that it is attained is part of the work. The set $F_\varepsilon$ is filtered from $E$ and includes only arcs whose flow is shared by all $\varepsilon$ -optimal circulations. The halving run computes its error from the current circulation; it does not take an unrelated error sequence. Once that error is zero, the loop has returned and later sequence entries are unconstrained. These choices exclude a vacuous or artificially fixed error parameter and a preselected optimal flow.

The explicit reading of the report's asymptotic count is $t=\lceil\log_2(2n)\rceil$ halvings per factor- $2n$ reduction and at most $m$ such blocks, giving $m t$ refinements. This is a statement about refinement count, not a RAM-operation bound. Contributions on Theorem 4.2, the residual-cycle characterization of positive tight error, the fixed-arc strictness lemma, and the final finite counting argument all support the goal. The circulation, price, and fixed-arc infrastructure can be reused beyond this particular implementation.

Selected references

A. V. Goldberg and R. E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987; journal version in Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI: 10.1287/moor.15.3.430. The mission's page and theorem indices refer to the 1987 report.

9 thms3 active usersReviewed

Combinatorics Graph Theory Probability·Captain: mikedeng1

The Chromatic Number of Random Graphs: For Fixed 0 < p < 1, Almost Every G(n,p) Has n/s₀ ≤ χ(G) ≤ (n/s₀)(1 + 3 log log n / log n), where s₀ ≈ 2 log_d n and d = 1/(1−p)Research Paper

Motivation

The chromatic number $\chi(G)$ of a graph is the least number of colours in a proper vertex colouring. Determining it for a typical graph was, in the words of the paper, "one of the best known and most studied unsolved problems in the theory of random graphs". For the dense random graph $G_{n,p}$ with fixed edge probability $p$ , the clique number had been known precisely since the 1970s, but the chromatic number was known only up to a factor of $2$ .

Timeline:

1975. Grimmett and McDiarmid (doi:10.1017/S0305004100051124) proved that almost every $G_{n,p}$ satisfies $\frac{n}{2\log_d n}(1+o(1))\le\chi(G_{n,p})\le\frac{n}{\log_d n}(1+o(1))$ , with $d=1/(1-p)$ . The lower bound comes from the independence number; the upper bound from the greedy algorithm.
1976. Bollobás and Erdős (doi:10.1017/S0305004100053056) determined the clique number of $G_{n,p}$ up to two consecutive values, and slightly sharpened the bounds above.
1987. Matula (Combinatorica 7) improved the upper bound to $\frac{2n}{3\log_d n}(1+o(1))$ . Shamir and Spencer (Combinatorica 7) proved that $\chi(G_{n,p})$ is concentrated on an interval of length $\omega(n)\sqrt n$ , without locating that interval.
1988. Bollobás (this paper, doi:10.1007/BF02122551) showed that the lower bound is the truth: $\chi(G_{n,p})=(1+o(1))\,n/(2\log_d n)$ for almost every $G_{n,p}$ .

Setting

Let $n\ge 1$ , let $V=[n]$ , and let $N=\binom n2$ . For a fixed real $0<p<1$ , the random graph $G_p=G_{n,p}$ includes each of the $N$ pairs of vertices as an edge independently with probability $p$ . A graph $G$ on $V$ with $e(G)$ edges thus occurs with probability $p^{e(G)}(1-p)^{N-e(G)}$ . A property of graphs holds for almost every $G_p$ if its probability tends to $1$ as $n\to\infty$ .

Put $q=1-p$ and $d=1/q$ . Write $\log$ for the natural logarithm and $[x]$ for the integer part of $x$ , and set

s_0=\bigl[\,2\log_d n-\log_d\log_d n+2\log_d(e/2)+1\,\bigr].

$s_0$ is slightly larger than the independence number of $G_p$ , which is about $2\log_d n-2\log_d\log_d n$ .

Supporting objects: $E(n,r)=\binom nr p^{\binom r2}$ is the expected number of $r$ -cliques of $G_{n,p}$ , and $E_q(n,r)$ is the same with $q$ for $p$ . $X$ is the maximal number of pairwise edge-disjoint $K^r$ subgraphs, and $X'$ is the number of $K^r$ subgraphs that share no edge with any other $K^r$ . Finally $s_1=s_0-\lfloor 5\log_d\log n\rfloor$ .

Formalization targets

Goal: Theorem 4

\mathbb P\Bigl(\frac n{s_0}\le\chi(G_p)\le\frac n{s_0}\Bigl(1+\frac{3\log\log n}{\log n}\Bigr)\Bigr)\longrightarrow 1\qquad(n\to\infty).

Both bounds are part of the goal. The companion statement $\chi(G_p)=(n/s_0)(1+o(1))$ for almost every $G_p$ is a separate item.

Milestones

Lemma 1 (a martingale inequality the paper attributes to Freedman). If $|X_{k+1}-X_k|\le c$ , $b=mc^2$ and $a>0$ , then $\mathbb P(X_m\le\mathbb E X_m-a)\le\bigl(\tfrac b{a+b}\bigr)^{a+b}e^a\le\exp\{-a^2/2(a+b)\}$ .
Adding one edge changes $X$ by at most one. Hence (5): $\mathbb P(X\le\mathbb EX-a)\le\exp\{-a^2/2(a+N)\}$ .
(6), (8), (9): $\mathbb E(X')\ge(1+o(1))E(n,r)$ when $E(n,r)=n^\alpha$ , $\alpha\ge\tfrac12$ , $n^\alpha=o(n^2/(\log n)^4)$ .
Theorem 2: under those hypotheses, $\mathbb P(Y_r\le(1-c)n^\alpha)\le\exp\{-(c^2+o(1))n^{2\alpha-2}\}$ for $0<c\le1$ , where $Y_r$ is the number of $r$ -cliques.
Corollary 3: under explicit growth conditions on $n'$ and $r'$ , almost every $G_p$ has a $K^{r'}$ in every $n'$ -subset of vertices.
The complement of $G_p$ is $G_q$ , and almost no $G_q$ contains $K^{s_0+1}$ . This gives the lower bound.
The choice of $n_1$ with $2n_1^{5/3}\le E_q(n_1,s_1)\le3n_1^{5/3}$ and $n_1=O(n/(\log n)^2)$ ; the greedy colouring bound $\chi\le n/s_1+n_1$ ; and the final inequality $n/s_1+n_1<(n/s_0)(1+3\log\log n/\log n)$ .

Significance

Theorem 4 settles the first-order asymptotics of $\chi(G_{n,p})$ for constant $p$ : $\chi(G_{n,p})\sim n/(2\log_d n)$ . It shows that the trivial lower bound $n/\alpha(G)$ is asymptotically tight. It also shows that greedy colouring, which uses about twice as many colours, is far from optimal. The method also became standard: concentration of a cleverly chosen packing variable, combined with the edge-exposure martingale. It reappears in Łuczak's extension to sparse random graphs and in the later literature on the concentration of $\chi(G_{n,p})$ .

The theorem has been proved since 1988 and is textbook material (Bollobás, Random Graphs; Alon–Spencer, The Probabilistic Method). As of this mission it has no machine-checked proof in Mathlib. A formal proof would add:

a reusable finite model of $G(n,p)$ on SimpleGraph (Fin n);
a lower-tail martingale inequality of Freedman type;
the first formal treatment of the edge-exposure martingale;
a careful audit of the paper's constants, several of which are misprinted (see Formalization scope).

Difficulty

The natural first attempt is to colour greedily and to control the independence number of every large vertex set by a union bound. It fails. The probability that a fixed set of $n'$ vertices has no independent set of size about $2\log_d n'$ is not small enough to beat the $\binom n{n'}$ sets. The second moment method gives only a polynomially small failure probability, and that is what limits earlier results to a constant factor.

The paper needs a failure probability of order $\exp(-n'^{1+\delta})$ for the absence of a large independent set. Two difficulties block this:

The number $Y_r$ of $r$ -cliques is not a Lipschitz function of the edges: one edge can lie in many cliques.
Its concentration is therefore not available from a bounded-differences inequality.

Replacing $Y_r$ by the edge-disjoint packing number $X$ restores the Lipschitz property. The price is a lower bound on $\mathbb E X$ , which requires the count $X'$ of "isolated" cliques and a delicate estimate of the overlap sums $\sum_l F_l$ . These estimates depend on $r$ being within $O(1)$ of the clique number, so the asymptotics of $r_1(n)$ and of the binomial coefficients must be controlled uniformly in $n$ .

Formalization scope

Model. Vertices are Fin n, graphs are SimpleGraph (Fin n), and $G(n,p)$ is given by explicit finite sums: the weight $p^{e(G)}(1-p)^{N-e(G)}$ , probabilities and expectations. No measure is built for the random graph. "Almost every" is Tendsto (fun n => P_n) atTop (𝓝 1). Lemma 1 alone is stated on an arbitrary probability space with a Mathlib Filtration and Martingale.
Fixed $p$ . $p$ is a real constant with $0<p<1$ , the standing assumption of §1, and never depends on $n$ .
Asymptotic notation. $o(1)$ is an explicit sequence $\varepsilon_n\to0$ , quantified after every parameter the page fixes. $f=o(g)$ is Asymptotics.IsLittleO. Hypotheses on $n$ -indexed sequences hold for all large $n$ , because $E(n,r)=n^\alpha$ cannot hold for small $n$ .
Conventions. $\chi$ is Mathlib's chromaticNumber, which is finite on Fin n and converted to ℕ. $s_0,s_1$ are integers built with Int.floor and Real.logb d. For small $n$ they take junk values that no asymptotic statement depends on.
Corrected misprints, each disclosed in the item's Formalization Note:
- Theorem 2's exponent is stated as in the last display of its proof, $\exp\{-(c^2+o(1))n^{2\alpha-2}\}$ .
- (6) omits a factor $\mathbb P(A)$ ; the inequality is stated without conditioning.
- The "maximal" $n_1$ should be minimal; only its existence is stated.
- The printed $n_1\le n/(\log n)^2$ is false with constant $1$ and is replaced by $n_1\le Cn/(\log n)^2$ for some $C>0$ .
- The last display has $n/s_1$ on its right-hand side; it is stated with $n/s_0$ , which is what Theorem 4 requires.
Added hypotheses. Lemma 1 assumes $X_0$ almost surely constant, without which it is false at $m=0$ ; this matches the paper's application. The greedy colouring assumes $s\ge1$ .
Not trivializable. The goal mentions only $\chi$ , $s_0$ and the random graph. It contains no martingale, packing number, $s_1$ or $n_1$ . It keeps both bounds, so neither the well-known lower bound alone nor the asymptotic companion suffices.
Infrastructure needed and reusable:
- the identity $\sum_G p^{e(G)}(1-p)^{N-e(G)}=1$ , and the marginalization over a fixed edge set;
- the edge-exposure martingale on SimpleGraph (Fin n);
- a one-sided Freedman/Bennett inequality, for which Mathlib's conditional sub-Gaussian MGF bounds are a natural starting point;
- Stirling-type estimates for $\binom nr p^{\binom r2}$ near the clique number.

Contributions to any of these are welcome, as are independent proofs of the deterministic milestones (greedy colouring, the final inequality, the complement identity).

Selected references

B. Bollobás, The chromatic number of random graphs, Combinatorica 8 (1988) 49–55. https://doi.org/10.1007/BF02122551
G. R. Grimmett and C. J. H. McDiarmid, On colouring random graphs, Math. Proc. Cambridge Philos. Soc. 77 (1975) 313–324. https://doi.org/10.1017/S0305004100051124
B. Bollobás and P. Erdős, Cliques in random graphs, Math. Proc. Cambridge Philos. Soc. 80 (1976) 419–427. https://doi.org/10.1017/S0305004100053056
D. W. Matula, Expose-and-merge exploration and the chromatic number of a random graph, Combinatorica 7 (1987).
E. Shamir and J. Spencer, Sharp concentration of the chromatic number on random graphs $G_{n,p}$ , Combinatorica 7 (1987).
D. A. Freedman, On tail probabilities for martingales, Ann. Probab. 3 (1975) 100–118. https://doi.org/10.1214/aop/1176996452
K. Azuma, Weighted sums of certain dependent random variables, Tôhoku Math. J. 19 (1967) 357–367. https://doi.org/10.2748/tmj/1178243286
B. Bollobás, Random Graphs, Academic Press, 1985.

15 thms3 active usersReviewed

Combinatorics Discrete Geometry Linear Optimization·Captain: mikedeng1

A Quasi-Polynomial Bound for the Diameter of Graphs of Polyhedra: Every Polyhedron Given by n Inequalities in ℝ^d, Bounded or Not, Has Graph Diameter at Most n^(log₂ d + 2)Research Paper

Motivation

The simplex method solves a linear program by walking along the edges of the feasible polyhedron, from vertex to vertex. However cleverly a pivot rule chooses its steps, it cannot reach the optimum in fewer steps than the graph distance from the starting vertex. The largest possible graph diameter of a polyhedron therefore bounds from below the worst-case number of pivots of every pivot rule, and whether that diameter is polynomial in the size of the problem is one of the basic open questions of linear optimization (Klee–Kleinschmidt 1987).

Timeline.

1957: Hirsch conjectures that a $d$ -dimensional polyhedron with $n$ facets has graph diameter at most $n-d$ (reported in Dantzig, Linear Programming and Extensions, 1963).
1967: Klee and Walkup show the conjecture false for unbounded polyhedra, with the lower bound $n-d+[d/5]$ for $n\ge2d$ (Acta Math. 1967).
1967–1970: Barnette proves $\Delta(d,n)\le n3^{d-3}$ , and Larman improves it to $n2^{d-3}$ (Proc. LMS 1970); both are linear in $n$ but exponential in $d$ .
1990–1992: Kalai proves a subexponential bound, and then Kalai and Kleitman prove the quasi-polynomial bound $n^{\log d+2}$ that is the subject of this mission (Bull. AMS 1992, arXiv:math/9204233).
2012: Santos disproves the Hirsch conjecture for bounded polytopes (Ann. Math. 2012). Whether a polynomial bound holds remains open; the best general upper bounds known are refinements of the exponent of the Kalai–Kleitman bound.

Setting

A polyhedron in $\mathbb R^d$ is the solution set of finitely many linear inequalities,

P=\{x\in\mathbb R^d:\ \langle a_i,x\rangle\le b_i,\ i=1,\dots,n\},\qquad a_i\in\mathbb R^d,\ b_i\in\mathbb R .

It may be bounded or unbounded, and empty. Its vertices are its extreme points. Two distinct vertices $u,v$ are adjacent when the segment $[u,v]$ is an edge of $P$ , a one-dimensional face; unbounded one-dimensional faces (rays) are not edges. The graph $G(P)$ consists of these vertices and edges, and its diameter $\delta(P)$ is the largest graph distance between two vertices. Kalai and Kleitman write $\Delta(d,n)$ for the largest diameter of the graph of a $d$ -dimensional polyhedron with $n$ facets.

For a set $F$ of row indices, the relaxation $Q_F$ is the polyhedron obtained from $P$ by ignoring the inequalities with index outside $F$ . A walk of $B$ steps is a sequence $w_0,\dots,w_B$ of points in which each step stays put or crosses an edge; "diameter at most $B$ " means that any two vertices are joined by such a walk, which includes connectivity of the graph.

Formalization targets

Goal: Theorem 1

\Delta(d,n)\le n^{\log d+2}.

Stated for polyhedra given by inequalities: for all $d,n$ and all $a\in(\mathbb R^d)^n$ , $b\in\mathbb R^n$ , the graph of $P$ is connected and has diameter at most $\lfloor n^{\log_2 d+2}\rfloor$ . No nonemptiness, boundedness or full-dimensionality is assumed.

Milestones, in the order the proof uses them

If a vertex $\omega$ of $P$ satisfies with equality only rows in $F$ , then $\omega$ is a vertex of $Q_F$ (published).
If an edge of $Q_F$ starts at a point of $P$ and is not an edge of $P$ , then it meets the hyperplane of an ignored row at a vertex of $P$ adjacent to its start, or at its start (published).
The claim $k_v\le\Delta(d,[n/2])$ : if every vertex within distance $k$ of $v$ lies only on rows of $F$ , and $G(Q_F)$ has diameter at most $B$ , then every vertex within distance $k$ of $v$ is within distance $B$ of $v$ .
The facet step: any two vertices of a face $\{x\in P:\langle a_i,x\rangle=b_i\}$ with $a_i\ne0$ are joined, inside that face, by a walk of at most $\Delta(d-1,n-1)$ edges.
The recursion $\Delta(d,n)\le\Delta(d-1,n-1)+2\Delta(d,[n/2])+2$ , for polyhedra with nonzero rows.
The arithmetic: $N(d,n)=\lfloor n^{\log_2 d+2}\rfloor$ satisfies $N(d-1,n-1)+2N(d,\lfloor n/2\rfloor)+2\le N(d,n)$ for $d\ge2$ , $n\ge d+1$ .

Significance

The bound is polynomial in $n$ for each fixed $d$ , and $n^{O(\log d)}$ overall. Before it, every bound was exponential in $d$ or subexponential in $n$ . It remains, up to improvements of the exponent, the best known upper bound on the diameter of polyhedra, and thus the best known limit on how badly an optimal pivot rule must behave. Its proof is also the template for the later abstractions of the problem (connected layer families, subset partition graphs) in which the polynomial Hirsch question is studied.

The bounded case is already formalized on the platform: Hirsch.kalai_kleitman_bound states the theorem for nonempty bounded polytopes and is Proved, together with the bounded forms of the recursion (Hirsch.kalai_kleitman_recursion), of the facet step (Hirsch.facet_reduction, Hirsch.facet_walk) and of the zero-row reduction (Hirsch.diamLE_of_nonzero_rows), and the one-step relaxation lemma Hirsch.relaxation_no_new_neighbours. Kalai and Kleitman state Theorem 1 for all polyhedra: their introduction contrasts unbounded polyhedra (where Hirsch fails) with bounded ones. This mission formalizes the theorem as the paper states it, including unbounded polyhedra, where the bounded proofs do not apply as written. The combinatorial abstraction of the same bound (EHRR10.KalaiKleitman.diameter_le_kalai_kleitman, for the Eisenbrand–Hähnle–Razborov–Rothvoß model) is a different object and is not reused.

Difficulty

The bounded argument relies on compactness: faces are polytopes, every relaxation used in the induction is again a polytope, and the facet of a polytope is a polytope of one dimension less. The relaxation $Q_F$ contains $P$ and is typically unbounded even when $P$ is bounded, and for an unbounded polyhedron a face on a facet hyperplane can be unbounded or have no vertices at all. Each step must therefore hold for general polyhedra: that a shortest walk in $G(Q_F)$ between two vertices of the ball uses only edges of $P$ , and that the graph of a face, identified with a polyhedron in $\mathbb R^{d-1}$ , sits inside $G(P)$ . The "maximal positive number $k_v$ " of the paper need not exist, and the proof must handle the two cases (no radius qualifies; every radius qualifies) separately. Zero rows are allowed in the goal and must be removed before the recursion applies, since a zero row with $b_i=0$ is tight everywhere.

Formalization scope

Lean represents $\mathbb R^d$ as EuclideanSpace ℝ (Fin d) and the polyhedron as Hirsch.Hpoly a b with a : Fin n → ℝ^d, b : Fin n → ℝ, from the published definition Hirsch_model, which also supplies adjacency Hirsch.Adj (the segment is an extreme subset) and the diameter predicate Hirsch.DiamLE. The mission commits to these explicit readings:

" $\Delta(d,n)\le N$ " is ∀ a b, DiamLE (Hpoly a b) N over $n$ inequalities in $\mathbb R^d$ . This is equivalent to the facet formulation, since a $d$ -dimensional polyhedron is cut out by its facet inequalities and a polyhedron given by $n$ inequalities in $\mathbb R^d$ has dimension at most $d$ and at most $n$ facets.
"log" is $\log_2$ (Real.logb 2), the power is the real power, and the integer bound is its floor ⌊·⌋₊, which is equivalent because distances are natural numbers.
" $[n/2]$ " is $\lfloor n/2\rfloor$ (ℕ division); "at most $n/2$ facets" is a row set of cardinality at most $\lfloor n/2\rfloor$ .
An ignored row is replaced by the vacuous inequality $\langle0,x\rangle\le1$ , which keeps the index type Fin n.
Walks have exactly $B$ steps with stationary steps allowed, so " $B$ steps" means "at most $B$ edges".
The paper's $k_v$ is not defined; milestone 3 quantifies over every radius with the ball property.
Milestones 4 and 5 assume nonzero rows; the goal does not.

A statement with a boundedness or nonemptiness hypothesis, with the graph diameter measured by a distance function whose value on unreachable pairs is $0$ , or with the bound read with Nat.log or the natural logarithm, is not the target. Contributions welcome: proofs of the general-polyhedron facet step and of milestone 3, a general zero-row reduction, the arithmetic of milestone 6, and the base cases $d\le1$ and $n\le d$ .

Selected references

G. Kalai and D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26 (1992), 315–316. https://doi.org/10.1090/S0273-0979-1992-00285-9 (arXiv:math/9204233)
V. Klee and D. W. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Math. 117 (1967), 53–78. https://doi.org/10.1007/BF02395040
V. Klee and P. Kleinschmidt, The d-step conjecture and its relatives, Math. Oper. Res. 12 (1987), 718–755. https://doi.org/10.1287/moor.12.4.718
D. G. Larman, Paths on polytopes, Proc. London Math. Soc. (3) 20 (1970), 161–178. https://doi.org/10.1112/plms/s3-20.1.161
F. Santos, A counterexample to the Hirsch conjecture, Ann. of Math. 176 (2012), 383–412. https://doi.org/10.4007/annals.2012.176.1.7

9 thms3 active usersReviewed

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

MNL-Bandit: A Dynamic Learning Approach to Assortment Selection I: The Epoch-Based UCB Policy Has Regret at Most C₁√(NT log NT) + C₂N log² NT Under the No-Purchase AssumptionResearch Paper

Motivation

A retailer that decides which products to display, an online platform that decides which items to show in a recommendation slot, and an airline that decides which fare classes to open all face the same problem: the set of options offered changes what customers buy, and the substitution pattern is not known in advance. The multinomial logit (MNL) model is the standard model of this substitution in revenue management (Talluri and van Ryzin 2004), and optimizing the offered set under a known MNL model is a classical, efficiently solvable problem (e.g. Rusmevichientong, Shen and Shmoys 2010, for a capacity constraint).

The MNL-Bandit asks what happens when the MNL parameters are unknown and must be learned from the purchases themselves, while revenue is being earned. Earlier approaches (Rusmevichientong, Shen and Shmoys 2010; Sauré and Zeevi 2013) separate exploration from exploitation and need the gap between the best and the second-best assortment to be known. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 2019, arXiv:1706.03880) give a single upper-confidence-bound policy whose regret is of order $\sqrt{NT}$ up to logarithmic factors, with no such knowledge. This mission formalizes that result, Theorem 1 of the paper.

Setting

There are $N$ products with known revenues $r_i\in[0,1]$ . At each time $t=1,\dots,T$ the seller offers an assortment $S_t$ from a family $\mathcal S$ of feasible subsets of $\{1,\dots,N\}$ , and one customer either buys a product $c_t\in S_t$ or buys nothing ( $c_t=0$ ). Given $S_t=S$ , the choice follows the MNL model with attraction parameters $v_1,\dots,v_N\ge0$ and $v_0=1$ :

p_i(S)=\frac{v_i}{1+\sum_{j\in S}v_j}\quad(i\in S\cup\{0\}),\qquad p_i(S)=0\ \text{otherwise},

independently of the past. The expected revenue of $S$ is $R(S,v)=\sum_{i\in S}r_iv_i\big/\big(1+\sum_{j\in S}v_j\big)$ . The family $\mathcal S$ is described by totally unimodular constraints, $\mathcal S=\{S : A\,x(S)\le b\}$ with $x(S)$ the incidence vector of $S$ , $A$ totally unimodular and $b$ integral (cardinality constraints are the main example). A policy chooses $S_t$ from the past choices, and its regret is

\mathrm{Reg}_\pi(T,v)=T\,R(S^*,v)-\mathbb E_\pi\Big[\sum_{t=1}^TR(S_t,v)\Big],\qquad R(S^*,v)=\max_{S\in\mathcal S}R(S,v).

The seller knows $r$ and $\mathcal S$ but not $v$ .

Algorithm 1 works in epochs: epoch $\ell$ offers one assortment $S_\ell$ repeatedly until a customer buys nothing. Let $\hat v_{i,\ell}$ be the number of purchases of $i$ in epoch $\ell$ , $T_i(\ell)$ the number of the first $\ell$ epochs that offered $i$ , and $\bar v_{i,\ell}$ the average of $\hat v_{i,\tau}$ over those epochs. The algorithm forms the upper confidence bounds

v^{\mathrm{UCB}}_{i,\ell}=\bar v_{i,\ell}+\sqrt{\bar v_{i,\ell}\,\frac{48\log(\sqrt N\ell+1)}{T_i(\ell)}}+\frac{48\log(\sqrt N\ell+1)}{T_i(\ell)},

starting from $v^{\mathrm{UCB}}_{i,0}=1$ , and offers next the assortment in $\mathcal S$ that maximizes $R(S,v^{\mathrm{UCB}}_{\cdot,\ell})$ .

Formalization targets

Goal: Theorem 1 (p. 11)

Under Assumption 4.1 (every $v_i\le v_0=1$ , and $\mathcal S$ is closed under taking subsets) there are absolute constants $C_1,C_2$ such that for every instance and every horizon $T$ ,

\mathrm{Reg}_\pi(T,v)\le C_1\sqrt{NT\log NT}+C_2N\log^2NT .

The constants are not fixed: the goal asserts the order of the regret, which is what the paper claims.

Milestones

The milestones follow the proof in Appendix A of the paper:

The law of an epoch's purchase count: Lemma A.1, its moment generating function given the offered assortment.
Concentration: Theorem 5, Chernoff bounds for geometric variables; Corollary D.1; and Lemma A.2 for the averages $\bar v_{i,\ell}$ along Algorithm 1.
Lemma 4.1: $v^{\mathrm{UCB}}_{i,\ell}\ge v_i$ with probability at least $1-6/(N\ell)$ , and its rate of convergence.
Optimism of the revenue estimate: Lemma A.3 (monotonicity of the optimal revenue in $v$ ) and Lemma 4.2.
The per-epoch error: Lemma A.4 (a Lipschitz bound) and Lemma 4.3.
The epoch decomposition of the regret, (A.14).

Significance

Theorem 1 shows that learning the choice model costs only $\tilde O(\sqrt{NT})$ revenue, with no dependence on how separated the instance is. The paper also proves a lower bound of order $\sqrt{NT/K}$ under a $K$ -cardinality constraint (its Theorem 2), so for small $K$ the bound is optimal up to logarithmic factors. The epoch device used here reduces the analysis of a choice model with substitution to unbiased i.i.d. estimates of each $v_i$ .

The result is proved in the paper (Appendix A, with the concentration bounds in Appendix D). It has not been machine-checked. A formal proof would also settle several printed slips that the formalization had to repair (listed under Formalization scope). The concentration bounds for geometric variables, Theorem 5 and Corollary D.1, are useful outside this mission.

Difficulty

The estimates $\hat v_{i,\ell}$ are counted in epochs whose assortments are chosen adaptively from earlier estimates, so they are not independent a priori. The paper's argument that they are i.i.d. geometric with mean $v_i$ has to be made rigorous for an adaptive policy. The variables are unbounded, so the standard Chernoff–Hoeffding bounds for bounded variables do not apply, and the number of samples $T_i(\ell)$ is random, which requires a union bound over all its possible values. Finally, the regret is a sum over customers while the analysis is per epoch, and the two are linked through the expected epoch length $1+\sum_{j\in S_\ell}v_j$ under a random number of epochs and a horizon that cuts the last one.

Formalization scope

Model. Products are Fin N; a choice is none (no purchase) or some i. The parameter $v_0$ is normalized to $1$ , as the paper allows. Algorithm 1 is deterministic, so a history of horizon $T$ is a sequence of $T$ choices with the product law $\prod_tp_{c_t}(S_t)$ , and every expectation is a finite sum. The revenue $R(S,v)$ is the published definition ChoiceCDLP.MNL.mnlObjective v r 1 S.
Feasible family. $\mathcal S$ is a finite family with the TU representation (2.3), closed under subsets, and nonempty (the paper presupposes nonemptiness when it writes $S^*=\arg\max$ ).
Algorithm. Algorithm 1 is a policy defined by recursion on the history. It receives $r$ and an argmax selector for $\mathcal S$ , never $v$ . Every statement quantifies over all selectors, that is, over every tie-breaking rule. While a product has never been offered, its $v^{\mathrm{UCB}}$ stays at the initial value $1$ .
Epoch events. The lemmas about epoch $\ell$ are stated for every finite horizon $T$ , on the event that epoch $\ell$ is completed by customer $T$ ; uniformity in $T$ is the paper's infinite-horizon statement.
Repairs of the page, all disclosed in the items:
1. Lemma A.2's misprinted $\log(\ell+1)$ is replaced by $\log(\sqrt N\ell+1)$ .
2. Lemmas 4.2 and 4.3 are indexed by the estimate built at the end of epoch $\ell$ .
3. Lemma 4.3's free index $i$ becomes the sum over $i\in S_{\ell+1}$ .
4. Lemmas 4.1 and 4.3 use the explicit constants $C_1=\sqrt{72}+\sqrt{24}$ and $C_2=144$ of the proof.
5. Lemma A.3 and Lemma 4.2 require positive parameters on the optimal set; the printed versions are false otherwise.
6. (A.14) is an inequality, since the horizon cuts the last epoch.
Not stated. Corollary A.1 (the epoch estimates are i.i.d. geometric across the epochs of the adaptive policy) is not posed as an item: a single-epoch law would be a weaker statement than the page's.
No trivialization. The policy cannot see $v$ , the constants of the goal precede every other quantifier, and the regret is the paper's (2.6), so the goal cannot be met by a policy that offers $S^*$ or by constants that depend on the instance.
Welcome contributions. Infrastructure for adaptive sampling (the i.i.d. property of the epoch estimates), Chernoff bounds for geometric and sub-exponential variables, and a Wald-type identity for epochs.

The paper's own proofs are in its Appendices A and D.

Selected references

S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5):1453–1485, 2019. arXiv:1706.03880v2, doi:10.1287/opre.2018.1832
P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic assortment optimization with a multinomial logit choice model and capacity constraint, Operations Research 58(6):1666–1680, 2010. doi:10.1287/opre.1100.0866
D. Sauré, A. Zeevi, Optimal dynamic assortment planning with demand learning, Manufacturing & Service Operations Management 15(3):387–404, 2013. doi:10.1287/msom.2013.0429
K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1):15–33, 2004. doi:10.1287/mnsc.1030.0147
M. Mitzenmacher, E. Upfal, Probability and Computing, Cambridge University Press, 2005.

15 thms3 active usersReviewed

Completed

Combinatorics Operations Research Probability+1·Captain: mikedeng1

Online Stochastic Matching: Beating 1-1/e 3: No Online Algorithm Beats Expected Approximation Factor 26/27 on a 6-Cycle, and None Reaches 1 − o(1) on Disjoint 6-CyclesResearch Paper

Motivation

Online bipartite matching asks an algorithm to assign arriving requests to resources it cannot reassign later. In display advertising, the requests are page views (impressions) and the resources are advertisers who have bought a fixed number of impressions in advance; each impression must be served immediately or lost. In the adversarial model, Karp, Vazirani and Vazirani (STOC 1990) showed that the RANKING algorithm achieves a $1 - 1/e$ fraction of the optimum in expectation, and that no online algorithm does better. Advertising systems, however, have historical traffic data, which motivates the i.i.d. model: the impression types are drawn independently from a distribution that is known in advance.

Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) were the first to beat $1 - 1/e$ in this model, with an algorithm that achieves $\approx 0.67$ with high probability. Their Section 3 asks the complementary question: how close to $1$ can any online algorithm get when the distribution is known? Their Theorem 3 answers that the expected approximation factor of every online algorithm is bounded strictly away from $1$ , already on a graph with six vertices. Later work in the same model (Manshadi, Oveis Gharan and Saberi, SODA 2011, arXiv:1007.1673) sharpened both the algorithmic and the hardness side.

Setting

An instance consists of a bipartite graph $G = (A, I, E)$ between a finite set $A$ of advertisers and a finite set $I$ of impression types, a distribution $D$ on $I$ , and a number $n$ of arrivals. In this mission $D$ is the uniform distribution on $I$ . Online, $n$ impressions arrive one at a time; their types $\omega(0), \dots, \omega(n-1)$ are independent draws from $D$ . When impression $t$ arrives, the algorithm must immediately either assign it to an advertiser $a$ with $(a, \omega(t)) \in E$ that has not yet been used, or leave it unassigned. Each advertiser can be used at most once, and decisions are final.

A deterministic online algorithm decides what to do with arrival $t$ from the types $\omega(0), \dots, \omega(t)$ seen so far; it knows $G$ , $D$ and $n$ , but not the future. A randomized online algorithm is a probability distribution over deterministic ones. $\mathrm{ALG}(\omega)$ is the number of impressions the algorithm assigns on the arrival sequence $\omega$ . $\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 adjacent to $\omega(t)$ : the most impressions that could have been assigned with hindsight. The expected approximation factor of an algorithm is

\mathbb E\!\left[\frac{\mathrm{ALG}(\omega)}{\mathrm{OPT}(\omega)}\right],

the expectation taken over the algorithm's randomness and the arrivals.

The 6-cycle instance has $A = \{a, b, c\}$ , $I = \{x, y, z\}$ and $E = \{(x,a),(y,a),(y,b),(z,b),(z,c),(x,c)\}$ , with the uniform distribution and $n = 3$ . The family $\Gamma_k$ consists of $k$ disjoint copies of the 6-cycle, with the uniform distribution on its $3k$ impression types and $n = 3k$ arrivals.

Formalization targets

Goal: Theorem 3

On the 6-cycle, every randomized online algorithm satisfies

\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le \frac{26}{27},

and there are a constant $c < 1$ and a threshold $K_0$ such that for every $k \ge K_0$ and every randomized online algorithm on $\Gamma_k$ ,

\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le c .

The second part is the paper's "there exists a family of instances with $n \to \infty$ for which no algorithm can achieve an expected approximation of $1 - o(1)$ ", stated on the paper's own family. It leaves $c$ unspecified: Appendix B estimates $c \approx 0.9898$ through approximate counts, and a sharper constant would not invalidate the goal.

Milestones

The $(x, y, y)$ scenario (§3, p. 4). For every deterministic online algorithm on the 6-cycle and every type $u$ of the first arrival there is a type $v$ with $\mathrm{ALG}(u, v, v) \le 2$ and $\mathrm{OPT}(u, v, v) = 3$ .
Theorem 3, first sentence (p. 4). The bound $26/27$ on the 6-cycle, for every randomized online algorithm.

Significance

Theorem 3 sets the ceiling against which algorithms in the i.i.d. model are measured. It rules out an online algorithm with expected factor arbitrarily close to $1$ , even though the distribution is known and the instance is tiny, so a constant-factor gap between online and offline matching is intrinsic to the model and not an artefact of adversarial arrivals. The paper's positive results ( $1 - 1/e$ for the Suggested Matching algorithm, $\approx 0.67$ for Two Suggested Matchings) sit between $1 - 1/e$ and this ceiling.

The single-instance bound has a short counting proof. The family statement is argued in the paper only in outline: Appendix B approximates the fractions of copies receiving $1$ , $2$ , $3$ or more impressions, assumes the most favourable outcome on each, and reports the resulting ratio as approximately $0.9898$ . A machine-checked proof of the family statement would turn that sketch into a theorem with an explicit constant. To our knowledge neither part has been formalized before.

Difficulty

The single-cycle bound reduces to a finite check, but the paper's "without loss of generality (from the symmetry of the 6-cycle)" hides the cases the algorithm can choose: assigning the first impression to either neighbour, or not assigning it at all. Each case needs its own bad continuation. The passage from deterministic to randomized algorithms is an averaging step.

The family bound is harder. On $\Gamma_k$ the algorithm sees all arrivals in all copies and may coordinate its decisions across copies, so the per-copy loss of the single cycle does not transfer by independence. Moreover the target is the expectation of a ratio, $\mathbb E[\mathrm{ALG}/\mathrm{OPT}]$ , not a ratio of expectations: a bound on the expected loss must be combined with concentration of the number of copies that receive exactly three impressions, and with a lower bound on $\mathrm{OPT}$ that holds with high probability. The approximations " $\simeq 3/e^3$ , $9/(2e^3)$ , $27/(6e^3)$ " of Appendix B have unquantified errors and cannot be used as they stand.

Formalization scope

The model is formalized for general finite $A$ and $I$ with uniform arrivals. Arrival sequences are functions Fin n → I. A deterministic online algorithm is a function that receives the time $t$ , the prefix of the first $t$ types (Fin t → I) and the current type, and returns an advertiser or none; it cannot read later arrivals. A proposal of a non-adjacent or already used advertiser leaves the impression unassigned, so the encoding covers all online algorithms, including ones that skip an impression while a neighbour is free. A randomized online algorithm is a probability distribution (PMF) on the finite type of deterministic algorithms; by Kuhn's theorem this is equivalent to fresh random choices at each step. $\mathrm{OPT}$ is the maximum size of an injective, edge-respecting partial assignment of arrivals to advertisers. The expected approximation factor is a finite average over all $|I|^n$ arrival sequences, weighted by the algorithm distribution.

The explicit instantiations of the paper's asymptotic wording are as follows:

"no algorithm can achieve an expected approximation of $1 - o(1)$ " becomes $\exists\, c < 1,\ \exists K_0,\ \forall k \ge K_0,\ \forall P:\ \mathbb E[\mathrm{ALG}/\mathrm{OPT}] \le c$ on $\Gamma_k$ , with $n = 3k$ tied to $k$ , and with $c$ and $K_0$ chosen before $k$ and before the algorithm.
The paper's constant $0.9898$ is not part of the statement.

Lean's division sets $x/0 = 0$ . A formalization of the form "there is an instance on which every algorithm has expected factor at most $26/27$ " would be satisfied trivially by a graph without edges, where $\mathrm{OPT} = 0$ ; the statements here are on the paper's explicit instances, where every impression type has an adjacent advertiser and $\mathrm{OPT} \ge 1$ on every arrival sequence.

A complete development needs finite case analysis on runs of online algorithms, averaging over mixed strategies, and, for the family, concentration inequalities for occupancy counts (Azuma or McDiarmid, both available on the platform) together with bounds on maximum matchings of disjoint unions. The online-algorithm model and the averaging lemmas are reusable for other lower bounds in the i.i.d. model. Proofs of either milestone, and independent proofs of the family statement with any explicit $c < 1$ , are welcome.

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
V. H. Manshadi, S. Oveis Gharan, A. Saberi, Online Stochastic Matching: Online Actions Based on Offline Statistics, SODA 2011; arXiv:1007.1673. https://arxiv.org/abs/1007.1673

5 thms3 active usersReviewed

Completed

Combinatorics Operations Research Probability+1·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

12 thms3 active usersReviewed

Completed

Machine Learning Optimization Reinforcement Learning·Captain: mikedeng1

On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift 6: Agnostic Q-NPG for Log-Linear Policies, Bounded by Transfer Error, Excess Risk and Condition NumberResearch Paper

Motivation

Policy gradient methods optimize a decision rule by changing the parameters that determine its action probabilities. In reinforcement learning, the objective is the expected total reward collected over time. Once a policy is restricted to a feature-based class, the best policy may be less effective than the unrestricted optimum. A useful guarantee must therefore compare the computed policy with a chosen comparator and account for both the limits of the features and the error in estimating an update direction. Agarwal, Kakade, Lee and Mahajan give such a guarantee for a version of the natural policy gradient method that fits action values with linear features, called Q-NPG (Agarwal et al., §6.2).

The result matters when a policy has far fewer parameters than there are state-action pairs. A bound phrased only for exact action values or an unrestricted policy class would leave out the errors introduced by fitting from samples and by moving the fitting distribution from the states of a comparator to the states visited by the current policy. Theorem 6.1 keeps those effects visible as separate terms. It also avoids assuming that the comparator is an optimal policy; the comparator can be a policy selected for an application or a benchmark within a restricted class.

Setting

A discounted Markov decision process has a finite state set S, a finite nonempty action set A, transition probabilities P(s'|s,a), immediate rewards r(s,a) in [0,1], and a discount factor γ in [0,1). A policy π assigns a probability distribution over A to every state. The value V^π(s) is the expected sum of discounted rewards from s, and V^π(ρ) averages this value over an initial state distribution ρ. The action value Q^π(s,a) starts by choosing a in s and then follows π. Its advantage is A^π(s,a)=Q^π(s,a)−V^π(s). These are the unnormalized value conventions of §3, pp. 9–12.

For each state-action pair, fix a feature vector φ(s,a) in Euclidean d-space. The log-linear policy with parameter θ assigns probability proportional to exp(θ·φ(s,a)):

\pi_\theta(a\mid s)= \frac{\exp(\theta\cdot\phi(s,a))} {\sum_{a'\in A}\exp(\theta\cdot\phi(s,a'))}.

The Q-NPG fitting loss $L(w;\theta,\upsilon)$ is the mean squared error of predicting $Q^{\pi_\theta}(s,a)$ by $w\cdot\phi(s,a)$ under a state-action distribution $\upsilon$ . Q-NPG uses an approximate minimizer w of this loss under its current on-policy measure and updates θ by ηw. The distribution ν specifies the initial state-action pair for that measure. At time zero, the pair is drawn directly from ν; the given initial action is executed before later actions follow the current policy. These definitions are (19)–(20) of §6.2, pp. 27–28.

The comparison policy π⋆ has discounted state visitation distribution $d^{\pi^\star}_\rho$ . The paper's transfer measure $d^\star$ pairs those states with a uniform action from A. The excess risk measures how much worse an approximate fitting direction is than an exact constrained minimizer under the current on-policy measure. The transfer error measures the exact minimizer's loss under $d^\star$ . A relative condition number κ bounds, in every feature direction, the covariance quadratic form under $d^\star$ by κ times that under ν (Assumptions 6.1–6.2, pp. 28–29).

Formalization targets

Agnostic Q-NPG guarantee

The goal is Theorem 6.1, p. 29. Starting with θ⁽⁰⁾=0, taking T positive updates with step size $\eta=\sqrt{2\log|A|/(B^2W^2T)}$ , bounding feature norms by B and update norms by W, and assuming the expected excess and transfer errors are at most $\varepsilon_{\rm stat}$ and $\varepsilon_{\rm bias}$ , respectively, it asserts

\mathbb E\!\left[ \min_{t<T}\{V^{\pi^\star}(\rho)-V^{\pi_{\theta^{(t)}}}(\rho)\} \right] \le \frac{BW}{1-\gamma}\sqrt{\frac{2\log|A|}{T}} + \sqrt{\frac{4|A|\kappa\varepsilon_{\rm stat}}{(1-\gamma)^3}} + \frac{\sqrt{4|A|\varepsilon_{\rm bias}}}{1-\gamma}.

The expectation encloses the minimum: each random run may have a different best iterate. The claim gives a finite-horizon comparison with π⋆ even when π⋆ is not globally optimal.

Supporting targets

The milestones are the paper's performance-difference identity (Lemma 3.2), smoothness of bounded-feature log-linear policies (Remark 6.7), the deterministic NPG regret lemma (Lemma 6.2), and the two displayed bounds that control transfer and estimation terms ((25) and (26)). Together they connect the MDP's value comparison with the two statistical errors in the goal. Each milestone states a source result rather than a weakened surrogate.

Significance

The theorem separates three quantities that can vary independently in an application: the number of iterations, the statistical quality of the update direction, and the mismatch between the comparator's visited states and the fitting distribution. If both errors vanish, the displayed bound decreases with T at a square-root rate. With imperfect features, the transfer term shows the remaining performance limit. With finite-sample fitting, the excess-risk term shows how estimation quality affects the policy value. This is an agnostic statement because the comparator need not belong to a globally complete policy class (Agarwal et al., Theorem 6.1 and discussion, pp. 29–30).

The paper proves these claims mathematically. This mission asks for machine-checked proofs of the same statements in Lean, including the probabilistic expectation and the exact constants. The reusable parts are the state-action visitation distribution with a prescribed initial action, the log-linear policy and its smoothness property, the least-squares loss, and the deterministic regret lemma. Those objects can support other policy-gradient analyses with different fitting guarantees.

Difficulty

The update direction minimizes a loss under the distribution generated by the current policy, while the value comparison uses states visited by a different policy. The two distributions need not agree, and prediction error under one cannot simply be substituted for error under the other. The relative condition number controls the feature geometry of this shift, while the transfer error separately measures how well an exact on-policy fit predicts under the comparator's measure. Random approximate minimizers add a further layer: the bound concerns the expectation of the best iterate in each run, rather than a deterministic iterate chosen in advance. These are the obstacles identified around Assumptions 6.1–6.2 and the proof of Theorem 6.1.

Formalization scope

The Lean development uses finite state and action types, as in the paper's §3 standing setting. It imports published definitions of transition kernels, policies, occupation probabilities, value and Q-functions, and defines this paper's advantage, discounted visitation, log-linear class and fitting loss on top of them. Parameters and features lie in EuclideanSpace ℝ (Fin d), so the norm is the Euclidean norm used by the paper. A general probability space carries the random update directions and exact constrained minimizers; their measurability and boundedness make the displayed loss expectations integrable.

The action type is nonempty so that the uniform action distribution exists. B and W are positive and T is positive, because the prescribed step size divides by $B^2W^2T$ and the result minimizes over $t<T$ . The comparator is assumed to be a policy, with no optimality hypothesis. The nonnegative condition number is represented by its quadratic-form upper-bound property for every direction. This avoids undefined real ratios when a covariance form vanishes and includes the finite coefficient in Assumption 6.2. The value and loss expressions are calculated from P, r, π and φ; they are not free variables. The Q-NPG parameter sequence is defined by the update rule from θ⁽⁰⁾=0. In particular, the goal does not assume the regret lemma or either of the two statistical inequalities that the proof must establish.

The paper notes that some §6 results extend beyond finite state or action spaces. This mission fixes the finite case inherited from §3. Contributions that prove the source milestones, establish the required summability and integrability facts, or generalize the development to larger measurable spaces are useful; a generalization must keep the same statistical and comparator conventions.

Selected references

Alekh Agarwal, Sham M. Kakade, Jason D. Lee and Gaurav Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. arXiv:1908.00261v5
Sham M. Kakade and John Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning, 2002. PDF

16 thms3 active usersReviewed

Completed

Machine Learning Optimization Reinforcement Learning·Captain: mikedeng1

On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift 2: On a Chain MDP All Low-Order Derivatives of the Value Are Exponentially Small at Suboptimal PoliciesResearch Paper

Motivation

Policy gradient methods adjust a policy by following derivatives of its expected reward. A common expectation is that a small gradient indicates a policy close to optimal. For discounted Markov decision processes, that interpretation can fail when a policy rarely reaches the states where reward is available. Agarwal, Kakade, Lee, and Mahajan study this obstruction as part of their analysis of optimality and distribution shift in policy gradient methods. Their chain example makes the obstruction quantitative: even derivatives of several orders can be exponentially small while the value gap grows with the chain length. Agarwal et al., §4.3 and Proposition 4.1.

The example isolates a specific issue for local optimization. A parameter change at an early state affects reward only after the agent has passed through many intermediate decisions. A local derivative therefore measures the behavior of a policy under its own visitation pattern, which can be very different from the visitation pattern of an optimal policy. This mission states the resulting separation with explicit constants rather than treating “vanishing gradients” as a qualitative description.

Setting

A discounted Markov decision process has a finite set of states, a finite set of actions, a transition probability for each state and action, a reward in $[0,1]$ , and a discount $0\le\gamma<1$ . The value $V^\pi(s)$ of a policy $\pi$ is the expected sum of discounted rewards when the process starts in state $s$ and follows $\pi$ . An optimal policy $\pi^\star$ has value at least as large as every other policy at every state. These conventions are those of §3 of the paper and its unnormalized infinite-horizon value definition. Agarwal et al., §3, pp. 9–12.

The central model is a deterministic chain with states $s_0,s_1,\ldots,s_{H+1}$ and four actions. At $s_0$ the process moves to $s_1$ . At each interior state $s_i$ , action $a_1$ moves forward to $s_{i+1}$ , while $a_2,a_3,a_4$ move backward to $s_{i-1}$ . State $s_{H+1}$ is absorbing. The only positive reward is $r(s_{H+1},a_1)=1$ , and $\gamma=H/(H+1)$ . This is Figure 2 and the transition matrix in equation (27). Agarwal et al., Figure 2, p. 11, and (27), p. 50.

The direct policy parameter $\theta$ has three free coordinates at each interior state: the probabilities assigned to $a_1,a_2,a_3$ . The probability of $a_4$ is their complement. Write $\pi_\theta$ for this policy expression and $F_H(\theta)=V^{\pi_\theta}(s_0)$ for its value from the starting state. The paper studies parameters whose free coordinates lie strictly between zero and one and whose forward-action coordinates satisfy $\theta_{i,a_1}<1/4$ .

Formalization targets

The goal is Proposition 4.1. For $H\ge1$ , every such $\theta$ , and every nonnegative integer $k$ satisfying $k\le H/(40\log(2H))-1$ , it asserts the multilinear operator-norm bound

\|\nabla^k F_H(\theta)\|_{\mathrm{op}}\le (1/3)^{H/4}.

The same statement compares this policy with an optimal policy:

V^{\pi^\star}(s_0)-F_H(\theta) \ge \frac{H+1}{8}-\frac{(H+1)^2}{3^H}.

Both clauses and their constants are part of the target. The derivative order includes $k=0$ whenever the displayed threshold admits it. Agarwal et al., Proposition 4.1, p. 16.

Three supporting targets follow the appendix's attack path. First, $F_H(\theta)$ equals the $(0,H+1)$ entry of the resolvent $M^p=(I-\gamma P^p)^{-1}$ , where $p_i=\theta_{i,a_1}$ . Second, equation (32) gives the derivative of any entry of $M^p$ in one forward probability. Third, the appendix separately bounds the optimal value below by $(H+1)/8$ and $F_H(\theta)$ above by $(H+1)^2/3^H$ . A companion theorem records Lemma 3.1: a five-state deterministic example has a value function that is nonconcave in both the direct and softmax parameterizations. Agarwal et al., Appendix B.2, pp. 51, 54, 59; Lemma 3.1, p. 11.

Significance

The proposition supplies an explicit family in which local derivative information, even at orders growing with $H/\log H$ , is small at policies with a large value gap. It limits what a guarantee based only on finding a point with small low-order derivatives can imply about global policy quality. The paper uses this example to motivate attention to state visitation and distribution mismatch in its positive results. Agarwal et al., §4.3, pp. 16–17.

The mathematical result is proved in the cited paper. The remaining work is a machine-checked development of the chain model, its value and resolvent identities, the higher derivative estimates, and the value-gap inequality. The reusable parts include finite-state discounted value calculations, differentiation of a matrix inverse, and operator-norm estimates for multilinear derivatives. The statements in this proposal are proof targets; they do not themselves claim that those proofs have been formalized.

Difficulty

A policy can have a small gradient simply because it almost never reaches the rewarding state. The obvious inference from a near-zero gradient to near-optimal value therefore fails in this model. The technical difficulty is quantitative: each differentiation of a resolvent entry produces terms involving several entries, and the operator norm combines all mixed partial derivatives. The bound must remain exponentially small after that combination, uniformly over every derivative order allowed by the threshold. The second clause must simultaneously show that a policy taking the forward action reaches the reward often enough to create a large value gap. Agarwal et al., Appendix B.2, pp. 54–59.

Formalization scope

States are Fin (H + 2) and actions are Fin 4; the parameter space is EuclideanSpace ℝ (Fin H × Fin 3). Its norm is the Euclidean norm, so the norm of the iterated Fréchet derivative is the paper's multilinear operator norm. The first and last states have no free policy parameters. All four actions at $s_0$ induce the same transition to $s_1$ , and the parameterized policy chooses $a_1$ at both boundary states. The resolvent is the matrix inverse of $I-\gamma P^p$ ; its milestone statements are restricted to interior probabilities $0<p_i<1$ , where that inverse is nonsingular.

The displayed coordinate assumptions of Proposition 4.1 do not require the three free probabilities at a state to sum to at most one. The Lean goal retains exactly those assumptions. Its value expression is still determined by the forward probabilities, because every other action has the same backward transition and only the absorbing state yields reward. This prevents an added simplex constraint from silently narrowing the proposition. A constant function or a free value variable cannot replace the chain value: $F_H$ is computed from the concrete transition and reward arrays.

The development uses the published finite-state transition-kernel, policy, occupation, value, and optimal-policy definitions. Contributions needed for a proof include stochasticity of the chain, geometric-series evaluation of its absorbing reward, nonsingularity and differentiation of its resolvent, and estimates that pass from mixed partial derivatives to the Euclidean operator norm. For the companion example, direct parameters lie in the product of action simplices, with positive discount; at zero discount its value is constant and the nonconcavity claim would be false.

Selected references

Alekh Agarwal, Sham M. Kakade, Jason D. Lee, Gaurav Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. arXiv:1908.00261v5.

12 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Optimality and Duality Theory for Stochastic Optimization Problems with Nonlinear Dominance Constraints 3: The Dual Functional of a Dominance Constraint Is Minus an Expected Concave ConjugateResearch Paper

Dual decomposition of dominance constraints

A stochastic dominance constraint asks a random outcome $X$ of a decision to be at least as good as a benchmark outcome $Y$ for every risk-averse decision maker: in the second-order version, $\mathbb E[u(X)] \ge \mathbb E[u(Y)]$ for every concave nondecreasing utility $u$ . Dentcheva and Ruszczyński introduced optimization problems with such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim. 2003), where the outcome itself is the decision variable, and extended the theory in the paper this mission formalizes, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program. 2004, DOI 10.1007/s10107-003-0453-z), to outcomes $X_i = G_i(z)$ that depend nonlinearly on a decision $z$ .

The paper's §4 builds a Lagrangian dual of these problems. The multipliers of the $i$ -th dominance constraint are a utility function $u_i$ and an almost-sure multiplier $\theta_i$ for the coupling $X_i = G_i(z)$ . The dual functional splits into a part $D_0$ that involves only the decision $z$ and one part $D_i$ per dominance constraint. This mission is about the second kind of part: Theorem 4 computes $D_i$ in closed form as a concave conjugate, and Theorem 5 gives its subgradients. Those two facts are what make the dual problem amenable to nonsmooth optimization and decomposition methods, which is the purpose the paper states for them.

The underlying shortfall function $F_2(X;\eta)=\int_{-\infty}^{\eta}P[X\le\alpha]\,d\alpha$ and its dual characterization are due to Ogryczak and Ruszczyński (Dual stochastic dominance and related mean–risk models, SIAM J. Optim. 2002). The pure-dominance case of the optimality theory is the 2003 paper above.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space, $\mathcal L_1$ the integrable and $\mathcal L_\infty$ the essentially bounded random variables. Fix a bounded interval $[a,b]$ ( $a\le b$ ) and a reference outcome $Y\in\mathcal L_1$ .

The utility class $\mathcal U_1([a,b])$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave and nondecreasing, vanish on $[b,\infty)$ , and are affine on $(-\infty,a]$ : $u(t)=u(a)+c(t-a)$ for $t\le a$ , with a constant $c\ge 0$ . For such $u$ , the left derivative $u'_-(a)$ at $a$ is that slope $c$ .

The concave conjugate of $v:\mathbb R\to\mathbb R$ is

v^*(\xi)=\inf_{t\in\mathbb R}\,[\xi t-v(t)]\in[-\infty,+\infty).

For a random variable $\zeta$ , $v^*(\zeta)$ is the extended-real random variable $\omega\mapsto v^*(\zeta(\omega))$ .

The dual functional of one dominance constraint, eq. (34), is

D(w,\zeta)=\sup_{X\in\mathcal L_1}\mathbb E\big[w(X)-w(Y)-\zeta X\big]\in\overline{\mathbb R},\qquad w\in\mathcal U_1([a,b]),\ \zeta\in\mathcal L_\infty .

The functional of eq. (35) is $f(v,\zeta)=-\mathbb E\,v^*(\zeta)$ , considered on $\mathrm{Lip}(\mathbb R)\times\mathcal L_1$ , where $\mathrm{Lip}(\mathbb R)$ is the space of Lipschitz functions with norm $\|v\|_{\mathrm{Lip}}=|v(0)|+\sup_{t\ne s}|v(t)-v(s)|/|t-s|$ .

Formalization targets

Goal: Theorem 4

For every $v\in\mathcal U_1([a,b])$ and every $\zeta\in\mathcal L_\infty$ ,

D(v,\zeta)=-\mathbb E\big[v^*(\zeta)+v(Y)\big].

The formal statement has two cases. If $0\le\zeta\le v'_-(a)$ almost surely, then $v^*(\zeta)$ is a.s. finite and integrable and the identity holds between real numbers. Otherwise $D(v,\zeta)=+\infty$ .

Milestones

Unbounded cases (proof of Theorem 4, p. 13): $P[\zeta<0]>0 \Rightarrow D(v,\zeta)=+\infty$ ; and $P[\zeta>v'_-(a)]>0 \Rightarrow D(v,\zeta)=+\infty$ .
Pointwise maximizer (p. 13): for $0\le\xi\le v'_-(a)$ , the function $t\mapsto v(t)-\xi t$ attains its maximum at some $t_0\in[a,b]$ , so $v^*(\xi)=\xi t_0-v(t_0)$ is finite.
Measurable selection (p. 13): if $0\le\zeta\le v'_-(a)$ a.s., there is a measurable $X\in[a,b]$ a.s. with $X(\omega)\in\operatorname{argmax}_t[v(t)-\zeta(\omega)t]$ a.s.
Effective domain (p. 13): $D(v,\zeta)<+\infty \iff 0\le\zeta\le v'_-(a)$ a.s.
Theorem 5 (p. 14): for $\bar v\in\mathcal U_1([a,b])$ , $\bar\zeta\in\mathcal L_1$ with $0\le\bar\zeta\le\bar v'_-(a)$ a.s., and a measurable maximizer selection $X$ with values in $[a,b]$ , the pair $(P_X,-X)$ is a subgradient of $f$ at $(\bar v,\bar\zeta)$ :

f(v,\zeta)\ge f(\bar v,\bar\zeta)+\int\big(v-\bar v\big)\,dP_X-\mathbb E\big[X(\zeta-\bar\zeta)\big]\quad\text{for all }(v,\zeta)\in\mathrm{Lip}(\mathbb R)\times\mathcal L_1.

Significance

Theorem 4 reduces an optimization over the infinite-dimensional space $\mathcal L_1$ to one scalar maximization per scenario: the dual functional is an expected conjugate. It identifies the effective domain of the dual in the multiplier $\zeta$ (bounded between $0$ and the slope of the utility at the left end of the interval), and it makes evaluating $D$ as cheap as evaluating $v^*$ . Theorem 5 supplies explicit subgradients, the law of a maximizer and the maximizer itself, which is what bundle and cutting-plane methods for the dual problem (31) consume. The paper's §5–§6 build their finite-scenario theory and numerical method on this decomposition.

Both theorems are proved in the paper. Neither has a machine-checked proof; no concave conjugate on $\mathbb R$ with values in $[-\infty,+\infty)$ , no dual functional of this kind, and no measurable-selection theorem for argmax correspondences of this shape exist on the platform. A complete formalization would provide reusable infrastructure: an extended-real concave conjugate, interchange of supremum and expectation for a scalar integrand with a bounded maximizer, and a concrete measurable-selection argument.

Difficulty

The hard step is the interchange $\sup_{X\in\mathcal L_1}\mathbb E[\,\cdot\,]=\mathbb E\sup_t[\,\cdot\,]$ . The inequality " $\le$ " is pointwise, but " $\ge$ " needs a random variable that attains the pointwise maximum, is measurable, and is integrable. The paper cites Rockafellar–Wets for both the interchange and the selection. The maximizers are not unique: where $\zeta(\omega)=0$ or $\zeta(\omega)=v'_-(a)$ the argmax is an unbounded half-line, so an arbitrary measurable selection need not be integrable, and the bounded one must be constructed. The unbounded cases need care because $\zeta$ is only essentially bounded and the test outcomes $M\mathbb 1_{\{\zeta<0\}}$ must be shown integrable.

Formalization scope

This chunk's objects are in NonlinSSD.DualFunctional; it imports the already moderated utility class NonlinSSD.Optimality.U1. Random variables are functions $\Omega\to\mathbb R$ on a probability space with IsProbabilityMeasure P; $\mathcal L_1$ is Integrable, $\mathcal L_\infty$ is MemLp ζ ⊤ P. The conventions and explicit readings:

$c\ge 0$ in $\mathcal U_1([a,b])$ . The paper prints $c>0$ . The page calls $\mathcal U_1([a,b])$ a convex cone, which must contain $0$ , and the companion optimality theorem fails with $c>0$ ; the formalization uses $c\ge0$ .
Left derivative $v'_-(a)$ is derivWithin v (Set.Iic a) a, never deriv v a, which is $0$ at a kink.
Extended values. $v^*$ , $D$ and $f$ are EReal-valued, so an infimum equal to $-\infty$ and a supremum equal to $+\infty$ are represented, not replaced by $0$ . The supremum in $D$ is over integrable $X$ only.
Theorem 4 in two cases. The paper's right side is an expectation of an extended-real random variable, read as $+\infty$ off the domain. The statement separates the finite case (Bochner integral of the real part, with a.s. finiteness and integrability asserted) from the infinite case, which avoids extended-real subtraction.
$f$ equals the Bochner integral of $-v^*(\zeta)$ when $v^*(\zeta)$ is a.s. finite with integrable real part, and $+\infty$ otherwise. This is exact because $-v^*(\zeta)\ge v(0)$ .
Theorem 5 adds the hypothesis that the selection lies in $[a,b]$ a.s. As printed ("for every measurable selection") it is false: with $a=-1$ , $b=0$ , $\bar v(t)=\min(t,0)$ , $\bar\zeta=0$ on $[0,1]$ with Lebesgue measure, the selection $X(\omega)=1/\omega$ is not integrable. The continuity of $(P_X,-X)$ as a functional is stated as $X\in\mathcal L_\infty$ and the bound $\int|v|\,dP_X\le(|v(0)|+K)(1+\mathbb E|X|)$ for $K$ -Lipschitz $v$ .
The paper's index $i$ and the standing data of §4 ( $Y\in\mathcal L_1$ , $a\le b$ ) are explicit binders.

A trivializing formalization is ruled out: a real-valued conjugate or dual functional (junk $0$ at $\mp\infty$ ), a supremum over all measurable $X$ (junk integrals), or a one-sided case split would each make the goal easier than the paper's theorem, and a sorry-free check confirms that both cases of Theorem 4 are inhabited ( $v=\min(t,0)$ , $\zeta=1/2$ and $\zeta=2$ ).

Contributions are welcome at every level: proofs of the milestones in order, general lemmas on extended-real conjugates on $\mathbb R$ , and a measurable argmax selection for continuous integrands over a compact interval, which is reusable well beyond this paper.

Selected references

D. Dentcheva, A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Math. Program. 99 (2004). Author manuscript, rev. April 2003. https://doi.org/10.1007/s10107-003-0453-z
D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14 (2003). https://doi.org/10.1137/S1052623402420528
W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean–risk models, SIAM J. Optim. 13 (2002). https://doi.org/10.1137/S1052623400375075
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998 (Theorems 14.37, 14.60). https://doi.org/10.1007/978-3-642-02431-3

9 thms3 active usersReviewed

Completed

Combinatorics Linear Optimization Operations Research+1·Captain: mikedeng1

Online Primal-Dual Algorithms for Covering and Packing 3: A Deterministic O(log d log(n/OPT))-Competitive Algorithm for Online Unweighted Set CoverResearch Paper

Motivation

Online set cover is the basic covering problem in which the requests arrive over time. A ground set of elements and a family of sets are known in advance, but which elements must be covered is revealed one element at a time, and each arriving element has to be covered at once by a set chosen irrevocably. The problem models resource placement under unknown demand (facilities, servers, sensors that must serve clients as they appear) and is the prototype for a family of online covering problems.

Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 2009) gave the first deterministic algorithm, with competitive ratio $O(\log m\log n)$ for $n$ elements and $m$ sets, and showed that no deterministic algorithm does better than $\Omega(\log m\log n/(\log\log m+\log\log n))$ on some instances. Buchbinder and Naor (Math. Oper. Res. 2009) recast the fractional part of that algorithm as an instance of a general online primal-dual scheme for covering and packing linear programs, and turned an offline pessimistic estimator of Srinivasan into an online potential function. The result, in their Section 5.1, is a deterministic algorithm whose ratio $O(\log d\log(n/OPT))$ depends on the maximum element frequency $d$ instead of the number of sets $m$ , and on the ratio $n/OPT$ instead of $n$ .

Timeline:

2003 (conference), 2009 (journal): Alon et al., deterministic $O(\log m\log n)$ for unweighted online set cover, with a potential $\sum_{j\notin C} n^{2w_j}$ .
2005 (conference), 2009 (journal): Buchbinder and Naor, the general online fractional covering/packing scheme, and the derandomized rounding of this mission.

Setting

A set-cover instance consists of a finite ground set $X$ of $n$ elements and a finite family $\mathcal S$ of $m$ sets. For an element $e$ , $\mathcal S_e$ is the collection of sets containing $e$ , and $d$ bounds its size: $|\mathcal S_e|\le d$ for every $e$ (the frequency). In the unweighted problem every set costs $1$ .

Elements arrive in a list $\sigma$ . The algorithm maintains:

fractional weights $w(s)\ge 0$ for the sets, produced by the paper's Section 3 scheme with $\{0,1\}$ coefficients: when an element $e$ arrives that is not yet fractionally covered ( $\sum_{s\in\mathcal S_e}w(s)<1$ ), its dual variable $y(e)$ is raised to the least value at which

w(s)=\max\Big\{w(s),\ \tfrac1d\Big(\exp\Big(\tfrac{B}{2c(s)}\textstyle\sum_{k:\ s\ni e_k}y(e_k)\Big)-1\Big)\Big\}\qquad(s\ni e)

gives $\sum_{s\in\mathcal S_e}w(s)\ge 1$ ; here $B>0$ is a parameter;

a cover $\mathcal C\subseteq\mathcal S$ that only grows; $C$ is the set of elements covered by $\mathcal C$ .

With $f(e)=\min\{1,\exp(-\alpha+\alpha\sum_{s\ni e}w(s))\}$ , the potential is $\Phi=\Phi_1+\Phi_2$ with

\Phi_1=1-\prod_{e\in X\setminus C}\big(1-f(e)\big),\qquad \Phi_2=\exp\Big(\sum_{s\in\mathcal S}\big((\ln 2)\chi_{\mathcal C}(s)-\alpha w(s)\big)-OPT\Big),

where $OPT$ is the optimum number of sets covering the arrived elements, assumed known, $r=e\ln(e/(e-1))$ and $\alpha=\max\{1,\ln(rn/OPT)\}$ . The rounding rule: each time the weight of a set $s$ is augmented, $s$ is added to $\mathcal C$ if this does not increase $\Phi$ .

Formalization targets

Goal: Lemma 5.2

Every arriving element is covered by $\mathcal C$ , and at every time

|\mathcal C|\ \le\ \frac{\big(2\alpha\ln(1+d)+1\big)\,OPT}{\ln 2},\qquad \alpha=\max\Big\{1,\ln\frac{rn}{OPT}\Big\}.

This is the paper's $OPT\cdot O(\log d\log(n/OPT))$ with the constant its proof gives.

Milestones

Theorem 3.2 (covering half): for every $B>0$ , the $\{0,1\}$ scheme with frequency bound $\ell$ yields a fractional cover of cost at most $2\ln(1+\ell)$ times that of any fractional cover.
Lemma 5.1 (i): initially $\Phi\le 1$ ; $\Phi>0$ in every state.
Lemma 5.1 (ii): after the weight of a set is augmented by $\delta\ge0$ , taking the set or excluding it leaves $\Phi$ no larger than before.

Significance

The bound improves Alon et al.'s $O(\log m\log n)$ whenever sets are many but each element lies in few of them ( $d\ll m$ ), and whenever the optimum is large compared with $n$ . It also shows that the fractional part and the rounding part of an online covering algorithm can be designed separately: any online fractional solution with a competitive guarantee can be rounded deterministically by an online potential function. The same method gives the routing result of Section 5.2 of the paper.

As far as is known, none of these results is machine-checked. Related formal work on the platform covers Alon et al.'s algorithm and its $O(\log m\log n)$ bound (a different potential and a different fractional update), and the general covering scheme of Buchbinder and Naor's monograph; neither states Lemma 5.1 or Lemma 5.2, nor Theorem 3.2 for the $\{0,1\}$ scheme with $\ell$ in place of $n$ . A complete development here would give a verified derandomized rounding argument, reusable for other online covering problems.

Difficulty

The difficulty is not in the final inequality, which follows from $\Phi_2\le1$ in one line, but in keeping $\Phi\le1$ throughout. The decision to take a set must be made with no knowledge of future elements, and the potential has to account for elements that may never arrive: $\Phi_1$ ranges over the whole ground set. Lemma 5.1 (ii) asks that, for every current state, one of the two decisions does not increase a non-linear function of all uncovered elements at once and this must hold for every state, not only for the states a particular run reaches. On the fractional side, Theorem 3.2 is only asserted, "along the same lines" as Theorem 3.1, so its constant has to be re-derived with $\ell$ in place of $n$ and with the scheme's continuous increase made discrete.

A tempting shortcut is to bound $|\mathcal C|$ by the number of rounds or by $\sum_s w(s)$ directly; neither gives a logarithmic factor in $n/OPT$ , which comes only from the choice of $\alpha$ in $\Phi$ .

Formalization scope

The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (elements E, set indices T, incidence elemSets, positive costs c), with elementWeight and coveredBy. Unit costs are the hypothesis ∀ s, inst.c s = 1 in Lemma 5.2; Theorem 3.2 is stated for general positive costs. Logarithms are natural (Real.log), because they invert Real.exp.

Committed conventions:

The fractional scheme is the discrete form of the continuous increase: in each round $y(e)$ is the least $t\ge0$ (an sInf) at which the new constraint holds. Arrival lists may repeat elements; an element already covered changes nothing.
The rounding treats each set's increase within a round as one augmentation; the augmented sets are processed one at a time in the order of a list ord containing every set, and a set is added when $\Phi(w+\delta_s\mathbf 1_s,\mathcal C\cup\{s\})\le\Phi(w,\mathcal C)$ . Lemma 5.2 holds for every order.
The algorithm is a function, so every run exists.
$OPT$ is a natural number $\ge1$ bounding the size of some cover of the arrived elements; $d\ge1$ bounds the frequency of every element. At the true optimum and the maximum frequency this is the paper's statement.
Explicit constants replacing $O(\cdot)$ : Theorem 3.2's $O(\log\ell)$ is $2\ln(1+\ell)$ ; Lemma 5.2's $OPT\cdot O(\log d\log(n/OPT))$ is $(2\alpha\ln(1+d)+1)\,OPT/\ln2$ with $\alpha=\max\{1,\ln(rn/OPT)\}$ .
The proof of Lemma 5.1 (i) on p. 13 prints $d$ where $r$ is meant (" $\exp(-dne^{-\alpha})$ ", " $\alpha\ge\ln(dn/OPT)$ "); the statement uses $r$ , and $r$ is printed " $e\ln(e/e-1)$ " for $e\ln(e/(e-1))$ .

Not in scope: the packing half of Theorem 3.2, Theorem 3.1 for general coefficients, and the doubling wrapper of p. 12 that removes the assumption that $OPT$ is known. The guarantee is for the algorithm run with the stated $\alpha$ ; a formalization in which $\Phi$ 's product ranges only over arrived elements, or in which the weights or the chosen family are free variables constrained by hypotheses instead of being produced by the algorithm ( $OPT$ is an input of the algorithm, as the page assumes it known), would be a different and weaker statement and is ruled out.

Contributions welcome: proofs of the three milestones and of the goal, and general lemmas about the fractional round (attainment of the least $t$ , monotonicity of the weights) that other online covering missions can reuse.

Selected references

N. Buchbinder, J. Naor, Online Primal-Dual Algorithms for Covering and Packing, Mathematics of Operations Research 34(2), 2009. https://doi.org/10.1287/moor.1080.0363
N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM Journal on Computing 39(2), 2009. https://doi.org/10.1137/060661946
A. Srinivasan, Improved approximation guarantees for packing and covering integer programs, SIAM Journal on Computing 29(2), 1999. https://doi.org/10.1137/S0097539796314240
N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024

10 thms3 active usersReviewed

Completed

Linear algebra Machine Learning Optimization·Captain: mikedeng1

Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers VII: Factor Model Fitting — the ADMM X-Update in Closed Form, Entry by EntryTextbook

Motivation

Alternating direction methods are used when one part of an optimization problem is easy to minimize and another part has a simple projection. Chapter 9 of Boyd, Parikh, Chu, Peleato and Eckstein (2011) examines this idea with nonconvex constraints. Its examples include sparse vectors, Boolean vectors and low-rank matrices. The chapter says explicitly that ADMM can fail to converge in this setting and that a limit need not be globally optimal. The useful claim here is narrower and concrete: several individual updates can still be computed exactly.

The capstone is factor-model fitting. A symmetric data matrix, such as an empirical covariance matrix, is approximated by a positive semidefinite matrix of prescribed rank plus a nonnegative diagonal matrix. This decomposition gives one component that captures shared variation and another that represents coordinate-specific variation. The chapter separates the diagonal fit from the rank constraint and writes the resulting ADMM X-update entry by entry. This mission formalizes that exact update and two other projection rules stated in the same chapter.

Setting

Fix a positive integer $n$ . Write $\mathbb S^n$ for the real symmetric $n\times n$ matrices, and let $\Sigma\in\mathbb S^n$ be the matrix to approximate. The Frobenius norm squares and sums every ordered matrix entry: $\|X\|_F^2=\sum_{i,j}X_{ij}^2$ . A vector $d\in\mathbb R^n$ is nonnegative when $d_i\ge0$ for every $i$ , and $\operatorname{diag}(d)$ places those entries on a diagonal matrix. The book's reduced fitting loss is

f_\Sigma(X)=\inf_{d\ge0}\frac12\|X+\operatorname{diag}(d)-\Sigma\|_F^2.

In the scaled ADMM iteration, $Z$ carries the positive semidefinite rank constraint and $U$ is the scaled dual matrix. Given the current symmetric matrices $Z,U$ and a penalty $\rho>0$ , the X-step minimizes $f_\Sigma(X)+(\rho/2)\|X-Z+U\|_F^2$ over $X\in\mathbb S^n$ . The X-step itself has no rank or positive semidefinite restriction. The following Z-step projects onto the chosen rank-constrained positive semidefinite set. The theorem here concerns the X-step, whose definition is independent of the chosen rank.

The other two results concern Euclidean projection of vectors $v\in\mathbb R^n$ . The cardinality $\operatorname{card}(x)$ is the number of nonzero coordinates of $x$ . The sparse set is $\{x:\operatorname{card}(x)\le c\}$ for a nonnegative integer $c$ . The Boolean cube is $\{0,1\}^n$ . Projection means a nearest point in squared Euclidean distance; it may have more than one value when coordinates tie.

Formalization targets

Partial minimization of the diagonal

The first milestone identifies the book's infimum as the explicit componentwise loss and states that the optimizing diagonal is attained:

f_\Sigma(X)=\frac12\sum_{i\ne j}(X_{ij}-\Sigma_{ij})^2+ \frac12\sum_i(X_{ii}-\Sigma_{ii})_+^2, \qquad d_i=(\Sigma_{ii}-X_{ii})_+.

The sum over $i\ne j$ counts both $(i,j)$ and $(j,i)$ . The statement preserves that convention instead of treating a symmetric matrix as a list of independent upper-triangular entries.

Exact projections for two nonconvex sets

The page 74 milestones say that retaining the $\min(c,n)$ entries of largest absolute value gives a nearest point in $\{x:\operatorname{card}(x)\le c\}$ , and that rounding every coordinate to a nearest element of $\{0,1\}$ gives a nearest Boolean vector. They assert nearest-point status for ties without asserting uniqueness. These are chapter results on the same theme of exact nonconvex updates, although they are independent of the factor-model goal.

Factor-model X-update

The goal identifies the unique symmetric minimizer $X^+$ of the X-subproblem. With $a_{ij}=Z_{ij}-U_{ij}$ , its off-diagonal and diagonal entries are

X^+_{ij}=\frac{\Sigma_{ij}+\rho a_{ij}}{1+\rho}\quad(i\ne j),\qquad X^+_{ii}=\begin{cases} \dfrac{\Sigma_{ii}+\rho a_{ii}}{1+\rho},&\Sigma_{ii}\le a_{ii},\\ a_{ii},&\Sigma_{ii}>a_{ii}. \end{cases}

The target asserts both the formula and global minimality over symmetric matrices. It does not replace minimality with a stationarity condition.

Significance

The exact X-update separates the matrix fit from the nonconvex rank projection. It establishes that the factor-model algorithm's X-step is a well-defined, single-valued minimization for every symmetric current state and every positive penalty. It also makes the one-sided diagonal loss explicit: a nonnegative diagonal can absorb a shortfall below $\Sigma_{ii}$ , but cannot absorb an excess. The two vector projections give similarly exact updates for sparse and Boolean constraint sets.

The mathematical claims are given in §9.1–9.1.2 of the published monograph; they are not open conjectures. The formalization work is to check the infimum, projection and unique-minimizer statements with every domain and tie convention explicit. The mission poses theorem statements for proofs; these draft statements themselves do not yet supply machine-checked proofs. A complete development can reuse its finite matrix loss and finite vector projection vocabulary in other splitting algorithms.

Difficulty

The diagonal partial minimization is one-sided, while the proximal penalty is symmetric around $Z-U$ . An entrywise formula alone does not show that the assembled matrix minimizes the full objective or that it is the only minimizer. Symmetry also couples the two displayed off-diagonal positions $(i,j)$ and $(j,i)$ , so a scalar statement on one entry must agree with its transpose. For sparse projection, ties at the cutoff make a rule phrased as “the projection” ambiguous. For Boolean projection, the midpoint is a tie and requires a declared convention. These issues are part of the theorem statements, not numerical implementation details.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; symmetry is an entrywise equality predicate. The factor-model statements assume $n\ge1$ , symmetric $\Sigma,Z,U$ , and $\rho>0$ . The book uses $Z^k,U^k$ at an iteration; the Lean theorem uses those current matrices as parameters and does not posit convergence of an ADMM sequence. The reduced loss is literally the infimum over all componentwise nonnegative $d$ , and the Frobenius square is the finite sum of entry squares. The stated X-minimization ranges over all symmetric matrices, with no positive semidefinite or rank hypothesis on $X$ .

For sparse vectors, the index set has size $\min(c,n)$ and its selected magnitudes dominate unselected ones. This covers $c=0$ , $c>n$ and cutoff ties. The Boolean rounding function chooses zero when an entry equals $1/2$ . The book uses indices $1,\ldots,n$ ; Fin n uses $0,\ldots,n-1$ . On page 75 the printed diagonal branch conditions omit the superscript $k$ on $Z$ and $U$ ; the formalization uses the current $Z,U$ that appear in the surrounding ADMM update. The theorem requires the candidate to minimize the book's reduced loss, preventing an arbitrary replacement loss from making the statement trivial.

The development needs finite-sum algebra, real infima with an attained lower bound, symmetry of matrices, and nearest-point arguments for finite vectors. The rank- $c$ singular-value projection on page 74 is already an open target elsewhere and is outside this mission. The positive semidefinite rank- $k$ eigenvalue projection on page 76 is also outside this goal; it would require a separate spectral development. Contributions that prove the three milestones or the goal against these definitions are in scope. The page also mentions rounding under integer constraints; this mission selects the preceding Boolean claim as its projection milestone.

Selected references

Stephen Boyd, Neal Parikh, Eric Chu, Borja Peleato and Jonathan Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011, pp. 73–76, §§9.1–9.1.2. DOI: 10.1561/2200000016.

7 thms3 active usersReviewed

Completed

Combinatorics Operations Research 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 thms3 active usersReviewed

Completed

Machine Learning Operations Research Probability+1·Captain: mikedeng1

From Predictive to Prescriptive Analytics 2: For Costs in [0, c̄] That Are L-Lipschitz, w.p. ≥ 1 − δ Every Decision Rule in F Costs ≤ Its Empirical Cost + c̄√(log(1/δ)/2N) + L·ℜ_N(F)Research Paper

Motivation

Many operations decisions are made after observing side information: an inventory manager sees weather, search trends and calendar effects before ordering; a supply-chain planner sees market signals before shipping. Bertsimas and Kallus, in From Predictive to Prescriptive Analytics (arXiv:1402.5481v4, Management Science 2020), study how to turn such data into decisions. Besides their local, weight-based prescriptions (the subject of mission 1 of this series), their §8 analyses a second approach: choose a decision rule $z(\cdot)$ from a structured class, such as norm-bounded linear rules, by empirical risk minimization — minimizing the average historical cost of the rule.

The question this mission formalizes is the one any practitioner of that approach must answer: how far can the true expected cost of the chosen rule exceed its in-sample cost? Classical statistical learning answers it with Rademacher complexity (Bartlett and Mendelson, JMLR 2002), but only for real-valued predictors. Operations decisions are vectors (order quantities for several products, shipments to several locations), so the paper extends the theory to multivariate decision rules.

Setting

Covariates $x$ take values in a measurable space $\mathcal X$ , the uncertain quantity $y$ in a measurable space $\mathcal Y$ , and decisions $z$ in $\mathbb R^{d}$ , unconstrained. Data are an i.i.d. sample $S_N=((x^1,y^1),\dots,(x^N,y^N))$ from a probability measure $\mu$ on $\mathcal X\times\mathcal Y$ , and $S_N^x=(x^1,\dots,x^N)$ is its covariate part. A cost $c(z;y)$ is incurred when decision $z$ meets outcome $y$ . A decision rule is a measurable map $z(\cdot):\mathcal X\to\mathbb R^d$ ; $\mathcal F$ is a class of decision rules. Its expected cost is $\mathbb E[c(z(X);Y)]$ , and its empirical cost is $\frac1N\sum_{i=1}^N c(z(x^i);y^i)$ , the objective of problem (4).

The empirical multivariate Rademacher complexity of $\mathcal F$ (Definition 3) on a sample $s_1,\dots,s_N$ is

\widehat{\mathfrak R}_N(\mathcal F;S_N)=\mathbb E_\sigma\Big[\frac2N\sup_{g\in\mathcal F}\sum_{i=1}^N\sum_{k=1}^d\sigma_{ik}\,g_k(s_i)\Big],

with $\sigma_{ik}$ independent uniform signs, and the marginal complexity $\mathfrak R_N(\mathcal F)$ is its expectation over the sample. For real-valued classes ( $d=1$ ) these are the usual Rademacher complexities with factor $2/N$ and no absolute value. Lean notation: empRademacher, margRademacher, expCost, empCost, costClass in PrescAnalytics.ERM.

Formalization targets

Goal: Theorem 13 (out-of-sample guarantees)

If $0\le c(z;y)\le\bar c$ and $|c(z;y)-c(z';y)|\le L\|z-z'\|_\infty$ , then for any $\delta>0$ each of the following holds with probability at least $1-\delta$ :

\mathbb E[c(z(X);Y)]\le\frac1N\sum_{i=1}^N c(z(x^i);y^i)+\bar c\sqrt{\frac{\log(1/\delta)}{2N}}+L\,\mathfrak R_N(\mathcal F)\quad\forall z\in\mathcal F,\tag{26}

\mathbb E[c(z(X);Y)]\le\frac1N\sum_{i=1}^N c(z(x^i);y^i)+3\bar c\sqrt{\frac{\log(2/\delta)}{2N}}+L\,\widehat{\mathfrak R}_N(\mathcal F;S_N^x)\quad\forall z\in\mathcal F.\tag{27}

In particular they hold for the empirical risk minimizer. The goal is stated for a general class $\mathcal F$ , not only the linear rules (25).

Milestones

Lemma 1 (comparison): for $\mathcal G=\{(x,y)\mapsto c(f(x);y):f\in\mathcal F\}$ , $\widehat{\mathfrak R}_N(\mathcal G;S_N)\le L\,\widehat{\mathfrak R}_N(\mathcal F;S_N^x)$ and $\mathfrak R_N(\mathcal G)\le L\,\mathfrak R_N(\mathcal F)$ .
Theorem 14 (29): for a class $\mathcal G$ of functions with values in $[0,\bar g]$ , with probability at least $1-\delta$ , $\mathbb E g\le\frac1N\sum_i g(u^i)+\bar g\sqrt{\log(1/\delta)/(2N)}+\mathfrak R_N(\mathcal G)$ for all $g\in\mathcal G$ .
Theorem 14 (30): the data-dependent version with $3\bar g\sqrt{\log(2/\delta)/(2N)}+\widehat{\mathfrak R}_N(\mathcal G;S_N)$ .

Significance

Theorem 13 says that the quantity empirical risk minimization optimizes is, up to confidence terms that do not depend on the rule, an upper bound on the true expected cost of every rule in the class, uniformly. Bound (27) is computable from data, so it certifies a learned policy without a holdout set. Combined with complexity bounds for norm-restricted linear rules (the paper's Lemmas 2 and 3, not part of this mission), it shows the confidence terms vanish as $N\to\infty$ .

The results are known: (29) and (30) for $[0,\bar g]$ -valued classes are the standard Rademacher bounds (Mohri, Rostamizadeh and Talwalkar, Foundations of Machine Learning, Thm 3.3, after rescaling). What is new in the paper is the $\infty$ -norm vector comparison inequality of Lemma 1 with constant $1$ . None of these statements has a machine-checked proof on the platform. A formal development would supply a reusable symmetrization-plus-McDiarmid pipeline and a vector contraction lemma. Related items posed in this repository are Bartlett–Mendelson's Theorem 8 (RadGauss.RiskBound.theorem_8, with an absolute value in the complexity and constant $\sqrt{8\ln(2/\delta)/n}$ ), Maurer's Euclidean vector contraction with constant $\sqrt2$ (SPOBounds.Margin.maurer_vector_contraction), and the open uniform law HighDimStat.UniformLaws.uniform_law_rademacher_complexity; none is the same statement as a target here.

Difficulty

The uniform bound needs three ingredients: a concentration inequality for the supremum of the deviation over the class (bounded differences), a symmetrization step relating the expected supremum to the Rademacher complexity, and a comparison inequality to pass from the cost class to the decision rules. The scalar contraction principle of Ledoux and Talagrand does not apply directly, since each cost depends on a $d$ -dimensional output; applying it coordinatewise loses a factor of $d$ , and Euclidean vector contraction loses $\sqrt2$ and uses the wrong norm. Lemma 1 needs an argument specific to the $\infty$ -norm. Measure theory adds its own difficulty: the supremum over an uncountable class must be shown measurable before its expectation or probability means anything.

Formalization scope

Decisions are Fin d → ℝ, whose Lean norm is the $\infty$ -norm; $\mathcal X$ , $\mathcal Y$ are general measurable spaces. Samples are drawn from the product measure Measure.pi (fun _ : Fin N => μ), with $N\ge1$ . The following readings are explicit:

Each "with probability at least $1-\delta$ , … for all $z\in\mathcal F$ " is a bound $\le\delta$ on the outer measure of the set of samples where the inequality fails for some $z$ ; the quantifier over the class is inside the event.
Empirical complexities are in EReal (an unbounded class gives $+\infty$ ), marginal ones are lower Lebesgue integrals in $[0,\infty]$ ; $0\cdot\infty=0$ .
The paper assumes only $\sup c\le\bar c$ (resp. $|g|\le\bar g$ ). With that alone (26) and (29) are false — a two-point outcome with a constant rule violates them with probability $1/2$ — so the costs are assumed to take values in $[0,\bar c]$ , keeping every printed constant.
The undefined $\delta',\delta''$ are $\delta$ (the i.i.d. case of the paper's Theorem 21); the Lipschitz denominator printed as $\|z_k-z'_k\|_\infty$ is $\|z-z'\|_\infty$ .
Decision rules and the cost are measurable and the class is pointwise separable (a countable subclass approximates every member pointwise). The paper takes probabilities and expectations of suprema over the class without comment; without such a convention the statement fails for pathological classes.

A trivializing formalization is ruled out: the quantifier over the class sits inside the probability, the complexity has no absolute value and is never a junk $0$ for unbounded classes, and the hypotheses are satisfied by a clipped newsvendor cost. Solvers will need McDiarmid's inequality, symmetrization with a ghost sample, and the comparison lemma; each is reusable for any Rademacher-based generalization bound. Formalizations of these tools as separate lemmas are welcome.

Selected references

D. Bertsimas, N. Kallus, From Predictive to Prescriptive Analytics, arXiv:1402.5481v4, 2018; Management Science 66(3), 2020. https://arxiv.org/abs/1402.5481 , https://doi.org/10.1287/mnsc.2018.3253
P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, JMLR 3, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
M. Ledoux, M. Talagrand, Probability in Banach Spaces, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4
M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018. https://mitpress.mit.edu/9780262039406/
A. Maurer, A Vector-Contraction Inequality for Rademacher Complexities, ALT 2016. https://arxiv.org/abs/1605.00251

7 thms3 active usersReviewed

Completed

Algebraic Geometry Differential Geometry Linear Optimization+2·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 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Theoretical Computer Science·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 3: The Incomparable-Pairs Graphs of Canonical Interval Orders Have Unbounded Chromatic NumberResearch Paper

Motivation

Single-machine scheduling with precedence constraints asks for an order in which one machine processes jobs while respecting prescribed comparisons between them. For the objective of minimizing total weighted completion time, the structure of the precedence order can influence the quality of approximation algorithms. Ambühl, Mastrolilli, Mutsanas, and Svensson connect one such approach to coloring a graph built from the order's incomparable pairs. A bounded number of colors would make a certain class of coloring-based guarantees uniform over the class of precedence orders. Their Theorem 4.3 shows that canonical interval orders have no such uniform bound for this particular graph. Ambühl et al., §4.2, p. 658

An interval order is a partial order whose elements can be represented by closed real intervals, with one element strictly before another when the first interval ends before the second begins. Interval orders are a familiar restriction of general precedence systems. The paper distinguishes them from semiorders, represented by intervals of equal length, for which it reports a three-element realizer bound and a corresponding scheduling guarantee. The chromatic obstruction here explains why that particular bounded-color route cannot be extended uniformly from semiorders to all interval orders. It does not assert that every scheduling approach to interval orders fails. Ambühl et al., §§3–4.2, pp. 656–658

Setting

For an integer $n\ge2$ , let $[n]$ be a linearly ordered set with $n$ points. The canonical interval order $I_n$ has one element for every pair of distinct points $a<b$ in $[n]$ , viewed as the closed interval $[a,b]$ . For two such intervals, write $S\le_{I_n}T$ when $S=T$ or the right endpoint of $S$ is strictly less than the left endpoint of $T$ . Thus intervals that touch at an endpoint remain incomparable. The formalization represents each interval by its two-element endpoint set, and its order relation is equivalent to this endpoint rule. Ambühl et al., §4.2, p. 658

For any partial order $P$ on a ground set $N$ , an ordered incomparable pair is $(x,y)$ with neither $x\le_P y$ nor $y\le_P x$ . Both $(x,y)$ and $(y,x)$ are vertices when $x$ and $y$ are incomparable. A linear extension of $P$ is a linear order on the same elements that contains all comparisons of $P$ . It reverses $(x,y)$ if it places $y$ before $x$ . The graph $G_P$ has the ordered incomparable pairs as vertices. Two distinct vertices form an edge when no linear extension reverses both, while each singleton can be reversed by some linear extension. This singleton condition is the minimality clause in the paper's definition through its hypergraph of incomparable pairs. Ambühl et al., §2.1, p. 655, §3, p. 656

A proper $k$ -coloring assigns one of $k$ colors to every vertex of $G_P$ so that endpoints of an edge have different colors. The graph's chromatic number $\chi(G_P)$ is the least positive number of colors that works, when the graph is nonempty. The mission uses the equivalent predicate that no proper map into a fixed $k$ -element color set exists once $n$ is large enough. This also gives a clear interpretation at $k=0$ .

Formalization targets

The goal is Theorem 4.3: for each fixed integer $k$ , all sufficiently large canonical interval orders have incomparable-pairs graphs with chromatic number greater than $k$ . With $k\ge0$ , the Lean target is

\forall k\in\mathbb N,\ \exists n_0\ge2,\ \forall n\ge n_0,\quad G_{I_n}\text{ is not $k$-colorable}.

The paper states $k$ as an integer. Its negative cases are immediate from nonnegativity of chromatic numbers; the target states the substantive range. The threshold $n_0$ may depend on $k$ , while $I_n$ and $G_{I_n}$ are constructed from $n$ rather than supplied as arbitrary objects. Ambühl et al., Theorem 4.3, p. 658

Two assertions from the theorem's proof serve as milestones. First, $\chi(G_{I_n})$ is nondecreasing as $n$ increases. Second, for four endpoints $i<j<\ell<m$ , the vertices $(\{i,j\},\{j,\ell\})$ and $(\{j,\ell\},\{\ell,m\})$ are adjacent in $G_{I_n}$ . They are recorded with their wording and provenance from §4.2. A separately published theorem on hypergraph Ramsey numbers is included as a reference because the source uses that theorem in its large- $n$ argument. Ambühl et al., proof of Theorem 4.3, p. 658

Significance

The result provides a precise structural limitation: across the canonical interval orders, the chromatic numbers of $G_{I_n}$ cannot be bounded by one constant. The graph $G_P$ is a specific graph of ordered incomparable pairs, distinct from other graphs that can be associated with a scheduling instance. Thus the conclusion addresses the bounded-color approach attached to this graph, without asserting an algorithmic impossibility for interval-order scheduling. The paper contrasts this limitation with the bounded-realizer situation for semiorders. Ambühl et al., §§3–4.2, pp. 656–658

The theorem is proved in the 2011 paper. The remaining work in this mission is a machine-checked development of its definition layer, its two stated supporting assertions, and the unbounded-color conclusion. The partial-order property of $I_n$ is already proved in the definition file; the three theorem statements are open proof targets in the proposal. A completed formalization would also give reusable components for finite interval orders, ordered incomparable pairs, and coloring arguments in dimension theory.

Difficulty

A pair of intervals overlapping or touching is easy to recognize as incomparable, but graph adjacency has a stronger meaning: it quantifies over every linear extension of the entire partial order. A local test based only on the four displayed intervals would silently change the graph. Likewise, the fact that two vertices have different endpoint descriptions does not by itself make them adjacent. The formal argument must connect the canonical interval representation to the global extension-based edge condition, then show that a bounded coloring cannot persist as the endpoint set grows. Ambühl et al., proof of Theorem 4.3, p. 658

Formalization scope

The endpoint set is Fin n, hence indexed $0,\ldots,n-1$ rather than the paper's $1,\ldots,n$ ; the shift preserves order. Elements of $I_n$ are exactly two-element subsets of this set. The order relation includes equality and strict separation of endpoint sets and is proved to be a partial order. The graph is defined for an arbitrary binary relation so it can be reused, but every target here applies it to the concrete partial order $I_n$ . Vertices are ordered incomparable pairs, and adjacency retains both singleton reversibility and failure of simultaneous reversibility. Defining adjacency directly from the desired four-point pattern would trivialize the target and is excluded.

Colorable n k means existence of a proper function from all vertices of $G_{I_n}$ to Fin k. For an empty graph, zero-colorability is allowed by this representation. The theorem therefore includes a threshold $n_0\ge2$ and quantifies over every $n\ge n_0$ ; the assertion itself forces the threshold past any empty-graph exceptions. The formal target uses natural $k$ ; the paper's negative integer values need no separate theorem. No asymptotic notation or unspecified constants occur. The source's Ramsey number $R(3:4,\ldots,4)$ is not hard-coded into the goal, because the source asserts existence of a suitable threshold, not that the least threshold equals that value.

The printed adjacency justification names an alternating-cycle pair set different from the two adjacent vertices in the preceding sentence. The milestone formalizes the adjacency assertion itself and records the printed explanation verbatim for review; it does not turn the mismatched pair set into a hypothesis. The mission needs finite order embeddings, linear extensions, graph colorings, and a finite Ramsey theorem. The existing published Ramsey theorem is referenced as a reusable result. No scheduling approximation algorithm, polynomial-time statement, or numerical scheduling guarantee is formalized in this mission.

Selected references

Christoph Ambühl, Monaldo Mastrolilli, Nikolaos Mutsanas, and Ola Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4), 653–669, 2011. DOI: 10.1287/moor.1110.0512

7 thms3 active usersReviewed

All missions

An Optimal Algorithm for On-line Bipartite Matching 2: No Randomized On-line Algorithm Guarantees an Expected Matching Larger Than n(1 − 1/e) + o(n)Research Paper

Motivation

Setting

Formalization targets

Main theorem

Milestone statements

Significance

Difficulty

Formalization scope

Selected references

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 VI: With a Forecast Update, Buy-Back Terms with w₁ − w₂ + λc₂ = λc₁ Give the Retailer λΩ₁(q₁) and a Lower Period-2 Margin w₂ − c₂ < w₁ − c₁Textbook

Motivation

Setting

Formalization targets

Goal: the buy back contract coordinates

Milestones

Significance

Difficulty

Formalization scope

Selected references

Complexity of Machine Scheduling Problems 3: KNAPSACK Reduces to Single-Machine Total Weighted TardinessResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4(d)

The equivalence and its claims

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 VII: In the Single-Location Base-Stock Model the Transfers t_I = (1 − λ)h_r, t_B = β_r − λβ Make the Retailer's Cost λc(s_r)Textbook

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Complexity of Machine Scheduling Problems 2: KNAPSACK Reduces to Single-Machine Maximum Lateness, Weighted Number of Late Jobs, and Weighted Completion Time with DeadlinesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4(b), (c), (e), (f)

Milestones: the four yes-instance equivalences

Significance

Difficulty

Formalization scope

Selected references

Complexity of Machine Scheduling Problems 1: PARTITION Reduces to Makespan and to Weighted Completion Time on Two Identical MachinesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references