The OR Formalization Drive

Dynamical Systems Operations Research Probability+1·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 7: Weak Limit Points of the Occupation Measures of a Weak Asymptotic Pseudotrajectory Are InvariantResearch Paper

Motivation

Stochastic approximation algorithms are recursions $x_{n+1}-x_n=\gamma_{n+1}(F(x_n)+U_{n+1})$ driven by small steps $\gamma_n$ and noise $U_{n+1}$ ; they include the Robbins–Monro scheme, stochastic gradient methods and learning dynamics in games. The ODE method studies their long-run behaviour by comparing a time-interpolation of the iterates with the trajectories of a deterministic dynamical system. In Benaïm's lecture notes (Benaïm 1999) this comparison is formalized by the notion of an asymptotic pseudotrajectory, introduced in Benaïm and Hirsch (1996): a path that, over every window of fixed length, shadows the deterministic orbit started at its current position with an error that vanishes as time goes to infinity.

The pathwise results of the earlier sections of the notes concern algorithms whose step sizes decrease fast enough, typically $\gamma_n=o(1/\log n)$ or $\gamma_n=O(n^{-\alpha})$ . When the step sizes go to zero more slowly, the limit sets of the process can no longer be characterized precisely: with steps of order $1/\log n$ the process may fail to converge even when the chain recurrent set of the ODE consists of isolated equilibria. Section 10, which is mainly based on work of Benaïm and Schreiber, describes instead the statistical behaviour of such processes in terms of the deterministic dynamics. It introduces a weaker, conditional notion, the weak asymptotic pseudotrajectory, and proves in Theorem 10.1 that the empirical distribution of the time spent by the process in different regions of the state space accumulates only on invariant measures of the deterministic dynamics. This is an ergodic-theoretic counterpart of the limit-set theorems of Section 5.

Setting

A semiflow on a metric space $(M,d)$ is a continuous map $\Phi:\mathbb R_+\times M\to M$ , $(t,x)\mapsto\Phi_t(x)$ , with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$ for $t,s\ge0$ . Throughout, $M$ is a separable metric space with its Borel $\sigma$ -algebra.

Let $(\Omega,\mathcal F,P)$ be a probability space and $\{\mathcal F_t\}_{t\ge0}$ a nondecreasing family of sub- $\sigma$ -algebras. A process $X:\mathbb R_+\times\Omega\to M$ is a weak asymptotic pseudotrajectory of $\Phi$ if

it is progressively measurable: for every $T>0$ the restriction of $X$ to $[0,T]\times\Omega$ is measurable for the product of the Borel $\sigma$ -field of $[0,T]$ and $\mathcal F_T$ ;
for each $\alpha>0$ and $T>0$ , almost surely

\lim_{t\to\infty}P\Big\{\sup_{0\le h\le T}d\big(X(t+h),\Phi_h(X(t))\big)\ge\alpha\ \Big|\ \mathcal F_t\Big\}=0 .

Let $\mathcal P(M)$ be the space of Borel probability measures on $M$ with the topology of weak convergence. A measure $\mu\in\mathcal P(M)$ is $\Phi$ -invariant if $(\Phi_t)_*\mu=\mu$ for every $t\ge0$ ; the set of invariant measures is $\mathcal M(\Phi)$ . The occupation measure of the process at time $t>0$ is the random probability measure

\mu_t(\omega)=\frac1t\int_0^t\delta_{X(s,\omega)}\,ds ,

and $\mathcal M(X,\omega)\subset\mathcal P(M)$ is the set of its weak limit points as $t\to\infty$ .

Formalization targets

Goal: Theorem 10.1

If $X$ is a weak asymptotic pseudotrajectory of $\Phi$ , there is a set $\tilde\Omega\subset\Omega$ with $P(\tilde\Omega)=1$ such that for all $\omega\in\tilde\Omega$

\mathcal M(X,\omega)\subset\mathcal M(\Phi).

No tightness is assumed, so $\mathcal M(X,\omega)$ may be empty; the statement asserts the inclusion, not nonemptiness.

Milestones

Fix a uniformly continuous $f:M\to[0,1]$ and $T>0$ , and set $U_n(f,T)=\int_{(n-1)T}^{nT}f(X(s))\,ds$ for $n\ge1$ . The milestones are the numbered displays of the proof on pp. 62–63:

Eq. (47): $\frac1n\sum_{i=1}^n[U_i(f,T)-E(U_i(f,T)\mid\mathcal F_{(i-1)T})]\to0$ almost surely (stated for every continuous $f$ with values in $[0,1]$ , since the proof also applies it to $f\circ\Phi_T$ );
Eq. (50): the same with $U_{i+1}(f,T)$ conditioned on $\mathcal F_{(i-1)T}$ ;
Eq. (51): $E(U_{i+1}(f,T)-U_i(f\circ\Phi_T,T)\mid\mathcal F_{(i-1)T})\to0$ almost surely;
Eq. (52): $\frac1n\sum_{i=1}^nU_{i+1}(f,T)-\frac1n\sum_{i=1}^nU_i(f\circ\Phi_T,T)\to0$ almost surely;
Eq. (53): for a single measurable path whose occupation measures converge weakly to $\mu$ along $t_j\to\infty$ , the averages $\frac1{n_jT}\sum_{i=0}^{n_j-1}\int_{iT}^{(i+1)T}f(x_s)\,ds$ with $n_j=\lfloor t_j/T\rfloor$ converge to $\int f\,d\mu$ for every bounded continuous $f$ .

Significance

The result. Theorem 10.1 locates the long-run statistics of a stochastic process that only shadows a deterministic semiflow in conditional probability. When the occupation measures are tight, for example when the path has compact closure, $\mathcal M(X,\omega)$ is nonempty, and the theorem restricts where the process spends its time to the supports of invariant measures. Right after the theorem the notes define the minimal center of attraction of the process from the supports of the measures in $\mathcal M(X,\omega)$ ; the conclusion applies to processes, such as slowly decreasing step-size algorithms, for which the pathwise limit-set theorem of Section 5 is not available.

Formalizing it. The theorem has a complete published proof. No machine-checked version of it, of weak asymptotic pseudotrajectories, or of occupation-measure limit theorems for continuous-time processes is known to exist. The mission produces a formal definition of progressively measurable weak asymptotic pseudotrajectories, occupation measures of measurable paths and their weak limit points, and a proof that combines a martingale law of large numbers in discrete time with weak convergence in $\mathcal P(M)$ .

Difficulty

The obvious route is to apply the pathwise argument for asymptotic pseudotrajectories along each path. It fails, because condition 2 controls only conditional probabilities: the deviation events may occur infinitely often along almost every path while their conditional probabilities tend to zero. The proof therefore has to work with averages and conditional expectations instead of with individual paths: a strong law of large numbers for bounded martingale differences transfers conditional statements to time averages, and this must be done for one test function and one horizon at a time. Passing from countably many test functions to invariance requires a countable family of uniformly continuous functions that determines weak convergence on the separable space $M$ , and the a.s. sets must be intersected over that family and over rational horizons. Measurability is a second difficulty: paths are not assumed continuous, so the integrals, suprema and conditional expectations involved must be shown to be well defined from progressive measurability alone.

Formalization scope

Time is $\mathbb R_{\ge0}$ ; the semiflow is Mathlib's Flow ℝ≥0 M; the filtration is a Filtration ℝ≥0; $\mathcal P(M)$ is ProbabilityMeasure M with its topology of weak convergence. $M$ is a separable metric space with its Borel $\sigma$ -algebra; it is not assumed compact, complete or Polish. Progressive measurability is stated literally for every $T>0$ . The conditional probability in condition 2 is the conditional expectation of the indicator of the deviation event, which is required to be measurable (the paper's $P\{\cdot\mid\mathcal F_t\}$ presupposes an event); the supremum over $h\in[0,T]$ is taken in $[0,\infty]$ . Invariance for the semiflow is $(\Phi_t)_*\mu=\mu$ for all $t\ge0$ , the form the proof establishes; for a flow it agrees with the definition $\mu(A)=\mu(\Phi_t(A))$ of Section 8.3. Weak limit points are cluster points of $t\mapsto\mu_t(\omega)$ as $t\to\infty$ ; the occupation measure is a genuine probability measure for every measurable path and $t>0$ .

The following formalizations would trivialize the statement and are excluded by the definitions: an "occupation measure" equal to the zero measure for a non-measurable path; a conditional probability of a non-measurable event, which Lean evaluates to $0$ and which would make condition 2 vacuous; invariance defined through images $\Phi_t(A)$ , which need not be Borel for a semiflow; and a compactness or Polish assumption on $M$ , which the theorem does not make.

A complete development needs: Fubini-type measurability for progressively measurable processes, square-integrable martingale convergence and Kronecker's lemma (both largely in Mathlib), conditional expectations of time integrals, a convergence-determining countable family of uniformly continuous functions on a separable metric space, and the identification of weak convergence with convergence of integrals of bounded continuous functions. The martingale law of large numbers (Eqs. (47), (50)) and Eq. (53) are reusable outside this mission. Proofs of any milestone, and alternative arguments for the goal, are welcome.

Selected references

M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. Section 10, Theorem 10.1, pp. 60–63. https://doi.org/10.1007/BFb0096509
M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617

10 thms1 active userReviewed

Completed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

On the Power of Randomization in On-Line Algorithms 2: The Bound α∘β Against Adaptive Off-Line Adversaries Is TightResearch Paper

Motivation

An on-line algorithm must answer each request as it arrives, without knowing the requests to come; paging, caching, the $k$ -server problem and metrical task systems are standard examples. Its quality is measured by competitive analysis: its cost is compared with the cost of an optimal off-line solution that knows the whole request sequence. For randomized on-line algorithms the comparison depends on how much the adversary producing the requests is allowed to see. Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994; conference version STOC 1990) introduced the three standard adversaries — oblivious, adaptive on-line and adaptive off-line — and related the competitive ratios achievable against each.

Their Theorem 2.2 (manuscript p. 10) shows that if a randomized algorithm is $\alpha$ -competitive against adaptive on-line adversaries and some randomized algorithm is $\beta$ -competitive against oblivious adversaries, then the first algorithm is $\alpha\beta$ -competitive against adaptive off-line adversaries. This mission formalizes the paper's claim (manuscript p. 11) that this product bound cannot be improved in general, together with the explicit construction on pp. 12–13 that proves it.

Setting

A request-answer game consists of a request set $R$ , a finite answer set $A$ , and cost functions $f_n : R^n \times A^n \to \mathbb R$ . For a request sequence $\underline r \in R^n$ , the off-line optimum is $c(\underline r) = \min_{\underline a \in A^n} f_n(\underline r, \underline a)$ . A deterministic on-line algorithm $G$ answers the $i$ -th request with $a_i = g_i(r_1, \dots, r_i)$ ; a randomized one is a probability distribution over deterministic algorithms $G_x$ , $x$ being the coin tosses.

An adaptive off-line adversary $Q$ chooses each request $r_{i+1} = q_i(a_1, \dots, a_i)$ from the answers given so far, stops after at most $d_Q$ requests, and pays the off-line optimum $c_Q(G) = c(\underline r)$ of the requests it made; the algorithm pays $c_G(Q) = f_n(\underline r, \underline a)$ . An adaptive on-line adversary $S$ must in addition answer each request itself, before the algorithm does, with $b_{i+1} = p_i(a_1, \dots, a_i)$ , and pays $c_S(G) = f_n(\underline r, \underline b)$ . An oblivious adversary fixes $\underline r$ in advance and pays $c(\underline r)$ . A randomized $G$ is $\alpha$ -competitive against oblivious adversaries if $\mathbb E_x[c_{G_x}(\underline r)] \le \alpha\, c(\underline r)$ for all $\underline r$ , and against adaptive on-line adversaries if $\mathbb E_x[c_{G_x}(S)] \le \mathbb E_x[\alpha\, c_S(G_x)]$ for all $S$ .

The construction uses the mates game: $R = A$ is a set of $2t$ elements split into $t$ pairs of mates, and for $n \ge 2$ the cost depends only on the first answer $a_1$ and the second request $r_2$ : it is $1$ if $a_1 = r_2$ , $M$ if $a_1$ is the mate of $r_2$ , and $m$ otherwise. The algorithm $G$ draws $a_1$ uniformly at random. The parameters solve

\beta = \frac{(2t-2)m + M + 1}{2t}, \qquad \alpha = \frac{1 + (2t-1)M}{2 + (2t-2)m}.

Formalization targets

Goal: tightness of Theorem 2.2

For $1 < \beta \le \alpha$ (or $\alpha = \beta = 1$ ) and every $C < \alpha\beta$ , there are a game and a randomized algorithm $G$ such that

G \text{ is } \alpha\text{-competitive against adaptive on-line adversaries}, \qquad G \text{ is } \beta\text{-competitive against oblivious adversaries},

and for every randomized algorithm $K$ some adaptive off-line adversary $Q$ achieves

\mathbb E[c_Q(K)] > 0, \qquad \mathbb E[c_K(Q)] \ge C\cdot \mathbb E[c_Q(K)].

Milestones (pp. 12–13)

The closed forms $m(t)$ , $M(t)$ are the unique solution of the two equations.
$m(t) \to \beta$ and $M(t) \to \alpha\beta$ as $t \to \infty$ .
For all large $t$ : $M(t) \ge \max(m(t)^2, C)$ , $1 \le m(t) \le M(t)$ , $\alpha(m(t)-1) \le M(t) - m(t)$ .
$G$ is $\beta$ -competitive against oblivious adversaries in the mates game.
$G$ is $\alpha$ -competitive against adaptive on-line adversaries in the mates game.
An adaptive off-line adversary makes every algorithm pay $M$ while paying $1$ .

Significance

The result. Together with Theorem 2.2, the claim pins down exactly how much the adaptive off-line adversary can gain over the other two: the product $\alpha\beta$ is an upper bound for every game and is approached by a single game for every admissible pair $(\alpha, \beta)$ . It shows that no general argument relating the three adversary models can give a bound better than the product, so any improvement for a specific problem (paging, $k$ -server) must use the structure of that problem. The paging example cited on p. 11 (RANDOM against the three adversaries) gives one instance of tightness; the mates game gives tightness for every admissible pair.

Formalizing it. The result is proved in the paper, in about one page, with two steps left to the reader ("by inspection of the equations", "a simple case analysis"). No machine-checked proof of this or of any statement about adaptive adversaries is known to us. The formalization makes the model of §2 precise (sequences, stopping, the order in which adversary and algorithm commit, expectations over coins), checks the asymptotics of the parameters, and verifies the case analysis, which on inspection needs an inequality the page does not state. Two printed formulas on p. 12 contain typos; the formal statements carry the correct values.

Difficulty

The construction is explicit, but each competitiveness claim quantifies over all adversaries, which may adapt their requests to the algorithm's random answers, stop at any time, and (for the on-line adversary) commit to their own answers in advance. The algebra of $\alpha$ -competitiveness is tight: the adversary's best expected advantage is exactly zero, so every case of its best reply must be checked with no slack. The page's condition $M \ge m^2$ does not suffice for this: when $a_1$ is neither the adversary's first answer nor its mate, the reply "mate of $a_1$ " beats the reply "the adversary's own answer" only when $\alpha(m-1) \le M - m$ , which holds for the solved parameters but is not implied by $M \ge m^2$ . At $\beta = 1 < \alpha$ the solved parameter $m$ is below $1$ for every $t$ , and the oblivious bound fails.

Formalization scope

All declarations live in OnlineRandomization.Tightness. The conventions:

Costs are real-valued; the paper allows $+\infty$ , so the game class is a special case.
Answer sets are nonempty finite types; request sets are arbitrary types.
Sequences are Lean lists, oldest first; cost r a is $f_n$ on lists of equal length $n$ .
Adversaries return none for "stop" and carry a depth bound $d_Q$ ; an on-line adversary's answer $b_{i+1}$ depends only on $a_1, \dots, a_i$ .
Randomized algorithms are a probability space of coins with a deterministic algorithm per coin and measurable answers; expectations are Bochner integrals, with $\alpha$ applied inside the expectation. In the goal, coin spaces range over Type.
Competitiveness uses the ratio functions $x \mapsto \alpha x$ and $x \mapsto \beta x$ , with no additive constant.
The mates game is on Fin t × Bool, with mate $(i, b) \mapsto (i, \lnot b)$ . The paper leaves the costs of plays with fewer than two requests undefined; the formalization sets $f_0 = 0$ and $f_1 \equiv 1$ (with $f_1 \equiv 0$ the algorithm would not be $\alpha$ -competitive).
Range. The goal assumes $1 < \beta \le \alpha$ or $\alpha = \beta = 1$ ; the page's case $\beta = 1 < \alpha$ is not covered by its construction and is left out. In fact the claim is false there for $1 < C < \alpha$ : an algorithm that is $1$ -competitive against oblivious adversaries answers optimally, almost surely, on every request sequence (its cost is never below the optimum and its expected cost does not exceed it), and an adaptive off-line adversary reaches only finitely many request sequences, so against $K = G$ every adversary has $\mathbb E[c_G(Q)] = \mathbb E[c_Q(G)]$ , a ratio of $1 < C$ .

The positivity requirement $\mathbb E[c_Q(K)] > 0$ in the goal is essential: without it the adversary that asks nothing satisfies $\mathbb E[c_K(Q)] \ge C \cdot 0$ for every $K$ , and the third clause would hold vacuously.

A complete development needs: finite expectations over a uniform coin, the evaluation of the play of an adversary against a constant algorithm, and limit and eventual-inequality arguments for rational functions of $t$ . The model of §2 is shared with the other missions of this series and is reusable for any request-answer formulation of an on-line problem. Proofs of individual milestones are welcome.

Selected references

S. Ben-David, A. Borodin, R. Karp, G. Tardos, A. Wigderson, On the power of randomization in on-line algorithms, Algorithmica 11 (1994) 2–14. https://doi.org/10.1007/BF01294260 (cited from the authors' manuscript, manuscript pp. 7–13).
A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998. ISBN 0-521-56392-5.
P. Raghavan, M. Snir, Memory versus randomization in on-line algorithms, IBM Journal of Research and Development 38 (1994) 683–707. https://doi.org/10.1147/rd.386.0683

9 thms3 active usersReviewed

Control Theory Operations Research Probability+1·Captain: mikedeng1

Dynamic Scheduling of a System with Two Parallel Servers in Heavy Traffic with Resource Pooling: The Threshold Policy Is Asymptotically OptimalResearch Paper

Motivation

Many service systems route several classes of work to servers with overlapping skills: call centers with cross-trained agents, manufacturing cells with flexible machines, computing clusters with heterogeneous processors. Choosing which server works on which class at each moment is a dynamic scheduling problem. Exact optimal policies are out of reach except in toy cases, so heavy-traffic theory replaces the queueing system by a Brownian control problem, solves that limit problem, and then asks for a policy in the original system whose performance converges to the Brownian optimum. This programme was proposed by Harrison (Harrison 1988), and the parallel server system studied here is the example Harrison used (Harrison, Ann. Appl. Probab. 1998) to show that the greedy static priority rule can be very inefficient.

Bell and Williams (2001) gave the first proof of asymptotic optimality of a continuous-review policy for this system, with renewal arrivals and general service times. Harrison (1998) had treated Poisson arrivals and deterministic service times with a discrete-review policy and a pathwise criterion. Harrison and López (Queueing Systems, 1999) identified the complete resource pooling condition for general parallel server systems. The threshold policy and the proof method of Bell and Williams were later extended to multiserver systems (Bell and Williams, Electron. J. Probab., 2005).

Setting

There are two job classes and two servers. Server 1 serves class 1 (activity 1); server 2 serves class 1 (activity 2) and class 2 (activity 3). A sequence of such systems is indexed by $r\to\infty$ . On a probability space, i.i.d. sequences $\check u_k(i)$ ( $k=1,2$ ) and $\check v_j(i)$ ( $j=1,2,3$ ), $i\ge1$ , are fixed: strictly positive, mutually independent, with mean one and finite variances $\alpha_k^2,\beta_j^2$ . In system $r$ the interarrival times are $u_k^r(i)=\check u_k(i)/\lambda_k^r$ and the service times are $v_j^r(i)=\check v_j(i)/\mu_j^r$ . The renewal processes $A_k^r(t)$ and $S_j^r(t)$ count arrivals and potential service completions.

A scheduling control policy is an allocation $T=(T_1,T_2,T_3)$ , where $T_j(t)$ is the time devoted to activity $j$ in $[0,t]$ . Each $T_j(t)$ is a random variable, each $T_j$ is continuous and nondecreasing from $0$ , and so are the idle times $I_1=t-T_1$ and $I_2=t-T_2-T_3$ . The queue lengths

Q_1(t)=A_1(t)-S_1(T_1(t))-S_2(T_2(t)),\qquad Q_2(t)=A_2(t)-S_3(T_3(t))

must be nonnegative. Policies may anticipate the future. The rates satisfy Assumption 3.1: $\lambda_1>\mu_1$ , $1-(\lambda_1-\mu_1)/\mu_2=\lambda_2/\mu_3$ , and the rates converge at rate $1/r$ to limits with second-order parameters $\theta_1,\theta_2$ . Assumption 3.2 is $h_1\mu_2\ge h_2\mu_3$ , and Assumption 3.3 gives finite exponential moments near $0$ . With $\hat Q^r(t)=r^{-1}Q^r(r^2t)$ the cost is

\hat J^r(T^r)=\mathbf E\Big(\int_0^\infty e^{-\gamma t}\,h\cdot\hat Q^r(t)\,dt\Big).

The threshold policy with $L^r=[c\log r]$ works as follows. Server 1 works whenever it has a class 1 job available. Server 2 serves class 1 with preemptive-resume priority when more than $L^r$ class 1 jobs are present, and otherwise serves class 2. The Brownian benchmark is built from a two-dimensional Brownian motion $\tilde X$ with drift $\theta$ and diagonal covariance, from $y=(1,\mu_2/\mu_3)$ , and from the reflected process $\tilde W^*=y\cdot\tilde X+\tilde V^*$ with $\tilde V^*(t)=-\inf_{s\le t}y\cdot\tilde X(s)$ . Its cost is $J^*=\mathbf E\int_0^\infty e^{-\gamma t}h_2\,\tilde W^*(t)/y_2\,dt$ .

Formalization targets

Goal: Theorem 5.3

For $c$ larger than a constant $c_0$ that depends only on the model data, and for every sequence $\{T^r\}$ of scheduling control policies,

\liminf_{r\to\infty}\hat J^r(T^r)\ \ge\ J^*\ =\ \lim_{r\to\infty}\hat J^r(T^{r,*}),\qquad J^*<\infty .

Milestones

Proposition B.1: the one-dimensional Skorokhod problem, its explicit solution and its minimality.
Appendix A, (181) and (184): Cramér-type deviation bounds for delayed renewal processes.
Theorem 7.2: after first reaching $L^r$ , the class 1 queue stays within $L^r-1$ of the threshold, with probability tending to one.
Theorem 7.1: $(\hat Q_1^r,\hat I_1^r)\Rightarrow(0,0)$ under the threshold policy.
Lemma 8.1: the fluid-scaled threshold allocations converge to $\bar T^*(t)=(t,\frac{\lambda_1-\mu_1}{\mu_2}t,\frac{\lambda_2}{\mu_3}t)$ .
Theorem 5.2 (state-space collapse): $(\hat Q_1^r,\hat Q_2^r,\hat I_1^r,\hat I_2^r)\Rightarrow(0,\tilde Q_2^*,0,\tilde I_2^*)$ .
Lemma 9.3: along a subsequence achieving a finite $\liminf$ cost, the fluid-scaled processes converge to $(0,\lambda t,\mu t,\bar T^*,0)$ .

A further draft theorem states that Definition 5.1 determines an admissible allocation, unique pathwise, whenever $L^r\ge1$ .

Significance

The theorem proves that a simple state-dependent rule, which sends server 2 to class 1 only when the class 1 queue exceeds a logarithmic safety stock, is asymptotically optimal among all policies, including those that anticipate the future. The limiting cost is the explicit optimum of the Brownian control problem. The proof gives a template for heavy-traffic asymptotic optimality under complete resource pooling: a lower bound valid for every policy, and state-space collapse under the proposed policy. The residual process analysis of Section 7 shows how a threshold of order $\log r$ makes starvation of server 1 negligible on the diffusion time scale.

The paper's results are proved but not machine-checked; no formal proof exists in any proof assistant. The mission asks for formal statements of the paper's main theorem and its supporting lemmas, followed by formal proofs. Parts of the development are independent of the paper: the one-dimensional Skorokhod map, renewal large deviation bounds, and convergence encodings on path space.

Difficulty

The lower bound must hold for arbitrary, possibly anticipating, policies, so no Markov structure is available. The argument has to pass through fluid limits of an arbitrary cost-minimizing subsequence and a pathwise minimality property, and Fatou's lemma for the limit needs uniform control. For the upper bound, the obvious approach, a static priority rule, is known to fail: it starves server 1 and produces a large class 1 queue. With a threshold policy, the hard step is to show that the class 1 queue, once at the threshold, rarely moves $L^r-1$ away from it over a time interval of length $r^2t$ . That requires large deviation estimates for renewal processes started at random, multiparameter stopping times. Showing that $\hat J^r(T^{r,*})$ converges to $J^*$ , rather than only that the processes converge in distribution, also requires uniform integrability of the scaled queue lengths.

Formalization scope

Classes and activities are indexed by Fin 2 and Fin 3. The i.i.d. sequences keep the paper's index base $i\ge1$ , and the systems are indexed by $n\in\mathbb N$ with $r=r_n\in[1,\infty)$ , $r_n\to\infty$ . Time is real, and every condition is imposed for $t\ge0$ . Admissibility is exactly (11)–(14). Measurability in (11) is with respect to the completion of $\mathbf P$ , since the paper's space is complete. Finiteness of the renewal processes everywhere on $\Omega$ , which the paper obtains by discarding a null set, is a hypothesis. Queue lengths are real, costs are lower Lebesgue integrals in $[0,\infty]$ , counting processes take values in $\mathbb N\cup\{\infty\}$ , and $\Lambda$ , $\Lambda^*$ take values in the extended reals.

The constant $c_0$ is existential and is chosen after the model data and before $c$ , the policies and the Brownian motions. The threshold relations are required only for the systems with $L^r\ge1$ , which are all but finitely many. Each convergence to a deterministic limit (Theorem 7.1, Lemmas 8.1 and 9.3) is stated as u.o.c. convergence in probability, the paper's own equivalence (p. 633). Theorem 5.2 is stated in coupling form: there are copies of the processes on one probability space, with Skorokhod paths and the same laws, that converge almost surely uniformly on compacts. This is equivalent to weak convergence in $\mathbf D^4$ to a limit with continuous paths. $J^*$ is defined by (44) from an arbitrary pair of independent standard Brownian motions (Mathlib's IsBrownianReal), not by a closed form.

Two formalizations would make the goal trivial, and both are excluded. Leaving out the requirement that $T^{r,*}$ actually follow the policy would make the goal false or empty. Narrowing the class of competing policies, for example to non-anticipating ones, would weaken the theorem. A draft theorem also states that the threshold allocation exists and is unique pathwise, so the hypothesis on $T^{r,*}$ can be satisfied.

The development needs renewal theory (functional central limit theorems, Cramér bounds), multiparameter stopping times, tightness in $\mathbf D$ , the Skorokhod representation theorem, the reflection map, and properties of reflected Brownian motion. Contributions are welcome at every level: proofs of milestones, reusable lemmas on renewal processes and the Skorokhod map, and further lemmas of the paper (Lemmas 7.5, 7.6 and 9.2 are not yet stated).

Selected references

S. L. Bell and R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Ann. Appl. Probab. 11 (2001) 608–649. https://doi.org/10.1214/aoap/1015345343
J. M. Harrison, Heavy traffic analysis of a system with parallel servers: asymptotic optimality of discrete-review policies, Ann. Appl. Probab. 8 (1998) 822–848.
J. M. Harrison and M. J. López, Heavy traffic resource pooling in parallel-server systems, Queueing Systems 33 (1999) 339–368.
J. M. Harrison, Brownian models of queueing networks with heterogeneous customer populations, in Stochastic Differential Systems, Stochastic Control Theory and Their Applications, Springer (1988) 147–186.
S. L. Bell and R. J. Williams, Dynamic scheduling of a parallel server system in heavy traffic with complete resource pooling: asymptotic optimality of a threshold policy, Electron. J. Probab. 10 (2005) 1044–1115.
J. M. Harrison, Brownian Motion and Stochastic Flow Systems, Wiley (1985).

14 thms1 active userReviewed

Completed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

On the Power of Randomization in On-Line Algorithms 1: α-Competitiveness Against Adaptive On-Line and β Against Oblivious Adversaries Give a Deterministic α∘β-Competitive AlgorithmResearch Paper

Why randomization matters in online algorithms

An online algorithm must answer each request before it sees the next one. Its performance is compared with an optimum that may choose all its answers after seeing the complete request string. Randomization can improve an online algorithm's guarantee when the request string is fixed in advance. The comparison changes when an adversary chooses later requests after seeing the algorithm's earlier answers. Ben-David, Borodin, Karp, Tardos and Wigderson studied these choices of adversary in a common request-answer model and proved a general relation between their competitive guarantees (Ben-David et al., 1994, manuscript §§2–3).

The paper distinguishes three adversaries. An oblivious adversary fixes the request string before the algorithm's random choices affect any answer. An adaptive off-line adversary chooses the next request from previous answers but serves the resulting request string optimally after the play. An adaptive on-line adversary also chooses its own answer as each request arrives. The ability to react to answers makes the latter two adversaries materially different from the oblivious one for randomized algorithms (Ben-David et al., 1994, manuscript pp. 7–9).

Request-answer games and competitive cost

A request-answer game has a request set $R$ , a finite nonempty answer set $A$ , and a real cost $f_n(r,a)$ for a request string $r\in R^n$ and an answer string $a\in A^n$ . The off-line optimum for $r$ is $c(r)=\min_{a\in A^n}f_n(r,a)$ . A deterministic online algorithm $D$ returns its $i$ th answer from the first $i$ requests alone; it has no access to the rest of $r$ or to the eventual stopping time. Its cost on $r$ is $c_D(r)=f_n(r,D(r))$ .

A randomized online algorithm is a distribution over deterministic online algorithms. With coins $\omega$ , write $G_\omega$ for the resulting deterministic algorithm. For a fixed request string $r$ , $G$ is $\beta$ -competitive against oblivious adversaries when $\mathbb E_\omega[c_{G_\omega}(r)]\leq\beta(c(r))$ . The paper calls a transformation “linear” when it has the affine form $x\mapsto ux+v$ (Ben-David et al., 1994, manuscript p. 7).

An adaptive off-line adversary $Q$ has a rule from prior answer strings to either the next request or a stop signal, together with a common finite upper bound on play length. Let $r(G_\omega,Q)$ denote its request string and $c_Q(G_\omega)=c(r(G_\omega,Q))$ . Its competitiveness condition places the transformation inside the expectation: $\mathbb E_\omega[c_{G_\omega}(Q)]\leq\mathbb E_\omega[\alpha(c_Q(G_\omega))]$ . An adaptive on-line adversary $S$ has the same request rule and an additional answer rule; its own cost is $c_S(G_\omega)$ , and the corresponding condition uses $\mathbb E_\omega[\alpha(c_S(G_\omega))]$ on the right (Ben-David et al., 1994, manuscript pp. 8–9).

Formalization targets

Randomization against adaptive off-line adversaries

The first target is Theorem 2.1: if some randomized algorithm is $\alpha$ -competitive against every adaptive off-line adversary, a deterministic algorithm has that same guarantee on every request string:

\exists G\;\forall Q,\quad \mathbb E[c_G(Q)]\leq\mathbb E[\alpha(c_Q(G))]\quad\Longrightarrow\quad\exists D\;\forall r,\quad c_D(r)\leq\alpha(c(r)).

Composition of two guarantees

Theorem 2.2 takes an $\alpha$ guarantee for $G$ against adaptive on-line adversaries and a $\beta$ guarantee for another randomized algorithm against oblivious adversaries. It concludes that $G$ has the composed guarantee against adaptive off-line adversaries:

\mathbb E[c_G(Q)]\leq\mathbb E[(\alpha\circ\beta)(c_Q(G))]\qquad\text{for every }Q.

The mission goal is Corollary 2.1, the deterministic consequence of these two results:

\exists D\;\forall r,\qquad c_D(r)\leq(\alpha\circ\beta)(c(r)).

The milestones follow the paper's two theorems and the stated claims in their proofs, including the finite-horizon winning-position formulation and the adversary that simulates a fixed online algorithm (Ben-David et al., 1994, manuscript pp. 9–13).

What the result supplies

The corollary turns the existence of two randomized guarantees under different information rules into the existence of a deterministic online strategy with an explicit composed cost transformation. It is an existence result: it does not say that the deterministic strategy can be computed efficiently from the randomized algorithms. The paper itself notes that such a construction is unavailable in full generality and then examines settings where constructive versions are possible (Ben-David et al., 1994, manuscript p. 13).

The mathematical results were proved in the 1994 paper; this mission asks for machine-checked Lean proofs of the abstract model, the intermediate claims, and Corollary 2.1. The local draft currently contains compiled statements with proof placeholders, so it does not yet provide checked proofs. A completed development would make the adversary distinctions and the exact placement of expectations available for reuse in later online-algorithm formalizations.

Why the proof is difficult

The apparent shortcut is to treat an adaptive request sequence as fixed and apply a guarantee against oblivious adversaries directly. That loses the dependence of later requests on the algorithm's earlier answers. For Theorem 2.1, a winning request strategy must have one finite horizon that works for every answer path; separate finite horizons for each branch do not suffice when the answer set is infinite. For Theorem 2.2, the simulated adversary must make its own answers before the algorithm answers the current request, while still matching a fixed online benchmark along every resulting play. The expectation inequalities must remain valid when the request string itself depends on the algorithm's coins (Ben-David et al., 1994, manuscript pp. 9–11).

Formalization scope

Lean represents requests and answers as oldest-first lists. List index zero is request one in the paper. The general game is a separate definition; the algorithm, adversary, and competitiveness definitions build on it. An off-line adversary's rule returns Option R, where none is the stop signal, and has a uniform finite depth bound. A randomized algorithm consists of a coin probability space and a deterministic prefix algorithm for each coin; its answer events are measurable. Finiteness of $A$ and bounded play depth make the cost of each fixed adversarial play take finitely many values, so its real expectation is an ordinary integrable expectation.

The formal game uses real-valued costs, a deliberate restriction of the paper's $\mathbb R\cup\{\infty\}$ costs. The answer set is finite and nonempty, while the request set may be infinite. The transformations $\alpha$ and $\beta$ are affine. Theorem 2.2 and the goal assume $\alpha$ is monotone: the paper applies $\alpha$ to an inequality in its proof, and its competitive-ratio examples have positive slope. Theorem 2.1 does not need this added assumption. The two randomized algorithms may have different coin spaces, each an arbitrary Lean type at the declaration's universe level. The off-line and on-line adaptive comparisons retain $\alpha$ inside the expectation.

The target ranges over every equal-length request and answer play generated by these rules, including an adversary that stops without a request. It does not allow the deterministic algorithm to see future requests or choose a different policy for each adversary. Reusable contributions include the game interface, bounded adaptive plays, measurable randomized algorithms, and finite-horizon winning positions. The statements of all three principal results, their intervening claims, and proofs of those statements are within scope.

Selected references

S. Ben-David, A. Borodin, R. Karp, G. Tardos and A. Wigderson, On the Power of Randomization in On-Line Algorithms, Algorithmica 11, 1994. DOI: 10.1007/BF01294260. The local source is the authors' 20-page manuscript; citations above use its page numbers.

11 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization 3: Fractional Double Greedy on the Multilinear Extension Achieves 1/2 of the OptimumResearch Paper

Motivation

Unconstrained submodular maximization (USM) asks for a subset $S$ of a finite ground set $\mathcal N$ maximizing a nonnegative submodular function $f$ . It contains Max-Cut, Max-DiCut and maximum facility location as special cases, and it is the basic subproblem of many constrained submodular maximization algorithms. Because $f$ is given only through a value oracle, the question is how close to the optimum a polynomial number of queries can get.

Timeline of the approximation ratio for USM in the value oracle model:

Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) showed that a uniformly random set achieves $1/4$ , local search achieves $1/3$ and $2/5$ , and that no algorithm making polynomially many queries achieves $1/2 + \varepsilon$ for any fixed $\varepsilon > 0$ .
Oveis Gharan and Vondrák (SODA 2011) reached $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) reached $0.42$ .
Buchbinder, Feldman, Naor and Schwartz (FOCS 2012) closed the gap with the double greedy algorithms: a deterministic $1/3$ -approximation and a randomized $1/2$ -approximation, both linear in the number of oracle calls. Their Appendix A gives a third, fractional variant, which is the subject of this mission.

This is the third mission on the FOCS 2012 paper; the first two treat the deterministic and the randomized double greedy on sets.

Setting

Let $\mathcal N$ be a finite ground set with $n$ elements and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$ . The function $f$ is submodular if

f(A) + f(B) \ge f(A \cup B) + f(A \cap B) \qquad \text{for all } A, B \subseteq \mathcal N .

Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$ and let $OPT$ be a maximizing set.

The multilinear extension of $f$ is the function on vectors $x \in [0,1]^{\mathcal N}$

F(x) = \sum_{S \subseteq \mathcal N} f(S) \prod_{u \in S} x_u \prod_{u \notin S} (1 - x_u) = \mathbb E\bigl[f(R(x))\bigr],

where the random set $R(x)$ contains each element $u$ independently with probability $x_u$ . A set is identified with its characteristic vector, so $F$ agrees with $f$ on $\{0,1\}^{\mathcal N}$ , and $\{u\}$ also denotes the unit vector at $u$ . For vectors, $x \vee y$ and $x \wedge y$ are the coordinate-wise maximum and minimum.

Algorithm 4 (MultilinearUSM). Fix an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and start from $x_0 = \emptyset$ and $y_0 = \mathcal N$ (the vectors $\mathbf 0$ and $\mathbf 1$ ). In iteration $i = 1, \dots, n$ compute

a_i = F(x_{i-1} + \{u_i\}) - F(x_{i-1}), \qquad b_i = F(y_{i-1} - \{u_i\}) - F(y_{i-1}),

set $a_i' = \max\{a_i, 0\}$ , $b_i' = \max\{b_i, 0\}$ , and update

x_i = x_{i-1} + \frac{a_i'}{a_i' + b_i'} \{u_i\}, \qquad y_i = y_{i-1} - \frac{b_i'}{a_i' + b_i'} \{u_i\},

with the convention that the two fractions are $1$ and $0$ when $a_i' = b_i' = 0$ . The output is the random set $R(x_n)$ . Every choice before the output is deterministic; the algorithm queries $F$ at four points per element.

For the analysis, $OPT_i = (OPT \vee x_i) \wedge y_i$ .

Formalization targets

Goal: Theorem A.1, oracle-access clause

For every nonnegative submodular $f$ and every order of the ground set,

x_n = y_n \qquad\text{and}\qquad f(OPT) \le 2\,F(x_n) = 2\,\mathbb E\bigl[f(R(x_n))\bigr].

Milestones, in the order the proof uses them

$a_i + b_i \ge 0$ at every iteration (proof of Lemma A.2; the page cites Lemma II.1).
Endpoints: $OPT_0 = OPT$ with $F(OPT) = f(OPT)$ , and $OPT_n = x_n = y_n$ .
(4) and (5): if $a_i \ge 0$ and $b_i > 0$ , then $F(x_i) - F(x_{i-1}) = a_i^2/(a_i+b_i)$ and $F(y_i) - F(y_{i-1}) = b_i^2/(a_i+b_i)$ .
(6): in the same case, $F(OPT_{i-1}) - F(OPT_i) \le a_i b_i/(a_i + b_i)$ , whether or not $u_i \in OPT$ .
Lemma A.2: for every $1 \le i \le n$ ,

F(OPT_{i-1}) - F(OPT_i) \le \tfrac12\bigl[F(x_i) - F(x_{i-1}) + F(y_i) - F(y_{i-1})\bigr].

Telescoped display: $F(OPT_0) - F(OPT_n) \le \tfrac12[F(x_n) - F(x_0)] + \tfrac12[F(y_n) - F(y_0)] \le \tfrac12(F(x_n) + F(y_n))$ .

Significance

The result. Theorem A.1 shows that the double greedy analysis survives a change of domain: the factor $1/2$ is obtained by a procedure that never flips a coin until the end, and whose state is a pair of fractional points. The ratio matches the Feige–Mirrokni–Vondrák hardness bound, so it cannot be improved in the value oracle model. Its output is a fractional point together with an independent rounding, which separates the optimization from the rounding step.

Formalizing it. The result is proved on paper; no machine-checked proof of a double greedy guarantee is known. A complete development yields reusable facts about the multilinear extension of a submodular function on a finite type: $F$ is affine in each coordinate, its coordinate increments are antitone in the other coordinates on $[0,1]^{\mathcal N}$ , and $F$ restricted to characteristic vectors is $f$ . These are the standard tools of every continuous-relaxation argument for submodular maximization.

Difficulty

The proof on the page is short, but it relies on two facts it does not prove. First, the page justifies $a_i + b_i \ge 0$ "by Lemma II.1", which is a statement about sets; for vectors it requires that the increment of $F$ along a coordinate decreases as the other coordinates increase, a property of the multilinear extension of a submodular function that must be derived from the sum defining $F$ . Second, inequality (6) is written out only for $u_i \notin OPT$ , and Case 2 of Lemma A.2 is omitted as analogous; the formal statements cover all cases. The main technical work is the bookkeeping of the run: that each coordinate is touched once, that $x_{i-1}(u_i) = 0$ and $y_{i-1}(u_i) = 1$ when it is touched, that $x_i \le OPT_i \le y_i$ , and that every state stays in $[0,1]^{\mathcal N}$ , where the antitonicity applies.

Formalization scope

The ground set is a Fintype $X$ with decidable equality; sets are Finset X; $f$ is real-valued, with nonnegativity a hypothesis ∀ S, 0 ≤ f S wherever the page uses it (the goal and the telescoped display). Submodularity is the published NonmonotoneSubmod.Shared.Submodular, the lattice form $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$ ; $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT; $F$ is the published NonmonotoneSubmod.Shared.F, the sum above, defined for every $x : X \to \mathbb R$ .
The order $u_1, \dots, u_n$ is a duplicate-free list containing every element; $u_i$ is the entry at index $i-1$ , and $n$ is the list's length. The state after $i$ iterations is obtained by folding one step over the first $i$ entries from $(\mathbf 0, \mathbf 1)$ . Statements hold for every such order.
The footnote's convention $a_i'/(a_i'+b_i') = 1$ , $b_i'/(a_i'+b_i') = 0$ when $a_i' = b_i' = 0$ is an explicit case split; with Lean's $0/0 = 0$ it would otherwise be reversed and the run would no longer end with $x_n = y_n$ .
Corrected slips of the page: lines 3–4 of Algorithm 4 assign $a_i', b_i'$ but define $a_i, b_i$ ; " $f : \mathcal N \to \mathbb R^+$ " means $f : 2^{\mathcal N} \to \mathbb R^+$ ; " $F(x) \triangleq \mathbb E[R(x)]$ " means $\mathbb E[f(R(x))]$ ; "NSM" in Theorem A.1 means USM. The main text's one-line definition of submodularity, read literally, forces monotonicity; the footnote's lattice form is used.
Not formalized: the sampling clause of Theorem A.1 (ratio $(1/2) - o(1)$ without oracle access to $F$ , whose proof the paper refers to Calinescu, Chekuri, Pál and Vondrák) and the running time. The guarantee is stated for the algorithm as printed, so the trivial existence of a $1/2$ -approximation by exhaustive search does not satisfy it. A statement in which $x_n$ is an arbitrary point, or the state any process with $x_i \le y_i$ , would not be this theorem.
Contributions welcome: the multilinear-extension facts above as general lemmas, the run invariants, and proofs of the milestones in any order.

Selected references

N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012, 649–658. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205; its numbering differs and is not used here).
U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011, 1133–1153. https://doi.org/10.1137/090779346
S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011, 1098–1117. https://doi.org/10.1137/1.9781611973082.83
M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011, 342–353. https://doi.org/10.1007/978-3-642-22006-7_29
G. Calinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a Monotone Submodular Function Subject to a Matroid Constraint, SIAM J. Comput. 40(6), 2011, 1740–1766. https://doi.org/10.1137/080733991

11 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Stochastic Systems·Captain: mikedeng1

Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance II: An O(n²) Extended Formulation of the Multiclass M/M/1 Performance PolymatroidResearch Paper

Motivation

A single server shared by several classes of customers is the basic model of scheduling under uncertainty: jobs of different types arrive at random, need random amounts of work, and a scheduler decides at every moment which type to serve. A classical way to optimize such a system, the achievable region approach, describes the set of all performance vectors that some scheduling policy can attain, and optimizes a linear cost over that set with linear programming. For the multiclass M/M/1 queue under preemptive, work-conserving scheduling, this set is a polyhedron described by conservation laws (Coffman and Mitrani, 1980; Gelenbe and Mitrani, 1980; Shanthikumar and Yao, 1992): it is the base of a polymatroid, its vertices are the performance vectors of the $n!$ strict priority rules, and minimizing a linear cost over it is solved greedily, which recovers the $c\mu$ rule.

That description uses one inequality for every nonempty set of classes, $2^n-1$ constraints in all. Bertsimas, Paschalidis and Tsitsiklis (working paper 1992, Annals of Applied Probability 1994) derived performance bounds for general multiclass networks from quadratic potential functions. Specialized to one station, their nonparametric method produces a different polyhedron, in $O(n^2)$ variables with $O(n^2)$ constraints, and they show that its projection is exactly the conservation-law polyhedron (Theorem 8.4). The paper remarks that this confirms, for this polymatroid, the belief that problems solvable in polynomial time admit polynomial-size formulations.

Setting

There are $n$ customer classes $E=\{1,\dots,n\}$ . Class $i$ has arrival rate $\lambda_i>0$ and service rate $\mu_i>0$ ; its traffic intensity is $\rho_i=\lambda_i/\mu_i$ , and the queue is stable: $\sum_{i\in E}\rho_i<1$ . For $S\subseteq E$ define

b(S)=\frac{\sum_{i\in S}\rho_i/\mu_i}{1-\sum_{i\in S}\rho_i},\qquad b(\emptyset)=0 .

In the queue, $n_i$ is the steady-state mean number of class $i$ customers and $n_i/\mu_i$ their mean remaining work; $b(S)$ is the mean work of the classes in $S$ when those classes have preemptive priority over the rest.

The performance polymatroid P1 (Theorem 8.3) is the set of $(n_i)\in\mathbb R_+^n$ with

\sum_{i\in S}\frac{n_i}{\mu_i}\ge b(S)\quad (S\subset E),\qquad \sum_{i\in E}\frac{n_i}{\mu_i}=b(E).

For a permutation $\pi=(\pi_1,\dots,\pi_n)$ of $E$ , the vector $v(\pi)$ is the solution of the triangular system $\sum_{j=1}^{k}x_{\pi_j}/\mu_{\pi_j}=b(\{\pi_1,\dots,\pi_k\})$ , $k=1,\dots,n$ (Eq. (58) with $f_i^S=1/\mu_i$ ).

The extended formulation P2 (Theorem 8.4) is the set of nonnegative $(n_i)_{i\in E}$ and $(I_{ij})_{i,j\in E}$ satisfying

\mu_iI_{ii}-\lambda_in_i=\lambda_i,\qquad \mu_iI_{ij}+\mu_jI_{ji}-\lambda_jn_i-\lambda_in_j=0\ (i\neq j),\qquad \sum_{i\in E}I_{ij}=n_j .

In the queue, $I_{ij}$ is the steady-state mean of the number of class $j$ customers on the event that the server is busy with class $i$ . The projection $\mathrm{P2}'$ of P2 is the set of $(n_i)$ for which some $(I_{ij})$ makes $((n_i),(I_{ij}))$ a point of P2.

Formalization targets

Goal: Theorem 8.4

\mathrm{P2}'=\mathrm{P1}.

Both inclusions are part of the goal. The statement fixes no constants and holds for every $n$ , every positive rate vector and every stable load.

Milestones

§8.2, proof of Theorem 8.3. The extreme points of P1 are exactly the vectors $v(\pi)$ , and P1 is their convex hull:

\operatorname{ext}\mathrm{P1}=\{v(\pi)\},\qquad \mathrm{P1}=\operatorname{conv}\{v(\pi)\}.

§8.2, proof of Theorem 8.4. The easy inclusion, which the paper obtains from its Theorem 4.4:

\mathrm{P2}'\subseteq\mathrm{P1}.

Significance

The result. Theorem 8.4 replaces $2^n-1$ constraints by $O(n^2)$ constraints in $O(n^2)$ variables without changing the projected set. Any linear program over the M/M/1 performance region, including problems with side constraints where the greedy $c\mu$ rule no longer applies, can then be solved with a polynomial-size LP. It also identifies the paper's nonparametric method as exact at a single station: the method loses nothing there, which is the baseline against which its gaps in networks are measured.

Formalizing it. The result is proved in the paper, but the reverse inclusion $\mathrm{P1}\subseteq\mathrm{P2}'$ is argued through achievability: every point of P1 is the performance of some (randomized) policy, and every policy's performance satisfies the equations of P2. That argument rests on stochastic objects (invariant distributions under arbitrary policies, and time-0 randomizations over priority rules) that the paper does not define precisely. The paper points to a purely combinatorial derivation in Paschalidis' thesis, which we have not seen. A machine-checked proof of the polyhedral identity is therefore new content: it supplies the deterministic argument the paper delegates. The polymatroid structure of P1 (Milestone 1) is classical for supermodular set functions; this mission requires it for this specific $b$ . We know of no formalization of either result.

Difficulty

The inclusion $\mathrm{P2}'\subseteq\mathrm{P1}$ only combines the equations of P2 with nonnegativity. The reverse inclusion is the hard half: for each point of P1 one must exhibit a nonnegative matrix $(I_{ij})$ satisfying $n^2$ linear equations, and the inequalities of P1 say nothing directly about the off-diagonal entries $I_{ij}$ . The paper's own argument does not help here, since it produces $I$ as a steady-state expectation under a scheduling policy, an object defined through a Markov chain and given in no closed form. The sign constraints $I_{ij}\ge0$ are where the $2^n-1$ inequalities of P1 are encoded, and a proof has to explain how $O(n^2)$ sign conditions on auxiliary variables carry exactly the information of exponentially many inequalities in the original ones.

Formalization scope

Classes are Fin n; rates are real functions lam mu : Fin n → ℝ with 0 < lam i, 0 < mu i and ∑ i, lam i / mu i < 1. The paper's $n_i$ is written x i, because n is the number of classes. A point of P2 is a pair (x, I) with I i j $=I_{ij}$ , including the diagonal entries. P1 is the platform definition AllocationIndices.achievablePolytope with the matrix $A^S_i=1/\mu_i$ : inequality for every $S\neq E$ , equality at $S=E$ , nonnegativity. The paper writes $N$ for the class set $E$ in (65) and (71); every such sum runs over all classes. The constraints (64)–(65) bound $n_i/\mu_i$ , not $n_i$ . $v(\pi)$ is given by its closed form, $v(\pi)_{\pi_k}=\mu_{\pi_k}\bigl(b(\{\pi_1,\dots,\pi_k\})-b(\{\pi_1,\dots,\pi_{k-1}\})\bigr)$ , which solves (58). The standing hypothesis $\lambda_i>0$ is presupposed by the model (Poisson arrivals at rate $\lambda_i$ ); the load condition is the paper's stability condition and keeps every denominator of $b$ positive.

No statement involves a policy, a Markov chain or an expectation; the queueing meaning above is motivation only. In particular, neither "P1 is the achievable region" nor "the performance vector of each priority rule is achievable" is formalized. The goal is the full set identity: stating only $\mathrm{P2}'\subseteq\mathrm{P1}$ , or assuming $\mathrm{P1}=\operatorname{conv}\{v(\pi)\}$ as a hypothesis of the goal, would not be Theorem 8.4.

A complete development needs: supermodularity of $b$ under the load condition; the greedy (Edmonds) description of base polytopes of supermodular functions, which is reusable well beyond this mission; and a nonnegative solution of the P2 system at each $v(\pi)$ . Contributions of any of these as separate lemmas are welcome.

Selected references

D. Bertsimas, I. Ch. Paschalidis, J. N. Tsitsiklis, Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance, MIT Sloan School WP #3509-92-MSA, 1992; Annals of Applied Probability 4(1):43–75, 1994. https://doi.org/10.1214/aoap/1177005200
E. G. Coffman, I. Mitrani, A characterization of waiting time performance realizable by single-server queues, Operations Research 28(3):810–821, 1980. https://doi.org/10.1287/opre.28.3.810
J. G. Shanthikumar, D. D. Yao, Multiclass queueing systems: polymatroidal structure and optimal scheduling control, Operations Research 40(S2):S293–S299, 1992. https://doi.org/10.1287/opre.40.3.S293
D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21(2):257–306, 1996. https://doi.org/10.1287/moor.21.2.257
J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, pp. 69–87.

5 thms3 active usersReviewed

Completed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

On the Power of Randomization in On-Line Algorithms 3: An Augmented Potential Function Yields an Explicit Deterministic α∘β-Competitive AlgorithmResearch Paper

Motivation

Competitive analysis measures an online algorithm, which must answer each request before seeing the next, against the best off-line answer to the whole request sequence. Randomized online algorithms are often much better than deterministic ones against an oblivious adversary, who fixes the requests in advance; the paging problem is the standard example. Against an adaptive adversary, who sees the algorithm's answers before choosing the next request, the advantage can disappear.

Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994; preliminary version STOC 1990) made this precise in an abstract framework of request-answer games. Their Corollary 2.1 says: if a game has a randomized algorithm that is $\alpha$ -competitive against adaptive on-line adversaries and one that is $\beta$ -competitive against oblivious adversaries, then it has a deterministic $\alpha\circ\beta$ -competitive algorithm. That proof is non-constructive: it goes through a game-theoretic determinacy argument. Section 3 of the paper gives a constructive version. Most competitive analyses of randomized algorithms against adaptive adversaries are carried out with a potential function, in the style of Manasse, McGeoch and Sleator (J. Algorithms 11, 1990). The paper shows that such a potential function, together with any oblivious-competitive algorithm $H$ , determines an explicit deterministic algorithm $M$ , answer by answer. This mission formalizes that construction and its guarantee.

Setting

A request-answer game has a request set $R$ , a finite answer set $A$ and cost functions $f_n : R^n \times A^n \to \mathbb R$ . The off-line optimum of $r \in R^n$ is $c(r) = \min_{a \in A^n} f_n(r, a)$ . A deterministic online algorithm $M$ is a sequence of maps $m_i : R^i \to A$ ; on $r = (r_1,\dots,r_n)$ it answers $M(r) = (m_1(r_1), m_2(r_1,r_2), \dots, m_n(r))$ , at cost $c_M(r) = f_n(r, M(r))$ . It is $\alpha$ -competitive if $c_M(r) \le \alpha(c(r))$ for all $r$ . Throughout, $\alpha$ and $\beta$ are affine maps $\mathbb R \to \mathbb R$ (the paper's "linear functions").

A randomized online algorithm $H$ is a probability distribution over deterministic algorithms $H_y$ ; it is $\beta$ -competitive against any oblivious adversary if $\mathbb E_y[f_n(r, H_y(r))] \le \beta(c(r))$ for all $r$ . The algorithm $G$ analysed by the potential function is described by its next-answer laws $g_{n+1}(r r_{n+1}, a)$ on $A$ , given the requests so far, the new request and its own past answers. An adaptive on-line adversary $S$ chooses each request from the algorithm's past answers and answers it itself, before the algorithm does, for at most $d_Q$ rounds; a configuration after $n$ rounds is $(r, a, b) \in R^n \times A^n \times A^n$ : requests, algorithm's answers, adversary's answers.

An augmented potential function for $\alpha$ and $G$ (Definition 3.1) is a family $\Phi_n : R^n \times A^n \times A^n \to \mathbb R$ with (1) $\Phi_0 = 0$ ; (2) $\Phi_n(r,a,b) \le \alpha(f_n(r,b)) - f_n(r,a)$ for every configuration; (3) $\mathbb E_{a_{n+1} \sim g_{n+1}(r r_{n+1}, a)}[\Phi_{n+1}(r r_{n+1}, a a_{n+1}, b b_{n+1})] \ge \Phi_n(r,a,b)$ for every configuration, every $r_{n+1} \in R$ and every $b_{n+1} \in A$ .

Formalization targets

Goal: Theorem 3.1 (p. 15)

Let $\Phi$ be an augmented potential function for $\alpha$ and $G$ , and $H$ a $\beta$ -competitive algorithm against oblivious adversaries. Say that $M$ obeys the potential rule if for every $r \in R^n$ and $r' = rt$ ,

\mathbb E_y\big[\Phi_{n+1}(r', M(r)\,m_{n+1}(r'), H_y(r'))\big] \ \ge\ \mathbb E_y\big[\Phi_n(r, M(r), H_y(r))\big].

Then such an $M$ exists, and every such $M$ satisfies

c_M(r) \le \alpha\big(\beta(c(r))\big) \quad \text{for all } r .

Both parts are part of the goal: the rule can be followed, and following it guarantees $\alpha\circ\beta$ -competitiveness.

Milestones

In every play of $G$ against an adaptive on-line adversary, the expected final potential is nonnegative (proof of Lemma 3.1).
Lemma 3.1, "if" direction: an augmented potential function for $\alpha$ and $G$ makes $G$ $\alpha$ -competitive against any adaptive on-line adversary, $\mathbb E[c_G(S)] \le \mathbb E[\alpha(c_S(G))]$ .
For every $r$ , $t$ and every $a \in A^n$ , some $a' \in A$ satisfies $\mathbb E_y[\Phi_{n+1}(rt, aa', H_y(rt))] \ge \mathbb E_y[\Phi_n(r, a, H_y(r))]$ .
If $M$ obeys the rule, $\mathbb E_y[\Phi_n(r, M(r), H_y(r))] \ge 0$ for every $r$ .
If $M$ obeys the rule, $f_n(r, M(r)) \le \mathbb E_y[\alpha(f_n(r, H_y(r)))]$ for every $r$ : $M$ is $\alpha$ -competitive against the randomized adaptive adversary that serves its requests with $H$ .

Significance

The theorem turns two separate analyses into one deterministic algorithm with an explicit description. The potential function certifies $G$ against the strongest on-line adversary; the oblivious algorithm $H$ need not be related to $G$ , and the paper remarks that $H$ may be $G$ itself. The next answer of $M$ is computable whenever the expected potential under $H$ is (Corollary 3.1, stated informally in the paper), and the paper notes that for the potential functions used in the $K$ -server literature this expectation is computable in time polynomial in the number of nodes and $K$ . Read in this light, a potential-function proof for a randomized algorithm doubles as a deterministic algorithm.

The result is proved in the paper. As far as is known, neither this theorem nor the abstract framework of request-answer games with adaptive adversaries has a machine-checked formalization. The mission produces that framework and a checked derandomization principle that applies to every request-answer game with real costs, not to one problem.

Difficulty

The obvious argument for the existence of $m_{n+1}(r')$ averages property (3) of $\Phi$ ; the work is in seeing which configuration to apply it to. The rule compares $M$ 's configuration against $H_y$ 's answers, not against an adversary playing $G$ , and the paper argues through an auxiliary on-line adversary that asks $r'$ and serves it with $H_y$ . Making this rigorous requires interchanging the expectation over $H$ 's coins with the finite expectation over $G$ 's next answer, and checking that the needed expectations are finite.

The second difficulty is the two kinds of randomness. $G$ enters only through its next-answer laws, while $H$ must be a single distribution over deterministic algorithms: the rule evaluates $H_y(r)$ and $H_y(r')$ with the same coins $y$ . Replacing $H$ by a behavioural description breaks the coupling between consecutive rounds.

Formalization scope

Requests and answers are Lean lists, oldest first, and $f_n(r,a)$ is F.cost r a on lists of common length; values on lists of different lengths are never used. Costs are real: the paper allows $f_n = +\infty$ , so every statement here is about the real-valued games. The answer type is finite and nonempty, so the minimum $c(r)$ exists. Affine maps are written $\alpha(x) = c x + d$ . The goal additionally assumes $\alpha$ nondecreasing: the last step of the paper's proof applies $\alpha$ to an inequality, which needs it, and the paper's examples are positive ratios. In Lemma 3.1 and milestone 5 linearity of $\alpha$ is kept as the paper's standing convention, although with $\alpha$ inside the expectation the argument does not use it.

$G$ is a map from (requests, own answers) to a probability mass function on $A$ (behavioural form); its play against an adaptive on-line adversary is a probability mass function on final configurations, with finite support, and its expectations are finite sums. $H$ is a probability measure on a coin space with a deterministic algorithm per coin, each answer measurable in the coins; expectations over $H$ are Bochner integrals of functions with finitely many values. $\alpha$ stays inside expectations, as in the paper's definition of competitiveness against adaptive adversaries. Adversaries stop by returning none and have a uniform depth bound.

The goal cannot be satisfied vacuously: it states the existence of an algorithm obeying the rule alongside the guarantee for every such algorithm, and Definition 3.1 is required at every configuration, not only at reachable ones.

Not formalized: the "only if" direction of Lemma 3.1, which the paper only sketches, and Corollary 3.1, whose notion of computability the paper leaves unspecified. The definitions of request-answer games, online algorithms, adversaries and competitiveness are reusable for the other missions of this paper and for any problem-specific competitive analysis. Contributions welcome: proofs of the milestones, and a lemma relating the mixed and behavioural forms of a randomized algorithm.

Selected references

S. Ben-David, A. Borodin, R. Karp, G. Tardos, A. Wigderson, On the power of randomization in on-line algorithms, Algorithmica 11 (1994), 2–14. https://doi.org/10.1007/BF01294260
M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, Journal of Algorithms 11 (1990), 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
D. Sleator, R. Tarjan, Amortized efficiency of list update and paging rules, Communications of the ACM 28 (1985), 202–208. https://doi.org/10.1145/2786.2793
A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998. ISBN 0-521-56392-5

9 thms3 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

On the Power of Randomization in On-Line Algorithms 4: Restarting a Bounded-Cost Algorithm Is (1+ε)α-Competitive in Games of Finite DiameterResearch Paper

Motivation

Competitive analysis compares an online algorithm, which must answer each request before seeing the next, with the optimal off-line solution of the same request sequence. Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994) set up a general framework, request-answer games, in which paging, the $K$ -server problem and metrical task systems are all instances, and used it to compare the power of randomized algorithms against several kinds of adversaries.

One of their results (Theorem 2.1) says that if a randomized algorithm is $\alpha$ -competitive against every adaptive off-line adversary, then some deterministic algorithm is already $\alpha$ -competitive. The argument is a game-theoretic existence proof: it says nothing about how to compute the deterministic algorithm. Section 4 of the paper, "A Constructive Version of Theorem 2.1", answers the natural follow-up question for a large class of games: under monotonicity, locality and a finite diameter, a deterministic algorithm that loses only a factor $1+\epsilon$ can be assembled from a finite object.

Setting

A request-answer game $F$ has a request set $R$ , a finite answer set $A$ , and cost functions $f_n : R^n \times A^n \to \mathbb{R}$ , $n \ge 0$ ; $f_0$ is the cost of the empty play. The off-line optimum of a request sequence $r$ of length $n$ is $c(r) = \min_{a \in A^n} f_n(r, a)$ . A deterministic online algorithm $G$ answers the $i$ -th request by a function $g_i(r_1, \dots, r_i)$ of the requests so far; its cost on $r$ is $c_G(r) = f_n(r, G(r))$ . It is $\alpha$ -competitive if $c_G(r) \le \alpha(c(r))$ for every $r$ .

The game is monotone if $f_{n+1}(rt, ab) \ge f_n(r, a)$ always, and local if for every $h > 0$ only finitely many request sequences have $c(r) \le h$ . The discrepancy of two request-answer sequences is

\delta((r,a),(r',a')) = f(rr', aa') - f(r,a) - f(r',a'),

and the diameter $D(F)$ is the supremum of $|\delta|$ over all pairs.

For a real $H$ , the set $R_H$ consists of the request sequences all of whose proper prefixes have off-line optimum at most $H$ . Given a deterministic algorithm $A_H$ , the restart algorithm simulates $A_H$ and, as soon as the request sequence leaves $R_H$ , starts over as if it had received no previous requests. This cuts every request sequence into segments $r = r(1)\, r(2) \cdots r(t)$ , each a longest prefix in $R_H$ of what remains.

Formalization targets

Goal: Theorem 4.1 through its construction

Let $F$ be monotone and local, with finite nonempty $R$ and $A$ , $f_0 \ge 0$ , and diameter at most $D$ . Let $\alpha(x) = d\,x$ with $d \ge 1$ , $\epsilon > 0$ , and

H = \frac{(2+\epsilon) D}{\epsilon}.

Then $R_H$ is finite; the restart algorithm depends on $A_H$ only through its values on $R_H$ ; and for every $A_H$ with $c_{A_H}(r) \le \alpha(c(r))$ on $R_H$ ,

c_{\mathrm{Restart}}(r) \le (1+\epsilon)\,\alpha(c(r)) \qquad \text{for all request sequences } r.

Milestones (proof of Theorem 4.1, pp. 17–18)

$R_H$ is finite.
The restart rule produces the greedy decomposition into longest prefixes in $R_H$ .
The restart algorithm answers $A_H(r(1)), A_H(r(2)), \dots, A_H(r(t))$ .
$c(r(i)) \ge H$ for $i = 1, \dots, t-1$ .
$c(r) \ge c(r(1)) + \sum_{i=2}^{t} (c(r(i)) - D(F))$ .
$c_{\mathrm{Restart}}(r) \le \alpha(c(1)) + \sum_{i=2}^{t} (\alpha(c(i)) + D(F))$ .

Significance

Theorem 2.1 shows that, against adaptive off-line adversaries, randomization gives no advantage, but only as an existence statement. Theorem 4.1 turns it into a recipe: a deterministic algorithm need only be good on the finite set $R_H$ , which can be prepared in advance, and restarting extends it to all inputs at a loss of $1+\epsilon$ . The paper illustrates this with $K$ -server problems on finite graphs, where $A_H$ is a finite table and each step of the resulting algorithm costs one dynamic-programming evaluation of an off-line optimum.

The restart construction is of independent use: it is a general way to turn a guarantee on bounded-cost inputs into a guarantee on all inputs when the cost is nearly additive over concatenation.

To our knowledge neither the abstract request-answer game model nor this theorem has a machine-checked proof. The mission produces a formal model of request-answer games with the monotonicity, locality and diameter conditions, the restart algorithm as an explicit definition, and the full chain of inequalities of the proof.

Difficulty

The individual inequalities are elementary; the work lies in the bookkeeping of the construction. The algorithm is defined online, one request at a time, while the analysis is phrased through the decomposition of the whole sequence. Relating the two requires showing that the online rule produces exactly the decomposition into longest prefixes in $R_H$ , and that the answers produced on each segment are those of $A_H$ run from scratch, so that the cost of the whole play can be compared with the costs on the segments. The constants must close exactly: with $H = (2+\epsilon)D/\epsilon$ the additive losses at the $t-1$ cuts, on both the algorithm's side and the optimum's side, must be absorbed by the factor $1+\epsilon$ , and they do so only for ratios $d \ge 1$ .

A tempting shortcut is to conclude Theorem 4.1 from Theorem 2.1 directly: a deterministic $\alpha$ -competitive algorithm is trivially $(1+\epsilon)\alpha$ -competitive when costs are nonnegative. This proves the sentence of the theorem without its point, and is ruled out below.

Formalization scope

Request and answer sequences are Lean Lists, oldest first; $f_n(r,a)$ is F.cost r a with r.length = a.length. Costs are real-valued (the paper allows $+\infty$ ; real costs are a special case).
The answer set is a Fintype and nonempty; in the goal the request set is a Fintype and nonempty.
A deterministic algorithm is one function List R → A. Competitiveness of a deterministic algorithm against adaptive off-line adversaries is stated as competitiveness on every request sequence, which is equivalent for deterministic algorithms (p. 8).
Finite diameter is a real bound $D$ with $|\delta| \le D$ for all pairs, and every statement holds for every such $D$ , in particular $D = D(F)$ ; no real supremum is taken.
$f_0 \ge 0$ is assumed in the goal; with monotonicity it makes every cost nonnegative. It holds in the paper's examples.
$\alpha(x) = d\,x$ with $d \ge 1$ in the goal; the cost bound for the restart algorithm (milestone 6) holds for an arbitrary $\alpha$ .
$H$ is fixed to the paper's value $(2+\epsilon)D/\epsilon$ .
The restart algorithm is a definition (a left fold over the requests), not a hypothesis. The paper's assumption of a randomized algorithm competitive against adaptive off-line adversaries is used only, through Theorem 2.1, to obtain $A_H$ ; the goal quantifies over every $A_H$ that is $\alpha$ -competitive on $R_H$ . "Computable" has no precise meaning for real costs; its content is the finiteness of $R_H$ together with the fact that the restart algorithm reads $A_H$ only on $R_H$ . A formalization that proves only the existence of a deterministic $(1+\epsilon)\alpha$ -competitive algorithm, without the construction, does not meet the goal.
Milestones 5 and 6 are stated for nonempty request sequences, so that $t \ge 1$ ; milestone 5 is stated for every decomposition into consecutive pieces.

Contributions welcome: proofs of the milestones, and a connection to the other missions of this series, where the randomized model and Theorem 2.1 are formalized.

Selected references

S. Ben-David, A. Borodin, R. Karp, G. Tardos, A. Wigderson, On the power of randomization in on-line algorithms, Algorithmica 11 (1994). https://doi.org/10.1007/BF01294260
M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, New results on server problems, SIAM Journal on Discrete Mathematics 4 (1991), 172–181. https://doi.org/10.1137/0404017

10 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

A Multicut Algorithm for Two-Stage Stochastic Linear Programs 1: Worst-Case Bound on Multicut Major IterationsResearch Paper

Motivation

Two-stage stochastic linear programs with recourse are a standard model for planning under uncertainty: a first-stage decision $x$ is taken before a random outcome $\xi$ is observed, and a second-stage (recourse) decision $y$ corrects for it afterwards at a cost. When $\xi$ has finitely many realizations, the problem is a large but structured linear program, and the classical way to solve it is the L-shaped method of Van Slyke and Wets (1969), a Benders-type outer linearization of the expected recourse cost.

Birge and Louveaux (1988) proposed the multicut L-shaped algorithm: instead of one cut on the expected recourse function per iteration, it adds one cut per realization. They compared the two methods by worst-case counts of major iterations (the operations between two returns to the master problem), and showed that the multicut count grows linearly in the number $K$ of realizations, while their bound for the single-cut method grows like $K^{m_2}$ . The multicut idea is now part of every textbook treatment of decomposition for stochastic programming (Birge and Louveaux, Introduction to Stochastic Programming, Ch. 5) and of most production implementations of Benders decomposition.

Setting

The data are a matrix $A\in\mathbb R^{m_1\times n_1}$ , vectors $b$ , $c$ , a fixed recourse matrix $W\in\mathbb R^{m_2\times n_2}$ , and $K$ realizations $k=1,\dots,K$ , each with a cost $q_k\in\mathbb R^{n_2}$ , a right-hand side $h_k\in\mathbb R^{m_2}$ , a technology matrix $T_k\in\mathbb R^{m_2\times n_1}$ and a probability $p_k$ . Row vectors are written without transposes, as in the paper. The second-stage value of realization $k$ is

Q_k(x)=\min\{\,q_k y\mid Wy=h_k-T_kx,\ y\ge 0\,\}\in\mathbb R\cup\{\pm\infty\},

the expected recourse is $\Omega(x)=\sum_k p_kQ_k(x)$ , and the deterministic equivalent (2) minimizes $cx+\Omega(x)$ over $K_1\cap K_2$ , where $K_1=\{x\mid Ax=b,\ x\ge 0\}$ and $K_2$ is the set of $x$ for which every second-stage problem is feasible.

The multicut algorithm keeps feasibility cuts $(D_l,d_l)$ and, for each $k$ , optimality cuts $(E_{l(k)},e_{l(k)})$ . Step 1 solves the master

\min\ cx+\sum_{k}\theta_k\quad\text{s.t. } Ax=b,\ x\ge0,\ D_lx\ge d_l,\ E_{l(k)}x+\theta_k\ge e_{l(k)},

ignoring $\theta_k$ when scenario $k$ has no cut. Step 2 tests feasibility of each scenario at the master solution $x^\nu$ and, at the first infeasible one, adds a feasibility cut $(\sigma T_k,\sigma h_k)$ from the simplex multiplier $\sigma$ of a phase-one LP. Step 3 solves each second-stage problem at $x^\nu$ with simplex multiplier $\pi_k$ ; for every $k$ with $\theta_k<p_k\pi_k(h_k-T_kx^\nu)$ (condition (14)) it adds the optimality cut $(p_k\pi_kT_k,\ p_k\pi_kh_k)$ . If no $k$ satisfies (14) the algorithm stops.

The cut set $\mathcal C_k$ is the finite set of all optimality cuts that Step 3 can produce for scenario $k$ : the cuts of simplex-optimal bases of the scenario- $k$ problem at points of $K_1$ .

Formalization targets

Goal: the iteration bound (17)

The paper states (Theorem, p. 388):

Let b be the slope number of the second stage of (2). Then, the maximum number of iterations for the multicut algorithm is 1 + K(b^{m₂} − 1) (17) while the maximum number of iterations for the L-shaped algorithm is [1 + K(b − 1)]^{m₂} (18) where K is the number of the different realizations of ξ.

The goal is (17) with the number of facets replaced by the number of distinct cuts: if $|\mathcal C_k|\le M$ for every $k$ and $M\ge1$ , then in every run of the algorithm, for every choice of optimal master solutions and optimal bases,

\#\{\text{returns to Step 1 from Step 3}\}\ \le\ 1+K(M-1).

Milestones

The feasibility cuts determine $K_2$ (a point lies in $K_2$ exactly when it satisfies every feasibility cut, §2, p. 385), and each optimality cut is an affine minorant of $p_kQ_k$ touching it where it was generated (the multicut algorithm outer-linearizes each $Q_k$ , p. 387).
Aggregating one cut per scenario gives a valid L-shaped cut, and $z(\text{multi})\ge z(\text{L-shaped})$ (proof of the Proposition, p. 387).
When (14) holds for no $k$ , $x^\nu$ is optimal for (2) (stopping rule, p. 387).
The first return from Step 3 records one cut for each scenario, and every return records at least one cut not recorded before (proof of the Theorem, p. 388).

Significance

The bound explains why the multicut method needs few major iterations: the information sent to the master grows additively over scenarios, while the facets of $\Omega$ are combinations of facets of the $Q_k$ and their number can grow multiplicatively. The paper itself notes the trade-off this creates against master size ( $m_1+K$ rows instead of $m_1+1$ ), which is the basis of later work on partial aggregation of cuts.

The mission produces a formal model of the multicut algorithm as a transition system over all admissible choices, valid-cut lemmas for both cut types with dual feasibility made explicit, the correctness of the stopping rule, and the counting argument. These results are proved on paper but, to our knowledge, no machine-checked version of the multicut L-shaped algorithm or its iteration bound exists. The model is reusable for other results on Benders-type methods for stochastic programs.

Difficulty

The counting argument is short once the right invariants are in place; the difficulty is the invariants. A cut recorded earlier must still be satisfied by the current master solution, while the cut added for a scenario satisfying (14) is violated by it, so the new cut differs from every recorded one. This uses that every recorded cut comes from a basis whose multiplier is dual feasible: a basis that merely attains the optimal value under degeneracy can produce a cut that is not valid. The stopping rule needs strong duality at the final bases and weak duality at all earlier ones, together with extended-real bookkeeping of $Q_k$ on points where a scenario is infeasible.

Formalization scope

The model is the published StochasticProg_Recourse_Instance ( $Q_k$ in EReal, $+\infty$ when infeasible) with simplex bases and multipliers from StochasticProg_LShaped_Bases. Vectors are Fin n → ℝ, scenarios Fin K. A simplex-optimal basis is defined locally: invertible basic submatrix, nonnegative basic solution, and dual-feasible multiplier ( $\pi W\le q_k$ ; for the phase-one LP, $\sigma W\le 0$ and $|\sigma_i|\le 1$ ). The algorithm is an inductive step relation on states (feasibility cuts, per-scenario cut lists, return counter); a run is any finite sequence of steps from the empty state. Master optima are attained optimal solutions, not infima.

Pinned-down readings:

The paper writes the bound with $b^{m_2}$ , from its slope number $b$ , and asserts without derivation that each $Q_k$ has at most $b^{m_2}$ facets. We state the bound for any $M$ bounding the number of distinct cuts of each scenario, which is what the paper's proof counts. The L-shaped bound (18) is not stated.
"Iterations" are returns to Step 1 from Step 3. The final, stopping solve is not counted, consistent with Appendix A (four facets of $\Omega$ , five L-shaped solves; two multicut returns), and Step-2 (feasibility) returns are not counted, as in the paper's bound.
Positive probabilities $p_k>0$ are assumed where $K_2$ or optimality appears (the paper's realizations form the support of $\xi$ ).
A scenario with no optimality cut has $\theta_k$ omitted from the objective and always satisfies (14).

The transition relation allows every choice the paper allows; a relation that fixed, say, a particular basis or a particular master solution would prove a bound for fewer runs, and one that required the cut set to be smaller than the paper's would make the bound easy. Neither is done here.

Contributions welcome: proofs of the milestones, a sorry-free proof of the goal from them, and a worked check that the definitions admit the run of Appendix A.

Selected references

J. R. Birge and F. V. Louveaux, A multicut algorithm for two-stage stochastic linear programs, European Journal of Operational Research 34 (1988) 384–392. https://doi.org/10.1016/0377-2217(88)90159-2
R. M. Van Slyke and R. J.-B. Wets, L-shaped linear programs with applications to optimal control and stochastic programming, SIAM Journal on Applied Mathematics 17 (1969) 638–663. https://doi.org/10.1137/0117061
J. F. Benders, Partitioning procedures for solving mixed-variables programming problems, Numerische Mathematik 4 (1962) 238–252. https://doi.org/10.1007/BF01386316
J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

12 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

The Price of Anarchy of Finite Congestion Games I: The Pure Price of Anarchy of the Average Social Cost Is 5/2Research Paper

Motivation

When many independent users share a resource whose cost grows with use (links of a network, servers, machines), each user chooses for itself, and the outcome is a Nash equilibrium rather than a socially optimal allocation. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures the cost of this decentralisation: the worst ratio between the social cost of an equilibrium and the optimal social cost. It has become a standard yardstick in algorithmic game theory, network routing and the design of distributed protocols.

Christodoulou and Koutsoupias (STOC 2005) determined the price of anarchy of finite congestion games with linear latencies, the atomic, unweighted counterpart of selfish routing. This mission formalizes the central entry of their table: pure equilibria, general (asymmetric) strategy sets, and the average social cost.

Timeline:

1973. Rosenthal defines congestion games and shows that they always have pure Nash equilibria (IJGT 2).
1999. Koutsoupias and Papadimitriou define the price of anarchy, for load balancing on parallel links (STACS 1999).
2002. Roughgarden and Tardos prove that the price of anarchy of non-atomic selfish routing with linear latencies is $4/3$ (J. ACM 49).
2005. Christodoulou and Koutsoupias prove that for finite (atomic) congestion games with linear latencies the pure price of anarchy of the average social cost is exactly $5/2$ ; independently, Awerbuch, Azar and Epstein obtain $2.5$ for unweighted and $(3+\sqrt5)/2\approx2.618$ for weighted games (STOC 2005).
2009. Roughgarden shows that this type of bound extends to mixed, correlated and coarse correlated equilibria (STOC 2009).

Setting

A congestion game has a finite set $N$ of players, a finite set $E$ of facilities, for every player $i$ a set $\Sigma_i\subseteq 2^E$ of pure strategies (each a set of facilities), and for every facility $e$ a latency function $f_e$ giving the cost of $e$ to each of its users as a function of how many users it has. A pure strategy profile $A=(A_1,\dots,A_n)$ picks $A_i\in\Sigma_i$ for each player. The load $n_e(A)$ is the number of players $i$ with $e\in A_i$ , and player $i$ pays

c_i(A)=\sum_{e\in A_i}f_e\bigl(n_e(A)\bigr).

The profile $A$ is a pure Nash equilibrium if no player can lower its cost by switching alone: $c_i(A)\le c_i(A_{-i},S)$ for all $i$ and all $S\in\Sigma_i$ , where $(A_{-i},S)$ replaces $A_i$ by $S$ . The social cost is $\mathrm{SUM}(A)=\sum_{i\in N}c_i(A)$ , which is $|N|$ times the average cost of a player. Latencies are linear: $f_e(k)=a_ek+b_e$ with $a_e,b_e\ge0$ . The game is asymmetric in the sense that each player has its own strategy set (symmetric games, where all $\Sigma_i$ coincide, are a special case).

The pure price of anarchy of the average social cost is

PA=\sup_{A\text{ Nash}}\frac{\mathrm{SUM}(A)}{\mathrm{opt}},\qquad \mathrm{opt}=\min_{P}\mathrm{SUM}(P),

the minimum taken over pure strategy profiles. In Lean these objects are CongestionGame, load, cost, IsProfile, IsPureNash, sumCost and IsLinear in the namespace CongestionPoA.AsymSum.

Formalization targets

Goal: the pure price of anarchy is exactly 5/2

The goal theorem pure_poa_sum_eq_five_halves is the conjunction of Theorems 1 and 2 of the paper:

\text{for every linear game, Nash } A \text{ and profile } P:\quad \mathrm{SUM}(A)\le\tfrac52\,\mathrm{SUM}(P),

\text{for every } N\ge3 \text{ there are a linear game with } N \text{ players, Nash } A \text{ and profile } P:\quad \mathrm{SUM}(A)=\tfrac52\,\mathrm{SUM}(P).

The first part is the upper bound; the second shows that it is attained for every number of players from three on.

Milestones

Lemma 1: $\beta(\alpha+1)\le\frac13\alpha^2+\frac53\beta^2$ for nonnegative integers $\alpha,\beta$ .
Deviation inequality (proof of Theorem 1): at a Nash equilibrium $A$ , $c_i(A)\le c_i(A_{-i},P_i)\le\sum_{e\in P_i}f_e(n_e(A)+1)$ .
Summing over players (proof of Theorem 1): $\mathrm{SUM}(A)\le\sum_{e\in E}n_e(P)\,f_e(n_e(A)+1)$ .
Theorem 1: the upper bound $\mathrm{SUM}(A)\le\frac52\mathrm{SUM}(P)$ .
Theorem 2: the matching instances for every $N\ge3$ .

Significance

The value $5/2$ is the benchmark for atomic congestion with affine costs. It is the reference point for the later results of the paper (the symmetric case $(5N-2)/(2N+1)$ , the maximum social cost $\Theta(\sqrt N)$ , mixed equilibria $(3+\sqrt5)/2$ ) and for a large literature on coordination mechanisms, taxes and the price of stability, which compare their guarantees against it. The bound is also the standard example of what later became the smoothness framework, through which the same constant governs mixed and coarse correlated equilibria and hence no-regret learning outcomes.

Both theorems are proved in the paper; nothing here is open. The proofs for affine latencies, however, are only indicated: the paper displays the identity case $f_e(k)=k$ and states that the arguments extend. The mission states the affine case and asks for complete machine-checked proofs, including the lower-bound construction, which the paper describes and declares "not hard to verify". No machine-checked proof of these results is on the platform.

Difficulty

The Nash conditions give one inequality per player, each mixing the equilibrium loads $n_e(A)$ with the strategies $P_i$ of the comparison profile. Bounding the loads crudely, for instance by the number of players, gives a ratio that grows with $N$ ; the constant $5/2$ requires comparing the cross term $\sum_e n_e(P)\,n_e(A)$ with both social costs simultaneously and with the right weights. The integrality of the loads matters at that point: the natural pointwise inequality is false for real arguments, so a proof that treats loads as real numbers cannot reach $5/2$ .

For the lower bound, a Nash equilibrium must be verified against every unilateral deviation of every player, for all $N\ge3$ at once, in a construction with cyclic indices. The case $N=2$ is genuinely different (the paper states that its price of anarchy is $2$ ), so the argument has to use $N\ge3$ .

Formalization scope

Players and facilities are finite types; a profile is a map from players to finite sets of facilities, and feasibility ( $A_i\in\Sigma_i$ ) is a separate predicate. Latencies are real-valued functions of the natural-number load, and "linear" means affine with nonnegative coefficients. The upper bound is stated multiplicatively, for every Nash $A$ and every feasible $P$ , which is equivalent to $PA\le5/2$ and avoids dividing by $\mathrm{opt}$ . The lower bound quantifies over players Fin N, $N\ge3$ , and existentially over a finite facility type, a linear game, a Nash equilibrium and an optimal feasible profile of positive social cost. The positivity rules out the trivializing witness: in the all-zero latency game every profile is a Nash equilibrium and $0=\frac52\cdot0$ . The Nash condition is the paper's cost form; it agrees with the payoff-form AGT.IsPureNash of agt_games for payoffs $-c_i$ .

Trivializing formalizations are ruled out: the comparison profile $P$ must be feasible (otherwise $\mathrm{SUM}(P)$ could be $0$ by letting players use no facility), the upper bound covers all affine latencies rather than only $f_e(k)=k$ , and the lower-bound instance must have linear latencies with nonnegative coefficients.

A complete development needs finite double counting (regrouping $\sum_i\sum_{e\in P_i}$ by facilities), monotonicity of affine latencies, and a decidable or explicit check of the lower-bound game. The congestion-game layer is reused by the other missions of this series. Proofs of individual milestones, and alternative proofs of the upper bound, are welcome.

Selected references

G. Christodoulou and E. Koutsoupias, The Price of Anarchy of Finite Congestion Games, Proc. 37th ACM STOC, 2005. https://doi.org/10.1145/1060590.1060600
B. Awerbuch, Y. Azar and A. Epstein, The Price of Routing Unsplittable Flow, Proc. 37th ACM STOC, 2005. https://doi.org/10.1145/1060590.1060599
E. Koutsoupias and C. Papadimitriou, Worst-case Equilibria, STACS 1999, LNCS 1563. https://doi.org/10.1007/3-540-49116-3_38
R. W. Rosenthal, A Class of Games Possessing Pure-Strategy Nash Equilibria, International Journal of Game Theory 2, 1973. https://doi.org/10.1007/BF01737559
T. Roughgarden and É. Tardos, How Bad Is Selfish Routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
T. Roughgarden, Intrinsic Robustness of the Price of Anarchy, Proc. 41st ACM STOC, 2009. https://doi.org/10.1145/1536414.1536485

7 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

The Price of Anarchy of Finite Congestion Games IV: For Symmetric Games the Maximum Social Cost Price of Anarchy Is at Most 5/2Research Paper

Motivation

The price of anarchy measures how much a system of selfish agents loses compared with a centrally optimized one: it is the worst ratio, over all Nash equilibria, between the social cost of the equilibrium and the optimal social cost. Koutsoupias and Papadimitriou introduced it in 1999 (Worst-case equilibria, STACS 1999), and bounding it for routing and congestion games became a central topic of algorithmic game theory. Congestion games model routing in networks, load balancing on machines and any setting where agents choose sets of shared resources whose cost grows with their usage.

Christodoulou and Koutsoupias (The price of anarchy of finite congestion games, STOC 2005) determined the pure price of anarchy of finite (atomic, unweighted) congestion games with linear latencies for two social costs — the sum of the players' costs and the maximum cost of a player — and for asymmetric and symmetric games. Awerbuch, Azar and Epstein obtained the $5/2$ bound for the sum independently in the same proceedings (The price of routing unsplittable flow, STOC 2005). This mission is the fourth of a series that formalizes the paper: the symmetric games with the maximum social cost (Sect. 3.4). For asymmetric games the maximum social cost has price of anarchy $\Theta(\sqrt N)$ (mission III); symmetry brings it down to a constant.

Setting

A congestion game has a finite set of players $N=\{1,\dots,n\}$ , a finite set $E$ of facilities, for each player $i$ a collection $\Sigma_i$ of pure strategies (each a subset of $E$ ), and for each facility $e$ a latency function $f_e:\mathbb N\to\mathbb R$ . A pure strategy profile $A=(A_1,\dots,A_n)$ picks $A_i\in\Sigma_i$ for every player. The load $n_e(A)$ is the number of players whose strategy contains $e$ , and the cost of player $i$ is

c_i(A)=\sum_{e\in A_i} f_e\big(n_e(A)\big).

A profile $A$ is a pure Nash equilibrium if no player can lower its cost by changing only its own strategy: $c_i(A)\le c_i(A_{-i},S)$ for every $i$ and every $S\in\Sigma_i$ , where $(A_{-i},S)$ replaces $A_i$ by $S$ .

The maximum social cost is $\mathrm{MAX}(A)=\max_{i} c_i(A)$ and the sum social cost is $\mathrm{SUM}(A)=\sum_i c_i(A)$ . Latencies are linear when $f_e(k)=a_e k+b_e$ with $a_e,b_e\ge 0$ . The game is symmetric when all players share one strategy set, $\Sigma_i=\Sigma$ . The pure price of anarchy for the maximum social cost is

\mathrm{PA}=\sup_{A\ \text{Nash}}\frac{\mathrm{MAX}(A)}{\min_{P}\mathrm{MAX}(P)}.

Formalization targets

Goal: Theorems 7 and 8

For every symmetric linear congestion game with at least one player, every pure Nash equilibrium $A$ and every pure strategy profile $P$ ,

\mathrm{MAX}(A)\le\tfrac52\,\mathrm{MAX}(P),

and for every $N\ge3$ there is a symmetric linear congestion game with $N$ players, a pure Nash equilibrium $A$ and a profile $P$ that minimizes the maximum social cost, with $\mathrm{MAX}(P)>0$ and

\mathrm{MAX}(A)=\frac{5N+1}{2N+2}\,\mathrm{MAX}(P).

The second part shows that the constant $5/2$ of the first is tight as $N\to\infty$ .

Milestones

Theorem 7, proof (first display). In a symmetric linear game, a Nash equilibrium cost is bounded by the cost of every strategy $P_j$ evaluated at loads $n_e(A)+1$ : $c_i(A)\le\sum_{e\in P_j}f_e(n_e(A)+1)$ .
Theorem 7, proof (second display). Summed over $j$ : $N\cdot c_i(A)\le\sum_e n_e(P)f_e(n_e(A)+1)$ .
Lemma 1. $\beta(\alpha+1)\le\frac13\alpha^2+\frac53\beta^2$ for nonnegative integers $\alpha,\beta$ .
Theorem 7, proof (Lemma 1 step). $\sum_e n_e(P)f_e(n_e(A)+1)\le\frac13\mathrm{SUM}(A)+\frac53\mathrm{SUM}(P)$ .
Theorem 1. For linear congestion games, $\mathrm{SUM}(A)\le\frac52\mathrm{SUM}(P)$ at every pure Nash equilibrium $A$ .
Theorem 7 and Theorem 8 as separate statements.

Significance

The result says that in symmetric congestion games with linear costs no player at an equilibrium is ever more than $5/2$ times worse off than the worst-off player under the best allocation, regardless of the number of players. This contrasts with the asymmetric case, where the ratio grows like $\sqrt N$ (Theorems 5 and 6 of the paper), and it fills the symmetric–maximum entry of the paper's Table 1. Together with the sum bounds it completes the picture of pure equilibria under linear latencies that later work on smoothness and robust price of anarchy (Roughgarden, Intrinsic robustness of the price of anarchy, STOC 2009) generalized.

The results are proved in the paper, which only displays the identity-latency case and states that the arguments extend to affine latencies. No machine-checked version of any of the paper's bounds is known to exist; the mission produces a formal proof of the affine statement, a checked construction for the lower bound (the paper verifies its Nash condition only partly), and a congestion-game layer shared with the rest of the series.

Difficulty

The obvious attempt bounds the worst player's cost by its deviation to its own optimal strategy only, as in the proof for the sum; that gives one inequality per player and loses the factor $N$ needed to compare with $\mathrm{MAX}(P)$ . Without symmetry the factor cannot be recovered at all (Theorem 6 of the paper). For the lower bound, the difficulty is that the construction must be a Nash equilibrium against all strategies in the common set — including the other players' equilibrium strategies and the isolated strategy of the maximum-cost player — while the paper only writes out the deviation to the optimal strategies; its parameters are left as the solution of a linear equation, which must be chosen integral for every $N\ge3$ .

Formalization scope

Players form a finite type (Fin N in the lower bound) and facilities a finite type; profiles are maps from players to Finsets of facilities, with feasibility $A_i\in\Sigma_i$ as a separate predicate IsProfile. Latencies are real-valued functions on natural-number loads; "linear" means affine with nonnegative coefficients. MAX is the maximum over a nonempty player set. Upper bounds are stated for every Nash equilibrium and every feasible profile, never dividing by the optimum. The lower bound asserts that $P$ minimizes MAX over all profiles and that $\mathrm{MAX}(P)>0$ : without positivity the equality would be satisfied by a game with all costs $0$ , and without symmetry or the full common strategy set the instance would not be the paper's. The lower bound gives $\mathrm{PA}\ge\frac{5N+1}{2N+2}$ for the instance, which is what the paper's proof shows.

The development needs sums over facilities exchanged with sums over players ( $\sum_j\sum_{e\in P_j}g(e)=\sum_e n_e(P)g(e)$ ), monotonicity of affine latencies, and an explicit finite instance. The congestion-game definitions are shared with the other missions of the series and will be merged with them; Lemma 1 and Theorem 1 are also milestones of mission I. Proofs of any milestone, and alternative constructions for Theorem 8, are welcome.

Selected references

G. Christodoulou and E. Koutsoupias, The price of anarchy of finite congestion games, Proc. 37th ACM STOC, 2005. https://doi.org/10.1145/1060590.1060600
B. Awerbuch, Y. Azar and A. Epstein, The price of routing unsplittable flow, Proc. 37th ACM STOC, 2005. https://doi.org/10.1145/1060590.1060599
E. Koutsoupias and C. Papadimitriou, Worst-case equilibria, STACS 1999, LNCS 1563. https://doi.org/10.1007/3-540-49116-3_38
R. W. Rosenthal, A class of games possessing pure-strategy Nash equilibria, International Journal of Game Theory 2, 1973. https://doi.org/10.1007/BF01737559
T. Roughgarden, Intrinsic robustness of the price of anarchy, Proc. 41st ACM STOC, 2009. https://doi.org/10.1145/1536414.1536430

9 thms3 active usersReviewed

Analysis Operations Research Optimization·Captain: mikedeng1

The Łojasiewicz Inequality for Nonsmooth Subanalytic Functions with Applications to Subgradient Dynamical Systems I: The Łojasiewicz Inequality at Critical Points of Continuous Subanalytic FunctionsResearch Paper

Motivation

For a real-analytic function $f : U \to \mathbb{R}$ on an open set $U \subseteq \mathbb{R}^n$ and a critical point $a$ (so $\nabla f(a) = 0$ ), the Łojasiewicz gradient inequality says that there is an exponent $\theta \in [0,1)$ such that $|f - f(a)|^{\theta} / \|\nabla f\|$ stays bounded near $a$ . It is the standard tool for proving that bounded gradient trajectories $\dot x = -\nabla f(x)$ have finite length and converge to a single critical point, and, in its descendants (the Kurdyka–Łojasiewicz property), for proving convergence of the whole iterate sequence of nonconvex descent methods: proximal gradient, alternating minimization, PALM, ADMM. Those algorithmic results all assume a nonsmooth version of the inequality, for functions that may take the value $+\infty$ and are not differentiable.

Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007)) supplied that nonsmooth version. This mission formalizes their first main result, Theorem 3.1: the inequality at critical points of subanalytic functions that are continuous on a closed domain.

Timeline.

1963: Łojasiewicz proves the inequality for real-analytic functions (Une propriété topologique des sous-ensembles analytiques réels), and in 1984 derives convergence of bounded analytic gradient trajectories.
1998: Kurdyka (Ann. Inst. Fourier 48) extends it to $C^1$ functions definable in an o-minimal structure, with a desingularizing function in place of the power.
2006: Bolte, Daniilidis and Lewis prove a nonsmooth Sard theorem (J. Math. Anal. Appl. 321): a subanalytic function continuous on its closed domain is constant on each connected component of its critical set.
2007: The present paper proves the nonsmooth inequality for continuous subanalytic functions (Theorem 3.1) and for lower semicontinuous convex ones (Theorem 3.3).
2007: Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18) extend it to lower semicontinuous functions definable in o-minimal structures (the KL property).

Setting

Write $\mathbb{R}^n$ with its Euclidean norm. A function $f : \mathbb{R}^n \to \mathbb{R} \cup \{+\infty\}$ has domain $\operatorname{dom} f = \{x : f(x) < +\infty\}$ .

Subanalytic sets (Definition 2.1). A set $A \subseteq \mathbb{R}^n$ is semianalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ on which $A \cap V = \bigcup_{i=1}^{p}\bigcap_{j=1}^{q}\{x \in V : f_{ij}(x) = 0,\ g_{ij}(x) > 0\}$ with $f_{ij}, g_{ij}$ real-analytic on $V$ . It is subanalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ such that $A \cap V$ is the projection onto $\mathbb{R}^n$ of a bounded semianalytic subset of $\mathbb{R}^n \times \mathbb{R}^m$ , $m \ge 1$ . A function $f$ is subanalytic if its graph $\{(x,\lambda) \in \mathbb{R}^n \times \mathbb{R} : f(x) = \lambda\}$ is subanalytic. Semialgebraic functions, and functions locally built from analytic ones by finitely many algebraic operations, max/min and compositions, are subanalytic.

Subdifferentials (Definition 2.10). The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y \to x,\, y \ne x} \frac{f(y) - f(x) - \langle x^*, y - x\rangle}{\|y - x\|} \ge 0$ (empty off $\operatorname{dom} f$ ). The limiting subdifferential $\partial f(x)$ is the set of limits of $x^*_k \in \hat\partial f(x_k)$ along $x_k \to x$ with $f(x_k) \to f(x)$ .

Slope and critical points. The nonsmooth slope is $m_f(x) = \inf\{\|x^*\| : x^* \in \partial f(x)\}$ , equal to $+\infty$ when $\partial f(x) = \emptyset$ (equation (4)). The critical set is $\operatorname{crit} f = \{x : 0 \in \partial f(x)\}$ (Definition 2.11).

Formalization targets

Goal: Theorem 3.1

Let $f$ be subanalytic with closed domain and $f|_{\operatorname{dom} f}$ continuous, and let $a \in \operatorname{crit} f$ . Then there is $\theta \in [0,1)$ such that

\frac{|f - f(a)|^{\theta}}{m_f} \ \text{ is bounded around } a,

with the conventions $0^0 = 1$ and $\infty/\infty = 0/0 = 0$ . In division-free form: there are $C$ and a neighbourhood $U$ of $a$ with $|f(x) - f(a)|^{\theta} \le C\|x^*\|$ for all $x \in U$ and $x^* \in \partial f(x)$ . The exponent is existential; the goal fixes no value of $\theta$ or $C$ .

Milestones

Remark 2.12, for $f$ continuous on a closed domain: the graph of $\partial f$ is closed; $\operatorname{crit} f$ is closed; $m_f$ is lower semicontinuous; $\operatorname{crit} f = m_f^{-1}(0)$ .
Proposition 2.13(ii), its clause on the critical set: if $f$ is subanalytic and relatively bounded on its domain, then $\operatorname{crit} f$ is subanalytic.
Equation (6), recalled from the nonsmooth Sard theorem: $f$ is constant on the connected component of $\operatorname{crit} f$ containing $a$ .
The curve selection lemma, recalled from Bierstone–Milman: a boundary point of a subanalytic set is the origin of an analytic arc entering the set.

Significance

The result. Theorem 3.1 is the nonsmooth Łojasiewicz inequality at critical points. With the subgradient in place of the gradient, it yields finite length of bounded trajectories of subgradient systems $\dot x \in -\partial f(x)$ (Section 4 of the paper) and is the template for the Kurdyka–Łojasiewicz property that underlies convergence proofs for proximal and splitting methods on nonconvex, nonsmooth problems (e.g. Attouch–Bolte–Redont–Soubeyran 2010, Bolte–Sabach–Teboulle 2014). Those papers assume the KL property and cite this line of results to know it holds for semialgebraic and subanalytic objectives.

Formalizing it. The theorem is proved; this mission produces a machine-checked proof. To our knowledge no proof assistant has a formal definition of subanalytic sets or of the nonsmooth Łojasiewicz inequality. The definitions layer (semianalytic and subanalytic sets, the slope, the inequality) is reusable by any later formalization of KL-based convergence analyses, and the milestones on Remark 2.12 are general facts about limiting subdifferentials that apply well beyond subanalytic geometry.

Difficulty

The obvious argument restricts $f$ and $m_f$ to an analytic curve and compares their Puiseux expansions. That step needs three pieces of subanalytic geometry that no library has: curve selection, the structure of one-variable subanalytic functions (monotonicity and Puiseux expansions), and the fact that the sets built in the proof (sets of points with a subgradient satisfying an inequality, level-wise infima of $m_f$ ) are again subanalytic, which in the paper goes through global subanalyticity and the projection theorem. The second obstacle is that $f$ is not smooth: the classical proof differentiates $f$ along a curve, while here only Fréchet subgradients are available, and the chain rule along an analytic curve holds only almost everywhere. The constancy of $f$ on critical components, equation (6), is itself a nonsmooth Sard-type theorem whose published proof uses stratification. A solver who replaces subanalytic by semialgebraic, or assumes $f$ real-valued and $C^1$ , proves a different and much weaker statement.

Formalization scope

Space and values. The space is EuclideanSpace ℝ (Fin n). The function is f : E → EReal with f x ≠ ⊥ for every x. The domain is {x | f x ≠ ⊤}; it is assumed closed, and f is assumed ContinuousOn it.
Subdifferentials. $\hat\partial f$ and $\partial f$ are the published platform definitions NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff, which match Definition 2.10 for functions never equal to $-\infty$ .
Subanalyticity. It is defined on any finite-dimensional real normed space, so that the same definition covers $\mathbb{R}^n$ , $\mathbb{R}^n \times \mathbb{R}$ and $\mathbb{R}^n \times \mathbb{R}^m$ . Analyticity is AnalyticOnNhd ℝ. The boundedness of the semianalytic set in Definition 2.1(ii) is part of the definition: without it every projection of a semianalytic set would count.
Slope. The slope is valued in $[0,+\infty]$ , with $+\infty$ on points without subgradients.
The inequality. It is the predicate LojIneqAt f a θ: one constant $C$ and one neighbourhood of $a$ , quantified over all limiting subgradients. Under $0^0 = 1$ the value $\theta = 0$ never works at a critical point, as under the paper's conventions.
Not assumed. The goal does not assume lower semicontinuity, real values, global subanalyticity, compactness of the critical set, or $f(a) = 0$ . These are reductions inside the paper's proof. Any formalization that adds them, fixes $\theta$ , or replaces the class of $f$ by semialgebraic or $C^1$ functions trivializes the target.
Infrastructure. A complete proof needs: curve selection; the monotonicity lemma and Puiseux expansions for one-variable globally subanalytic functions; the projection theorem or an equivalent definability argument; the nonsmooth Sard theorem (6); and a chain rule for Fréchet subgradients along analytic curves. Each of these is welcome as a separate contribution, and the subanalytic-geometry results are reusable well beyond this mission.

Selected references

J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17 (2007) 1205–1223. https://doi.org/10.1137/050644641
J. Bolte, A. Daniilidis, A. Lewis, A Sard theorem for non-differentiable functions, J. Math. Anal. Appl. 321 (2006) 729–740.
E. Bierstone, P. Milman, Semianalytic and subanalytic sets, Publ. Math. IHÉS 67 (1988) 5–42. https://doi.org/10.1007/BF02699126
K. Kurdyka, On gradients of functions definable in o-minimal structures, Ann. Inst. Fourier 48 (1998) 769–783. https://doi.org/10.5802/aif.1638
J. Bolte, A. Daniilidis, A. Lewis, M. Shiota, Clarke subgradients of stratifiable functions, SIAM J. Optim. 18 (2007) 556–572. https://doi.org/10.1137/060670080
S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, in Les Équations aux Dérivées Partielles, CNRS, Paris, 1963, 87–89.
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Grundlehren 317, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

12 thms2 active usersReviewed

Completed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

A Characterization of Waiting Time Performance Realizable by Single-Server Queues: The Conservation-Law Polytope Is the Convex Hull of the Preemptive Priority VectorsResearch Paper

Motivation

A single server shared by several classes of jobs must decide, at every moment, which class to serve. Different scheduling rules give different mean response times to the classes, and a system designer often starts from the other end: a target vector of mean response times, one per class, and the question whether any rule can meet it. Coffman and Mitrani answered this question for the multiclass M/M/1 queue in A Characterization of Waiting Time Performance Realizable by Single-Server Queues (Operations Research 28 (1980), 810–821). Their answer is a polytope with an explicit description: the response-time vectors that can be realized are exactly the convex combinations of the vectors of the preemptive priority rules, and these are exactly the vectors satisfying one equation and $2^M-2$ inequalities.

The starting point is Kleinrock's conservation law (Kleinrock, Naval Res. Logist. Quart. 12 (1965)): a weighted sum of the response times does not depend on the rule. The characterization is the first instance of what was later called the achievable region method, developed for general multiclass systems by Federgruen and Groenevelt (Oper. Res. 36 (1988)), Shanthikumar and Yao (Oper. Res. 40 (1992)) and Bertsimas and Niño-Mora (Math. Oper. Res. 21 (1996)), and used to derive priority-index policies such as the $c\mu$ rule and Gittins indices.

Setting

There are $M\ge1$ job classes. Jobs of class $i$ arrive in a Poisson stream at rate $\lambda_i>0$ and have exponential service times with parameter $\mu_i>0$ . The traffic intensity of class $i$ is $\rho_i=\lambda_i/\mu_i$ , and the system is stable: $\rho=\rho_1+\cdots+\rho_M<1$ . A performance vector $W=(W_1,\dots,W_M)$ lists the mean response times of the classes. Write $a_i=\rho_i/\mu_i$ , $V=\sum_i\lambda_i/\mu_i^2$ , and for a set $g$ of classes

f(g)=\frac{\sum_{i\in g}a_i}{1-\sum_{i\in g}\rho_i},\qquad f(\emptyset)=0 .

The conservation law (1): $\sum_{i=1}^M\rho_iW_i=V/(1-\rho)$ , which equals $f(\{1,\dots,M\})$ .
The inequalities (4): $\sum_{i\in g}\rho_iW_i\ge f(g)$ for each proper nonempty set $g$ of classes.
$H^{**}$ is the set of $W$ satisfying (1) and (4).
A priority order lists the classes as $i_1,\dots,i_M$ , $i_1$ highest. The preemptive priority vector $P(i_1,\dots,i_M)$ is the vector with $\sum_{i\in S_k}\rho_iW_i=f(S_k)$ for the top sets $S_k=\{i_1,\dots,i_k\}$ , $k=1,\dots,M$ ; explicitly $P_{i_k}=(f(S_k)-f(S_{k-1}))/\rho_{i_k}$ . For $M=2$ , $P(1,2)_1=1/(\mu_1-\lambda_1)$ , the M/M/1 response time of class 1 alone.
$H$ , (3), is the set of convex combinations $\sum_{k=1}^M\alpha_kP_k$ of $M$ preemptive priority vectors.

In Lean the data are a structure Params M carrying $\lambda,\mu$ and the three standing assumptions; Params.f, Params.Hss ( $H^{**}$ ), Params.prioVec, topSet and Params.H are the objects above.

Formalization targets

Goal: Theorem 2, analytical form

H^{**}=H .

The paper's Theorem 2 says a vector is achievable by a scheduling strategy iff it lies in $H$ ; its proof is the chain $H\subseteq H^*\subseteq H^{**}\subseteq H$ , where $H^*$ is the achievable set. The goal is the part of the chain that involves no strategies.

Milestones

The priority vector is the unique solution of the equations (5) for its chain of top sets.
The first inequality of the proof of Lemma 2: $(1-\rho(g_1))(1-\rho(g_2))>(1-\rho(g_1\cup g_2))(1-\rho(g_1\cap g_2))$ for crossing $g_1,g_2$ .
The second inequality of that proof, in the coefficients $a_i$ .
Lemma 1 at the priority vectors: every $P(i_1,\dots,i_M)$ lies in $H^{**}$ .
Two sets on which a point of $H^{**}$ satisfies (4) with equality are nested.
Lemma 2: every vertex of $H^{**}$ is a preemptive priority vector.

A further item states the paper's final remark (§4): every linear cost $\sum_ic_iW_i$ is minimized over $H^{**}$ at some preemptive priority vector.

Significance

The theorem turns a question about all scheduling rules into a finite check: a target vector is realizable iff it satisfies (1) and the inequalities (4), and every realizable vector is realized by randomly mixing at most $M$ priority rules. Linear costs over the realizable vectors are minimized by a priority rule, the fact behind the optimality of priority-index rules in multiclass queues. The paper also gives a linear program for finding the mixture.

The result has been proved since 1980. No machine-checked proof of it is known. The Prove2Me library holds the abstract generalized conservation law theorem of Gittins, Glazebrook and Weber (AllocationIndices.achievable_region_theorem, included as a reference item), which assumes the inequalities (4) for every policy and whose polytope also imposes nonnegativity; it does not compute the right-hand sides for the M/M/1 queue, does not prove that the priority vectors satisfy (4), and uses equality on the lowest-priority sets rather than the highest. This mission supplies the concrete polytope, the closed form of the priority vectors and the strict supermodularity of $f$ .

Difficulty

That the priority vectors lie in $H^{**}$ is a family of inequalities between ratios $f(S_k)$ , one for each pair of a priority order and a set $g$ , and the order and $g$ need not interact in any simple way. The reverse inclusion is a statement about vertices: a vertex is determined by $M$ tight constraints, and one has to show that they form a chain. This needs strict inequalities with the right direction for every crossing pair of sets, which is where the positivity of every $\lambda_i,\mu_i$ is used. If some $\lambda_i=0$ , then $W_i$ appears in no constraint, $H^{**}$ is unbounded and the goal is false. Finally, $H$ uses only $M$ points, not all $M!$ , so the goal contains a Carathéodory-type bound for the hyperplane of (1).

Formalization scope

Classes are Fin M, numbered from $0$ . A priority order is π : Equiv.Perm (Fin M) with π r the class of rank r, rank $0$ highest. "Vertex" is an element of Set.extremePoints ℝ. The points of (3) are prioVec (σ k) for an arbitrary σ : Fin M → Equiv.Perm (Fin M), so repetitions are allowed. The priority vectors are given by their closed form, not as solutions of a system. The goal assumes $M\ge1$ ; for $M=0$ the set $H$ is empty.

The paper's notion "achievable by some scheduling strategy" is replaced by its analytical characterization $H^{**}$ : the strategy class of the paper (Assumptions 1–3, p. 812) is described only in prose and the steady-state means are assumed to exist, so the queueing half of the proof (Theorem 1, Lemma 1 for arbitrary strategies, the conservation law itself) is not stated. The goal is not to be stated on an abstract set satisfying hypotheses that encode Lemma 1 and (1); that form is already proved and drops the content of milestone 4. The conservation law is an equality, never the inequality (4) at the full set.

A complete development needs finite-set sums, the extreme points of a polyhedron and a Carathéodory argument in an affine hyperplane; the inequalities of milestones 2 and 3 and the vertex-chain argument are reusable for any strictly supermodular set function. Proofs of any milestone, and alternative proofs of the goal through polymatroid theory, are welcome.

Selected references

E. G. Coffman, Jr. and I. Mitrani, A Characterization of Waiting Time Performance Realizable by Single-Server Queues, Operations Research 28(3, Part II), 810–821, 1980. https://doi.org/10.1287/opre.28.3.810
L. Kleinrock, A Conservation Law for a Wide Class of Queueing Disciplines, Naval Research Logistics Quarterly 12, 181–192, 1965. https://doi.org/10.1002/nav.3800120206
A. Federgruen and H. Groenevelt, Characterization and Optimization of Achievable Performance in General Queueing Systems, Operations Research 36(5), 733–741, 1988. https://doi.org/10.1287/opre.36.5.733
J. G. Shanthikumar and D. D. Yao, Multiclass Queueing Systems: Polymatroidal Structure and Optimal Scheduling Control, Operations Research 40(3-supplement-2), S293–S299, 1992. https://doi.org/10.1287/opre.40.3.S293
D. Bertsimas and J. Niño-Mora, Conservation Laws, Extended Polymatroids and Multiarmed Bandit Problems; A Polyhedral Approach to Indexable Systems, Mathematics of Operations Research 21(2), 257–306, 1996. https://doi.org/10.1287/moor.21.2.257
J. Gittins, K. Glazebrook and R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033

9 thms4 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

A Multicut Algorithm for Two-Stage Stochastic Linear Programs 2: Multicut for Simple Recourse Stops Within J·m2 + 1 IterationsResearch Paper

Motivation

Two-stage stochastic linear programs model decisions taken before uncertainty is resolved (first stage) and corrected afterwards at a cost (second stage, the recourse). The standard solution method for problems with finitely many scenarios is the L-shaped method of Van Slyke and Wets (1969), an outer linearization in the style of Benders decomposition: a master program approximates the expected recourse function by cutting planes, one cut per iteration. Birge and Louveaux (1988) proposed the multicut variant, which approximates the recourse function of each realization separately and can add several cuts per iteration, and compared the two methods by worst-case counts of major iterations.

The paper's §5 treats the special case of simple recourse, where the second stage only penalizes shortage and surplus of each component of the first-stage output against a random target. Simple recourse arises in production planning, inventory and capacity models, and is the case in which the recourse function separates into one-dimensional pieces. There the paper derives an explicit LP (25) equivalent to the problem, a dedicated multicut algorithm for it, and the bound of $Jm_2+1$ iterations quoted below. This mission formalizes that section.

Setting

First-stage data are $c\in\mathbb R^{n_1}$ , $A\in\mathbb R^{m_1\times n_1}$ , $b\in\mathbb R^{m_1}$ , and the first-stage feasible set is $K_1=\{x\mid Ax=b,\ x\ge0\}$ . A deterministic technology matrix $T\in\mathbb R^{m_2\times n_1}$ , with rows $T_i$ , maps $x$ to the tender $\chi=Tx\in\mathbb R^{m_2}$ . Problem (3) of the paper is

\min\ z(x)=cx+\Psi(Tx)\quad\text{s.t. } x\in K_1 .

For each row $i=1,\dots,m_2$ the random vector $\xi_i=(q_i^+,q_i^-,h_i)$ takes $J$ values $\xi_{ij}=(q^+_{ij},q^-_{ij},h_{ij})$ with probabilities $p_{ij}$ . The simple recourse cost (20) of row $i$ is the optimal value of a one-row LP,

\psi_i(\chi_i,\xi_{ij})=\min\{q^+_{ij}y^+ + q^-_{ij}y^- \mid y^+-y^-=h_{ij}-\chi_i,\ y^+,y^-\ge0\},

and by separability (19) the expected recourse function is $\Psi(\chi)=\sum_i\Psi_i(\chi_i)$ with $\Psi_i(\chi_i)=\sum_j p_{ij}\psi_i(\chi_i,\xi_{ij})$ . Write $q_{ij}=q^+_{ij}+q^-_{ij}$ .

The multicut algorithm for simple recourse problems (p. 389) keeps a set $I$ of identified pairs $l=(i,j)$ , initially empty. Step 1 solves the master program (26),

\min\ cx+\sum_{i,j}p_{ij}q^-_{ij}(T_ix)+\sum_{l\in I}u_l\quad\text{s.t. } Ax=b,\ x\ge0,\ u_l\ge e_l-E_lx,\ u_l\ge0\ (l\in I),

with $E_l=p_{ij}q_{ij}T_i$ and $e_l=p_{ij}q_{ij}h_{ij}$ . Step 2 adds to $I$ every pair for which the constraint $0\ge p_{ij}q_{ij}(h_{ij}-T_ix^\nu)$ (27) is violated at the master's solution $x^\nu$ , and returns to Step 1; when no pair is added the algorithm stops.

Formalization targets

Goal: the $Jm_2+1$ bound, with correctness

The paper states (p. 389): "The initial problem (26) involves $m_1$ constraints and $n_1$ variables. For this problem, the worst-case situation is when at each iteration, only one constraint (27) is violated in Step 2. Then, the maximal number of iterations is $Jm_2+1$ ." The goal asserts, for every run of the algorithm (any optimal solution of (26) may be used at each Step 1):

\nu\text{-th solve of Step 1 takes place}\ \Longrightarrow\ \nu\le Jm_2+1,

and, when the algorithm stops at $x^\nu$ , $x^\nu\in K_1$ and $cx^\nu+\Psi(Tx^\nu)\le cx+\Psi(Tx)$ for all $x\in K_1$ .

Milestones

(22)–(23): for $q^++q^-\ge0$ the LP (20) attains its minimum $\max\{q^-(\chi-h),q^+(h-\chi)\}$ , so each $\theta_{ij}$ has only two cuts.
(24)–(25): the simple recourse problem is equivalent to the LP (25): same optimal $x$ , and the value of (25) at $x$ with the best slacks is $z(x)$ .
Relaxation and stopping: (26) is a relaxation of (25), and if no unidentified pair violates (27) at an optimum of (26), that optimum (extended by zero slacks) is optimal for (25).
Facets: each $\Psi_i$ is a maximum of $J+1$ affine functions, so $\Psi$ is a maximum of at most $(J+1)^{m_2}$ affine functions.

Significance

The bound is linear in $m_2$ and $J$ , while the L-shaped method may need as many iterations as $\Psi$ has facets, up to $(J+1)^{m_2}$ (milestone 4). This is the paper's clearest instance of the multicut method's worst-case advantage, and the equivalence (25) shows that simple recourse problems are LPs of size linear in $m_2J$ , a fact used throughout the later literature on simple and integrated recourse.

The results are proved in the paper, briefly. To our knowledge none has a machine-checked proof. Formalizing them produces a checked reduction of simple recourse to an explicit LP, a checked correctness proof of a constraint-generation algorithm with an explicit iteration bound, and the piece count of a sum of one-dimensional convex piecewise linear functions.

Difficulty

The counting argument is short once the algorithm is pinned down; the difficulty lies in the rest. Correctness at stopping requires relating three optimization problems (3), (25) and (26) whose objectives differ by a constant and by slack variables that are only present for identified pairs, and doing so for an arbitrary optimal solution of the master. The step from (20) to (22)–(23) requires solving an LP in closed form, as an infimum that must first be shown finite. The facet count requires showing that a sum of $J$ convex functions, each with one breakpoint, is a maximum of exactly $J+1$ affine functions, which is not a consequence of convexity alone.

Formalization scope

All vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, realizations are indexed by Fin J, and pairs $(i,j)$ by Fin m2 × Fin J. The second-stage value $\psi$ is the EReal infimum of the LP (20), not its closed form; expectations are finite sums weighted by $p_{ij}\ge0$ with $\sum_jp_{ij}=1$ .

Readings pinned down, each recorded in the item statements:

$q_{ij}\ge0$ . The paper never states it, but without it (20) is unbounded below and (25) is not equivalent to (3). It is a field of the model.
$x\ge0$ belongs to (3) and is omitted in the displays of (25) and (26); it is kept in both.
Step 2 ranges over unidentified pairs. The paper writes "for each $i$ and $j$ "; read literally, an identified pair whose $u_l$ already covers it could be re-added forever. The paper's remark that (27) "identifies any constraints in (25) that are not met" fixes the reading. The state of the algorithm is the set of identified pairs; the order of identification, and so the index $t$ , is immaterial.
Stopping rule. It is implicit in the paper: stop when (27) is violated for no pair.
Counting. The paper writes "the maximal number of iterations is $Jm_2+1$ "; we count solves of Step 1, the stopping solve included, which is what its argument counts.
Constant. The objective of (26) omits the constant $-\sum p_{ij}q^-_{ij}h_{ij}$ of (25), as printed.
Facets. " $\Psi_i$ contains $J+1$ facets" is read as "is a maximum of $J+1$ (not necessarily distinct) affine functions".

A formalization in which the master step could fire without a violated, unidentified pair, or in which the algorithm's optimal solutions were fixed in advance, would make the bound either false or empty; the definitions exclude both. The goal includes optimality at stopping so that it is not only a statement about a set growing inside a finite set.

Needed infrastructure: elementary LP feasibility and optimality, finite sums in EReal, and piecewise linear convex functions on $\mathbb R$ . Contributions of any of the milestones, in any order, are welcome; milestone 1 is the natural first step.

Selected references

J.R. Birge and F.V. Louveaux, A multicut algorithm for two-stage stochastic linear programs, European Journal of Operational Research 34 (1988) 384–392. https://doi.org/10.1016/0377-2217(88)90159-2
R.M. Van Slyke and R. Wets, L-shaped linear programs with applications to optimal control and stochastic programming, SIAM Journal on Applied Mathematics 17 (1969) 638–663. https://doi.org/10.1137/0117061
J.R. Birge and F.V. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

7 thms3 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Fundamentals of Queueing Theory IX: Kingman's Upper Bound on the G/G/1 Queue WaitTextbook

Motivation

The single-server queue with general independent interarrival and service times, the G/G/1 queue, is the basic model of a congested resource: a machine, a link, a checkout. For Markovian arrivals or services the mean wait has a closed form (the Pollaczek–Khintchine formula for M/G/1, the geometric law for G/M/1). For general distributions it has none, and the mean wait depends on the whole distributions of the interarrival and service times, not only on their moments. Capacity planning still needs numbers. Bounds that use only the first two moments are therefore the practical tool. They say how bad congestion can be for any queue with a given arrival rate, service rate and variabilities, and they become exact as the traffic intensity approaches one.

This mission formalizes Chapter 7, §7.1 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), together with the heavy-traffic Theorem 7.1 of §7.2.3.

Timeline. Lindley (Proc. Cambridge Philos. Soc., 1952) derived the recursion for successive waiting times and characterized the stationary law. Kingman (Proc. Cambridge Philos. Soc., 1961, 1962) proved the heavy-traffic exponential limit. In "Some inequalities for the queue GI/G/1" (Biometrika, 1962) he proved the two-moment upper bound. Marshall (1968) derived further moment relations and bounds (Operations Research, 1968). Marchal (Operations Research, 1978) gave the lower bound (7.14).

Setting

A G/G/1 queue is specified by two probability laws on $[0,\infty)$ : the law $A$ of an interarrival time $T$ and the law $B$ of a service time $S$ . Both have finite second moments, and

E[T] = \frac1\lambda,\quad E[S] = \frac1\mu,\quad \sigma_A^2 = \mathrm{Var}[T],\quad \sigma_B^2 = \mathrm{Var}[S],\quad \rho = \frac{\lambda}{\mu}.

The pairs $(S^{(n)}, T^{(n)})$ are independent and identically distributed, and $S^{(n)}$ is independent of $T^{(n)}$ . Customers are served first come, first served. The line delay $W_q^{(n)}$ of the $n$ th customer obeys Lindley's recursion

W_q^{(n+1)} = \max\bigl(0,\ W_q^{(n)} + U^{(n)}\bigr), \qquad U^{(n)} = S^{(n)} - T^{(n)}, \tag{7.1}

and $W_q^{(n)}$ is independent of $(S^{(n)}, T^{(n)})$ . The idle gap $X^{(n)} = -\min(0, W_q^{(n)} + U^{(n)})$ is the time between the $n$ th departure and the next start of service.

The queue is stationary when the law $\nu$ of $W_q^{(n)}$ does not depend on $n$ , that is, when one step of (7.1) maps $\nu$ to itself. The mean stationary line delay is $W_q = E[W_q^{(n)}] = \int w\,d\nu(w)$ . In the Lean development these objects are IsGG1Input A B lam mu, lindley, idleX, IsStationaryWaitLaw A B ν and meanWait ν, in the namespace QueueingFundamentals.Bounds.

Formalization targets

Goal: Kingman's upper bound (7.13)

For every stationary G/G/1 queue with $\rho < 1$ , $W_q$ is finite and

W_q \le \frac{\lambda(\sigma_A^2 + \sigma_B^2)}{2(1-\rho)}.

Milestones

the idle-gap identity $E[X] = -E[U] = 1/\lambda - 1/\mu$ (7.4), and the mean-wait formula (7.7)

W_q = \frac{E[X^2] - E[U^2]}{2E[U]};

the variance of the interdeparture time $D = S^{(n+1)} + X^{(n)}$ (7.12): $\mathrm{Var}[D] = 2\sigma_B^2 + \sigma_A^2 - 2W_q(1/\lambda - 1/\mu)$ ;
Marchal's lower bound (7.14), $W_q \ge (\lambda^2\sigma_B^2 + \rho(\rho-2))/(2\lambda(1-\rho))$ ;
the distributional lower bound $W_q \ge r_0$ , with $r_0$ the unique nonnegative root of $f(z) = z - \int_{-z}^\infty [1 - U(t)]\,dt$ and $U(t)$ the CDF of $S - T$ ((7.15), (7.16));
the two-sided estimate (7.17), $\max\bigl(0, r_0, \tfrac{\lambda^2\sigma_B^2 + \rho(\rho-2)}{2\lambda(1-\rho)}\bigr) \le W_q \le \tfrac{\lambda(\sigma_A^2+\sigma_B^2)}{2(1-\rho)}$ ;
Theorem 7.1 (heavy traffic): for a sequence of G/G/1 queues with $\rho_j \to 1$ , $\alpha_j = -E[S_j - T_j]$ and $\beta_j^2 = \mathrm{Var}[S_j - T_j]$ , under convergence of the input laws, $\mathrm{Var}[S - T] > 0$ and uniformly bounded $(2+\delta)$ -moments,

\frac{2\alpha_j}{\beta_j^2}\,W_{q,j} \xrightarrow{d} \mathrm{Exp}(1).

The goal is (7.13) rather than the stronger (7.17) because it depends only on the first two moments of the input.

Significance

Kingman's bound is the most widely used performance estimate for single-server queues. It needs no distributional form, only two means and two variances. It yields the "Kingman formula" approximation used across manufacturing and service operations, and it is asymptotically exact as $\rho \to 1$ (Theorem 7.1). The departure variance (7.12) drives the decomposition approximations for networks of §7.3. The heavy-traffic theorem is the entry point to diffusion approximations of queues.

All results here are proved in the literature (Theorem 7.1 is stated in the book without proof). This mission produces the first machine-checked versions. As far as a search of the platform shows, none of these statements, and no stationary Lindley recursion, has been formalized. The substrate it needs is reusable for any mission on G/G/1, G/G/c or random walks: stationary laws of a recursion on distributions, moment identities for $\max(0,\cdot)$ , and convergence in distribution.

Difficulty

The book's derivation squares (7.3) and takes expectations, using $E[(W_q^{(n+1)})^2] = E[(W_q^{(n)})^2]$ . That step is valid only if the stationary wait has a finite second moment. It is not assumed here and fails in general: with finite second moments of $S$ and $T$ the stationary wait has a finite mean, but its second moment is finite only if $E[S^3] < \infty$ . So the moment identity (7.7) cannot be obtained by cancelling second moments. A truncation or limiting argument is needed, and even the finiteness of $W_q$ has to be proved rather than assumed. The lower bound $W_q \ge r_0$ further needs a Jensen argument for the conditional mean of one Lindley step. Theorem 7.1 needs a uniform-integrability argument across a sequence of queues.

Formalization scope

Conventions committed to in Lean:

laws, not random variables: $A$ , $B$ and the stationary law $\nu$ are Measure ℝ; independence of $W_q^{(n)}, S^{(n)}, T^{(n)}$ (and $S^{(n+1)}$ for $D$ ) is the product measure;
the input laws are probability measures on $[0,\infty)$ with finite second moments (MemLp id 2), $E[T] = 1/\lambda$ , $E[S] = 1/\mu$ , $\lambda, \mu > 0$ , $\rho = \lambda/\mu < 1$ ;
stationarity is invariance of the whole law $\nu$ under one step of (7.1), not equality of means;
$W_q$ , the variances (Mathlib variance) and $f_1$ are Lebesgue integrals. Every theorem therefore asserts, as part of its conclusion, that $\nu$ has a finite mean, and none assumes a finite second moment of $\nu$ ;
$U(t)$ is Mathlib's cdf of the law of $S - T$ ;
convergence in distribution is convergence of $\int g$ for all bounded continuous $g$ , and $\mathrm{Exp}(1)$ is expMeasure 1.

Closed forms carried by the statements: (7.4), (7.7), (7.12), (7.13), (7.14) and (7.17) exactly as printed, and the scaling $2\alpha_j/\beta_j^2$ of Theorem 7.1.

Stating (7.13) with $W_q$ , $E[X^2]$ or the idle probability as free real numbers constrained by (7.7) would reduce it to algebra. Here $W_q$ is always the mean of a stationary law of the queue.

Not formalized: (7.5) and (7.8), which need the idle-period law $I$ and the arrival-point probability $q_0$ as separate objects, and the multiserver bounds of §7.1.3. Proofs of any milestone are welcome, as are reusable lemmas on stationary laws of Lindley's recursion (existence, uniqueness, and finiteness of the mean under $E[S^2] < \infty$ ).

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
D. V. Lindley, The theory of queues with a single server, Math. Proc. Cambridge Philos. Soc. 48 (1952)
J. F. C. Kingman, The single server queue in heavy traffic, Math. Proc. Cambridge Philos. Soc. 57 (1961)
J. F. C. Kingman, Some inequalities for the queue GI/G/1, Biometrika 49 (1962)
K. T. Marshall, Some inequalities in queuing, Operations Research 16 (1968)
W. G. Marchal, Some simpler bounds on the mean queuing time, Operations Research 26 (1978)

10 thms3 active usersReviewed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources III: Active, Semiactive, Pseudoactive and Quasiactive Schedules Are Minimal Points of the Feasible RegionTextbook

Motivation

Exact and heuristic methods for resource-constrained project scheduling do not search the whole continuum of start-time vectors. They enumerate a finite candidate set that is guaranteed to contain an optimal schedule. For machine scheduling and precedence-only project scheduling the classical candidate sets (semiactive and active schedules) are defined by shifting single activities earlier. With general time lags — minimum and maximum delays between the starts of activities — several activities can be rigidly tied together, and single-activity shifts no longer describe the right candidate sets.

Neumann, Nübel and Schwindt (Neumann et al. 2000) introduced shifts of sets of activities and four resulting classes of schedules: active, semiactive, pseudoactive and quasiactive. Section 2.4 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (Springer 2003), characterizes each class geometrically as the minimal points of a subset of the feasible region. The branch-and-bound procedures of §2.5 of the book enumerate exactly these objects: each enumeration node is a strict order $O$ together with the minimal point of its order polyhedron.

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ ; $0$ and $n+1$ are fictitious activities marking the project beginning and completion, and $1,\dots,n$ are the real activities. Activity $i$ has an integer duration $p_i$ , with $p_0=p_{n+1}=0$ and $p_i>0$ otherwise. Time lags are the arcs $\langle i,j\rangle\in E$ of the project network $N$ with integer weights $\delta_{ij}$ . A schedule is a vector $S=(S_0,\dots,S_{n+1})$ of real start times with $S_0=0$ and $S_i\ge0$ . It is time-feasible if $S_j-S_i\ge\delta_{ij}$ for all $\langle i,j\rangle\in E$ ; these schedules form the polyhedron $\mathcal S_T$ .

There are renewable resources $k\in\mathcal R$ with capacity $R_k$ ; activity $i$ uses $r_{ik}\le R_k$ units while it is in progress. With the active set $\mathcal A(S,t)=\{i\mid S_i\le t<S_i+p_i\}$ , a schedule is resource-feasible if $\sum_{i\in\mathcal A(S,t)}r_{ik}\le R_k$ for every $k$ and every $t\ge0$ . The feasible region is $\mathcal S=\mathcal S_T\cap\mathcal S_R$ . It is in general neither convex nor connected.

A schedule induces the strict order $O(S)=\{(i,j)\mid i\ne j,\ S_j\ge S_i+p_i\}$ . For a strict order $O$ , the order polyhedron is $\mathcal S_T(O)=\{S\in\mathcal S_T\mid S_j\ge S_i+p_i\ \forall (i,j)\in O\}$ . $O$ is feasible if $\emptyset\ne\mathcal S_T(O)\subseteq\mathcal S$ . $\mathcal S_T(O(S))$ is the schedule polyhedron of $S$ .

A left-shift from $S$ to $S'$ means $S'\le S$ componentwise and $S'\ne S$ . For feasible $S\ne S'$ , the shift is global; it is local if a continuous trajectory $x:[0,1]\to\mathcal S$ joins $S$ to $S'$ ; it is order-preserving if $O(S)\subseteq O(S')$ and order-monotone if $O(S)\subseteq O(S')$ or $O(S)\supseteq O(S')$ . A feasible schedule is active, semiactive, pseudoactive or quasiactive if no global, local, order-monotone or order-preserving left-shift, respectively, starts at it. A minimal point of $\mathcal M\subseteq\mathbb R^{n+2}$ is a point $S\in\mathcal M$ such that no $S'\in\mathcal M$ satisfies $S'\le S$ , $S'\ne S$ .

Formalization targets

Goal: Theorem 2.4.9

For a feasible schedule $S$ :

\begin{aligned} &\text{(a) } S \text{ active} &&\iff S \text{ is a minimal point of } \mathcal S,\\ &\text{(b) } S \text{ semiactive} &&\iff S \text{ is a minimal point of a component of } \mathcal S,\\ &\text{(c) } S \text{ pseudoactive} &&\iff S \text{ is the minimal point of } \mathcal S_T(O) \text{ for every feasible strict order } O\subseteq O(S),\\ &\text{(d) } S \text{ quasiactive} &&\iff S \text{ is the minimal point of } \mathcal S_T(O(S)). \end{aligned}

Part (a) is close to a restatement of the definitions. The content lies in (b), which passes from trajectories to connected components; in (c), which replaces a condition on shifts by a condition on finitely many polyhedra; and in (d), which reduces quasiactivity to a single polyhedron.

Milestones

Lemma 2.4.7: for a strict order $O$ with $\mathcal S_T(O)\ne\emptyset$ , $lb\,\mathcal S_T(O)$ is the unique minimal point of $\mathcal S_T(O)$ .
§2.4, p. 39: an order-monotone shift is local.
§2.4, p. 42: $\mathcal{AS}\subseteq\mathcal{SAS}\subseteq\mathcal{PAS}\subseteq\mathcal{QAS}$ .
§2.4, p. 44: the pseudoactive schedules are exactly the local minimal points of $\mathcal S$ in the Euclidean metric.
Remark 2.4.10 (a): if $\mathcal S\ne\emptyset$ , some minimal point of $\mathcal S$ is an optimal schedule.
Remark 2.4.10 (b): quasiactive schedules are integer-valued, and $\mathcal S\neq\emptyset$ iff an integer-valued optimal schedule exists.
Proposition 2.10.2: $S_{n+1}\le\bar d=\sum_{i\in V}\max(p_i,\max_{\langle i,j\rangle\in E}\delta_{ij})$ for every quasiactive $S$ .

Significance

The characterization makes each schedule class checkable and enumerable. By (d), deciding quasiactivity is a longest-path computation in the schedule network. Deciding activeness is NP-hard (Neumann et al. 2000); the same holds for semiactive and pseudoactive schedules, which is why exact algorithms enumerate the quasiactive schedules. Remark 2.4.10 and Proposition 2.10.2 then give the two facts every such algorithm relies on: an optimal schedule lies among the (integer-valued) quasiactive schedules, and all of them fit into the horizon $[0,\bar d]$ . Regular objective functions other than the project duration (§2.10) inherit the same candidate sets.

On the formal side, the mission produces a reusable model of $PS|temp|C_{\max}$ with real start times and general time lags: time-feasible and resource-feasible schedules, schedule-induced orders, order polyhedra and the four schedule classes. No part of this material is formalized on Prove2Me or, as far as is known, anywhere else. The results are all proved in the literature (Neumann et al. 2000; the book gives proofs or calls them obvious); the work here is to formalize them.

Difficulty

The obvious argument for (b) says "a trajectory stays in one component, so local shifts move within components". The converse needs that two schedules in the same connected component of $\mathcal S$ are joined by a path inside $\mathcal S$ . That is false for general sets and has to come from the structure of $\mathcal S$ as a finite union of order polyhedra (the basic structural theorem of Bartusch, Möhring and Radermacher), which is not part of this mission's statements and must be proved on the way.

For (c), the difficulty is that an order-monotone shift may shrink the order $O(S)$ . The proof has to produce, from a feasible sub-order $O\subseteq O(S)$ whose polyhedron has a smaller minimal point, a shift that is short enough to keep every overlap of $S$ . This requires the resource feasibility of whole order polyhedra, i.e. that $\mathcal S_T(O(S))\subseteq\mathcal S$ for feasible $S$ . Resource feasibility is a condition on all times $t\ge0$ , while the orders only record pairwise relations between activities.

Formalization scope

Activities are Fin (n + 2), with 0 and Fin.last (n + 1) the fictitious ones. Durations are natural numbers, arc weights integers, and start times real. Resource requirements and capacities are natural numbers. The resource constraints hold for every $t\ge0$ ; (2.1.4) writes $0\le t\le\bar d$ , but the book's proofs use the unrestricted form. Minimal points are Mathlib's Minimal for the componentwise order on Fin (n + 2) → ℝ. Components in (b) are connected components (connectedComponentIn), while local shifts are defined by continuous trajectories from the unit interval, as in Definition 2.4.3. The theorem is stated for feasible $S$ , since the schedule classes consist of feasible schedules by definition. The lower bound $lb$ is a vector of real infima and is used only for nonempty order polyhedra.

Defining "active" as "minimal point of $\mathcal S$ ", or any class through its right-hand side, would make the goal trivial. That is ruled out: every class is defined through the shifts of Definitions 2.4.1–2.4.6, including the trajectory condition and the orders $O(S)$ .

Remark 2.4.8 (the minimal point of $\mathcal S_T(O)$ is the vector of longest path lengths in $N(O)$ ) is not stated, since it needs path lengths and the reachability conventions of Remarks 1.1.2. Contributions of that network layer, and of the structural theorem $\mathcal S=\bigcup_O\mathcal S_T(O)$ (Theorem 2.3.7), are welcome as supporting lemmas.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. https://doi.org/10.1007/978-3-540-24800-2
K. Neumann, H. Nübel, C. Schwindt, Active and stable project scheduling, Mathematical Methods of Operations Research 52 (2000), 441–465. https://doi.org/10.1007/s001860000092
M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988), 201–240. https://doi.org/10.1007/BF02283745
A. Sprecher, R. Kolisch, A. Drexl, Semi-active, active, and non-delay schedules for the resource-constrained project scheduling problem, European Journal of Operational Research 80 (1995), 94–102. https://doi.org/10.1016/0377-2217(93)E0294-8

10 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research·Captain: mikedeng1

Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems II: High-Probability and Expected Regret of Exp3.PTextbook

Motivation

In the adversarial (non-stochastic) multi-armed bandit problem a forecaster repeatedly chooses one of $K$ actions while an opponent sets the rewards, and only the reward of the chosen action is revealed. The model was proposed as a way of playing an unknown repeated game: Baños (1968) studied the repeated game in which the player observes only its own payoff, which is exactly the bandit problem against an opponent who reacts to the player's past moves. It is the basic model of online decision making under partial feedback without statistical assumptions, and it underlies regret minimization in games, adversarial routing and online advertising. Chapter 3 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2) collects its fundamental results: the Exp3 forecaster of Auer, Cesa-Bianchi, Freund and Schapire (SIAM J. Comput. 2002), its high-probability variant Exp3.P, and the $\sqrt{nK}$ minimax lower bound.

Setting

There are $K \ge 2$ arms and rounds $t = 1, 2, \dots, n$ . At each round an adversary assigns a gain $g_{i,t} \in [0,1]$ to every arm $i$ ; the forecaster picks an arm $I_t$ , possibly at random, and observes only $g_{I_t,t}$ . The adversary may be non-oblivious (adaptive): $g_{i,t} = g_{i,t}(I_1,\dots,I_{t-1})$ may depend on the forecaster's past actions. A forecaster rule maps the past actions to a probability vector $p_t$ on the arms, and a run is a sequence of random arms with $I_t \sim p_t$ given the past. The regret is the random variable

R_n = \max_{i=1,\dots,K}\sum_{t=1}^n g_{i,t} - \sum_{t=1}^n g_{I_t,t},

and, in the loss version $\ell_{i,t} \in [0,1]$ , the pseudo-regret is $\overline R_n = \mathbb E\sum_t \ell_{I_t,t} - \min_i \mathbb E\sum_t \ell_{i,t}$ . Since the maximum sits inside the expectation, $\overline R_n \le \mathbb E R_n$ in the gain version, and against an adaptive adversary the two can differ.

Exp3 draws $I_t$ from exponential weights $p_{i,t+1} \propto \exp(-\eta_t \tilde L_{i,t})$ of importance-weighted cumulative loss estimates $\tilde L_{i,t} = \sum_{s \le t} \ell_{i,s}\mathbb 1_{I_s = i}/p_{i,s}$ . Exp3.P uses biased gain estimates $\tilde g_{i,t} = (g_{i,t}\mathbb 1_{I_t=i} + \beta)/p_{i,t}$ and mixes in the uniform distribution:

p_{i,t+1} = (1-\gamma)\frac{\exp(\eta\tilde G_{i,t})}{\sum_k \exp(\eta \tilde G_{k,t})} + \frac{\gamma}{K}, \qquad \tilde G_{i,t} = \sum_{s=1}^t \tilde g_{i,s}.

Formalization targets

Goal: Theorem 3.3 (expected regret of Exp3.P)

With $\beta = \sqrt{\ln K/(nK)}$ , $\eta = 0.95\sqrt{\ln K/(nK)}$ , $\gamma = 1.05\sqrt{K\ln K/n}$ , against every adaptive adversary,

\mathbb E R_n \le 5.15\sqrt{nK\ln K} + \sqrt{\frac{nK}{\ln K}}.

Milestones

Lemma 3.1: for $\beta \in (0,1]$ and a fixed arm $i$ , with probability at least $1-\delta$ , $\sum_t g_{i,t} \le \sum_t \tilde g_{i,t} + \ln(\delta^{-1})/\beta$ .
Eq. (3.12): if $\gamma \le 1/2$ and $(1+\beta)K\eta \le \gamma$ , then with probability at least $1-\delta$ ,

R_n \le \beta nK + \gamma n + (1+\beta)\eta Kn + \frac{\ln(K\delta^{-1})}{\beta} + \frac{\ln K}{\eta}.

Theorem 3.2: with $\beta = \sqrt{\ln(K\delta^{-1})/(nK)}$ , $R_n \le 5.15\sqrt{nK\ln(K\delta^{-1})}$ (3.10); with $\beta = \sqrt{\ln K/(nK)}$ , $R_n \le \sqrt{nK/\ln K}\,\ln(\delta^{-1}) + 5.15\sqrt{nK\ln K}$ (3.11), each with probability at least $1-\delta$ .
Theorem 3.1: Exp3 with $\eta = \sqrt{2\ln K/(nK)}$ has $\overline R_n \le \sqrt{2nK\ln K}$ (3.2); with $\eta_t = \sqrt{\ln K/(tK)}$ , $\overline R_n \le 2\sqrt{nK\ln K}$ (3.3).
Lemma 3.2 and Theorem 3.4: for $n \ge K \ge 2$ and every forecaster there is a Bernoulli instance with $\max_i \mathbb E\sum_t Y_{i,t} - \mathbb E\sum_t Y_{I_t,t} \ge \sqrt{nK}/20$ .

Significance

The goal bounds the expected regret, not the pseudo-regret, against an opponent that adapts to the forecaster's randomized past choices. A pseudo-regret bound says nothing about $\mathbb E R_n$ in that setting, and the book obtains the expected-regret bound by first proving a high-probability bound valid at every confidence level, (3.11), and integrating its tail. Together with Theorem 3.4 the chapter shows that $\sqrt{nK}$ is the minimax rate of adversarial bandits up to a $\sqrt{\ln K}$ factor. Lemma 3.1, the concentration of biased importance-weighted estimates, holds for any forecaster rule and is the step that turns exponential weights into a high-probability guarantee.

All results are proved in the book. On the formal side, the platform has the pseudo-regret bound of Exp3 against an oblivious adversary (a fixed reward table, Bandit Algorithms V) and an Exp3-IX high-probability bound; it has no Exp3.P, no regret bound against adaptive adversaries and no Bernoulli $\sqrt{nK}/20$ lower bound. This mission adds an explicit model of adaptive adversaries and randomized forecaster runs, and the chapter's statements with the book's exact constants.

Difficulty

Against an adaptive adversary the gains are random and depend on the forecaster's own past draws, so the argument used for a fixed reward table (take expectations of an inequality that holds for every fixed sequence) does not control $\mathbb E R_n$ : the maximum over arms does not commute with the expectation. Unbiased estimates do not help either, because the variance of $\ell_{i,t}/p_{i,t}$ is of order $1/p_{i,t}$ , which can be arbitrarily large; even with uniform mixing at rate $n^{-1/2}$ the cumulative variance is of order $n^{3/2}$ . The bias $\beta$ and the mixing $\gamma$ have to be tuned jointly so that the estimate concentrates while the exponential-weights analysis survives, and the constants $0.95$ , $1.05$ and $5.15$ come out of that tuning. The lower bound needs an information-theoretic comparison of a forecaster's behaviour on $K+1$ Bernoulli instances, against forecasters that may be randomized.

Formalization scope

Arms are Fin K with $K \ge 2$ ; rounds are numbered $1,\dots,n$ ; logarithms are natural. Action sequences are functions $\mathbb N \to$ Fin K whose entry $0$ is ignored. An adversary is a structure holding values in $[0,1]$ that may depend on the past actions only (gains for Exp3.P, losses for Exp3); a randomized adversary with independent external randomness reduces to this case by conditioning. A run of a forecaster rule $p$ on a probability space is pinned down by the cylinder identity $\mathbb P(I_1 = h_1,\dots,I_t = h_t) = \mathbb P(I_1=h_1,\dots,I_{t-1}=h_{t-1})\,p_t(h)(h_t)$ , which determines the law of $(I_1,\dots,I_n)$ . "With probability at least $1-\delta$ " is $\mathbb P(\text{event}) \ge 1-\delta$ for $\delta \in (0,1)$ , and $\mathbb E R_n$ is the Bochner integral of the bounded, measurable regret. The lower bounds use a stochastic model in which the forecaster sees past actions and the rewards of the played arms, and rewards are i.i.d. product Bernoulli.

Constants and conventions:

Every constant is the book's exact one: $0.95$ , $1.05$ , $5.15$ , $1/20$ . No $O(\cdot)$ is involved.
Exp3.P with $1.05\sqrt{K\ln K/n} > 1$ is outside the box's range $\gamma \in [0,1]$ ; its vector can then have negative entries, and if it does on a history of positive probability no run exists. This happens only when $n < 1.11\,K\ln K$ , where the printed bounds already follow from $R_n \le n$ , so the statements are true there whether or not a run exists.
Corrected misprints: the Exp3 box's $\tilde\ell_{i,s}$ is $\tilde\ell_{i,t}$ ; the sign in (3.16) is the box's $\exp(+\eta\tilde G)$ ; the proof of (3.10) says the bound is trivial "if $n \ge 5.15\sqrt{\cdots}$ ", which should be $n \le$ . The statements carry no lower bound on $n$ .
Added standing hypotheses: $K \ge 2$ everywhere, $n \ge K$ in Theorem 3.4 (from the protocol box, p. 6; Theorem 3.4 is false without it), $\beta > 0$ and $p_{i,t} > 0$ in Lemma 3.1.
Theorem 3.4 is stated as "for every forecaster there is a Bernoulli instance with regret at least $\sqrt{nK}/20$ ", which implies the book's $\inf\sup$ (3.18).

A trivializing formalization is ruled out: the forecasters are fixed rules of the observed history drawn with fresh randomness, the adversary is not restricted to a fixed sequence, and the lower bounds quantify over all forecasters and exhibit the instance.

Welcome contributions: a reusable construction of runs (existence of a probability space carrying a run for every rule), the supermartingale form of Lemma 3.1, the exponential-weights potential argument, a tail-integration lemma $\mathbb E W \le \int_0^1 \delta^{-1}\mathbb P(W > \ln\delta^{-1})\,d\delta$ , and a KL/Pinsker comparison for bandit runs.

Selected references

S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2, doi:10.1561/2200000024
P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 2002. doi:10.1137/S0097539701398375
J.-Y. Audibert, S. Bubeck, Regret bounds and minimax policies under partial monitoring, Journal of Machine Learning Research 11, 2010. jmlr.org/papers/v11/audibert10a
N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. doi:10.1017/CBO9780511546921

13 thms1 active userReviewed

Completed

Algorithmic Game Theory Complexity Theory Operations Research·Captain: mikedeng1

The Complexity of Computing a Nash Equilibrium 1: Approximate Fixed Points of Nash's Map Are Approximate Nash EquilibriaResearch Paper

Motivation

A finite game describes several decision makers whose payoffs depend on everyone's choices. A Nash equilibrium is a collection of choices at which no single player can improve their expected payoff by changing strategy alone. Equilibrium existence is a classical result, but a computational argument needs to connect an object that can be approximated numerically to a strategically meaningful outcome. Daskalakis, Goldberg and Papadimitriou make that connection using Nash's map on mixed-strategy profiles in their study of equilibrium computation (Daskalakis, Goldberg and Papadimitriou 2009, §3.2). This mission isolates their quantitative connection: a profile close to a fixed point of that particular map is close to a Nash equilibrium, with the paper's explicit error bound.

The result is a known lemma from the published paper, not an open conjecture. It belongs to the paper's route from finite games to approximate equilibrium computation. The present mission treats the analytic statements about the map and finite payoffs; it does not state the paper's PPAD completeness theorem or encode computational reductions.

Setting

A normal-form game has $r\ge2$ players. In the Nash-map section each player has the same nonempty set $[n]$ of $n$ pure strategies. A pure profile $s$ chooses one strategy for each player, and player $p$ receives a nonnegative real payoff $u^p_s$ . The largest entry among all these payoff tables is $U_{\max}$ . A mixed profile $x$ assigns each player $p$ probabilities $x^p_j\ge0$ that sum to one over $j\in[n]$ ; different players randomize independently. The expected payoff when everyone uses $x$ is $U^p(x)$ . If player $p$ instead uses the pure strategy $j$ while the others keep their mixed strategies, the expected payoff is $U^p_j(x)$ .

Write $B^p_j(x)=\max\{0,U^p_j(x)-U^p(x)\}$ for the positive part of this unilateral payoff gain. Nash's map $f$ assigns to each coordinate of a mixed profile the normalized value

f(x)^p_j=\frac{x^p_j+B^p_j(x)}{1+\sum_{k\in[n]}B^p_k(x)}.

The numerator raises the weight of a strategy whose pure payoff exceeds the current expected payoff. The common denominator ensures that the new weights for a player sum to one. These are exactly the quantities and normalization displayed on page 205 of the paper (Daskalakis, Goldberg and Papadimitriou 2009).

An $\varepsilon$ -approximate Nash equilibrium here means a mixed profile at which no player can increase expected payoff by more than $\varepsilon$ through any mixed-strategy deviation. This is the alternative approximation notion identified on page 199 and written as Eq. (27) on page 243. It is weaker than the paper's $\varepsilon$ -approximately well-supported condition; the two notions must remain distinct.

Formalization targets

The goal is Lemma 3.8 (p. 207). For any mixed profile $x$ with $\|f(x)-x\|_\infty\le\varepsilon'$ , where $\varepsilon'\ge0$ , its approximate-equilibrium error is bounded by the paper's exact quantity:

\varepsilon_{\mathrm{Nash}}= n\sqrt{\varepsilon'(1+nU_{\max})} \left(1+\sqrt{\varepsilon'(1+nU_{\max})}\right) \max\{U_{\max},1\}.

No numerical constant is left free or replaced by an unspecified asymptotic bound. The goal is universal over games and profiles satisfying the stated conditions; it does not merely assert the existence of one favorable profile.

The milestone list also includes Lemma 3.5, bounding the variation of a pure-strategy payoff when opponents change their distributions; Lemma 3.6, an inequality for normalized nonnegative sums; and Lemma 3.4, the explicit Lipschitz bound

\|f(x)-f(x')\|_\infty\le[1+2U_{\max}rn(n+1)]\,\delta \quad\text{when}\quad \|x-x'\|_\infty\le\delta.

Equation (3) on page 208 is a further milestone: it bounds each coordinate's share of the total positive gain under approximate fixedness. Lemma 3.4 has a separate role in the paper's grid analysis; it is not claimed as a prerequisite of Lemma 3.8.

Significance

The goal gives a quantitative translation between two kinds of approximation. An error measured in the coordinates of a fixed-point map becomes an upper bound on a player's incentive to deviate. The dependence on $n$ , $U_{\max}$ and $\varepsilon'$ matters because the later computational construction chooses its grid scale using an explicit threshold, not simply a convergence claim. Lemma 3.4 provides the separate sensitivity estimate for that map, also with its exact constant (Daskalakis, Goldberg and Papadimitriou 2009, pp. 205–207).

Formalizing these known statements supplies a reusable bridge between finite-game payoffs, mixed profiles and a concrete fixed-point map. The shared finite-game representation already exists in the published agt_games definition bundle. What remains here is a machine-checked proof of each quantitative statement and of the payoff identities needed to relate pure and mixed deviations. The local Lean statements compile as open theorem targets; the mission does not claim that their proofs are already formalized.

Difficulty

A coordinatewise small value of $f(x)-x$ does not by itself bound the largest payoff advantage by the same number. The map normalizes by a sum of all positive advantages, and a strategy with a large advantage might have little probability under $x$ . Conversely, controlling a player's current expected payoff requires information about the entire probability vector, including strategies that are worse than the current mix. The explicit square-root dependence in Lemma 3.8 captures this mismatch. A direct substitution of the fixed-point error for the equilibrium error would lose both the dimension and payoff-scale factors in the published bound.

Formalization scope

Lean represents players by Fin r, strategies by Fin n, payoffs by a real function on pure profiles, and mixed strategies by real-valued weight functions satisfying AGT.IsMixedProfile. The paper numbers players and strategies from one; Fin uses zero-based indices without changing the mathematical sets. AGT.expectedPayoff and AGT.profileProb implement the independent product distribution. Pure-strategy expected payoff is the same expectation after replacing just one player's lottery by a point mass. The maximum payoff is computed from the game's actual finite table; the statements require $r\ge2$ and $n>0$ , so this maximum exists. Nonnegative payoff entries, the standing convention from §2.1, are hypotheses.

The formula for $f$ is defined on all real coordinate arrays, exactly as an algebraic expression. Every theorem about an equilibrium supplies mixed-profile membership. This explicit condition rules out interpreting Lemma 3.8 on arbitrary vectors, for which “approximate Nash equilibrium” has no strategic meaning and the paper's argument does not apply. The infinity norm is written as a bound for every player-strategy pair, avoiding any dependence on a chosen norm instance. All error parameters appearing in the statements are nonnegative, and the denominator of $f$ is positive on mixed profiles because each $B^p_j(x)$ is nonnegative.

The development needs finite products and sums, real inequalities, the game bundle, and elementary facts about lotteries and unilateral deviations. Results about how expectations vary under a changed product distribution are reusable for other finite-game formalizations. Contributions proving the milestone inequalities, the payoff identities, and the goal's exact bound are welcome.

Selected references

C. Daskalakis, P. W. Goldberg and C. H. Papadimitriou, The Complexity of Computing a Nash Equilibrium, SIAM Journal on Computing 39(1):195–259, 2009. DOI: 10.1137/070699652.

7 thms4 active usersReviewed

Discrete Geometry Linear Optimization Operations Research+1·Captain: mikedeng1

Sensitivity Theorems in Integer Linear Programming: Every Integral m×n Matrix Has Chvátal Rank at Most 2^(n³+1)·n^(5n)·Δ(A)^(n+1)Research Paper

Motivation

An integer linear program $\max\{wx : Ax \le b,\ x \text{ integral}\}$ is usually attacked through its linear programming relaxation $\max\{wx : Ax \le b\}$ , which drops the integrality constraint. Two questions follow at once. How far can an optimal solution of the relaxation be from an optimal integer solution? And how many rounds of rounding-based cutting planes are needed before the relaxation describes the integer points exactly? Branch-and-bound, cutting-plane methods and the parametric analysis of integer programs all depend on the answers.

W. Cook, A.M.H. Gerards, A. Schrijver and É. Tardos, Sensitivity theorems in integer linear programming (Math. Programming 34 (1986) 251–264), answer both in terms of the number of variables $n$ and the largest subdeterminant $\Delta(A)$ of the constraint matrix, independently of the right-hand side.

Timeline.

1958–1963: Gomory introduces integer rounding cuts. In 1973 Chvátal (Discrete Math. 4) shows that finitely many rounds reach the integer hull of a bounded polyhedron.
1977–1979: Blair and Jeroslow prove that for a fixed matrix $A$ the distance between LP and IP optima, and the gap between their values, are bounded by constants depending on $A$ .
1980: Schrijver (Ann. Discrete Math. 9) proves that the Chvátal closure of a rational polyhedron is a polyhedron, and that every rational polyhedron, bounded or not, reaches its integer hull after finitely many rounds.
1986: Cook, Gerards, Schrijver and Tardos prove the explicit bounds of this mission, $n\Delta(A)$ for proximity, and show that every integral matrix has finite Chvátal rank.
Later work, for example Eisenbrand and Weismantel (2018), replaces the $\ell_\infty$ proximity bound by $\ell_1$ bounds for programs in standard form.

Setting

All matrices, vectors and polyhedra are rational. Let $A$ be an integral $m\times n$ matrix. A square submatrix of order $k$ , where $1\le k\le\min(m,n)$ , keeps $k$ rows and $k$ columns of $A$ . The quantity $\Delta(A)$ is the largest $|\det B|$ over all such submatrices $B$ . So $\Delta(0)=0$ , and $\Delta(A)\ge 1$ whenever $A\ne 0$ . Norms are $\|x\|_\infty=\max_i|x_i|$ and $\|x\|_1=\sum_i|x_i|$ .

For $b\in\mathbb{Q}^m$ write $P=\{x\in\mathbb{Q}^n : Ax\le b\}$ . An optimal solution of $\max\{wx : Ax\le b\}$ is a point of $P$ maximizing $wx$ . For $\max\{wx : Ax\le b,\ x\text{ integral}\}$ it is an integral point of $P$ maximizing $wx$ among the integral points of $P$ . A rational polyhedron is a set $\{x : Dx\le d\}$ with $D$ , $d$ rational. The integer hull $P_I$ is the convex hull of the integral points of $P$ .

If $ay\le\beta$ for all $y\in P$ , with $a$ integral and $\beta$ rational, then every integral point of $P$ satisfies the Chvátal cut $ax\le\lfloor\beta\rfloor$ . The Chvátal closure $P'$ is the set of points satisfying all Chvátal cuts. Set $P^{(0)}=P$ and $P^{(i)}=(P^{(i-1)})'$ . Then $P_I\subseteq P^{(i)}$ for all $i$ . The Chvátal rank of $P$ is the least $t$ with $P^{(t)}=P_I$ . The Chvátal rank of the matrix $A$ is the supremum of the Chvátal ranks of $\{x : Ax\le b\}$ over all integral vectors $b$ .

Formalization targets

Goal: Theorem 10 (p. 260)

\sup_{b\in\mathbb{Z}^m}\ \operatorname{rank}\{x : Ax\le b\}\ \le\ 2^{n^3+1}\,n^{5n}\,\Delta(A)^{n+1}.

In particular, every integral matrix has finite Chvátal rank, and the bound does not depend on $m$ or on $b$ .

Milestones, in attack order

Theorem 1 (p. 252). Suppose $Ax\le b$ has an integral solution and the LP maximum exists. Then every LP optimum has an IP optimum within $\ell_\infty$ -distance $n\Delta(A)$ , and every IP optimum has an LP optimum within the same distance.
Corollary 2 (p. 253). Under the same hypotheses, $\max\{wx: Ax\le b\}-\max\{wx : Ax\le b,\ x\text{ integral}\}\le n\Delta(A)\|w\|_1$ .
Theorem 5 (p. 255). Changing $b$ to $b'$ moves LP optima by at most $n\Delta(A)\|b-b'\|_\infty$ and IP optima by at most $n\Delta(A)(\|b-b'\|_\infty+2)$ . This result is off the goal's path.
Theorem 6 (p. 256). A non-optimal integral solution can be improved by an integral solution within $\ell_\infty$ -distance $n\Delta(A)$ .
Theorem 7 (p. 257). A single integral matrix $M$ , with entries at most $n^{2n}\Delta(A)^n$ in absolute value, gives $\{x: Ax\le b\}_I=\{x : Mx\le d_b\}$ for every $b$ for which $Ax\le b$ has an integral solution.
Theorem 8, printed "Theorem 9" (p. 259). If a rational polyhedron $P\subseteq\mathbb{Q}^n$ has no integral point, then $P^{(n^{2n}2^{n^3})}=\emptyset$ .
Corollary 9 (p. 260). Let $q=\max\{wx : x\in P_I\}$ with $w$ integral. Then $P^{(r)}\subseteq\{x : wx\le q\}$ for $r=(n^{2n}2^{n^3}+1)(\lfloor\max\{wx : x\in P\}\rfloor-q)+1$ .

Significance

The result. Theorem 10 shows that the number of Gomory–Chvátal rounding rounds needed for $\{x : Ax\le b\}$ is controlled by $A$ alone. It is the first general finite bound on the Chvátal rank of a matrix. Earlier, the matrices of Chvátal rank 0 had been characterized by Hoffman and Kruskal: they are the matrices whose transpose is unimodular. Some classes of rank 1 had also been characterized (Edmonds–Johnson, Gerards–Schrijver). The proximity results of §2 are used on their own. They bound the work needed to solve an integer program from an LP optimum, and they show that the optimal value of an integer program changes at most affinely with $b$ . They are also the standard starting point for the later proximity literature.

Formalizing it. All results are proved in the paper. As far as is known, none of them has a machine-checked proof: the Prove2Me corpus holds no Chvátal rank bound, and its existing proximity theorems concern a different bound, the $\ell_1$ bound with $\Delta$ the largest entry. This mission asks for Lean proofs of the paper's statements with the constants exactly as printed. It also builds a reusable layer over $\mathbb{Q}$ : polyhedra, LP and IP optimality, integer hulls, the Chvátal closure and the Chvátal rank.

Difficulty

The proximity theorems need a conic decomposition $\bar x-\bar z=\sum\lambda_i g^i$ into integral generators with entries bounded by $\Delta(A)$ . That requires Cramer's rule bounds on cone generators and Carathéodory's theorem, and neither is in Mathlib in this form for rational polyhedral cones.

Theorem 7 needs finite generation of integral cones with explicit coefficient bounds, together with LP duality.

The Chvátal-rank part is harder. The obvious induction on the value of a valid inequality fails, because the value gap $\lfloor\max_P wx\rfloor-q$ is not bounded independently of $b$ until Theorem 7 and Corollary 2 bound it by $n^{2n+2}\Delta(A)^{n+1}$ . Theorem 8 itself rests on a flatness theorem for lattice-free polyhedra (Lenstra; Grötschel–Lovász–Schrijver), which the paper cites without proof. It also needs Schrijver's lemma that $P^{(k)}\cap F\subseteq F^{(k)}$ for faces $F$ , and invariance under unimodular affine maps. None of these is in Mathlib.

Formalization scope

Rationality. Everything is over $\mathbb{Q}$ , following the paper's standing assumption on p. 252. Points are Fin n → ℚ, $A$ is Matrix (Fin m) (Fin n) ℤ cast to $\mathbb{Q}$ , and a polyhedron is a finite system of rational inequalities.
$\Delta(A)$ . Only nonempty submatrices count, so $\Delta(0)=0$ .
Optimality. "The maximum exists" means an optimal solution exists. Existence claims that the paper proves are part of the conclusions: the IP optimum in Theorem 1 and Corollary 2, and $\max\{wx : x\in P\}$ in Corollary 9.
Chvátal closure. It is defined for every subset of $\mathbb{Q}^n$ , using all integral $a$ and rational $\beta$ . The rank is valued in $\mathbb{N}\cup\{\infty\}$ , with $\infty$ if no iterate equals $P_I$ . A version with junk value $0$ would make the goal trivial and is not used. The matrix rank is a supremum over integral $b$ , as printed.
Added hypotheses. Theorems 1 and 6 carry the hypothesis $A\ne0$ . For $A=0$ the bound $n\Delta(A)=0$ makes both statements false, and the proof on p. 257 assumes $A\ne0$ as well. In Corollary 9 the value $q$ is taken to be an integer. This loses nothing, because a maximum of an integral $w$ over $P_I$ is attained at an integral point.
Constants. All constants are exactly as printed, written in $\mathbb{N}$ with $0^0=1$ .

A complete development needs the following:

cone generation with Cramer bounds and Carathéodory's theorem;
LP duality and Farkas' lemma over $\mathbb{Q}$ ;
the polyhedrality of $P'$ for rational polyhedra (Schrijver 1980);
Schrijver's face lemma and unimodular invariance;
a flatness theorem.

The LP, cone and Chvátal-closure layers are reusable beyond this mission. Proofs of any milestone are welcome, and so is groundwork such as polyhedrality of the Chvátal closure or the flatness theorem, submitted as separate theorems.

Selected references

W. Cook, A.M.H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34 (1986) 251–264. https://doi.org/10.1007/BF01582230
V. Chvátal, Edmonds polytopes and a hierarchy of combinatorial problems, Discrete Mathematics 4 (1973) 305–337. https://doi.org/10.1016/0012-365X(73)90167-2
A. Schrijver, On cutting planes, Annals of Discrete Mathematics 9 (1980) 291–296. https://doi.org/10.1016/S0167-5060(08)70085-2
W. Cook, C.R. Coullard, Gy. Turán, On the complexity of cutting-plane proofs, Discrete Applied Mathematics 18 (1987) 25–38. https://doi.org/10.1016/0166-218X(87)90039-4
F. Eisenbrand, R. Weismantel, Proximity results and faster algorithms for integer programming using the Steinitz lemma, ACM Transactions on Algorithms 16 (2020), Art. 5. https://doi.org/10.1145/3340322

11 thms1 active userReviewed

Completed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

On Sequential Decisions and Markov Chains 1: Deterministic Stationary Procedures Are Optimal for the Long-Run Average Cost and for the Total Cost to AbsorptionResearch Paper

Why restrict to stationary procedures

A Markov decision process with finitely many states and decisions is the basic model of sequential decision making under uncertainty: inventory replacement, machine maintenance, queue control and pursuit problems all fit it. Its computational methods (Howard's policy iteration, 1960; Manne's linear programming formulation, 1960) search only over stationary procedures, which use the same decision every time the system is in the same state. A controller, however, may also remember the whole past and randomize. Whether such procedures can do better is a genuine question: as Derman puts it, "a proof is required before a procedure optimal over $C'$ can be considered as the optimal procedure."

Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (Management Science 9(1):16–24) answers it for two criteria, the long-run average cost and the total cost until absorption, by showing that a deterministic stationary procedure is optimal against all procedures. This mission formalizes that theorem, Theorem 1, together with the steps of its proof.

Timeline. Karlin (1955) gives the existence of a discount-optimal procedure used here; Howard (1960) and Manne (1960) solve the average-cost problem over stationary procedures; Wagner (1960) shows by linear programming that an optimal average-cost procedure can be taken deterministic and stationary; Derman (1962) proves the reduction for both criteria by the functional equation approach; Blackwell (1962) strengthens the discounted side to procedures optimal for all discount factors close to $1$ .

Setting

The system is observed at times $t = 0, 1, \dots$ in one of finitely many states $0, \dots, L$ . After each observation one of $K$ decisions $d_1, \dots, d_K$ is made; every decision is available in every state. If the system is in state $i$ and decision $d_k$ is made, it moves to state $j$ with probability $q_{ij}(k) \ge 0$ , where $\sum_j q_{ij}(k) = 1$ , and a cost $w_{ik}$ is incurred.

A procedure $R$ chooses decision $d_k$ at time $t$ with probability $D_k(X_0, \Delta_0, \dots, X_t)$ , which may depend on the whole history of states $X_s$ and decisions $\Delta_s$ . The class of all procedures is $C$ . The class $C'$ consists of the stationary randomized procedures, for which this probability is a number $D_{ik}$ depending only on the current state $i$ . The class $C''$ consists of the deterministic stationary procedures, those of $C'$ with $D_{ik} \in \{0, 1\}$ , that is, maps $f$ from states to decisions; $C''$ is finite.

Started from $X_0 = i$ , a procedure $R$ incurs the expected cost $W_t$ at time $t$ . The criteria are

Q_R(i) = \limsup_{T \to \infty} \frac1T \sum_{t=0}^{T} W_t \quad\text{(Problem 1)}, \qquad S_R(i) = \sum_{t=0}^{\infty} W_t \in [0, \infty] \quad\text{(Problem 2)},

and, for a discount factor $0 < \alpha < 1$ , the auxiliary discounted cost $V_R(i, \alpha) = \sum_{t \ge 0} \alpha^t W_t$ . Problem 1 assumes $w_{ik} > 0$ . Problem 2 assumes that state $L$ is absorbing under every decision and that $w_{Lk} = 0$ , so $S_R(i)$ is the expected cost of driving the system from $i$ into $L$ .

Formalization targets

Goal: Theorem 1

There are procedures $R_1, R_2 \in C''$ such that, for every state $i$ ,

Q_{R_1}(i) = \min_{R \in C} Q_R(i) \quad\text{(Problem 1)}, \qquad S_{R_2}(i) = \min_{R \in C} S_R(i) \ \ (\text{possibly } \infty) \quad\text{(Problem 2)}.

One procedure serves every initial state, and the minimum is over all of $C$ .

Milestones, in the order of the proof

The functional equation: $V_i = \min_{R \in C} V_R(i, \alpha)$ satisfies $V_i = \min_{D_i} \sum_k D_{ik}\,(w_{ik} + \alpha \sum_j q_{ij}(k) V_j)$ , the minimum over randomizations $D_i$ being attained.
For each $\alpha \in (0,1)$ some $R_\alpha \in C''$ minimizes $V_R(i, \alpha)$ over $C$ .
One $R^* \in C''$ is $\alpha_v$ -discount optimal along a sequence $\alpha_v \to 1$ .
$\lim_{v} (1 - \alpha_v) V_{R^*}(i, \alpha_v) = Q_{R^*}(i)$ for a stationary $R^*$ (published).
The Abelian inequality $Q_R(i) \ge \limsup_{\alpha \to 1^-} (1 - \alpha) V_R(i, \alpha)$ for every $R \in C$ (published).
Theorem 1 (1) itself (published, as part of Sennott's Proposition 6.2.3).
$S_R(i) = \lim_{\alpha \to 1^-} V_R(i, \alpha)$ for every $R \in C$ , finite or not.

Significance

Theorem 1 is what makes finite optimization possible for these problems: once $C''$ is known to contain an optimal procedure, the search runs over finitely many maps, and the linear programs of the paper's §3 (the next mission of this series) and of Manne describe the whole problem rather than a restriction of it. Part (2) is a total-cost result without any assumption that the absorbing state is reached; it holds even when every procedure has infinite cost from some state, which separates it from the stochastic shortest path theory that assumes properness.

Part (1) is available on the platform as part of Sennott's Proposition 6.2.3 (stated there, not yet proved), and it is referenced here rather than restated. Part (2), the functional equation for history-dependent procedures and the Abel-limit identity for the total cost have no statement on the platform; to our knowledge none has a machine-checked proof.

Difficulty

The obvious argument compares an arbitrary procedure with stationary ones state by state, but a history-dependent randomized procedure does not induce a Markov chain, so no transition matrix is available for it. The comparison has to pass through the discounted problem, where an optimal stationary procedure exists for each $\alpha$ , and then let $\alpha \to 1$ . Two limit exchanges are needed: for the average cost, an Abelian inequality valid for every procedure plus a Markov chain limit theorem for the stationary one; for the total cost, monotone convergence in $[0, \infty]$ , which must work when the limit is infinite. The discount-optimal procedure depends on $\alpha$ , and the finiteness of $C''$ is what yields a single procedure along a sequence $\alpha_v \to 1$ .

Formalization scope

The model is the published SennottDP.AvgFinite.Model (a Markov decision chain with finite action sets, nonnegative costs in $\mathbb R_{\ge 0}$ and transition probabilities in $[0, \infty]$ ) with finite nonempty types of states and decisions and every action set equal to the whole decision type. Derman's class $C$ is its Policy (history-dependent, randomized); $C''$ is StationaryPolicy. $W_t$ is expCost, $V_R(i, \alpha)$ is discCost, and $Q_R(i)$ is avgCost $= \limsup_n \frac1n \sum_{t<n} W_t$ , which has the same value as Derman's normalization because $W_t$ is bounded. $S_R(i)$ is a new definition, a sum in $[0, \infty]$ . Every discount factor is restricted to $(0, 1)$ explicitly. "Minimum over $C$ " is stated as an inequality against every policy, with the optimal procedure chosen before the initial state.

Problems 1 and 2 enter as separate implications with their own cost hypotheses; the page's " $w_{ik} > 0$ " is read as $w_{ik} > 0$ for $i \ne L$ in Problem 2, since $w_{Lk} = 0$ there. A formalization that compares only against stationary procedures, or that states the total cost as a real series (whose divergent values default to $0$ ), is ruled out: the competitors are all policies and $S_R(i)$ lives in $[0, \infty]$ .

A complete development needs the discounted Bellman equation for history-dependent policies, the selection of a deterministic minimizer, and Abelian theorems for nonnegative series. These are reusable across the platform's dynamic programming missions, and proofs of the referenced Sennott propositions are welcome contributions in their own right.

Selected references

C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
S. Karlin, The Structure of Dynamic Programming Models, Naval Research Logistics Quarterly 2(4):285–294, 1955. https://doi.org/10.1002/nav.3800020408
A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3):268–269, 1960. https://doi.org/10.1287/mnsc.6.3.268
D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Propositions 6.1.1, 6.2.2, 6.2.3. https://doi.org/10.1002/9780470317037

11 thms4 active usersReviewed

The OR Formalization Drive

Missions

Dynamics of Stochastic Approximation Algorithms 7: Weak Limit Points of the Occupation Measures of a Weak Asymptotic Pseudotrajectory Are InvariantResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 10.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Power of Randomization in On-Line Algorithms 2: The Bound α∘β Against Adaptive Off-Line Adversaries Is TightResearch Paper

Motivation

Setting

Formalization targets

Goal: tightness of Theorem 2.2

Milestones (pp. 12–13)

Significance

Difficulty

Formalization scope

Selected references

Dynamic Scheduling of a System with Two Parallel Servers in Heavy Traffic with Resource Pooling: The Threshold Policy Is Asymptotically OptimalResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Power of Randomization in On-Line Algorithms 1: α-Competitiveness Against Adaptive On-Line and β Against Oblivious Adversaries Give a Deterministic α∘β-Competitive AlgorithmResearch Paper

Why randomization matters in online algorithms

Request-answer games and competitive cost

Formalization targets

Randomization against adaptive off-line adversaries

Composition of two guarantees

What the result supplies

Why the proof is difficult

Formalization scope

Selected references

A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization 3: Fractional Double Greedy on the Multilinear Extension Achieves 1/2 of the OptimumResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem A.1, oracle-access clause

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance II: An O(n²) Extended Formulation of the Multiclass M/M/1 Performance PolymatroidResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Power of Randomization in On-Line Algorithms 3: An Augmented Potential Function Yields an Explicit Deterministic α∘β-Competitive AlgorithmResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.1 (p. 15)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Power of Randomization in On-Line Algorithms 4: Restarting a Bounded-Cost Algorithm Is (1+ε)α-Competitive in Games of Finite DiameterResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1 through its construction

Milestones (proof of Theorem 4.1, pp. 17–18)

Significance

Difficulty

Goal: the $Jm_2+1$ bound, with correctness