Operations Research

Completed

Convex Optimization Linear Optimization Optimization·Captain: mikedeng1

Path-Finding Methods for Linear Programming I: Centering with Weights on the Weighted Central PathResearch Paper

Motivation

Interior point methods solve a linear program by following a central path: a curve of minimizers of a penalized objective that trades off cost against distance from the boundary of the feasible region. The classical analysis of path following with the logarithmic barrier needs $O(\sqrt{m}\,L)$ iterations for a program with $m$ constraints, where $L$ is the bit complexity of the input (Renegar 1988). For programs with many more constraints than variables, $m$ can be far larger than the dimension $n$ or the rank of the constraint matrix, and the $\sqrt m$ factor is then the bottleneck.

Lee and Sidford (FOCS 2014) reduce the iteration count to $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ by following a weighted central path in which each constraint carries its own positive weight, and the weights are re-computed as the algorithm moves. Their improved maximum-flow algorithm is an application of the same method.

Timeline. Karmarkar (1984) gave the first polynomial-time interior point method for linear programming. Renegar (1988) showed that path following with the logarithmic barrier needs $O(\sqrt m L)$ iterations. Nesterov and Nemirovskii (1994) showed that a universal self-concordant barrier yields $O(\sqrt n L)$ iterations, but that barrier is not known to be efficiently computable. Lee and Sidford (2014) achieved $\tilde O(\sqrt{\mathrm{rank}(A)}L)$ iterations, each reducible to $\tilde O(1)$ linear-system solves.

This mission covers the first half of that framework (§IV of the paper): the weighted central path, the weighted Newton step, and the centering theorem that shows a single step followed by re-weighting makes constant-factor progress.

Setting

Let $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ , and consider the linear program

\min_{x\in\mathbb R^n:\ Ax\ge b} c^Tx .

The slack of a point $x$ is $s(x)=Ax-b$ , and the interior is $S^0=\{x : Ax>b\}$ , the points with all slacks strictly positive. For a path parameter $t$ and a vector of positive weights $w\in\mathbb R^m_{>0}$ , the weighted penalized objective is

f_t(x,w)=t\,c^Tx-\sum_{i=1}^m w_i\log s(x)_i .

A pair $(x,w)$ is feasible if $x\in S^0$ and $w>0$ .

Write $S_x=\mathrm{diag}(s(x))$ , $W=\mathrm{diag}(w)$ and $\|v\|_M=\sqrt{v^TMv}$ . The Newton step and the centrality are

\vec h_t(x,w)=\big(A^TS_x^{-1}WS_x^{-1}A\big)^{-1}\big(tc-A^TS_x^{-1}w\big),\qquad \delta_t(x,w)=\big\|\vec h_t(x,w)\big\|_{A^TS_x^{-1}WS_x^{-1}A}.

The matrix $A^TS_x^{-1}WS_x^{-1}A$ is the Hessian of $f_t$ in $x$ , and $tc-A^TS_x^{-1}w$ is its gradient; $\delta_t(x,w)=0$ exactly when $x$ minimizes $f_t(\cdot,w)$ .

For slacks $s$ and weights $w$ the projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A(A^TS^{-1}WS^{-1}A)^{-1}A^TS^{-1}W^{1/2}$ and the slack sensitivity is

\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\vec 1_i\big\|_{P_{S^{-1}A}(w)} .

A weight function (Definition 4) is a differentiable map $\vec g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ from slacks to weights with constants $c_1$ (size, a bound on $\|\vec g(s)\|_1$ ), $c_\gamma\ge1$ (slack sensitivity, $\gamma(s,\vec g(s))\le c_\gamma$ ), $c_r\ge1$ (step consistency, two inequalities on the Jacobian $G'(s)$ of $\vec g$ that hold for every $r\ge c_r$ ), and uniformity $\|\vec g(s)\|_\infty\le2$ .

Formalization targets

Goal: Theorem 5 (Centering with Weights), §IV.C

Let $\vec g$ be a weight function for $A$ with constants $c_1,c_\gamma,c_r$ , let $x^{(old)}\in S^0$ , $s^{(old)}=s(x^{(old)})$ , and

x^{(new)}=x^{(old)}-\frac{1}{1+c_r}\,\vec h_t\big(x^{(old)},\vec g(s^{(old)})\big).

If $\delta_t(x^{(old)},\vec g(s^{(old)}))\le\frac{1}{100c_\gamma c_r^2}$ , then $x^{(new)}\in S^0$ and

\delta_t\big(x^{(new)},\vec g(s^{(new)})\big)\le\Big(1-\frac{1}{4c_r}\Big)\delta_t\big(x^{(old)},\vec g(s^{(old)})\big).

The theorem is stated for every weight function, not for the specific one constructed in §V of the paper; that construction is the subject of a separate mission.

Milestone: Lemma 3 (Split Newton Step), §IV.B

For feasible $(x^{(old)},w^{(old)})$ and $r\ge0$ , the split step $x^{(new)}=x^{(old)}-\frac1{1+r}\vec h_t$ , $w^{(new)}=w^{(old)}+\frac r{1+r}W_{(old)}S_{(old)}^{-1}A\vec h_t$ satisfies, whenever $\delta_t\le\frac1{8\gamma}$ ,

\delta_t\big(x^{(new)},w^{(new)}\big)\le\frac{2}{1+r}\,\gamma\,\delta_t^2,

with $\gamma=\gamma(s(x^{(old)}),w^{(old)})$ , and the new pair is feasible.

Milestone: Lemma 1, §IV.B

For feasible $(x,w)$ and $\alpha,t\ge0$ :

\delta_{(1+\alpha)t}(x,w)\le(1+\alpha)\delta_t(x,w)+\alpha\sqrt{\|w\|_1}.

Significance

Theorem 5 is the centering half of the weighted path-following method. Combined with Lemma 1, it shows that the path parameter can be doubled, while staying close to the weighted central path, in a number of steps of the form (5) controlled by $c_\gamma$ , $c_r$ and $\sqrt{c_1}$ . The paper then constructs (§V, Theorem 1) a weight function with $c_1=2\,\mathrm{rank}(A)$ , $c_\gamma=2$ and $c_r$ logarithmic in $m/\mathrm{rank}(A)$ , which yields the $\tilde O(\sqrt{\mathrm{rank}(A)})$ iteration bound. The theorem isolates exactly which properties of a weighting scheme are needed, so it applies to any weight function satisfying Definition 4.

The FOCS extended abstract states these results without proofs; the proofs are in the arXiv full version (arXiv:1312.6677). The results are proved on paper. No machine-checked formalization of weighted path following, or of the Lee–Sidford framework, is known. A formal proof would check the constants $\frac1{100}$ , $\frac1{4}$ , $\frac18$ and $\frac2{1+r}$ as stated in the extended abstract, and would produce reusable Lean infrastructure for Newton steps of barrier functions with explicit matrix formulas.

Difficulty

The standard analysis of Newton's method on a self-concordant barrier gives quadratic convergence of centrality for a fixed barrier. Here the barrier changes during the step: the weights are reset to $\vec g(s(x^{(new)}))$ , so the new centrality is measured with respect to a different Hessian and a different gradient. The obvious argument, analysing the step at fixed weights and then treating the re-weighting as a small perturbation, does not give a contraction factor independent of $m$ : without control of how $\vec g$ reacts to changes in the slacks, the re-weighting can undo the progress of the step. The step-consistency conditions of Definition 4 are the only hypotheses that control this reaction, and they are pointwise bounds on the Jacobian of $\vec g$ , while the step moves the slacks by a finite amount.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and products are Matrix.mulVec and dotProduct. $S^{-1}$ is the diagonal matrix of reciprocals, $W^{\pm1/2}$ the diagonal matrices of $\sqrt{w_i}^{\pm1}$ , and $\|v\|_M=\sqrt{v^TMv}$ . The Newton step and centrality are defined by the explicit formulas (3) and (4), not by derivatives of $f_t$ ; the centrality uses the Hessian-norm form of (4). The Jacobian $G'(s)$ is the Fréchet derivative fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm.

Conventions fixed where the paper is silent:

Full column rank. Every theorem assumes A.rank = n. The paper uses $(A^TS_x^{-1}WS_x^{-1}A)^{-1}$ without comment; the inverse exists for positive slacks and weights exactly when $A$ has full column rank. Lean's matrix inverse is $0$ on singular matrices, which would make $\vec h_t$ , $\delta_t$ and $\gamma$ vanish and every statement trivially true; the rank hypothesis rules this trivializing reading out.
Size as an upper bound. Definition 4's " $c_1(\vec g)=\|\vec g(s)\|_1$ " is read as $\|\vec g(s)\|_1\le c_1$ for all $s>0$ (the paper's own weight function reports a $c_1$ above its $\ell_1$ norm). $c_1$ does not enter Theorem 5.
Operator norm. Step consistency's first bullet is written as $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ for all $y$ .
Lemma 3's $r$ ranges over $r\ge0$ , and $\gamma(x,w)$ means $\gamma(s(x),w)$ .
Feasibility of the new point is part of the conclusion of Lemma 3 and Theorem 5, since the page's conclusion evaluates quantities defined only on the interior.
Maximum over $[m]$ is a supremum over Fin m (attained for $m\ge1$ , equal to $0$ for $m=0$ ).
The path parameter $t$ is unrestricted in Theorem 5 and Lemma 3, as on the page; Lemma 1 assumes $t\ge0$ as the page does.

A complete development needs basic facts about weighted norms and the projection matrix $P_{S^{-1}A}(w)$ , spectral comparison of the matrices $A^TS^{-1}WS^{-1}A$ for nearby slacks and weights, and calculus for vector-valued maps on the positive orthant. The weighted-norm and projection-matrix material is reusable for any interior point analysis. Proofs of the milestones, alternative arguments, and sharper constants are welcome.

Selected references

Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv:1312.6677, 2013. https://arxiv.org/abs/1312.6677
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40, 1988, pp. 59–93. https://doi.org/10.1007/BF01580724
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, pp. 373–395. https://doi.org/10.1007/BF02579150
Y. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

6 thms2 active usersReviewed

Completed

Linear Optimization Optimization·Captain: mikedeng1

Critical-Path Planning and Scheduling II: The Project Cost Curve Is Non-Increasing, Piecewise Linear and ConvexResearch Paper

Motivation

A large engineering or construction project is a set of jobs with precedence constraints, and most jobs can be finished faster at a higher cost (overtime, more crews, faster equipment). Planners want to know, for every possible project duration, the cheapest way to meet it. The resulting trade-off between duration and direct cost is what management compares with overhead, penalties and market losses when it picks a schedule.

J. E. Kelley, Jr. and M. R. Walker introduced the critical-path method (CPM) in 1959, from work at du Pont and Remington Rand (Kelley and Walker 1959). Alongside the critical-path computation, they modelled each job's cost as a linear function of its duration and posed the choice of durations as a parametric linear program. They stated that its optimal value, as a function of the project duration $\lambda$ , is a non-increasing, piecewise linear, convex function, which they called the project cost curve. The 1959 paper gives no proof and defers the detailed development to a separate paper (Kelley 1961). Fulkerson (1961) gave a network-flow algorithm that computes the curve. Time–cost trade-off analysis ("crashing") has been a standard part of project management since then.

Setting

A project network has events labelled $0, 1, \dots, n$ with $n \ge 1$ . Event $0$ is the origin and event $n$ the terminus. A finite set $P$ of jobs is given, each an ordered pair $(i,j)$ : an arrow from event $i$ to event $j$ . As in the paper, labels increase along arrows ( $i < j$ for every $(i,j) \in P$ ), the origin precedes every event, and the terminus follows every event.

For job durations $y = (y_{ij})$ , the earliest event times are given by recursion (1):

t_0^{(0)} = 0,\qquad t_j^{(0)} = \max\,[\,y_{ij} + t_i^{(0)} \mid i<j,\ (i,j)\in P\,],\quad 1\le j\le n,

and $t_n^{(0)}(y)$ is the earliest project completion time.

Each job has a crash duration $d_{ij}$ and a normal duration $D_{ij}$ with $0 \le d_{ij} \le D_{ij}$ , and a linear job cost $a_{ij}y_{ij} + b_{ij}$ with $a_{ij} \le 0$ , $b_{ij} \ge 0$ . The project (direct) cost is

\text{(7)}\qquad \sum_{(i,j)\in P} (a_{ij} y_{ij} + b_{ij}).

A schedule for $\lambda$ is a pair $(y,t)$ with

\text{(5)}\ d_{ij}\le y_{ij}\le D_{ij},\qquad \text{(8)}\ y_{ij}\le t_j-t_i\quad ((i,j)\in P),\qquad \text{(9)}\ t_0=0,\ t_n=\lambda.

Let $\Lambda$ be the set of $\lambda$ for which a schedule exists. For $\lambda \in \Lambda$ the project cost curve $C(\lambda)$ is the minimum of (7) over schedules for $\lambda$ . Write $\lambda_c = t_n^{(0)}(d)$ (all jobs crashed) and $\lambda_N = t_n^{(0)}(D)$ (all jobs normal).

Formalization targets

Goal: the shape of the project cost curve (p. 165)

C \text{ is non-increasing on } \Lambda,\qquad C \text{ is piecewise linear on } \Lambda,\qquad C \text{ is convex on } \Lambda .

Piecewise linear means finitely many breakpoints $\beta_0<\dots<\beta_m$ with $\Lambda\subseteq[\beta_0,\infty)$ , and affine pieces on $\Lambda\cap[\beta_k,\beta_{k+1}]$ and on $\Lambda\cap[\beta_m,\infty)$ . The goal fixes no breakpoints or slopes. It asserts only the shape the paper claims, on the whole of $\Lambda$ .

Milestones

Feasible range (p. 165, "until no further reduction in project completion time is possible"): $\Lambda = [\lambda_c, \infty)$ .
Existence of optimal schedules (p. 165, the linear program (8), (9)): for every $\lambda\in\Lambda$ the minimum of (7) is attained.
All-normal solution (p. 165): $(D, t^{(0)}(D))$ is a minimum cost schedule for $\lambda = \lambda_N$ .
$\lambda$ is the earliest completion time (p. 165, "within the limits of most interest"): for $\lambda_c\le\lambda\le\lambda_N$ some minimum cost schedule $(y,t)$ for $\lambda$ has $t_n^{(0)}(y)=\lambda$ .

Significance

The cost curve is the output of CPM's cost analysis. Its convexity is what makes the paper's parametric procedure valid: jobs are expedited in order of increasing marginal cost, and the curve is traced from $\lambda_N$ down to $\lambda_c$ one linear piece at a time. Monotonicity justifies reading the curve as a trade-off. Piecewise linearity with finitely many pieces means the whole curve is determined by finitely many characteristic schedules, the vertices plotted in the paper's Fig. 3. The milestones identify the domain of the curve, show that it is well defined, and fix its right end at the all-normal solution.

These facts are classical: they follow from parametric linear programming, and Kelley (1961) and Fulkerson (1961) develop them in detail. No machine-checked proof of them is known. Prove2Me has a related result, LinearOptimization.lp_optimal_cost_convex_in_rhs (Bertsimas–Tsitsiklis, Theorem 5.1): convexity of the optimal cost of a standard-form LP in its right-hand side. It covers convexity only, for a different LP form, and says nothing about monotonicity or finitely many pieces. This mission adds a formal model of CPM's time–cost program and the full three-part shape theorem.

Difficulty

Convexity alone follows from the usual argument: a convex combination of optimal schedules for two durations is a schedule for the combined duration. Monotonicity needs the structure of the network: when $\lambda$ increases, only the constraints (8) on jobs ending at the terminus loosen, because no job leaves the terminus. The hard part is piecewise linearity with finitely many pieces. Convexity does not imply it, and a general result on value functions of linear programs has to be tied to this specific program, whose right-hand side depends on $\lambda$ only through $t_n = \lambda$ . The domain is also unbounded, so the argument must show that the curve is eventually a single affine (in fact constant) piece. It cannot just produce finitely many pieces on a compact interval.

Formalization scope

Events are Fin (n + 1) with origin 0 and terminus Fin.last n, and 1 ≤ n. Jobs are a Finset of ordered pairs, with at most one job per ordered pair. The standing assumptions of pp. 161–162 are fields of ProjectNetwork: labels increase along jobs, and reachability via Relation.ReflTransGen from the origin and to the terminus. Times and durations are real. Job data are functions Fin (n+1) → Fin (n+1) → ℝ, constrained and read only on $P$ . The hypotheses $0\le d_{ij}\le D_{ij}$ , $a_{ij}\le 0$ and $b_{ij}\ge 0$ are fields of JobData. Recursion (1) is earliest, defined by well-founded recursion on the label. It uses a fallback value $0$ for an event without predecessors, which occurs only at the origin. The paper's $\lambda$ is written lam. Constraint (9) fixes $t_n = \lambda$ exactly, and the event times are otherwise unconstrained.

The goal takes $C : \mathbb{R}\to\mathbb{R}$ with the hypothesis that $C(\lambda)$ is the least element of the set of costs of schedules for $\lambda$ , for every $\lambda \in \Lambda$ . All three conclusions are stated on $\Lambda$ only. This rules out the trivializing formalizations:

a junk-valued infimum off $\Lambda$ plays no role;
$C$ is tied to the program, and the hypothesis on $C$ is satisfiable by milestone 2;
piecewise linearity requires finitely many pieces that cover all of $\Lambda$ ;
all three properties are claimed, not convexity alone.

The goal keeps $a_{ij}\le 0$ , as the page does throughout §3, although monotonicity and convexity would hold without it.

Disclosed readings:

Milestone 1 renders "until no further reduction in project completion time is possible" as $\Lambda=[\lambda_c,\infty)$ .
Milestone 4 reads "within the limits of most interest" as $\lambda_c\le\lambda\le\lambda_N$ . It asserts that some optimal schedule has $t_n^{(0)}(y)=\lambda$ . "Every" is false: when all $a_{ij}=0$ , the all-crash durations are optimal for every $\lambda$ .

A complete development needs:

the existence of LP optima under a bounded objective, or a direct compactness argument on the feasible polyhedron;
a parametric-LP or polyhedral argument for finitely many linear pieces;
basic facts on the recursion (1).

The one-variable notion IsPiecewiseLinearOn and the facts on earliest event times can be reused in scheduling missions. Proofs of the milestones, of any of the three goal conjuncts separately, and general lemmas on parametric LP value functions are all welcome.

Not formalized: general piecewise linear convex job costs (deferred by the paper to its references [7], [8]), and the primal–dual procedure itself (a method, not a claim).

Selected references

J. E. Kelley, Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proc. Eastern Joint IRE-AIEE-ACM Computer Conference, 1959, pp. 160–173. https://doi.org/10.1145/1460299.1460318
J. E. Kelley, Jr., Critical-Path Planning and Scheduling: Mathematical Basis, Operations Research 9(3), 1961, pp. 296–320. https://doi.org/10.1287/opre.9.3.296
D. R. Fulkerson, A Network Flow Computation for Project Cost Curves, Management Science 7(2), 1961, pp. 167–178. https://doi.org/10.1287/mnsc.7.2.167
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §5.2 (the optimal cost as a function of the right-hand side).

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design·Captain: mikedeng1

Incentives in Teams: The Own Profit Incentive Structure Is an Optimal Incentive Structure for a ConglomerateResearch Paper

Motivation

An organization whose members hold private information faces two problems at once. The first is the team problem of Marschak and Radner: choose the rules by which members observe, communicate and decide so as to maximize the expected payoff of the organization as a whole (Marschak–Radner 1972). The second is the incentive problem: a member who is paid by their own results has no reason to follow those rules, and in particular no reason to report truthfully what they have observed. Theodore Groves' Incentives in Teams (Econometrica 41(4), 1973) connected the two. For a decentralized firm in which subunits report to a head, it exhibits compensation rules that make the team-optimal behaviour, truthful messages included, each subunit manager's unique best reply.

The construction is the origin of what is now called the Groves scheme, and with Vickrey's second-price auction (Vickrey 1961) and Clarke's pivot rule (Clarke 1971) it forms the Vickrey–Clarke–Groves (VCG) family of mechanisms.

Timeline:

1961, Vickrey: second-price auctions make truthful bidding a dominant strategy for a single object.
1971, Clarke: pivot payments for public-good decisions with deterministic valuations.
1972, Marschak–Radner: the economic theory of teams, with information and decision structures but a common payoff.
1973, Groves: compensation $C_i^{II}$ based on the head's conditional expectation of the other units' payoffs; Theorem 1 proves optimality in a conglomerate with independent component states and one round of communication.
1977, Green–Laffont: in the complete-information setting, Groves-type payments are the only ones that make truth-telling dominant (Econometrica 45(2)).
1979, d'Aspremont–Gérard-Varet: Bayesian incentive-compatible mechanisms with expected externality payments (J. Public Econ. 11(1)).

The conglomerate model

The organization consists of a head (component $0$ ) and finitely many subunits $i = 1, \dots, n$ . Each component $k$ has its own random component state $s_k \in S_k$ , and the components are independent: the state of the environment $s = (s_0, s_1, \dots, s_n)$ is distributed according to the product law $P(s) = P_0(s_0) \prod_{i} P_i(s_i)$ (Condition S.2).

Every member plays a strategy $\beta_k = (\zeta_k, \gamma_k, \delta_k)$ made of an observation strategy $\zeta_k$ on its own state, a message strategy $\gamma_k$ and a decision strategy $\delta_k$ (Condition S.3). Communication runs only between the head and each subunit, in one exchange: the head observes $\zeta_0(s_0)$ and sends $\gamma_0^i(\zeta_0(s_0))$ to subunit $i$ ; the subunit, with information $y_i(s) = [\zeta_i(s_i), \gamma_0^i(\zeta_0(s_0))]$ , sends back $\gamma_i(y_i(s))$ ; the head's information is $y_0(s) = [\zeta_0(s_0), \{\gamma_i(y_i(s))\}_{i}]$ (3.1). Decisions are $\delta_i(y_i(s))$ and $\delta_0(y_0(s))$ .

The organization payoff is a sum of components (Condition S.4),

\omega_0(\beta, s) = \sum_{i=1}^n v_i[\delta_i(y_i(s)), \delta_0(y_0(s)); s_i] + v_0[\delta_0(y_0(s)), s_0],

and $\bar\omega_0(\beta) = E[\omega_0(\beta, s)]$ . Each $v_i$ accrues directly to subunit $i$ (Condition S.5). Strategy sets $B_0, B_1, \dots, B_n$ are given; $\beta/\beta_i$ denotes $\beta$ with subunit $i$ 's strategy replaced by $\beta_i$ . Two strategies $\beta_i', \beta_i''$ are equivalent if $\bar\omega_0(\beta/\beta_i') = \bar\omega_0(\beta/\beta_i'')$ for every $\beta \in B$ .

Assumption A requires a $\beta^* \in B$ maximizing $\bar\omega_0$ over $B$ such that, for each subunit, $\bar\omega_0(\beta^*) > \bar\omega_0(\beta^*/\beta_i)$ whenever $\beta_i \in B_i$ is not equivalent to $\beta_i^*$ .

An incentive structure $W = \{\omega_i\}$ pays subunit $i$ the amount $\omega_i(\beta, s)$ . The class $\mathscr{J}$ (3.2) consists of those of the form $\omega_i = v_i[\dots] + C_i(y_0(s))$ : own payoff plus a compensation computed from the head's information only. $W$ is optimal (2.6) if $\beta_i^*$ maximizes $\bar\omega_i(\beta^*/\beta_i)$ over $B_i$ , uniquely up to equivalence.

Formalization targets

Goal: Theorem 1 (p. 625)

With $C_i^{II}(y_0) = \sum_{j \ne i} E\big[v_j[\delta_j^*(y_j^*(s)), \delta_0^*(y_0^*(s)); s_j] \,\big|\, y_0^*(s) = y_0\big] - A_i$ , the sum running over all components $j \in \{0, \dots, n\}$ other than $i$ and the expectation taken under $\beta^*$ (3.3), the structure $\omega_i^{II} = v_i[\dots] + C_i^{II}(y_0(s))$ lies in $\mathscr{J}$ and satisfies, for every subunit $i$ and every $\beta_i \in B_i$ ,

\bar\omega_i^{II}(\beta^*/\beta_i) \le \bar\omega_i^{II}(\beta^*), \qquad \text{with strict inequality if } \beta_i \not\equiv \beta_i^*.

It holds for every $\beta^*$ satisfying Assumption A, all strategy sets and all constants $A_i$ .

Milestones

The Appendix Lemma: the sets of states consistent with the head's information under $\beta^*/\beta_i$ and under $\beta^*$ have the same projections onto every component other than $i$ .
The right-hand side of (A.2): the head's conditional expectation factorizes over the independent components.
(A.2) for a subunit $j \ne i$ , and 4. (A.2) for the head's component $j = 0$ : the expected payoff of component $j$ under $\beta^*/\beta_i$ equals the expected value of its conditional expectation.
(A.1): $\bar\omega_i^{II}(\beta^*/\beta_i) + A_i = \bar\omega_0(\beta^*/\beta_i)$ for all $\beta_i \in B_i$ .

Significance

Theorem 1 shows that a head who knows only the messages it receives can nonetheless align every subunit's interest with the organization's, without monitoring decisions or observations. It is an early statement that expected-externality payments make truthful communication an equilibrium of a decentralized organization, and the Bayesian, team-theoretic counterpart of the dominant-strategy results of Vickrey and Clarke. Its structure (own payoff plus a transfer depending only on the others' reported information) is the template later characterized by Green and Laffont and generalized by d'Aspremont and Gérard-Varet.

Theorem 1 is proved in the paper; nothing here is open mathematically. What the mission adds is a machine-checked version with every modelling choice explicit: how information is generated by the message protocol, what the conditional expectation in (3.3) means on events of probability zero, and which equivalence "uniquely" refers to. No machine-checked proof of Theorem 1 is known to the platform. The platform's AGT.vcg_incentive_compatible treats the complete-information, direct-revelation analogue (deterministic valuations, dominant strategies), a different model with a different conclusion.

Difficulty

The tempting argument conditions on the head's information $y_0^*(s) = y_0$ under $\beta^*$ and compares it with the head's information under a deviation. That comparison fails when a deviating subunit sends a message that $\gamma_i^*$ never sends: the conditioning event then has probability zero under $\beta^*$ , and the conditional expectation of (3.3) is not determined by the joint law. A second obstacle is that the head's information under a deviation differs from the information under $\beta^*$ in every coordinate the deviation touches, while the compensation is computed as if $\beta^*$ were played; the statement to be proved compares expectations taken under two different joint strategies, and the one-exchange protocol makes the head's messages, and hence every subunit's information, depend on the head's own state. Treating these dependencies loosely either produces a circular definition of the information functions (as (3.1) is printed) or a statement that fails on events of probability zero.

Formalization scope

Every component state space $S_k$ is a finite type with weights that are nonnegative and sum to one; the joint law is the product of these weights and expectations are finite sums. The paper allows general probability spaces; the finite case covers the whole argument and gives conditional expectations at a point an elementary meaning.
Subunits form a finite index type; the head is a separate component with its own observation, message and decision types. Observation, message and decision spaces are fixed types per component.
Information (3.1) follows the single exchange of messages the paper describes in §4.A (p. 627): the head's message to subunit $i$ is a function of the head's observation. As printed, (3.1) is circular; this protocol is the paper's own resolution.
$C_i^{II}$ is used in factorized form: the head's term conditions only the head's state on the head's observation, and subunit $j$ 's term conditions only $s_j$ on the message $j$ sent. A separate milestone states that this equals the literal conditional expectation of (3.3) whenever the conditioning event has positive probability. The literal elementary quotient takes the value $0$ on null events, and with it Theorem 1 is false (one subunit that can send an unused message suffices); the factorized form is what the Appendix computes. The sum in (3.3) includes the head's component $v_0$ .
Equivalence of strategies is footnote 5's, over all $\beta \in B$ ; optimality includes the strict inequality for non-equivalent deviations. A formalization that replaces equivalence by equality of strategies, fixes $B_i = \{\beta_i^*\}$ , drops the strict inequality, or assumes (A.1) as a hypothesis is not this theorem.
The Lemma carries the added hypothesis that the set $B(s)$ is nonempty; the paper's proof presumes it and the statement is false without it.

Contributions welcome: proofs of the milestones, and reusable finite-probability facts (conditioning on product events, iterated expectation over a coordinate) stated for product weights.

Selected references

T. Groves, Incentives in Teams, Econometrica 41(4):617–631, 1973. https://doi.org/10.2307/1914085
J. Marschak and R. Radner, Economic Theory of Teams, Yale University Press, 1972.
W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16(1):8–37, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
E. H. Clarke, Multipart Pricing of Public Goods, Public Choice 11:17–33, 1971. https://doi.org/10.1007/BF01726210
J. Green and J.-J. Laffont, Characterization of Satisfactory Mechanisms for the Revelation of Preferences for Public Goods, Econometrica 45(2):427–438, 1977. https://doi.org/10.2307/1911219
C. d'Aspremont and L.-A. Gérard-Varet, Incentives and Incomplete Information, Journal of Public Economics 11(1):25–45, 1979. https://doi.org/10.1016/0047-2727(79)90043-4

7 thms2 active usersReviewed

Graph Theory Linear Optimization Theoretical Computer Science·Captain: mikedeng1

Finding Minimum-Cost Circulations by Canceling Negative Cycles: Polynomial Termination of Minimum-Mean Cycle CancelingResearch Paper

Motivation

The minimum-cost circulation problem is a central problem of network optimization: transportation, assignment, shortest-path and maximum-flow problems are all special cases, and it is one of the few classes of linear programs with fast combinatorial algorithms. The oldest algorithm for it, the cycle-canceling algorithm of Klein (1967), repeatedly finds a residual cycle of negative cost and pushes as much flow as possible around it. With an arbitrary choice of cycle it can take exponentially many iterations even on integer data, and it need not terminate at all when capacities are irrational.

Goldberg and Tarjan (J. ACM 36(4), 1989) showed that one simple selection rule repairs this: always cancel a residual cycle whose mean cost (cost divided by number of arcs) is as small as possible. The resulting algorithm is strongly polynomial: its number of iterations is bounded by a polynomial in the number of vertices and arcs alone, independent of the magnitudes of capacities and costs. This mission formalizes that bound.

Timeline:

1967, Klein: the cycle-canceling algorithm, without an iteration bound.
1972, Edmonds and Karp: the first polynomial algorithm for minimum-cost flow (capacity scaling), polynomial in the bit length of the capacities.
1985, Tardos: the first strongly polynomial algorithm, introducing the arc-fixing idea that Theorem 3.8 generalizes.
1987–1989, Goldberg and Tarjan: generalized cost scaling and ε-optimality; in this paper, minimum-mean cycle canceling terminates after O(nm² log n) iterations for real costs (Theorem 3.9) and O(nm log(nC)) for integer costs bounded by C (Theorem 3.7).

Setting

A circulation network is a finite directed graph $G=(V,E)$ with $n=|V|$ vertices and $m=|E|$ arcs, which is symmetric ( $(v,w)\in E$ iff $(w,v)\in E$ , so $m$ counts both directions), together with real capacities $u(v,w)$ and real costs $c(v,w)$ , the cost being antisymmetric: $c(v,w)=-c(w,v)$ .

A circulation is a real function $f$ on arcs satisfying $f(v,w)\le u(v,w)$ , $f(v,w)=-f(w,v)$ on every arc, and conservation $\sum_{v:(w,v)\in E} f(v,w)=0$ at every vertex $w$ . Its cost is $\operatorname{cost}(f)=\tfrac12\sum_{(v,w)\in E}c(v,w)f(v,w)$ , and $f$ is minimum-cost (optimal) if no circulation has smaller cost.

The residual capacity of an arc is $u_f(v,w)=u(v,w)-f(v,w)$ ; arcs with $u_f>0$ are residual arcs. A residual cycle is a simple cycle of residual arcs; its capacity is the minimum residual capacity along it, its cost $c(\Gamma)$ is the sum of its arc costs, and its mean cost is $c(\Gamma)/|\Gamma|$ . Canceling a residual cycle raises the flow on each of its arcs by its capacity (and lowers the flow on each reverse arc by the same amount).

The minimum-mean cycle-canceling algorithm starts from any circulation and, while some residual cycle has negative cost, cancels a residual cycle whose mean cost is minimum among all residual cycles. Ties are broken arbitrarily, so the algorithm is a nondeterministic process; a run of length $K$ is any sequence $f_0,\dots,f_K$ of circulations produced by $K$ such iterations.

The analysis uses a price function $p:V\to\mathbb R$ , the reduced cost $c_p(v,w)=c(v,w)+p(v)-p(w)$ , and ε-optimality: for $\varepsilon\ge0$ , $f$ is ε-optimal if some $p$ gives $c_p(v,w)\ge-\varepsilon$ on every residual arc. The quantity $\varepsilon(f)$ is the least such $\varepsilon$ , and an arc is ε-fixed if all ε-optimal circulations carry the same flow on it.

Formalization targets

Goal: Theorem 3.9, with the proof's constant

For every circulation network with $n\ge2$ vertices, $m$ arcs, arbitrary real capacities and arbitrary real antisymmetric costs, every run of the minimum-mean cycle-canceling algorithm has length

K\ \le\ n\,m^2\,\lceil \ln n+1\rceil .

The statement quantifies over all starting circulations, all tie-breaking choices and all real data; it is the paper's $O(nm^2\log n)$ with the constant its proof establishes.

Milestones

In the order the proof uses them: Theorem 2.1 (optimal iff no negative residual cycle), Theorem 3.1 (optimal iff some price function has $c_p\ge0$ on residual arcs), Theorem 3.3 ( $\varepsilon(f)=-\mu(f)$ for nonoptimal $f$ , where $\mu(f)$ is the minimum cycle mean of the residual graph), Lemma 3.5 (a minimum-mean cancellation does not increase $\varepsilon(f)$ ), Lemma 3.6 ( $m$ cancellations shrink $\varepsilon(f)$ by a factor $1-1/n$ ), and Theorem 3.8 (an arc with $|c_p(v,w)|\ge2n\varepsilon$ is ε-fixed).

Significance

Theorem 3.9 shows that a classical, natural algorithm is strongly polynomial: its iteration count depends only on the combinatorial size of the network. Combined with Karp's $O(nm)$ minimum-mean cycle algorithm it yields an $O(n^2m^3\log n)$ strongly polynomial algorithm (Theorem 3.10), and its method, measuring progress by the minimum cycle mean and fixing arcs once $\varepsilon(f)$ is small, underlies the faster cancel-and-tighten algorithm of Section 4 and later strongly polynomial analyses of network-flow and related algorithms.

The theorem has been proved since 1989; this mission's contribution is a machine-checked proof. To the best of the platform's catalogue, no cycle-canceling bound, minimum cycle mean or ε-optimality statement has been formalized. The platform does hold the negative-cycle optimality criterion in a different model (LinearOptimization.network_no_negative_cycle_optimal, Bertsimas–Tsitsiklis Theorem 7.6, with nonnegative flows and supplies) and a flow decomposition theorem (LinearOptimization.network_flow_decomposition); both are related to milestones here but are stated for a different network model.

Difficulty

The obvious potential function, the cost of the circulation, decreases at every iteration but by amounts that depend on the data, so it yields no bound independent of the capacities and costs. The analysis instead has to track $\varepsilon(f)$ , an infimum over price functions, and relate it to the minimum cycle mean of a residual graph that changes after each cancellation, including arcs that appear only because of earlier cancellations. The strongly polynomial part needs a second ingredient: showing that the flow on some arc never changes again, which requires comparing the current circulation with all other ε-optimal circulations of the network, not only those the algorithm visits.

Formalization scope

Vertices form a finite type V; the arc set is E : Finset (V × V); capacities, costs and flows are real functions V → V → ℝ read only on E. $n$ is Fintype.card V and $m$ is E.card, counting $(v,w)$ and $(w,v)$ separately, as in the paper. Cycles are nonempty duplicate-free vertex lists, whose arcs are the cyclically consecutive pairs; one- and two-vertex cycles are allowed and have cost $0$ . Minimum mean is taken over all residual simple cycles of the current circulation. $\varepsilon(f)$ is an infimum (sInf) over a set that is nonempty and bounded below for every circulation; its attainment is to be proved, never assumed.

Explicit constants replacing the paper's $O(\cdot)$ :

Theorem 3.9: the paper prints $O(nm^2\log n)$ ; its proof uses groups of $k=m\,n\lceil\ln n+1\rceil$ iterations, at most $m$ of them, so the goal states $K\le n\,m^2\lceil\ln n+1\rceil$ with the natural logarithm.
The standing assumption $n\ge2$ (p. 874) is kept on the goal; the standing assumption $m\ge n$ is not used by the proof and is omitted.

"Terminates after at most $B$ iterations" means that every run has length at most $B$ . Asserting only that some run is short, or that the process eventually stops, does not formalize the theorem; nor does a step relation that drops negativity, simplicity of the cycle, minimality of the mean over all residual cycles, or the update by exactly the cycle's capacity.

A complete development needs cycle decomposition of the difference of two circulations, LP duality for circulations (Theorem 3.1), and bookkeeping for the residual graph under cancellation. These are reusable for any cycle-canceling or cost-scaling analysis, and contributions of that infrastructure as separate lemmas are welcome. Theorem 3.7 (the integer-cost bound) and Section 4 are outside this mission.

Selected references

A. V. Goldberg, R. E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, J. ACM 36(4):873–886, 1989. https://doi.org/10.1145/76359.76368
M. Klein, A primal method for minimal cost flows with applications to the assignment and transportation problems, Management Science 14(3):205–220, 1967. https://doi.org/10.1287/mnsc.14.3.205
É. Tardos, A strongly polynomial minimum cost circulation algorithm, Combinatorica 5(3):247–255, 1985. https://doi.org/10.1007/BF02579369
A. V. Goldberg, R. E. Tarjan, Finding minimum-cost circulations by successive approximation, Mathematics of Operations Research 15(3):430–466, 1990. https://doi.org/10.1287/moor.15.3.430
R. M. Karp, A characterization of the minimum cycle mean in a digraph, Discrete Mathematics 23(3):309–311, 1978. https://doi.org/10.1016/0012-365X(78)90011-0
J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, J. ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699

10 thms2 active usersReviewed

Dynamic Programming Probability Stochastic Systems·Captain: mikedeng1

On the optimality equation for average cost Markov decision processes and its validity for inventory control: The Average-Cost Optimality Equation for Setup-Cost Inventory ControlResearch Paper

Motivation

Average-cost criteria are standard in inventory, queueing and maintenance models that run indefinitely. For a Markov decision process (MDP), the central object is the average-cost optimality equation (ACOE). It couples a constant $w$ (the optimal long-run cost per period) with a relative value function $\tilde u$ . A stationary policy that attains the minimum in the ACOE is average-cost optimal. When the state space is uncountable, the one-step cost is unbounded and the transition probability is only weakly continuous, the ACOE is not automatically available.

Feinberg, Kasyanov and Zadoianchuk (2012) proved that under their Assumptions W* and B the weaker average-cost optimality inequality (ACOI) holds. For setwise continuous transition probabilities, Hernández-Lerma and Lasserre (1996, Theorem 5.5.4) gave conditions for the ACOE via equicontinuity. Feinberg and Lewis (2015) established the ACOI and optimality of $(s,S)$ policies for periodic-review inventory control with setup costs and general demand. Feinberg and Liang (2022, online 2017) extended the equicontinuity condition to weakly continuous transitions and used it to show that the inventory problem satisfies the full equation, not just the inequality.

Setting

An MDP has a state space $\mathbb X$ and an action space $\mathbb A$ (Borel subsets of Polish spaces). It has a one-step cost $c:\mathbb X\times\mathbb A\to\mathbb R\cup\{+\infty\}$ , bounded below, and a transition probability $q(dy\mid x,a)$ . A policy chooses actions from the observed history, possibly at random. A stationary policy is a measurable map $\phi:\mathbb X\to\mathbb A$ . For a discount factor $\alpha\in[0,1)$ :

$v_\alpha(x)$ is the infimum over all policies of the expected total discounted cost from $x$ ;
$m_\alpha=\inf_x v_\alpha(x)$ ;
$u_\alpha=v_\alpha-m_\alpha$ is the discounted relative value function.

The average cost of a policy is $w^\pi(x)=\limsup_N \frac1N\mathbb E^\pi_x\sum_{t<N}c(x_t,a_t)$ , and $w(x)=\inf_\pi w^\pi(x)$ . Set $\underline w=\liminf_{\alpha\uparrow1}(1-\alpha)m_\alpha$ . For a sequence $\alpha_n\uparrow1$ , define

\tilde u(x)=\liminf_{n\to\infty,\ y\to x}u_{\alpha_n}(y).

Assumption EC for $\{\alpha_n\}$ has two parts:

the family $\{u_{\alpha_n}\}$ is equicontinuous;
some measurable $U\ge u_{\alpha_n}$ has $\int U\,dq(\cdot\mid x,a)<\infty$ for all $x,a$ .

The inventory problem has inventory level $x\in\mathbb R$ (negative means backlog) and order quantity $a\ge0$ . Inventory evolves by $x_{t+1}=x_t+a_t-D_{t+1}$ , with i.i.d. nonnegative demands $D$ . The cost is

c(x,a)=K\,I_{\{a>0\}}+\bar c\,a+\mathbb E[h(x+a-D)],

with setup cost $K\ge0$ , unit cost $\bar c>0$ , and convex $h$ with $h(x)\to\infty$ as $|x|\to\infty$ . Let $\alpha^*=1+\lim_{x\to-\infty}h(x)/(\bar cx)$ and $H(x)=\bar cx+\mathbb E[h(x-D)]+\mathbb E[\tilde u(x-D)]$ . A function $f$ is $K$ -convex if $f((1-\lambda)x+\lambda y)\le(1-\lambda)f(x)+\lambda f(y)+\lambda K$ for $x\le y$ and $\lambda\in(0,1)$ . An $(s,S)$ policy orders up to $S$ whenever the inventory is below $s$ .

Formalization targets

Goal: Theorem 4.5

For every sequence of nonnegative discount factors $\alpha_n\uparrow1$ with $\alpha_1>\alpha^*$ , the inventory MDP satisfies Assumption EC. Along a subsequence, $u_{\alpha_{n_k}}\to\tilde u$ , and some stationary $\phi$ satisfies

w+\tilde u(x)=K I_{\{\phi(x)>0\}}+H(x+\phi(x))-\bar cx=\min\Big\{\min_{a\ge0}[K+H(x+a)],\,H(x)\Big\}-\bar cx .

Moreover:

$\tilde u$ and $H$ are $K$ -convex, continuous and inf-compact;
the $(s,S)$ policy built from a minimizer of $H$ satisfies the equation;
so do the limits $(s^*,S^*)$ of discount-optimal thresholds.

Milestones

Lemma 3.3: for equicontinuous families, the pointwise and joint lower limits coincide.
Theorem 3.2: Assumptions W*, B and EC imply the ACOE for a general MDP.
The cited facts used in §4:
- Assumptions W* and B hold for the inventory problem;
- the sets $\mathbb X_\alpha$ of minimizers of $v_\alpha$ lie in a bounded interval (4.4);
- discount-optimal $(s_\alpha,S_\alpha)$ policies (Theorem 4.3);
- their average-cost limits (Theorem 4.4);
- the renewal bounds (4.11)–(4.12).
Lemma 4.6: an explicit dominating function $U$ .
Lemma 4.7: equicontinuity of $\{u_{\alpha_n}\}$ for the inventory problem.

Significance

The ACOE is stronger than the ACOI. It identifies the optimal actions of an average-cost problem as the minimizers of a one-step lookahead with $\tilde u$ , and it makes $\tilde u$ a genuine relative value function: $\tilde u$ is the pointwise limit of the discounted relative values along a subsequence. For inventory control, Theorem 4.5 gives three further conclusions:

the $K$ -convexity and continuity of the average-cost relative value function;
that an optimal $(s,S)$ policy can be computed from $H$ by the same argmin rule that works for discounted costs;
that limits of discount-optimal thresholds solve the average-cost problem.

The results are proved in the paper, and in the cited works of Feinberg and coauthors for the cited milestones. None is formalized. There is no formal library of MDPs on Borel spaces with history-dependent randomized policies. This mission builds that layer (strategic measures via Ionescu Tulcea, discounted and average costs, Assumptions W*, B and EC) and states the general ACOE theorem on it. A proof of the goal would also require formal proofs of the cited inventory results of Feinberg–Lewis (2015) and Feinberg–Liang (2017a), which are milestones here.

Difficulty

One obvious route is to pass to the limit in the discounted optimality equation $v_\alpha=\min_a[c+\alpha\int v_\alpha\,dq]$ . After subtracting $m_\alpha$ , this needs two things: convergence of $u_{\alpha_n}$ , and exchanging limit and integral. Pointwise lower limits give only the inequality (ACOI). The reverse inequality needs actual convergence of a subsequence and a dominating function. For weakly continuous $q$ , convergence of $\int u_{\alpha_n}\,dq$ additionally requires uniform convergence on compacts, which is where equicontinuity enters.

For the inventory problem the hard step is equicontinuity itself. The functions $u_\alpha$ are not uniformly Lipschitz. It must be shown that costs from two nearby starting inventories stay close uniformly in $\alpha$ . This comparison runs through the time until inventory falls below the reorder point, and it is controlled by renewal-theoretic bounds on the number of demand arrivals.

Formalization scope

The Lean development lives in the namespace FeinbergLiang.ACOE. It commits to the following conventions.

Spaces. $\mathbb X,\mathbb A$ are separable metric spaces with standard Borel σ-algebras. This is the paper's "Borel subsets of Polish spaces", up to homeomorphism. The inventory case is $\mathbb X=\mathbb R$ , $\mathbb A=\mathbb R_{\ge0}$ . The integer case $\mathbb X=\mathbb Z$ , $\mathbb A=\mathbb N_0$ is out of scope, as are Corollary 4.8 and Theorem 4.9.
Costs and infinities. The cost is stored as a real lower bound plus a $[0,\infty]$ -valued part. Every value function ( $v_\alpha$ , $m_\alpha$ , $u_\alpha$ , $w$ , $\underline w$ , $\tilde u$ ) is the $[0,\infty]$ -valued part, with the explicit real shift described in the definitions. $u_\alpha$ equals $v_\alpha-m_\alpha$ whenever $m_\alpha<\infty$ , which Assumption B guarantees. $\alpha^*$ is an extended real and may be $-\infty$ . $G_\alpha$ and $H$ are extended-real valued, and each theorem using them concludes their finiteness. Likewise the ACOE conclusions include $\underline w<\infty$ and $\tilde u<\infty$ , so an equation of the form $\infty=\infty$ can never satisfy them.
Policies. $v_\alpha$ and $w$ are infima over all history-dependent randomized policies, with trajectory laws given by Mathlib's Ionescu Tulcea kernel Kernel.trajMeasure. They are never defined as solutions of an optimality equation.
Readings of informal words.
1. " $\alpha_n\uparrow1$ " means values in $[0,1)$ , nondecreasing, with limit $1$ ; "nonnegative discount factors" is the lower end of $[0,1)$ .
2. The paper's $\alpha_1$ is Lean's α 0.
3. "Equicontinuous" is Mathlib's Equicontinuous, applied to the real values of $u_{\alpha_n}$ together with their finiteness.
4. " $\liminf_{n\to\infty,y\to x}$ " is the lower limit along the product filter atTop ×ˢ 𝓝 x.
5. "Uniform on each compact subset" is TendstoUniformlyOn on every compact set.
6. " $=\min$ " in (3.3) and (4.10) means the middle term is attained and is a lower bound for all actions.
7. "Assumption EC for the sequence" is a property of a given sequence.
8. "Can be selected as an $(s^*,S^*)$ policy" is stated for every limit of discount-optimal thresholds along a further subsequence, with $\tilde u$ that of Theorem 3.2(i).
9. "Can be selected as an $(s,S)$ policy" is stated for every minimizer $S$ of $H$ .
10. Theorem 4.4's "optimality inequality (4.8)" is read as the ACOI (3.1) for the $(s^*,S^*)$ policy.
Standing assumptions. The paper's "without loss of generality $h\ge0$ and $h(0)=0$ " is a pair of hypotheses of the inventory model. This is the paper's normalization, not an addition.
Not trivializable. Defining $v_\alpha$ through its optimality equation, restricting policies to stationary ones, or dropping the finiteness conclusions would make the goal a different, weaker statement. The definitions rule each of these out.

Contributions welcome: proofs of the milestones, especially the general Theorem 3.2 and the renewal estimates behind Lemmas 4.6–4.7. The Borel-space MDP definitions are reusable by later average-cost and discounted MDP missions.

Selected references

E. A. Feinberg and Y. Liang, On the optimality equation for average cost Markov decision processes and its validity for inventory control, Annals of Operations Research 317 (2022) 569–586. https://doi.org/10.1007/s10479-017-2561-9
E. A. Feinberg, P. O. Kasyanov and N. V. Zadoianchuk, Average cost Markov decision processes with weakly continuous transition probability, Mathematics of Operations Research 37(4) (2012) 591–607. https://doi.org/10.1287/moor.1120.0555
E. A. Feinberg and M. E. Lewis, On the convergence of optimal actions for Markov decision processes and the optimality of (s, S) policies for inventory control, preprint arXiv:1507.05125, 2015. https://arxiv.org/abs/1507.05125
E. A. Feinberg and Y. Liang, Structure of optimal policies to periodic-review inventory models with convex costs and backorders for all values of discount factors, Annals of Operations Research (2017a). https://doi.org/10.1007/s10479-017-2548-6
O. Hernández-Lerma and J. B. Lasserre, Discrete-Time Markov Control Processes: Basic Optimality Criteria, Springer, 1996. https://doi.org/10.1007/978-1-4612-0729-0

12 thms2 active usersReviewed

Combinatorics Graph Theory Linear Optimization·Captain: mikedeng1

Optimum Branchings: The Vertices of the Branching Polyhedron Are Exactly the BranchingsResearch Paper

Motivation

A branching in a directed graph is a set of edges that contains no cycle (even ignoring directions) and in which no two edges point to the same node; a connected branching is an arborescence, a tree rooted at one node with all edges directed away from the root. The optimum branching problem asks, for real weights on the edges, for a branching of maximum total weight. It contains the minimum-cost spanning arborescence problem (the directed analogue of the minimum spanning tree), which appears in network design, in the analysis of broadcast and routing structures, in phylogenetics, and in dependency parsing in computational linguistics, where maximum spanning arborescences are the standard decoding step of graph-based parsers.

J. Edmonds solved the problem in Optimum branchings (J. Res. Nat. Bur. Standards 71B (1967) 233–240). The paper gives an algorithm (the shrinking algorithm usually attributed to Chu–Liu and Edmonds) and, proved together with it, a polyhedral theorem: the linear system that every branching obviously satisfies has no other vertices. This was one of the first integral polyhedron theorems beyond bipartite matching and network flows, and together with Edmonds' matching polytope (1965) it set the pattern of polyhedral combinatorics: describe the convex hull of the combinatorial objects by linear inequalities, and prove optimality by a linear programming dual.

Timeline:

1965: Y. J. Chu and T. H. Liu describe the shrinking algorithm for the maximum arborescence.
1965: Edmonds, Paths, trees, and flowers and Maximum matching and a polyhedron with 0,1-vertices: the matching polytope.
1967: Edmonds, Optimum branchings: the algorithm, Theorem 2 (vertices of the branching polyhedron), and the dual certificate built along the algorithm.
1970–1971: Edmonds' matroid intersection theorem, which contains the branching polyhedron theorem as the intersection of a graphic matroid and a partition matroid.
1977–1986: faster implementations (Tarjan; Gabow, Galil, Spencer and Tarjan).

Setting

A graph $G$ consists of a finite set $V$ of nodes and a finite set $E$ of edges. Each edge $e$ is directed toward a node $\mathrm{front}(e)$ , its front end, and away from a different node $\mathrm{rear}(e)$ , its rear end. Parallel edges are allowed; loops are not.

For $F\subseteq E$ , a node $v$ meets $k$ edges of $F$ if $\#\{e\in F:\mathrm{front}(e)=v\}+\#\{e\in F:\mathrm{rear}(e)=v\}=k$ . A set $B\subseteq E$ is a forest if it contains no polygon, i.e. no nonempty $F\subseteq B$ in which every node meets zero or two edges of $F$ ; it is a branching if in addition distinct edges of $B$ have distinct front ends. The incidence vector $x^B\in\mathbb R^E$ of $B$ has $x^B_e=1$ for $e\in B$ and $0$ otherwise.

The branching polyhedron $P_G\subseteq\mathbb R^E$ is the set of $x$ with

$(L_1)$ $x_e\ge0$ for every edge $e$ ;
$(L_2)$ $\sum_{e:\,\mathrm{front}(e)=v}x_e\le1$ for every node $v$ ;
$(L_3)$ $\sum_{e:\,\mathrm{front}(e),\mathrm{rear}(e)\in S}x_e\le|S|-1$ for every set $S$ of two or more nodes.

A vertex of a set $P\subseteq\mathbb R^E$ is a point of $P$ that is the unique maximizer over $P$ of some linear function $x\mapsto\sum_e c_ex_e$ .

For weights $c\in\mathbb R^E$ , the dual variables are $y_h$ for each node $v_h$ and $y_S$ for each $S$ with $|S|\ge2$ ; write $w_e=\sum_{S\ni\mathrm{front}(e),\mathrm{rear}(e)}y_S$ and $(b,y)=\sum_hy_h+\sum_S(|S|-1)y_S$ . Edmonds' conditions are (15) $y_h\ge0$ , (16) $y_S\ge0$ , (17) $y_{\mathrm{front}(e)}+w_e\ge c_e$ for every edge, and, for a branching $B$ , (18) $y_h\ne0\Rightarrow$ some edge of $B$ enters $v_h$ , (19) $y_S\ne0\Rightarrow$ exactly $|S|-1$ edges of $B$ lie inside $S$ , (20) $y_{\mathrm{front}(e)}+w_e=c_e$ for $e\in B$ .

Formalization targets

Goal: Theorem 2 (p. 235)

\{x:\ x\text{ is a vertex of }P_G\}\;=\;\{x^B:\ B\text{ is a branching of }G\}.

Both inclusions, for every finite loopless directed multigraph.

Milestones

§5, p. 236: for every branching $B$ , $x^B\in P_G$ .
§5, p. 236: for every branching $B$ , $x^B$ is a vertex of $P_G$ .
§6, (12)–(14): if $B$ is a branching and $y$ satisfies (15)–(20), then $(c,x^B)=(b,y)$ , $x^B$ maximizes $(c,x)$ over $P_G$ , and $y$ minimizes $(b,y)$ subject to (15)–(17).
§7, p. 237: for every $c\in\mathbb R^E$ there are a branching $B$ and a $y$ satisfying (15)–(20).
Lemma 1, p. 236: for every $c\in\mathbb R^E$ some branching vector lies in $P_G$ and maximizes $\sum_ec_ex_e$ over $P_G$ .

Significance

Theorem 2 says that the linear program $\max\{(c,x):x\in P_G\}$ always has an optimal solution that is a branching, and that every vertex of $P_G$ is one. Consequently optimum branchings, and after the reductions of the paper's §2 optimum spanning and rooted arborescences, can be computed by linear programming, and their optimality is certified by a dual vector satisfying (15)–(20). The same statement underlies the separation-based treatment of arborescence constraints in integer programming formulations of network design and of the asymmetric travelling salesman problem. The integrality of the dual for integer weights (the paper's §8) yields min–max theorems of König type for branchings.

The result is proved and classical; no machine-checked proof of it in a proof assistant is known. The mission asks for the paper's own proof chain: branching vectors are points and vertices of $P_G$ , linear programming optimality from complementary slackness, existence of a dual certificate for every weight vector, and the deduction of Theorem 2. Proofs through matroid intersection or total dual integrality would also establish the goal and are welcome as alternative routes.

Difficulty

The inclusion "branching vectors are vertices" and the certificate criterion are short. The substance is Milestone 4: for arbitrary real weights, a branching and a dual vector satisfying the complementary slackness conditions must exist simultaneously. Finiteness gives an optimum branching at once, but that says nothing about optimality over the fractional points of $P_G$ ; the difficulty is the dual. The natural attempt, taking $y_S=0$ for all sets and $y_h$ the largest positive weight entering $v_h$ , violates (20) as soon as the greedy choice closes a circuit: the $(L_3)$ duals of nested node sets, arising from repeatedly shrinking circuits, are needed, and they must be kept nonnegative through weight changes of the form $c_3+c_0-c_4$ on edges entering a shrunk circuit.

Formalization scope

A graph is a structure Graph V E with front rear : E → V and a proof that front e ≠ rear e; V and E carry Fintype and DecidableEq. Edge sets are Finset E; vectors are E → ℝ; the linear function with weights c is ∑ e, c e * x e. A branching is defined combinatorially (no nonempty edge subset in which every node meets zero or two edges, and distinct front ends), never by counting edges inside node sets, and $P_G$ is the solution set of $(L_1)$ – $(L_3)$ , never a convex hull; either shortcut would make half of Theorem 2 true by definition. A vertex is a unique maximizer of a linear function, as on p. 236 (Mathlib's Set.exposedPoints has the same content); the set variables of the dual are a function Finset V → ℝ whose values on sets of fewer than two nodes are ignored. The right side of $(L_3)$ is the real number $|S|-1$ .

Implicit conventions made explicit: the no-loop condition is part of the graph (with a loop $e$ , the vector of $\{e\}$ is a vertex of $P_G$ but not a branching); parallel edges are allowed; weights have arbitrary sign and the empty branching is allowed. The mission does not model the algorithm of §4 or Theorem 1's notion of a "good" algorithm; Milestone 4 states only the existence of a certificate, which is what Lemma 1 uses.

Useful reusable infrastructure: finite directed multigraphs with an edge type, forests via polygons, and a finite LP duality lemma for $\max\{c^\top x: x\ge0,\ Ax\le b\}$ ; contributions of either are welcome.

Selected references

J. Edmonds, Optimum branchings, J. Res. Nat. Bur. Standards Sect. B 71B (1967), 233–240. https://doi.org/10.6028/jres.071b.032
Y. J. Chu and T. H. Liu, On the shortest arborescence of a directed graph, Scientia Sinica 14 (1965), 1396–1400.
J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
R. E. Tarjan, Finding optimum branchings, Networks 7 (1977), 25–35. https://doi.org/10.1002/net.3230070103
H. N. Gabow, Z. Galil, T. Spencer and R. E. Tarjan, Efficient algorithms for finding minimum spanning trees in undirected and directed graphs, Combinatorica 6 (1986), 109–122. https://doi.org/10.1007/BF02579168
A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer (2003), Chapter 52.

9 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning Probability·Captain: mikedeng1

Stochastic Linear Optimization under Bandit Feedback 2: A Regret Lower Bound on the CircleResearch Paper

Motivation

In stochastic linear optimization under bandit feedback a learner repeatedly chooses a point $x_t$ from a compact decision set $D\subset\mathbb R^n$ and observes only the random cost $\ell_t$ of that point, whose mean is $\mu\cdot x_t$ for an unknown vector $\mu$ . The problem models online routing, ad placement and other sequential decisions with linearly structured costs. The quality of a learner is measured by its regret against the best fixed decision.

For the $K$ -armed bandit the achievable regret for a fixed instance is logarithmic in the horizon $T$ (Lai and Robbins 1985; Auer, Cesa-Bianchi and Fischer 2002). Dani, Hayes and Kakade (COLT 2008) showed that for linear costs the picture depends on the geometry of $D$ . Their Theorem 1 gives polylogarithmic regret when the decision set has a positive gap between the best and second-best extreme point (a polytope, for instance), and their Theorem 2 gives $O^*(n\sqrt T)$ regret for every decision set. Their Theorem 3 shows that the second rate cannot be improved in general: on a decision set with zero gap, every algorithm pays $\Omega(\sqrt T)$ in expectation.

Timeline:

2002: Auer, Using confidence bounds for exploitation–exploration trade-offs (JMLR 3), introduces confidence-bound algorithms for linear bandits on finite decision sets.
2008: Dani, Hayes and Kakade prove the $O^*(n\sqrt T)$ upper bound for ConfidenceBall₂ and the $\Omega(\sqrt T)$ lower bound on a product of circles, the subject of this mission. A hypercube lower bound for the adversarial setting appears in their NIPS 2007 paper.
2010: Rusmevichientong and Tsitsiklis, Linearly parameterized bandits (Math. OR 35), give $\Omega(n\sqrt T)$ lower bounds on the unit sphere.
2020: Lattimore and Szepesvári, Bandit Algorithms, Theorems 24.1 and 24.2, give minimax lower bounds on the hypercube and the unit ball with Gaussian noise.

Setting

The decision set is the unit circle $D_2=S^1=\{x\in\mathbb R^2: x_1^2+x_2^2=1\}$ . An unknown mean vector $\mu\in\mathbb R^2$ is drawn once, uniformly from the circle $D_2/2$ of radius $1/2$ ; concretely $\mu=\mu(\theta)=\tfrac12(\cos\theta,\sin\theta)$ with $\theta$ uniform on $[0,2\pi)$ .

On each round $t=1,\dots,T$ the algorithm plays $x_t\in D_2$ and observes a cost $\ell_t\in\{-1,+1\}$ with $\Pr(\ell_t=+1)=(1+\mu\cdot x_t)/2$ , so that $\mathbb E[\ell_t]=\mu\cdot x_t$ . Given the decision, the cost is independent of the past.

An algorithm may be randomised. It draws a seed $s$ once from a probability measure $\rho$ on a measurable space $S$ , and chooses $x_t$ as a function of $s$ and the costs $\ell_1,\dots,\ell_{t-1}$ observed so far, measurably in $s$ .

The regret over $T$ rounds is

R=\sum_{t=1}^T(\mu\cdot x_t-\mu\cdot x^*),\qquad \mu\cdot x^*=\min_{x\in D_2}\mu\cdot x,

so each round costs $r_t=\mu\cdot x_t+\tfrac12\ge0$ when $\|\mu\|=1/2$ . The expected regret $\mathbb E R=\mathbb E_\mu\,\mathbb E(R\mid\mu)$ averages over the seed, the prior and the costs.

In the Lean development these objects are unitCircle, meanVec, optCost, RandomizedPolicy and expectedRegret in the namespace StochLinOpt.LowerBound.

Formalization targets

Goal: Theorem 3 for $n=2$

There is a universal constant $c>0$ such that for every randomised algorithm and every $T\ge1$ ,

\mathbb E R\ \ge\ c\sqrt T.

The constant is left existential, which is the form that survives any later improvement of the constant; it is chosen before the algorithm and before $T$ .

Milestones

Section 6.1, Eq. (3). For $\|\mu_1\|=\|\mu_2\|=1/2$ , $x\in S^1$ , a posterior probability $p\in[0,1]$ of $\mu=\mu_1$ and a cost $\ell\in\{\pm1\}$ , the Bayes-updated bias $b_{t+1}$ satisfies $|b_{t+1}-b_t|\le|(\mu_1-\mu_2)\cdot x|$ , where $b_t=2p-1$ .
Lemma 15. With $\varepsilon=\|\mu_1-\mu_2\|>0$ and the same data,

\mathbb E_\mu(r_t\mid\mathcal H_t)\ge\frac1{16}\Big(\varepsilon^2+\frac{|b_{t+1}-b_t|^2}{\varepsilon^2}\Big)\mathbf 1\{|b_t|\le1/2\}.

Theorem 4 (Freedman). For a martingale difference sequence $X_1,\dots,X_T$ bounded above by $b$ , with conditional variance sum $V$ , and all $a,v>0$ ,

\Pr\Big(\sum_i X_i\ge a,\ V\le v\Big)\le\exp\Big(\frac{-a^2}{2v+2ab/3}\Big).

Significance

The lower bound shows that the $\sqrt T$ dependence of the problem-independent upper bound (Theorem 2 of the same paper) is necessary. It also shows that the gap-dependent polylogarithmic rate of Theorem 1 cannot extend to decision sets without a gap, such as the sphere. Together with the upper bound it characterises the minimax regret of stochastic linear bandits in $T$ up to logarithmic factors, and in the paper's general- $n$ form it also underlies the claim that the price of bandit information is $\Theta^*(\sqrt n)$ .

The result is proved in the paper for $n=2$ and has not been machine-checked. The mission produces a checked Bayesian lower bound over all randomised algorithms, with an explicit probability model for the protocol. Two related platform results are different theorems: BanditAlgorithm.linear_bandit_unit_ball_minimax_lower_bound (Lattimore–Szepesvári Theorem 24.2: unit ball, Gaussian noise, a worst-case $\mu$ ) and BanditAlgorithm.linear_bandit_hypercube_minimax_lower_bound (Theorem 24.1: hypercube). The $\{-1,+1\}$ costs, the circle and the uniform prior used here are not covered by either.

Difficulty

The obvious attempt is a two-point change-of-measure argument with a fixed pair of means at distance $\varepsilon$ . It fails as stated because the decision set has no gap: an algorithm that plays close to the optimum of both candidates learns slowly but also pays little. The per-round trade-off between regret and information (Lemma 15) is exact only while the posterior is undecided, $|b_t|\le1/2$ . Turning it into a bound on the whole horizon requires controlling how long the posterior stays undecided, which is a statement about a martingale whose step sizes are chosen by the algorithm; a concentration bound that ignores the accumulated conditional variance (Azuma–Hoeffding with worst-case steps) is too weak for this. The averaging step from a two-point prior to the uniform prior on the circle is also part of the formal work.

Formalization scope

Vectors are Fin 2 → ℝ with the dot product ⬝ᵥ; Euclidean norms are written through dot products, never with Lean's sup norm. Rounds are 0-indexed internally: the Lean index $t$ is the paper's round $t+1$ . The expected regret is the exact finite expectation

\mathbb E R=\int_S\frac1{2\pi}\int_0^{2\pi}\sum_{\ell\in\{\pm1\}^T}\prod_{t=1}^T\frac{1+\ell_t\,\mu(\theta)\cdot x_t}{2}\;R\;d\theta\,d\rho(s),

so no infinite product of measures is needed. A randomised algorithm is a seeded policy, which covers every randomised algorithm. The optimal cost is the infimum of $\mu\cdot x$ over the compact circle and is attained. Every junk value in the model (a non-integrable integrand) could only make the lower bound harder to prove, never easier.

A statement over deterministic algorithms only, over a worst-case $\mu$ instead of the uniform prior, or with the constant allowed to depend on the algorithm or on $T$ would be a weaker theorem. The goal quantifies $\exists c>0$ before the algorithm and $T$ , and fixes the prior.

Corrections relative to the printed paper:

General $n$ is not stated. Theorem 3 as printed claims $\mathbb E R\ge\frac1{10}n\sqrt T$ for every even $n$ . It is false for $n>10$ : on $D_n$ with $\mu\in D_n/n$ each round has regret at most $1$ , so at $T=1$ the claim would need $\mathbb E R\ge n/10>1$ . The general case rests on Lemma 16, which has no proof. The goal is the $n=2$ case, which Section 6.1 proves.
The constant. For $n=2$ the paper prints $\frac15\sqrt T$ ; its proof gives $c=\frac1{16}\min(\frac12-\frac1e,\frac1{64})=\frac1{1024}$ . The proof's Freedman step prints $2\exp(-\frac{1/4}{1/8+\varepsilon/3})\le 2/e^2$ ; with $v=1/32$ the denominator is $1/16+\varepsilon/3$ , and the bound $2/e^2$ then needs $\varepsilon=T^{-1/4}\le3/16$ . Small $T$ is covered by the first round, whose expected regret is $1/2$ . The goal leaves $c$ existential.
Theorem 4. The printed variance sum runs to $n$ ; it runs to $T$ . The conditioning is on a general filtration, and square-integrability of the steps is assumed so that the conditional variance is defined.
Lemma 15. Its right side depends on the round- $t$ cost $\ell_t$ , which is not part of $\mathcal H_t$ ; the Lean statement holds for either value of $\ell_t$ .

Welcome contributions: a Lean proof of Freedman's inequality (reusable across the bandit and concentration missions on the platform); the averaging argument from two-point priors to the uniform prior; and the stopped-martingale bookkeeping for the bias sequence.

Selected references

Varsha Dani, Thomas P. Hayes, Sham M. Kakade, Stochastic Linear Optimization under Bandit Feedback, Proceedings of the 21st Annual Conference on Learning Theory (COLT), 2008.
David A. Freedman, On tail probabilities for martingales, The Annals of Probability 3(1):100–118, 1975. https://doi.org/10.1214/aop/1176996452
Colin McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer, 1998. https://doi.org/10.1007/978-3-662-12788-9_6
Peter Auer, Using confidence bounds for exploitation–exploration trade-offs, JMLR 3:397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
Paat Rusmevichientong, John N. Tsitsiklis, Linearly parameterized bandits, Mathematics of Operations Research 35(2):395–411, 2010. https://doi.org/10.1287/moor.1100.0446
Tor Lattimore, Csaba Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 24. https://doi.org/10.1017/9781108571401

5 thms2 active usersReviewed

Combinatorics Graph Theory Linear Optimization·Captain: mikedeng1

On Certain Polytopes Associated with Graphs V: Zero-One Optima of the Odd-Cycle Relaxation on Series-Parallel GraphsResearch Paper

Motivation

The stable set problem asks for a largest set of pairwise non-adjacent vertices in a graph; its size is the stability number $\alpha(G)$ . It is NP-hard in general, and a standard way to attack it in integer programming is to write down linear inequalities valid for all stable sets and solve the resulting linear program. The weakest such relaxation uses only the edge inequalities $x_v+x_w\le 1$ ; its optimum can be as large as $|V|/2$ on graphs with small $\alpha(G)$ . Adding, for every odd circuit $C$ , the inequality $\sum_{u\in C}x_u\le\frac12(|C|-1)$ gives the odd-cycle relaxation, the first strengthening that cuts off the fractional point $x\equiv\frac12$ on odd cycles.

Section 7 of V. Chvátal, On certain polytopes associated with graphs (J. Combin. Theory Ser. B 18 (1975) 138–154, doi:10.1016/0095-8956(75)90041-6) identifies a graph class on which this relaxation is exact for the all-ones objective, with an integral certificate on the dual side: the series-parallel networks. The paper conjectures (Conjecture 7.3) that for these graphs the odd-cycle inequalities describe the whole stable set polytope; graphs with that property were later called t-perfect.

Timeline:

1960: G. A. Dirac, in "In abstrakten Graphen vorhandene vollständige 4-Graphen und ihre Unterteilungen" (Math. Nachr. 22), proves that graphs containing no subdivided $K_4$ have at least two vertices of degree at most two.
1975: Chvátal introduces the system (7.1) and proves Theorem 7.1 (this mission): on series-parallel networks, $\max\sum_u x_u$ subject to (7.1) and its dual both have zero–one optima. He conjectures the full polyhedral statement.
1979: M. Boulala and J.-P. Uhry, "Polytope des indépendants d'un graphe série-parallèle" (Discrete Math. 27), prove the conjecture: (7.1) defines the stable set polytope of every series-parallel graph.
1986: A. M. H. Gerards and A. Schrijver, "Matrices with the Edmonds–Johnson property" (Combinatorica 6), extend this to graphs with no odd- $K_4$ subdivision.

Setting

All graphs $G=(V,E)$ are finite, undirected and loopless, with no parallel edges. A stable set is a set of vertices no two of which are adjacent. We write $d(u)$ for the degree of $u$ .

A set $C\subseteq V$ induces an odd circuit if the induced subgraph $G[C]$ is a cycle of length $2k+1$ with $k\ge1$ ; triangles count, and such a cycle has no chords. $Z(G)$ is the set of all such $C$ . The odd-cycle system of $G$ is

\begin{aligned} 0\le x_u&\le 1 && (u\in V),\\ x_v+x_w&\le 1 && (vw\in E),\\ \textstyle\sum_{u\in C}x_u&\le \tfrac12(|C|-1) && (C\in Z(G)). \end{aligned}\tag{7.1}

Its linear programming dual for the objective $\sum_u x_u$ , with $x\ge0$ read as sign constraints, has variables $y_u\ge0$ , $z_e\ge0$ , $w_C\ge0$ and reads

\min\ \sum_{u}y_u+\sum_{e}z_e+\sum_{C\in Z(G)}\tfrac12(|C|-1)\,w_C\quad\text{s.t.}\quad y_u+\sum_{e\ni u}z_e+\sum_{C\ni u}w_C\ge 1\ \ (u\in V).

A homeomorph of $K_4$ is a graph obtained from $K_4$ by subdividing its edges into paths through new vertices of degree two. $G$ is a series-parallel network if no subgraph of $G$ is a homeomorph of $K_4$ .

Formalization targets

Goal: Theorem 7.1

For every series-parallel network $G$ ,

\exists\,x\in\{0,1\}^V\ \text{feasible for (7.1)}:\ \ \sum_u x_u=\max\Big\{\sum_u x'_u : x'\in\mathbb R^V\text{ satisfies (7.1)}\Big\},

and there is a zero–one dual feasible $(y,z,w)$ whose dual objective equals the minimum over all real dual feasible points. Both optimality claims are against real points. Chvátal's statement has no constants to improve; the formal goal is his theorem as printed.

Milestones

Dirac's theorem (§7, p. 150): a series-parallel network with at least two vertices has two distinct vertices of degree at most two.
Case 4 closure (p. 151): if $d(u)=2$ and the neighbours $v,w$ of $u$ are non-adjacent, deleting $u$ and identifying $v$ with $w$ yields a series-parallel network.
The combinatorial core (p. 151, (i)–(ii)): there are a stable set $S$ and a spanning subgraph $F\le G$ whose components are isolated vertices, isolated edges and odd circuits, such that with $a$ isolated vertices, $b$ isolated edges and $c_k$ circuits of length $2k+1$ ,

a+b+\sum_k k\,c_k=|S|.

Significance

The result. Theorem 7.1 says that on series-parallel networks the odd-cycle relaxation computes $\alpha(G)$ exactly, and that the optimum is certified by a covering of the vertex set by single vertices, edges and chordless odd circuits whose total weight equals $|S|$ . This is a min–max theorem of König type for a non-bipartite, non-perfect class: odd cycles of length at least five are series-parallel and not perfect, so the clique inequalities of the perfect-graph theory (mission I of this series) do not suffice here. The statement is the unweighted case of the later polyhedral results of Boulala–Uhry and Gerards–Schrijver, and the combinatorial core (milestone 3) is the basis of a polynomial algorithm for $\alpha(G)$ on this class, as the paper remarks.

Formalizing it. The theorem has been proved since 1975; neither Mathlib nor the Prove2Me library contains a formal proof of it. A formal proof needs a working notion of graph subdivision (topological minor), which Mathlib does not have, Dirac's degree theorem, the induction of the paper with its four cases, and the passage from the combinatorial core to a pair of LP optima through weak duality. Each of these is reusable: topological minors and the $K_4$ -subdivision-free class appear throughout structural graph theory.

Difficulty

The combinatorial core is proved by induction on $|V|$ removing a vertex of degree at most two, and three of the four cases are routine. The obstacle is Case 4 ( $d(u)=2$ , neighbours non-adjacent): deleting $u$ alone loses the information needed to recover $S$ and $F$ , so the proof identifies the two neighbours. That requires the class to be closed under this identification, a statement about subdivisions that is not a local edge count, and a lifting of $(S',F')$ from the reduced graph with a case split on the component of $F'$ containing the merged vertex. A second gap is between $F$ and the dual: an odd-circuit component of $F$ may have chords in $G$ and so need not lie in $Z(G)$ , and the zero–one dual solution must be extracted from it. Finally, Dirac's theorem itself is the one place where the absence of $K_4$ subdivisions is used positively, and it is not a consequence of a degree-counting argument.

Formalization scope

Graphs are SimpleGraph V on a Fintype V with decidable equality and decidable adjacency. $Z(G)$ is a Finset (Finset V) whose members induce a subgraph isomorphic to Mathlib's cycleGraph (2k+1), $k\ge1$ . The dual variables are indexed by V, by the edge set G.edgeSet, and by the subtype of $Z(G)$ ; $x\ge0$ is a sign constraint with no dual variable. "Contains a homeomorph of $K_4$ " is encoded by four distinct branch vertices and six paths (Walk.IsPath) that avoid other branch vertices and meet only at common endpoints; it is not the $K_4$ -minor notion and not the series–parallel composition notion, whose equivalence with it is not part of the paper.

Conventions and implicit hypotheses made explicit:

Dirac's theorem is stated with $|V|\ge 2$ ; as printed it fails for graphs with fewer than two vertices.
In Case 4 the identified graph has vertex set $V\setminus\{u,w\}$ , with $v$ representing $v\equiv w$ ; parallel edges merge.
Optimality in the goal is against every real feasible point of each program. A statement comparing the zero–one points only with other zero–one points would reduce the primal half to $\alpha(G)\le\alpha(G)$ and is ruled out.
In milestone 3 the sum $a+b+\sum_k k c_k$ is written as a sum over the connected components of $F$ of $1$ (one or two vertices) or $(n-1)/2$ ( $n\ge3$ vertices).

Corollary 7.2 (stated without proof) and Conjecture 7.3 are not part of this mission. Contributions welcome: a general topological-minor library, Dirac's theorem, and a proof of the combinatorial core.

Selected references

V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
G. A. Dirac, In abstrakten Graphen vorhandene vollständige 4-Graphen und ihre Unterteilungen, Math. Nachr. 22 (1960) 61–85 (reference [6], Satz 5, of the paper).
R. J. Duffin, Topology of series-parallel networks, J. Math. Anal. Appl. 10 (1965) 303–318 (reference [7] of the paper).
M. Boulala, J.-P. Uhry, Polytope des indépendants d'un graphe série-parallèle, Discrete Math. 27 (1979) 225–243.
A. M. H. Gerards, A. Schrijver, Matrices with the Edmonds–Johnson property, Combinatorica 6 (1986) 365–379.

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization·Captain: mikedeng1

On Certain Polytopes Associated with Graphs IV: Adjacent Stable Sets on the Stable Set PolytopeResearch Paper

Motivation

Many combinatorial optimization problems are linear programs over a polytope whose vertices are the zero–one incidence vectors of the feasible objects: matchings, stable sets, spanning trees. The edges of such a polytope (pairs of vertices joined by a one-dimensional face) govern the behaviour of the simplex method and of local-search procedures, which move from vertex to vertex along edges: a pivot of the simplex method on a nondegenerate basis replaces a vertex by one of its neighbours.

In December 1971 M. L. Balinski asked when two matchings $M_1, M_2$ of a graph are neighbours on the matching polyhedron determined by Edmonds (Edmonds 1965). V. Chvátal answered a more general question in §6 of On certain polytopes associated with graphs (Chvátal 1975): he characterized the neighbours on the stable set polytope of an arbitrary graph. Since matchings of $G$ are the stable sets of the line graph $L(G)$ , Balinski's question is the special case of line graphs (Corollary 6.3 of the paper).

Setting

Let $G=(V,E)$ be a finite undirected loopless graph. A stable set is a set of vertices no two of which are adjacent. $S(G)$ denotes the set of all zero–one vectors $x=(x_u : u\in V)$ such that $\{u : x_u=1\}$ is stable, and the stable set polytope is

P(G)=\operatorname{conv} S(G)\subseteq \mathbb R^V .

For $y\in S(G)$ the corresponding stable set is $Y=\{u : y_u=1\}$ .

For an integer-valued vector $c=(c_u : u\in V)$ write $cx=\sum_{u\in V}c_ux_u$ . Two vectors $y, z$ are neighbours in $P(G)$ if there is an integer-valued $c$ such that $y$ and $z$ are the only two vectors which maximize $cx$ over $S(G)$ ; in particular $y\neq z$ . This is the definition the paper states at the start of the proof of Theorem 6.2.

A bicoloration of a graph $T$ is a partition $V=B\cup R$ , $B\cap R=\emptyset$ , such that every edge joins $B$ to $R$ . Every tree has one.

In the Lean development these objects are stableVectors G ( $S(G)$ ), stablePolytope G ( $P(G)$ ), onesSet y ( $Y$ ), AreNeighbors G y z and IsBicoloration T B R, all in the namespace ChvatalPolytopes.Neighbors.

Formalization targets

Goal: Theorem 6.2 (p. 149)

For $y,z\in S(G)$ with corresponding stable sets $Y,Z$ ,

y \text{ and } z \text{ are neighbours in } P(G) \iff \text{the subgraph } H \text{ of } G \text{ induced by } (Y-Z)\cup(Z-Y) \text{ is connected.}

Milestone: Lemma 6.1 (p. 149)

For a tree $T=(V,E)$ with a bicoloration $V=B\cup R$ there are nonnegative integers $c_u$ ( $u\in V$ ) and $m$ with

\sum_{u\in V}c_ux_u\le m\quad\text{for all } x\in S(T),

with equality exactly when $x$ is the incidence vector of $B$ or of $R$ .

Milestone: the certificate of the "if" part (p. 149, proof of Theorem 6.2, (i))

If $H$ is connected with spanning tree $T$ , and $c_u$ ( $u\in (Y-Z)\cup(Z-Y)$ ), $m$ are as in Lemma 6.1 for $T$ , extend $c$ by $c_u=1$ on $Y\cap Z$ and $c_u=-1$ outside $Y\cup Z$ . Then

\sum_{u\in V}c_ux_u\le m+|Y\cap Z|\quad\text{for all } x\in S(G),

with equality if and only if $x=y$ or $x=z$ .

Significance

Theorem 6.2 describes the 1-skeleton of the stable set polytope of every graph by a condition that can be checked in linear time, although optimizing over $P(G)$ is NP-hard in general and no complete linear description of $P(G)$ is known for general graphs. Through line graphs it gives the adjacency criterion for the matching polytope (two matchings are neighbours if and only if their symmetric difference is a single path or cycle), which settled Balinski's question. Characterizations of this type underlie the analysis of simplex-type and pivoting algorithms on combinatorial polytopes and the study of their diameters.

The result has been proved since 1975. The mission asks for a machine-checked proof of the theorem as stated in the paper; no formal proof of Theorem 6.2 or of the matching-polytope corollary is known to exist on Prove2Me or in Mathlib. The two milestones isolate the constructive half (Lemma 6.1 and the weighting built from it), which is reusable for any statement that needs an explicit objective singling out two stable sets.

Difficulty

The "only if" direction and the equality analysis are elementary; the substance lies in the "if" direction. An objective that makes both $y$ and $z$ optimal is easy to write down, for example $c=y+z$ ; the difficulty is to make them the only optimal vectors. Any stable set that agrees with $Y$ on some connected pieces of $H$ and with $Z$ on others ties with $y$ and $z$ under naive weightings, so the weights on $(Y-Z)\cup(Z-Y)$ must be chosen so that every mixed choice loses strictly. The integrality requirement on $c$ and the need to control all of $S(G)$ , not only the stable sets contained in $Y\cup Z$ , rule out a direct perturbation argument.

Formalization scope

Graphs. $V$ is a finite type with decidable equality and $G$ is a SimpleGraph V; loops and multiple edges are excluded, as in the paper.
$S(G)$ and $P(G)$ . $S(G)$ is the set of incidence vectors in V → ℝ of stable finsets; $P(G)$ is convexHull ℝ (S G).
Neighbours. Defined exactly as on p. 149: $y\ne z$ and, for some $c : V\to\mathbb Z$ , the set of maximizers of $cx$ over $S(G)$ equals $\{y,z\}$ . The face-lattice notion of an edge of $P(G)$ is not used; its equivalence with this definition is not part of the paper.
Induced subgraph and connectedness. $H$ is G.induce of the set $(Y\setminus Z)\cup(Z\setminus Y)$ , and "connected" is Mathlib's SimpleGraph.Connected, which requires at least one vertex. For $y=z$ both sides of the goal are therefore false.
Trees. SimpleGraph.IsTree, which includes connectedness; a spanning tree of $H$ is a graph $T$ on the vertex set of $H$ with $T\le H$ and T.IsTree. In Lemma 6.1 the integers $c_u$ and $m$ are natural numbers.

A trivializing formalization — defining neighbours through the symmetric-difference condition or through Lemma 6.1's certificate, or omitting $y\neq z$ from the definition — is excluded: neighbours are defined only through unique maximizers of integer objectives over $S(G)$ .

A complete development needs only finite graphs, induced subgraphs, spanning trees of connected graphs (available in Mathlib) and finite sums. Contributions welcome beyond the milestones: the equivalence of this notion of neighbours with the one-dimensional faces of $P(G)$ , and Corollary 6.3 for the matching polytope via line graphs.

Selected references

V. Chvátal, On certain polytopes associated with graphs, Journal of Combinatorial Theory, Series B 18 (1975), 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
M. W. Padberg, On the facial structure of set packing polyhedra, Mathematical Programming 5 (1973), 199–215. https://doi.org/10.1007/BF01580121

6 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization·Captain: mikedeng1

On Certain Polytopes Associated with Graphs II: No Clique Is a Cutset of a Connected α-Critical GraphResearch Paper

Motivation

The stability number $\alpha(G)$ of a graph, the largest number of pairwise non-adjacent vertices, is the optimum of an integer program over the stable set polytope $P(G)$ . Linear programming duality turns any explicit linear description of $P(G)$ into a certificate of optimality for $\alpha(G)$ , which is why the question "which inequalities are needed to describe $P(G)$ ?" has been central to polyhedral combinatorics since Edmonds' description of the matching polytope (Edmonds 1965). Chvátal's 1975 paper (doi:10.1016/0095-8956(75)90041-6) initiated the systematic study of $P(G)$ for arbitrary graphs: which graph operations preserve a known description, and which inequalities are facets, i.e. indispensable in every description.

Section 4 of the paper treats one such operation, gluing two graphs along a complete subgraph, and one family of facets, the "rank" inequality $\sum_u x_u\le\alpha(G)$ for graphs whose critical edges connect all vertices. Combining the two yields a purely graph-theoretic fact about $\alpha$ -critical graphs (graphs in which deleting any edge increases the stability number): no complete subgraph separates such a graph. The fact is due to Berge (Graphes et hypergraphes, 1970, Ch. 13, §3, Corollary 2); Chvátal's derivation obtains it from polyhedral arguments. $\alpha$ -critical graphs were studied by Erdős and Gallai, Hajnal, Andrásfai and Lovász, and their structure is closely tied to the facets of $P(G)$ .

Setting

Graphs are finite, undirected and loopless: $G=(V,E)$ . A stable set is a set of pairwise non-adjacent vertices; $\alpha(G)$ is the largest size of a stable set. The incidence vector of $s\subseteq V$ is $\chi^s\in\mathbb R^V$ with $\chi^s_u=1$ for $u\in s$ and $0$ otherwise. $S(G)$ is the set of incidence vectors of stable sets and

P(G)=\operatorname{conv}S(G)\subseteq\mathbb R^V .

A finite system $\sum_{u\in V}a_{iu}x_u\le b_i$ $(i\in J)$ is a defining linear system of $P$ if its solution set is exactly $P$ . An inequality $\sum_u a_ux_u\le b$ is a facet of $P$ if every defining linear system of $P$ contains, for some $t>0$ , the inequality $\sum_u ta_ux_u\le tb$ .

An edge $e$ of $G$ is critical if $\alpha(G-e)=\alpha(G)+1$ ; $E^*$ denotes the set of critical edges, $G^*=(V,E^*)$ , and $G$ is $\alpha$ -critical if every edge is critical. For graphs $G_1=(V_1,E_1)$ , $G_2=(V_2,E_2)$ put $G_1\cap G_2=(V_1\cap V_2,E_1\cap E_2)$ and $G_1\cup G_2=(V_1\cup V_2,E_1\cup E_2)$ . A vertex set $K$ is a cutset of $G$ if two vertices outside $K$ are joined by no path of $G-K$ , the subgraph induced on $V\setminus K$ .

In Lean, all objects live in the namespace ChvatalPolytopes.Separation: stablePolytope G, IsFacet P a b, IsCriticalEdge, criticalGraph G (for $G^*$ ), IsAlphaCritical G and IsCutset G K.

Formalization targets

Goal: Corollary 4.3 (p. 144)

For a finite connected $\alpha$ -critical graph $G$ and any $K\subseteq V$ inducing a complete subgraph,

K \text{ is not a cutset of } G .

The goal is pure graph theory; its proof in the paper consists of the two polyhedral theorems below.

Milestones

Proposition 2.1 (pp. 139–140). For a finite nonempty set $S$ of solutions of $-x_u\le0$ $(u\in V)$ , $\sum_u a_{iu}x_u\le b_i$ $(i\in J)$ : the solution set equals $\operatorname{conv}S$ if and only if for every $c\in\mathbb Z^V$

\max\{cx:x\in S\}=\min\Big\{\sum_i\lambda_ib_i:\lambda\ge0,\ \sum_i\lambda_ia_{iu}\ge c_u\ (u\in V)\Big\}.

Theorem 4.1 (p. 141). If $G_1\cap G_2$ is complete, the union of defining linear systems of $P(G_1)$ and $P(G_2)$ (each containing its nonnegativity rows) is a defining linear system of $P(G_1\cup G_2)$ .
Theorem 4.2 (p. 143). If $G^*$ is connected, then

\sum_{u\in V}x_u\le\alpha(G)

is a facet of $P(G)$ .

Significance

Theorem 4.1 says that clique-sums are harmless for linear descriptions of $P(G)$ : a description of a graph glued along a clique is the union of descriptions of the pieces. It underlies the later decomposition theory of stable set polytopes (clique cutsets appear throughout the study of perfect and $t$ -perfect graphs). Theorem 4.2 supplies a large class of facets with a combinatorial certificate, and was the starting point of the study of rank facets. Corollary 4.3 illustrates how polyhedral statements yield structural graph theory: the facet in Theorem 4.2 cannot coexist with a clique cutset.

All three results are proved in the paper, and Berge's corollary was known before it. None of them has, to the knowledge of this mission, a machine-checked proof; Mathlib has stable sets (IsIndepSet, indepNum), cliques and convex hulls, but no stable set polytope, no notion of facet via defining systems, and no $\alpha$ -critical graphs. The mission produces these definitions and the formal proofs of Proposition 2.1, Theorems 4.1, 4.2 and Corollary 4.3.

Difficulty

Proposition 2.1 requires LP duality in the form "min = max with both optima attained" together with a separation argument that reduces arbitrary objectives to integral ones; the "if" direction fails without the nonnegativity rows, so the statement is sensitive to the exact form of the system. In Theorem 4.1 the inclusion $P(G_1\cup G_2)\subseteq$ (solutions of the union) is routine; the difficulty is the converse: a point whose restrictions lie in $P(G_1)$ and in $P(G_2)$ is a convex combination of stable sets on each side, and the two combinations have to be matched on the clique $V_1\cap V_2$ to produce stable sets of $G_1\cup G_2$ . Theorem 4.2 concerns every defining linear system, so it cannot be proved by exhibiting one description; the natural route via "affinely independent tight points" is a different definition of facet and needs full-dimensionality of $P(G)$ to be equivalent. Finally, the goal requires translating a cutset into a decomposition $G=G_1\cup G_2$ with complete intersection, and then showing that a union of two systems on smaller vertex sets cannot contain a positive multiple of $\sum_{u\in V}x_u\le\alpha(G)$ .

Formalization scope

Graphs are SimpleGraph V on a Fintype V with DecidableEq V. $S(G)$ is a set of functions V → ℝ (incidence vectors of stable finsets), and $P(G)$ is convexHull ℝ (stableVectors G).
Linear systems are indexed by finite types with real coefficients. "Defining linear system" is equality of the solution set with the polytope. IsFacet quantifies over all finite index types J : Type and all real systems whose solution set equals the polytope; it is the paper's definition, not the affinely-independent-points characterization.
Proposition 2.1: "min = max" means an attained minimum equal to the maximum; the hypothesis $S\neq\emptyset$ is added (the paper's $\max$ over $S$ needs it), and the nonnegativity rows are kept.
Theorem 4.1: the glued graph $G$ lives on a type $V$ with finsets $V_1\cup V_2=V$ ; $G_1,G_2$ are the induced subgraphs on $V_1,V_2$ ; " $G_1\cap G_2$ complete" is encoded as " $V_1\cap V_2$ is a clique of $G$ and no edge joins $V_1-V_2$ to $V_2-V_1$ ", which is equivalent to the paper's hypotheses. The rows of each system are evaluated on the restriction of $x$ .
Theorem 4.2: " $G^*$ connected" is Mathlib's Connected, which requires $V\neq\emptyset$ — for $V=\emptyset$ the statement would be false. $\alpha(G)$ is indepNum, cast to $\mathbb R$ .
Corollary 4.3: "complete subgraph" is any clique set G.IsClique K, not only maximal cliques (the paper reserves "clique" for maximal complete subgraphs, but the corollary speaks of complete subgraphs), including $K=\emptyset$ . "Cutset" means two vertices outside $K$ joined by no path of $G-K$ . The formalization " $G-K$ is not connected" is ruled out: under Mathlib's convention it would make $K=V$ a cutset and the statement false for $K_1$ and $K_2$ .
Reusable infrastructure: the stable set polytope, facets via defining systems, Proposition 2.1 (shared with the other missions of this series), critical edges and $\alpha$ -critical graphs. Contributions of intermediate lemmas (LP duality in the attained form, full-dimensionality of $P(G)$ , the cutset–decomposition equivalence) are welcome.

Selected references

V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
C. Berge, Graphes et hypergraphes, Dunod, Paris, 1970 (English translation: Graphs and Hypergraphs, North-Holland, 1973), Chapter 13, §3.
J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
M. W. Padberg, On the facial structure of set packing polyhedra, Math. Programming 5 (1973) 199–215. https://doi.org/10.1007/BF01580121
L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization·Captain: mikedeng1

On Certain Polytopes Associated with Graphs I: Clique Inequalities Define the Stable Set Polytope Exactly for Perfect GraphsResearch Paper

Motivation

Many combinatorial optimization problems ask for the best subset of a finite set subject to combinatorial side conditions. The polyhedral method replaces the finite family of feasible subsets by the convex hull of their incidence vectors and asks for an explicit system of linear inequalities describing that convex hull; once such a system is known, linear programming duality gives min–max theorems and certificates of optimality. The maximum weight stable set problem is the central test case: it is NP-hard in general, so no tractable complete description of its polytope is expected for all graphs, and the question becomes for which graphs a simple description suffices.

V. Chvátal's 1975 paper On certain polytopes associated with graphs answers this question for the two simplest families of valid inequalities, and its Section 3 connects the answer to Berge's perfect graphs. The result is a standard entry point to polyhedral combinatorics and is one of the ingredients behind the later polynomial-time algorithms for stable sets in perfect graphs by Grötschel, Lovász and Schrijver.

Timeline. Berge (1961) introduced perfect graphs and conjectured that a graph is perfect if and only if its complement is. Lovász (Normal hypergraphs and the perfect graph conjecture, Discrete Math. 1972; A characterization of perfect graphs, J. Combin. Theory Ser. B 1972) proved this, together with the characterization of perfection by $\alpha(G_A)\,\omega(G_A)\ge|A|$ and the invariance of perfection under vertex duplication. Fulkerson's theory of antiblocking polyhedra (1971–72) gave a polyhedral route to the same equivalence. Chvátal (received 1972, published 1975) gave the self-contained polyhedral statement formalized here, with a proof based on Lovász's two theorems.

Setting

A graph $G=(V,E)$ is finite, undirected and loopless. A stable set is a set of vertices no two of which are adjacent. A clique is a maximal complete subgraph, and $C(G)$ is the set of vertex sets $W\subseteq V$ of the cliques of $G$ .

$S(G)\subseteq\mathbb R^V$ is the set of zero–one vectors $x=(x_u:u\in V)$ such that $\{u:x_u=1\}$ is stable, and the stable set polytope is $P(G)=\operatorname{conv}S(G)$ . A finite system of linear inequalities is a defining linear system of $P(G)$ if its solution set is exactly $P(G)$ . For $c\in\mathbb R^V$ write $cx=\sum_{u\in V}c_ux_u$ .

$G$ is perfect (the paper's $\alpha$ -perfect) if for every zero–one vector $c$ ,

\max\{cx:x\in S(G)\}=\min\Big\{\sum_{W\in C(G)}\lambda_W:\ \lambda_W\in\{0,1\},\ \sum_{W\in C(G),\,u\in W}\lambda_W\ge c_u\ (u\in V)\Big\}.

For $A\subseteq V$ , $G_A$ is the induced subgraph, $\alpha(G_A)$ its stability number and $\omega(G_A)$ its clique number. To duplicate a vertex $u$ is to add a new vertex $u'$ adjacent to all neighbours of $u$ but not to $u$ .

In the Lean development these are stableVectors G, stablePolytope G, maximalCliques G, IsPerfect G and duplicate G u in the namespace ChvatalPolytopes.Perfect.

Formalization targets

Goal: Theorem 3.1 (p. 140)

For every graph $G$ , the system

-x_u\le0\quad(u\in V),\qquad\sum_{u\in W}x_u\le1\quad(W\in C(G))

is a defining linear system of $P(G)$ if and only if $G$ is perfect. Both directions are required.

Milestones

Proposition 2.1 (pp. 139–140). For a finite nonempty set $S$ of solutions of $-x_u\le0$ , $\sum_u a_{iu}x_u\le b_i$ $(i\in J)$ , the solution set equals $\operatorname{conv}S$ if and only if for every $c\in\mathbb Z^V$

\max\{cx:x\in S\}=\min\Big\{\sum_i\lambda_ib_i:\lambda\ge0,\ \sum_i\lambda_ia_{iu}\ge c_u\ (u\in V)\Big\}.

Lovász's first theorem (§3, p. 140). Every nonperfect $G$ has $A\subseteq V$ with $\alpha(G_A)\,\omega(G_A)<|A|$ .
Lovász's second theorem (§3, p. 140). Duplicating a vertex of a perfect graph gives a perfect graph.
Condition (iii) (p. 141). $G$ is perfect if and only if for every $c\in\mathbb Z^V$

\max\{cx:x\in S(G)\}=\min\Big\{\sum_{W\in C(G)}\lambda_W:\lambda_W\ge0,\ \sum_{W\ni u}\lambda_W\ge c_u\ (u\in V)\Big\}.

Significance

The result. The nonnegativity and clique inequalities are valid for $P(G)$ for every graph. Theorem 3.1 says they are complete exactly for perfect graphs, so on perfect graphs the maximum weight stable set problem is a linear program over an explicitly described polytope, and weighted min–max theorems (stable sets versus clique covers) follow from LP duality. Combined with the perfect graph theorem, it gives a polyhedral characterization of perfect graphs, and it is the model for later results that identify graph classes by the facets of their stable set polytopes (odd-cycle inequalities, $t$ -perfection, Section 7 of the same paper).

Formalizing it. The result is classical and proved. No machine-checked version of it is known, and Mathlib has neither perfect graphs nor stable set polytopes. The mission produces a formal statement of the polyhedral characterization with the paper's own notion of perfection, a formal version of the convex-hull/LP min–max principle (Proposition 2.1), which is reusable for any 0–1 polytope, and formal statements of the two theorems of Lovász that the proof relies on.

Difficulty

Proposition 2.1 reduces Theorem 3.1 to the equivalence of perfection with a fractional min–max for all integer weights. The obvious approach to that equivalence fails in both directions. From perfection one only gets the min–max for zero–one weights and zero–one multipliers; general integer weights do not reduce to zero–one weights by linearity, because the minimum over clique covers is not additive in $c$ . Conversely, a fractional clique cover of value $\alpha$ does not directly produce an integral one. The paper crosses this gap with two theorems of Lovász: a numerical certificate of nonperfection, and the invariance of perfection under vertex duplication. Both are substantial graph-theoretic results in their own right, and neither follows from the definitions by routine manipulation.

Proposition 2.1 itself needs separation of a point from a polytope by an integral objective and LP strong duality with the nonnegativity rows handled separately.

Formalization scope

Vertices form a finite type V with decidable equality; a graph is a SimpleGraph V. $S(G)$ is a set of functions V → ℝ, and $P(G)$ is Mathlib's convexHull ℝ of it. $C(G)$ is the finset of finsets that are maximal among cliques (Maximal), as on the page; with $V=\emptyset$ the only maximal clique is $\emptyset$ . "Defining linear system" is an equality of sets. Every "max = min" is written out in full: there is a value $m$ that is the maximum over $S$ (attained and an upper bound), some feasible multiplier vector attains $m$ , and every feasible multiplier vector has objective at least $m$ . Clique multipliers are functions Finset V → ℝ read only on $C(G)$ .

Explicit conventions and added hypotheses:

In Proposition 2.1 the index set $J$ is a finite type, coefficients are real, the nonnegativity rows are kept as a separate conjunct $x\ge0$ , and $S$ is assumed nonempty (the paper's $\max$ over $S$ needs it).
$\alpha$ and $\omega$ are Mathlib's indepNum and cliqueNum (natural numbers) of G.induce A.
The duplicated graph lives on Option V, with none the new vertex.

Perfection is the paper's zero–one min–max, not "the clique system defines $P(G)$ " (which would make the goal a tautology) and not Berge's $\chi(G_A)=\omega(G_A)$ (a different definition, equivalent only through the perfect graph theorem). $P(G)$ is the convex hull of $S(G)$ , never the solution set of an inequality system.

Needed infrastructure, all reusable: integral separation from a rational polytope and LP strong duality in the form $\max\{cx:Ax\le b,x\ge0\}=\min\{\lambda b:\lambda A\ge c,\lambda\ge0\}$ ; basic facts about stable sets and maximal cliques of induced subgraphs and of duplicated graphs; invariance of IsPerfect under graph isomorphism and under taking induced subgraphs. Proofs of the Lovász milestones, which have independent value for a Mathlib theory of perfect graphs, are welcome.

Selected references

V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4
L. Lovász, A characterization of perfect graphs, J. Combin. Theory Ser. B 13 (1972) 95–98. https://doi.org/10.1016/0095-8956(72)90045-7
D. R. Fulkerson, Anti-blocking polyhedra, J. Combin. Theory Ser. B 12 (1972) 50–71. https://doi.org/10.1016/0095-8956(72)90032-9
M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

8 thms2 active usersReviewed

Completed

Optimization Theoretical Computer Science·Captain: mikedeng1

An Optimal On-Line Algorithm for Metrical Task System 1: Every n-State Metrical Task System Has Competitive Ratio 2n - 1Research Paper

Motivation

A system that processes a stream of tasks can often be configured in several ways, and the configuration affects both the cost of the current task and the cost of switching before the next one: paging schemes, replicated files, server placements. When the future is unknown, the natural worst-case yardstick is competitive analysis, introduced by Sleator and Tarjan for list update and paging (Sleator–Tarjan 1985): an on-line strategy is compared with the optimal strategy that knows the whole input in advance.

Borodin, Linial and Saks (J. ACM 1992; conference version STOC 1987) proposed metrical task systems as a single model containing all such problems, and determined the exact deterministic competitive ratio of every such system. Their theorem is the starting point of the on-line-algorithms literature on metrical task systems, the $k$ -server problem (Manasse–McGeoch–Sleator 1990) and their randomized variants.

Timeline. 1985: Sleator and Tarjan introduce competitive analysis for paging and list update. 1987: Borodin, Linial and Saks prove $w(S,d)=2n-1$ for every $n$ -state metrical task system (journal version 1992). 1990: Manasse, McGeoch and Sleator extend the task-system model to restricted task sets and pose the $k$ -server conjecture. The randomized ratio of the uniform task system, bounded in the same paper between $H(n)$ and $2H(n)$ , is the subject of the companion mission.

Setting

A task system $(S,d)$ has a finite set $S$ of $n$ states and a transition-cost matrix $d$ with $d(i,i)=0$ , $d(i,j)>0$ for $i\neq j$ , and the triangle inequality $d(i,j)+d(j,k)\ge d(i,k)$ . It is metrical if also $d(i,j)=d(j,i)$ .

A task $T$ is a vector of nonnegative processing costs $T(s)$ , $s\in S$ . Given a task sequence $\mathbf T=T^1\cdots T^m$ and an initial state $s_0$ , a schedule is a map $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$ ; task $T^i$ is processed in state $\sigma(i)$ , and the cost is

c(\mathbf T;\sigma)=\sum_{i=1}^m d(\sigma(i-1),\sigma(i))+\sum_{i=1}^m T^i(\sigma(i)).

The off-line optimum $c_0(\mathbf T)$ is the minimum over all schedules. An on-line algorithm $A$ chooses $\sigma(i)$ knowing only $s_0$ and $T^1,\dots,T^i$ ; its cost is $c_A(\mathbf T)$ . For $w>0$ , $A$ is $w$ -competitive if there is a constant $K_w$ with $c_A(\mathbf T)\le w\,c_0(\mathbf T)+K_w$ for every finite task sequence. The competitive ratio of $A$ is $w(A)=\inf\{w: A\text{ is }w\text{-competitive}\}$ , and the competitive ratio of the task system is $w(S,d)=\inf_A w(A)$ .

For the upper bound the paper also uses continuous-time schedules, in which task $T^i$ occupies the interval $[i,i+1)$ and the scheduler may change state at any real time, paying $\int_i^{i+1}T^i(\sigma(t))\,dt$ for processing. For a general (possibly asymmetric) matrix $d$ , the cycle offset ratio $\psi(d)$ is the maximum over closed walks $s_0,\dots,s_k=s_0$ of $\sum_i d(s_{i-1},s_i)\big/\sum_i d(s_i,s_{i-1})$ ; it equals $1$ when $d$ is symmetric.

Formalization targets

Goal: Theorem 1.1

For every metrical task system $(S,d)$ with $n$ states,

w(S,d)=2n-1 .

The value depends on $n$ only, not on the distances.

Milestones

Lemma 2.1. If $c_0(T^1\cdots T^m)\to\infty$ along an infinite task sequence $\mathbf T$ , then $w(A)\ge w_{\mathbf T}(A)=\limsup_m c_A/c_0$ .
Theorem 2.2. Against the cruel taskmaster $M(\varepsilon)$ , which charges $\varepsilon$ in the state the algorithm currently occupies,

w_{\mathbf T(\varepsilon)}(A)\ge\frac{2n-1}{1+\varepsilon/\min_{i\neq j}d(i,j)} .

Lemma 3.1. Every on-line continuous-time algorithm is matched, on every task sequence, by an on-line discrete-time algorithm.
Lemmas 6.3, 6.4, 6.2. Properties of the functions $f_k$ that drive the algorithm $A^*_d$ : $f_k(s)-f_k(s')\le d(s',s)$ ; the identity $2\sum_{s\ne s_k}f_k(s)+f_k(s_k)=C_{k-1}+\sum_{i\le k}d(s_i,s_{i-1})$ ; and $f_k\le h_k$ , the off-line cost at the $k$ -th transition time.
Theorem 6.1 (= Theorem 1.2). For every task system, symmetric or not, $A^*_d$ has competitive ratio at most $(2n-1)\psi(d)$ .

Significance

The theorem settles the deterministic competitive ratio of the whole class of metrical task systems: the lower bound says that no deterministic on-line strategy can beat $2n-1$ on any metric, and the upper bound supplies one algorithm that achieves it on every metric. For asymmetric costs the same algorithm gives $(2n-1)\psi(d)$ . The $2n-1$ lower bound is also the benchmark against which restricted models, such as paging and the $k$ -server problem, measure their improvements, and the randomized question it leaves open drove much of the later work on metrical task systems.

The result was proved in 1987 and is standard; to the best of our knowledge no machine-checked proof exists. A formal development would provide a reusable model of deterministic on-line algorithms and competitiveness (on-line maps from task prefixes, additive competitiveness, infima over algorithms), an adversary construction by mutual recursion with an arbitrary algorithm, and an exact treatment of continuous-time schedules with piecewise-constant task costs. These pieces are reusable for other competitive-analysis results.

Difficulty

The lower bound is not a single bad input: the adversary is built from the algorithm it plays against, so the hard task sequence exists only as a recursion interleaved with the algorithm's choices, and the bound must hold for every deterministic on-line map, including ones that behave erratically. Obtaining the exact constant $2n-1$ , rather than some $\Omega(n)$ bound, requires a sharp estimate of the off-line cost of that sequence.

The upper bound needs an algorithm defined in continuous time, whose transition times are determined by accumulated processing costs; the budgets can be zero, so transitions can be instantaneous, and a formal cost must remain well defined before one knows that only finitely many transitions occur. Relating the off-line cost function at those times to the recursively defined $f_k$ (Lemma 6.2) requires reasoning about all continuous-time off-line schedules. Finally, the goal combines both directions through infima over all on-line algorithms, and the discretization of Lemma 3.1 must be composed with the continuous-time algorithm.

Formalization scope

States form a finite type S (Fintype, DecidableEq, Nonempty); the goal is stated for all $n\ge1$ , where $n=1$ gives $w(S,d)=1$ . Task costs are finite nonnegative reals; the paper also allows $+\infty$ entries, which are excluded (this affects neither bound). A task sequence is T : Fin m → S → ℝ, with T i the paper's $T^{i+1}$ , and a schedule is σ : Fin (m+1) → S. An on-line algorithm is a map sending $(s_0,[T^1,\dots,T^i])$ to $\sigma(i)$ , so on-line behaviour is built into the type. Competitiveness is written additively, $c_A\le w\,c_0+K$ , with $K$ independent of the task sequence and of $s_0$ .

The competitive ratio competitiveRatio d is the real infimum of the set of all $w$ for which some on-line algorithm is $w$ -competitive. It is not defined as an infimum of per-algorithm real infima: a non-competitive algorithm has $W_A=\emptyset$ , whose real infimum is $0$ , and that would drag $w(S,d)$ to $0$ for every system. Since the goal's value $2n-1$ is at least $1$ while the empty set's real infimum is $0$ , the goal cannot hold vacuously.

Continuous-time algorithms are given as lists of $(\text{state},\text{length})$ pieces per unit interval; processing integrals are exact finite sums. The algorithm $A^*_d$ minimizes over states different from the current one, as its proof requires (the printed rule ranges over all states, and would stall); ties are left arbitrary. Its budgets may be $0$ , its entry times are Option ℝ, and its cost is a sum in $[0,\infty]$ , so that Theorem 6.1 itself asserts that only finitely many transitions occur. The ratio $\psi(d)$ excludes closed walks that never move, and Theorems 2.2 and 6.1 require $n\ge2$ , where $\min_{i\ne j}d(i,j)$ and $\psi(d)$ are defined. Lemma 3.1 is stated comparing $A$ with $A'$ (the printed statement says "as well as $A$ ").

A complete development needs: the discrete model and off-line optimum (finite minimum over schedules), limsup arguments in EReal, continuous-time schedules with piecewise-constant costs, and the recursion defining $A^*_d$ . Proofs of any milestone, including the purely combinatorial Lemmas 6.3 and 6.4, are welcome, as is a formal composition of Lemma 3.1 with Theorem 6.1.

Selected references

A. Borodin, N. Linial, M. E. Saks, An optimal on-line algorithm for metrical task system, Journal of the ACM 39(4):745–763, 1992. https://doi.org/10.1145/146585.146588
D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Communications of the ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, Journal of Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W

12 thms2 active usersReviewed

Combinatorics Discrete Geometry Linear Optimization·Captain: mikedeng1

On Sub-determinants and the Diameter of Polyhedra: A Polynomial Diameter Bound in the Largest SubdeterminantResearch Paper

Motivation

The combinatorial diameter of a polyhedron is the largest distance, in its vertex-edge graph, between two vertices. It is a lower bound on the number of pivots any edge-following method such as the simplex method needs in the worst case, which is why the polynomial Hirsch conjecture — the diameter of $P = \{x \in \mathbb{R}^n : Ax \le b\}$ is bounded by a polynomial in $m$ and $n$ — is a central open question of linear optimization and discrete geometry. The best general upper bound is quasi-polynomial, $m^{1+\log n}$ (Kalai–Kleitman 1992); the original Hirsch bound $m - n$ is false for polytopes (Santos 2012).

A different line of work bounds the diameter by the arithmetic of the constraint matrix instead of its size. For an integer matrix $A$ let $\Delta$ be the largest absolute value of a sub-determinant of $A$ . Dyer and Frieze (1994) showed that for totally unimodular $A$ ( $\Delta = 1$ ) the diameter is polynomial, $O(m^{16} n^3 (\log mn)^3)$ . Bonifas, Di Summa, Eisenbrand, Hähnle and Niemeier (SoCG 2012; Discrete Comput Geom 52, 2014) improved and generalized this to $O(\Delta^2 n^4 \log n\Delta)$ for all polyhedra and $O(\Delta^2 n^{3.5} \log n\Delta)$ for polytopes, bounds that do not depend on the number $m$ of inequalities. This mission formalizes the polytope case.

Setting

Let $A \in \mathbb{Z}^{m\times n}$ with rows $a_1,\dots,a_m$ , let $b \in \mathbb{R}^m$ , and let $P = \{x \in \mathbb{R}^n : Ax \le b\}$ . A vertex of $P$ is an extreme point; for a polyhedron this is a point of $P$ at which $n$ linearly independent inequalities are tight. Two vertices $u \ne v$ are adjacent if the segment $[u,v]$ is an edge (a one-dimensional face) of $P$ . This gives the polyhedral graph $G_P = (V, E)$ , and the diameter of $P$ is at most $B$ if every two vertices are joined by a walk of at most $B$ edges.

$A$ has sub-determinants bounded by $\Delta$ if every $k\times k$ submatrix, for every $k \ge 1$ , has determinant in $[-\Delta, \Delta]$ . In particular every entry is at most $\Delta$ in absolute value.

For a vertex $v$ the normal cone $C_v$ is the set of objectives $c$ for which $v$ maximizes $c^T x$ over $P$ . With $B_n$ the closed unit ball, the volume of a set $U \subseteq V$ of vertices is

\mathrm{vol}(U) = \mathrm{vol}\Big(\bigcup_{v\in U} C_v \cap B_n\Big),

and the neighbourhood $\mathcal N(I)$ of $I \subseteq V$ is the set of vertices outside $I$ adjacent to a vertex of $I$ . A spherical cone is $S = C \cap B_n$ with $C$ closed under non-negative scaling; its dockable surface $D(S)$ is the $(n-1)$ -dimensional measure of the part of its boundary inside the open ball. A cone of revolution of angle $0<\theta\le\pi/2$ is $\{x \in B_n : v^T x \ge \cos\theta\,\|v\|\,\|x\|\}$ . $P$ is non-degenerate if every vertex has exactly $n$ tight inequalities.

Formalization targets

Goal: Theorem 2 (p. 105)

If $A \in \mathbb{Z}^{m\times n}$ has all sub-determinants bounded by $\Delta$ and $P$ is bounded, then

\operatorname{diam}(P) \le 2\Big\lfloor \sqrt{2\pi}\,\Delta^2 n^{5/2}\ln\!\big(2^n\, n!\, n^{n/2}\,\Delta^n\big)\Big\rfloor + 2 \;=\; O(\Delta^2 n^{3.5}\log n\Delta).

No non-degeneracy, full-dimensionality or rank condition is assumed, and the bound is uniform in $m$ and $b$ .

Milestones

Lemma 3 (p. 108): for a vertex $v$ of a non-degenerate polytope, $D(S_v) \le \Delta^2 n^3\,\mathrm{vol}(S_v)$ , where $S_v = C_v \cap B_n$ .
Lemma 4 (p. 109): among spherical cones of a given volume, a cone of revolution has minimum dockable surface.
Lemma 5 (p. 110): for a cone of revolution, $D(S) \ge \sqrt{2n/\pi}\,\mathrm{vol}(S)$ .
Lemma 6 (p. 111): for every measurable spherical cone with $\mathrm{vol}(S) \le \frac12 \mathrm{vol}(B_n)$ , $D(S) \ge \sqrt{2n/\pi}\,\mathrm{vol}(S)$ .
Lemma 1 (p. 105): for a non-degenerate polytope and $I \subseteq V$ with $\mathrm{vol}(I) \le \frac12\mathrm{vol}(B_n)$ ,

\mathrm{vol}(\mathcal N(I)) \ge \sqrt{\tfrac{2}{\pi}}\,\frac{1}{\Delta^2 n^{2.5}}\,\mathrm{vol}(I).

Eq. (1) (p. 105): if $I_j$ is the set of vertices at graph distance at most $j$ from a vertex $v$ and $\mathrm{vol}(I_j) \le \frac12\mathrm{vol}(B_n)$ , then $j \le \sqrt{2\pi}\,\Delta^2 n^{2.5}\ln(2^n/\mathrm{vol}(I_0))$ .

Significance

The result. Theorem 2 bounds the diameter of every integral polytope by a polynomial in the dimension and the largest sub-determinant, independently of the number of facets. For totally unimodular matrices, which cover network-flow, bipartite matching and transportation polytopes, it gives $O(n^{3.5}\log n)$ , improving the Dyer–Frieze bound by a large polynomial factor. It shows that the obstruction to a polynomial Hirsch bound, if any, must come from matrices with large sub-determinants. The volume-expansion method — measuring breadth-first search by the volume of the normal fan it has covered — was later refined, for instance in the shadow-vertex analysis of Dadush–Hähnle, which improves the dependence on $n$ .

Formalizing it. The theorem is proved (2012/2014); no machine-checked proof is known. A formal development needs, on top of Mathlib, the normal fan of a polytope and its relation to the vertex-edge graph, a Hausdorff-measure calculus for cones (surface of a cone in terms of its base), Lévy's isoperimetric inequality on the sphere in a measure-theoretic form, and explicit Gamma-function estimates. Each of these is reusable well beyond this paper.

Difficulty

The combinatorial side is short; the geometry is not. Lemma 4 is the spherical isoperimetric inequality of Lévy, which Mathlib does not have in any form, and which the paper cites rather than proves; the relations between the volume of a spherical cone, the area of its base, its lateral surface and the length of the base's boundary (Eq. (3), "basic integration") are also absent. Lemma 3 depends on the structure of the normal cone of a vertex of a non-degenerate polytope (full-dimensional, simplicial, generated by rows of $A$ ), none of which is available for Mathlib's extreme points. Lemma 1 depends on the normal fan of a polytope: the normal cones have pairwise disjoint interiors, cover $\mathbb{R}^n$ , and share a facet exactly when their vertices are adjacent. The step from non-degenerate to arbitrary polytopes perturbs $b$ and needs the diameter not to decrease, a statement about the vertex-edge graph under perturbation. A shortcut through a finite graph abstraction is not available: the constant depends on the geometry of the normal cones, not only on the graph.

Formalization scope

The polyhedron is Hirsch.Hpoly (rowVec A) b, with rowVec A i the $i$ -th row of $A \in$ Matrix (Fin m) (Fin n) ℤ as a vector of EuclideanSpace ℝ (Fin n). Vertices are Set.extremePoints ℝ P, adjacency is Hirsch.Adj, "diameter at most $B$ " is Hirsch.DiamLE P B, all from the published Hirsch_model. The normal cone is the published FirstOrderOpt.ConvexTheory.normalCone. Volumes are Lebesgue measure with values in $[0,\infty]$ ; the dockable surface uses μHE[n-1], the Hausdorff measure normalized to agree with Lebesgue measure on hyperplanes, applied to frontier S ∩ Metric.ball 0 1. $\Delta$ is a natural number and the sub-determinant bound ranges over all sizes $k \ge 1$ .

Explicit constants. The paper writes $O(\Delta^2 n^{3.5}\log n\Delta)$ in Theorem 2; the proof on pp. 105–106 yields $2\lfloor K\rfloor + 2$ with $K = \sqrt{2\pi}\,\Delta^2 n^{5/2}\ln(2^n n!\, n^{n/2}\Delta^n)$ , from Eq. (1), the bound $\mathrm{vol}(I_0) \ge 1/(n!\,n^{n/2}\Delta^n)$ and the fact that the diameter is at most twice the number of breadth-first-search iterations needed to cover more than half of $B_n$ . This explicit bound is the goal. The ratios $D/\mathrm{vol}$ of Lemmas 3, 5, 6 are stated in multiplicative form.

Non-degeneracy is a hypothesis of Lemma 3, Lemma 1 and Eq. (1) only, as in the paper's §1.1, and never of Theorem 2. The neighbourhood $\mathcal N(I)$ excludes $I$ ; including it would make Lemma 1 trivial, since its constant is below $1$ . Lemma 4 is stated against every competitor: for every measurable spherical cone $S$ and every cone of revolution $S^*$ of the same volume, $D(S^*) \le D(S)$ ; it does not assert existence of a cone of a prescribed volume. The goal is Theorem 2 about the polytope and its graph, not an abstract statement about set families with a volume-expansion property; integrality of $A$ and the bound on minors of every size are both essential (scaling a real matrix down makes $\Delta$ arbitrarily small), and the raw Hausdorff measure μH[n-1] would put Lemmas 3 and 6 on incompatible scales.

Contributions are welcome at every level: the normal fan and its adjacency structure, cone surface formulas, the Gamma estimate $\Gamma(x+\frac12)/\Gamma(x) \ge \sqrt{x-\frac14}$ , and a formal Lévy inequality.

Selected references

N. Bonifas, M. Di Summa, F. Eisenbrand, N. Hähnle, M. Niemeier, On Sub-determinants and the Diameter of Polyhedra, Discrete Comput Geom 52 (2014) 102–115. https://doi.org/10.1007/s00454-014-9601-x
M. Dyer, A. Frieze, Random walks, totally unimodular matrices, and a randomised dual simplex algorithm, Math. Program. 64 (1994) 1–16. https://doi.org/10.1007/BF01582563
G. Kalai, 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
F. Santos, A counterexample to the Hirsch conjecture, Annals of Math. 176 (2012) 383–412. https://doi.org/10.4007/annals.2012.176.1.7
T. Figiel, J. Lindenstrauss, V. Milman, The dimension of almost spherical sections of convex bodies, Acta Math. 139 (1977) 53–94 (Lévy's isoperimetric inequality, Theorem 2.1). https://doi.org/10.1007/BF02392234
D. Dadush, N. Hähnle, On the shadow simplex method for curved polyhedra, Discrete Comput Geom 56 (2016). https://arxiv.org/abs/1412.6705

11 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Nonmonotone Spectral Projected Gradient Methods on Convex Sets I: SPG2 Is Well Defined and Its Accumulation Points Are StationaryResearch Paper

Motivation

Minimizing a smooth function over a closed convex set $\Omega\subseteq\mathbb R^n$ on which projection is cheap (a box, a ball, a simplex) is a routine subproblem in large-scale optimization: box-constrained minimization is the inner solver of augmented Lagrangian methods, and bound-constrained least squares, image restoration and density estimation all have this form. The classical projected gradient method of Goldstein and of Levitin and Polyak is simple and needs only gradients and projections, but with constant or Armijo-type step lengths it is slow.

Spectral projected gradient (SPG) methods, introduced by Birgin, Martínez and Raydan (paper), combine three ingredients: the projected gradient direction; the Barzilai–Borwein (spectral) step length $\alpha_{k+1}=\langle s_k,s_k\rangle/\langle s_k,y_k\rangle$ , an inverse Rayleigh quotient of the average Hessian along the last step; and the nonmonotone line search of Grippo, Lampariello and Lucidi, which compares a trial value with the worst of the last $M$ objective values instead of the current one. The method is widely used in practice, and its analysis is the template for many later nonmonotone projected methods.

Timeline:

1964–1966: Goldstein; Levitin and Polyak introduce gradient projection.
1976: Bertsekas analyses the Armijo rule along the projection arc.
1986: Grippo, Lampariello and Lucidi introduce the nonmonotone line search for unconstrained problems.
1988: Barzilai and Borwein propose the two-point step size; Raydan (1993, 1997) proves convergence for quadratics and combines it with nonmonotone search in the unconstrained case.
2000: Birgin, Martínez and Raydan define SPG1 and SPG2 for convex constraints (SIAM J. Optim. 10(4)).
2003: the same authors publish the convergence proof that Theorem 2.1 refers to, in the inexact setting (IMA J. Numer. Anal. 23).

Setting

Let $\Omega\subseteq\mathbb R^n$ be nonempty, closed and convex, with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . Let $f$ have continuous partial derivatives on an open set $U\supseteq\Omega$ and write $g(x)=\nabla f(x)$ . The orthogonal projection $P(z)$ is the unique point of $\Omega$ nearest to $z$ . The scaled projected gradient is $g_t(x)=P(x-t\,g(x))-x$ for $x\in\Omega$ , $t>0$ . A point $\bar x$ is a constrained stationary point if $\langle g(\bar x),x-\bar x\rangle\ge0$ for all $x\in\Omega$ .

The parameters are an integer $M\ge1$ , reals $0<\alpha_{\min}<\alpha_{\max}$ , a sufficient-decrease constant $\gamma\in(0,1)$ and safeguards $0<\sigma_1<\sigma_2<1$ . Algorithm SPG2 starts from $x_0\in\Omega$ and $\alpha_0\in[\alpha_{\min},\alpha_{\max}]$ and at iteration $k=0,1,\dots$ :

Stop test. If $\|P(x_k-g(x_k))-x_k\|=0$ , stop: $x_k$ is stationary.
Backtracking. Set $d_k=P(x_k-\alpha_k g(x_k))-x_k$ and $\lambda=1$ . While

f(x_k+\lambda d_k)\le\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})+\gamma\lambda\langle d_k,g(x_k)\rangle\qquad(3)

fails, replace $\lambda$ by any $\lambda_{\rm new}\in[\sigma_1\lambda,\sigma_2\lambda]$ . When (3) holds, $\lambda_k=\lambda$ and $x_{k+1}=x_k+\lambda_kd_k$ . 3. Spectral step. With $s_k=x_{k+1}-x_k$ , $y_k=g(x_{k+1})-g(x_k)$ , $b_k=\langle s_k,y_k\rangle$ : $\alpha_{k+1}=\alpha_{\max}$ if $b_k\le0$ , else $\alpha_{k+1}=\min\{\alpha_{\max},\max\{\alpha_{\min},\langle s_k,s_k\rangle/b_k\}\}$ .

In Lean the projection is a function P with the predicate IsProjOnto Ω P, $g_t$ is scaledProjGrad P f t, stationarity is IsConstrainedStationary Ω f, the maximum in (3) is nonmonotoneRef f x M k, and an infinite run is IsSPG2Run Ω f P M αmin αmax γ σ₁ σ₂ x α.

Formalization targets

Goal: Theorem 2.1, accumulation points are stationary

For every infinite run $(x_k,\alpha_k)$ of SPG2 and every accumulation point $\bar x$ of $(x_k)$ ,

\langle g(\bar x),x-\bar x\rangle\ge0\qquad\text{for all }x\in\Omega.

The statement fixes no parameter values and assumes neither convexity of $f$ nor a bounded level set.

Milestones

Lemma 2.1 (ii). For $\bar x\in\Omega$ and $t\in(0,\alpha_{\max}]$ : $g_t(\bar x)=0$ iff $\bar x$ is a constrained stationary point.
Lemma 2.1 (i). For $x\in\Omega$ and $t\in(0,\alpha_{\max}]$ :

\langle g(x),g_t(x)\rangle\le-\tfrac1t\|g_t(x)\|_2^2\le-\tfrac1{\alpha_{\max}}\|g_t(x)\|_2^2.

Theorem 2.1, first clause (SPG2 is well defined). At a point where Step 1 does not stop, every admissible backtracking sequence reaches a step satisfying (3). The step is stated for an arbitrary reference value $R\ge f(x)$ , which covers the maximum in (3).
Section 2, p. 4. The iterates remain in $\Omega_0=\{x\in\Omega:f(x)\le f(x_0)\}$ .

Significance

Theorem 2.1 is the global convergence guarantee for SPG2. It holds without monotone decrease of $f$ and without any restriction on the spectral step beyond the safeguards. These are the two features that make the method fast in practice, and together they mean that no classical monotone projected-gradient argument applies directly. The same statement underlies the convergence claims of the SPG software (ACM TOMS Algorithm 813) and of the many methods that reuse the nonmonotone spectral framework: inexact SPG, augmented Lagrangian inner solvers, and projected BB methods for machine learning.

Status: the theorem is proved in the literature. This paper's proof reads "See [7]", a pointer to Birgin, Martínez and Raydan (2003). No Lean formalization of this theorem, of the nonmonotone Armijo analysis, or of the projected-gradient stationarity lemma is known. The mission produces a formal proof and a reusable Lean interface for projection-based first-order methods on convex sets.

Difficulty

The obvious argument for monotone descent methods is to show that $f(x_k)$ decreases, so that the total decrease is finite and the per-iteration decrease $\gamma\lambda_k|\langle d_k,g(x_k)\rangle|$ tends to zero. Here $f(x_k)$ need not decrease. Only the reference value $\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})$ is nonincreasing, and a small decrease of this maximum along the whole sequence does not by itself give a small decrease at the iterates that approach a given accumulation point $\bar x$ . A second difficulty is that the accepted step lengths $\lambda_k$ may tend to zero along the subsequence, while $f$ is $C^1$ only on a neighbourhood of $\Omega$ and no Lipschitz constant for $g$ is available, so no uniform sufficient-decrease estimate holds. The spectral steps $\alpha_k$ vary within $[\alpha_{\min},\alpha_{\max}]$ , so the directions $d_k$ are not a fixed function of $x_k$ .

Formalization scope

Space and data. The space is EuclideanSpace ℝ (Fin n) with inner ℝ and the 2-norm. $f$ is a total function EuclideanSpace ℝ (Fin n) → ℝ with ContDiffOn ℝ 1 f U on an open U ⊇ Ω, and $g$ is Mathlib's gradient f. The algorithm evaluates $f$ and $g$ only at points of $\Omega$ .
Iteration and trials. Iterations are indexed from $0$ . The backtracking choice (2) is universally quantified: a run carries, at each iteration, a finite trial list $\lambda^{(0)}=1$ , $\lambda^{(i+1)}\in[\sigma_1\lambda^{(i)},\sigma_2\lambda^{(i)}]$ , in which test (3) fails at every trial but the last and holds at the last.
Step size. $\alpha_{k+1}$ is given by Step 3 exactly.
Accumulation point. An accumulation point is MapClusterPt x̄ atTop x.
Excluded simplifications. A run predicate that accepts any positive step, or lets $\alpha_{k+1}$ range freely over $[\alpha_{\min},\alpha_{\max}]$ , is not SPG2. Nor is a goal stating $g_t(\bar x)=0$ instead of the variational inequality, or one that adds convexity of $f$ , a Lipschitz gradient or a bounded level set.
Non-vacuity. The hypotheses of the goal are satisfiable: for $f(x)=\|x\|^2$ , $\Omega=\mathbb R^n$ , $M=1$ , $\alpha_{\min}=1/8$ , $\alpha_{\max}=1/4$ , $\gamma=1/2$ and $v\ne0$ , the iterates $x_k=2^{-k}v$ with $\alpha_k=1/4$ form an infinite run with accumulation point $0$ .
Infrastructure. A complete development needs the variational characterization of the projection (Mathlib has it for the iInf form: norm_eq_iInf_iff_real_inner_le_zero), continuity properties of the projection, a mean-value estimate for $C^1$ functions on segments in $\Omega$ , and the nonmonotone reference-value bookkeeping. The projection lemmas and the nonmonotone bookkeeping are reusable beyond this mission, in particular for the companion mission on SPG1, and contributions of them as separate lemmas are welcome.

Selected references

E. G. Birgin, J. M. Martínez, M. Raydan, Nonmonotone spectral projected gradient methods on convex sets, SIAM J. Optim. 10(4) (2000) 1196–1211; authors' updated version, July 2004. https://doi.org/10.1137/S1052623497330963, https://www.ime.unicamp.br/~martinez/bmr.pdf
E. G. Birgin, J. M. Martínez, M. Raydan, Inexact spectral projected gradient methods on convex sets, IMA J. Numer. Anal. 23 (2003) 539–559. https://doi.org/10.1093/imanum/23.4.539
J. Barzilai, J. M. Borwein, Two-point step size gradient methods, IMA J. Numer. Anal. 8 (1988) 141–148. https://doi.org/10.1093/imanum/8.1.141
L. Grippo, F. Lampariello, S. Lucidi, A nonmonotone line search technique for Newton's method, SIAM J. Numer. Anal. 23 (1986) 707–716. https://doi.org/10.1137/0723046
M. Raydan, The Barzilai and Borwein gradient method for the large scale unconstrained minimization problem, SIAM J. Optim. 7 (1997) 26–33. https://doi.org/10.1137/S1052623494266365
D. P. Bertsekas, On the Goldstein–Levitin–Polyak gradient projection method, IEEE Trans. Automat. Control 21 (1976) 174–184. https://doi.org/10.1109/TAC.1976.1101194

10 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Robust Solutions of Optimization Problems Affected by Uncertain Probabilities II: A Self-Concordant Barrier for the Perspective ConstraintResearch Paper

Motivation

Robust optimization protects a decision against every scenario in an uncertainty set. When the uncertain data are probabilities, a natural uncertainty set is a ball around a nominal distribution measured by a φ-divergence (Kullback–Leibler, Burg entropy, χ², Hellinger and others). Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) show that the robust counterpart of a linear constraint over such a set is a finite convex system, and then ask whether that system is computationally tractable: can an interior-point method solve it in polynomial time?

For the Burg and Kullback–Leibler divergences the reformulated constraints (Eqs. (29) and (32) of the paper) have the shape $\lambda f(s_i/\lambda)\le\dots$ , a perspective constraint. Polynomial-time solvability by interior-point methods follows once the constraint set carries a self-concordant barrier in the sense of Nesterov and Nemirovski (Interior-Point Polynomial Algorithms in Convex Programming, SIAM 1994). Theorem 2 of the paper supplies such a barrier for every perspective constraint whose generating function satisfies a one-dimensional differential inequality. The same question arises for perspective and relative-entropy cones in conic optimization generally, so the criterion is of interest beyond φ-divergences.

Setting

A function $\varphi:F\to\mathbb R$ on an open convex set $F\subseteq\mathbb R^n$ is $\kappa$ -self-concordant ( $\kappa\ge0$ ) if it is three times continuously differentiable on $F$ and for every $y\in F$ and every direction $h\in\mathbb R^n$

\bigl|\nabla^3\varphi(y)[h,h,h]\bigr|\le 2\kappa\,\bigl(h^{\mathsf T}\nabla^2\varphi(y)h\bigr)^{3/2},

where $\nabla^k\varphi(y)[h,\dots,h]$ is the $k$ -th differential of $\varphi$ at $y$ in direction $h$ (Definition 1, p. 350). In Lean this is PhiDivRobust.Barrier.IsSelfConcordant κ F φ.

Let $f$ be a real function on $(0,\infty)$ . Its perspective is $g(s,y)=y\,f(s/y)$ for $s,y>0$ (perspective f). The constraint set (34) is

\{(s,y,z):\ y f(s/y)\le z,\ s\ge0,\ y\ge0\},

and its logarithmic barrier (35) is

\varphi_B(s,y,z)=-\ln\bigl(z-yf(s/y)\bigr)-\ln s-\ln y

(logBarrier f), finite on the open set $F_f=\{(s,y,z): s>0,\ y>0,\ yf(s/y)<z\}$ (barrierDomain f). Directions are $h=(h_1,h_2)$ for $g$ , with $h_1$ along $s$ and $h_2$ along $y$ , and $h\in\mathbb R^3$ for $\varphi_B$ .

Formalization targets

Goal: Theorem 2 (p. 350)

If $f$ is convex on $(0,\infty)$ and, for some $\kappa>0$ ,

|f'''(s)|\le\kappa\,\frac{f''(s)}{s}\qquad(s>0),\tag{33}

then $\varphi_B$ is $\bigl(2+\tfrac{\sqrt2}{3}\kappa\bigr)$ -self-concordant on $F_f$ .

Milestones (the displayed steps of the proof)

Eq. (37): $\nabla^2 g(s,y)[h,h]=f''(s/y)\bigl(h_1^2/y-2sh_1h_2/y^2+s^2h_2^2/y^3\bigr)$ .
The third differential of $g$ in terms of $f''(s/y)$ and $f'''(s/y)$ .
Under (33), inequality (36) with $\beta=3+\kappa\sqrt2$ :

\bigl|\nabla^3 g(s,y)[h,h,h]\bigr|\le\beta\,h^{\mathsf T}\nabla^2 g(s,y)h\,\sqrt{h_1^2/s^2+h_2^2/y^2}.

Lemma A.2 of den Hertog (1994), as quoted in the proof: if (36) holds with $\beta\ge0$ , then $\varphi_B$ is $(1+\beta/3)$ -self-concordant on $F_f$ .

Milestones 3 and 4 give the goal, since $1+\tfrac13(3+\kappa\sqrt2)=2+\tfrac{\sqrt2}{3}\kappa$ . A further item records the paper's application: $f(s)=-\log s$ (the Burg case) satisfies (33) with $\kappa=2$ .

Significance

The result. Theorem 2 turns a two-line calculus check on a scalar function into a certificate of polynomial-time solvability for a three-dimensional convex constraint. The paper uses it to conclude that the robust counterparts for the Burg entropy and Kullback–Leibler uncertainty sets are tractable, and the criterion applies to any other convex $f$ satisfying (33); for example $f(s)=s\log s$ satisfies it with $\kappa=1$ , which covers the relative-entropy cone. The constant $2+\tfrac{\sqrt2}{3}\kappa$ enters the complexity bound of any path-following method through the barrier parameter.

Formalizing it. The theorem is proved in the paper, but the decisive step is delegated to Lemma A.2 of den Hertog's monograph, which in turn belongs to the compatibility theory of Nesterov and Nemirovski. As far as is known none of these statements has a machine-checked proof. The mission produces a checked version of the compatibility lemma for perspective constraints, which is reusable for any barrier of the form $-\ln(z-g)-\ln s-\ln y$ , together with explicit second- and third-differential formulas for perspectives in Mathlib's iteratedFDeriv language. The printed third-differential display contains a typo (see below); the formal statements fix it.

Difficulty

The differential identities (milestones 1 and 2) are routine but heavy: they require computing iterated Fréchet derivatives of a composition with a quotient in two variables and matching them with one-variable iterated derivatives of $f$ . The inequality (milestone 3) is elementary real-variable algebra once the differentials are available.

The central difficulty is den Hertog's lemma. The obvious approach, bounding the three terms of $\nabla^3\varphi_B$ separately against $(\nabla^2\varphi_B)^{3/2}$ , fails: the cross term $-3\,(\nabla\omega\cdot h)\,\nabla^2 g[h,h]/\omega^2$ with $\omega=z-g$ couples the first and second differentials, and bounding it separately loses the constant $1+\beta/3$ . A further practical difficulty is that $F_f$ is open and convex only because the perspective of a convex function is jointly convex and continuous, which must itself be established.

Formalization scope

Points are $(s,y,z)\in\mathbb R\times\mathbb R\times\mathbb R$ and directions for $g$ are in $\mathbb R\times\mathbb R$ . Differentials are iteratedFDeriv ℝ k applied to the constant tuple $(h,\dots,h)$ ; $f''$ and $f'''$ are iteratedDeriv 2 f and iteratedDeriv 3 f. The power $x^{3/2}$ is Real.rpow, which is $0$ for $x<0$ ; this makes the Lean definition of self-concordance no weaker than the paper's. Real.log and division have junk values outside $F_f$ , but $F_f$ is open, so no differential at a point of $F_f$ sees them.

Committed conventions and disclosed deviations:

" $f:\mathbb R^+\to\mathbb R$ " is read as $f$ convex on the open half-line $(0,\infty)$ ; the Burg case $f=-\log$ is undefined at $0$ , and $f$ is only evaluated at $s/y$ with $s,y>0$ .
$f$ is assumed $C^3$ on $(0,\infty)$ . The page does not say so, but (33) uses $f'''$ and Definition 1 requires the barrier to be $C^3$ .
The printed third-differential display ends in $s^3h_x^3/y^5$ ; the correct term is $s^3h_2^3/y^5$ , and the Lean statement uses it. The milestone text keeps the printed version.
Lemma A.2 is stated with $\beta\ge0$ added. The quoted text says "if there exists a $\beta$ ", which is false for $\beta<0$ : with $f\equiv0$ , (36) holds for every $\beta$ and $\beta=-3$ would give a $0$ -self-concordant $-\ln z-\ln s-\ln y$ . The goal uses $\beta=3+\kappa\sqrt2>0$ and is unaffected.

A trivializing formalization is excluded. The self-concordance predicate requires $C^3$ regularity and quantifies over all directions $h\in\mathbb R^3$ , the domain is exactly $F_f$ (not a subset such as $\emptyset$ ), and $\kappa>0$ is as printed. The constant of the conclusion is tied to the same $\kappa$ as in (33).

Useful infrastructure, reusable beyond this mission: iterated derivatives of perspectives, joint convexity of perspectives, and the calculus of self-concordance (sums, $-\ln$ of a concave function composed with an affine map). Proofs of the milestones independently of the goal are welcome, as are proofs of the Burg item's consequence and of the analogous statement for $f(s)=s\log s$ .

Selected references

A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
D. den Hertog, Interior Point Approach to Linear, Quadratic and Convex Programming: Algorithms and Complexity, Kluwer Academic Publishers, 1994. https://doi.org/10.1007/978-94-011-1134-8
Yu. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791

8 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Robust Solutions of Optimization Problems Affected by Uncertain Probabilities I: The Robust Counterpart of a Linear Constraint under φ-Divergence UncertaintyResearch Paper

Motivation

Many decision problems contain a constraint whose coefficients are an expectation under a probability vector that is not known exactly: an expected cost under uncertain scenario probabilities, an expected payoff of an asset under an estimated distribution, the expected demand in a newsvendor model. The probabilities are usually estimated from data, and a solution that is feasible for the estimate can be infeasible for the true distribution. Robust optimization protects against this by requiring the constraint to hold for every probability vector in an uncertainty region around the estimate.

A natural region is a ball in a φ-divergence, a family of statistical distances between probability vectors that contains the Kullback–Leibler divergence, the Burg entropy, the χ² distances, the Hellinger distance and the variation distance. Such balls arise as asymptotic confidence sets for the true distribution given observed frequencies (Pardo 2006), so the radius has a statistical meaning. Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) showed that the robust version of a linear constraint over such a ball is equivalent to a finite convex system involving the convex conjugate of φ. This reformulation is a standard tool in the later literature on distributionally robust optimization.

Setting

A φ-divergence function is a function $\phi:\mathbb R\to\mathbb R\cup\{+\infty\}$ that is convex on $[0,\infty)$ , finite on $(0,\infty)$ , and satisfies $\phi(1)=0$ ; the value $\phi(0)$ may be $+\infty$ . Examples are $\phi(t)=t\log t-t+1$ (Kullback–Leibler), $\phi(t)=-\log t+t-1$ (Burg), $\phi(t)=(t-1)^2$ (modified χ²) and $\phi(t)=|t-1|$ (variation). For $p,q\in\mathbb R^m$ with $q>0$ the φ-divergence is

I_\phi(p,q)=\sum_{i=1}^m q_i\,\phi\!\left(\frac{p_i}{q_i}\right),

and the conjugate of $\phi$ is $\phi^*(s)=\sup_{t\ge0}\{st-\phi(t)\}$ , a function with values in $\mathbb R\cup\{+\infty\}$ .

Fix $a\in\mathbb R^n$ , $B\in\mathbb R^{n\times m}$ with columns $b_i$ , $\beta\in\mathbb R$ , $C\in\mathbb R^{k\times m}$ with columns $c_i$ , $d\in\mathbb R^k$ , a nominal vector $q\in\mathbb R^m$ and a radius $\rho>0$ . The uncertainty region is

U=\{p\in\mathbb R^m\mid p\ge0,\ Cp\le d,\ I_\phi(p,q)\le\rho\},

where the linear constraints $Cp\le d$ can encode $e^\top p=1$ and any further information on $p$ . A decision $x\in\mathbb R^n$ satisfies the robust linear constraint if

(a+Bp)^\top x\le\beta\qquad\text{for all }p\in U. \tag{11}

Inequalities between vectors are componentwise throughout.

Formalization targets

Goal: Theorem 1

Assume $q>0$ and $q\in U$ . Then $x$ satisfies (11) if and only if there are $\eta\in\mathbb R^k$ and $\lambda\in\mathbb R$ with

a^\top x+d^\top\eta+\rho\lambda+\lambda\sum_{i}q_i\,\phi^*\!\left(\frac{b_i^\top x-c_i^\top\eta}{\lambda}\right)\le\beta,\qquad\eta\ge0,\ \lambda\ge0, \tag{13}

where $0\phi^*(s/0):=0$ for $s\le0$ and $0\phi^*(s/0):=+\infty$ for $s>0$ . The statement fixes no constants and no particular φ; it holds for the whole class.

Milestones

The proof in the paper has three displayed steps, which are the milestones. With the Lagrange function $L(p,\lambda,\eta)=(a+Bp)^\top x+\rho\lambda-\lambda I_\phi(p,q)+\eta^\top(d-Cp)$ and the dual objective $g(\lambda,\eta)=\sup_{p\ge0}L(p,\lambda,\eta)$ :

Closing identity. For $\lambda\ge0$ , $(\lambda\phi)^*(s)=\sup_{t\ge0}\{st-\lambda\phi(t)\}$ equals $\lambda\phi^*(s/\lambda)$ , with the convention above at $\lambda=0$ .
Eq. (15). For $q>0$ and $\lambda\ge0$ ,

g(\lambda,\eta)=a^\top x+d^\top\eta+\rho\lambda+\sum_{i=1}^m q_i(\lambda\phi)^*(b_i^\top x-c_i^\top\eta).

Duality. Under the hypotheses of Theorem 1, $x$ satisfies (11) if and only if $g(\lambda,\eta)\le\beta$ for some $\lambda\ge0$ , $\eta\ge0$ . This is split into the weak-duality direction and the strong-duality direction with attainment.

An additional item states Corollary 1, the specialization to $U=\{p\ge0,\ e^\top p=1,\ I_\phi(p,q)\le\rho\}$ , where the multiplier $\eta\in\mathbb R$ of the normalization is free in sign.

Significance

Theorem 1 turns a semi-infinite constraint, one inequality for each $p$ in a convex set, into a single convex inequality in $(x,\lambda,\eta)$ . The left side of (13) is jointly convex because $\lambda\phi^*(s/\lambda)$ is the perspective of a convex function. For the divergences of Table 4 of the paper the conjugate has a closed form, and the robust constraint becomes a linear, conic quadratic or self-concordant-barrier-representable constraint. The paper's applications (robust asset pricing, a robust newsvendor, and the tractability results of its §5) all start from this theorem, as do its Corollaries 2–5.

The theorem is proved in the paper; no machine-checked proof of it is known. Formalizing it adds a checked robust-counterpart theorem for φ-divergence regions, a reusable encoding of φ-divergences with extended values, and a strong-duality statement with attainment for convex programs whose constraint function takes the value $+\infty$ on the boundary of the orthant. It also records a correction: the paper states the theorem for $q\ge0$ , and that version is false (see Formalization scope).

Difficulty

The separation step (15) and the conjugate identity are elementary manipulations of suprema, but in extended arithmetic: $\phi$ may be $+\infty$ at $0$ , the conjugate may be $+\infty$ , and the case $\lambda=0$ follows its own convention. The central difficulty is the duality step. The worst-case problem is a convex program whose constraint $I_\phi(p,q)\le\rho$ is not a finite convex function on a closed set: for the Burg or χ² divergence it is $+\infty$ on the boundary of the orthant, and $U$ itself need not be closed. Textbook statements of Slater-type strong duality usually assume finite-valued convex functions on a closed domain, so they do not apply as stated. The statement also requires attainment of the dual minimum, not only the absence of a duality gap, and this is the part a naive limiting argument does not give.

Formalization scope

Conventions:

Vectors are Fin n → ℝ with the componentwise order; $B$ and $C$ are Matrix (Fin n) (Fin m) ℝ and Matrix (Fin k) (Fin m) ℝ; $b_i$ and $c_i$ are the columns fun j => B j i and fun j => C j i.
$\phi$ is ℝ → EReal, never $-\infty$ , finite on $(0,\infty)$ , with $\phi(1)=0$ and convexity on $[0,\infty)$ written out in EReal. $\phi(0)=+\infty$ is allowed, so the Burg, χ² and J divergences are covered.
$I_\phi(p,q)$ , $\phi^*$ , $(\lambda\phi)^*$ , $L$ , $g$ and the left side of (13) are EReal-valued. $\lambda\phi(t)$ is the EReal product, in which $0\cdot(+\infty)=0$ . The term $\lambda\phi^*(s/\lambda)$ is defined by an explicit case split at $\lambda=0$ , and $\lambda\sum_i q_i\phi^*(\cdot/\lambda)$ in (13) is read as $\sum_i q_i\,(\lambda\phi^*(\cdot/\lambda))$ with the convention applied term by term.
The paper's $\max_{p\ge0}$ in $g$ is a supremum; $\min_{\lambda,\eta\ge0}g\le\beta$ is stated in its attained form, $\exists\,\lambda\ge0,\eta\ge0$ with $g(\lambda,\eta)\le\beta$ .
$m$ and $k$ may be $0$ .

Corrected slip. The paper's standing assumption is $q\ge0$ . The third equality of (15) substitutes $p_i=q_it$ , which needs $q_i>0$ , and Theorem 1 is false for $q\ge0$ : with $m=k=2$ , $n=1$ , $\phi(t)=|t-1|$ , $q=(1,0)$ , both columns of $C$ equal to $(1,-1)^\top$ , $d=(1,-1)$ , $a=0$ , $B=(0\ \ 1)$ , $x=1$ , $\rho=1$ , $\beta=0$ , the vector $p=(1/2,1/2)$ lies in $U$ and violates (11), while $\eta=0$ , $\lambda=0$ satisfy (13). Every statement of the mission therefore assumes $q_i>0$ for all $i$ . The hypothesis $q\in U$ (the paper's "such that $q\in U$ ") and $\rho>0$ are kept.

Ruled-out trivializations: a conjugate taken as a supremum over all $t\in\mathbb R$ of a real-valued φ with junk values at $t<0$ is a different function; computing the $\lambda=0$ term as $0\cdot\phi^*(s/0)$ with Lean's $s/0=0$ makes it identically $0$ ; a real-valued, everywhere finite φ silently excludes the Burg, χ² and J divergences; dropping $q\in U$ or $\rho>0$ removes the Slater point and changes the theorem. The mission's definitions avoid all four.

Needed infrastructure: suprema of EReal-valued families over half-lines and orthants, the interchange of a supremum over a product with a finite sum, and a Lagrangian strong-duality theorem with attainment for a convex program with finitely many affine inequality constraints and one convex, possibly infinite-valued, inequality constraint with a Slater point in the interior of its domain. That duality theorem, and the φ-divergence definitions, are reusable beyond this mission, in particular for the paper's Corollaries 2–5 and for other distributionally robust formulations. Contributions of any of these pieces as separate theorems are welcome.

Selected references

A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
L. Pardo, Statistical Inference Based on Divergence Measures, Chapman & Hall/CRC, 2006. https://doi.org/10.1201/9781420034813
A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

12 thms2 active usersReviewed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Open, Closed, and Mixed Networks of Queues with Different Classes of Customers: The Product-Form Equilibrium DistributionResearch Paper

Motivation

Networks of queues model computer systems, communication networks and manufacturing lines: customers (jobs, packets, parts) move between service centers, wait, receive service and move on. Their equilibrium behaviour determines throughputs, utilizations and response times, and for most networks it can only be computed by solving the full balance equations of a continuous-time Markov chain whose state space grows combinatorially with the number of centers and customers. A product-form network is one whose equilibrium distribution factorizes over the centers; for such networks performance measures can be computed exactly by efficient algorithms (convolution, mean value analysis), and this is the basis of much of classical computer-performance modelling.

Timeline of the main product-form results:

1957–1963, Jackson (Oper. Res. 5, 1957; Manag. Sci. 10, 1963): open networks of exponential FCFS queues, one customer class, Poisson arrivals.
1967, Gordon and Newell (Oper. Res. 15): the closed single-class exponential case.
1975, Baskett, Chandy, Muntz and Palacios (J. ACM 22): several customer classes with class switching, four service disciplines (FCFS, processor sharing, infinite server, preemptive-resume LCFS), service times with rational Laplace transforms at the last three, and open, closed or mixed networks with state-dependent Poisson arrivals. This is the BCMP theorem, the subject of this mission.
1975–1979, Kelly (J. Appl. Prob. 12, 1975; Reversibility and Stochastic Networks, Wiley 1979): symmetric queues and quasi-reversibility, a general framework containing the BCMP disciplines.

Setting

A network has $N$ service centers and $R$ customer classes. A class- $r$ customer finishing service at center $i$ next requires center $j$ in class $s$ with probability $p_{i,r;j,s}$ and leaves the network with probability $1-\sum_{j,s}p_{i,r;j,s}$ . The pairs $(i,r)$ are partitioned into subchains $E_1,\dots,E_m$ that routing never leaves. Each center has one of four types:

FCFS, with an exponential service time of rate $\mu_i$ common to all classes;
a single processor-sharing server (each of $n$ customers is served at rate $1/n$ );
an infinite-server center;
a single preemptive-resume LCFS server.

At types 2–4 the class- $r$ service time is Coxian: $u_{ir}\ge1$ exponential stages of rates $\mu_{irl}$ , and after stage $l$ the customer continues with probability $a_{irl}$ or finishes with probability $b_{irl}=1-a_{irl}$ . The state $S=(x_1,\dots,x_N)$ records the FCFS order of classes at type 1, the number $m_{irl}$ of class- $r$ customers in stage $l$ at types 2 and 3, and the LCFS order of (class, stage) pairs at type 4. External arrivals are Poisson, either with rate $\lambda(M(S))$ depending on the total population $M(S)$ (process A) or with one stream per subchain of rate $\lambda_k(M(S/E_k))$ (process B); an arrival joins center $j$ in class $s$ with probability $q_{js}$ . A subchain with $q\equiv0$ is closed and keeps a fixed population $K_k$ .

With relative arrival rates $e_{ir}\ge0$ solving the traffic equations $\sum_{(i,r)}e_{ir}p_{i,r;j,s}+q_{js}=e_{js}$ and $A_{irl}=\prod_{j<l}a_{irj}$ (the probability of reaching stage $l$ , stages numbered from 0), the paper defines $f_i(x_i)$ per center type and a factor $d(S)$ from the arrival rates.

Formalization targets

Goal: the BCMP theorem (§3.2, pp. 253–254)

\pi(S)=d(S)\,f_1(x_1)\,f_2(x_2)\cdots f_N(x_N)

satisfies the global balance equations of the network, and, under the paper's assumption that the equilibrium distribution is unique, every equilibrium distribution equals $\pi/Z$ whenever $Z=\sum_S\pi(S)$ is finite and positive. The goal covers all four center types, open, closed and mixed networks, and both arrival processes.

Milestones

§3.1 (p. 252): independent balance implies global balance.
§3.2 (p. 254): the product form satisfies the independent balance equations.
§4.1 (p. 254): the aggregate-state probabilities are $C\,d(S)\,g_1(y_1)\cdots g_N(y_N)$ .

A further supporting item, also from §4.1 (p. 254), states that summing $f_i$ over local states with fixed class counts gives $g_i$ . So $g_i$ depends on the service times only through their means $1/\mu_{ir}=\sum_lA_{irl}/\mu_{irl}$ .

Significance

The theorem places the four disciplines, class switching and mixed open/closed populations under one formula. Its corollary in §4.1, that aggregate probabilities depend on service time distributions only through their means (insensitivity), is what makes the model usable with measured mean service times, and it underlies the convolution and mean value analysis algorithms for normalizing constants.

The result is classical and proved on paper. As far as the platform's catalogue shows, it is not formalized: the platform has Kelly's single-class migration process with exponential service, a special case. A machine-checked BCMP theorem would provide a verified multiclass queueing-network model (states, event-driven transition rates, balance equations) on which later results can build: mean value analysis, the state-dependent rates of §5, and the open-network marginals of §4.2.

The printed statement contains an error. The paper defines $A_{irl}=\prod_{j=1}^{l}a_{irj}$ (p. 253). With the branching of its Figs. 1 and 3, this product includes the branch out of stage $l$ . For exponential service ( $u_{ir}=1$ ) it gives $A_{ir1}=a_{ir1}=0$ , so every $f_i$ of a type 2–4 center with a customer present vanishes, and a closed network of such centers would have no normalizable solution. The mission states the corrected theorem with $A_{irl}=\prod_{j<l}a_{irj}$ , which the mean-service-time identity of §4.1 also requires. The type-2 factor $1/m_{ikl}!$ is read as $1/m_{irl}!$ .

Difficulty

The algebra of the paper's proof is local: each independent balance equation reduces to the traffic equations. The difficulty is in making that statement precise for a real state space. The independent balance equations need a consistent labelling of each moving customer by the "stage" it leaves and enters. That labelling has to cover FCFS centers, where per-class labels are inconsistent (p. 253), the outside world of each open subchain, and LCFS preemption. Every in-flow into a state is a sum over predecessor states, and those states differ by list operations (appending at an FCFS tail, pushing on an LCFS head) or by stage-count updates. The factorials in the processor-sharing and infinite-server factors, and the telescoping identity $\sum_lA_{irl}b_{irl}=1$ for departures, must line up exactly with the rates. The obvious shortcut is to check global balance directly for a single class with exponential service. That covers neither class switching, nor Coxian stages, nor mixed networks.

Formalization scope

Centers are Fin N, classes Fin R and subchains Fin m. The class- $r$ stages at center $i$ are Fin (u i r) with u i r : ℕ+, numbered from 0. A local state is an inductive type with three shapes (FCFS list, stage-count array, LCFS list of (class, stage) pairs). The state space is the subtype of configurations whose shapes match the center types and whose closed subchains hold their fixed populations. Transition rates are the sums of the rates of explicit events (arrivals, FCFS completions, stage moves and completions, LCFS moves and completions). Global balance uses tsum; every state has finitely many successors and predecessors with nonzero rate, so these sums are finite. The standing assumptions (substochastic routing closed on subchains, closed subchains with no arrivals and no departures, positive rates, continuation probabilities in $[0,1]$ vanishing at the last stage) are collected in Network.IsValid. Irreducibility of subchains is not assumed, and any nonnegative solution of the traffic equations is allowed. Under process B the product in $d(S)$ runs over open subchains only. Uniqueness of the equilibrium is a hypothesis, as in the paper. The type-1 rate is constant, and the state-dependent rates of Condition 1 and §5 are not covered.

The following formalizations would trivialize the mission and are ruled out: stating only global balance of $\pi$ (satisfied by $\pi\equiv0$ ), quantifying over arbitrary rate functions instead of the rates built from the network data, and restricting the goal to exponential service or to a single class.

Needed infrastructure: finite-support tsum manipulations, multinomial identities for the §4.1 sums over orderings and stage assignments, and bookkeeping for list and array updates. The model and the balance-equation layer can be reused for later queueing missions. Contributions are welcome on each milestone, on the per-center-type pieces of the independent balance check, and on helper lemmas about the event system.

Selected references

F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, Closed, and Mixed Networks of Queues with Different Classes of Customers, J. ACM 22(2):248–260, 1975. https://doi.org/10.1145/321879.321887
J. R. Jackson, Networks of Waiting Lines, Operations Research 5(4):518–521, 1957. https://doi.org/10.1287/opre.5.4.518
J. R. Jackson, Jobshop-like Queueing Systems, Management Science 10(1):131–142, 1963. https://doi.org/10.1287/mnsc.10.1.131
W. J. Gordon, G. F. Newell, Closed Queuing Systems with Exponential Servers, Operations Research 15(2):254–265, 1967. https://doi.org/10.1287/opre.15.2.254
F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979. http://www.statslab.cam.ac.uk/~frank/rsn.html
D. R. Cox, A Use of Complex Probabilities in the Theory of Stochastic Processes, Proc. Cambridge Phil. Soc. 51:313–319, 1955. https://doi.org/10.1017/S0305004100030231

9 thms2 active usersReviewed

Dynamic Programming Probability·Captain: mikedeng1

Coherent Multiperiod Risk Adjusted Values and Bellman's Principle: Stability of the Test Probabilities Is Equivalent to Bellman's PrincipleResearch Paper

Motivation

A coherent risk measure assigns to a future financial position the smallest amount of capital that makes it acceptable to a supervisor. Artzner, Delbaen, Eber and Heath characterised the one-period version: every coherent risk measure has the form $\pi(X)=\inf_{\mathbb Q\in\mathcal P}\mathbb E_{\mathbb Q}[X]$ for a set $\mathcal P$ of test probabilities (ADEH 1999). Regulators, insurers and banks, however, assess positions that evolve over several periods and whose risk is re-evaluated as information arrives. A multiperiod measurement should then be time consistent: the value assigned today should agree with the values the same method assigns tomorrow, so that it can be computed by backward induction, as in dynamic programming.

Artzner, Delbaen, Eber, Heath and Ku (Ann. Oper. Res. 2007) identify exactly which sets of test probabilities give time-consistent multiperiod risk-adjusted values. The condition, stability under pasting, also appears as "rectangularity" in the recursive multiple-priors model of decision theory (Epstein and Schneider 2003), and as m-stability in the theory of risk-neutral measures (Delbaen, The structure of m-stable sets, Séminaire de Probabilités XXXIX, 2006). Riedel treated dynamic coherent risk measures on finite state spaces (Riedel 2004); the continuous-time case is in Delbaen's m-stable paper and Cheridito, Delbaen and Kupper 2004.

Setting

Let $(\Omega,\mathcal F,\mathbb P_0)$ be a probability space with a filtration $(\mathcal F_n)_{n\ge0}$ and a horizon $N$ . A value process is an adapted process $X=(X_n)_{0\le n\le N}$ with every $X_n$ essentially bounded; the class of value processes is $\mathcal G$ . All stopping times take values in $\{0,\dots,N\}$ , and $\mathcal F_\sigma$ is the σ-algebra of the stopping time $\sigma$ .

A set $\mathcal P$ of test probabilities is a closed convex set of probabilities on $(\Omega,\mathcal F_N)$ , each absolutely continuous with respect to $\mathbb P_0$ . Its elements are identified with their densities $f=d\mathbb Q/d\mathbb P_0$ , and "closed" refers to $L^1(\mathbb P_0)$ . $\mathcal P^e$ denotes the elements equivalent to $\mathbb P_0$ . Each $\mathbb Q\in\mathcal P$ has the density martingale $Z^{\mathbb Q}_n=\mathbb E_{\mathbb P_0}[d\mathbb Q/d\mathbb P_0\mid\mathcal F_n]$ .

Pasting. For $\mathbb Q^0,\mathbb Q\in\mathcal P^e$ with density martingales $Z^0,Z$ and a stopping time $\tau$ , the pasted martingale is $L_n=Z^0_n$ for $n\le\tau$ and $L_n=Z^0_\tau Z_n/Z_\tau$ for $n\ge\tau$ : the pasted probability follows $\mathbb Q^0$ up to $\tau$ and $\mathbb Q$ afterwards. $\mathcal P$ is stable (Definition 3.1) if every such pasting is again in $\mathcal P$ .

Two risk-adjusted values. For a value process $X$ and a stopping time $\sigma$ ,

\Psi_\sigma(X)=\operatorname*{ess.inf}\bigl\{\mathbb E_{\mathbb Q}[X_\tau\mid\mathcal F_\sigma]\ \bigm|\ \tau\ge\sigma\text{ a stopping time},\ \mathbb Q\in\mathcal P^e\bigr\},

the worst conditional expected value over all test probabilities and all later stopping times. The generalized Snell envelope is the backward recursion

\bar\Psi_N(X)=X_N,\qquad \bar\Psi_n(X)=X_n\wedge\operatorname*{ess.inf}_{\mathbb Q\in\mathcal P^e}\mathbb E_{\mathbb Q}\bigl[\bar\Psi_{n+1}(X)\mid\mathcal F_n\bigr].

For a stopping time $\tau$ let $X^{\tau-}_n=X_n$ for $n<\tau$ and $X_{\tau-1}$ for $n\ge\tau$ , and ${}^\tau X_n=0$ for $n<\tau$ and $X_n-X_{\tau-1}$ for $n\ge\tau$ .

Formalization targets

Goal: Theorem 4.2

Assume $\mathcal F_0$ is $\mathbb P_0$ -trivial and $\mathcal P^e\neq\emptyset$ . Then the following are equivalent:

$\mathcal P$ is stable.
For every $\mathbb Q\in\mathcal P$ and $X\in\mathcal G$ , $\Psi(X)$ is a $\mathbb Q$ -submartingale.
$\Psi(X)=\bar\Psi(X)$ for every $X\in\mathcal G$ .
Bellman's principle holds: for every $X\in\mathcal G$ and all stopping times $\sigma\le\tau$ ,

\Psi_\sigma(X)=\Psi_\sigma\bigl(X^{\tau-}+\Psi_\tau({}^\tau X)\mathbf 1_{[\tau,N]}\bigr).

Milestones

In attack order, all stated for any set $\mathcal P$ with $\mathcal P^e\neq\emptyset$ unless stability is named:

Theorem 4.1. $\bar\Psi(X)$ is the largest process in $\mathcal G$ that lies below $X$ and is a $\mathbb Q$ -submartingale for every $\mathbb Q\in\mathcal P$ .
Step (1) of the proof of Theorem 4.2. $\Psi_n(X)\ge\bar\Psi_n(X)$ .
Theorem 4.2, first sentence. The family $(\Psi_\sigma(X))_\sigma$ is a process: $\Psi_\sigma(X)=\Psi_{\sigma(\omega)}(X)(\omega)$ a.s.
Remark after Theorem 4.2. $\Psi_\tau(X)=\Psi_\tau({}^\tau X)+X_{\tau-1}$ .
Lemma 3.1 (stable $\mathcal P$ ). For $\tau\le\sigma\le\nu$ , $\{(Z_\nu/Z_\sigma,Z_\sigma/Z_\tau)\mid Z\in\mathcal P^e\}=\{(Z'_\nu/Z'_\sigma,Z_\sigma/Z_\tau)\mid Z,Z'\in\mathcal P^e\}$ .
Lemma 4.1 (stable $\mathcal P$ ). The family defining $\Psi_\sigma(X)$ is closed under minima and maxima.
Corollary of Lemma 4.1 (stable $\mathcal P$ ). $\mathbb E_\mu[\Psi_\sigma(X)]=\inf\{\mathbb E_\mu[\mathbb E_{\mathbb Q}[X_\tau\mid\mathcal F_\sigma]]\mid\mathbb Q\in\mathcal P^e,\ \tau\ge\sigma\}$ for every probability $\mu\ll\mathbb P_0$ .

A supporting item states that the essential infimum defining $\Psi_\sigma(X)$ exists.

Significance

The result. Theorem 4.2 characterises the sets of test probabilities for which the natural worst-case risk-adjusted value is computable by dynamic programming. Stability is thereby the structural condition behind time-consistent coherent risk measurement, recursive multiple-priors utility and backward-induction pricing under ambiguity. Without it, the worst-case value computed today may disagree with the value obtained by first computing tomorrow's worst case and then today's. The equivalence with the submartingale property says that stability is also exactly what makes $\Psi(X)$ the largest submartingale minorant of Theorem 4.1. Theorem 4.3 and the recursivity results for final values in Section 5 are corollaries.

Formalizing it. The paper's proof is complete apart from Lemma 4.1 and its Corollary, whose proofs are left to the reader. No machine-checked version of this result, of the generalized Snell envelope or of essential infima of families of random variables is known to exist. A formal proof would provide a reusable development of discrete-time optimal stopping under a set of probabilities, the essential-infimum calculus of Neveu, and density-martingale pasting — infrastructure that many results on robust optimal stopping, dynamic risk measures and robust Markov decision processes need.

Difficulty

The direction from stability to Bellman's principle needs an essential infimum to be exchanged with a conditional expectation under another probability (step (3) of the proof). This is false for a general family: an essential infimum of conditional expectations is not the conditional expectation of an essential infimum. The exchange works only because stability makes the family closed under minima (Lemma 4.1), so that it is directed downward and its essential infimum is the limit of a decreasing sequence, and because Lemma 3.1 lets the test probabilities used before and after $\tau$ be chosen independently. The converse, from the submartingale property to stability, is not a computation: it uses the separation theorem in $L^1$ against a pasted density assumed outside $\mathcal P$ , which is where convexity and $L^1$ -closedness of $\mathcal P$ are used. Dropping either hypothesis breaks that direction.

Formalization scope

Lean represents $\mathcal P$ by its set of densities in $\mathbb P_0$ : $\mathcal F_N$ -measurable, a.s. nonnegative, integrable, of mass one, convex, sequentially closed in the $L^1(\mathbb P_0)$ seminorm and saturated under a.s. equality. Test probabilities are $\mathbb Q_f=f\cdot\mathbb P_0$ , and $\mathbb E_{\mathbb Q}[\cdot\mid\mathcal F_\sigma]$ is Mathlib's conditional expectation under $\mathbb Q_f$ . Time is $\mathbb N$ , and every stopping time is bounded by $N$ . A $\mathbb Q$ -submartingale on $0,\dots,N$ is Mathlib's Submartingale of the process frozen after $N$ . The essential infimum of a family is defined in the mission (Mathlib has only that of a single function); a supporting item shows that it exists, so its fallback value is never used. All identities between risk-adjusted values hold $\mathbb P_0$ -almost surely.

Conventions made explicit:

the goal assumes that $\mathcal F_0$ is $\mathbb P_0$ -trivial, which the proof uses when it treats $\Psi_0(X)$ as a number (without it, stability is not implied by (2)–(3));
$\mathcal P^e\neq\emptyset$ replaces the paper's convenience assumption $\mathbb P_0\in\mathcal P$ ;
$X_{-1}=0$ ;
the Corollary's printed essential infimum over $\mathbb Q$ alone is read over $\mathbb Q$ and $\tau\ge\sigma$ , as its right-hand side and its use require.

Bellman's principle must be stated with $\Psi$ on both sides and for all stopping times $\sigma\le\tau$ . Replacing $\Psi$ by $\bar\Psi$ , or restricting to deterministic times, turns the goal into a property of the recursion and is not the theorem.

Needed infrastructure, reusable beyond this mission: existence and directedness of essential infima of families; conditional expectations under equivalent measures and the Bayes formula; optional sampling for bounded stopping times under each $\mathbb Q$ ; the $L^1$ – $L^\infty$ separation theorem. Contributions of any of these, and proofs of the milestones in any order, are welcome.

Selected references

P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, H. Ku, Coherent multiperiod risk adjusted values and Bellman's principle, Annals of Operations Research 152 (2007) 5–22. https://doi.org/10.1007/s10479-006-0132-6
P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9 (1999) 203–228. https://doi.org/10.1111/1467-9965.00068
L. G. Epstein, M. Schneider, Recursive multiple-priors, Journal of Economic Theory 113 (2003) 1–31. https://doi.org/10.1016/S0022-0531(03)00097-8
F. Riedel, Dynamic coherent risk measures, Stochastic Processes and their Applications 112 (2004) 185–200. https://doi.org/10.1016/j.spa.2004.03.004
P. Cheridito, F. Delbaen, M. Kupper, Coherent and convex monetary risk measures for bounded càdlàg processes, Stochastic Processes and their Applications 112 (2004) 1–22. https://doi.org/10.1016/j.spa.2004.01.009
F. Delbaen, The structure of m-stable sets and in particular of the set of risk neutral measures, Séminaire de Probabilités XXXIX, Lecture Notes in Mathematics 1874 (2006) 215–258. https://doi.org/10.1007/978-3-540-35513-7_17
J. Neveu, Discrete-Parameter Martingales, North-Holland, 1975 (French original: Martingales à temps discret, Masson, 1972).
Y. S. Chow, H. Robbins, D. Siegmund, Great Expectations: The Theory of Optimal Stopping, Houghton Mifflin, 1971; Dover reprint, 1991.

12 thms2 active usersReviewed

Completed

Mechanism Design·Captain: naimengye

Fundamentals of Supply Chain Theory XIII: AuctionsTextbook

When is the auctioneer's revenue acceptable?

The Vickrey-Clarke-Groves auction is the textbook mechanism for selling several objects at once: bidders report valuations for bundles, the auctioneer computes the welfare-maximizing allocation, and each winner pays the externality it imposes on the others. Truthful bidding is a dominant strategy and the outcome is efficient. Yet Ausubel and Milgrom (2006) catalogued its practical defects: revenue can be zero when the objects are valuable, revenue can fall when bidders or bids are added, losing bidders can profit by colluding, and a bidder can profit from false identities. Chapter 15 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) reproduces those examples and then gives the cooperative-game answer to when they cannot occur: the VCG payoff vector should lie in the core, the set of outcomes no coalition of auctioneer and bidders can improve upon, and it does so for every set of participants exactly when the coalitional value function is bidder-submodular. This mission formalizes that characterization, Theorem 15.3, together with the lemma and theorem leading to it.

Setting

Players are the auctioneer $0$ and bidders $1, \dots, n$ . A coalitional value function $V$ assigns to each coalition $T$ the value it can create by trading among themselves: $0$ if the auctioneer, who owns the objects, is not in $T$ , and otherwise the optimal value of the auctioneer's allocation problem among the bidders of $T$ , each bidder receiving at most one bundle and bundles disjoint (capValue). Two properties of $V$ are all the theory uses: coalitions without the auctioneer are worthless, and adding players never lowers the value (IsCoalitionalValue).

A payoff vector $\pi$ gives each player a payoff. It lies in the core of the game on a coalition $S \ni 0$ (InCore V S π) if the payoffs of $S$ sum to $V(S)$ and no sub-coalition $T \subseteq S$ is paid less than $V(T)$ . The VCG payoff vector $\bar\pi(S)$ (vcgPayoff) pays each bidder $k$ its marginal contribution $V(S) - V(S \setminus k)$ , which is its valuation minus its VCG payment, and the auctioneer the remainder. A core vector is bidder dominant (BidderDominant) if every bidder weakly prefers it to every other core vector. $V$ is bidder-submodular (BidderSubmodular) if each bidder's marginal contribution weakly decreases as the coalition grows.

Formalization targets

Goal: Theorem 15.3

For a coalitional value function $V$ , the following are equivalent: (i) $V$ is bidder-submodular; (ii) for every coalition $S \ni 0$ the core equals $\Pi_S = \{\pi : \sum_{k \in S}\pi_k = V(S),\ 0 \le \pi_k \le \bar\pi_k(S)\ \forall k \in S \setminus 0\}$ ; (iii) for every coalition $S \ni 0$ , $\bar\pi(S)$ lies in the core of $S$ . This is vcg_core_characterization.

Supporting targets

That the combinatorial auction's $V$ is a coalitional value function; Lemma 15.1, the core is nonempty and each bidder's VCG payoff is the largest it receives at any core point; Theorem 15.2, the VCG vector is the bidder-dominant core point when it is in the core, and otherwise no bidder-dominant point exists and the auctioneer's VCG payoff is below every core payoff.

The English auction of Sect. 15.2, presented as a primal-dual interpretation of a linear program, and the combinatorial allocation problem of Sect. 15.3 carry no numbered results and are not targets.

Significance

Theorem 15.3 is the criterion an auction designer can check before running a VCG auction: when the bidders' valuations make $V$ bidder-submodular (for instance when objects are substitutes), the VCG outcome is a competitive outcome, its revenue meets the core benchmark, and none of the defects of Sect. 15.4.2 can arise; when they do not, Theorem 15.2 says the auctioneer's revenue is strictly below every competitive outcome. The result underlies the ascending package auctions proposed as VCG alternatives and the procurement auctions used in supply chains, such as the combinatorial reverse auctions of the chapter's case study.

None of these results has a machine-checked proof. The book proves all three. The formal treatment of the core and of marginal-contribution vectors is reusable for the cooperative-game models of cost allocation in supply chains.

Difficulty

The theorems are combinatorial statements about a function on finite sets, and the difficulty is entirely in the bookkeeping of coalitions. Lemma 15.1 needs the explicit core vector of its proof to be verified against every sub-coalition, which splits into cases on whether the sub-coalition contains the auctioneer and the distinguished bidder. The implication (i) $\Rightarrow$ (ii) telescopes marginal contributions along a chain of coalitions between a sub-coalition and $S$ , and the chain has to be built and its sum computed. The implication (iii) $\Rightarrow$ (i) is the delicate one: a failure of submodularity is a pair of nested coalitions, and the proof needs to extract from it a single-element step at which a bidder's marginal contribution increases, then show the two-bidder sub-coalition blocks the VCG vector. The obvious idea, that submodularity can be checked only on single-element extensions, is correct but must itself be proved.

Formalization scope

Coalitions are finite sets of Fin (n+1) and payoff vectors are functions on all players; the core and $\Pi_S$ constrain only the players of $S$ , so vectors differing outside $S$ are interchangeable. The core's budget equation sums over all players of the coalition, including the auctioneer, which is what the book's proofs use although its displayed definition sums over the bidders. The theorems take $V$ as any function with the two properties, and the auction's $V$ is shown to have them; the VCG vector is defined by the formulas (15.23) and (15.24) rather than through the payment rule, whose equivalence is the book's derivation. Bidder-submodularity is stated for $S \subseteq S'$ rather than proper inclusion, which changes nothing.

The definition module is shared by all five items. The single-item English auction as a primal-dual algorithm and the condition on individual preferences (substitutes) that implies bidder-submodularity are natural extensions on the same definitions.

Selected references

L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 15. https://doi.org/10.1002/9781119584445
L. M. Ausubel and P. Milgrom, The lovely but lonely Vickrey auction, in Combinatorial Auctions, MIT Press, 2006. https://doi.org/10.7551/mitpress/9780262033428.003.0002
S. de Vries and R. V. Vohra, Combinatorial auctions: a survey, INFORMS Journal on Computing 15(3), 2003. https://doi.org/10.1287/ijoc.15.3.284.16077
W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, Journal of Finance 16(1), 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x

5 thms2 active usersReviewed

Completed

Algorithmic Game Theory·Captain: naimengye

The Theory and Practice of Revenue Management V: CompetitionTextbook

When competing firms settle on prices and allocations

Revenue management is practised by firms that compete: airlines matching fares while allocating seats, retailers ordering stock and then pricing to clear it, hotels protecting rooms for late high-paying guests. Chapter 8 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) surveys the economics behind these situations: monopoly pricing and mechanism design, the Coase problem, advance-purchase discounts, and oligopoly in quantities (Cournot), in prices (Bertrand, Bertrand–Edgeworth with capacities), in newsvendor capacities and in RM allocations. Most of its numbered results are quoted from the literature; what the book itself establishes is a family of equilibrium arguments built on Talluri's equilibrium graph: when each firm's best response moves monotonically with the rival's action, following best-response arcs must end in an equilibrium pair. This mission formalizes those arguments, with Proposition 8.3, existence of an equilibrium in offer sets under the multinomial-logit choice model, as the goal.

Setting

A two-firm game on finite chains of strategies has payoffs $u_1, u_2$ , best responses and pure Nash equilibria (IsBestResponse1, IsNashEquilibrium); its equilibrium graph has no crossing arcs (NoCrossing1) when best-response arcs $(k_2, k_1)$ , $(l_2, l_1)$ with $k_2 < l_2$ always have $k_1 \le l_1$ . The chapter's games are: the RM duopoly of Sect. 8.4.1.3, two firms with capacity $C$ and fares $p_L < p_H$ whose high-fare demand spills over to the rival beyond its protection level (spilloverDemand), each firm answering with Littlewood's protection level (littlewoodResponse); the duopoly newsvendor of Example 8.16 with effective demands $R_1 = D_1 + (D_2 - x_2)^+$ (effectiveDemand); linear Cournot (cournotPayoff); Bertrand–Edgeworth price competition with capacity $C$ per firm, linear demand and efficient rationing (beSales, bePayoff, IsBEEquilibrium); the advance-purchase model of Sect. 8.3.6 (peakLoadRevenue, advancePurchaseRevenue); and the one-period offer-set game of Sect. 8.4.3.2, where a firm offering its first $k$ products earns $g(C_k)/(W_1(k) + W_2(l) + w_0)$ with $g(C_k) = \sum_{j \le k} w_j(p_j - \Delta) - w_0\delta$ (OfferFirm, offerPayoff1, CaseI, CaseII).

Formalization targets

Goal: Proposition 8.3

If both firms are in Case I ( $g(G^*) \ge 0$ ) or both in Case II ( $g < 0$ on every complete set), the offer-set game has a pure-strategy equilibrium in complete sets: mnl_offer_set_equilibrium.

Supporting targets

The equilibrium-graph lemma, monotone best responses for both firms give an equilibrium (Sect. 8.4.1.3); Proposition 8.1, Littlewood responses in the RM duopoly are monotone in the rival's protection level, and the resulting equilibrium of the RM duopoly game; Example 8.16, duopoly newsvendor capacities total at least the monopoly capacity; Example 8.15, the symmetric Cournot equilibrium and its price; Theorem 8.5 (i)-(ii), the pure-strategy Bertrand–Edgeworth equilibria; and the advance-purchase comparison of Sect. 8.3.6, $w_2 < \hat w$ and $V_{APD}(\hat w) \ge V_{peak}(w_2)$ .

Not targets: Theorems 8.1-8.2 (the Coase problem, subgame-perfect equilibria of an infinite-horizon game, proofs in von der Fehr and Kühn), Theorem 8.3 (Harris–Raviv priority pricing, stated with a garbled price formula), Theorem 8.4 (existence via quasiconcavity, cited), Theorem 8.5 (iii), 8.6 and 8.7-8.8 (mixed-strategy and supergame equilibria of Kreps and Scheinkman and Benoit and Krishna), Proposition 8.2 and Proposition 8.4 (the dynamic offer-set game under condition (8.32), proved in Talluri's paper), and the Kreps–Scheinkman derivation of Sect. 8.4.1.6, which rests on Theorem 8.6.

Significance

The equilibrium graph is the chapter's own contribution: a bipartite picture of best responses on chains in which monotonicity, the absence of crossing arcs, forces an equilibrium. It is the finite, combinatorial form of the monotone comparative-statics route to Nash equilibrium (Tarski's fixed point on a chain), and it is what makes RM allocation games tractable: the two-class duopoly with Littlewood responses always has an equilibrium, and the offer-set duopoly does whenever the two firms face the same sign of $g$ , while Example 8.18 shows a best-response cycle when they do not. The Bertrand–Edgeworth, Cournot and newsvendor results are the benchmarks the book uses to interpret RM competition: capacity constraints soften Bertrand's zero-profit outcome, competing in allocations tends to raise total capacity above the monopoly level, and advance-purchase discounts dominate peak-load pricing as a self-selection mechanism. None of these has a machine-checked proof.

Difficulty

The lemma and the goal are fixed-point arguments on finite chains: the largest best response is a monotone map of the rival's index, the composition of two monotone (or two antitone) maps on a finite chain has a fixed point, and for the offer-set game the monotonicity itself must be extracted from the ratio structure $g(C_k)/(W(k) + a)$ as in the appendix's inequalities (8.A.3)-(8.A.5), separately in the two cases. Proposition 8.1 is a monotonicity of tail probabilities under the pointwise order of effective demands. Example 8.16 is a short probabilistic argument that needs the identity $\{D > x_1 + x_2\} = \{R_1 > x_1\} \cap \{R_2 > x_2\}$ and the strict monotonicity of the tail. Theorem 8.5 requires computing efficient-rationing sales for every unilateral deviation from a symmetric profile, through the recursive definition of residual demand, and a quadratic inequality for upward deviations in part (ii). The advance-purchase item reduces to the identity $V_{APD}(w) - V_{peak}(w) = (1 - \alpha)w$ and the strict decrease of the first-order-condition function.

Formalization scope

Products, protection levels and complete sets are natural numbers; the offer-set game's strategies are the complete sets $C_1, \dots, C_n$ of the book, and its payoff is (8.31) up to the positive factor $\lambda$ and the terms independent of both offer sets. Prices decreasing in the product index are a hypothesis, as the nested-by-revenue order of Sect. 8.4.3.2. The RM duopoly is modeled through Littlewood's response, as the book's appendix argues, rather than through expected revenues. Efficient rationing is defined recursively over the firms priced strictly below a given firm, with equal sharing among firms at the same price. Example 8.16 is stated with the equilibrium conditions (8.23) and the strictly increasing distribution of aggregate demand as hypotheses. The advance-purchase item takes the first-order conditions (8.13) and (8.15) and the book's uniqueness assumption as hypotheses, the latter as $(v - w) - F(w)/f(w)$ strictly decreasing in $w$ (the page prints "increasing", but its footnote identifies it with the monotone marginal-revenue assumption, which is decreasing in the waiting cost). Theorem 8.5 is stated for its pure-strategy parts (i) and (ii) only.

Selected references

K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 8. https://doi.org/10.1007/b139000
D. M. Kreps and J. A. Scheinkman, Quantity precommitment and Bertrand competition yield Cournot outcomes, Bell Journal of Economics 14(2), 1983. https://doi.org/10.2307/3003636
S. A. Lippman and K. F. McCardle, The competitive newsboy, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.54
S. Netessine and R. A. Shumsky, Revenue management games: horizontal and vertical competition, Management Science 51(5), 2005. https://doi.org/10.1287/mnsc.1040.0356
I. L. Gale and T. J. Holmes, Advance-purchase discounts and monopoly allocation of capacity, American Economic Review 83(1), 1993. https://www.jstor.org/stable/2117500
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

8 thms2 active usersReviewed

Completed

Combinatorics·Captain: naimengye

Fundamentals of Supply Chain Theory XII: The Vehicle Routing ProblemTextbook

Many vehicles, one depot

The vehicle routing problem asks for the cheapest set of delivery routes from a depot to a set of customers when each vehicle can carry only so much. It generalizes the traveling salesman problem, which is the case of a single vehicle of unlimited capacity, and it is the operational problem behind every distribution fleet. Exact methods reach a few hundred customers; the questions that shape fleet design are structural: how does the optimal routing cost compare with the cost of a single grand tour, and how does it grow with the number of customers? Haimovich and Rinnooy Kan (1985) answered both for unit demands by bounding the optimal cost above and below in terms of the optimal TSP tour and the average distance to the depot. Chapter 11 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) presents that result with its full proof as Theorem 11.6, and it is the goal of this mission.

Setting

Nodes are the depot $0$ and customers $1, \dots, n$ , with distances $c_{ij}$ that are symmetric, nonnegative and satisfy the triangle inequality (VRPMetric). Every customer has demand $1$ and every vehicle capacity $C$ , so a route is a sequence of at most $C$ distinct customers, served by one vehicle that leaves the depot, visits them in order and returns; its length is routeCost c L. A solution is a family of routes visiting every customer exactly once (IsVRPSolution), with total length solutionCost; the number of routes is free. The optimal VRP value $z^*$ (vrpOpt c C) is the least total length, the optimal TSP value $z_T$ (tspOpt c) is the least length of a single route through all customers, and $\bar c$ (avgDepotDist) is the average distance from the depot to a customer.

Formalization targets

Goal: Theorem 11.6

For every metric instance with $n \ge 1$ customers and capacity $C \ge 1$ ,

\max\Big\{2\frac{n}{C}\bar c,\ z_T\Big\} \;\le\; z^* \;\le\; 2\Big\lceil\frac{n}{C}\Big\rceil\bar c + \Big(1 - \frac{1}{C}\Big)z_T.

This is vrp_tsp_bounds.

Supporting targets

The three steps of the book's proof: the radial bound $2\frac{n}{C}\bar c \le z^*$ , obtained route by route from the triangle inequality and the capacity; the routing bound $z_T \le z^*$ ; and the iterated optimal tour partition bound (11.59), that for any tour $\Gamma$ through all customers some partition of its customer sequence into $\lceil n/C\rceil$ consecutive routes costs at most $2\lceil n/C\rceil\bar c + (1 - \lceil n/C\rceil/n)\,z(\Gamma)$ .

The chapter's other numbered results are not targets: Proposition 11.1 (state-space relaxation of the routing dynamic program) and Theorem 11.2 (the capacitated comb inequality, proof omitted, which needs the bin-packing function $v(S)$ ), and Theorems 11.3, 11.5, 11.7 and Lemma 11.4 (almost-sure asymptotics of random instances and the location-based heuristic), whose proofs the book cites.

Significance

Theorem 11.6 is the quantitative link between routing and the two things a planner can estimate without solving anything: the TSP length, which grows like $\sqrt{n}$ for random customers, and the average depot distance. It says that the VRP cost is the TSP cost plus a radial term $2\bar c$ per vehicle, and that this decomposition is exact up to a factor bounded by the capacity. The radial term explains Theorem 11.7, that the optimal cost grows linearly in $n$ for fixed capacity, and the tour partition heuristic in the proof is a practical route-first-cluster-second method with a provable guarantee. The bounds are the basis of the continuous approximation formulas used in strategic distribution design.

None of these results has a machine-checked proof. The book proves Theorem 11.6 in full. The formal treatment of routes as lists and of the averaging argument over rotations of a tour is reusable for the capacitated heuristics of Sect. 11.3.

Difficulty

The upper bound is an averaging argument that is easy to state and fiddly to formalize: for each of the $n$ rotations of the tour's customer sequence, the sequence is cut into blocks of $C$ , and one must count, across all rotations, how often each customer is the first or last of a block and how often each tour edge is cut. The counts, $\ell = \lceil n/C\rceil$ each, hold only after the rotations are indexed carefully, and the passage from the average to the best rotation needs the sum of the $n$ solution costs computed exactly.

The lower bound has two parts with different flavors. The radial part needs, for each route, that the closed route from the depot is at least twice the largest depot distance among its customers, which is the triangle inequality applied along the route, followed by an averaging step that uses the capacity. The routing part is a shortcutting argument: the routes of a solution concatenate into a closed walk that revisits the depot, and removing the repeated depot visits must not increase the length. The obvious idea, that a VRP solution is itself a tour, is false, and the shortcut has to be constructed.

Formalization scope

Routes are lists of customers, solutions are lists of routes, and the feasibility predicate requires nonempty routes of length at most $C$ avoiding the depot, with the concatenation of all routes a duplicate-free list containing every customer. Costs use the closed walk through the depot followed by the route. The optimal values are infima of finite nonempty sets of reals, nonempty because singleton routes are feasible when $C \ge 1$ . The ceiling $\lceil n/C\rceil$ is Mathlib's Nat.ceil of the real quotient. The number of vehicles is unrestricted, as the section assumes; the fixed-fleet version of the problem is not modeled.

The TSP value $z_T$ is defined as the least route cost over all orderings of the customers, so no separate tour model is needed and the mission does not depend on the TSP mission of this series.

The definition module is shared by all five items. Problem 11.18 (tightness of both bounds) and Theorem 11.7 for deterministic instance families are natural extensions on the same definitions.

Selected references

L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 11. https://doi.org/10.1002/9781119584445
M. Haimovich and A. H. G. Rinnooy Kan, Bounds and heuristics for capacitated routing problems, Mathematics of Operations Research 10(4), 1985. https://doi.org/10.1287/moor.10.4.527
P. Toth and D. Vigo (eds.), Vehicle Routing: Problems, Methods, and Applications, 2nd ed., SIAM, 2014. https://doi.org/10.1137/1.9781611973594

5 thms2 active usersReviewed

Completed

Combinatorics·Captain: naimengye

Fundamentals of Supply Chain Theory XI: The Traveling Salesman ProblemTextbook

The problem every routing model contains

A salesman must visit $n$ cities and return home by the shortest route. The traveling salesman problem is the prototype of combinatorial optimization: easy to state, NP-hard (Karp 1972), and solved to optimality on instances with tens of thousands of nodes by branch-and-cut. In a supply chain it is the core of every vehicle routing model and of the location-routing models of the chapters that follow. Chapter 10 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) covers the symmetric metric TSP, in which distances satisfy the triangle inequality: the cutting planes of branch-and-cut (comb inequalities), the construction heuristics with their worst-case guarantees, culminating in Christofides' (1976) 3/2-approximation, and the lower bounds of Little et al. and of Held and Karp (1970). This mission formalizes those results, with Christofides' theorem as its goal.

Setting

Nodes are $N = \{1, \dots, n\}$ with distances $c_{ij}$ that are symmetric, nonnegative, zero on the diagonal and satisfy the triangle inequality $c_{ij} \le c_{ik} + c_{kj}$ (IsMetric). A tour is a visiting order $\tau$ of all the nodes, of length $z(\tau) = \sum_k c(\tau_k, \tau_{k+1})$ with indices mod $n$ (tourLength); $z^*$ is the least tour length (optTourLength). A tour has an edge set (tourEdges), and for a node set $S$ the counts of tour edges inside $S$ and leaving $S$ (edgesWithin, edgesLeaving) are the sums $\sum_{i,j \in S} x_{ij}$ and $\sum_{i \in S, j \notin S} x_{ij}$ of the integer programming formulation. A comb is a handle $H$ with an odd number $s \ge 3$ of pairwise disjoint teeth, each meeting both $H$ and its complement (IsComb); when every tooth has exactly two nodes the comb is a 2-matching configuration.

The nearest neighbor heuristic always moves to a nearest unvisited node (IsNearestNeighborTour); the nearest insertion heuristic grows a partial tour by inserting the unvisited node nearest to it at the cheapest position (IsNearestInsertionRun, with cycleLength and distToTour). The minimum spanning tree heuristic doubles an MST (IsMST, graphWeight), takes an Eulerian tour of the doubled tree and shortcuts it, visiting the nodes in order of first appearance (IsShortcut). Christofides' heuristic instead adds to the MST a minimum-weight perfect matching on its odd-degree nodes (oddNodes, IsMinMatchingOn) before taking the Eulerian tour. A 1-tree rooted at $r$ is a spanning tree on the other nodes plus two edges at $r$ (Is1Tree); the revised distances $c'_{ij} = c_{ij} + \lambda_i + \lambda_j$ (revisedCost) define the Held-Karp bound.

Formalization targets

Goal: Theorem 10.13

For every metric instance, every minimum spanning tree $T^*$ , every minimum-weight perfect matching $M$ on the odd-degree nodes of $T^*$ , every Eulerian tour of $T^* + M$ and its shortcut $\tau$ ,

z(\tau) \;\le\; \tfrac{3}{2}\, z^*.

This is christofides_bound.

Supporting targets

Theorem 10.1, the reduced-matrix bound $\sum_i \rho_i + \sum_j \kappa_j \le z^*$ ; Theorem 10.2, Proposition 10.3 and Theorem 10.4, the 2-matching and comb inequalities valid for every tour; Theorem 10.6, $z_{NN} \le \frac{1}{2}(\lceil\log_2 n\rceil + 1) z^*$ ; Theorem 10.7, $z_{NI} \le 2z^*$ ; Lemma 10.9, $z(T^*) \le z^*$ ; Theorem 10.10, Euler's theorem; Theorem 10.11, $z_{MST} \le 2z^*$ ; Lemma 10.12, the handshaking lemma; Lemma 10.15, the 1-tree bound; Lemma 10.16, the revised distance identities; Theorem 10.17, the Held-Karp bound. Theorem 10.5 (no constant-factor approximation unless P = NP), Theorem 10.8 and the second part of Theorem 10.6 (tightness instances), Lemma 10.14 (Euclidean tours do not cross), Lemma 10.18 (the integrality gap) and Theorem 10.19 (the Beardwood-Halton-Hammersley asymptotics) are not targets.

Significance

Christofides' bound was the best approximation guarantee for the metric TSP for over forty years, until the $3/2 - 10^{-36}$ of Karlin, Klein and Oveis Gharan (2021), and it is the reference point against which every heuristic in the chapter is measured: nearest neighbor has no constant bound, nearest insertion and the MST heuristic achieve $2$ , Christofides $3/2$ . The comb inequalities are the cuts that make branch-and-cut work, and the Held-Karp bound is the lower bound that tells a practitioner how far a heuristic tour is from optimal. Theorem 10.1 is the historical bounding rule of the first branch-and-bound algorithm.

None of these results has a machine-checked proof. The book proves Theorems 10.2, 10.11, 10.13 and 10.17 and Proposition 10.3 and Lemma 10.9, cites Theorems 10.6, 10.7 and 10.10, and leaves Theorem 10.4 and Lemmas 10.12 and 10.16 as exercises. The formal infrastructure for tours, shortcutting and Eulerian walks is reusable for the vehicle routing chapter.

Difficulty

Christofides' argument has three steps and each has a formal obstacle. The MST bound is a spanning-path argument that needs the removal of an edge from a tour to yield a tree, in Mathlib's terms a connected acyclic subgraph of the complete graph. The matching bound is the subtle one: the optimal tour shortcut to the odd-degree nodes, of length at most $z^*$ by the triangle inequality, is an even cycle whose alternate edges form two perfect matchings on those nodes, the cheaper of which costs at most $z^*/2$ ; formalizing the decomposition of a cycle on an even node set into two matchings, and the shortcut's length bound, is the bulk of the work. The final step, that shortcutting an Eulerian walk does not lengthen it, is an induction along the walk using the triangle inequality on the skipped stretches, and it needs the first-occurrence order to be handled explicitly.

The obvious approach to the heuristic bounds, comparing the heuristic tour directly with the optimal tour, fails; every proof goes through a spanning tree. For nearest insertion the tree is Prim's, grown in the same order as the insertions, and the bound charges each insertion cost to a tree edge; for nearest neighbor the argument of Rosenkrantz et al. bounds the sum of the $k$ largest steps by $2z^*$ for each $k$ and sums a geometric series, which is where the logarithm comes from.

The comb inequalities are counting arguments on degrees, but the general comb of Theorem 10.4 needs the case analysis of how a tour enters and leaves each tooth. Euler's theorem in the sufficiency direction is Hierholzer's construction, which is not in Mathlib.

Formalization scope

Tours are permutations of Fin n, so a tour is an ordering rather than an edge set, and every tie-breaking of a heuristic is covered by a predicate on its output rather than by an algorithm. Graphs are Mathlib SimpleGraphs on Fin n; the multigraphs of the two tree heuristics are represented by closed walks with prescribed edge multisets, and shortcutting is the first-occurrence order along the walk's node sequence. All degree and edge-set computations use classical decidability. Theorems on tours assume $n \ge 3$ where a tour must have distinct edges, $n \ge 1$ otherwise.

Theorem 10.1 is stated for the reduction of the full off-diagonal matrix, because the book's upper-triangular version is false: a random metric instance violates it, since the last row and first column of a triangular matrix are empty and the two edges at a node need not be one row and one column entry. The full-matrix version is the statement of Little et al. It is stated for $n \ge 2$ , because a one-node "tour" is a self-loop that no off-diagonal entry constrains.

Theorem 10.4 is stated with the comb inequality's right-hand side corrected to $|H| + \sum_k(|T_k| - 1) - \tfrac{1}{2}(s+1)$ , the standard form. The book prints $+\tfrac{1}{2}(s-1)$ , which contradicts its own 2-matching special case (10.15) and is weaker by $s$ . The corrected statement implies the printed one.

The $1$ -tree root is an explicit node $r$ , the book's node $1$ . The nearest insertion run is a sequence of lists indexed by iteration, and the theorem compares the $n$ -th list's closed length with $z^*$ ; a run always exists, so the hypothesis is satisfiable.

The definition module is shared by all fifteen items. Theorem 10.8 and Problem 10.12 (tightness of the bounds of $2$ ), the second part of Theorem 10.6, and Lemma 10.18 on the integrality gap are natural extensions on the same definitions.

Selected references

L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 10. https://doi.org/10.1002/9781119584445
N. Christofides, Worst-case analysis of a new heuristic for the travelling salesman problem, Report 388, GSIA, Carnegie Mellon University, 1976; reprinted in Operations Research Forum 3, 2022. https://doi.org/10.1007/s43069-021-00101-z
D. J. Rosenkrantz, R. E. Stearns and P. M. Lewis II, An analysis of several heuristics for the traveling salesman problem, SIAM Journal on Computing 6(3), 1977. https://doi.org/10.1137/0206041
M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees, Operations Research 18(6), 1970. https://doi.org/10.1287/opre.18.6.1138
J. D. C. Little, K. G. Murty, D. W. Sweeney and C. Karel, An algorithm for the traveling salesman problem, Operations Research 11(6), 1963. https://doi.org/10.1287/opre.11.6.972
M. Grötschel and M. W. Padberg, On the symmetric travelling salesman problem I and II, Mathematical Programming 16, 1979. https://doi.org/10.1007/BF01582116

15 thms2 active usersReviewed

Completed

Optimization·Captain: naimengye

The Theory and Practice of Revenue Management III: Dynamic PricingTextbook

Prices that respond to inventory

A retailer marking down a seasonal line, an airline raising fares as seats sell, a manufacturer pricing while restocking: each sets prices over time against a finite and changing inventory. Chapter 5 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) collects the structural theory of that problem. Without replenishment, the Bernoulli-arrival model of Gallego and van Ryzin (1994) gives a marginal value of capacity that falls with inventory and with time, hence prices that jump up at each sale and drift down between sales, and the deterministic fluid model bounds it from above. With replenishment, the model of Federgruen and Heching (1999) has a jointly concave and supermodular continuation value, from which the base-stock, posted-price policy follows: below a base-stock level order up to it and post a fixed price, above it order nothing and discount, more the higher the inventory. This mission formalizes those results with Proposition 5.3 as the goal.

Setting

Bernoulli demand (Sect. 5.2.2.2). One customer arrives per period with a random willingness to pay; the firm's decision is the demand rate $d \in [0, 1]$ , the probability of a sale at the inverse-demand price $p(t, d)$ , with revenue rate $r(t, d) = d\,p(t, d)$ (revenueRate). The value function (5.12) is $V_t(x) = \max_{d}\{r(t, d) - d\,\Delta V_{t+1}(x)\} + V_{t+1}(x)$ , $V_{T+1} = 0$ , $V_t(0) = 0$ (bernoulliValue), and $\Delta V_t(x) = V_t(x) - V_t(x-1)$ (bernoulliDelta). The deterministic model (5.1) maximizes $\sum_t r(t, d(t))$ over rates with $\sum_t d(t) \le C$ (deterministicValue).

Pricing with replenishment (Sect. 5.3.2). Inventory may be negative (backorders). In period $t$ with inventory $x$ the firm orders up to $y \ge x$ at unit cost $c_t$ , chooses a rate $d \in [0, \bar d]$ , sells the random demand $D(t, d, \xi_t) = a_t(\xi_t)\,d + b_t(\xi_t)$ (additive, multiplicative or mixed noise), and pays the convex cost $h_t$ on ending inventory. The value function (5.20) is $V_t(x) = \sup_{y \ge x,\, d}\{r(t, d) - c_t(y - x) + G_{t+1}(y, d)\}$ with the continuation value $G_{t+1}(y, d) = \mathbb E[V_{t+1}(y - D(t, d, \xi_t)) - h_t(y - D(t, d, \xi_t))]$ (ReplPricing.value, contValue). Assumption 7.2, marginal revenue decreasing, is the concavity of $r(t, \cdot)$ .

Formalization targets

Goal: Proposition 5.3

For every period, $G_{t+1}$ is jointly concave on $\mathbb R \times [0, \bar d]$ , $V_t$ is concave on $\mathbb R$ , and $G_{t+1}$ has increasing differences in $(y, d)$ , the supermodularity that the book states through its partial derivatives: replenishment_concave_supermodular.

Supporting targets

Proposition 5.2, the marginal value of capacity in the Bernoulli model decreases in $t$ and in $x$ ; the upper bound of Sect. 5.2.2.3, the optimal deterministic revenue dominates the optimal expected stochastic revenue; and the base-stock, posted-price structure of Sect. 5.3.2.1, derived from Proposition 5.3: below the unconstrained optimum $y^0$ order up to it and use $d^0$ , above it order nothing and use a rate at least $d^0$ that is nondecreasing in the inventory.

Proposition 5.1 and Lemma 5-5.A.1 (the continuous-demand model without replenishment) are not targets; see the formalization scope. The deterministic sections (efficient prices, discrete price sets), the asymptotic optimality of the deterministic heuristic, the infinite-horizon stationary problem and the multiproduct and finite-population models carry no numbered results.

Significance

Proposition 5.3 is the structural core of joint pricing and inventory control: joint concavity makes the period problem a concave program, and supermodularity is what turns its solution into a policy, the base-stock, posted-price rule that Federgruen and Heching showed optimal and that later work on pricing with inventory builds on. Proposition 5.2 is the reason optimal dynamic prices in the stochastic single-item model rise at every sale and fall while inventory sits, the behaviour of Figure 5.5, and the deterministic upper bound is what justifies the fluid model as a benchmark and a heuristic, the pattern quantified in Table 5.6. None of these has a machine-checked proof; the replenishment result in particular needs the interplay of concavity, expectation and partial maximization on all of $\mathbb R$ .

Difficulty

Proposition 5.2 is an induction whose step compares suprema over the rate interval, with the boundary condition $V_t(0) = 0$ breaking the recursion at $x = 1$ and requiring $r(t, 0) = 0$ . The deterministic bound is an induction on periods that uses the concavity of the deterministic value in the inventory (a concave program's value) to absorb the two branches of the Bernoulli recursion. The goal needs: integrability and continuity of $V_{t+1}(y - D) - h_t(y - D)$ under bounded noise; that the expectation of a concave function of an affine map is jointly concave, and its increasing differences from those of the concave integrand; that a partial supremum of a jointly concave function over the convex feasible set $\{y \ge x\}$ is concave in $x$ ; and the boundedness of the objective so that every supremum is a real number. The base-stock item is the segment argument that moves an unconstrained maximizer onto the boundary $y = x$ and a monotone comparative-statics argument on the supermodular objective, with maxima attained by continuity on the compact rate interval.

Formalization scope

Periods are natural numbers with value t the value with $T + 1 - t$ periods to go, the maxima are suprema, and the book's ranges are hypotheses. The demand is affine in the rate, which is the additive and multiplicative models the book names; with a merely convex demand (Assumption 5.1) the joint concavity of Proposition 5.3 fails when $V_{t+1} - h_t$ is not monotone, and the noise has bounded support, strengthening Assumption 7.6. The partial-derivative statements (iii)-(iv) are in difference form. Proposition 5.1 is not formalized: its model (5.11) evaluates $V_{t+1}(x - D)$ at negative inventories the model does not define while truncating revenue at $x$ , and its Lemma 5-5.A.1 (joint concavity of $r^+$ ) is false as stated, its Hessian argument mistaking an indefinite matrix for a negative definite one; a counterexample is in the mission's check. The deterministic model restricts rates to $[0, 1]$ , the rates the Bernoulli model can realize.

Selected references

K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 5. https://doi.org/10.1007/b139000
G. Gallego and G. J. van Ryzin, Optimal dynamic pricing of inventories with stochastic demand over finite horizons, Management Science 40(8), 1994. https://doi.org/10.1287/mnsc.40.8.999
A. Federgruen and A. Heching, Combined pricing and inventory control under uncertainty, Operations Research 47(3), 1999. https://doi.org/10.1287/opre.47.3.454
W. Elmaghraby and P. Keskinocak, Dynamic pricing in the presence of inventory considerations, Management Science 49(10), 2003. https://doi.org/10.1287/mnsc.49.10.1287.17315
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

5 thms2 active usersReviewed

Completed

Markov Chain·Captain: naimengye

Fundamentals of Supply Chain Theory X: Supply UncertaintyTextbook

When the supplier is the risk

Every model in the earlier chapters of this series treats demand as the uncertain quantity and supply as given. Chapter 9 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) reverses the roles: demand is deterministic and the supplier fails. A disruption is a binary event, modeled as a two-state Markov process between up and down periods, during which nothing can be ordered. The chapter's thesis, from Snyder and Shen (2006), is that supply uncertainty is a mirror image of demand uncertainty: the optimal base-stock level has the same critical-fractile form as the newsvendor solution but with the fractile taken over the disruption-length distribution (Tomlin 2006), and consolidation, which pools demand risk, now does nothing to expected cost and multiplies its variance, the risk-diversification effect of Schmitt, Sun, Snyder and Shen (2015). The chapter closes with the reliable fixed-charge location problem of Snyder and Daskin (2005). This mission formalizes the chapter's theorems on disruptions, with the risk-diversification theorem as its goal.

Setting

A supplier that is up is disrupted next period with probability $\alpha$ ; one that is down recovers with probability $\beta$ . The disruption chain records $0$ when the supplier is up and $n \ge 1$ in the $n$ -th consecutive period of a disruption; its stationary distribution is $\pi_0 = \beta/(\alpha+\beta)$ and $\pi_n = \frac{\alpha\beta}{\alpha+\beta}(1-\beta)^{n-1}$ (disruptionPmf), with distribution function $F(n) = \sum_{i \le n}\pi_i$ (disruptionCdf).

A single location faces demand $d$ per period, pays $h$ per unit held and $p$ per unit backordered per period, and follows a base-stock policy: it orders up to $S$ in every up period and nothing in down periods. In the $n$ -th period of a disruption it has $S - (n+1)d$ units on hand or backordered, so its cost is $\hat g(S, n) = h[S-(n+1)d]^+ + p[(n+1)d - S]^+$ (periodCost), and the expected cost per period is $g(S) = \sum_n \pi_n \hat g(S, n)$ (meanCost), with variance $V(S)$ over the disruption state (varCost). The critical fractile $\gamma = p/(p+h)$ and $F^{-1}(\gamma)$ , the smallest $n$ with $F(n) \ge \gamma$ , determine the optimal level.

In the reliable fixed-charge location problem (RFLP), sites fail independently with probability $q$ and each customer is assigned to a chain of facilities: its level- $r$ facility serves it when the $r$ closer facilities are disrupted, until it is assigned to an emergency facility $u$ that never fails and charges the penalty $\theta_i$ . The objective (9.61) is fixed cost plus expected transportation cost, with coefficients $\psi_{ijr} = h_i c_{ij} q^r (1-q)$ (rflpPsi, rflpCost) under the constraints (9.62)-(9.67) (RFLPFeasible).

Formalization targets

Goal: Theorem 9.9

For $N$ identical locations and the centralized location formed by merging them (demand $Nd$ ):

S^*_C = NS^*, \qquad g^*_C = g^*_D = Ng^*, \qquad V^*_C = N V^*_D = N^2 V^*,

that is, an optimal single-location level $S$ scales to the optimal centralized level $NS$ , the centralized expected cost at $NS$ is $N$ times the single-location cost, and its variance is $N^2$ times the single-location variance. This is risk_diversification.

Supporting targets

Lemma 9.2, the stationary distribution and distribution function of the disruption chain; Lemma 9.4, that the optimal base-stock level is a multiple of $d$ ; Theorem 9.5, $S^* = d + dF^{-1}(p/(p+h))$ , as the least minimizer of $g$ ; and Theorem 9.10, that in every optimal RFLP solution consecutive backup assignments are ordered by cost. Theorem 9.3, the optimality of base-stock policies, is cited by the book to Song and Zipkin without a model of the policy space and is not a target; Proposition 9.1 and the multisupplier results of Sect. 9.4 are left for a later mission, as discussed below.

Significance

Theorem 9.5 is the supply-side newsvendor formula: it says exactly how much inventory buys protection against disruptions of a given length, and it underlies the disruption models used in practice for raw-material buffers. Theorem 9.9 is the chapter's central insight and the reason supply and demand uncertainty call for opposite strategies: pooling reduces expected cost under demand uncertainty but only redistributes risk under supply uncertainty, concentrating it. Its three identities are what a risk-averse planner needs to compare the two designs by a mean-variance criterion. Theorem 9.10 is what lets the RFLP be formulated without ordering constraints and solved by Lagrangian relaxation like the UFLP.

None of these results has a machine-checked proof. The book proves Theorem 9.5 and the identities behind Theorem 9.9, sketches Lemma 9.4, and leaves Lemma 9.2 and Theorem 9.10 as exercises. The formal treatment of the piecewise-linear cost $g$ and its finite differences is reusable for the yield-uncertainty and multi-supplier models of the same chapter.

Difficulty

The cost $g$ is an infinite series whose terms grow linearly in $n$ against a geometric weight, so every statement about it begins with summability, and the finite-difference identity $\Delta g(S) = d[(h+p)F(S/d - 1) - p]$ requires exchanging a difference with a sum. Theorem 9.5 then needs the convexity and piecewise linearity of $g$ to pass from a sign condition on slopes at multiples of $d$ to a global minimum over all real $S$ , and the identification of the least minimizer needs the slopes to be strictly negative below $S^*$ . The obvious idea, treating the problem as a discrete newsvendor over multiples of $d$ , is only half of the argument: it does not by itself exclude non-multiple minimizers, which is what Lemma 9.4 asserts.

Lemma 9.2 is elementary but the stationary equations involve a series over all down states, and the proof must establish summability before manipulating it. Theorem 9.9's scaling identities are termwise, but the optimality transfer in part 1 requires the scaling to preserve minimizers, which follows from the cost identity holding for every $S$ .

Theorem 9.10 is an exchange argument on a binary program with layered constraints. The delicate case is the emergency facility: swapping it into a lower level is infeasible, and the correct move is to promote it and drop the later assignment, which changes the constraints for every higher level; the argument must show feasibility of the modified solution level by level.

Formalization scope

The disruption distribution is given by Lemma 9.2's formula rather than defined as the stationary distribution, and Lemma 9.2 shows it satisfies the stationary equations; the theorems assume $0 < \alpha \le 1$ and $0 < \beta \le 1$ , under which every series is a geometric series times a polynomial and is summable. The quantity $F^{-1}(\gamma)$ enters Theorem 9.5 as a natural number $k$ characterized by $F(k) \ge \gamma$ and $F(n) < \gamma$ for $n < k$ , which exists since $F(n) \to 1 > \gamma$ ; the conclusion asserts both optimality and leastness of $d + dk$ among all real levels.

Theorem 9.9 is stated as the scaling of the single-location functions; the decentralized totals $Ng^*$ and $NV^*$ are the mean and variance of a sum of $N$ independent copies, which the book asserts rather than derives, and are not modeled separately. In the RFLP, levels are indexed by Fin m, the emergency facility is a designated index $u$ whose data satisfy the book's conventions through the hypotheses, and demands are positive with $0 < q < 1$ , both needed: with $q = 0$ or $h_i = 0$ backup assignments are free and any order is optimal.

The EOQ with disruptions (Proposition 9.1) is a renewal-reward derivation without a formal model of the renewal process in the book, and the multisupplier newsvendor of Sect. 9.4 (Lemma 9.6, Theorems 9.7 and 9.8) rests on differentiability conditions the book defers to Dada et al. and on a lemma it leaves as an exercise; both are natural extensions on the same definitions rather than targets here.

Selected references

L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 9. https://doi.org/10.1002/9781119584445
B. Tomlin, On the value of mitigation and contingency strategies for managing supply chain disruption risks, Management Science 52(5), 2006. https://doi.org/10.1287/mnsc.1060.0515
A. J. Schmitt, S. A. Sun, L. V. Snyder and Z.-J. M. Shen, Centralization versus decentralization: risk pooling, risk diversification, and supply chain disruptions, Omega 52, 2015. https://doi.org/10.1016/j.omega.2014.10.010
L. V. Snyder and M. S. Daskin, Reliability models for facility location: the expected failure cost case, Transportation Science 39(3), 2005. https://doi.org/10.1287/trsc.1040.0107
L. V. Snyder and Z.-J. M. Shen, Supply and demand uncertainty in multi-echelon supply chains, working paper, 2006. https://doi.org/10.1287/msom.1080.0224

6 thms2 active usersReviewed

Completed

Optimization·Captain: naimengye

Fundamentals of Supply Chain Theory IX: Facility Location ModelsTextbook

Where to put the warehouses

Choosing where to open distribution centers is the strategic decision that fixes a supply chain's shape for years. The basic model, the uncapacitated fixed-charge location problem (UFLP) of Balinski (1965), trades the fixed cost of opening sites against the cost of transporting demand from open sites to customers. It is NP-hard, yet routinely solved to optimality, and the reason is a fact about its relaxations: the LP relaxation is unusually tight, and Lagrangian relaxation, which Cornuejols, Fisher and Nemhauser (1977) brought to location problems, gives the same bound with a subproblem solvable by inspection. Chapter 8 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) develops the UFLP, its Lagrangian relaxation and Erlenkotter's (1978) DUALOC dual-ascent method, then the p-median problem with Hakimi's (1965) node-optimality theorem and the covering models. This mission formalizes the chapter's numbered results, with the equality of the Lagrangian and LP bounds as its goal.

Setting

Customers $i \in I$ have demands $h_i$ ; candidate sites $j \in J$ have fixed costs $f_j$ ; shipping one unit from $j$ to $i$ costs $c_{ij}$ . A solution opens sites ( $x_j \in \{0,1\}$ ) and assigns demand fractions ( $y_{ij} \ge 0$ , $\sum_j y_{ij} = 1$ , $y_{ij} \le x_j$ ); its cost is $\sum_j f_j x_j + \sum_i \sum_j h_i c_{ij} y_{ij}$ (uflpCost, UFLPFeasible). The optimal value is $z^*$ (uflpOpt); relaxing $x_j \in \{0,1\}$ to $0 \le x_j \le 1$ gives the LP relaxation with value $z_{LP}$ (uflpLP).

Lagrangian relaxation removes the assignment constraints and charges $\lambda_i$ per unit of violation. For fixed multipliers $\lambda$ the subproblem (UFLP-LR $_\lambda$ ) minimizes $\sum_j f_j x_j + \sum_i\sum_j (h_i c_{ij} - \lambda_i) y_{ij} + \sum_i \lambda_i$ over $y_{ij} \le x_j$ , $x$ binary, $y \ge 0$ (lagrObjective, LagrFeasible), with value $z_{LR}(\lambda)$ (zLR). It separates by site: the benefit of opening $j$ is $\beta_j = \sum_i \min\{0, h_i c_{ij} - \lambda_i\}$ (benefit), and $j$ is opened iff $\beta_j + f_j < 0$ . The best bound is the Lagrangian dual value $z_{LR} = \max_\lambda z_{LR}(\lambda)$ (zLRbest).

DUALOC works with the condensed dual of the LP relaxation, whose variables $v_i$ satisfy $\sum_i \max\{0, v_i - \hat c_{ij}\} \le f_j$ with $\hat c_{ij} = h_i c_{ij}$ . A dual solution $v$ and a site set $J^+$ form a primal-dual pair (PDP) when these constraints are tight on $J^+$ and every customer has a site in $J^+$ with $\hat c_{ij} \le v_i$ ; the primal solution opens $J^+$ and assigns each customer to its nearest open site $j^+(i)$ (NearestIn, primalX, primalY).

For the p-median problem on a network, the customers are the nodes, $d$ is the shortest-path distance between nodes, and a facility may sit at position $t$ along an edge $(u, w)$ of length $\ell$ , at distance $\min\{d(i,u) + t\ell, d(i,w) + (1-t)\ell\}$ from node $i$ (NetPoint, netDist). The p-center problem minimizes the largest distance from a customer to its nearest of $p$ open sites; pCenterValue c p is its optimal value.

Formalization targets

Goal: Corollary 8.2

For every instance with at least one candidate site,

z_{LP} \;=\; z_{LR} \;=\; \sup_\lambda z_{LR}(\lambda).

This is lagrangian_equals_lp.

Supporting targets

Theorem 8.1, the closed form $z_{LR}(\lambda) = \sum_j \min\{0, \beta_j + f_j\} + \sum_i \lambda_i$ with its optimal solution; the bounds (8.16) $z_{LR}(\lambda) \le z^*$ and (8.19) $z_{LP} \le z_{LR} \le z^*$ ; Theorem 8.3, the variable-fixing tests; Lemma 8.4, the DUALOC duality gap $z^+_P - z^+_D = \sum_i \sum_{j \in J^+, j \ne j^+(i)} \max\{0, v_i - \hat c_{ij}\}$ ; Lemma 8.6, the characterization of complementary slackness violations; Theorem 8.7, Hakimi's theorem that some $p$ nodes are optimal among all $p$ -point sets; Lemma 8.8, the equivalence between the $p$ -center value being at most $r$ and a set cover of radius $r$ with at most $p$ sites. Proposition 8.5, which concerns the output of a specific procedure, is not a target.

Significance

Corollary 8.2 explains the behavior of every Lagrangian location code: the bound cannot beat the LP bound, so its value lies in the ease of the subproblem and in extensions to nonlinear location models (the location model with risk pooling of Chapter 12) where no LP is available. Theorem 8.1 is the subproblem solution those codes use; Theorem 8.3 is the variable-fixing device of Daskin, Snyder and others that shrinks branch-and-bound trees. Lemmas 8.4 and 8.6 are the analytical core of DUALOC, the method that made large UFLP instances solvable in the 1970s. Hakimi's theorem is the reason the $p$ -median problem is a discrete problem at all, and Lemma 8.8 is the reason $p$ -center problems are solved by bisection over covering problems rather than by their weak MIP formulation.

None of these results has a machine-checked proof. The book proves Theorems 8.1 and 8.3 and Lemma 8.6, cites Corollary 8.2 to Appendix D and Theorem 8.7 to Hakimi, and leaves Lemmas 8.4 and 8.8 as exercises. The formal treatment of the integrality property and of Lagrangian duality for a linear objective over a product of boxes is reusable for the p-median and capacitated variants the chapter goes on to discuss.

Difficulty

The goal is an LP duality statement in disguise, and the obvious idea, that $z_{LR}(\lambda)$ is the dual function of the LP relaxation, is exactly what needs proof. Two facts must be established: that for fixed $\lambda$ the subproblem over binary $x$ has the same value as over $x \in [0,1]$ , because after the optimal $y$ is substituted the objective is linear in $x$ ; and that the supremum over $\lambda$ of the resulting concave piecewise-linear function equals the LP minimum. The second is strong duality for a linear program, which Mathlib does not provide ready-made; it has to be obtained either through a Farkas-type argument or by exhibiting, for the LP optimum, a multiplier vector that attains it, which for this problem can be read off the LP dual. The book proves none of this; it invokes Lemma D.3.

The bounds (8.16) and (8.19) are easier but not free: the infima and suprema defining $z^*$ , $z_{LP}$ and $z_{LR}$ must be shown attained, which needs finiteness of the binary choices and compactness of the assignment polytope. Theorem 8.3 depends on the value of the subproblem with one variable forced, which is Theorem 8.1 applied to a modified instance. Hakimi's theorem needs a concavity argument in each point's position and a bookkeeping step, since moving several points to nodes may merge them and the result must still have exactly $p$ nodes. Lemma 8.8 is combinatorial and short once the $p$ -center value is identified with a minimum over $p$ -subsets.

Formalization scope

Customers and sites are Fin n and Fin m; demands, costs and fixed costs are arbitrary reals, as the book's formulations are, and the theorems that need it assume $m \ge 1$ . Optimal values are infima or suprema of the sets of attainable objective values, all of which are nonempty and bounded under the stated hypotheses. The Lagrangian dual value is a supremum over all real multiplier vectors, so Corollary 8.2 asserts in particular that the supremum equals the attained LP value.

The DUALOC statements take the nearest-facility assignment $j^+(i)$ as a function a with the defining property, so ties are resolved by the hypothesis, and the complementary slackness violation is written exactly as (8.51) with $(x^+, y^+)$ substituted. Hakimi's theorem is stated for a family of $p$ points with repetition allowed, which is stronger than for a set. It assumes what the book's network supplies: the node distances satisfy the triangle inequality, since they are shortest-path distances, and every edge carrying a point is at least as long as the distance between its endpoints. The argument needs both: they make the ends of an edge coincide with its nodes, and without them a point on a short fictitious edge can beat every node. The set covering value in Lemma 8.8 is expressed through the existence of a cover with at most $p$ sites rather than as a natural-number infimum, whose value $0$ on infeasible instances would falsify the equivalence.

The definition module is shared by all ten items. The Lagrangian relaxation of the $p$ -median problem (Sect. 8.3.2.2), the continuous knapsack subproblem of the capacitated problem, and Proposition 8.5 on the dual-ascent procedure are natural extensions on the same definitions.

Selected references

L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 8. https://doi.org/10.1002/9781119584445
M. L. Balinski, Integer programming: methods, uses, computation, Management Science 12(3), 1965. https://doi.org/10.1287/mnsc.12.3.253
G. Cornuejols, M. L. Fisher and G. L. Nemhauser, Location of bank accounts to optimize float, Management Science 23(8), 1977. https://doi.org/10.1287/mnsc.23.8.789
D. Erlenkotter, A dual-based procedure for uncapacitated facility location, Operations Research 26(6), 1978. https://doi.org/10.1287/opre.26.6.992
S. L. Hakimi, Optimum distribution of switching centers in a communication network and some related graph theoretic problems, Operations Research 13(3), 1965. https://doi.org/10.1287/opre.13.3.462
A. M. Geoffrion, Lagrangean relaxation for integer programming, Mathematical Programming Study 2, 1974. https://doi.org/10.1007/BFb0120690

10 thms2 active usersReviewed

Operations Research

Missions

Path-Finding Methods for Linear Programming I: Centering with Weights on the Weighted Central PathResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5 (Centering with Weights), §IV.C

Milestone: Lemma 3 (Split Newton Step), §IV.B

Milestone: Lemma 1, §IV.B

Significance

Difficulty

Formalization scope

Selected references

Critical-Path Planning and Scheduling II: The Project Cost Curve Is Non-Increasing, Piecewise Linear and ConvexResearch Paper

Motivation

Setting

Formalization targets

Goal: the shape of the project cost curve (p. 165)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Incentives in Teams: The Own Profit Incentive Structure Is an Optimal Incentive Structure for a ConglomerateResearch Paper

Motivation

The conglomerate model

Formalization targets

Goal: Theorem 1 (p. 625)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Finding Minimum-Cost Circulations by Canceling Negative Cycles: Polynomial Termination of Minimum-Mean Cycle CancelingResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.9, with the proof's constant

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the optimality equation for average cost Markov decision processes and its validity for inventory control: The Average-Cost Optimality Equation for Setup-Cost Inventory ControlResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.5

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimum Branchings: The Vertices of the Branching Polyhedron Are Exactly the BranchingsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 235)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Linear Optimization under Bandit Feedback 2: A Regret Lower Bound on the CircleResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 for n=2n=2n=2

Milestones

Significance

Difficulty

Formalization scope

Selected references

On Certain Polytopes Associated with Graphs V: Zero-One Optima of the Odd-Cycle Relaxation on Series-Parallel GraphsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 7.1

Milestones

Significance

Goal: Theorem 3 for $n=2$