Operations Research

Completed

Dynamic Programming Optimization Probability·Captain: mikedeng1

Robust Dynamic Programming 2: The Discounted Robust Value Function Is the Unique Fixed Point of the Robust Bellman OperatorResearch Paper

Motivation

Markov decision processes model sequential decisions under uncertainty, and their optimal policies are computed from transition probabilities that in practice are estimated from data. Optimal policies can be sensitive to estimation error in those probabilities. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. Garud Iyengar's Robust dynamic programming (CORC Tech Report TR-2002-07, 2002, rev. 2004; Mathematics of Operations Research 30(2), 2005) set up this theory for countable state spaces and history-dependent policies. It isolated the Rectangularity assumption under which the robust problem keeps a Bellman equation. In the same period, Nilim and El Ghaoui studied robust control of Markov decision processes with finite state spaces.

Timeline:

1968, 1973. Satia (PhD thesis) and Satia and Lave (Operations Research 21) treat finite-state, finite-action Markov decision processes with uncertain transition probabilities. They state the max–min optimality equation and the optimality of stationary policies, assuming convex uncertainty sets, and do not prove that the solution of the equation is the robust value function.
2001. Bagnell, Ng and Schneider analyse robust policies when the decision maker is restricted to stationary policies.
2002–2005. Iyengar (this paper) and Nilim and El Ghaoui (Operations Research 53, 2005) give the rectangular theory. Iyengar proves the discounted robust Bellman equation for countable state spaces, against history-dependent randomized policies and an adversary that may change the law at every visit.

Setting

A discounted ambiguous Markov decision process has a countable state set $\mathcal S$ , for each state $s$ a nonempty set $\mathcal A(s)$ of admissible actions, for each admissible pair $(s,a)$ a nonempty set $\mathcal P(s,a)$ of probability measures on $\mathcal S$ (the ambiguity set), a bounded reward $r(s,a,s')$ and a discount factor $\lambda\in(0,1)$ . Decisions are made at epochs $t=0,1,2,\dots$ .

A policy $\pi=(d_0,d_1,\dots)$ maps each history $h_t=(s_0,a_0,\dots,s_t)$ to a probability measure on $\mathcal A(s_t)$ . $\Pi$ is the set of all such policies. A deterministic Markov policy plays $d_t(s_t)$ for maps $d_t:\mathcal S\to\mathcal A$ with $d_t(s)\in\mathcal A(s)$ . A stationary policy uses one such rule $d$ at every epoch.

Under Rectangularity, the adversary picks a law $p\in\mathcal P(s_t,a_t)$ separately at every epoch and history, and may pick a different law each time a state–action pair recurs. This is the dynamic model, and the set of path measures it generates is $\mathcal T^\pi$ . In the static model the adversary fixes one $\bar p_{sa}\in\mathcal P(s,a)$ per pair. The robust value of a policy and the robust value function are

V^\pi_\lambda(s)=\inf_{\mathbf P\in\mathcal T^\pi}\mathbf E^{\mathbf P}\Big[\sum_{t=0}^\infty\lambda^t r(s_t,d_t(h_t),s_{t+1})\Big],\qquad V^*_\lambda(s)=\sup_{\pi\in\Pi}V^\pi_\lambda(s).

Let $\mathbf V$ be the bounded functions on $\mathcal S$ with $\|V\|=\sup_s|V(s)|$ . For a set $\mathcal D$ of deterministic Markov rules, the robust Bellman operator is

\mathcal L_{\mathcal D}V(s)=\sup_{d\in\mathcal D}\ \inf_{p\in\mathcal P(s,d(s))}\mathbf E^p\big[r(s,d(s),s')+\lambda V(s')\big].

Formalization targets

Goal: Corollary 2(b)

V^*_\lambda(s)=\sup_{a\in\mathcal A(s)}\ \inf_{p\in\mathcal P(s,a)}\mathbf E^p\big[r(s,a,s')+\lambda V^*_\lambda(s')\big],\qquad s\in\mathcal S,

$V^*_\lambda$ is the only bounded solution of this equation, and for every $\epsilon>0$ some stationary deterministic policy $\pi^\epsilon$ has $V^{\pi^\epsilon}_\lambda\ge V^*_\lambda-\epsilon$ .

Milestones

Theorem 5(a). $\mathcal L_{\mathcal D}$ maps $\mathbf V$ to $\mathbf V$ and $\|\mathcal L_{\mathcal D}U-\mathcal L_{\mathcal D}V\|\le\lambda\|U-V\|$ .
Theorem 5(b). For $\mathcal D=\prod_s\mathcal D(s)$ , the equation $\mathcal L_{\mathcal D}V=V$ has a unique bounded solution, equal to the robust value over deterministic Markov policies with rules in $\mathcal D$ .
Corollary 2(a). The robust value of a stationary policy $(d,d,\dots)$ is the unique bounded solution of $V(s)=\inf_{p\in\mathcal P(s,d(s))}\mathbf E^p[r(s,d(s),s')+\lambda V(s')]$ .
Theorem 4. $V^*_\lambda(s)=\sup_{\pi\in\Pi_{MD}}V^\pi_\lambda(s)$ .
Lemma 3. For a stationary policy, the dynamic and static models give the same value.
Lemma 2. The value of a stationary policy is the optimal solution of the robust program (31).
Lemma 1, first claim. The output of robust value iteration is within $\epsilon/4$ of $V^*_\lambda$ .

Significance

Corollary 2(b) justifies computing the robust value function by solving a state-wise max–min equation. Value iteration, policy iteration and their approximations all rely on that equation. It also shows that a decision maker facing a history-dependent adversary loses at most $\epsilon$ by committing to a stationary deterministic rule. Corollary 2(a) and Lemma 2 make robust policy evaluation a fixed point problem and a robust optimization problem. Lemma 3 shows that, for stationary policies, the dynamic model costs nothing relative to the static model, in which the true transition law is fixed but unknown.

The results are proved on paper. The page proves Theorem 4 only by citation to Puterman's non-robust arguments. No machine-checked proof of any of them is known. The platform has finite-state analogues posed by the Nilim–El Ghaoui and Satia–Lave missions, which compare only stationary or Markov controllers. This mission poses the countable, history-dependent version, and proving it would establish them in this generality.

Difficulty

The contraction property is a state-by-state $\epsilon$ -argument. The hard step is to identify the fixed point with the value of the game against all history-dependent randomized policies. The adversary's choices at different epochs interact only through Rectangularity, so splitting the infimum over path measures into a first-step infimum and a continuation infimum must be justified for an infinite horizon, uncountably many adversary strategies and no attainment of the infima. The ambiguity sets need not be convex or closed. The naive route, "take the minimizing law at each state", is unavailable, and every bound must be carried with an $\epsilon$ slack. Truncating the infinite sum needs the uniform reward bound. Theorem 4 needs a separate argument that randomization and history dependence do not help the decision maker against the dynamic adversary.

Formalization scope

States and actions are countable Lean types; $\mathcal A(s)$ and $\mathcal P(s,a)$ are sets, assumed nonempty, with no convexity or closedness. Laws are PMFs and $\mathbf E^p[f]=\sum_x p(x)f(x)$ as a tsum. The rewards satisfy $|r(s,a,s')|\le R$ on admissible actions. This is the reading of the page's " $\sup r=R<\infty$ ", which its bounds $\pm R/(1-\lambda)$ require. The discount factor satisfies $0<\lambda<1$ . Epochs start at $0$ , so the first reward is undiscounted.

A policy maps $(n, h_n)$ to a PMF supported on $\mathcal A(s_n)$ . The dynamic adversary maps $(n,h_n,a)$ to a law in $\mathcal P(s_n,a)$ . The path law is built by PMF.bind, and the discounted reward is $\sum_t\lambda^t\mathbf E[r(s_t,a_t,s_{t+1})]$ , which converges absolutely. Values are real infima and suprema over nonempty families bounded by $R/(1-\lambda)$ , so no junk value arises. $\mathbf V$ is the predicate "bounded", and $\|\cdot\|$ is a supremum (the page writes max). All uniqueness claims are uniqueness among bounded functions.

$V^*_\lambda$ is a supremum over all history-dependent randomized policies. Defining it over deterministic Markov or stationary policies would make Theorem 4 trivial and weaken the goal, so it is ruled out. The adversary in $V^\pi_\lambda$ is the dynamic one; the static adversary appears only in Lemma 3.

The mission deviates from the page in three places:

Theorem 5(b) is stated for product sets $\mathcal D=\prod_s\mathcal D(s)$ . For an arbitrary $\mathcal D$ the printed statement fails, because its proof pastes $\epsilon$ -greedy actions state by state. Both uses in Corollary 2 are products.
Lemma 3 is stated for randomized Markov rules, which is the page's "any decision rule". The page proves it for deterministic rules.
Lemma 2 adds $\sum_s\alpha(s)<\infty$ and restricts the program to bounded $V$ .

Only the first claim of Lemma 1 is posed. Its second claim, that an $\epsilon/2$ -greedy rule is $\epsilon$ -optimal, is false as printed.

A complete development needs a general toolkit that is reusable beyond this mission: path laws of countable controlled processes with history-dependent policies, a uniform $\epsilon$ -optimal selection argument for real infima over arbitrary sets, and the Banach fixed point theorem on bounded functions (Mathlib's ContractingWith). Proofs of individual milestones are welcome in any order. Theorem 5(a) is the natural entry point.

Selected references

G. Iyengar, Robust dynamic programming, CORC Tech Report TR-2002-07, Columbia University, 2002 (rev. May 4, 2004); published in Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
J. K. Satia and R. E. Lave, Markovian decision processes with uncertain transition probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
J. A. Bagnell, A. Y. Ng and J. Schneider, Solving uncertain Markov decision problems, Tech. Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001. https://www.ri.cmu.edu/publications/solving-uncertain-markov-decision-problems/
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

12 thms1 active userReviewed

Linear Optimization Optimization Probability·Captain: mikedeng1

Primal and Dual Linear Decision Rules in Stochastic and Robust Optimization 3: In Multistage Programs, the Primal and Dual Linear Decision Rule Problems Equal the LPs (4.2) and (4.6)Research Paper

Motivation

A linear multistage stochastic program chooses decisions over $T$ stages while a random vector is revealed one piece at a time; each decision may depend only on what has been observed so far. Such programs model production planning, capacity expansion, hydro scheduling and portfolio problems. Computing their optimal value exactly is intractable in general: Shapiro and Nemirovski argue that even medium-accuracy solutions are out of reach when the number of stages grows (Shapiro–Nemirovski 2005), and already the one-stage problem is #P-hard (Dyer–Stougie 2006, Theorem 3.2, as cited by the paper).

Linear decision rules restrict every decision to be an affine function of the observations. Introduced for robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004) and carried into stochastic programming by Shapiro and Nemirovski and by Chen, Sim, Sun and Zhang (2008), they turn the problem into a finite one whose optimal value is an upper bound. Kuhn, Wiesemann and Georghiou (Optimization Online 2009/02/2218; Math. Program. 130, 2011) apply the same restriction to the dual problem, which yields a lower bound. They show that, for polyhedral supports, both bounds are values of explicit linear programs. This mission formalizes the multistage version of that statement, Theorem 3 of the preprint.

Setting

Stages are $t \in \mathbb T = \{1,\dots,T\}$ . The uncertainty is $\xi = (\xi_1,\dots,\xi_T) \in \mathbb R^k$ with $\xi_t \in \mathbb R^{k_t}$ and $k = \sum_t k_t$ ; by convention $k_1 = 1$ and $\xi_1 = 1$ . The history at stage $t$ is $\xi^t = (\xi_1,\dots,\xi_t) \in \mathbb R^{k^t}$ , $k^t = \sum_{s\le t} k_s$ , and the truncation operator $P_t = [\,I\ \ 0\,] \in \mathbb R^{k^t\times k}$ maps $\xi$ to $\xi^t$ . The law $\mathbb P$ of $\xi$ has support $\Xi = \{\xi : W\xi \ge h\}$ , a nonempty bounded polyhedron spanning $\mathbb R^k$ , whose first two constraints encode $\xi_1 = 1$ . $\mathbb E_t$ denotes conditional expectation given $\xi^t$ , and $M = \mathbb E(\xi\xi^\top)$ is the second-order moment matrix.

A stage- $t$ decision is a square-integrable Borel function $x_t$ of $\xi^t$ (written $x_t \in \mathcal L^2_{k^t,n_t}$ ). The program $\mathcal{MSP}$ minimizes

\mathbb E\Big(\sum_{t=1}^T c_t(\xi^t)^\top x_t(\xi^t)\Big) \quad\text{subject to}\quad \mathbb E_t\Big(\sum_{s=1}^T A_{ts}x_s(\xi^s)\Big) \le b_t(\xi^t)\ \ \mathbb P\text{-a.s.},\ t\in\mathbb T,

with deterministic matrices $A_{ts}$ , $c_t(\xi^t) = C_tP_t\xi$ and $b_t(\xi^t) = B_tP_t\xi$ . The linear conditional mean assumption requires $\mathbb E_t(\xi) = M_tP_t\xi$ almost surely for some $M_t \in \mathbb R^{k\times k^t}$ ; it holds, for example, for stagewise independent data.

The primal approximation $\mathcal{MSP}^u$ sets $x_t(\xi^t) = X_tP_t\xi$ and slacks $s_t(\xi^t) = S_tP_t\xi$ . The dual approximation $\mathcal{MSP}^l$ keeps general rules $x_t, s_t$ but imposes the slack equations only in the weak form $\mathbb E([\sum_s A_{ts}x_s + s_t - b_t][P_t\xi]^\top) = 0$ . The linear programs (4.2) and (4.6) are written in the matrices $X_t$ , multipliers $\Lambda_t$ and slack matrices $S_t$ , with $N_t = MP_t^\top(P_tMP_t^\top)^{-1}$ .

Formalization targets

Goal: Theorem 3 (p. 22)

Under the standing assumptions, the linear conditional mean assumption, and strict feasibility of $\mathcal{MSP}$ ,

\mathrm{val}(\mathcal{MSP}^u) = \mathrm{val}(4.2) \qquad\text{and, if } k \ge 2 \text{ or } \hat W \ne 0,\qquad \mathrm{val}(\mathcal{MSP}^l) = \mathrm{val}(4.6),

as extended-real optimal values. Both equalities are part of the goal.

Milestones

Lemma 2 (p. 20): for every $x_t \in \mathcal L^2_{k^t,n_t}$ there is a unique $X_t$ with $X_tP_tM = \mathbb E(x_t(\xi^t)\xi^\top)$ , and likewise for slacks.
Lemma 3 (p. 21): a moment condition $S_tP_tM = \mathbb E(s(\cdot)\xi^\top)$ with $s \ge 0$ can be met by a non-anticipative slack $s_t(\xi^t)$ iff it can be met by a slack depending on the full $\xi$ .
§4, (4.7) (p. 21): through (4.3), the equality constraints of $\mathcal{MSP}^l$ are equivalent to $\sum_s A_{ts}X_sP_sN_tP_t + S_tP_t = B_tP_t$ .

Significance

The theorem makes both linear-decision-rule bounds on a multistage stochastic program computable by linear programming, with size polynomial in $k$ , $l$ , $\sum_t m_t$ and $\sum_t n_t$ and hence typically linear in the number of stages. The gap between the two values measures the suboptimality of the primal linear rule. These results underlie later work on piecewise-linear and lifted decision rules and on multistage robust and distributionally robust optimization.

The preprint omits the proof of Theorem 3 ("it widely parallels the argumentation in Section 2"), so a formal proof has to supply the multistage details: the conditional-expectation bookkeeping, the truncation operators and the transfer of the one-stage cone description to non-anticipative slacks. No part of this paper has been machine-checked before; the companion mission of this series formalizes the one-stage Theorem 1.

Difficulty

The obvious route repeats the one-stage argument stage by stage, and it breaks at the slack constraints of $\mathcal{MSP}^l$ . A slack $s_t$ must be a function of $\xi^t$ alone, while the one-stage cone characterization of moment vectors $\mathbb E(s(\xi)\xi)$ concerns functions of the full $\xi$ ; Lemma 3 bridges them only through the linear conditional mean assumption and conditional expectations. A second difficulty is the closure gap between that cone and its polyhedral outer description: the equality of $\mathrm{val}(\mathcal{MSP}^l)$ and $\mathrm{val}(4.6)$ relies on strict feasibility, and a proof that ignores it is wrong. On the primal side, the passage from almost sure constraints to identities of matrices needs both that every point of $\Xi$ is charged by $\mathbb P$ and that $\Xi$ spans $\mathbb R^k$ .

Formalization scope

Vectors are functions Fin d → ℝ; stage $t$ is the Fin T index $t-1$ and coordinate $1$ is index 0. The history dimension is kbar kk t, the truncation is the restriction to the first $k^t$ coordinates, and $P_t$ is also given as a $0/1$ matrix. $\mathbb E_t$ is Mathlib's condExp with respect to the σ-algebra generated by $P_t$ . " $\Xi$ is the support of $\mathbb P$ " means: $\Xi$ closed, $\mathbb P(\Xi^c) = 0$ , and every ball around a point of $\Xi$ has positive mass. Decision rules are Borel functions of the history whose composition with $P_t$ is in $L^2(\mathbb P)$ . Optimal values are infima in EReal ( $+\infty$ if infeasible, $-\infty$ if unbounded), and "equivalent" means equal optimal values. The matrices $M_t$ are data, with the conditional-mean identity as a hypothesis.

Three conventions are fixed where the page is silent or misprinted. Strict feasibility of $\mathcal{MSP}$ , not defined in §4, is the analogue of (2.9) for the standard form (4.1): slacks at least $\varepsilon > 0$ almost surely. The equality constraint of $\mathcal{MSP}^l$ is printed with $s_t - b_t$ inside $\sum_s$ ; the formalization follows (4.7), where the sum covers only $A_{ts}x_s$ . The sign condition in (4.5c) is printed as $\tilde s_t(\xi^t) \ge 0$ for a function of $\xi$ , and is read as $\tilde s_t(\xi) \ge 0$ . The theorem's last sentence (polynomial size, efficient solvability) is informal and not formalized. One hypothesis is added: the goal's second equality assumes $k \ge 2$ or that some row of $\hat W$ (the rows of $W$ below (2.1b)) is nonzero (the first equality is stated without it). For $k = 1$ the support is the single point $\{1\}$ , and if $W$ has no nonzero row beyond (2.1b) the cone of Proposition 3 is all of $\mathbb R$ ; the printed second equality then fails (a strictly feasible one-stage instance has $\mathrm{val}(\mathcal{MSP}^l) = 0$ while (4.6) is unbounded below). The added hypothesis excludes exactly this case.

Expectations are Bochner integrals, which vanish on non-integrable functions; under the standing assumptions $\xi$ is bounded almost surely, so all integrands involving square-integrable rules are integrable and no constraint is satisfied vacuously. Matrix.inv returns $0$ on singular matrices, but $P_tMP_t^\top$ is positive definite under the standing assumptions. The linear conditional mean hypothesis cannot be dropped from Lemmas 2 and 3: without it $X_t$ need not exist.

A complete development needs the support and moment facts of §2 ( $M \succ 0$ , almost sure constraints extend to $\Xi$ ), Farkas-type duality for the polyhedron $\Xi$ , the tower property of conditional expectation, and the cone results of Propositions 3 and 4 of the preprint. These are reusable across the series. Proofs of the milestones, or of these supporting facts as separate lemmas, are welcome.

Selected references

D. Kuhn, W. Wiesemann, A. Georghiou, Primal and dual linear decision rules in stochastic and robust optimization, Optimization Online preprint 2009/02/2218, 2009; Math. Program. 130:177–209, 2011. https://optimization-online.org/2009/02/2218/ ; https://doi.org/10.1007/s10107-009-0331-4
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99:351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
A. Shapiro, A. Nemirovski, On complexity of stochastic programming problems, in Continuous Optimization, Springer, 2005. https://doi.org/10.1007/0-387-26771-9_4
X. Chen, M. Sim, P. Sun, J. Zhang, A linear decision-based approximation approach to stochastic programming, Oper. Res. 56(2):344–357, 2008. https://doi.org/10.1287/opre.1070.0441
M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Math. Program. 106:423–432, 2006. https://doi.org/10.1007/s10107-005-0597-0

8 thms1 active userReviewed

Linear Optimization Probability·Captain: mikedeng1

Stochastic Machine Scheduling with Precedence Constraints 1: LP-Based Delayed List Scheduling Is a (1 + β)(1 + 1/β + max{1, (m − 1)Δ/m})-Approximation for P|r_j, prec|E[Σ w_j C_j]Research Paper

Motivation

Scheduling jobs whose processing times are not known in advance is a basic problem of production planning, project management and computing systems. In the stochastic machine scheduling model only the distribution of each processing time is known beforehand; the actual duration of a job is revealed when the job completes. A solution is then not a schedule but a scheduling policy, which decides at every point in time what to start next on the basis of what has been observed so far.

For precedence-constrained problems, constant-factor guarantees for policies were long unavailable. Möhring, Schulz and Uetz (J. ACM 1999) introduced LP relaxations with load inequalities for stochastic scheduling and obtained the first constant-factor policies for independent jobs. In the deterministic setting, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 2001) gave a list scheduling algorithm with deliberate idle times for $\mathrm P\,|\,r_j,\mathit{prec}\,|\sum w_jC_j$ . Skutella and Uetz (SIAM J. Comput. 2005) combined the two and gave the first constant-factor approximation for stochastic scheduling with precedence constraints and release dates. This mission formalizes that result.

Setting

A finite set $V$ of jobs is to be scheduled on $m\ge1$ identical parallel machines, nonpreemptively. Precedence constraints are the arcs $A$ of an acyclic digraph: an arc $(i,j)$ requires $j$ to start no earlier than $i$ completes, and $i$ is a predecessor of $j$ if a directed path leads from $i$ to $j$ . Job $j$ has a release date $r_j\ge0$ , before which it must not start, and a weight $w_j\ge0$ . Following §2 of the paper, release dates are assumed to respect the precedence constraints (Assumption 2.1: $r_i\le r_j$ whenever $i$ is a predecessor of $j$ ).

The processing time of job $j$ is a random variable $P_j\ge0$ with finite mean $\mathrm E[P_j]$ ; the $P_j$ are stochastically independent. For a realization $p$ of the processing times, a feasible schedule assigns start times $S_j\ge r_j$ such that $S_i+p_i\le S_j$ for every arc and at most $m$ jobs are in process at any time. A policy $\Pi$ maps realizations to feasible schedules; it is nonanticipatory if what it has started by time $t$ depends only on what has been observed by $t$ . The completion time of $j$ under $\Pi$ is $C^\Pi_j(P)=S^\Pi_j(P)+P_j$ .

The coefficient of variation is $\mathrm{CV}[P_j]=\sqrt{\mathrm{Var}[P_j]}/\mathrm E[P_j]$ ; the mission assumes $\mathrm{CV}[P_j]\le\sqrt\Delta$ for all $j$ and some $\Delta\ge0$ . With $\mu_j=\mathrm E[P_j]$ , the set function

f(W)=\frac1{2m}\Big(\big(\textstyle\sum_{j\in W}\mu_j\big)^2+\sum_{j\in W}\mu_j^2\Big)-\frac{(m-1)(\Delta-1)}{2m}\sum_{j\in W}\mu_j^2

defines the LP relaxation: minimize $\sum_jw_jC^{\mathrm{LP}}_j$ subject to $\sum_{j\in W}\mu_jC^{\mathrm{LP}}_j\ge f(W)$ for all $W\subseteq V$ , $C^{\mathrm{LP}}_j\ge C^{\mathrm{LP}}_i+\mu_j$ for $(i,j)\in A$ , and $C^{\mathrm{LP}}_j\ge\mu_j$ .

Algorithm CMNS takes a priority list $L$ and a parameter $\beta$ . Whenever a machine is idle and the first job of the residual list (the jobs not yet scheduled) is available, it is scheduled. Otherwise the first available job $j$ of the residual list is deliberately delayed; idle machines accumulate deliberate idle time charged to $j$ , and once $j$ has been charged $\beta\,\mathrm E[P_j]$ it is scheduled out of order. The critical chain of a job $j$ is traced backwards through critical predecessors (those completing last, after $r_j$ ); its length is $\ell_j(p)$ .

Formalization targets

Goal: Theorem 4.1

If $C^{\mathrm{LP}}$ is an optimal LP solution, $L$ orders the jobs by nondecreasing $C^{\mathrm{LP}}_j$ and $\beta>0$ , then for every feasible nonanticipatory policy $\Pi$

\mathrm E\Big[\sum_jw_jC^{\mathrm{CMNS}}_j(P)\Big]\le(1+\beta)\Big(1+\frac1\beta+\max\Big\{1,\frac{m-1}m\Delta\Big\}\Big)\,\mathrm E\Big[\sum_jw_jC^\Pi_j(P)\Big].

Milestones

Observation 2.4: each job is charged at most $\beta\,\mathrm E[P_j]$ ; idle time while $j$ waits is charged to jobs before $j$ ; no deliberate idle time is uncharged.
Lemma 2.5: the per-realization bound $C_j(p)\le\frac{m-1}m\ell_j(p)+\frac1mr_j+\frac1m\big(\sum_{i\in B_j}(p_i+\beta\mathrm E[P_i])+\sum_{i\in O_j(p)}p_i\big)$ .
Lemma 2.6: $\mathrm E[\sum_{i\in O_j(P)}P_i]=\mathrm E[\sum_{i\in O_j(P)}\mathrm E[P_i]]$ .
Lemma 2.7: $\frac1m\mathrm E[\sum_{i\in O_j(P)}\mathrm E[P_i]]\le\frac1\beta\mathrm E[\ell_j(P)]$ .
Theorem 2.8: $\mathrm E[C_j(P)]\le\big(\frac{m-1}m+\frac1\beta\big)\mathrm E[\ell_j(P)]+\frac{1+\beta}m\sum_{i\in B_j}\mathrm E[P_i]+\frac1mr_j$ .
Theorem 3.1: the load inequalities $\sum_{j\in W}\mathrm E[P_j]\mathrm E[C^\Pi_j(P)]\ge f(W)$ .
§3: expected completion times of any policy are LP-feasible, so the LP optimum is a lower bound.
Lemma 3.3: $\frac1m\sum_{k\le j}\mathrm E[P_k]\le\big(1+\max\{1,\frac{m-1}m\Delta\}\big)C^{\mathrm{LP}}_j$ along the LP order.
§4: $\ell_j(p)\le C_j(p)$ in any feasible schedule, so $\mathrm E[\ell_j(P)]$ is a lower bound for every policy.

Significance

The theorem gives a policy with a performance guarantee independent of the number of jobs for $\mathrm P\,|\,r_j,\mathit{prec}\,|\,\mathrm E[\sum w_jC_j]$ , using only the expected processing times and a bound on their coefficients of variation. For NBUE distributions ( $\Delta=1$ ) and $\beta=1/\sqrt2$ it yields $3+2\sqrt2\approx5.83$ , matching the deterministic guarantee of Chekuri et al. The analysis separates cleanly into an algorithmic half (Theorem 2.8, valid for arbitrary distributions) and a polyhedral half (load inequalities and Lemma 3.3), both reused for the in-forest results of the same paper and in later work on stochastic scheduling.

The result is proved in the paper; it has no machine-checked proof. Formalizing it produces a precise definition of nonanticipatory policies and of a list scheduling algorithm with deliberate idle times in continuous time, a formal proof of the Möhring–Schulz–Uetz load inequalities, and a verified approximation guarantee for a stochastic scheduling policy.

Difficulty

Lemma 2.6 is the step where the stochastic setting departs from the deterministic one: the set $O_j(P)$ of out-of-order jobs is random and correlated with the schedule, and the identity holds only because the decision to start a job out of order is taken before its processing time is revealed. Making this rigorous requires a formal notion of nonanticipation and an independence argument over a random set. On the algorithmic side, the bookkeeping of deliberate idle time, which accumulates at a rate equal to the number of idle machines, must be made precise at instants where several jobs start, including jobs of length zero. The load inequalities compare every nonanticipatory policy at once and involve second moments of the processing times, so they cannot be checked policy by policy.

Formalization scope

Jobs form a finite type; arcs are a relation whose transitive closure is irreflexive; machine capacity is the counting condition "at most $m$ jobs in process", with half-open processing intervals. Processing times may be zero. The CV bound is encoded as finite second moments, positive means and $\mathrm{Var}[P_j]\le\Delta\,\mathrm E[P_j]^2$ .

Algorithm CMNS is characterized by its rules: a decision order nondecreasing in time, the scheduling rule at each decision, and the condition that after the decisions at any time nothing remains to be done. A CMNS policy is a map $\sigma$ with this property for every realization. Nonanticipation and measurability of $\sigma$ , which the paper asserts without proof (p. 795; §5), are hypotheses. Critical chains use a fixed tie-breaking order.

Standing assumptions and added hypotheses: independence, Assumption 2.1, $r_j\ge0$ , $w_j\ge0$ and finite means appear in every statement where they are used. $\beta>0$ is assumed wherever $1/\beta$ appears (Lemma 2.7, Theorem 2.8), where the page allows $\beta\ge0$ with $1/0=\infty$ . Lemma 2.6 assumes that $L$ is a linear extension, as in the surrounding Lemma 2.5 and Theorem 2.8; with zero processing times it fails otherwise. Comparator policies have integrable completion times and, like $\sigma$ , are measurable for the law of $P$ , which §5's requirement that every policy be universally measurable implies.

The goal is not trivialized: comparators range over every feasible nonanticipatory policy, not over list policies or the algorithm itself; $C^{\mathrm{LP}}$ is optimal over all $W\subseteq V$ , not merely feasible; and the expected cost of CMNS is asserted to be finite, so neither side can collapse to a default integral value.

Contributions welcome: proofs of any milestone, in particular Theorem 3.1 and Lemma 3.3, which are reusable for the companion in-forest mission, and a proof that the CMNS rules determine a unique, nonanticipatory, measurable policy.

Selected references

M. Skutella, M. Uetz, Stochastic machine scheduling with precedence constraints, SIAM J. Comput. 34(4) (2005) 788–802. https://doi.org/10.1137/S0097539702415007
R. H. Möhring, A. S. Schulz, M. Uetz, Approximation in stochastic scheduling: the power of LP-based priority policies, J. ACM 46(6) (1999) 924–942. https://doi.org/10.1145/331524.331530
C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31(1) (2001) 146–166. https://doi.org/10.1137/S0097539797327180
R. H. Möhring, F. J. Radermacher, G. Weiss, Stochastic scheduling problems I: General strategies, Z. Oper. Res. 28 (1984) 193–260. https://doi.org/10.1007/BF01919323

12 thms1 active userReviewed

Linear Optimization Optimization Probability·Captain: mikedeng1

Primal and Dual Linear Decision Rules in Stochastic and Robust Optimization 1: With Fixed Recourse, the Primal and Dual Linear Decision Rule Problems Equal the LPs (2.3) and (2.8)Research Paper

Motivation

Linear stochastic programs with recourse model decisions that are taken after an uncertain parameter $\xi$ has been observed: the decision is a decision rule $x(\xi)$ , a function of the data. Computing the optimal value exactly is intractable in general. Dyer and Stougie showed that already two-stage linear stochastic programs are #P-hard (Math. Program. 2006), and the same holds for the one-stage problem $\mathcal{SP}$ below even when $\mathbb P$ is uniform on a cube.

A widely used remedy restricts decision rules to be linear in $\xi$ . Ben-Tal, Goryashko, Guslitzer and Nemirovski introduced this restriction in robust optimization (Math. Program. 2004); Shapiro and Nemirovski (2005) and Chen, Sim, Sun and Zhang (Oper. Res. 2008) carried it into stochastic programming. The restriction yields an upper bound, but on its own it says nothing about how much optimality is lost. Kuhn, Wiesemann and Georghiou (Optimization Online 2009/02/2218; published in Math. Program. 2011) also apply the linear restriction to the dual multipliers. This gives a lower bound, so the gap between the two computable bounds estimates the approximation error. This mission formalizes the paper's model result for the case of fixed recourse and polyhedral support (§2, Theorem 1).

Setting

Uncertainty is a probability measure $\mathbb P$ on $(\mathbb R^k, \mathfrak B(\mathbb R^k))$ . The support $\Xi$ of $\mathbb P$ is the smallest closed set of probability one. A decision rule is an element of $\mathcal L^2_{k,n}$ , the Borel measurable, square-integrable functions $\mathbb R^k \to \mathbb R^n$ . Inequalities between vectors and matrices are componentwise.

The data are a fixed recourse matrix $A \in \mathbb R^{m\times n}$ , matrices $C \in \mathbb R^{n\times k}$ and $B \in \mathbb R^{m\times k}$ giving the costs $c(\xi) = C\xi$ and right-hand sides $b(\xi) = B\xi$ , and $W \in \mathbb R^{l\times k}$ , $h \in \mathbb R^l$ . The stochastic program is

\mathcal{SP}:\quad \min_{x \in \mathcal L^2_{k,n}} \ \mathbb E\big(c(\xi)^\top x(\xi)\big) \quad\text{s.t.}\quad Ax(\xi) \le b(\xi)\ \ \mathbb P\text{-a.s.}

The standing assumptions of §2 are:

the support is the nonempty bounded polyhedron $\Xi = \{\xi : W\xi \ge h\}$ (2.1a);
(2.1b) holds: the first two rows of $W$ are $e_1^\top$ and $-e_1^\top$ , the remaining rows form $\widehat W$ , and $h = (1,-1,0,\dots,0)$ , so that $\xi_1 = 1$ on $\Xi$ ;
$\Xi$ spans $\mathbb R^k$ .

The second-order moment matrix is $M = \mathbb E(\xi\xi^\top)$ . $\mathcal{SP}$ is strictly feasible (2.9) if some $\bar x \in \mathcal L^2_{k,n}$ , $\bar s \in \mathcal L^2_{k,m}$ and $\varepsilon > 0$ satisfy $A\bar x(\xi) + \bar s(\xi) = b(\xi)$ and $\bar s(\xi) \ge \varepsilon e$ almost surely.

The two approximations are as follows.

Primal linear decision rules, $\mathcal{SP}^u$ : minimize $\operatorname{Tr}(MC^\top X)$ over $X \in \mathbb R^{n\times k}$ , $S \in \mathbb R^{m\times k}$ with $AX\xi + S\xi = B\xi$ and $S\xi \ge 0$ almost surely.
Dual linear decision rules, $\mathcal{SP}^l$ : minimize $\mathbb E(c(\xi)^\top x(\xi))$ over $x \in \mathcal L^2_{k,n}$ , $s \in \mathcal L^2_{k,m}$ with $\mathbb E\big([Ax(\xi)+s(\xi)-b(\xi)]\xi^\top\big) = 0$ and $s \ge 0$ almost surely.

Formalization targets

Goal: Theorem 1 (p. 10)

Under the standing assumptions, $\widehat W \ne 0$ (see Formalization scope) and strict feasibility,

\operatorname{val}\mathcal{SP}^u = \operatorname{val}(2.3) \quad\text{and}\quad \operatorname{val}\mathcal{SP}^l = \operatorname{val}(2.8),

where (2.3) and (2.8) are the linear programs

(2.3)\quad \min_{X,\Lambda}\ \operatorname{Tr}(MC^\top X)\ \text{ s.t. }\ AX + \Lambda W = B,\ \Lambda h \ge 0,\ \Lambda \ge 0,

(2.8)\quad \min_{X,S}\ \operatorname{Tr}(MC^\top X)\ \text{ s.t. }\ AX + S = B,\ (W - he_1^\top)MS^\top \ge 0.

Milestones, in the order the proof uses them

§2.2 (p. 5). The almost-sure constraints of $\mathcal{SP}^u$ hold on all of $\Xi$ , and $AX\xi + S\xi = B\xi$ a.s. is equivalent to $AX + S = B$ .
Proposition 1 (p. 5). If $\Xi$ is nonempty, then $z^\top\xi \ge 0$ on $\Xi$ if and only if $z = W^\top\lambda$ for some $\lambda \ge 0$ with $h^\top\lambda \ge 0$ .
Proposition 2 (p. 7). $M$ is positive definite and invertible.
§2.4 (p. 7). $\operatorname{val}\mathcal{SP}^l$ equals the optimal value of the moment problem (2.6).
Proposition 3 (p. 7). If $\widehat W \ne 0$ , then $\emptyset \ne \operatorname{int}\mathcal K \subseteq \mathcal K_{\mathbb P} \subseteq \mathcal K$ , for the polyhedral cone $\mathcal K = \{z : (W-he_1^\top)z \ge 0\}$ and the moment cone $\mathcal K_{\mathbb P} = \{\mathbb E(s(\xi)\xi) : s \in \mathcal L^2_{k,1},\ s \ge 0\}$ .
Proposition 4 (p. 9). Under strict feasibility and $\widehat W \ne 0$ , (2.6) and (2.8) have the same optimal value.

Significance

Because $\mathcal{SP}^u \ge \mathcal{SP} \ge \mathcal{SP}^l$ , Theorem 1 brackets the value of an intractable stochastic program between two explicit linear programs. The sizes of these programs are polynomial in $k, l, m, n$ . They depend on $\mathbb P$ only through its support and its second-order moment matrix. The difference $\operatorname{val}(2.3) - \operatorname{val}(2.8)$ is therefore a computable certificate of how much the linear-decision-rule restriction can lose. Sections 3 and 4 of the paper extend the same scheme to random recourse (semidefinite programs) and to multistage problems; they are the subjects of the companion missions 2 and 3.

The theorem is proved in the paper. As far as a search of the platform shows, none of the statements above has a machine-checked proof. A formal proof would check the measure-theoretic steps that the paper passes over quickly. These are the passage from "almost surely" to "on the support", the density argument behind $\operatorname{int}\mathcal K \subseteq \mathcal K_{\mathbb P}$ , and the approximation argument of Proposition 4. A formal proof would also produce reusable results on robust counterparts of polyhedral constraints and on moment cones.

Difficulty

The primal half is robust-optimization duality. Its only delicate point is that almost-sure constraints become constraints on all of $\Xi$ , which uses the fact that every point of the support is charged. The dual half is harder. The constraint " $SM$ has rows in $\mathcal K_{\mathbb P}$ " is a family of moment problems over nonnegative square-integrable densities, and $\mathcal K_{\mathbb P}$ is in general not closed. Replacing it by the polyhedral cone $\mathcal K$ is exact only up to the boundary, and it is strict feasibility that removes the boundary effect. Without strict feasibility the optimal values of (2.6) and (2.8) are only known to bracket each other. The proof of Proposition 3 also needs a description of the closed cone generated by $\Xi$ , and this description uses (2.1b).

Formalization scope

Vectors in $\mathbb R^k$ are Fin k → ℝ and matrices are Matrix (Fin m) (Fin k) ℝ. The paper's 1-based indices are 0-based in Lean, so $e_1$ is index 0 and the rows of (2.1b) are rows 0 and 1. The data form a structure Setting, and the standing assumptions form one predicate Standing. The support is encoded by three conditions on $\Xi$ : it is closed, $\mathbb P(\Xi^c) = 0$ , and every ball centred in $\Xi$ has positive mass. This is equivalent to "smallest closed set of probability one"; $\mathbb P(\Xi) = 1$ alone would not be enough. Decision rules are measurable functions with MemLp x 2 P. Expectations of vector- and matrix-valued quantities are written entrywise as Bochner integrals. Under the standing assumptions $\xi$ is bounded almost surely, so every integrand involved is integrable and no integral defaults to $0$ .

"Equivalent" means equal optimal values. Each optimal value is the infimum of the objective over the feasible set in EReal: $+\infty$ if the problem is infeasible and $-\infty$ if it is unbounded below. A one-sided inequality between the values, or the bare statement that the problems are linear programs, is not Theorem 1 and does not close the goal. Strict feasibility is a hypothesis of both equalities, as printed. Proposition 1 is stated for any $W, h$ with a nonempty polyhedron, since nonemptiness is the only property of $\Xi$ it uses. Proposition 3, Proposition 4 and Theorem 1 carry one hypothesis the paper does not state, $\widehat W \ne 0$ (some row of $W$ below the first two is nonzero). The printed statements are false without it: for $k = 1$ , $W = (1,-1)^\top$ , $h = (1,-1)^\top$ , $\mathbb P = \delta_1$ every assumption holds, $W - he_1^\top = 0$ , so $\mathcal K = \mathbb R$ while $\mathcal K_{\mathbb P} = [0,\infty)$ , and (2.8) loses the sign constraint $S \ge 0$ that (2.6) keeps. Under the standing assumptions the hypothesis is automatic whenever $k \ge 2$ . Theorem 1's closing sentence ("the sizes of these linear programs are polynomial … efficiently solvable") is informal and is not formalized.

A complete development needs strong LP duality or Farkas' lemma for inequality systems, the support of a measure in $\mathbb R^k$ , density of $L^2$ -densities in nonnegative measures, and basic facts on interiors of polyhedral cones. The Farkas lemma is on the platform (LinearOptimization.farkas_lemma). Proofs of the milestones are welcome independently. Proposition 1 and Proposition 3 are reusable outside this paper.

Selected references

D. Kuhn, W. Wiesemann, A. Georghiou, Primal and dual linear decision rules in stochastic and robust optimization, Optimization Online 2009/02/2218 (2009); Math. Program. 130 (2011) 177–209. https://doi.org/10.1007/s10107-009-0331-4
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Oper. Res. Lett. 25 (1999) 1–13. https://doi.org/10.1016/S0167-6377(99)00016-4
X. Chen, M. Sim, P. Sun, J. Zhang, A linear decision-based approximation approach to stochastic programming, Oper. Res. 56 (2008) 344–357. https://doi.org/10.1287/opre.1070.0441
M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Math. Program. 106 (2006) 423–432. https://doi.org/10.1007/s10107-005-0597-0
A. Shapiro, A. Nemirovski, On complexity of stochastic programming problems, in Continuous Optimization, Springer (2005) 111–144. https://doi.org/10.1007/0-387-26771-9_4

10 thms1 active userReviewed

Functional Analysis Probability·Captain: mikedeng1

Conditional Risk Mappings: A Positively Homogeneous Lower Semicontinuous Conditional Risk Mapping Is the Supremum of Countably Many Conditional ExpectationsResearch Paper

Motivation

Risk measures quantify the danger of an uncertain cost $X$ by a single number. The axiomatic theory of coherent and convex risk measures (Artzner, Delbaen, Eber and Heath, Coherent measures of risk, 1999; Föllmer and Schied, Convex measures of risk and trading constraints, 2002) is static: the risk is evaluated once, with no information beyond what is known at time zero. Multistage stochastic optimization and dynamic risk management need risk evaluated conditionally: at time 1 part of the uncertainty has been resolved, and the risk of a time-2 cost should be a function of what is known at time 1.

Ruszczyński and Shapiro, in Conditional risk mappings (preprint of February 21, 2004; journal version Mathematics of Operations Research 31(3), 2006), extend their earlier static theory (Optimization of convex risk functions, Math. Oper. Res. 31(3), 2006) to this conditional setting. They define conditional risk mappings by three axioms, derive a pointwise conjugate duality, and show that positively homogeneous conditional risk mappings are, under regularity conditions, suprema of countably many conditional expectations. The last result explains the word conditional: the conditional expectation is the prototype, and every positively homogeneous conditional risk mapping is a worst case over a countable family of them.

Setting

Let $\Omega$ be a set with $\sigma$ -algebras $\mathcal F_1\subset\mathcal F_2$ ; $\mathcal F_1$ is the information available when risk is evaluated. Let $\mathcal X_2$ be a real vector space of $\mathcal F_2$ -measurable functions $X:\Omega\to\mathbb R$ , and $\mathcal X_1\subset\mathcal X_2$ a subspace of $\mathcal F_1$ -measurable ones. Let $\mathcal Y_2$ be a real vector space of finite signed measures on $(\Omega,\mathcal F_2)$ with $\int|X|\,d|\mu|<\infty$ , and pair them by

\langle\mu,X\rangle=\int_\Omega X\,d\mu .

Both spaces carry locally convex topologies that are compatible with this pairing: the continuous linear functionals on each space are exactly the pairings with elements of the other. Two standing conditions hold throughout: (C) if $\mu\in\mathcal Y_2$ is not a nonnegative measure, some nonnegative $X\in\mathcal X_2$ has $\langle\mu,X\rangle<0$ ; (C′) $\mathbb 1_B\in\mathcal X_1$ for every $B\in\mathcal F_1$ .

A conditional risk mapping is a map $\rho:\mathcal X_2\to\mathcal X_1$ with, writing $\rho_\omega(X)=[\rho(X)](\omega)$ :

(A1) convexity: $\rho_\omega(tX+(1-t)Y)\le t\rho_\omega(X)+(1-t)\rho_\omega(Y)$ for $t\in[0,1]$ ;
(A2) monotonicity: $Y(\omega')\ge X(\omega')$ for all $\omega'$ implies $\rho_\omega(Y)\ge\rho_\omega(X)$ ;
(A3) translation equivariance: $\rho(X+Y)=\rho(X)+Y$ for every $Y\in\mathcal X_1$ .

Costs are minimised: smaller $X$ is better. All inequalities hold at every $\omega\in\Omega$ , not almost surely. $\rho$ is positively homogeneous if $\rho(tX)=t\rho(X)$ for $t>0$ , and lower semicontinuous if each $\rho_\omega$ is.

The conjugate is $\rho^*(\mu,\omega)=\sup_{X}\{\langle\mu,X\rangle-\rho_\omega(X)\}\in\overline{\mathbb R}$ and the risk envelope is $\mathcal A(\omega)=\{\mu:\rho^*(\mu,\omega)<\infty\}$ . $\mathcal P_{\mathcal Y_2}$ denotes the probability measures in $\mathcal Y_2$ , and $\mathcal P_{\mathcal Y_2|\mathcal F_1}(\omega)$ those $\nu$ with $\nu(B)=\mathbb 1_B(\omega)$ for all $B\in\mathcal F_1$ . A map $\omega\mapsto\mu_\omega$ is weakly* $\mathcal F_1$ -measurable if every $\omega\mapsto\langle\mu_\omega,X\rangle$ is $\mathcal F_1$ -measurable. For such a selection of $\mathcal A$ , the operator $[\mathbb Q_\mu(\nu)](A)=\int\mu_\omega(A)\,d\nu(\omega)$ acts on $\mathcal Y_2$ . Assumption (K): $\mathcal P_{\mathcal Y_2}$ is compact, and every such $\mathbb Q_\mu$ maps $\mathcal P_{\mathcal Y_2}$ into itself with a closed graph. Finally, $\mu(\cdot)$ is the conditional probability of $\nu$ given $\mathcal F_1$ if each $\omega\mapsto\mu_\omega(A)$ is $\mathcal F_1$ -measurable and $\int_S\mu_\omega(A)\,d\nu=\nu(A\cap S)$ for $S\in\mathcal F_1$ , $A\in\mathcal F_2$ ; then $\mathbb E_\nu[X|\mathcal F_1](\omega)=\langle\mu_\omega,X\rangle$ .

Formalization targets

Goal: Theorem 2 (p. 11)

If $\mathcal X_2$ is separable, (K) holds and $\rho$ is a positively homogeneous, lower semicontinuous conditional risk mapping, then there are probability measures $\nu^i\in\mathcal P_{\mathcal Y_2}$ , $i\in\mathbb N$ , with

\rho_\omega(X)=\sup_{i\in\mathbb N}\mathbb E_{\nu^i}[X|\mathcal F_1](\omega)\qquad\text{for all }X\in\mathcal X_2,\ \omega\in\Omega,

each conditional expectation being the integral against a weakly* $\mathcal F_1$ -measurable conditional probability of $\nu^i$ .

Milestones

$\operatorname{dom}\rho^*(\cdot,\omega)\subseteq\mathcal P_{\mathcal Y_2|\mathcal F_1}(\omega)$ (proof of Theorem 1, pp. 5–6).
Theorem 1 (p. 5): $\rho_\omega(X)=\sup_{\mu\in\mathcal P_{\mathcal Y_2|\mathcal F_1}(\omega)}\{\langle\mu,X\rangle-\rho^*(\mu,\omega)\}$ , and its converse.
(3.8) (p. 6): for positively homogeneous $\rho$ , $\rho^*(\cdot,\omega)$ is the indicator of a closed convex $\mathcal A(\omega)$ and $\rho_\omega(X)=\sup_{\mu\in\mathcal A(\omega)}\langle\mu,X\rangle$ .
Lemma 1 (p. 11): for separable $\mathcal X_2$ , countably many weakly* measurable selections of $\mathcal A$ suffice.
Under (K), each $\mathbb Q_\mu$ has a fixed point in $\mathcal P_{\mathcal Y_2}$ (p. 10).
Proposition 3 (p. 9): a fixed point $\bar\nu$ of $\mathbb Q_\mu$ has $\mu$ as its conditional probability given $\mathcal F_1$ .

Corollary 1 (p. 10, singleton envelopes give a conditional expectation) and Proposition 2 (p. 7, $\rho(YX)=Y\rho(X)$ for nonnegative $\mathcal F_1$ -step functions $Y$ ) are included as further statements.

Significance

Theorem 2 identifies the positively homogeneous conditional risk mappings with suprema of conditional expectations. It is the conditional analogue of the representation of a coherent risk measure as a worst-case expectation over a set of probability measures. It shows that the axioms (A1)–(A3), stated at every $\omega$ , are the right abstraction of "conditional": nothing beyond conditional expectations and a supremum is needed to generate them. Theorem 1, the pointwise duality on which it rests, is what makes conditional risk mappings usable in multistage problems. Its envelope form (3.8) is what the paper's composition results and dynamic programming equations in §5–§7 manipulate.

The results are proved in the paper, partly by reference: the duality of Theorem 1 by applying the authors' earlier unconditional theorem "verbatim" at each $\omega$ , Lemma 1 through a measurable-selection theorem, and Theorem 2 through Kakutani's fixed-point theorem. None of them is formalized. A formalization would check these deferred steps. In particular the passage, in the proof of Lemma 1, from a dense subset of $\mathcal X_2$ to all of $\mathcal X_2$ uses only lower semicontinuity of $\rho_\omega$ , and whether that suffices in every separable paired space is open to scrutiny.

Difficulty

Theorem 1 needs the Fenchel–Moreau theorem in a general locally convex space, paired through integrals against signed measures. Mathlib's convex duality is mostly finite-dimensional or normed, and the extended-real bookkeeping of conjugates is delicate. The main obstacle is Lemma 1. The envelope $\mathcal A(\omega)$ can be uncountable, and choosing countably many selections that are simultaneously measurable in $\omega$ and exhaust the supremum for every $X$ requires a measurable-selection theorem for multifunctions with values in $\mathcal Y_2$ , a space that need not be metrizable. The obvious argument fixes a dense sequence $X_n$ , picks $\varepsilon$ -optimal measures for each $X_n$ , and passes to general $X$ by semicontinuity. As written, that last step appears to need more than the proof supplies: approximation of $\langle\mu,X\rangle$ by $\langle\mu,X_n\rangle$ uniformly over the chosen $\mu$ needs more than lower semicontinuity of $\rho_\omega$ . The fixed-point step needs a Kakutani-type theorem in a locally convex space, which Mathlib does not provide.

Formalization scope

$\mathcal X_2$ and $\mathcal Y_2$ are abstract real vector spaces with their own topologies (instances of IsTopologicalAddGroup, ContinuousSMul ℝ, LocallyConvexSpace ℝ), realised by injective linear maps into $\Omega\to\mathbb R$ and into Mathlib's SignedMeasure Ω. They are not subspaces of $\Omega\to\mathbb R$ with the pointwise topology. The ambient MeasurableSpace Ω is $\mathcal F_2$ ; $\mathcal F_1\le\mathcal F_2$ is a structure field. The pairing is $\int X\,d\mu^+-\int X\,d\mu^-$ , and integrability against $|\mu|$ is a field, so no integral takes a junk value. Compatibility includes continuity of both pairings as well as the representation of continuous functionals. The paper's space $\mathcal Y_1$ is not modelled; no statement uses it.

Committed conventions:

every statement holds at every $\omega$ ; there are no a.e. classes;
the conjugate and the supremum in (3.6) are in EReal;
suprema of real numbers ((3.8), (4.7), (4.9)) are least upper bounds (IsLUB), never sSup on $\mathbb R$ ;
(K) is taken in its closed-graph form and quantifies over every weakly* measurable selection;
separability is that of the topology of $\mathcal X_2$ .

Two hypotheses are added where the page relies on them implicitly. $\Omega$ is nonempty in the goal, Corollary 1 and the fixed-point milestone. $\mathbb 1_A\in\mathcal X_2$ for every $A\in\mathcal F_2$ is assumed in the goal, Proposition 3 and Corollary 1, because the paper derives measurability of $\omega\mapsto\mu_\omega(A)$ from weak* measurability.

The goal cannot be satisfied by an almost-everywhere version of a conditional expectation chosen separately for each $X$ , which would allow $\rho$ itself as a "version". Each $\mathbb E_{\nu^i}[\cdot|\mathcal F_1]$ is integration against one kernel $\kappa^i$ that is a conditional probability of $\nu^i$ . The goal mentions no selection, fixed point or Kakutani; $\mathbb Q_\mu$ appears only inside (K).

Contributions are welcome on all of the following:

Fenchel–Moreau duality for paired locally convex spaces;
measurable selections of weakly* measurable multifunctions;
a Kakutani–Fan–Glicksberg or Schauder–Tychonoff fixed-point theorem.

All three are reusable beyond this mission.

Selected references

A. Ruszczyński, A. Shapiro, Conditional risk mappings, preprint dated February 21, 2004; Mathematics of Operations Research 31(3):544–561, 2006. https://doi.org/10.1287/moor.1060.0204
A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072
P. Billingsley, Probability and Measure, 3rd ed., Wiley, 1995 (conditional probability, pp. 430–431).

8 thms1 active userReviewed

Optimization·Captain: mikedeng1

Theoretical and Numerical Comparison of Relaxation Methods for Mathematical Programs with Complementarity Constraints 3: Kadrani et al. Relaxation Limits Are M-Stationary under MPEC-CPLDResearch Paper

Motivation

Mathematical programs with complementarity constraints (MPCCs, also called MPECs) model optimization problems in which some constraints say that, for every index $i$ , at least one of two nonnegative quantities $G_i(x)$ , $H_i(x)$ must vanish. They arise in bilevel optimization, Stackelberg games, the design of equilibria in traffic and electricity markets, and contact problems in mechanics (Luo, Pang, Ralph 1996). Standard nonlinear-programming algorithms do not apply directly: at every feasible point of an MPEC the Mangasarian–Fromovitz constraint qualification fails, so the classical convergence theory of SQP or interior-point methods gives no guarantees.

Relaxation methods replace the MPEC by a sequence of better-behaved nonlinear programs $R(t_k)$ with a parameter $t_k \downarrow 0$ , solve each one approximately, and study the limits of the computed points. The question every relaxation method has to answer is what kind of stationary point such limits are, and under which constraint qualification.

Timeline of the result formalized here:

2001: Scholtes introduces the global relaxation $G_iH_i \le t$ and proves that limits are C-stationary under MPEC-LICQ (SIAM J. Optim. 11).
2009: Kadrani, Dussault and Benchakroun propose a relaxation whose feasible set is the union of two shifted orthants (below), and prove that limits are M-stationary under MPEC-LICQ (SIAM J. Optim. 20).
2010–2013: Hoheisel, Kanzow and Schwartz compare five relaxation schemes; for the Kadrani et al. scheme they replace MPEC-LICQ by the much weaker MPEC-CPLD (Theorem 3.5 of the Würzburg preprint, published in Math. Program. 137).

Setting

The MPEC (1) on $\mathbb R^n$ is

\min f(x)\ \text{ s.t. }\ g_i(x)\le 0\ (i\le m),\ h_i(x)=0\ (i\le p),\ G_i(x)\ge 0,\ H_i(x)\ge 0,\ G_i(x)H_i(x)=0\ (i\le l),

with continuously differentiable data. At a feasible $x^*$ the index sets are $I_g=\{i\mid g_i(x^*)=0\}$ , $I_{0+}=\{i\mid G_i(x^*)=0<H_i(x^*)\}$ , $I_{00}=\{i\mid G_i(x^*)=0=H_i(x^*)\}$ (the biactive set) and $I_{+0}=\{i\mid G_i(x^*)>0=H_i(x^*)\}$ .

A feasible $x^*$ is weakly stationary if there are multipliers $\lambda\ge 0$ with $\lambda_ig_i(x^*)=0$ , $\mu$ , $\gamma$ , $\nu$ such that

\nabla f(x^*)+\sum_i\lambda_i\nabla g_i(x^*)+\sum_i\mu_i\nabla h_i(x^*)-\sum_i\gamma_i\nabla G_i(x^*)-\sum_i\nu_i\nabla H_i(x^*)=0,

with $\gamma_i=0$ on $I_{+0}$ and $\nu_i=0$ on $I_{0+}$ . It is M-stationary if the same multipliers satisfy, for every $i\in I_{00}$ , either $\gamma_i>0$ and $\nu_i>0$ , or $\gamma_i\nu_i=0$ .

The tightened program TNLP $(x^*)$ replaces the complementarity constraints by $G_i=0\le H_i$ on $I_{0+}$ , $G_i\ge 0=H_i$ on $I_{+0}$ and $G_i=H_i=0$ on $I_{00}$ . CPLD (constant positive linear dependence) for a nonlinear program says: whenever a set of active-constraint gradients is positive-linearly dependent at $x^*$ (a nontrivial vanishing combination with nonnegative coefficients on the inequalities), the same gradients stay linearly dependent on a neighbourhood of $x^*$ . MPEC-CPLD is CPLD for TNLP $(x^*)$ .

The relaxation of Kadrani et al. is, for $t>0$ ,

R^{KDB}(t):\quad\min f(x)\ \text{ s.t. }\ g(x)\le 0,\ h(x)=0,\ G_i(x)\ge -t,\ H_i(x)\ge -t,\ (G_i(x)-t)(H_i(x)-t)\le 0.

A stationary point of $R^{KDB}(t)$ is a feasible point with KKT multipliers.

Formalization targets

Goal: Theorem 3.5

t_k\downarrow 0,\quad x^k \text{ stationary for } R^{KDB}(t_k),\quad x^k\to x^*,\quad \text{MPEC-CPLD at } x^*\ \Longrightarrow\ x^* \text{ is M-stationary for (1)}.

Milestones, in proof order

MPEC-CPLD written out in terms of the MPEC data (§2.2, display (3)).
The KKT conditions of $R^{KDB}(t_k)$ recast with $\eta^{G,k}_i=-\gamma^k_i(H_i(x^k)-t_k)$ , $\eta^{H,k}_i=-\gamma^k_i(G_i(x^k)-t_k)$ : identity (11), disjointness (13), signs (14).
Eventual support inclusions (12) into $I_{00}\cup I_{0+}$ and $I_{00}\cup I_{+0}$ .
Reduction to linearly independent gradients (15).
Boundedness of the multiplier sequence under MPEC-CPLD.
Weak stationarity of the limit $x^*$ .

Significance

Local minimizers of an MPEC are M-stationary under weak constraint qualifications, whereas strong stationarity needs stronger ones such as MPEC-LICQ; a C-stationary point, the kind of limit the Scholtes relaxation delivers, may still admit first-order descent directions. Theorem 3.5 shows that the Kadrani et al. relaxation reaches M-stationary limits under a constraint qualification that is implied by MPEC-LICQ and MPEC-MFCQ and that holds, for instance, whenever all constraint functions are affine. It separates this scheme from the Scholtes and Steffensen–Ulbrich relaxations in the comparison of the paper.

The theorem is proved in the paper. As far as is known, no part of MPEC theory (constraint qualifications for MPECs, the stationarity hierarchy, relaxation schemes) has a machine-checked proof in Lean or Mathlib. This mission produces a formal account of the stationarity notions of Definition 2.3, of CPLD and MPEC-CPLD, and a complete formal proof of the convergence result, including the standard constraints $g$ , $h$ that the paper's proof skips for brevity.

Difficulty

The obvious argument passes to the limit in the KKT conditions of $R^{KDB}(t_k)$ . This fails because the multipliers need not be bounded: unlike under MPEC-LICQ or MPEC-MFCQ, MPEC-CPLD does not by itself bound KKT multipliers, and the KKT points of the relaxed programs need not satisfy any constraint qualification themselves (Example 3.6 of the paper). The second difficulty is the biactive set $I_{00}$ : the product constraint contributes multipliers $\eta^{G,k}$ , $\eta^{H,k}$ to both $\nabla G_i$ and $\nabla H_i$ , with signs that are not fixed a priori, so a naive limit of the multipliers only gives C-stationarity-type information, or none at all.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and gradients are Mathlib's gradient; indices are 0-based (Fin m, Fin p, Fin l), and $m,p,l$ may be zero. Explicit choices fixed by the formalization:

The standing assumption of p. 1 (all data $C^1$ ) is a hypothesis P.IsC1 of every analytic statement.
" $\{t_k\}\downarrow 0$ " is $t_k>0$ , $t$ nonincreasing, $t_k\to 0$ .
"Stationary point" of an NLP means feasible with KKT multipliers (p. 5).
Gradient sets are indexed families; linear (in)dependence is LinearIndependent ℝ of a family indexed by a disjoint union of subtypes, so repeated gradients count as dependent.
In positive-linear dependence (Definition 2.1), "not all of them being zero" refers to all coefficients; the sign constraint is on the inequality part only.
"Linearly dependent for all $x\in N(x^*)$ " is ∀ᶠ y in 𝓝 x*.
Definition 2.3 is used with its two misprints corrected ( $\mu_i\nabla h_i(x^*)$ ; $\lambda_ig_i(x^*)=0$ for $i\le m$ ); weak and M-stationarity include feasibility of $x^*$ , which the goal derives rather than assumes.
TNLP $(x^*)$ has exactly the constraints the paper lists (subtype index sets, no padding with zero constraints).
The standard constraints $g$ , $h$ , skipped in the paper's proof, are kept in every statement; displays (12) and (15) are extended by their $g$ , $h$ parts.

Two trivializing readings are ruled out. M-stationarity uses one multiplier tuple for both the weak-stationarity equation and the condition on $I_{00}$ ; separate multipliers would make the sign condition vacuous. MPEC-CPLD demands linear dependence on a whole neighbourhood of $x^*$ , not only at $x^*$ ; the pointwise version is a different hypothesis.

A complete development needs the gradient calculus of products and compositions on EuclideanSpace, a Carathéodory-type lemma (a conic combination can be reduced to one over linearly independent vectors with the same signs), and compactness of bounded sequences in finite dimensions. The Carathéodory lemma and the CPLD/positive-linear-dependence layer are reusable for any constraint-qualification argument in nonlinear programming. Proofs of individual milestones, and of the lemma behind (15), are welcome independently of the goal.

Selected references

T. Hoheisel, C. Kanzow, A. Schwartz, Theoretical and numerical comparison of relaxation methods for mathematical programs with complementarity constraints, Preprint 299, Institute of Mathematics, University of Würzburg, 2010; Mathematical Programming 137 (2013) 257–288. https://doi.org/10.1007/s10107-011-0488-5
A. Kadrani, J.-P. Dussault, A. Benchakroun, A new regularization scheme for mathematical programs with complementarity constraints, SIAM Journal on Optimization 20 (2009) 78–103. https://doi.org/10.1137/070705490
S. Scholtes, Convergence properties of a regularization scheme for mathematical programs with complementarity constraints, SIAM Journal on Optimization 11 (2001) 918–936. https://doi.org/10.1137/S1052623499361233
S. Steffensen, M. Ulbrich, A new relaxation scheme for mathematical programs with equilibrium constraints, SIAM Journal on Optimization 20 (2010) 2504–2539. https://doi.org/10.1137/090748883
Z.-Q. Luo, J.-S. Pang, D. Ralph, Mathematical Programs with Equilibrium Constraints, Cambridge University Press, 1996. https://doi.org/10.1017/CBO9780511983658

9 thms1 active userReviewed

Completed

Combinatorics Linear Optimization·Captain: mikedeng1

A Branch-and-Cut Algorithm for the Dial-a-Ride Problem: The Generalized Order-Matching Inequality x(H) + Σ x(T_h) ≤ |H| + Σ|T_h| − 2m Is Valid for Every Feasible Route PlanResearch Paper

Motivation

The dial-a-ride problem (DARP) asks for minimum-cost vehicle routes that carry users from individual pick-up points to individual drop-off points, subject to vehicle capacities, time windows, route durations and a bound on each user's ride time. It models door-to-door transport for elderly and disabled people, shared taxis and on-demand microtransit. Cordeau (Oper. Res. 54(3), 2006) gave a mixed-integer formulation of the DARP and the first branch-and-cut algorithm for it, and reported that instances with up to 30 users can be solved to optimality in reasonable time. The algorithm's strength comes from families of valid inequalities: linear constraints satisfied by every feasible route plan that cut off fractional points of the linear relaxation. Several of these families were adapted from the precedence-constrained asymmetric TSP (Balas, Fischetti and Pulleyblank 1995; Grötschel and Padberg 1985) and from the pick-up and delivery problem (Ruland and Rodin 1997); others, notably the generalized order-matching inequalities, were new in this paper.

Setting

Let $n$ be the number of users. Nodes are $N = \{0, 1, \dots, 2n+1\}$ with pick-up nodes $P = \{1,\dots,n\}$ , drop-off nodes $D = \{n+1,\dots,2n\}$ , origin depot $0$ and destination depot $2n+1$ ; user $i$ travels from node $i$ to node $n+i$ . An instance fixes, for each node $i$ , a load $q_i$ , a service duration $d_i \ge 0$ and a time window $[e_i, l_i]$ ; for each pair of nodes a travel time $t_{ij}$ ; for each vehicle $k$ in a finite set $K$ a capacity $Q_k$ and a maximal route duration $T_k$ ; and a maximal ride time $L$ . The standing conditions are $q_0 = q_{2n+1} = 0$ , $q_i = -q_{n+i}$ for $i \in P$ , and $d_0 = d_{2n+1} = 0$ .

A feasible solution gives each vehicle $k$ a route $0 \to v_1 \to \dots \to v_r \to 2n+1$ through distinct nodes of $P \cup D$ , start-of-service times $B^k_i$ and loads $Q^k_i$ such that every node of $P \cup D$ is visited by exactly one vehicle, $i$ and $n+i$ are on the same route with $i$ first, $B^k_j \ge B^k_i + d_i + t_{ij}$ and $Q^k_j \ge Q^k_i + q_j$ along each travelled arc, the ride time $B^k_{n+i} - (B^k_i + d_i)$ lies in $[t_{i,n+i}, L]$ , the route lasts at most $T_k$ , and the time windows and capacity bounds hold at every visited node. These are the constraints (2)–(14) of the paper's model.

The arc variables are $x^k_{ij} = 1$ when vehicle $k$ travels from $i$ to $j$ , and $x_{ij} = \sum_{k \in K} x^k_{ij}$ . For a node set $S$ write $\bar S = N \setminus S$ , $x(S) = \sum_{i,j\in S} x_{ij}$ , $x(\delta^+(S)) = \sum_{i\in S, j\in \bar S} x_{ij}$ , $x(\delta^-(S)) = \sum_{i \in \bar S, j \in S} x_{ij}$ , $\pi(S) = \{i \in P \mid n+i \in S\}$ and $\sigma(S) = \{n+i \in D \mid i \in S\}$ . An inequality in $x$ is valid for the DARP when the aggregated arc variables of every feasible solution satisfy it.

Formalization targets

Goal: Proposition 5 (p. 578)

Let $i_1, \dots, i_m$ be distinct users and let $H, T_1, \dots, T_m \subseteq P \cup D$ satisfy $\{i_h, n+i_h\} \subseteq T_h$ and $H \cap T_h = \{i_h\}$ . Then every feasible solution satisfies

x(H) + \sum_{h=1}^m x(T_h) \le |H| + \sum_{h=1}^m |T_h| - 2m. \tag{39}

The handle $H$ and the teeth $T_h$ are not required to be disjoint from one another beyond $H \cap T_h = \{i_h\}$ , and $m$ is arbitrary.

Milestones (the steps of the proof of Proposition 5)

$x(S) \le |S| - 1$ for every nonempty $S \subseteq P \cup D$ .
If $x(T) = |T| - 1$ for a set $T \ni i, n+i$ , then a path of arcs with $x_{ab} = 1$ covers $T$ and does not finish at $i$ .
With $\alpha$ the number of teeth for which $x(T_h) = |T_h| - 1$ : $x(\delta^+(H)) \ge \alpha$ .
$x(\delta^+(H)) = x(\delta^-(H))$ and $2x(H) + x(\delta^+(H)) + x(\delta^-(H)) = 2|H|$ for $H \subseteq P \cup D$ .
$x(H) \le |H| - \alpha$ .

Companion statements

The mission also states the other propositions of §4: the lifted subtour elimination inequalities (33) and (34) (Propositions 1 and 2), the predecessor inequality (30), the two liftings (36) and (37) of the generalized order constraint (Propositions 3 and 4), the redundancy of the strengthening (40) of (39) under (30) for fractional points (Proposition 6), and the infeasible path inequality (41) under the triangle inequality for travel times (Proposition 7).

Significance

Valid inequalities are what make branch-and-cut work: each family is added to the linear relaxation by a separation heuristic, and the paper's computational section reports how the bound improves as families are added. Validity is the one property the algorithm cannot check at run time, since a cut that removes a feasible route plan silently returns a suboptimal answer. Remark 2 of the paper observes that (39) is stronger than the TSP comb inequality on the same sets, and Proposition 6 shows that its natural strengthening adds nothing once the predecessor inequalities (30) are present, which tells an implementer which families to separate.

All propositions are proved in the paper, partly in an appendix; none is formalized. A machine-checked development would give a precise route-based model of the DARP that later DARP and pick-up and delivery papers can reuse, and certified validity of the cut families that branch-and-cut codes for these problems separate.

Difficulty

The proofs are short on paper but argue about the shape of routes: "there exists a path connecting all nodes in $T_h$ ", "this path cannot finish at node $i_h$ because of the precedence constraint". Turning a tight subtour count $x(T) = |T| - 1$ into a single covering path requires knowing that the arcs of a feasible solution inside a subset of $P \cup D$ form vertex-disjoint paths, which in turn rests on each node of $P \cup D$ having exactly one predecessor and one successor and on routes containing no cycles. The arithmetic step from $\alpha$ tight teeth to the bound on the handle needs the degree identities for every subset of $P \cup D$ , and counting the arcs leaving $H$ needs the distinctness of the users $i_h$ . Reasoning directly with the linear constraints (2)–(14) does not suffice: those constraints alone do not exclude cycles of zero duration.

Formalization scope

Nodes are natural numbers, so $n+i$ and $2n+1$ appear literally; $N$ , $P$ , $D$ and $P \cup D$ are Finset.range (2n+2), Icc 1 n, Icc (n+1) (2n) and Icc 1 (2n). All data and arc variables are real-valued, and every right-hand side is computed in $\mathbb R$ . Feasible solutions are route-based: each vehicle has a duplicate-free list of nodes of $P \cup D$ , and the constraints of the model are imposed along that list. Read literally, the program (1)–(14) admits closed cycles when $d_i + t_{ij} = 0$ around a cycle, on which every proposition fails, and imposes (11)–(13) also at nodes a vehicle does not visit; the route encoding follows the paper's verbal definition of the DARP and its proofs, which reason about routes. Precedence ( $i$ before $n+i$ ) is a field of the solution, since with zero travel and service times the nonnegativity of ride times does not order the visits. The routing cost plays no role and is omitted. No positivity is assumed for travel or service times.

Added hypotheses, each necessary: sets $S$ in the subtour bound and in (30) are nonempty ( $S = \emptyset$ gives $0 \le -1$ ); the users of Proposition 5 are distinct; the generalized order constraint (Propositions 3 and 4) has $m \ge 2$ (for $m = 1$ it is false); the ordered sets of Propositions 1 and 2 have $h \ge 3$ nodes, the standing assumption of the paragraph that introduces them; Proposition 7 has $p \ge 1$ and a path through distinct nodes. Proposition 6 is the only statement about fractional points: it assumes nonnegativity, no loops, (2), (3) and (30), and drops the remaining constraints of the relaxation, which makes it stronger.

The inequalities are stated for the arc variables of every feasible solution, not for an arbitrary $0$ – $1$ vector satisfying a few degree constraints; a statement of the latter kind is a different and false theorem. Useful contributions include the path structure of the arcs of a feasible solution inside a subset of $P \cup D$ , the degree identities, and the milestone proofs, which are reusable for the other propositions.

Selected references

J.-F. Cordeau, A Branch-and-Cut Algorithm for the Dial-a-Ride Problem, Operations Research 54(3):573–586, 2006. https://doi.org/10.1287/opre.1060.0283
E. Balas, M. Fischetti, W. R. Pulleyblank, The precedence-constrained asymmetric traveling salesman polytope, Mathematical Programming 68:241–265, 1995 (as cited in Cordeau 2006).
M. Grötschel, M. W. Padberg, Polyhedral theory, in Lawler et al. (eds.), The Traveling Salesman Problem, Wiley, New York, 1985, pp. 251–305 (as cited in Cordeau 2006).
K. S. Ruland, E. Y. Rodin, The pickup and delivery problem: Faces and branch-and-cut algorithm, Computers & Mathematics with Applications 33:1–13, 1997 (as cited in Cordeau 2006).

7 thms1 active userReviewed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Validity of Heavy Traffic Steady-State Approximations in Generalized Jackson Networks: Scaled Stationary Queue Lengths Converge to the Stationary Distribution of the Reflected Brownian MotionResearch Paper

Motivation

Open networks of single-server queues with general (non-exponential) interarrival and service times, generalized Jackson networks (GJNs), model manufacturing lines, communication networks and service systems. Their stationary distributions are almost never available in closed form. The standard engineering approximation replaces the scaled queue-length vector by the stationary distribution of a reflected Brownian motion (RBM) in the orthant, which is the diffusion limit of the network in heavy traffic, when every station is close to full utilisation.

The diffusion limit itself (Reiman, 1984) is a statement about the process on finite time intervals. Using the RBM's stationary law as an approximation of the network's stationary law requires interchanging two limits: time to infinity (steady state) and traffic intensity to one (heavy traffic). For a long time this interchange was assumed rather than proved.

Timeline.

1984. Reiman proved the process-level heavy-traffic limit for open queueing networks started empty (doi:10.1287/moor.9.3.441).
1987. Harrison and Williams characterised when an orthant RBM has a stationary distribution and showed it is unique (doi:10.1080/17442508708833469).
1995. Dai related fluid-model stability to positive Harris recurrence of multiclass networks (doi:10.1214/aoap/1177004828).
2006. Gamarnik and Zeevi proved the interchange of limits for GJNs whose primitives have exponential moments (arXiv:math/0410066). This mission formalizes that result.

Setting

There are $J$ stations. Station $j$ receives external arrivals with i.i.d. interarrival times of law $F_{A,j}$ (rate $\alpha_j$ , or no arrivals at all) and serves jobs first-in-first-out with i.i.d. service times of law $F_{S,j}$ (mean $m_j$ , rate $\mu_j = 1/m_j$ ). A job finishing at $j$ moves to $k$ with probability $p_{jk}$ or leaves. The routing matrix $P$ is substochastic with spectral radius below one. Interarrival and service times have uniformly bounded conditional exponential moments of their residual lives (conditions (1)–(2)). The traffic equation $\lambda = \alpha + P'\lambda$ gives the effective rates $\lambda = [I-P']^{-1}\alpha$ and the traffic intensities $\rho_j = \lambda_j m_j$ .

The queue lengths $Q(t)$ are not Markov. The state $\bar Q(t) = (Q(t),\hat a(t),\hat v(t))$ , which adds the elapsed interarrival and service times, is a Markov process on $\mathcal X = \mathbb Z_+^J\times\mathbb R_+^{2J}$ . A law $\pi$ on $\mathcal X$ is stationary if $\bar Q(0)\sim\pi$ implies $\bar Q(t)\sim\pi$ for all $t\ge0$ .

Heavy traffic. Fix a critically loaded network $\Xi$ ( $\rho_j=1$ for all $j$ ) and a vector $\kappa^0>0$ . The network $\Xi^n$ slows the arrivals of $\Xi$ at station $j$ by the factor $1-\kappa^0_j/\sqrt n$ , so that $\rho^n_j = 1-\kappa_j/\sqrt n<1$ for an explicit $\kappa>0$ (display (17)). Let $\pi^n$ be any stationary distribution of $\Xi^n$ , and let $\hat\pi^n$ be the law of $Q^n(0)/\sqrt n$ under $\pi^n$ .

The RBM. For a Brownian motion $W$ with drift $\beta$ and covariance $\Gamma$ , the RBM $Z$ with parameters $(\beta,\Gamma,I-P')$ solves the Skorohod problem $Z = W + [I-P']Y\ge0$ , with $Y$ nondecreasing and increasing only when $Z$ is on the boundary. Here $\beta = -(I-P')M^{-1}\kappa$ and $\Gamma$ is the explicit covariance matrix of Reiman's theorem, built from $\mu$ , $\alpha$ , $P$ and the squared coefficients of variation $c^2_{a,j}$ , $c^2_{s,j}$ of $\Xi$ .

Formalization targets

Goal: Theorem 8 (p. 18)

\hat\pi^n\ \Rightarrow\ \pi_{\mathrm{RBM}}\qquad(n\to\infty),

where $\pi_{\mathrm{RBM}}$ is the unique stationary distribution of the $(\beta,\Gamma,I-P')$ -RBM. The formal goal asserts three things: a stationary distribution of the RBM exists, it is the only one, and $\hat\pi^n$ converges weakly to it, for every choice of stationary distributions $\pi^n$ .

Milestones

Theorems 5 and 6 (pp. 15–16). For a general Markov process, a geometric Lyapunov function $\Phi$ gives $\mathbb E_\pi\Phi\le\phi(t_0)K/(1-\gamma)$ . A Lyapunov function with control of $L_2$ gives an exponential tail $\mathbb P_\pi(\Phi>s)\lesssim e^{-\theta s}$ .
Proposition 1 (p. 11). The fluid model drains in time at most $w'z/\min_j\mu_j(1-\rho_j)$ , where $w=e'[I-P']^{-1}$ .
Lemma A.1 and Propositions 2–3 (pp. 17, 25). The net input deviates from its fluid path by $O(\sqrt n)$ uniformly over initial states. As a result, $\Phi(z,a,v)=w'z$ is a Lyapunov function for $\Xi^n$ with drift $-\sqrt n$ over time $nt_0$ .
Theorem 7 and Corollary 1 (pp. 17–18). $\mathbb P_{\pi^n}(n^{-1/2}w'Q^n(0)>s)\le C_1e^{-c_1s}$ uniformly in $n$ . Hence $\{\hat\pi^n\}$ is tight.
Theorems 4, 3 and 2 (cited). Reiman's process limit from a general initial law; Harrison and Williams's existence and uniqueness theorem for the RBM's stationary distribution; existence of $\pi^n$ .

Significance

The result. Theorem 8 justifies the use of the RBM's stationary distribution, which is computable or at least numerically tractable, as an approximation of steady-state queue lengths of a heavily loaded network. Theorem 7 also shows that each stationary queue is of order $(1-\rho^{*n})^{-1}$ uniformly in $n$ . Together with Theorem 8 this gives convergence of all moments (Corollary 2 of the paper) and, through Theorems 9–12, steady-state approximations of sojourn times and product-form limits.

Formalizing it. No part of this argument is machine-checked. The formalization would add reusable infrastructure for queueing theory in Lean: a Markov-state model of a generalized Jackson network with residual times, Lyapunov bounds on stationary distributions of general Markov processes (Theorems 5–6), and the link between tightness and identification of limit points for stationary laws. Reiman's theorem (Theorem 4) and the Harrison–Williams theorem (Theorem 3) are cited by the paper and are themselves open formalization targets.

Difficulty

Tightness and Reiman's theorem do not combine on their own. Reiman's theorem describes the network on finite time intervals, started empty, while a stationary distribution describes it as time goes to infinity; nothing in the finite-horizon limit forces a limit point of $\hat\pi^n$ to be stationary for the RBM, or forces different subsequences to have the same limit. The interchange therefore needs the process limit from an arbitrary initial law and the uniqueness of the RBM's stationary law, besides tightness.

The tightness step is the technical core. Moment bounds must be uniform in $n$ and in the initial residual times. A Lyapunov argument on the workload $w'Q$ over a time horizon of order $n$ requires deviation bounds of order $\sqrt n$ for renewal processes started at arbitrary ages. This is why the residual-life conditions (1)–(2) appear, and why the strong approximation of Lemma A.2 is used. A naive drift argument over a fixed time horizon fails: in heavy traffic the drift of $w'Q$ per unit time is only of order $n^{-1/2}$ .

Formalization scope

Stations are Fin J, vectors Fin J → ℝ, $P'$ is Pᵀ, and the norm $\|\cdot\|$ is the $\ell^1$ norm, written as an explicit sum. The spectral-radius condition is $P^m\to0$ .
A network is its data $(\mathcal J, F_A, F_S, P)$ plus the predicate IsGJN (positive times, conditions (1)–(2), substochastic $P$ ). $A_j$ and $S_j$ count renewal epochs in $[0,t]$ . The initial times $a_j(0)$ , $v_j(0)$ are residual lives given the elapsed ages $\hat a_j(0)$ , $\hat v_j(0)$ . States carry their elapsed times as reals; the predicate InStateSpace cuts out $\mathcal X=\mathbb Z_+^J\times\mathbb R_+^{2J}$ , and the uniform bounds over initial states (Lemma A.1, Propositions 2–3) and the initial laws of Theorem 4 range over $\mathcal X$ only.
A realization from an initial law is a probability space carrying the primitives with their joint law and processes $Q, B$ satisfying the dynamics (4)–(5) almost surely. $\mathbb E[\cdot\mid\bar Q(0)=x]$ is the expectation under a realization from $\delta_x$ . Stationarity of $\pi$ means: a realization from $\pi$ exists, and every realization from $\pi$ has $\bar Q(t)\sim\pi$ for all $t\ge0$ .
The heavy-traffic scaling is read as $a^n_j = a_j/(1-\kappa^0_j/\sqrt n)$ . The printed $a_j(1-\kappa^0_j/\sqrt n)$ would overload every $\Xi^n$ , so no $\pi^n$ would exist. $\kappa$ is defined so that (17) holds exactly, and every statement about $\Xi^n$ is for all large $n$ .
The RBM is built on the published Reiman84.QueueLength.Paths (Brownian motion with drift and covariance, and the reflection pair). An RBM stationary law must be a probability measure carried by $\mathbb R^J_+$ . Weak convergence of laws on $\mathbb R^J$ uses Mathlib's topology on ProbabilityMeasure. Theorem 4's process convergence is in coupling form with the uniform topology on $[0,T]$ .
Quantities $\limsup_n(\cdot)<\infty$ are rendered as one finite bound valid for all large $n$ . Expectations of nonnegative quantities are lower Lebesgue integrals in $[0,\infty]$ . Constants "depending only on $\Xi$ " are quantified before $n$ and before the stationary distributions.
Disclosed departures from the page:
- $\phi(t_0)<\infty$ is assumed in Theorem 5.
- $\{\Phi>K\}\neq\emptyset$ is assumed in Theorem 6. Its tail constant (29) is stated as $(\gamma\theta/2)^{-1}$ , which is what the paper's proof yields, instead of the printed $(1-\gamma\theta/2)^{-1}$ .
- $\Gamma$ is positive definite in Theorem 3, the hypothesis of Harrison and Williams.
- The derivative bound $w'\dot q(t)\le-\min_j\mu_j(1-\rho_j)$ of Proposition 1 is stated for $\rho_j\le1$ at every station; the page states it unconditionally, and it fails when two stations are overloaded.
- Theorems 5 and 6 are stated for the time- $t_0$ transition kernel of the Markov process.
A trivializing formalization is ruled out explicitly. The goal keeps the existence and uniqueness of $\pi_{\mathrm{RBM}}$ as conjuncts, stationarity requires a realization to exist, and the RBM's stationary law must live on the orthant. Hence neither an impossible network nor an empty RBM notion makes the goal vacuous.
Contributions are welcome on any milestone. The cited Theorems 2–4 are substantial on their own, and Theorems 5–6 are independent of queueing.

Selected references

D. Gamarnik and A. Zeevi, Validity of heavy traffic steady-state approximations in generalized Jackson networks, Ann. Appl. Probab. 16(1), 2006, 56–90. arXiv:math/0410066, doi:10.1214/105051605000000638
M. I. Reiman, Open queueing networks in heavy traffic, Math. Oper. Res. 9(3), 1984, 441–458. doi:10.1287/moor.9.3.441
J. M. Harrison and R. J. Williams, Brownian models of open queueing networks with homogeneous customer populations, Stochastics 22, 1987, 77–115. doi:10.1080/17442508708833469
J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Ann. Appl. Probab. 5(1), 1995, 49–77. doi:10.1214/aoap/1177004828
H. Chen and D. D. Yao, Fundamentals of Queueing Networks: Performance, Asymptotics, and Optimization, Springer, 2001 (reference [11] of the paper; Chapter 7).

18 thms1 active userReviewed

Probability Stochastic Systems·Captain: mikedeng1

A Theoretical Framework for the Pricing of Contingent Claims in the Presence of Model Uncertainty: Superreplication Price Equals a Supremum over Martingale Measures with Bracket BoundsResearch Paper

Motivation

Classical arbitrage pricing fixes one probabilistic model of the underlying asset and prices a contingent claim as an expectation under an equivalent martingale measure. When the volatility is not known, a seller who wants to be safe under every plausible model has to superreplicate: hold an initial capital and a trading strategy whose terminal value dominates the claim under all models at once. The uncertain volatility model (UVM) of Avellaneda, Levy and Parás (Appl. Math. Finance 1995) and Lyons (Appl. Math. Finance 1995) is the standard instance: the volatility is only known to lie in an interval $[\underline\sigma,\bar\sigma]$ .

The family of laws describing such uncertainty is not dominated by a single reference probability, so "almost surely" and the usual stochastic integral are not available. Denis and Martini (Ann. Appl. Probab. 2006) replace them by a capacity and a quasi-sure stochastic integral, and show that the superreplication price of a broad class of path-dependent European claims is a supremum of expectations over martingale laws. This framework is a precursor of quasi-sure analysis and $G$ -expectations (Denis, Hu and Peng, Potential Anal. 2011; Soner, Touzi and Zhang, Electron. J. Probab. 2011).

Setting

Fix $T>0$ . $\Omega$ is the space of continuous paths $B=(B_t)_{t\in[0,T]}$ with $B_0=0$ , with the uniform norm, Borel $\sigma$ -field $\mathcal B$ and canonical filtration $\mathcal F_t=\sigma(B_s:s\le t)$ . A martingale measure is a probability on $\Omega$ under which $B$ is an $(\mathcal F_t)$ -martingale; $\mathbf P_m$ denotes the set of these.

A nonzero measure $\bar\mu$ on $[0,T]$ with continuous distribution function $\bar\mu_t=\bar\mu([0,t])$ bounds the bracket. Hypothesis $H(\bar\mu)$ on a set $\mathbf P\subseteq\mathbf P_m$ says $d\langle B\rangle^P_t\le d\bar\mu_t$ for every $P\in\mathbf P$ ; $H(\underline\mu,\bar\mu)$ adds a lower bound $d\underline\mu_t\le d\langle B\rangle^P_t$ . In the UVM, $d\underline\mu=\underline\sigma^2dt$ and $d\bar\mu=\bar\sigma^2dt$ .

The capacity of a bounded continuous $\varphi$ is $c(\varphi)=\sup_{P\in\mathbf P}\|\varphi\|_{L^2(P)}$ , extended to all functions through lower semicontinuous majorants. A set is polar if its capacity is $0$ , and a property holds quasi-surely (q.s.) outside a polar set. $\mathcal L$ is the completion of $C_b(\Omega)$ under $c$ . Elementary integrands $h=\sum_i k_{t_i}\mathbb 1_{]t_i,t_{i+1}]}$ have integrals $I_T(h)=\sum_ik_{t_i}(B_{t_{i+1}}-B_{t_i})$ , and $\mathcal H$ is their completion for $\|h\|_{\mathcal H}=\sup_P(E_P\int_0^Th_s^2d\bar\mu_s)^{1/2}$ . $K=\{I_T(h):h\in\mathcal H\}$ is the space of attainable gains. The superreplication price of a claim $f$ is

\Lambda(f)=\inf\{a\in\mathbb R:\ \exists g\in K,\ a+g\ge f\ \text{q.s.}\}.

Formalization targets

Goal: Theorem 3.1 for explicit claims

Assume $H(\underline\mu,\bar\mu)$ and that $\bar\mu$ is Hölder continuous. There is a set $\mathbf P''\subset\mathbf P_m$ of martingale measures satisfying $H(\underline\mu,\bar\mu)$ such that

\Lambda(f)=\sup\{E_Pf:P\in\mathbf P''\}

for every bounded continuous $f$ of the form $F(B_{t_1},\dots,B_{t_d})$ , $G\big(\int_0^TF(B_s)ds\big)$ or $G(\sup_tB_t)$ , with $G$ (and the cylindrical $F$ ) bounded continuous. The goal leaves $\mathbf P''$ unspecified, as the paper does.

Milestones

In attack order: the transfer of a.s. inequalities to q.s. ones (Lemma A.7); the pathwise moment bound $(B_t-B_s)^{2n}\le\int_s^th\,dB+C\bar\mu(]s,t])^n$ q.s. (Proposition 2.9) and its price form $\Lambda((B_t-B_s)^{2n})\le C_{2n}\bar\mu([s,t])^n$ (Proposition 2.13); a universal bracket $\langle B\rangle_t\in\mathcal L$ (Lemma 2.10) approximated by realized variance (Lemma 2.14); weak duality $\Lambda(f)\ge\sup_{\mathbf P'}E_Pf$ (Lemma 2.15); the representation $\Lambda(f)=\sup_{Q\in\mathcal Q}E_Q\tilde f$ over probabilities on the Stone–Čech compactification $\tilde\Omega$ (§5, p. 19) and the Cauchy–Schwarz inequality for $\Lambda$ (Lemma 4.3); the martingale property and continuity of $\tilde B$ under each $Q$ (Proposition 5.2); the bracket bounds for the induced law $Q^*$ (Lemma 5.3); membership of the three claim families in the class $\Gamma$ of $f$ with $E_Q\tilde f=E_{Q^*}f$ (Lemmas 5.4–5.6); and Theorem 3.1 for the literal class $\Gamma$ .

Further statements: Theorem 6.1 (all martingale measures with $H(\underline\mu,\bar\mu)$ form a valid $\mathbf P''$ ), Proposition 3.2 (the case $\operatorname{dom}\Lambda=\mathcal L$ ), Proposition 2.12 (measures not charging polar sets inherit the bracket bounds), Theorem A.8 (closedness of $K$ under $H(a\bar\mu,\bar\mu)$ ).

Significance

The theorem identifies the cheapest model-free hedge of path-dependent European claims (cylindrical payoffs, Asian-type averages, lookbacks on the maximum) with a worst-case expectation over martingale laws obeying the same bracket bounds. Theorem 6.1 specializes it to the generalized UVM, where the dual set is all martingale measures with $d\underline\mu\le d\langle B\rangle\le d\bar\mu$ ; the paper notes this is new even for the Lebesgue case. The result supplies a rigorous non-dominated duality on which robust pricing bounds and $G$ -expectation pricing rest.

The theorem is proved in the paper; no part of it is machine-checked. A formalization would produce the first Lean development of a capacity on path space, of a quasi-sure stochastic integral, and of a continuous-time quadratic variation on the canonical space. These objects are absent from Mathlib, which has discrete- and continuous-time martingales, the Stone–Čech compactification and the Riesz–Markov–Kakutani theorem, but no stochastic integral.

Difficulty

The family $\mathbf P$ is not dominated, so neither the Itô integral of a single model nor a common null set is available: every inequality obtained under one $P$ by the Itô formula must be lifted to a quasi-sure one, and every limit taken in the capacity. The natural dual argument (Hahn–Banach on $\mathcal L$ ) produces linear forms whose representation as measures on $\Omega$ is not available because $\operatorname{dom}\Lambda$ need not be all of $\mathcal L$ . The paper's route works on bounded continuous claims and compactifies; the price is that the dual measures live on $\tilde\Omega$ , where $B_t$ is unbounded and must be extended by truncation, and the identity $E_Q\tilde f=E_{Q^*}f$ linking $\tilde\Omega$ back to $\Omega$ holds only for a class of claims that has to be checked family by family.

Formalization scope

$\Omega$ is a subtype of C(Set.Icc 0 T, ℝ) (paths with $B_0=0$ ) with the Borel $\sigma$ -field of the sup-norm topology. Distribution functions are continuous StieltjesFunctions vanishing at $0$ and positive at $T$ . The quadratic variation is a predicate: an adapted process with $P$ -a.s. continuous nondecreasing paths from $0$ such that $B^2-A$ is a martingale. The capacity takes values in $[0,\infty]$ with the Appendix's Lebesgue extension; q.s. means outside a set of capacity zero. $\mathcal L$ , $\mathcal H$ and $K$ are membership predicates on functions. $K$ is the image of the completion $\mathcal H$ . $\Lambda$ and every supremum are extended reals. $\tilde\Omega$ is Mathlib's StoneCech, and $\mathcal Q$ is the set of Borel probabilities on it dominated by $\Lambda$ on $C_b(\Omega)$ .

Standing assumptions, stated as hypotheses: $H(\bar\mu)$ on $\mathbf P$ for all §2 results, $H(\underline\mu,\bar\mu)$ where the page assumes it, and Hölder continuity of $\bar\mu$ for every result of §4–§5 and the goal (p. 12: "From now on, we assume that $\bar\mu$ is Hölder continuous"). The goal replaces the class $\Gamma$ , which is defined only inside the proof, by the three families of Lemmas 5.4–5.6. The literal form is a milestone. Lemma 2.14 adds $\mathbf P\neq\emptyset$ . Lemma 5.3 is stated for the law $Q^*$ on $\Omega$ .

The following trivializing formalizations are ruled out. An empty $\mathbf P$ with a real-valued $\Lambda$ would make the goal $0=0$ ; here both sides are $-\infty$ . Defining q.s. as "a.s. for every $P$ " would make Lemma A.7 a tautology. Replacing $K$ by the closure of elementary integrals would shrink $\Lambda$ . Dropping the martingale condition from the quadratic-variation predicate would make $H(\underline\mu,\bar\mu)$ satisfiable by any deterministic process.

A complete development needs Itô's formula and the Burkholder–Davis–Gundy inequalities for continuous martingales, Doob–Meyer uniqueness, a Kolmogorov continuity criterion, and the theory of regular Choquet capacities. These are reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

L. Denis and C. Martini, A theoretical framework for the pricing of contingent claims in the presence of model uncertainty, Ann. Appl. Probab. 16(2):827–852, 2006. arXiv:math/0607111v1. https://arxiv.org/abs/math/0607111
M. Avellaneda, A. Levy and A. Parás, Pricing and hedging derivative securities in markets with uncertain volatilities, Appl. Math. Finance 2(2):73–88, 1995. https://doi.org/10.1080/13504869500000005
T. J. Lyons, Uncertain volatility and the risk-free synthesis of derivatives, Appl. Math. Finance 2(2):117–133, 1995. https://doi.org/10.1080/13504869500000007
L. Denis, M. Hu and S. Peng, Function spaces and capacity related to a sublinear expectation: application to G-Brownian motion paths, Potential Anal. 34:139–161, 2011. https://doi.org/10.1007/s11118-010-9185-x
H. M. Soner, N. Touzi and J. Zhang, Quasi-sure stochastic analysis through aggregation, Electron. J. Probab. 16:1844–1879, 2011. https://doi.org/10.1214/EJP.v16-950

17 thms1 active userReviewed

Analysis Probability Stochastic Systems·Captain: mikedeng1

Law of Large Numbers Limits for Many-Server Queues 2: The Fluid Age Measure Converges to the Equilibrium Measure (1 − G(x))dxResearch Paper

Motivation

Large call centers, cloud server farms and hospital wards are modeled as many-server queues: $N$ identical servers, customers arriving according to a counting process, each customer served by one server for a random time drawn from a distribution $G$ , and customers who find all servers busy waiting in a first-come first-served queue. When $N$ is large, the number of customers is of order $N$ and the natural object of study is the fluid limit, obtained by dividing all quantities by $N$ and letting $N\to\infty$ . For exponential service times the fluid limit is a finite-dimensional ordinary differential equation. For a general service distribution — and call-center data show service times far from exponential (lognormal, in Brown et al., 2005) — the state must record how long each customer in service has been served, and the fluid limit is a measure-valued process.

Kaspi and Ramanan (Ann. Appl. Probab. 21 (2011) 33–114) characterize this limit by a pair of fluid equations for general $G$ with a density, prove that they have at most one solution, show that the scaled $N$ -server processes converge to it, and describe its long-time behavior. This mission is the last of these results: in the critically loaded fluid system, every solution converges to equilibrium.

Timeline. Whitt (2006) introduced a fluid model of the many-server queue with general service times and abandonment, and stated the case $\bar\lambda<1$ of property (1) of the goal theorem without proof (his Theorem 7.3). Kaspi and Ramanan (2011) gave the measure-valued formulation with the age process, uniqueness and existence of fluid solutions, and the convergence to equilibrium formalized here. Reed (2009) treated the related $G/GI/N$ queue in the Halfin–Whitt regime.

Setting

The service distribution $G$ has a density $g$ , is carried by $[0,\infty)$ , and has mean one: $\int_0^\infty x\,g(x)\,dx=\int_0^\infty(1-G(x))\,dx=1$ . Let $M=\sup\{x\ge0:G(x)<1\}\in(0,\infty]$ , and let $h=g/(1-G)$ be the hazard rate on $[0,M)$ .

The fluid state at time $t$ is a number $\bar X(t)\ge0$ , the scaled number of customers in system, and a measure $\bar\nu_t$ on $[0,M)$ of total mass at most one: $\bar\nu_t(A)$ is the scaled number of customers in service whose age (time already spent in service) lies in $A$ . The input is a nondecreasing càdlàg arrival function $\bar E$ with $\bar E(0)=0$ , an initial number $\bar X(0)$ and an initial age measure $\bar\nu_0$ , satisfying $1-\langle\mathbf 1,\bar\nu_0\rangle=[1-\bar X(0)]^+$ (servers are idle only when nobody waits). The set of such triples is $\mathcal S_0$ .

A càdlàg pair $(\bar X,\bar\nu)$ solves the fluid equations if the cumulative departures $\bar D(t)=\int_0^t\langle h,\bar\nu_s\rangle\,ds$ are finite, the entries into service $\bar K(t)=\langle\mathbf 1,\bar\nu_t\rangle-\langle\mathbf 1,\bar\nu_0\rangle+\bar D(t)$ satisfy the transport equation

\langle\varphi(\cdot,t),\bar\nu_t\rangle=\langle\varphi(\cdot,0),\bar\nu_0\rangle+\int_0^t\langle\varphi_x+\varphi_s,\bar\nu_s\rangle\,ds-\int_0^t\langle h\varphi(\cdot,s),\bar\nu_s\rangle\,ds+\int_{[0,t]}\varphi(0,s)\,d\bar K(s)

for every compactly supported test function $\varphi$ on $[0,M)\times[0,\infty)$ (ages grow at unit rate, customers leave at rate $h$ , new customers enter at age $0$ ), mass is conserved, $\bar X(t)=\bar X(0)+\bar E(t)-\bar D(t)$ , and the system is non-idling, $1-\langle\mathbf 1,\bar\nu_t\rangle=[1-\bar X(t)]^+$ .

The equilibrium measure is $\bar\nu_*(dx)=(1-G(x))\,dx$ on $[0,M)$ , a probability measure by the mean-one normalization. With $\bar E=\mathrm{id}$ (arrival rate equal to the total service capacity), $\bar X\equiv c\ge1$ and $\bar\nu\equiv\bar\nu_*$ is a constant solution. Assumption 2 asks that $h$ be bounded or lower semicontinuous near $M$ . The renewal measure of $G$ is $U=\sum_{n\ge0}G^{*n}$ , the unit mass at $0$ included.

Formalization targets

Goal: Theorem 3.9

Under Assumption 2:

if $\bar E=\bar\lambda\,\mathrm{id}$ with $\bar\lambda\in[0,1]$ and the system starts empty, then $\bar X(t)=\langle\mathbf 1,\bar\nu_t\rangle$ increases to $\bar\lambda$ and $\bar\nu_t$ increases weakly to $\bar\lambda\bar\nu_*$ ;
if $\int x^2g(x)\,dx<\infty$ , then for $\bar E=\mathrm{id}$ and every initial condition in $\mathcal S_0$ ,

\lim_{t\to\infty}\langle f,\bar\nu_t\rangle=\int_{[0,\infty)}f(x)(1-G(x))\,dx\qquad\text{for every bounded continuous }f.

Milestones

Lemma 3.4: a solution restarted at time $t$ solves the fluid equations for the shifted data.
Remark 3.8: the invariant solution $(c+\bar E-\mathrm{id},\bar\nu_*)$ when $\bar\lambda\ge1$ .
Corollary 4.4, (4.6): $\bar K$ is the renewal measure $U$ convolved with an explicit forcing term.
Proposition 6.1(1)–(3): the solution started empty, explicitly up to the first time $\tau_1$ it fills, its monotone convergence for constant $\bar\lambda\le1$ , and the comparison of an arbitrary solution with it.
Lemma 6.2: a reference system built from $U$ converges weakly to $\langle\mathbf 1,\pi_0\rangle\bar\nu_*$ .
Lemma 6.3: a uniform renewal estimate under a finite second moment.

Significance

Theorem 3.9(2) is the stability statement of the fluid model in the critically loaded case: whatever the initial occupancy and the initial ages, the age distribution of customers in service converges to the stationary excess distribution of $G$ . It justifies using $\bar\nu_*$ as the operating point around which diffusion approximations of many-server queues are built, and it is the fluid counterpart of the classical fact that the age of a stationary renewal process has density $1-G$ . Part (1) gives the transient behavior of an underloaded or critically loaded system started empty.

The result is proved in the paper; nothing here is open. To our knowledge none of it has been formalized. A formalization adds machine-checked statements of a measure-valued fluid model that the companion mission (uniqueness of fluid solutions, Theorem 3.5) shares, and exercises renewal theory — the renewal measure, a key renewal theorem for laws with a density, Lorden's inequality — in a form usable by other queueing developments.

Difficulty

The naive argument would show that $\langle f,\bar\nu_t\rangle$ is given by an explicit formula and pass to the limit. The explicit age representation of a solution involves $\bar K$ , which is known only through a renewal equation whose forcing term depends on $\bar\nu$ itself; there is no closed form unless the system never fills up. For $\bar E=\mathrm{id}$ the system can alternate between full and not full, and the convergence must be proved without knowing when. Two ingredients carry the weight: a comparison showing that the occupancy tends to one, and a key renewal theorem for the backward recurrence time of a renewal process with a density, which needs total-variation rather than vague convergence because the test functions are only bounded and continuous. The uniform-in-time control of Lemma 6.3 is where the second moment enters.

Formalization scope

Everything lives in ManyServerFluid.Equilibrium. The service law is a structure holding the density $g$ with $g\ge0$ , $g=0$ on $(-\infty,0)$ , $\int g=1$ , and mean one. Time is $\mathbb R$ , read on $[0,\infty)$ . Age measures are Mathlib FiniteMeasure ℝ carried by $[0,M)$ , with the weak topology, so "càdlàg" is in the paper's topology. The departures $\int_0^t\langle h,\bar\nu_s\rangle ds$ are lower integrals in $[0,\infty]$ ; $d\bar K$ and $dZ$ are Lebesgue–Stieltjes measures. The convolution powers are the published QueueingFundamentals.MG1.convPow.

Explicit choices, each also stated in the item that uses it:

$g=0$ below $0$ and $\int g=1$ are explicit; the paper's " $\bar\nu_0$ " is $\bar\nu(0)$ , stated as an equation.
Compact support of test functions is relative to $[0,M)\times\mathbb R_+$ , as the paper intends; the directional derivative is supplied as a second function.
Weak convergence is tested on bounded continuous functions on $\mathbb R$ ; for measures carried by $[0,M)$ this is equivalent to $\mathcal C_b[0,M)$ and $\mathcal C_b(\mathbb R_+)$ . "Increases" means nondecreasing.
"The unique solution" is the hypothesis "a solution"; uniqueness is the companion mission.
In Proposition 6.1(1) the printed limit $\int_0^{\tau_1}f(t-s)\cdots$ is read with $\tau_1$ for $t$ , and only for $\tau_1<\infty$ .
In Lemma 6.3 the free $t$ of (6.11) is quantified after $\exists T_\varepsilon$ , uniformly, as the proof establishes and uses.
Lemma 6.2 states that $Z\in\mathcal I_0$ and that a càdlàg family satisfying (6.6) exists, besides (6.7).
Remark 3.8 is stated as membership in the solution set, the conclusion the paper draws.

Weak convergence in Theorem 3.9(2) is against all bounded continuous functions, not compactly supported ones; vague convergence would let mass escape towards $M$ and is not the theorem. The monotonicity in part (1) is part of the statement. A formalization in which these were dropped, or in which $U$ omitted the unit mass at $0$ , would state a different result.

Existence. The paper's proof of Theorem 3.9(2) compares an arbitrary solution with the solution started empty, which it obtains from its Theorem 3.7 (existence via the $N$ -server limit); that theorem is not part of this series. Here every solution is a hypothesis, so nothing false is stated, but a proof of the goal must construct the empty-start solution for $\bar E=\mathrm{id}$ . It is explicit: $\bar\nu_t$ has density $1-G$ on $[0,t]$ while $t<\tau_1$ , and from $\tau_1=M<\infty$ on it equals $\bar\nu_*$ (Proposition 6.1, Remark 3.8, Lemma 3.4).

Contributions welcome: general renewal theory (local finiteness of $U$ , Lorden's inequality, the key renewal theorem for spread-out laws in total variation), and lemmas on the fluid equations shared with the uniqueness mission (the monotonicity of $\bar K$ , the renewal equation (4.5), the age representation (3.11)).

Selected references

H. Kaspi and K. Ramanan, Law of Large Numbers Limits for Many-Server Queues, Ann. Appl. Probab. 21(1) (2011) 33–114. https://doi.org/10.1214/09-AAP662
W. Whitt, Fluid Models for Multiserver Queues with Abandonments, Oper. Res. 54 (2006) 37–54. https://mathscinet.ams.org/mathscinet-getitem?mr=2201245
L. Brown, N. Gans, A. Mandelbaum, A. Sakov, H. Shen, S. Zeltyn and L. Zhao, Statistical analysis of a telephone call center: A queueing-science perspective, J. Amer. Statist. Assoc. 100 (2005) 36–50. https://mathscinet.ams.org/mathscinet-getitem?mr=2166068
J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Ann. Appl. Probab. 19 (2009) 2211–2269. https://mathscinet.ams.org/mathscinet-getitem?mr=2588244
S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003. https://mathscinet.ams.org/mathscinet-getitem?mr=1978607

13 thms1 active userReviewed

Dynamic Programming Optimization Probability·Captain: mikedeng1

Robust Dynamic Programming 1: The Robust Bellman Recursion and Optimality of Deterministic Markov Policies in Finite HorizonResearch Paper

Motivation

Markov decision processes assume that the transition law is known exactly. In practice it is estimated from data, and the optimal policy computed for the point estimate can perform badly when the true law differs. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. The worst case is taken against an adversary (nature) who may choose a law from the set at every step.

For this worst case to be computable by backward induction, the set of path measures of a policy has to decompose epoch by epoch. Garud Iyengar named this property Rectangularity and proved that under it the classical finite horizon theory carries over: a robust Bellman equation holds, and deterministic Markov policies are optimal among all history dependent randomized policies, with state and action sets that may be countably infinite and ambiguity sets that need not be convex (Iyengar, CORC Tech Report TR-2002-07, rev. 2004; published in Math. Oper. Res. 30(2), 2005).

Timeline:

1973: Satia and Lave study Markov decision processes with uncertain transition probabilities, finite states and actions (Oper. Res. 21(3)).
2001: Epstein and Schneider axiomatize recursive multiple priors, the decision-theoretic origin of rectangular ambiguity (J. Econ. Theory 113, working paper 2001).
2002–2005: Nilim and El Ghaoui give a robust counterpart of the Bellman recursion for finite state and action spaces and convex ambiguity sets, against Markov controllers (Oper. Res. 53(5)).
2002–2005: Iyengar proves the robust Bellman equation and Markov optimality for countable spaces, arbitrary ambiguity sets and all history dependent randomized policies, under Rectangularity.

Setting

A finite horizon ambiguous Markov decision process (AMDP) has decision epochs $t \in T = \{0,\dots,N-1\}$ , $N\ge 1$ , and a terminal epoch $N$ . States lie in a countable set $\mathcal S$ and actions in a countable set $\mathcal A$ . In state $s$ at epoch $t$ the admissible actions form a nonempty set $\mathcal A_t(s)$ . For each admissible action $a$ , the next state is drawn from some probability measure $p \in \mathcal P_t(s,a)$ , where $\mathcal P_t(s,a)$ is a nonempty set of probability measures on $\mathcal S$ , the ambiguity set. The decision maker receives $r_t(s,a,s')$ when $a$ is taken in $s$ and the next state is $s'$ , and $r_N(s)$ at the terminal epoch.

A history at epoch $n$ is $h_n=(s_0,a_0,\dots,s_{n-1},a_{n-1},s_n)$ . A policy $\pi=(d_t)$ assigns to each history $h_t$ a probability measure $d_t(h_t)$ on $\mathcal A_t(s_t)$ . It is deterministic ( $\Pi_D$ ) if every $d_t(h_t)$ is a point mass, and deterministic Markov ( $\Pi_{MD}$ ) if moreover the chosen action depends on the current state $s_t$ alone. $\Pi$ denotes all history dependent randomized policies.

Under Rectangularity (Assumption 1), the set $\mathcal T^\pi$ of path measures consistent with $\pi$ is a product of one-epoch sets: nature chooses, for every epoch $t$ , every history $h_t$ and every admissible action $a$ , a measure $p_{h_t,a}\in\mathcal P_t(s_t,a)$ , and the path measure is $\mathbf P(h_N)=\prod_t d_t(h_t)(a_t)\,p_{h_t,a_t}(s_{t+1})$ . The robust value of $\pi$ from $h_n$ and the robust value function are

V^\pi_n(h_n)=\inf_{\mathbf P\in\mathcal T^\pi_n}E^{\mathbf P}\Big[\sum_{t=n}^{N-1}r_t(s_t,a_t,s_{t+1})+r_N(s_N)\Big],\qquad V^*_n(h_n)=\sup_{\pi\in\Pi}V^\pi_n(h_n).

The optimistic values $\bar V^\pi_n$ , $\bar V^*_n$ replace the infimum over $\mathcal T^\pi_n$ by a supremum.

Formalization targets

Goal: Theorem 2 (Markov optimality)

For $n=0,\dots,N$ , $V^*_n(h_n)$ depends on $h_n$ only through $s_n$ ; for $n\in T$ , $V^*_n(s_n)=\sup_{\pi\in\Pi_{MD}}V^\pi_n(s_n)$ ; and

V^*_n(s)=\sup_{a\in\mathcal A_n(s)}\ \inf_{p\in\mathcal P_n(s,a)}E^p\big[r_n(s,a,s')+V^*_{n+1}(s')\big],\qquad n\in T. \tag{16}

Milestones

Proof of Theorem 1, eq. (15): at one epoch, randomizing over actions does not raise the worst-case value, and the adversary may choose its measure separately per action.
Theorem 1 (Bellman equation): $V^*_N(h_N)=r_N(s_N)$ and $V^*_n(h_n)=\sup_{a}\inf_{p\in\mathcal P_n(s_n,a)}E^p[r_n(s_n,a,s)+V^*_{n+1}(h_n,a,s)]$ (11).
Corollary 1: $V^*_n(h_n)=\sup_{\pi\in\Pi_D}V^\pi_n(h_n)$ for $n\in T$ .
Theorem 3: the optimistic analogue of Theorem 2, with recursion (18) in which both the outer and the inner optimizations are suprema.

The mission also contains, as a draft theorem that is not a milestone, the per-policy identity of the proof of Theorem 1, eq. (12): for each policy, $V^\pi_n(h_n)=\inf_{p\in\mathcal T^{d_n}}E^p[r_n+V^\pi_{n+1}(h_n,a_n,s_{n+1})]$ .

Significance

Theorem 2 is the basis of robust dynamic programming in finite horizon: computing an optimal robust policy reduces to $N$ backward passes, each a family of one-stage problems $\inf_{p\in\mathcal P_n(s,a)}E^p[v]$ . It also justifies restricting attention to deterministic Markov policies, which is what every algorithm in the robust MDP literature computes. Theorem 1 isolates the role of Rectangularity: without it the worst case over path measures does not decompose and the recursion characterizes nothing.

The results are proved on paper; no machine-checked proof is known. The platform holds the finite-state, Markov-controller special case (the Nilim–El Ghaoui RobustMDP series, posed, not proved), whose comparison class is too small to express the claim $\Pi_{MD}$ suffices against $\Pi$ . A formal proof here supplies the history dependent policy and adversary machinery on countable spaces that the discounted robust theory and the robust MDP literature reuse.

Difficulty

The obvious argument writes the robust value as an inf–sup over path measures and pushes the infimum inside the expectation epoch by epoch. That step is the content of (12): the infimum of an expectation equals the expectation of an infimum only because nature's continuation choice may depend on the realized action and next state, so near-worst continuations for different branches can be glued into one admissible adversary. Infima need not be attained (the ambiguity sets are arbitrary, the state set countable), so the gluing is an $\epsilon$ -argument over countably many branches. The supremum over policies needs a matching splicing of $\epsilon$ -optimal continuation policies (13)–(14). Finally, randomized decision rules must be eliminated (15), which uses Rectangularity again, now per action. Restricting either the policies or the adversary to Markov ones from the start is not allowed: it changes the comparison class and makes the goal circular.

Formalization scope

One countable state type S and one countable action type A serve all epochs; the page's epoch-dependent sets $\mathcal S_t$ embed into their disjoint union. Epochs are 0-based natural numbers, with terminal epoch M.N and 1 ≤ N.
A history at epoch $n$ is (Fin n → S × A) × S. Probability measures are PMF; $E^p[f]=\sum_s p(s)f(s)$ as a tsum. The expected reward under a policy and an adversary is computed by backward iterated sums, which is the expectation under the product path measure (3).
A policy is a decision rule for every epoch, admissible for t < N; the supremum over $\Pi$ equals that over the page's $\Pi_n$ because $V^\pi_n$ uses only $d_n,\dots,d_{N-1}$ . An adversary chooses $p_{h_t,a}\in\mathcal P_t(s_t,a)$ for every epoch, history and admissible action.
Added and implicit hypotheses: $\mathcal A_t(s)\neq\emptyset$ and $\mathcal P_t(s,a)\neq\emptyset$ (implicit on the page), and a uniform bound $|r_t|\le R$ , $|r_N|\le R$ (added: Section 2 states none, but with countable states the expectations and the real suprema and infima need it). All values then lie in a bounded interval, so no supremum or infimum is a junk value.
Ambiguity sets are arbitrary nonempty sets of measures: no convexity, closedness or attainment is assumed anywhere.
" $V^*_n$ is a function of the current state alone" is stated as the existence of $W(n,s)$ with $V^*_n(h_n)=W(n,s_n)$ ; the value is not defined on states, which would hide the claim. The notation $V^\pi_n(s_n)$ for Markov policies is made explicit as a clause.
Ruled out: restricting $\Pi$ or the adversary to Markov or stationary objects, a static adversary that fixes one $p$ per $(s,a)$ for the whole horizon, and suprema over unbounded or empty families; each makes some target false or trivial.

Definitions: AMDP, History, History.extend, IsPolicy, Policy, IsDeterministic, IsDetMarkov, Adversary, Selection, expect, expTail, expectedReward, V, Vstar, Vbar, VbarStar, all in RobustDP.FiniteHorizon. Lemmas about gluing adversaries along history prefixes and about suprema of bounded families indexed by subtypes are reusable. Contributions to any milestone are welcome, in any order; (15) is a one-epoch statement independent of the rest.

Selected references

G. Iyengar, Robust dynamic programming, CORC Tech Report TR-2002-07, Columbia University, revised May 4, 2004; Math. Oper. Res. 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Oper. Res. 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
J. K. Satia and R. E. Lave, Markovian decision processes with uncertain transition probabilities, Oper. Res. 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
L. G. Epstein and M. Schneider, Recursive multiple-priors, J. Econ. Theory 113(1):1–31, 2003. https://doi.org/10.1016/S0022-0531(03)00097-8
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

7 thms1 active userReviewed

Optimization Probability·Captain: mikedeng1

Stability of Multistage Stochastic Programs: Optimal Values Are Locally Lipschitz in the L_r Distance of the Inputs plus a Filtration DistanceResearch Paper

Motivation

A multistage stochastic program chooses decisions $x_1, \dots, x_T$ over $T$ time periods while a random input $\xi_1, \dots, \xi_T$ is revealed one stage at a time; the decision at stage $t$ may use what has been observed so far and nothing more. Such models are used for capacity expansion, hydro-thermal power scheduling, asset–liability management and production planning. In practice the true input process is never used directly: it is replaced by an estimate, a discretization or a scenario tree with few branches, and the program is solved for that approximation. Whether the optimal value of the approximate program is close to the true one is therefore the basic question behind every scenario-tree method.

For two-stage programs ( $T = 2$ ) the answer is classical: the optimal value is Lipschitz continuous with respect to suitable distances of probability distributions (Rachev and Römisch, 2002). For $T > 2$ that methodology breaks down, because the multistage objective depends on conditional expectations given the past, and hence on the information structure of the input, not only on its distribution. Heitsch, Römisch and Strugarek (SIAM J. Optim. 2006) showed that the gap is closed by adding one more term: a distance between the filtrations generated by the true and the approximate inputs. Their estimate is the basis of later work on scenario-tree construction and on the nested distance of Pflug and Pichler.

Setting

Let $(\Omega, \mathcal F, \mathbb P)$ be a probability space and $\xi = (\xi_1, \dots, \xi_T)$ a process with $\xi_t \in \mathbb R^d$ . The information available at stage $t$ is $\xi^t = (\xi_1, \dots, \xi_t)$ , and $\mathcal F_t = \sigma(\xi^t)$ is the σ-field it generates; $\xi_1$ is deterministic, so $\mathcal F_1 = \{\emptyset, \Omega\}$ . The linear multistage program (1) is

v(\xi) = \inf\Big\{ \mathbb E\Big[\sum_{t=1}^T \langle b_t(\xi_t), x_t\rangle\Big] \;:\; x_t \in X_t,\ x_t \ \mathcal F_t\text{-measurable},\ A_{t,0}x_t + A_{t,1}x_{t-1} = h_t(\xi_t)\ (t \ge 2) \Big\},

where $X_1 \subseteq \mathbb R^{m_1}$ is a polyhedron, $X_t \subseteq \mathbb R^{m_t}$ for $t \ge 2$ are polyhedral cones, $A_{t,0}$ and $A_{t,1}$ are fixed matrices, and the costs $b_t$ and right-hand sides $h_t$ are affine functions of the current input $\xi_t$ . Write $F(\xi, x)$ for the objective and $\mathcal X(\xi)$ for the feasible set.

Which data are random fixes two integrability exponents: if only the costs are random, $r = 1$ and $r' = \infty$ ; if only the right-hand sides are random, $r = r' = 1$ ; otherwise $r = r' = 2$ . The input lives in $L_r$ and the decisions in $L_{r'}$ , and $\|\xi - \tilde\xi\|_r$ is the $L_r$ distance of two inputs.

Three conditions are imposed: (A1) complete fixed recourse, $A_{t,0}X_t = \mathbb R^{n_t}$ for $t \ge 2$ ; (A2) $v(\xi)$ is finite and $F$ is level-bounded locally uniformly at $\xi$ : for some $\alpha > 0$ there are $\delta > 0$ and a bounded set $B \subseteq L_{r'}$ such that the level set $l_\alpha(F(\tilde\xi, \cdot)) = \{\tilde x \in \mathcal X(\tilde\xi) : F(\tilde\xi, \tilde x) \le v(\xi) + \alpha\}$ is nonempty and contained in $B$ whenever $\|\tilde\xi - \xi\|_r \le \delta$ ; (A3) $\xi \in L_r$ .

The filtration distance at stage $t$ compares how well a near-optimal decision of one problem is predicted from the other problem's information:

D_t(\mathcal F_t, \tilde{\mathcal F}_t) = \max\Big\{ \sup_{x \in l_\alpha(F(\xi,\cdot))} \|x_t - \mathbb E[x_t \mid \tilde{\mathcal F}_t]\|_{r'},\ \sup_{\tilde x \in l_\alpha(F(\tilde\xi,\cdot))} \|\tilde x_t - \mathbb E[\tilde x_t \mid \mathcal F_t]\|_{r'} \Big\}.

Formalization targets

Goal: Theorem 2.1

Under (A1)–(A3) and boundedness of $X_1$ there are positive constants $L$ , $\alpha$ , $\delta$ such that

|v(\xi) - v(\tilde\xi)| \le L\Big( \|\xi - \tilde\xi\|_r + \sum_{t=2}^{T-1} D_t(\mathcal F_t, \tilde{\mathcal F}_t) \Big)

for every input $\tilde\xi \in L_r$ with $\|\tilde\xi - \xi\|_r \le \delta$ and $v(\tilde\xi)$ finite. The constants are existential: the theorem asserts the shape of the estimate, not its numerical values.

Milestones

(10): the maps $M_t(u) = \{x \in X_t : A_{t,0}x = u\}$ are Lipschitz in the Hausdorff sense.
(11): every feasible policy for $\xi$ can be transferred to a feasible policy for $\tilde\xi$ , adapted to $\tilde{\mathcal F}_t$ , with a pointwise error bound whose constants do not depend on $\tilde\xi$ .
The three case estimates of $v(\tilde\xi) - v(\xi)$ : only right-hand sides random, only costs random, and $r = r' = 2$ .
(14) and (15): the two one-sided estimates, whose sum of filtration terms is bounded by $\sum_t D_t$ .

Significance

The theorem identifies what an approximation of a multistage input must preserve: closeness in $L_r$ alone is not enough, and the filtration term measures exactly the information that is lost or gained. It justifies scenario-tree construction by forward selection and reduction (Heitsch and Römisch, 2009), where both terms are controlled, and it is the precursor of the nested distance, for which analogous Lipschitz bounds are proved. Without such an estimate a scenario tree that matches the marginal distributions can still give an arbitrarily wrong optimal value.

The result is proved in the paper; it has not been formalized. A machine-checked version needs, and would produce, a formal theory of linear programs with decisions adapted to a generated filtration in $L_p$ spaces, Lipschitz continuity of polyhedral set-valued maps, and measurable selections of conditional-expectation projections. Each of these is reusable well beyond this paper.

Difficulty

The obvious argument — take a near-optimal policy for $\xi$ and evaluate it for $\tilde\xi$ — fails at once: that policy is adapted to $\mathcal F_t$ , not to $\tilde{\mathcal F}_t$ , so it is not feasible for the perturbed problem, and projecting it by conditional expectation onto $\tilde{\mathcal F}_t$ destroys the equality constraints. Any repaired policy must again be $\tilde{\mathcal F}_t$ -measurable at every stage, and an error made at stage $t$ propagates to all later stages through the recursion $A_{t,0}x_t + A_{t,1}x_{t-1} = h_t(\xi_t)$ , where it must stay controlled in the right $L_{r'}$ norm. The three integrability regimes need separate estimates; in the regime $r' = \infty$ the error must be bounded essentially, not only on average.

Formalization scope

The program is encoded in a single definitions file. Stages are natural numbers $1, \dots, T$ with dimension functions $m_t$ , $n_t$ . $X_1$ is given by finitely many linear inequalities and each $X_t$ , $t \ge 2$ , by finitely many homogeneous ones, so "polyhedral" and "polyhedral cone" are built in. The matrices are linear maps between Euclidean spaces; $b_t(y) = b_t^0 + B_t y$ and $h_t(y) = h_t^0 + H_t y$ . A randomness pattern (costs, rhs, both) carries the exponents $(r, r')$ and its restriction on the data: $H_t = 0$ for costs, $B_t = 0$ for rhs, none for both.

The committed conventions are:

$\mathcal F_t$ is the σ-field generated by $\xi_1, \dots, \xi_t$ ; conditional expectations are Mathlib's condExp;
an admissible input is measurable, in $L_r$ stage by stage, and has a deterministic first component; nothing assumes $\tilde\xi_1 = \xi_1$ or $\mathcal F_T = \mathcal F$ ;
a feasible policy has deterministic $x_1 \in X_1$ , $\mathcal F_t$ -measurable $x_t$ satisfying the constraints almost surely, and every $x_t$ in $L_{r'}$ ;
$\|\xi - \tilde\xi\|_r$ uses the Euclidean norm on $\mathbb R^{Td}$ ; "bounded in $L_{r'}$ " is read componentwise, which is equivalent;
optimal values are extended reals ( $+\infty$ when infeasible); norms, suprema and the estimate are stated in $[0, \infty]$ , so no default value of a partial operation enters;
both level sets in $D_t$ use the threshold $v(\xi) + \alpha$ , as (A2) defines them.

Trivializing formalizations are ruled out: the constants $L$ , $\alpha$ , $\delta$ are quantified before $\tilde\xi$ ; the theorem covers all three randomness patterns; the level sets are nonempty, so the suprema are not vacuous; and a sorry-free check exhibits data satisfying (A1) with a feasible policy, so the hypotheses are satisfiable.

Contributions are welcome on Lipschitz continuity of polyhedral set-valued maps (Walkup–Wets), measurable selections, conditional expectation of set-constrained random vectors, and any of the case estimates.

Selected references

H. Heitsch, W. Römisch, C. Strugarek, Stability of multistage stochastic programs, SIAM J. Optim. 17 (2006) 511–525. https://doi.org/10.1137/050632865 (formalized from the authors' manuscript, edoc.hu-berlin.de)
S. T. Rachev, W. Römisch, Quantitative stability in stochastic programming: the method of probability metrics, Math. Oper. Res. 27 (2002) 792–818. https://doi.org/10.1287/moor.27.4.792.304
R. T. Rockafellar, R. J-B Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
D. W. Walkup, R. J-B Wets, A Lipschitzian characterization of convex polyhedra, Proc. Amer. Math. Soc. 23 (1969) 167–173. https://doi.org/10.1090/S0002-9939-1969-0246200-8
H. Heitsch, W. Römisch, Scenario tree modeling for multistage stochastic programs, Math. Program. 118 (2009) 371–406. https://doi.org/10.1007/s10107-007-0197-2
G. Ch. Pflug, A. Pichler, A distance for multistage stochastic optimization models, SIAM J. Optim. 22 (2012) 1–23. https://doi.org/10.1137/110825054

9 thms1 active userReviewed

Optimization·Captain: mikedeng1

Theoretical and Numerical Comparison of Relaxation Methods for Mathematical Programs with Complementarity Constraints 2: MPEC-MFCQ Implies MFCQ for the Scholtes Relaxed Problems LocallyResearch Paper

Motivation

A mathematical program with complementarity constraints (MPEC, also called MPCC) is a nonlinear program in which some pairs of constraint functions must be nonnegative with at least one of each pair equal to zero. Such programs model bilevel optimization, Stackelberg games, contact problems in mechanics, and traffic equilibrium design; see Luo, Pang and Ralph, Mathematical Programs with Equilibrium Constraints (Cambridge University Press, 1996). The complementarity constraints make every standard constraint qualification of nonlinear programming fail at every feasible point: neither LICQ nor MFCQ ever holds. Off-the-shelf NLP theory and solvers therefore do not apply directly.

Relaxation methods work around this by replacing the MPEC with a family of ordinary nonlinear programs indexed by a parameter $t>0$ and letting $t\downarrow0$ . The oldest of these is the global relaxation of Scholtes (SIAM J. Optim. 11, 2001). The relaxed programs are only useful if they are themselves well posed: a local minimizer of a relaxed program should carry Lagrange multipliers, so that the sequence of KKT points the method computes actually exists. Hoheisel, Kanzow and Schwartz (Preprint 299, Univ. Würzburg, 2010; published in Mathematical Programming) compare five relaxation schemes, prove convergence under weaker MPEC constraint qualifications than before, and ask which standard constraint qualification the relaxed programs satisfy. This mission formalizes their answer for Scholtes' scheme, Theorem 3.2.

Setting

A standard nonlinear program (2) on $\mathbb R^n$ minimizes $f(x)$ subject to $g_i(x)\le0$ and $h_j(x)=0$ for finitely many $i$ and $j$ . At a feasible $x$ , the active set is $I_g(x)=\{i\mid g_i(x)=0\}$ . A family $\{\nabla g_i(x)\mid i\in I_1\}\cup\{\nabla h_j(x)\mid j\in I_2\}$ is positive-linearly dependent if some combination $\sum\alpha_i\nabla g_i(x)+\sum\beta_j\nabla h_j(x)$ vanishes with $\alpha_i\ge0$ and not all coefficients zero. The Mangasarian–Fromovitz constraint qualification (MFCQ) holds at $x$ if the gradients $\nabla h_j(x)$ are linearly independent and some direction $d$ has $\nabla g_i(x)^Td<0$ for every active $i$ and $\nabla h_j(x)^Td=0$ for every $j$ .

The MPEC (1) minimizes $f(x)$ subject to

g_i(x)\le0\ (i\le m),\quad h_i(x)=0\ (i\le p),\quad G_i(x)\ge0,\ H_i(x)\ge0,\ G_i(x)H_i(x)=0\ (i\le l),

with continuously differentiable data. At a feasible point $x^*$ the indices of the complementarity pairs split into $I_{0+}$ ( $G_i=0<H_i$ ), $I_{00}$ ( $G_i=H_i=0$ ) and $I_{+0}$ ( $G_i>0=H_i$ ). The tightened program TNLP $(x^*)$ replaces each pair by equalities on the components that vanish at $x^*$ and a sign constraint on the other. MPEC-MFCQ holds at $x^*$ if standard MFCQ holds for TNLP $(x^*)$ at $x^*$ .

Scholtes' relaxed program $R^S(t)$ , for $t>0$ , keeps $g_i\le0$ , $h_j=0$ , $G_i\ge0$ , $H_i\ge0$ and replaces $G_iH_i=0$ by $G_i(x)H_i(x)\le t$ . Its feasible set is $X^S(t)$ . Lean notation: the MPEC is MPEC n m p l, TNLP $(x^*)$ is P.TNLP xs, $R^S(t)$ is P.RS t, and MFCQ of an NLP Q at x is Q.IsMFCQ x.

Formalization targets

Goal: Theorem 3.2

If $x^*$ is feasible for the MPEC and MPEC-MFCQ holds at $x^*$ , there are a neighbourhood $N$ of $x^*$ and $\bar t>0$ such that

\text{standard MFCQ for } R^S(t) \text{ holds at every } x\in N\cap X^S(t).

The neighbourhood is fixed before $t$ and works for every $t>0$ .

Milestones, in attack order

Remark 2.2. MFCQ at a feasible point of an NLP is equivalent to positive-linear independence of the active inequality gradients together with all equality gradients.
MPEC-MFCQ at $x^*$ , rewritten as positive-linear independence of $\{\nabla g_i(x^*)\}_{I_g}$ (sign-constrained) together with $\{\nabla h_i(x^*)\}$ , $\{\nabla G_i(x^*)\}_{I_{00}\cup I_{0+}}$ and $\{\nabla H_i(x^*)\}_{I_{00}\cup I_{+0}}$ (free).
Persistence: the same family, with gradients evaluated at $x$ , stays positive-linearly independent for all $x\in X^S(t)$ near $x^*$ .
(6): near $x^*$ , the active sets of $R^S(t)$ at $x$ are contained in the corresponding index sets at $x^*$ , and the product constraint is never active together with $G_i\ge0$ or $H_i\ge0$ .
(7): near $x^*$ , the active-constraint gradients of $R^S(t)$ , regrouped by the index sets at $x^*$ , form a positive-linearly independent family.

Significance

Theorem 3.2 says that the relaxed programs inherit a standard constraint qualification from the MPEC. Consequently every local minimizer of $R^S(t)$ near $x^*$ is a KKT point, which is exactly the hypothesis of the convergence theorem for Scholtes' method (Theorem 3.1 of the paper: limits of KKT points of $R^S(t_k)$ are C-stationary under MPEC-MFCQ). Without it, the convergence theorem could be about sequences that do not exist. The result also replaces the MPEC-LICQ-based regularity results of earlier work by the weaker MPEC-MFCQ.

The theorem is proved in the paper; to our knowledge no part of this theory has been machine-checked. A formal development delivers a reusable layer for nonlinear programming in Lean: positive-linear dependence, MFCQ and its dual characterization, the tightened program of an MPEC and the MPEC constraint qualifications. Sibling missions of this series formalize Theorem 3.1 and the Kadrani–Dussault–Benchakroun relaxation (Theorem 3.5) on the same vocabulary.

Difficulty

The obvious argument is a continuity argument: MFCQ is an open condition, so it should persist near $x^*$ . This fails as stated, because MFCQ for $R^S(t)$ is not a perturbation of MFCQ for TNLP $(x^*)$ : the two programs have different constraints, and the active set of $R^S(t)$ at $x$ changes with $x$ and $t$ . Near a biactive index $i\in I_{00}$ , the product constraint $G_iH_i\le t$ can be active, and its gradient $G_i\nabla H_i+H_i\nabla G_i$ tends to zero as $x\to x^*$ . So it cannot be treated as a small perturbation of any gradient in the TNLP family. In addition, the neighbourhood must be uniform in $t$ , while the active product constraints depend on $t$ . The step that needs care is the regrouping of the multiplier equation of $R^S(t)$ into a combination of TNLP-type gradients, with every coefficient's sign accounted for. The separate step from MPEC-MFCQ to positive-linear independence needs a theorem of the alternative (Motzkin's transposition theorem), which is not in Mathlib in this form.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $\nabla f(x)^Td$ is the inner product of gradient f x with d. Indices $1,\dots,m$ are Fin m (0-based), and $m,p,l=0$ are allowed.
The standing assumption of p. 1 (all data $C^1$ ) is the explicit hypothesis P.IsC1 on the goal and on milestones 3–5. Milestones 1–2 do not need it.
Families of gradients are indexed families, not sets: a repeated vector makes a family linearly dependent.
Definition 2.1's "not all of them being zero" is read as "not all of the $\alpha_i$ and $\beta_j$ are zero".
TNLP $(x^*)$ uses subtype index types, so only the constraints the paper lists exist. Absent constraints are not padded with the zero function, which would be active with zero gradient and would destroy MFCQ.
"Standard MFCQ for $R^S(t)$ " is the MFCQ of the NLP $R^S(t)$ with its own active set, including the product constraint when $G_i(x)H_i(x)=t$ .
The paper introduces $\bar t>0$ and never uses it. The statement keeps $\bar t$ and quantifies over every $t>0$ , which is what the proof shows. The neighbourhood is a set in 𝓝 xs chosen before $t$ .
In (7), the sixth vector is printed as $G_i\nabla H_i+G_i\nabla H_i$ , a misprint for $G_i\nabla H_i+H_i\nabla G_i$ . The sign constraint applies to the $\nabla g_i$ only, as in the preceding display; this is the reading the paper's last step requires.
Persistence (milestone 3) is stated, as printed, for $x\in X^S(t)$ close to $x^*$ , with one neighbourhood of $x^*$ serving every $t>0$ .

The goal would be trivialized by a weakened MFCQ, for instance one that omits the linear independence of the equality gradients or requires the strict inequality only for some of the active constraints. Such a formalization is ruled out: IsMFCQ requires both conditions, over the full active set of $R^S(t)$ . The neighbourhood must be a genuine element of 𝓝 xs, so an empty $N$ is excluded.

Welcome contributions: a proof of Remark 2.2, general lemmas on persistence of positive-linear independence under continuous perturbation, and the final assembly. These lemmas apply to nonlinear programming in general, not only to this mission.

Selected references

T. Hoheisel, C. Kanzow, A. Schwartz, Theoretical and numerical comparison of relaxation methods for mathematical programs with complementarity constraints, Preprint 299, Institute of Mathematics, University of Würzburg, 2010; Mathematical Programming 137 (2013) 257–288. https://doi.org/10.1007/s10107-011-0488-5
S. Scholtes, Convergence properties of a regularization scheme for mathematical programs with complementarity constraints, SIAM Journal on Optimization 11 (2001) 918–936. https://doi.org/10.1137/S1052623499361233
L. Qi, Z. Wei, On the constant positive linear dependence condition and its application to SQP methods, SIAM Journal on Optimization 10 (2000) 963–981. https://doi.org/10.1137/S1052623497326629
Z.-Q. Luo, J.-S. Pang, D. Ralph, Mathematical Programs with Equilibrium Constraints, Cambridge University Press, 1996. https://doi.org/10.1017/CBO9780511983658
O. L. Mangasarian, S. Fromovitz, The Fritz John necessary optimality conditions in the presence of equality and inequality constraints, Journal of Mathematical Analysis and Applications 17 (1967) 37–47. https://doi.org/10.1016/0022-247X(67)90163-1

8 thms1 active userReviewed

Complexity Theory Theoretical Computer Science·Captain: wurtle

The approximation threshold for metric k-medianResearch Paper

Motivation

In metric $k$ -median, a finite set $J$ (or $D$ ) of clients and a finite set $F$ of candidate facilities lie in a common finite metric with rational distances. Given an integer $k\ge1$ , one opens a nonempty set $S\subseteq F$ with $|S|\le k$ and pays

\mathrm{cost}(S)=\sum_{j\in J}d(j,S),\qquad d(j,S)=\min_{i\in S}d(j,i),\qquad \mathrm{OPT}_k=\min_{S\subseteq F,\ 1\le|S|\le k}\mathrm{cost}(S).

Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. A lower bound has long been known: if $\mathrm P\ne\mathrm{NP}$ , no polynomial-time algorithm achieves a factor below $1+2/e\approx1.736$ in this candidate-facility model, by a reduction from Feige's coverage gap. The best polynomial-time algorithms had reached $2+\varepsilon$ , leaving a gap between $1.736$ and $2$ .

This mission asks for a formal proof that the threshold is exactly $1+2/e$ , as stated in an OpenAI preprint dated September 24, 2026 (source): a deterministic polynomial-time $(1+2/e+\varepsilon)$ -approximation for every fixed $\varepsilon>0$ , and hence, under $\mathrm P\ne\mathrm{NP}$ , an infimal approximation factor of exactly $1+2/e$ . The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

2001–2002 — Jain and Vazirani connect $k$ -median to facility location by Lagrangian relaxation and primal-dual methods (J. ACM 2001); Charikar, Guha, Tardos and Shmoys give the first constant-factor approximation by LP rounding (JCSS 2002); Jain, Mahdian and Saberi introduce greedy dual fitting (STOC 2002; J. ACM 2003).
2004 — Arya et al. show that bounded-swap local search achieves $3+\varepsilon$ (SICOMP 2004).
2016 — Li and Svensson show that constant-additive pseudo-approximations can be converted to true approximations at arbitrarily small loss, breaking the factor- $3$ barrier (SICOMP 2016).
2017–2023 — Bi-point rounding: $2.675+\varepsilon$ (Byrka et al., TALG 2017) and $2.613$ (Gowda et al., SODA 2023).
2019 — Cohen-Addad, Gupta, Kumar, Lee and Li give a tight FPT $(1+2/e+\varepsilon)$ -approximation in time $k^{O(k)}\mathrm{poly}$ (ICALP 2019).
2025–2026 — Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson reach $2+\varepsilon$ (arXiv:2503.10972); Byrka et al. develop iterative randomized rounding with $2+\varepsilon$ (arXiv:2604.06046).
September 2026 — Two OpenAI preprints claim a deterministic $(1+2/e+\varepsilon)$ -approximation, matching the known hardness threshold (source), and an independent randomized $(2-\sigma)$ -approximation via anchor recovery and bounded-price strictness (source).
Hardness — Feige proves the $\ln n$ threshold for set cover and the perfect-completeness Max- $k$ -Coverage gap (J. ACM 1998, Theorem 5.3); Anand and Lee record the resulting $1+2/e$ lower bound for $k$ -median with specified facilities under $\mathrm P\ne\mathrm{NP}$ (IPCO 2024).

Setting

An instance consists of $n$ points with a rational distance table $d$ that is a metric (nonnegative, zero exactly on the diagonal, symmetric, triangle inequality), a client set $J$ , a facility set $F$ (index sets that may overlap), and an integer $1\le k\le|F|$ , encoded in binary. A feasible solution is a nonempty $S\subseteq F$ with $|S|\le k$ . An algorithm is an $\alpha$ -approximation if it always outputs a feasible $S$ with $\mathrm{cost}(S)\le\alpha\,\mathrm{OPT}_k$ , and it is polynomial-time if it runs on a deterministic multi-stack Turing machine with finite alphabets in time polynomial in the encoding length.

Formalization targets

Milestone: Theorem 1.1 (p. 1)

For every fixed $\varepsilon>0$ there is a deterministic polynomial-time algorithm which, on every instance, returns a feasible $S$ with

\sum_{j\in J}d(j,S)\le\Bigl(1+\frac2e+\varepsilon\Bigr)\mathrm{OPT}_k .

Goal: Corollary 1.2 (p. 2)

If $\mathrm P\ne\mathrm{NP}$ , then

\inf\{\alpha:\ \text{a deterministic polynomial-time }\alpha\text{-approximation exists}\}=1+\frac2e .

The infimum is not asserted to be attained.

Significance

The result itself. It closes the approximability of metric $k$ -median with specified candidate facilities up to arbitrarily small additive error in the factor, ending a sequence of improvements from LP rounding through local search ( $3+\varepsilon$ ), bi-point rounding ( $2.675$ , $2.613$ ) to $2+\varepsilon$ . It shows that the FPT factor $1+2/e$ of Cohen-Addad et al. is achievable in polynomial time. The case $F=J$ has a different and still separate lower-bound question.

Formalizing it. The goal combines an algorithmic theorem with a hardness reduction. A formal proof needs: the Li–Svensson reduction from constant-additive pseudo-approximations (Theorem 2.2, p. 4); the grid preparation and iterative rounding with a finite directed comparison inequality whose scalar estimates are proved by rational polynomial certificates (Sections 3–5, Appendix A); derandomization by moment-matching distributions of polynomial size (Section 6); and, for the lower bound, NP-hardness of Feige's coverage gap in the Lean computation model. All are reusable for other clustering and covering problems.

Difficulty

Two obstacles meet. The cardinality budget is hard: allowing a constant number of extra facilities makes good connection cost much easier, and earlier rounding analyses in the iterative graph framework only certify factors at least $2$ (p. 2). The preprint's new ingredient is a potential that keeps track of surviving assignment copies after an opening and a finite directed comparison inequality (Theorem 4.1, p. 13) that pays for erasures. Then the randomized rounding must be made deterministic and polynomial-time while keeping the analysis valid, which requires preserving exactly the low-order moments the analysis uses (Lemma 6.1, p. 28; Theorem 6.2, p. 33), before Li–Svensson removes the additive surplus. The hardness side is classical but rests on the PCP-based Max- $k$ -Coverage gap.

Formalization scope

Instance carries n, a Fin n → Fin n → ℚ metric (distance_eq_zero is an iff, so a true metric), client and facility Finsets, and 1 ≤ k ≤ facilities.card. cost sums nearest distances over clients; optimum is the minimum over nonempty facility subsets of size $\le k$ .
Outputs are membership bit masks of an actual feasible set; FactorCorrect α I out requires that mask to describe a nonempty $S\subseteq F$ with $|S|\le k$ and $\mathrm{cost}(S)\le\alpha\,\mathrm{OPT}_k$ .
Polynomial time is Turing.TM2ComputableInPolyTime with finite tape alphabets, on the fixed binary instance encoding.
approximationFactors is the set of $\alpha$ admitting such an algorithm, and the goal is sInf approximationFactors = 1 + 2/Real.exp 1 under the hypothesis Complexity.PNeNP, where P and NP are defined in the same machine model (NP via polynomial-length witnesses and a finite-alphabet polynomial-time verifier). The set is nonempty by the milestone and bounded below, so sInf is meaningful.
The hypothesis $\mathrm P\ne\mathrm{NP}$ is not provable, so the goal is a conditional statement; deriving the lower bound requires a Cook–Levin-type NP-hardness of the coverage gap in this model.

Selected references

OpenAI, The approximation threshold for metric k-median, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Approximation-Threshold-for-Metric-k-Median-September-24-2026/main.pdf
OpenAI, Single-exponential recovery and bounded-price strictness for metric k-median, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Single-Exponential-Recovery-and-Bounded-Price-Strictness-for-Metric-k-Median-September-24-2026/paper.pdf
U. Feige, A threshold of ln n for approximating set cover, J. ACM 45 (1998). https://doi.org/10.1145/285055.285059
A. Anand, E. Lee, Separating k-median from the supplier version, IPCO 2024. https://doi.org/10.1007/978-3-031-59835-7_2
K. Jain, M. Mahdian, E. Markakis, A. Saberi, V. V. Vazirani, Greedy facility location algorithms analyzed using dual fitting with factor-revealing LP, J. ACM 50 (2003). https://doi.org/10.1145/950620.950621
M. Charikar, S. Li, A dependent LP-rounding approach for the k-median problem, ICALP 2012. https://doi.org/10.1007/978-3-642-31594-7_17
R. Gandhi, S. Khuller, S. Parthasarathy, A. Srinivasan, Dependent rounding and its applications to approximation algorithms, J. ACM 53 (2006). https://doi.org/10.1145/1147954.1147956
K. N. Gowda, T. Pensyl, A. Srinivasan, K. Trinh, Improved bi-point rounding algorithms and a golden barrier for k-median, SODA 2023. https://doi.org/10.1137/1.9781611977554.ch38
K. Jain, V. V. Vazirani, Approximation algorithms for metric facility location and k-median problems using the primal-dual schema and Lagrangian relaxation, J. ACM 48 (2001). https://doi.org/10.1145/375827.375845
M. Charikar, S. Guha, É. Tardos, D. B. Shmoys, A constant-factor approximation algorithm for the k-median problem, JCSS 65 (2002). https://doi.org/10.1006/jcss.2002.1882
V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local search heuristics for k-median and facility location problems, SIAM J. Comput. 33 (2004). https://doi.org/10.1137/S0097539702416402
S. Li, O. Svensson, Approximating k-median via pseudo-approximation, SIAM J. Comput. 45 (2016). https://doi.org/10.1137/130938645
J. Byrka, T. Pensyl, B. Rybicki, A. Srinivasan, K. Trinh, An improved approximation for k-median and positive correlation in budgeted optimization, ACM TALG 13 (2017). https://doi.org/10.1145/2981561
V. Cohen-Addad, A. Gupta, A. Kumar, E. Lee, J. Li, Tight FPT approximations for k-median and k-means, ICALP 2019. https://doi.org/10.4230/LIPIcs.ICALP.2019.42
V. Cohen-Addad, F. Grandoni, E. Lee, C. Schwiegelshohn, O. Svensson, A (2+ε)-approximation algorithm for metric k-median, arXiv:2503.10972 (2026 version). https://arxiv.org/abs/2503.10972v2

2 thms1 active userReviewed

Theoretical Computer Science·Captain: wurtle

Single-exponential recovery and bounded-price strictness for metric k-medianResearch Paper

Motivation

In metric $k$ -median, a finite set $J$ (or $D$ ) of clients and a finite set $F$ of candidate facilities lie in a common finite metric with rational distances. Given an integer $k\ge1$ , one opens a nonempty set $S\subseteq F$ with $|S|\le k$ and pays

\mathrm{cost}(S)=\sum_{j\in J}d(j,S),\qquad d(j,S)=\min_{i\in S}d(j,i),\qquad \mathrm{OPT}_k=\min_{S\subseteq F,\ 1\le|S|\le k}\mathrm{cost}(S).

Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. The hard part of the problem is the facility budget: a solution with small connection cost is much easier to find if a few extra facilities may be opened, and every approximation algorithm must eventually enforce $|S|\le k$ on its output.

This mission concerns two tools for enforcing that budget and their combination into a randomized approximation strictly below factor $2$ on arbitrary finite rational metrics, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

2001–2002 — Jain and Vazirani connect $k$ -median to facility location by Lagrangian relaxation and primal-dual methods (J. ACM 2001); Charikar, Guha, Tardos and Shmoys give the first constant-factor approximation by LP rounding (JCSS 2002); Jain, Mahdian and Saberi introduce greedy dual fitting (STOC 2002; J. ACM 2003).
2004 — Arya et al. show that bounded-swap local search achieves $3+\varepsilon$ (SICOMP 2004).
2016 — Li and Svensson show that constant-additive pseudo-approximations can be converted to true approximations at arbitrarily small loss, breaking the factor- $3$ barrier (SICOMP 2016).
2017–2023 — Bi-point rounding: $2.675+\varepsilon$ (Byrka et al., TALG 2017) and $2.613$ (Gowda et al., SODA 2023).
2019 — Cohen-Addad, Gupta, Kumar, Lee and Li give a tight FPT $(1+2/e+\varepsilon)$ -approximation in time $k^{O(k)}\mathrm{poly}$ (ICALP 2019).
2025–2026 — Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson reach $2+\varepsilon$ (arXiv:2503.10972); Byrka et al. develop iterative randomized rounding with $2+\varepsilon$ (arXiv:2604.06046).
September 2026 — Two OpenAI preprints claim a deterministic $(1+2/e+\varepsilon)$ -approximation, matching the known hardness threshold (source), and an independent randomized $(2-\sigma)$ -approximation via anchor recovery and bounded-price strictness (source).

Setting

Write $n=|D|$ and $N=|D|+|F|$ . A comparison solution $O\subseteq F$ of size $h$ assigns each client to a nearest member of $O$ (ties broken by fixed priorities); $C_i$ is the cluster of $i\in O$ and $P_i=\sum_{p\in C_i}d(p,i)$ , with $P=\mathrm{cost}(O)$ . An anchor is a supplied feasible $S\subseteq F$ with $|S|=h$ . A certificate partitions $O$ into good and bad centres and gives distinct proxies $\varphi_i\in S$ for the good centres. A randomized polynomial-time algorithm is a polynomial-time multi-stack Turing machine that reads the encoded instance together with a string of fair random bits whose length is a fixed polynomial in the input length.

Formalization targets

Milestone: refined recovery (Theorem 1.1, p. 2)

Let $D,F$ be disjoint, with distances between distinct indices positive integers bounded by a fixed polynomial in $N$ . Fix $\varepsilon>0$ , $0<L_0<\infty$ and a rational $0<\mu\le\min\{1/4,\varepsilon/12\}$ . There is a randomized algorithm that, given an anchor $S$ with $|S|=h\ge1$ and a failure parameter $\zeta\in(0,1)$ , always returns $\hat S\subseteq F$ with $|\hat S|\le h$ , runs in time polynomial in $N$ and $\log(1/\zeta)$ , and, whenever some comparison solution $O$ of size $h$ and cost $P>0$ admits a certificate with

\sum_{i\ \mathrm{good}}\sum_{p\in C_i}d(p,\varphi_i)\le \sum_{i\ \mathrm{good}}P_i+\mu P,\qquad \#\{i\ \mathrm{bad}\}\le L_0\log N,

satisfies $\mathrm{cost}(\hat S)\le(1+2/e+\varepsilon)P$ with probability at least $1-\zeta$ . The algorithm is not given $O$ , $P$ or the certificate.

Goal: global application (Theorem 1.2, p. 3)

There is an absolute constant $\sigma>0$ such that for every fixed $a>0$ some randomized polynomial-time algorithm for metric $k$ -median always returns a feasible $S$ (nonempty, $S\subseteq F$ , $|S|\le k$ ) and satisfies

\Pr\bigl[\mathrm{cost}(S)\le(2-\sigma)\,\mathrm{OPT}_k\bigr]\ \ge\ 1-(|D|+|F|+2)^{-a},\qquad \mathbb E\,\mathrm{cost}(S)\le(2-\sigma)\,\mathrm{OPT}_k .

Significance

The result itself. Theorem 1.1 makes the running time single-exponential in the number of clusters without accurate proxies, so logarithmically many exceptions are tractable; FPT methods with $k^{O(k)}$ dependence do not give this by setting $k=O(\log N)$ . Combined with a new proof of bounded-price strictness for one compatible execution of the logarithmic-surplus construction of Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson (Lemma 8.1, p. 43), it yields Theorem 1.2: a randomized approximation strictly below $2$ , both with high probability and in expectation, that opens at most $k$ facilities on every output. A companion preprint proves a stronger deterministic $(1+2/e+\varepsilon)$ bound by an independent route; Theorem 1.2's interest is the way recovery and payment accounting together enforce the budget.

Formalizing it. The statements are fully explicit about the machine model, the random bits, and the input encoding. A formal proof would need local-search anchoring (Theorem 3.3), leader/ball sampling with amortized radius guesses (Section 4), a finite categorical continuous-greedy algorithm with explicit error (Lemma 5.1, p. 21), the surplus construction as an external interface (Theorem 7.1, p. 35), and metric rounding and transfer (Lemma 2.1, p. 6). The submodular-optimization and local-search components are reusable.

Difficulty

Every factor- $2$ dual-fitting argument charges $\lambda+2P_C$ to a client set $C$ served by a comparison facility, which gives exactly $2$ ; improving the constant requires saving on connection cost while still paying for all $h$ regular openings with one final price, one set of copy lengths and the budgets of one actual replay of the construction (Section 1.2, p. 3). On the recovery side, guessing a good solution from an anchor naively costs $k^{O(k)}$ ; keeping the dependence single-exponential in the number of bad clusters requires interleaving leader sampling and removals and amortizing radius guesses over disjoint client sets (Section 4). Theorem 1.1 holds only for normalized integral metrics; the global application must construct its anchors after normalization and transfer the final cost bound back (Lemma 2.1, p. 6).

Formalization scope

RationalMetricInput: points Fin pointCount, a rational pseudometric table (zero on the diagonal, symmetric, triangle inequality), client and facility Finsets covering all points (they may overlap, so clients and facilities may share locations), a nonempty facility set and a positive budget $k$ . Feasible S is $S\subseteq F$ , $|S|\le k$ , and $S$ nonempty when there are clients; optimum minimizes over nonempty subsets of size $\le k$ .
A BinaryRandomizedAlgorithm is a TM2ComputableInPolyTime function of (input bits, random bits) with finite alphabets, using randomBits.eval (input length) fair bits; probabilities and expectations are uniform averages over all seeds.
In the goal, feasibility holds for every seed; the success bound is $1-(N+2)^{-a}$ with $N=|D|+|F|$ (Real.rpow); the same algorithm must also satisfy the expectation bound.
In the milestone, Input adds disjointness of $D$ and $F$ , integral distances, positivity between distinct indices, and an anchor with anchor.card = budget; Bounded bound caps distances by a fixed polynomial in $N$ ; ζ is passed in unary precision $\lceil\log_2(1/\zeta)\rceil$ , and PolynomialWork bounds work by $c(N+1)^d(1+\log(1/\zeta))^d$ . A Certificate encodes $O$ with $|O|=h$ , $P>0$ , the good set, injective proxies into the anchor, the proxy-cost promise with lexicographic tie-breaking, and at most $L_0\log N$ bad centres.

Selected references

OpenAI, Single-exponential recovery and bounded-price strictness for metric k-median, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Single-Exponential-Recovery-and-Bounded-Price-Strictness-for-Metric-k-Median-September-24-2026/paper.pdf
OpenAI, The approximation threshold for metric k-median, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Approximation-Threshold-for-Metric-k-Median-September-24-2026/main.pdf
V. Cohen-Addad, F. Grandoni, E. Lee, C. Schwiegelshohn, Breaching the 2 LMP approximation barrier for facility location with applications to k-median, arXiv:2207.05150 (2026 version). https://arxiv.org/abs/2207.05150v2
V. Cohen-Addad, C. Schwiegelshohn, On the local structure of stable clustering instances, FOCS 2017. https://doi.org/10.1109/FOCS.2017.14
G. Călinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a monotone submodular function subject to a matroid constraint, SIAM J. Comput. 40 (2011). https://doi.org/10.1137/080733991
J. Vondrák, Optimal approximation for the submodular welfare problem in the value oracle model, STOC 2008. https://doi.org/10.1145/1374376.1374389
K. Jain, M. Mahdian, E. Markakis, A. Saberi, V. V. Vazirani, Greedy facility location algorithms analyzed using dual fitting with factor-revealing LP, J. ACM 50 (2003). https://doi.org/10.1145/950620.950621
K. Jain, V. V. Vazirani, Approximation algorithms for metric facility location and k-median problems using the primal-dual schema and Lagrangian relaxation, J. ACM 48 (2001). https://doi.org/10.1145/375827.375845
M. Charikar, S. Guha, É. Tardos, D. B. Shmoys, A constant-factor approximation algorithm for the k-median problem, JCSS 65 (2002). https://doi.org/10.1006/jcss.2002.1882
V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local search heuristics for k-median and facility location problems, SIAM J. Comput. 33 (2004). https://doi.org/10.1137/S0097539702416402
S. Li, O. Svensson, Approximating k-median via pseudo-approximation, SIAM J. Comput. 45 (2016). https://doi.org/10.1137/130938645
J. Byrka, T. Pensyl, B. Rybicki, A. Srinivasan, K. Trinh, An improved approximation for k-median and positive correlation in budgeted optimization, ACM TALG 13 (2017). https://doi.org/10.1145/2981561
V. Cohen-Addad, A. Gupta, A. Kumar, E. Lee, J. Li, Tight FPT approximations for k-median and k-means, ICALP 2019. https://doi.org/10.4230/LIPIcs.ICALP.2019.42
V. Cohen-Addad, F. Grandoni, E. Lee, C. Schwiegelshohn, O. Svensson, A (2+ε)-approximation algorithm for metric k-median, arXiv:2503.10972 (2026 version). https://arxiv.org/abs/2503.10972v2

2 thms1 active userReviewed

Complexity Theory Theoretical Computer Science·Captain: wurtle

A Polynomial-Time Algorithm for Three-Machine Unit-Job SchedulingResearch Paper

Motivation

A set of unit-length jobs with precedence constraints is to be run on a fixed number of identical machines so that all jobs finish as early as possible. For two machines this was solved in 1969–1972; for a number of machines given as part of the input the problem is NP-complete (Ullman, 1975). Whether the problem is polynomial-time solvable for three machines, written $P3\mid\mathrm{prec},p_j=1\mid C_{\max}$ , is problem OPEN8 in the appendix of Garey and Johnson's 1979 book and is one of the best-known open questions on the complexity of scheduling.

Timeline

1969–1971. Fujii, Kasami and Ninomiya solve the two-processor case by matching (doi:10.1137/0117070, erratum doi:10.1137/0120018).
1972. Coffman and Graham give an optimal list-scheduling algorithm for two processors (doi:10.1007/BF00288685).
1975. Ullman proves NP-completeness when the number of machines is part of the input (doi:10.1016/S0022-0000(75)80008-0).
1979. Garey and Johnson list the fixed-three-machine problem as OPEN8; Graham, Lawler, Lenstra and Rinnooy Kan introduce the standard notation (doi:10.1016/S0167-5060(08)70356-X).
1983. Garey, Johnson, Tarjan and Yannakakis give a linear-time algorithm on three processors for opposing forests (doi:10.1137/0604011).
1984. Dolev and Warmuth give an $O(n^{h(m-1)+1})$ algorithm for precedence graphs of height $h$ (doi:10.1016/0196-6774(84)90039-7).
2016–2022. Approximation schemes for fixed machine counts: Levey and Rothvoß via LP hierarchies (doi:10.1145/2897518.2897532), Garg's quasi-PTAS (doi:10.4230/LIPIcs.ICALP.2018.59), Li (doi:10.1137/1.9781611976465.178), Das and Wiese (doi:10.4230/LIPIcs.ESA.2022.40).
2025. Nederlof, Swennenhuis and Węgrzycki give an exact algorithm in time $2^{O(\sqrt n\log n)}$ for three machines (doi:10.1137/1.9781611978322.16).

The source of this mission, an OpenAI preprint dated September 24, 2026, claims a deterministic polynomial-time algorithm.

Setting

The input is a directed acyclic graph $G=(V,E)$ on $V=\{1,\dots,n\}$ , $n\ge1$ , given as an explicit list of arcs, and optionally an integer deadline $T$ with $1\le T\le n$ . A feasible schedule with makespan at most $T$ is a map

\tau:V\to\{1,\dots,T\}

such that each value is taken at most three times (three machines) and $\tau(u)<\tau(v)$ for every arc $(u,v)\in E$ (precedence). Slot $t$ means execution during $[t-1,t)$ . There are no release dates, communication delays or other resources. The input length $L$ is the length of the binary encoding of the graph and deadline.

Formalization targets

Goal: Theorem 1.1

There is a single deterministic multitape Turing machine $M$ and a constant $C$ such that, on every such input of length $L$ , $M$ halts within

C\,(L+2)^{150020}

steps and

without a deadline, outputs a feasible schedule of minimum makespan;
with a deadline $T$ , outputs "infeasible" exactly when no feasible schedule with makespan at most $T$ exists, and otherwise outputs one.

The exponent is the one stated in the paper and is not optimized; the content of the theorem is that a fixed polynomial bound exists. The Lean statement OAI.ThreeMachine.main_theorem is open on the platform.

Significance

The theorem resolves the polynomial-time side of Garey and Johnson's OPEN8: unit-job makespan scheduling with arbitrary precedence constraints on three identical machines lies in P. Previous exact algorithms were either restricted to special precedence structures (forests, bounded height) or subexponential, and approximation schemes did not decide the optimum. The structural statement behind the algorithm, that feasible schedules admit recursive decompositions whose interval job sets have descriptions of bounded size, may be of independent use for other fixed-machine scheduling problems. No practical running time is claimed.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formal proof would also certify the running-time analysis in an explicit machine model, which is rarely done for algorithmic results of this size.

Difficulty

Removing selected slots from a feasible schedule leaves gaps that can be rescheduled independently, which suggests a recursive search over the job sets of gaps. The obstacle is their number: naming a gap by its two boundary triples does not determine its job set, and intersecting descriptions inherited from ancestors can make the descriptions grow without bound along a recursion of linear depth. The subexponential decomposition of Nederlof–Swennenhuis–Węgrzycki controls the number of subproblems only up to $2^{O(\sqrt n\log n)}$ ; a polynomial bound needs every subproblem to have a global description of constant size.

Formalization scope

Instance n is a list of arcs on Fin n; acyclic forbids a Relation.TransGen cycle. Jobs are Fin n (shifted to $1,\dots,n$ in the encoding).
Feasible G T τ: slots in $[1,T]$ , at most three jobs per slot, strict precedence.
CorrectOutput distinguishes the optimization mode (none) and the decision mode (some T).
The machine model is a custom multitape Turing machine Machine k q g over Fin (g+3) with $k+1$ tapes; input on tape 0 encoded by encodeInput (self-delimiting binary numbers), output read from tape 0 after halting. The time bound is $C\,(L+2)^{150020}$ with $L$ the encoded length.
The quantifiers are ordered so that the machine and constant are fixed before the instance (uniformity).

A complete development needs the combinatorics of the decomposition (separators and bounded global descriptions), a dynamic program over polynomially many descriptions, and its implementation and time analysis on the given Turing machine model. Contributions formalizing the purely combinatorial structure theorem, independently of the machine model, are welcome.

Selected references

OpenAI, A Polynomial-Time Algorithm for Three-Machine Unit-Job Scheduling, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-polynomial-time-algorithm-for-three-machine-unit-job-scheduling-September-24-2026/paper.pdf
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
E. G. Coffman Jr., R. L. Graham, Optimal scheduling for two-processor systems, Acta Inform., 1972. https://doi.org/10.1007/BF00288685
J. D. Ullman, NP-complete scheduling problems, J. Comput. System Sci., 1975. https://doi.org/10.1016/S0022-0000(75)80008-0
D. Dolev, M. K. Warmuth, Scheduling precedence graphs of bounded height, J. Algorithms, 1984. https://doi.org/10.1016/0196-6774(84)90039-7
J. Nederlof, C. M. F. Swennenhuis, K. Węgrzycki, A subexponential time algorithm for makespan scheduling of unit jobs with precedence constraints, SODA 2025. https://doi.org/10.1137/1.9781611978322.16
E. Levey, T. Rothvoß, A $(1+\epsilon)$ -approximation for makespan scheduling with precedence constraints using LP hierarchies, STOC 2016. https://doi.org/10.1145/2897518.2897532

2 thms1 active userReviewed

Complexity Theory Theoretical Computer Science·Captain: wurtle

Uniform computation of the squared-logarithmic k-server boundResearch Paper

Motivation

In the $k$ -server problem, $k$ labelled servers occupy points of a metric space, requests arrive online, and each request is served by moving one server onto it; the cost is the total distance moved, compared with the offline optimum through the competitive ratio. A companion OpenAI preprint claims that on every metric there exists a randomized policy with ratio $O(\log^2(k+1))$ against oblivious requests, matching the known worst-case lower bound. That result is an existence statement: it gives no procedure for computing the policy's probabilities.

This mission asks whether the bound can be realized by one uniform algorithm with explicit bit complexity on all finite rational metrics, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

1988–1990 — Manasse, McGeoch and Sleator introduce the $k$ -server problem and prove the deterministic lower bound $k$ (STOC 1988; J. Algorithms 1990).
1991 — Paging (the uniform metric): Fiat, Karp, Luby, McGeoch, Sleator and Young give the randomized marking algorithm and the harmonic lower bound (J. Algorithms 1991); McGeoch and Sleator attain $H_k$ exactly (Algorithmica 1991). This suggested the randomized $k$ -server conjecture, an $O(\log k)$ ratio on every metric.
1995 — Koutsoupias and Papadimitriou prove that the work function algorithm is $(2k-1)$ -competitive (J. ACM 1995).
1996–2004 — Probabilistic tree embeddings: Bartal (FOCS 1996) and Fakcharoenphol–Rao–Talwar with distortion $O(\log n)$ (JCSS 2004).
2012–2015 — Bansal, Buchbinder and Naor give $O(\log k)$ for weighted paging (J. ACM 2012); Bansal, Buchbinder, Mądry and Naor give the first polylogarithmic bound $O(\log^2k\log^3n\log\log n)$ on arbitrary finite metrics (J. ACM 2015).
2018 — Bubeck, Cohen, Lee, Lee and Mądry achieve $O(\log^2 k)$ on hierarchically separated trees, hence $O(\log^2k\log n)$ on $n$ -point metrics (STOC 2018).
2023 — Bubeck, Coester and Rabani disprove the randomized $k$ -server conjecture: some $(k+1)$ -point metrics need ratio $\Omega(\log^2k)$ (STOC 2023).
2026 — Coester and Cosson make the tree and finite-metric bounds polynomial-time, with ratio $O(\log n\log^2k)$ on general metrics (ICALP 2026).
September 2026 — Two OpenAI preprints claim the matching upper bound $O(\log^2(k+1))$ on every metric space (source) and a uniform bit-level implementation on finite rational metrics (source).

Setting

Fix $n\ge3$ and $2\le k<n$ . A rational metric on $X=\{1,\dots,n\}$ is a table $d(x,y)\in\mathbb Q$ that is nonnegative, zero exactly on the diagonal, symmetric, and satisfies the triangle inequality. An initial labelled tuple $s\in X^k$ may have repetitions. For a request word $\sigma$ , $\mathrm{cost}_{A,s}(\sigma)$ is the algorithm's total movement and $\mathrm{OPT}_s(\sigma)$ the minimum over all choices of serving labels with knowledge of $\sigma$ . $L$ denotes the total binary length of the encoding of $(n,k,d,s)$ .

The computational model is a bit machine: a finite control with an input tape, finitely many work tapes over $\{0,1,\text{blank}\}$ , an output channel, and one fresh unbiased random bit per step. At each request the input tape is replaced by the encoded request, the internal state is retained, and the output after the step budget names the server to move.

Formalization targets

Goal: Theorem 1.1 (p. 1)

There are an absolute constant $C$ and a polynomial $p$ such that a single uniform randomized online algorithm, on every instance $(n,k,d,s)$ as above,

preprocesses the instance in at most $p(L)$ bit operations;
serves request $r_t$ , for every reachable history and internal state, in at most $p\bigl(L+\lceil\log_2(t+1)\rceil\bigr)$ further bit operations, outputting a valid server label and moving exactly that server;
for every fixed finite request sequence $\sigma$ independent of its random bits satisfies

\mathbb E\,\mathrm{cost}_{A,s}(\sigma)\ \le\ C\,\bigl(\log(k+1)\bigr)^2\,\mathrm{OPT}_s(\sigma)+B_{d,k,s},

with $B_{d,k,s}<\infty$ independent of $\sigma$ and of its length.

Significance

The result itself. It converts the existence theorem into an algorithm whose ratio is independent of $n$ , using only unbiased random bits and polynomial work per request in the input length and the bit length of the request counter. The price is an additive constant $B_{d,k,s}$ with no size bound: the algorithm may serve a very long initial stretch with a fixed label while its constructor runs. Coester and Cosson obtain stronger time and randomness guarantees but with ratio $O(\log n\log^2k)$ on general metrics; the two results are incomparable.

Formalizing it. The goal is stated in an explicit machine model, so a formal proof certifies both the competitive bound and the bit-complexity bound. It needs the companion existence theorem (Theorem 2.1 here, p. 4) as an input; a full development therefore also requires formalizing that theorem or taking it as a separate milestone. Exact rational linear algebra (Fourier–Motzkin elimination), dyadic rounding of probabilities, and step-counted machine simulation are reusable.

Difficulty

Knowing that a good policy exists does not give its probabilities, and a finite horizon alone does not control a long input on which the optimum barely moves. The preprint (pp. 3–4) solves a rational linear system for each horizon, then filters requests so that only those missed by some strongly lazy service with bounded moves are retained, which bounds the retained word length; a marking fallback pays for trajectories exceeding the move cap. The constructor's running time is uncontrolled, so the algorithm simulates it for only $\lfloor\log_2(t+1)\rfloor$ steps at request $t$ (Proposition 4.2, p. 14), and the delayed activation is absorbed into $B_{d,k,s}$ .

Formalization scope

RationalMetric n is a Fin n → Fin n → ℚ table with the metric axioms; configurations are Fin k → Fin n; offlineCost is the sInf over label histories matching the request word (a finite, nonempty set of costs).
BitMachine has finitely many controls and tapes and a transition consuming one coin per step. Preprocessing (boot) runs $c(L+1)^e$ steps with all coins $0$ , so it is deterministic; this is satisfied by the source's deterministic constructor, and Theorem 1.1 does not require randomness there.
Each request runs exactly requestBudget c e L t $=c(L+\lceil\log_2(t+1)\rceil+1)^e$ steps (Nat.clog 2 (t+1)) and must have yielded with output value $<k$ for every reachable state and every coin string; requests are encoded by a fixed self-delimiting binary code.
machineExpectedCost averages over all coin strings of the step budget, i.e. uniformly random bits; the bound is required for every request list w, with $B\ge0$ chosen after $(d,s)$ and before w.
The machine, the polynomial $(c,e)$ and $C$ are fixed before $n$ , $k$ , $d$ , $s$ : the algorithm is uniform.

Selected references

OpenAI, Uniform computation of the squared-logarithmic k-server bound, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026.pdf
OpenAI, Squared-logarithmic randomized k-server on arbitrary metrics, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026.pdf
D. Komm, R. Královič, R. Královič, T. Mömke, Randomized online computation with high probability guarantees, Algorithmica (2022). https://doi.org/10.1007/s00453-022-00925-z
G. B. Dantzig, B. C. Eaves, Fourier–Motzkin elimination and its dual, J. Combin. Theory Ser. A 14 (1973). https://doi.org/10.1016/0097-3165(73)90004-6
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, J. Algorithms 11 (1990). https://doi.org/10.1016/0196-6774(90)90003-W
E. Koutsoupias, C. H. Papadimitriou, On the k-server conjecture, J. ACM 42 (1995). https://doi.org/10.1145/210118.210128
A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12 (1991). https://doi.org/10.1016/0196-6774(91)90041-V
N. Bansal, N. Buchbinder, A. Mądry, J. Naor, A polylogarithmic-competitive algorithm for the k-server problem, J. ACM 62 (2015). https://doi.org/10.1145/2783434
S. Bubeck, M. B. Cohen, J. R. Lee, Y. T. Lee, A. Mądry, k-server via multiscale entropic regularization, STOC 2018. https://doi.org/10.1145/3188745.3188798
S. Bubeck, C. Coester, Y. Rabani, The randomized k-server conjecture is false!, STOC 2023. https://doi.org/10.1145/3564246.3585132
C. Coester, R. Cosson, Randomized k-server in polynomial time, ICALP 2026. https://doi.org/10.4230/LIPIcs.ICALP.2026.65
J. Fakcharoenphol, S. Rao, K. Talwar, A tight bound on approximating arbitrary metrics by tree metrics, JCSS 69 (2004). https://doi.org/10.1016/j.jcss.2004.04.011

2 thms1 active userReviewed

Theoretical Computer Science·Captain: wurtle

Squared-logarithmic randomized k-server on arbitrary metricsResearch Paper

Motivation

In the $k$ -server problem, $k$ servers sit at points of a metric space; requests arrive one at a time, and each request must be served by moving some server onto it, at a cost equal to the distance travelled. An online policy sees only the requests revealed so far, and its quality is measured by its competitive ratio: how much more it moves, in expectation, than the offline optimum that knows the whole sequence. The problem was introduced as a common framework for paging, caching and other online service problems, and the question of the best ratio achievable by randomized policies has driven the development of metric embeddings, online primal-dual methods and entropic regularization.

This mission asks for a formal proof that randomized $k$ -server has competitive ratio $O(\log^2(k+1))$ on every metric space, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

1988–1990 — Manasse, McGeoch and Sleator introduce the $k$ -server problem and prove the deterministic lower bound $k$ (STOC 1988; J. Algorithms 1990).
1991 — Paging (the uniform metric): Fiat, Karp, Luby, McGeoch, Sleator and Young give the randomized marking algorithm and the harmonic lower bound (J. Algorithms 1991); McGeoch and Sleator attain $H_k$ exactly (Algorithmica 1991). This suggested the randomized $k$ -server conjecture, an $O(\log k)$ ratio on every metric.
1995 — Koutsoupias and Papadimitriou prove that the work function algorithm is $(2k-1)$ -competitive (J. ACM 1995).
1996–2004 — Probabilistic tree embeddings: Bartal (FOCS 1996) and Fakcharoenphol–Rao–Talwar with distortion $O(\log n)$ (JCSS 2004).
2012–2015 — Bansal, Buchbinder and Naor give $O(\log k)$ for weighted paging (J. ACM 2012); Bansal, Buchbinder, Mądry and Naor give the first polylogarithmic bound $O(\log^2k\log^3n\log\log n)$ on arbitrary finite metrics (J. ACM 2015).
2018 — Bubeck, Cohen, Lee, Lee and Mądry achieve $O(\log^2 k)$ on hierarchically separated trees, hence $O(\log^2k\log n)$ on $n$ -point metrics (STOC 2018).
2023 — Bubeck, Coester and Rabani disprove the randomized $k$ -server conjecture: some $(k+1)$ -point metrics need ratio $\Omega(\log^2k)$ (STOC 2023).
2026 — Coester and Cosson make the tree and finite-metric bounds polynomial-time, with ratio $O(\log n\log^2k)$ on general metrics (ICALP 2026).
September 2026 — Two OpenAI preprints claim the matching upper bound $O(\log^2(k+1))$ on every metric space (source) and a uniform bit-level implementation on finite rational metrics (source).

Setting

Let $(X,d)$ be a metric space and $s=(s_1,\dots,s_k)\in X^k$ the initial positions of $k$ labelled servers; repeated positions are allowed. To serve a request $r_t$ , a policy chooses one label $j$ and moves server $j$ to $r_t$ , leaving the others fixed (a server already at $r_t$ may be chosen at zero cost). For a finite request sequence $\sigma$ , $\mathrm{cost}_{A,s}(\sigma)$ is the total distance moved and $\mathrm{OPT}_s(\sigma)$ is the minimum of this cost over all label sequences, chosen with knowledge of $\sigma$ . A randomized online policy chooses, at each step, a probability distribution over labels as a function of the past requests, its own past choices and the current request. Requests are fixed in advance, independently of the policy's randomness (the oblivious adversary).

Formalization targets

Goal: Theorem 1.1 (p. 2)

There is an absolute constant $C<\infty$ such that for every $k\ge2$ , every metric space $(X,d)$ with at least $k+1$ points, and every $s\in X^k$ , there are a randomized online policy $A$ and a finite $B\ge0$ with

\mathbb E\,\mathrm{cost}_{A,s}(\sigma)\ \le\ C\,\bigl(\log(k+1)\bigr)^2\,\mathrm{OPT}_s(\sigma)+B

for every finite request sequence $\sigma$ . The same policy serves all sequences and horizons; $B$ may depend on $(X,d)$ , $k$ and $s$ but not on $\sigma$ ; and $B=0$ when the entries of $s$ are distinct.

Significance

The result itself. Combined with the Bubeck–Coester–Rabani lower bound, it identifies $\Theta(\log^2 k)$ as the worst-case order of the randomized competitive ratio over all metrics. The bound has no dependence on the number of points, the aspect ratio, finiteness or boundedness of $X$ , removing the $\log n$ factor left by static tree embeddings. No computational efficiency is claimed; a companion preprint turns the existence statement into a uniform algorithm on finite rational metrics.

Formalizing it. The statement is elementary to state, but its proof combines a rank-based allocation on separated trees, slowly varying simplex trackers, a compact potential for partition edits, online partitions with an embedded comparator, balanced rounding, and a compactness argument (Tychonoff) producing one policy for all finite inputs. None of these online-algorithm tools exist in a formal library, and a machine-checked competitive analysis of a randomized $k$ -server algorithm on general metrics is not known.

Difficulty

Embedding the metric into a random hierarchically separated tree and running an $O(\log^2k)$ tree algorithm loses the embedding distortion, which is $\Theta(\log n)$ in the worst case and is not bounded in terms of $k$ . Removing it requires changing the tree as requests arrive, and the cost of re-partitioning must be paid for. A previous dynamic approach (Lee's fusible HSTs) had its general claim withdrawn after a gap in that accounting (p. 3). In the preprint, the partition schedule is driven by the posterior measure of a hidden comparator, and the edit costs and the travel of parked mass are bounded separately (Sections 7–8). Passing from finite metrics and finite horizons to one policy on an arbitrary, possibly infinite and unbounded, space with a fixed constant requires a further compactness step (Section 10).

Formalization scope

X : Type u carries an arbitrary MetricSpace instance; "at least $k+1$ points" is an injection Fin (k+1) → X. No finiteness, separability or boundedness is assumed.
A Policy k X maps the history (list of past requests with the labels used) and the current request to a LabelDistribution k, i.e. a probability vector on Fin k. Every step moves exactly one server (Function.update), as in the source.
expectedCost is the finite sum over all label sequences of the path probability times the service cost; optimalCost is the sInf over all label sequences of the service cost (nonempty finite set, so the infimum is a minimum). Restricting the offline optimum to one-server-per-request service does not change it (triangle inequality).
The constant $C>0$ is chosen before $k$ , $X$ and $s$ ; the policy and $B\ge0$ are chosen after $s$ and before the request list; Function.Injective s → B = 0 encodes the distinct-start clause.
Logarithms are natural (Real.log).

Selected references

OpenAI, Squared-logarithmic randomized k-server on arbitrary metrics, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026.pdf
OpenAI, Uniform computation of the squared-logarithmic k-server bound, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026.pdf
J. R. Lee, Fusible HSTs and the randomized k-server conjecture, FOCS 2018. https://doi.org/10.1109/FOCS.2018.00049
A. Tychonoff, Über einen Funktionenraum, Math. Ann. 111 (1935). https://doi.org/10.1007/BF01472255
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, J. Algorithms 11 (1990). https://doi.org/10.1016/0196-6774(90)90003-W
E. Koutsoupias, C. H. Papadimitriou, On the k-server conjecture, J. ACM 42 (1995). https://doi.org/10.1145/210118.210128
A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12 (1991). https://doi.org/10.1016/0196-6774(91)90041-V
N. Bansal, N. Buchbinder, A. Mądry, J. Naor, A polylogarithmic-competitive algorithm for the k-server problem, J. ACM 62 (2015). https://doi.org/10.1145/2783434
S. Bubeck, M. B. Cohen, J. R. Lee, Y. T. Lee, A. Mądry, k-server via multiscale entropic regularization, STOC 2018. https://doi.org/10.1145/3188745.3188798
S. Bubeck, C. Coester, Y. Rabani, The randomized k-server conjecture is false!, STOC 2023. https://doi.org/10.1145/3564246.3585132
C. Coester, R. Cosson, Randomized k-server in polynomial time, ICALP 2026. https://doi.org/10.4230/LIPIcs.ICALP.2026.65
J. Fakcharoenphol, S. Rao, K. Talwar, A tight bound on approximating arbitrary metrics by tree metrics, JCSS 69 (2004). https://doi.org/10.1016/j.jcss.2004.04.011

2 thms1 active userReviewed

Complexity Theory Theoretical Computer Science·Captain: wurtle

A Direct Proof of Optimal Max-Cut HardnessResearch Paper

Motivation

Max-Cut asks for a partition of the vertices of a graph that maximizes the number of edges crossing it. Its decision version is one of Karp's original NP-complete problems, so the natural question is how well it can be approximated in polynomial time. Goemans and Williamson's semidefinite-programming algorithm with random-hyperplane rounding achieves ratio approaching

\alpha_{\mathrm{GW}}=\min_{-1\le\rho<1}\frac{2\arccos\rho}{\pi(1-\rho)}=0.878567\ldots

(GW 1995). Whether any polynomial-time algorithm can beat this constant is a central question of approximation algorithms: unconditional NP-hardness was known only above $16/17$ , and optimality of $\alpha_{\mathrm{GW}}$ was known only under Khot's Unique Games Conjecture.

This mission asks for a machine-checked proof that approximating Max-Cut within any fixed ratio $\alpha\in(\alpha_{\mathrm{GW}},1]$ is NP-hard, even on simple unweighted graphs, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 1). The preprint gives a direct reduction from the 2-to-1 Games Theorem, not via the Unique Games Conjecture. It has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

1972 — Karp lists Max-Cut among the original NP-complete problems (Karp 1972).
1995 — Goemans and Williamson give the SDP algorithm with ratio $\alpha_{\mathrm{GW}}$ (JACM 1995).
2000–2001 — Håstad's optimal inapproximability results (JACM 2001) combined with the gadgets of Trevisan, Sorkin, Sudan and Williamson (SICOMP 2000) rule out ratios above $16/17$ .
2002 — Feige and Schechtman show the SDP integrality gap approaches $\alpha_{\mathrm{GW}}$ (RSA 2002); Khot formulates the Unique Games Conjecture (STOC 2002).
2007–2010 — Khot, Kindler, Mossel and O'Donnell prove that $\alpha_{\mathrm{GW}}$ is optimal assuming the UGC, conditional on Majority Is Stablest (SICOMP 2007), which Mossel, O'Donnell and Oleszkiewicz prove (Annals 2010) via Borell's Gaussian noise-stability bound (1985). O'Donnell–Wu (STOC 2008) and Raghavendra (STOC 2008) extend the UG-based picture.
2017–2025 — The Grassmann-graph programme establishes the 2-to-1 Games Theorem with imperfect completeness: Khot–Minzer–Safra (ToC 2025), Dinur–Khot–Kindler–Minzer–Safra (ToC 2025), Barak–Kothari–Steurer (ITCS 2019), Khot–Minzer–Safra expansion (Annals 2023).
2026 — The OpenAI preprint claims unconditional NP-hardness at every ratio above $\alpha_{\mathrm{GW}}$ .

Setting

A simple unweighted graph on $N$ vertices is given by a symmetric, loopless Boolean adjacency table. A cut is a map $c$ from the vertices to $\{0,1\}$ ; its size is the number of unordered edges $\{u,v\}$ with $c(u)\ne c(v)$ , and $\mathrm{MaxCut}(G)$ is the largest cut size. An algorithm is an $\alpha$ -approximation if it always returns a cut of size at least $\alpha\cdot\mathrm{MaxCut}(G)$ .

3SAT inputs are bit strings decoding canonically to a conjunction of three-slot clauses (repeated variables and literals allowed); malformed strings are NO instances. A gap reduction for $\alpha$ consists of rationals $Y>0$ and $N\ge0$ with $N<\alpha Y$ , and a deterministic polynomial-time map $\varphi\mapsto(G_\varphi,Q_\varphi)$ outputting a graph together with a positive integer scale $Q_\varphi$ such that

\varphi\in\mathrm{3SAT}\Rightarrow \frac{\mathrm{MaxCut}(G_\varphi)}{Q_\varphi}\ge Y,\qquad \varphi\notin\mathrm{3SAT}\Rightarrow \frac{\mathrm{MaxCut}(G_\varphi)}{Q_\varphi}\le N.

Given such a reduction, an $\alpha$ -approximation algorithm would decide 3SAT by comparing its output with $N Q_\varphi$ .

Formalization targets

Goal: optimal Max-Cut hardness (Theorem 1.1, p. 1)

For every real $\alpha$ with $\alpha_{\mathrm{GW}}<\alpha\le1$ , a gap reduction for $\alpha$ from 3SAT to simple unweighted Max-Cut exists:

\forall\,\alpha\in(\alpha_{\mathrm{GW}},1]:\quad \mathrm{GapReduction}(\alpha)\ne\varnothing.

In Lean this is OAI.OptimalMaxCut.main : OptimalMaxCut.MainStatement. The preprint proves it from a sharper weighted gap (Theorem 1.2, p. 2): for rational $t\in(0,1)$ , $B(t)=\tfrac{2}{\pi}\arcsin t$ and $0<\varepsilon<(t-B(t))/4$ , it is NP-hard to distinguish $\mathrm{Val}\ge\frac{1+t}{2}-\varepsilon$ from $\mathrm{Val}\le\frac{1+B(t)}{2}+\varepsilon$ on graphs with a rational edge distribution; Appendix B (p. 35) converts weighted graphs to simple unweighted ones.

Significance

The result itself. Theorem 1.1 shows that the Goemans–Williamson algorithm is optimal among polynomial-time algorithms unless P = NP, removing the Unique Games hypothesis from the result of Khot, Kindler, Mossel and O'Donnell. It is the most prominent instance of an SDP-tight threshold, and the gap form (Theorem 1.2) gives a whole curve of completeness/soundness pairs.

Formalizing it. No machine-checked proof of any optimal inapproximability result for Max-Cut exists. A full development requires the 2-to-1 Games Theorem in the affine form stated as Proposition 2.2 (p. 6) and derived in Appendix A, the Majority Is Stablest theorem (Lemma 2.1, p. 5), and the paper's new ingredients: tree-code Fourier analysis (Section 5), a vector-valued affine hashing lemma (Lemma 6.1, p. 14), dimension-independent extraction (Proposition 7.1, p. 18) and decoding (Proposition 8.4, p. 24). Several of these — Majority Is Stablest, Boolean Fourier analysis, polynomial-time gap reductions on Turing machines — are reusable libraries in their own right.

Difficulty

The classical long-code test for Max-Cut, analysed via Majority Is Stablest, identifies an influential coordinate of an arbitrary cut. Under the Unique Games Conjecture that coordinate is directly a label of the source game. Starting instead from 2-to-1 games, the influential coordinate is indexed by a gate input of the test, not by a source-game label, and the two endpoints of a source edge cannot in general reconstruct a common context without knowing their projection. The decoding loss must also be independent of the source alphabet, because the alphabet dimension is chosen after the target soundness; a dimension-dependent loss would make the parameter choice circular (Introduction, pp. 3–4).

Formalization scope

Graphs are OptimalMaxCut.Graph: a vertex count with a symmetric loopless Bool adjacency function; maxCut maximizes cutSize over all Fin n → Bool, counting each unordered crossing edge once.
The output is a ScaledGraph with an explicit positive integer scale; the YES/NO bounds compare maxCut / scale in ℝ, and 0 < scale rules out division by zero.
alphaGW is defined as the sInf of $2\arccos\rho/(\pi(1-\rho))$ over $\rho\in[-1,1)$ ; this set is nonempty and bounded below, so the infimum is the true constant.
The reduction is a Turing.TM2ComputableInPolyTime machine with finite tape alphabets, from raw input bits (identity encoding) to ScaledGraph.bits (delimited vertex count and scale, then the full adjacency table); the rational bounds and the machine are fixed before the input.
The hypothesis $\alpha_{\mathrm{GW}}<\alpha\le1$ is satisfiable, and the conclusion requires an actual strict gap noBound < α * yesBound with 0 < yesBound, so there is no trivial reading. No assumption P ≠ NP is built in.

Welcome contributions: Boolean and Gaussian Fourier analysis (noise stability, influences, Borell's theorem), Majority Is Stablest, the 2-to-1 Games Theorem, and a reusable library for polynomial-time gap reductions on TM2 machines.

Selected references

OpenAI, A Direct Proof of Optimal Max-Cut Hardness, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Direct-Proof-of-Optimal-Max-Cut-Hardness-September-23-2026/paper.pdf
M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995). https://doi.org/10.1145/227683.227684
J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001). https://doi.org/10.1145/502090.502098
L. Trevisan, G. Sorkin, M. Sudan, D. Williamson, Gadgets, approximation, and linear programming, SIAM J. Comput. 29 (2000). https://doi.org/10.1137/S0097539797328847
S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal inapproximability results for MAX-CUT and other 2-variable CSPs?, SIAM J. Comput. 37 (2007). https://doi.org/10.1137/S0097539705447372
E. Mossel, R. O'Donnell, K. Oleszkiewicz, Noise stability of functions with low influences: invariance and optimality, Ann. of Math. 171 (2010). https://doi.org/10.4007/annals.2010.171.295
U. Feige, G. Schechtman, On the optimality of the random hyperplane rounding technique for MAX CUT, Random Structures Algorithms 20 (2002). https://doi.org/10.1002/rsa.10036
I. Dinur, S. Khot, G. Kindler, D. Minzer, M. Safra, Towards a proof of the 2-to-1 games conjecture?, Theory of Computing 21 (2025). https://doi.org/10.4086/toc.2025.v021a011
S. Khot, D. Minzer, M. Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion, Ann. of Math. 198 (2023). https://doi.org/10.4007/annals.2023.198.1.1
S. Khot, On the power of unique 2-prover 1-round games, STOC 2002. https://doi.org/10.1145/509907.510017

2 thms1 active userReviewed

Optimization·Captain: mikedeng1

Theoretical and Numerical Comparison of Relaxation Methods for Mathematical Programs with Complementarity Constraints 1: Scholtes Relaxation Limits Are C-Stationary under MPEC-MFCQResearch Paper

Motivation

A mathematical program with complementarity constraints (MPCC, also called MPEC, mathematical program with equilibrium constraints) is a nonlinear optimization problem in which some pairs of constraint functions must be nonnegative with at least one of each pair equal to zero. Such constraints model equilibria inside an optimization problem: bilevel programs whose lower level is replaced by its optimality conditions, Stackelberg games, traffic and electricity market equilibria, contact problems in mechanics. See Luo, Pang and Ralph, Mathematical Programs with Equilibrium Constraints (Cambridge University Press, 1996), doi:10.1017/CBO9780511983658.

The complementarity constraints make the standard theory fail. At every feasible point the Mangasarian–Fromovitz constraint qualification is violated, so the Karush–Kuhn–Tucker conditions are not necessary for optimality, and standard NLP solvers lose their convergence guarantees. A common remedy is relaxation: replace the MPEC by a family of ordinary nonlinear programs depending on a parameter $t>0$ , solve them for $t\downarrow0$ , and study the limits of their stationary points.

The first relaxation scheme, and the reference point for all later ones, is due to Scholtes (Convergence properties of a regularization scheme for mathematical programs with complementarity constraints, SIAM J. Optim. 11 (2001), doi:10.1137/S1052623499361233). Scholtes showed that limits of stationary points of the relaxed programs are C-stationary when MPEC-LICQ holds at the limit. Hoheisel, Kanzow and Schwartz (Preprint 299, University of Würzburg, 2010; later Math. Program. 137 (2013), doi:10.1007/s10107-011-0488-5) compare five relaxation schemes and weaken the constraint qualification in each convergence theorem. For Scholtes' scheme, their Theorem 3.1 replaces MPEC-LICQ by the weaker MPEC-MFCQ. This mission formalizes that theorem.

Setting

The MPEC (1) is

\min f(x)\ \ \text{s.t.}\ \ g_i(x)\le0\ (i\le m),\ \ h_i(x)=0\ (i\le p),\ \ G_i(x)\ge0,\ \ H_i(x)\ge0,\ \ G_i(x)H_i(x)=0\ (i\le l),

with continuously differentiable $f,g_i,h_i,G_i,H_i:\mathbb R^n\to\mathbb R$ and feasible set $X$ . For a point $x^*$ the paper uses the index sets $I_g=\{i\mid g_i(x^*)=0\}$ , $I_{0+}=\{i\mid G_i(x^*)=0<H_i(x^*)\}$ , $I_{00}=\{i\mid G_i(x^*)=H_i(x^*)=0\}$ and $I_{+0}=\{i\mid G_i(x^*)>0=H_i(x^*)\}$ .

A standard nonlinear program has constraints $g_i\le0$ , $h_j=0$ . Its point $x$ satisfies the Mangasarian–Fromovitz constraint qualification (MFCQ) if the gradients $\nabla h_j(x)$ are linearly independent and some direction $d$ has $\nabla g_i(x)^Td<0$ for all active $i$ and $\nabla h_j(x)^Td=0$ for all $j$ . A stationary point is the $x$ -part of a KKT point: $x$ is feasible and there are $\lambda\ge0$ , $\mu$ with $\lambda_ig_i(x)=0$ and $\nabla f(x)+\sum\lambda_i\nabla g_i(x)+\sum\mu_j\nabla h_j(x)=0$ .

The tightened program TNLP $(x^*)$ keeps $g_i\le0$ , $h_i=0$ and imposes $G_i=0,\ H_i\ge0$ on $I_{0+}$ , $G_i\ge0,\ H_i=0$ on $I_{+0}$ , and $G_i=H_i=0$ on $I_{00}$ . MPEC-MFCQ holds at $x^*$ if MFCQ holds at $x^*$ for TNLP $(x^*)$ .

A feasible $x^*$ is weakly stationary if there are multipliers $\lambda\in\mathbb R^m$ , $\mu\in\mathbb R^p$ , $\gamma,\nu\in\mathbb R^l$ with

\nabla f(x^*)+\sum_{i=1}^m\lambda_i\nabla g_i(x^*)+\sum_{i=1}^p\mu_i\nabla h_i(x^*)-\sum_{i=1}^l\gamma_i\nabla G_i(x^*)-\sum_{i=1}^l\nu_i\nabla H_i(x^*)=0,

$\lambda\ge0$ , $\lambda_ig_i(x^*)=0$ , $\gamma_i=0$ on $I_{+0}$ and $\nu_i=0$ on $I_{0+}$ . It is C-stationary if such multipliers can be chosen with, in addition, $\gamma_i\nu_i\ge0$ for all $i\in I_{00}$ .

Scholtes' relaxed program $R^S(t)$ replaces $G_i(x)H_i(x)=0$ by $G_i(x)H_i(x)\le t$ and keeps all other constraints of (1). The notation $\{t_k\}\downarrow0$ means a sequence of positive parameters decreasing to $0$ .

Formalization targets

Goal: Theorem 3.1

Let $\{t_k\}\downarrow0$ , let $x^k$ be a stationary point of $R^S(t_k)$ , and let $x^k\to x^*$ with MPEC-MFCQ at $x^*$ . Then

x^*\ \text{is a C-stationary point of the MPEC (1).}

No feasibility of $x^*$ is assumed; it is part of the conclusion.

Milestones

Remark 2.2: for a feasible point of a standard NLP, MFCQ holds if and only if the active inequality gradients together with all equality gradients are positive-linearly independent.
§2.2, pp. 6–7: MPEC-MFCQ written out explicitly, i.e. linear independence of $\nabla h_i$ , $\nabla G_i$ ( $I_{00}\cup I_{0+}$ ) and $\nabla H_i$ ( $I_{00}\cup I_{+0}$ ), plus a direction $d$ .
Proof of Theorem 3.2, p. 11: MPEC-MFCQ implies positive-linear independence of $\{\nabla g_i(x^*)\}_{I_g}\cup\{\{\nabla h_i\}\cup\{\nabla G_i\}_{I_{00}\cup I_{0+}}\cup\{\nabla H_i\}_{I_{00}\cup I_{+0}}\}$ .
Proof of Theorem 3.1, p. 9: for large $k$ , $I_g(x^k)\subseteq I_g$ , $I_G(x^k)\subseteq I_{00}\cup I_{0+}$ , $I_H(x^k)\subseteq I_{00}\cup I_{+0}$ .
Proof of Theorem 3.1, pp. 10–11: under the goal's hypotheses, $x^*$ is weakly stationary.

Significance

Theorem 3.1 says that Scholtes' scheme, run to the limit, produces C-stationary points under a constraint qualification strictly weaker than the one in Scholtes' original result. MPEC-MFCQ is the natural assumption here: under it the KKT multipliers of the relaxed programs need not converge, and the theorem shows that a convergent subsequence of suitably modified multipliers still exists. The result is the first of a family of convergence theorems in the paper (the schemes of Lin–Fukushima, Kadrani–Dussault–Benchakroun and Steffensen–Ulbrich follow the same pattern) and the baseline against which those schemes are compared.

The theorem is proved in the paper; it is not open. To the extent a search of the Prove2Me catalog shows, no MPEC stationarity concept, MPEC constraint qualification or relaxation result has been formalized there, and Mathlib has no theory of constraint qualifications for nonlinear programs. The mission produces a machine-checked proof of Theorem 3.1 and, along the way, reusable statements of Definition 2.1, MFCQ, KKT points and the MFCQ/positive-linear-independence equivalence for general nonlinear programs.

Difficulty

The obvious argument takes a limit of the KKT multipliers of $R^S(t_k)$ . That fails twice. First, under MPEC-MFCQ the multiplier sequence need not be bounded, so there may be nothing to take a limit of; boundedness has to be recovered from MPEC-MFCQ through positive-linear independence, a theorem of the alternative. Second, the multiplier $\delta^k$ of the product constraint $G_iH_i\le t_k$ multiplies $H_i\nabla G_i+G_i\nabla H_i$ , which is not a multiplier of $\nabla G_i$ or $\nabla H_i$ alone; how it is redistributed depends on whether $i$ lies in $I_{0+}$ , $I_{+0}$ or $I_{00}$ , and the sign condition on $I_{00}$ comes from the support disjointness between $\delta^k$ and the multipliers of $G_i\ge0$ , $H_i\ge0$ , which uses $t_k>0$ . Compactness, index-set bookkeeping along a subsequence and continuity of all gradients have to be combined.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), gradients are Mathlib's gradient, and $\nabla g(x)^Td$ is the inner product. Constraint indices are Fin m, Fin p, Fin l (0-based); $m,p,l$ may be $0$ .
The paper's standing assumption that all data are continuously differentiable (p. 1) is the explicit hypothesis P.IsC1 (ContDiff ℝ 1 for each function) of the goal and of milestones 4 and 5. Milestones 1–3 are pointwise linear algebra and assume no smoothness.
"Stationary point of $R^S(t_k)$ " is a KKT point of $R^S(t_k)$ viewed as a standard NLP with inequality constraints $g_i\le0$ , $-G_i\le0$ , $-H_i\le0$ , $G_iH_i-t\le0$ : feasibility, nonnegative multipliers and complementary slackness are included (p. 5).
" $\{t_k\}\downarrow0$ " is $t_k>0$ for all $k$ , $(t_k)$ nonincreasing, and $t_k\to0$ .
Families of gradients are indexed families (repeated vectors count as dependent); in MPEC-MFCQ an index of $I_{00}$ contributes both $\nabla G_i$ and $\nabla H_i$ . TNLP $(x^*)$ has constraints indexed by subtypes of the index sets; absent constraints are not padded by zero functions, which would make MPEC-MFCQ fail everywhere.
Definition 2.3(a) is printed with two misprints (" $\mu_ih_i(x^*)$ ", " $i=1,\dots,l$ " for the complementarity of $\lambda$ ); the formalization uses $\mu_i\nabla h_i(x^*)$ and $i=1,\dots,m$ . C-stationarity requires feasibility and one multiplier tuple satisfying both the weak-stationarity conditions and the sign condition on $I_{00}$ .
A "stationary point" that is merely a feasible point or a critical point of $f$ , or a C-stationarity whose sign condition refers to multipliers other than those of the weak-stationarity equation, would make the goal false or empty; neither reading is used. The hypotheses of the goal are jointly satisfiable (checked on the paper's Example 3.6 instance).
Infrastructure needed: theorems of the alternative (Motzkin/Farkas) for finite families in $\mathbb R^n$ , compactness of normalised multiplier sequences, continuity of gradients of $C^1$ maps. The NLP layer (positive-linear dependence, MFCQ, KKT points, Remark 2.2) is reusable for any constraint-qualification development. Contributions of proofs of the milestones, of general NLP lemmas, and of the goal are welcome.

Selected references

T. Hoheisel, C. Kanzow, A. Schwartz, Theoretical and numerical comparison of relaxation methods for mathematical programs with complementarity constraints, Preprint 299, Institute of Mathematics, University of Würzburg, September 2010; published in Math. Program. 137 (2013) 257–288. doi:10.1007/s10107-011-0488-5
S. Scholtes, Convergence properties of a regularization scheme for mathematical programs with complementarity constraints, SIAM J. Optim. 11 (2001) 918–936. doi:10.1137/S1052623499361233
Z.-Q. Luo, J.-S. Pang, D. Ralph, Mathematical Programs with Equilibrium Constraints, Cambridge University Press, 1996. doi:10.1017/CBO9780511983658

9 thms1 active userReviewed

Analysis Probability Stochastic Systems·Captain: mikedeng1

Law of Large Numbers Limits for Many-Server Queues 1: The Fluid Equations Have at Most One Solution, Given Explicitly by the Age Representation (3.11)Research Paper

Motivation

Large service systems such as call centers and hospital wards are modelled as many-server queues: $N$ identical servers, customers arriving according to a general process, service requirements drawn independently from a general distribution $G$ , and a single first-come-first-served queue. When $G$ is not exponential the number of customers in system is not Markov, and a tractable state must keep track of how long each customer in service has been served. Kaspi and Ramanan (Ann. Appl. Probab. 21 (2011)) take as state the number in system together with the age measure, the point measure of the ages of the customers in service, and prove a functional law of large numbers: scaled by $N$ , these processes converge to the unique solution of a deterministic system, the fluid equations. Earlier fluid and diffusion analyses of the $G/GI/N$ queue worked with other state descriptors (Reed, Ann. Appl. Probab. 19 (2009); Whitt, Oper. Res. 54 (2006)); the measure-valued description records the elapsed service time of every customer in service, which is the information a non-exponential service distribution requires.

This mission covers the deterministic half of that result: the fluid equations are well posed, and their solution is given in closed form.

Setting

Service requirements have a density $g$ that vanishes on $(-\infty,0)$ , $G(x)=\int_{(-\infty,x]}g$ , and the mean is normalized to one, $\int x\,g(x)\,dx=1$ . Let $M=\sup\{x\ge0: G(x)<1\}\in(0,\infty]$ and let $h=g/(1-G)$ be the hazard rate on $[0,M)$ ; $h$ is locally integrable on $[0,M)$ but not integrable on it. For a measure $\mu$ and a function $f$ write $\langle f,\mu\rangle=\int f\,d\mu$ , and $\mathbf 1$ for the constant one.

The data are a triple $(\bar E,\bar X(0),\bar\nu_0)$ in

\mathcal S_0=\{(f,x,\mu): f \text{ nondecreasing càdlàg}, f(0)=0;\ x\ge0;\ \mu \text{ a measure on }[0,M),\ \langle\mathbf 1,\mu\rangle\le1,\ 1-\langle\mathbf 1,\mu\rangle=[1-x]^+\},

where $\bar E$ is the cumulative arrival process, $\bar X(0)$ the initial number in system and $\bar\nu_0$ the initial age measure (per server, so the total capacity is one). A càdlàg pair $(\bar X,\bar\nu)$ , with $\bar\nu_t$ a sub-probability measure on $[0,M)$ in the weak topology, solves the fluid equations if for every $t\ge0$ : $\int_0^t\langle h,\bar\nu_s\rangle ds<\infty$ (3.4); for every test function $\varphi\in\mathcal C_c^{1,1}([0,M)\times\mathbb R_+)$

\langle\varphi(\cdot,t),\bar\nu_t\rangle=\langle\varphi(\cdot,0),\bar\nu_0\rangle+\int_0^t\langle\varphi_x+\varphi_s,\bar\nu_s\rangle ds-\int_0^t\langle h\varphi(\cdot,s),\bar\nu_s\rangle ds+\int_{[0,t]}\varphi(0,s)\,d\bar K(s)\quad(3.5);

$\bar X(t)=\bar X(0)+\bar E(t)-\bar D(t)$ (3.6); and the nonidling condition $1-\langle\mathbf 1,\bar\nu_t\rangle=[1-\bar X(t)]^+$ (3.7). Here $\bar D(t)=\int_0^t\langle h,\bar\nu_s\rangle ds$ is the cumulative departure process and $\bar K(t)=\langle\mathbf 1,\bar\nu_t\rangle-\langle\mathbf 1,\bar\nu_0\rangle+\bar D(t)$ the cumulative entry into service. Equation (3.5) is a weak form of a transport equation: mass moves to the right at unit speed, is killed at rate $h$ , and enters at age $0$ at rate $d\bar K$ .

Formalization targets

Goal: Theorem 3.5

For every $(\bar E,\bar X(0),\bar\nu_0)\in\mathcal S_0$ :

the fluid equations have at most one solution;
under (3.4) and the path conditions, $(\bar X,\bar\nu)$ is a solution if and only if it satisfies (3.6), (3.7) and, for every bounded continuous $f$ and $t\ge0$ ,

\langle f,\bar\nu_t\rangle=\int_{[0,M)}f(x+t)\frac{1-G(x+t)}{1-G(x)}\,\bar\nu_0(dx)+\int_{[0,t]}f(t-s)\big(1-G(t-s)\big)\,d\bar K(s);\quad(3.11)

if $\bar E$ has a density $\bar\lambda$ , then $\bar K$ has a density $\bar\kappa$ equal a.e. to $\bar\lambda$ where $\bar X<1$ , to $\bar\lambda\wedge\langle h,\bar\nu_t\rangle$ where $\bar X=1$ , and to $\langle h,\bar\nu_t\rangle$ where $\bar X>1$ (3.12);
if moreover $\bar\nu_0$ is absolutely continuous, so is every $\bar\nu_t$ .

Milestones

Remark 4.3, (4.4): integration by parts for the entry term of (4.3).
(4.55): the integrated hazard in closed form, $\psi_h(x,t)=(1-G(x))/(1-G(x-t))$ or $1-G(x)$ .
Theorem 4.1: for a Radon-measure-valued path satisfying the hazard bound (4.1), the age equation (4.2), which is (3.5) with an arbitrary Radon measure $\upsilon_0$ and an arbitrary $Z$ of bounded variation in place of $\bar\nu_0$ and $\bar K$ , holds if and only if the representation (4.3) holds.
Proof of Corollary 4.4: $\bar K$ is nondecreasing.
Corollary 4.4, (4.5): $\bar K(t)=\langle\mathbf 1,\bar\nu_t\rangle-\langle\mathbf 1,\bar\nu_0\rangle+\int\frac{G(x+t)-G(x)}{1-G(x)}\bar\nu_0(dx)+\int_0^tg(t-s)\bar K(s)ds$ .
Lemma 4.5: $\|\langle f,\bar\nu^2_s\rangle-\langle f,\bar\nu^1_s\rangle\|_T\le\|f\|_M|\Delta\upsilon_0|_{TV}+(2\|f\|_T+\|f'\|_T)\|\Delta Z\|_T$ .
Theorem 4.6: with equal initial measures, $\|\Delta\bar K\|_T\vee\|\Delta\bar D\|_T\le|\Delta\bar X(0)|+\|\Delta\bar E\|_T$ , together with (4.8) and (4.10).

Significance

Uniqueness of the fluid solution is what turns tightness of the scaled $N$ -server processes into convergence: every subsequential limit solves the fluid equations, so all coincide (the paper's Theorem 3.7). The representation (3.11) reduces the measure-valued equation to the scalar process $\bar K$ , and the continuity estimate of Theorem 4.6 says the fluid solution is a Lipschitz function of the arrival process. Both are used in the paper's study of long-time behaviour, where $\bar\nu_t$ converges to the measure with density $1-G$ , and (3.12) is the form of the entry rate used there.

The results are proved in the paper. None of them, and no part of the measure-valued fluid model, has a machine-checked proof. Formalizing them produces a checked weak-solution theory for a transport equation with an unbounded killing rate and a measure-valued boundary input, which is a reusable piece of infrastructure for other age- and residual-time-based queueing models.

Difficulty

The central step is Theorem 4.1. The naive approach treats (4.2) as a first-order PDE and integrates along characteristics, but the solution is only a càdlàg path of measures, $h$ is merely locally integrable and blows up near $M$ , and $Z$ may jump, so classical characteristics are not available; the test functions must not vanish on the boundary $x=0$ , since that is where the entry term lives. The second difficulty is in Theorem 4.6: the entry process $\bar K$ is defined implicitly through the nonidling condition, and comparing two solutions requires a first-crossing argument that distinguishes whether the system is below, at or above capacity at that time.

Formalization scope

The service law is its density $g$ (ServiceLaw), with $g=0$ below $0$ , $\int g=1$ and mean one. Time is $\mathbb R$ read on $[0,\infty)$ ; every condition is stated for $t\ge0$ . Measures of the fluid model are FiniteMeasure ℝ carried by $[0,M)$ , whose topology is weak convergence, so càdlàg paths are càdlàg in $\mathcal M_F[0,M)$ with the weak topology. The paths of Theorem 4.1 and Lemma 4.5 are ℝ → Measure ℝ with values Radon on $[0,M)$ (possibly infinite) and càdlàg in the vague topology. $M\in[0,\infty]$ is an extended number. The integral in (3.4) is a lower integral in $[0,\infty]$ , and $\bar D$ , $\bar K$ are its real value. $d\bar K$ is the Lebesgue–Stieltjes measure of $\bar K$ , with no atom at $0$ . A function $Z$ of bounded variation is a difference $Z_1-Z_2$ of nondecreasing càdlàg functions vanishing at $0$ .

Explicit choices: compact support of test functions is relative to $[0,M)\times\mathbb R_+$ , so $\varphi(0,s)$ need not vanish (with supports taken in $\mathbb R^2$ the entry term of (3.5) would vanish identically); $\bar\nu(0)=\bar\nu_0$ and $\bar X(0)$ equal to the datum are clauses of the fluid equations, but not of the age equation, where $\upsilon_0$ is arbitrary; functions in $\mathcal C_b(\mathbb R_+)$ , $\mathcal C_c(\mathbb R_+)$ and $\mathcal C^1_b(\mathbb R_+)$ are represented by functions on $\mathbb R$ of the same class, of which only values on $[0,\infty)$ are read; norms in Lemma 4.5 are computed in $[0,\infty]$ , since $|\Delta\upsilon_0|_{TV}$ may be infinite. Two printed statements are corrected: in Theorem 3.5 the paper's right-hand side of the equivalence lists (3.6) and (3.11); the nonidling condition (3.7), part of the fluid equations on the left, is kept on the right, as the proof requires. In (4.10), $\Delta\bar X(0)$ is replaced by $|\Delta\bar X(0)|$ , which is what Lemma 4.5 and (4.9) give.

A fluid solution is defined by the weak transport equation (3.5), never by the representation (3.11) or by a formula for $\bar\nu$ in terms of $\bar K$ ; with such a definition the equivalence of the goal would be an unfolding of definitions.

A complete development needs Lebesgue–Stieltjes integration by parts for càdlàg functions of bounded variation, the Riesz description of the vague topology, and uniqueness for weak solutions of transport equations; these are reusable beyond this mission. Proofs of any milestone, and of the parts of Theorem 3.5 separately, are welcome. The paper's Section 4.3 machinery (the abstract and simplified age equations, Lemmas 4.12–4.13, Propositions 4.15–4.16) is not posed here and may be formalized as supporting lemmas.

Selected references

H. Kaspi and K. Ramanan, Law of large numbers limits for many-server queues, Ann. Appl. Probab. 21(1) (2011), 33–114. https://doi.org/10.1214/09-AAP662
J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Ann. Appl. Probab. 19(6) (2009), 2211–2269. https://doi.org/10.1214/09-AAP609
W. Whitt, Fluid models for multiserver queues with abandonments, Oper. Res. 54(1) (2006), 37–54. https://doi.org/10.1287/opre.1050.0227
S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97236

10 thms1 active userReviewed

Algorithmic Game Theory Probability·Captain: mikedeng1

A Multiple-Choice Secretary Algorithm with Applications to Online Auctions: The Recursive k-Choice Secretary Algorithm Earns at Least (1 − 5/√k) Times the Sum of the k Largest ValuesResearch Paper

Motivation

The secretary problem asks how well an online decision maker can do when items arrive one at a time in random order and each must be accepted or rejected on the spot. With a single selection, the classical rule (observe a $1/e$ fraction, then take the first item better than everything seen) selects the best item with probability about $1/e$ , and no rule does better. Many allocation problems are not single-choice: a seller with $k$ identical goods facing bidders who arrive over time, an advertiser with a budget of $k$ impressions, an employer with $k$ openings. Each asks the multiple-choice secretary problem: how much of the best achievable total can an online rule collect when $k$ selections are allowed?

Kleinberg's 2005 SODA paper answered this for the sum objective. It gave a recursive algorithm whose expected total is at least $(1 - 5/\sqrt k)$ times the sum of the $k$ largest values, so the ratio tends to $1$ as $k$ grows, and stated a matching $1 - \Omega(\sqrt{1/k})$ upper bound for every algorithm, whose proof the extended abstract omits. The motivating application was online auctions: the algorithm becomes a strategyproof mechanism for selling $k$ identical items to bidders who arrive and depart over time, extending the single-item online auction of Hajiaghayi, Kleinberg and Parkes (EC 2004).

Timeline. Dynkin (1963) and the classical literature settle $k = 1$ with ratio $1/e$ . Hajiaghayi, Kleinberg and Parkes (2004) turn the single-item rule into an online auction. Kleinberg (2005) proves $1 - O(1/\sqrt k)$ for $k$ selections, with the explicit constant $5$ . Babaioff, Immorlica, Kempe and Kleinberg (2008) survey the resulting family of generalized secretary problems and their use in online auctions.

Setting

Let $S$ be a finite set of $n$ distinct non-negative real numbers. The elements of $S$ are revealed in a uniformly random order: each of the $n!$ orders has probability $1/n!$ . After each arrival the algorithm decides, irrevocably and using only the values seen so far, whether to select it. At most $k \ge 1$ elements may be selected. Write $T$ for the set of the $k$ largest elements of $S$ (all of $S$ if $k > n$ ) and

v = \sum_{x \in T} x

for their sum, the best total any rule could collect knowing $S$ in advance.

Kleinberg's algorithm $\mathcal A_k$ is defined by recursion on $k$ :

If $k = 1$ , use the classical rule: observe the first $\lfloor n/e \rfloor$ arrivals, then select the first later arrival that exceeds all earlier ones, if there is one.
If $k \ge 2$ , draw $m$ from the binomial distribution $B(n, 1/2)$ . Apply $\mathcal A_\ell$ , with $\ell = \lfloor k/2 \rfloor$ , to the first $m$ arrivals. Let $y_1 > y_2 > \dots > y_m$ be those $m$ values in decreasing order. After the $m$ -th arrival, select every arrival exceeding $y_\ell$ , until $k$ elements have been selected in total or the sequence ends.

The expected value of the algorithm is taken over the random order and over every binomial draw at every level of the recursion.

Formalization targets

Goal: Theorem 2.1

\mathbb E\Big[\sum_{x \text{ selected by } \mathcal A_k} x\Big] \;\ge\; \Big(1 - \frac{5}{\sqrt k}\Big)\, v \qquad \text{for every } S \subset \mathbb R_{\ge 0} \text{ finite and every } k \ge 1.

The statement is uniform in $n$ and $k$ ; it says nothing beyond the explicit constant $5$ printed in the paper.

Milestones: the claims of the proof sketch

The paper proves the theorem by induction on $k$ . Its sketch introduces $Y$ , the set of the first $m$ arrivals, $Z = S \setminus Y$ , the modified value of a set (the sum of its elements lying in $T$ ), and $q$ , the number of elements of $Z$ exceeding $y_\ell$ . The milestones are its stated claims, in order:

$Y$ is uniformly distributed on the $2^n$ subsets of $S$ .
$|Y \cap T|$ has the distribution $B(k, 1/2)$ .
Conditional on $|Y \cap T| = r$ , the expected modified value of $Y$ is $(r/k)v$ .
The displayed bound $\sum_{r=1}^{k}\Pr(|Y\cap T| = r)\,\frac{\min(r,\ell)}{k}\,v \ge \big(1 - \frac{1}{2\sqrt k}\big)\frac v2$ with $\ell = k/2$ .
The top $\ell = k/2$ elements of $Y$ have expected modified value at least $\big(1 - \frac{1}{2\sqrt k}\big)\frac v2$ .
$\mathbb E\,|q - \ell| \le \sqrt k$ .
The elements the algorithm selects from $Z$ have expected modified value at least $\big(\frac12 - \sqrt{1/k}\big)v$ .
The closing computation $\big(1 - \frac{5}{\sqrt{k/2}}\big)\big(1 - \frac{1}{2\sqrt k}\big)\frac12 + \frac12 - \sqrt{\frac1k} > 1 - \frac{5}{\sqrt k}$ .

Significance

The result. Theorem 2.1 shows that random arrival order costs only a $1 - O(1/\sqrt k)$ factor when many items are sold, against the constant $1/e$ for a single item. With the paper's matching upper bound, it pins down the optimal rate for the $k$ -choice problem. It is the base of the paper's strategyproof online auction for $k$ identical goods and a standard reference point for the later literature on secretary problems with combinatorial constraints and on online allocation in the random-order model.

Formalizing it. The paper is a two-page extended abstract, and the theorem's proof is a sketch: several steps are described as "easy", a stochastic-domination argument is stated without detail, and the behaviour of the algorithm when fewer than $\ell$ elements have been observed is not specified. A machine-checked proof would supply the complete argument for the explicit constant. The result is proved on paper only in this sketch; no machine-checked proof of it is known.

Difficulty

The obvious argument fixes $m = n/2$ and treats the threshold $y_\ell$ as if it split the remaining elements exactly. Both steps fail. With a fixed $m$ , the first $m$ arrivals are not a uniform subset of $S$ and $|Y \cap T|$ is hypergeometric, so the clean binomial computations of the sketch are not available; the binomial choice of $m$ is what makes $Y$ uniform. And the number $q$ of later elements beyond $y_\ell$ fluctuates by order $\sqrt k$ : the second phase may run out of budget before reaching all of $T \cap Z$ , or accept elements outside $T$ . Controlling this fluctuation, while the cap of $k$ also counts the first phase's selections, is the central step. The induction must then combine a recursive guarantee on a random, random-sized prefix with this estimate.

Formalization scope

The Lean development fixes these conventions.

$S$ is a Finset ℝ with all elements non-negative; distinctness is automatic. The arrival at time $t$ (0-based) under the order $\pi \in \mathrm{Perm}(\mathrm{Fin}\, n)$ is the $\pi(t)$ -th smallest element of $S$ , and expectations over the order use the published uniform average SecretaryWD.DiscUpper.uniformAvg.
The algorithm is a PMF over sets of selected positions, defined by well-founded recursion on $k$ . The base case is the published SecretaryWD.DiscUpper.classicalSecretary. $B(n, 1/2)$ is Mathlib's PMF.binomial (1/2). At $k = 0$ the algorithm selects nothing, for totality only; all statements assume $k \ge 1$ .
When the first phase has seen fewer than $\ell$ arrivals ( $m < \ell$ ), $y_\ell$ is taken to be $-\infty$ : every later arrival is selected until the cap. The page does not specify this case; under the reading "select nothing", the theorem fails when $n$ is much smaller than $k$ .
The cap of $k$ counts the selections of both phases. A cap applied to the second phase alone would let the algorithm select up to $k + \ell$ elements and is excluded.
The goal mentions only the algorithm, the order, $S$ , $k$ and $v$ . It does not mention $Y$ , $Z$ , $q$ or the modified value, which appear only in milestones, so the goal cannot be discharged by assuming any part of the sketch.
Three milestone hypotheses are added and disclosed: $k \le n$ for milestones 2, 3, 5 and 6 (for $n < k$ the law of $|Y \cap T|$ is $B(n, 1/2)$ , and milestone 6 fails); $k$ even for milestone 5 (the sketch writes $\ell = k/2$ ; for odd $k$ with $\ell = \lfloor k/2\rfloor$ the bound fails at $k = 3$ ). Milestone 4 uses the real number $\ell = k/2$ , as printed; with $\lfloor k/2\rfloor$ it fails for odd $k$ .

A complete development needs: the uniform-subset law of a binomially sized random prefix; conditional expectations over random subsets; tail and absolute-deviation bounds for sums of geometric variables and a stochastic-domination argument; and a careful treatment of the recursion through PMF.bind. The first and third are reusable beyond this mission, for other random-order and sample-based algorithms. Proofs of any milestone, of auxiliary lemmas about the random prefix, and of the goal by a route different from the sketch are all welcome.

Selected references

R. Kleinberg, A multiple-choice secretary algorithm with applications to online auctions, Proceedings of the 16th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2005.
M. T. Hajiaghayi, R. Kleinberg, D. C. Parkes, Adaptive limited-supply online auctions, Proceedings of the 5th ACM Conference on Electronic Commerce (EC), 2004, pp. 71–80. https://doi.org/10.1145/988772.988784
E. B. Dynkin, The optimum choice of the instant for stopping a Markov process, Soviet Mathematics Doklady 4, 1963.
T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493
M. Babaioff, N. Immorlica, D. Kempe, R. Kleinberg, Online auctions and generalized secretary problems, ACM SIGecom Exchanges, 2008. https://doi.org/10.1145/1399589.1399596

11 thms1 active userReviewed

Combinatorics Probability Random Matrix Theory·Captain: mikedeng1

Phase Transition of the Largest Eigenvalue for Nonnull Complex Sample Covariance Matrices 4: The Exponential Last Passage Time Has the Law of the Largest Sample EigenvalueResearch Paper

Motivation

Random growth models and random matrices share limit laws. The first exact instance was found by Johansson (Shape fluctuations and random matrices, Comm. Math. Phys. 2000), who showed that the last passage time of a lattice model with geometric or exponential weights has the law of the largest eigenvalue of a Laguerre (complex Wishart) random matrix. Baik, Ben Arous and Péché (Ann. Probab. 33 (2005)) extended the identity to weights whose rate depends on the row. On the matrix side this is a sample covariance matrix with a general population covariance $\Sigma$ ; on the growth side it is a corner growth model, or a series of exponential queues, with inhomogeneous service rates.

The identity is the reason the paper's main result, the phase transition of the largest sample eigenvalue as a few population eigenvalues ("spikes") cross the critical value $1 + \gamma^{-1}$ , is also a theorem about last passage percolation and tandem queues. In the queueing reading, a spike is a slow server, and the phase transition describes how slow a few servers must be before they change the centring and the fluctuation scale of the exit time.

Timeline:

2000, Johansson: equal rates; the geometric and exponential last passage time has the law of the largest Laguerre eigenvalue (his Proposition 1.4 is the case $\pi_1 = \cdots = \pi_N$ of (307)).
2001, Baryshnikov and, independently, Gravner, Tracy and Widom: the tandem-queue and GUE-minor descriptions of the same object.
2005, Baik, Ben Arous and Péché: row-dependent rates $\pi_i$ (Proposition 6.1), via the Robinson–Schensted–Knuth (RSK) formula for geometric weights (310) and a scaling limit.

Setting

Last passage time. Attach a real weight $X(i,j)$ to every site of the grid $\{1,\ldots,N\}\times\{1,\ldots,M\}$ . An up/right path from $(1,1)$ to $(N,M)$ is a sequence of $N+M-1$ sites starting at $(1,1)$ , ending at $(N,M)$ , each step adding $(1,0)$ or $(0,1)$ . The last passage time is

L(N,M) = \max_{\pi:(1,1)\nearrow(N,M)} \sum_{(i,j)\in\pi} X(i,j). \qquad (306)

Exponential environment. Given positive numbers $\pi_1,\ldots,\pi_N$ , the $X(i,j)$ are independent and $X(i,j)$ is exponential of mean $1/(\pi_iM)$ , i.e. density $\pi_iMe^{-\pi_iMx}$ on $x\ge0$ . All $M$ sites of row $i$ share one rate.

Sample covariance matrix. Let $g_{kj}$ , $1\le k\le M$ , $1\le j\le N$ , be independent standard complex Gaussians (real and imaginary parts independent $N(0,1/2)$ ). For a unitary $U$ and $\ell_j = \pi_j^{-1}$ (308), the samples $\vec y_k = U\,\mathrm{diag}(\sqrt{\ell_j})\,g_k$ are mean-zero complex Gaussian vectors with covariance $\Sigma = U\,\mathrm{diag}(\ell)\,U^*$ , and

S = \frac1M\sum_{k=1}^M \vec y_k\vec y_k^{\,*}, \qquad \lambda_1 = \text{largest eigenvalue of } S.

Schur functions and geometric weights. For a partition $\lambda$ , the Schur function $s_\lambda(x)$ is the sum over semistandard Young tableaux $T$ of shape $\lambda$ of $\prod_{c}x_{T(c)}$ . A geometric variable of parameter $q\in[0,1)$ has $\mathbb P(Y = k) = (1-q)q^k$ .

Formalization targets

Goal: Proposition 6.1

For $1\le N\le M$ , positive $\pi_1,\ldots,\pi_N$ and every unitary $U$ ,

\mathbb P\big(L(N,M)\le x\big) = \mathbb P\big(\lambda_1(M,N)\le x\big) \qquad \text{for all } x\in\mathbb R. \qquad (309)

The two sides are defined independently: one by a maximum over lattice paths of exponential weights, the other by the spectrum of a Gaussian random matrix.

Milestones

The recurrence (313): for every array of weights and every site with $a, b\ge2$ ,

L(a,b) = \max\{L(a-1,b), L(a,b-1)\} + X(a,b).

The Cauchy identity (311): $\sum_\lambda s_\lambda(x)s_\lambda(y) = \prod_{i,j}(1-x_iy_j)^{-1}$ for $x_i,y_j\ge0$ , $x_iy_j<1$ .
The geometric formula (310): for independent geometric weights $Y(i,j)$ of parameter $x_iy_j$ , $x_i,y_j\in[0,1)$ ,

\mathbb P\big(G(N,M)\le n\big) = \prod_{i,j}(1-x_iy_j)\sum_{\lambda:\lambda_1\le n}s_\lambda(x)s_\lambda(y).

The exponential formula (307): for $M\ge N$ and distinct $\pi_i$ ,

\mathbb P\big(L(N,M)\le x\big) = \frac1C\int_{[0,x]^N}\frac{\det(e^{-M\pi_i\xi_j})}{V(\pi)}V(\xi)\prod_{j}\xi_j^{M-N}\,d\xi.

Significance

The proposition makes every distributional statement about $\lambda_1$ in the paper a statement about last passage percolation with row-dependent rates: the $F_k$ (generalised Tracy–Widom) fluctuations at the critical spike value, the Gaussian fluctuations above it, and the fixed-dimension limit. Through (312)–(313) it also covers the exit time of $M$ customers from $N$ exponential servers in series, an operations research object. The geometric formula (310) is the entry point of the RSK method for exactly solvable growth models.

These results are proved in the literature; the paper cites (310) and (311) and derives (307) from them by a limit. None of them is machine-checked as far as this series knows. Formalizing them requires a Lean development of Schur functions, the Cauchy identity and the RSK correspondence on matrices with nonnegative integer entries, and of the Wishart eigenvalue density, each reusable well beyond this mission.

Difficulty

The recurrence (313) is elementary. Everything else is not. The geometric formula (310) needs the RSK bijection between nonnegative integer matrices and pairs of semistandard tableaux of the same shape, together with Schensted's theorem that the first row of the shape is the last passage time; neither is in Mathlib. The passage from (310) to (307) is a scaling limit $x_i = 1 - M\pi_i/L$ , $n = xL$ , $L\to\infty$ , in which a sum over partitions must converge to a multiple integral. The matrix side needs the joint eigenvalue density of a complex Wishart matrix with general $\Sigma$ , which uses the Harish-Chandra–Itzykson–Zuber integral. A direct coupling of the two sides is not known; the identity is an equality of laws, proved by computing both.

Formalization scope

The development lives in the namespace SpikedWishart.LastPassage. Conventions:

Sites and indices are 0-based; the paper's $(1,1)$ and $(N,M)$ are $(0,0)$ and $(N-1,M-1)$ , and $N, M\ge1$ .
$L$ is defined as the maximum over paths (306), never by the recurrence (313), so (313) is a genuine statement.
The exponential law is Mathlib's expMeasure with rate $\pi_iM$ .
The sample model is mean zero, uncentred, with factor $1/M$ and $\mathbb E|g|^2 = 1$ ; this is the model of (59), (61) and (307), and the page's centring by the sample mean and $S = (1/N)XX^*$ are printed slips. The covariance is $U\,\mathrm{diag}(\pi^{-1})U^*$ for every unitary $U$ ; specialising to diagonal $\Sigma$ would prove a special case.
$N\le M$ is a disclosed addition to the goal, matching the page's "for $M\ge N$ " in (307).
Proposition 6.1 prints $L(M,N)$ ; the object is (306)'s $L(N,M)$ .
Schur functions are the tableau sum with variables extended by zero. The Cauchy identity is stated with the exponent $-1$ that the page omits. In (307) the constant $C$ is the integral of the same integrand over $(0,\infty)^N$ , and the $\pi_i$ are distinct so that $V(\pi)\ne0$ ; the goal has no distinctness hypothesis.

A formalization in which either side of (309) is defined through the other, or through (307), would be trivial and is excluded: both laws are defined from scratch. Contributions are welcome on RSK and Schur function infrastructure, on the Wishart density, and on the measurability of $\lambda_1$ .

Selected references

J. Baik, G. Ben Arous, S. Péché, Phase transition of the largest eigenvalue for nonnull complex sample covariance matrices, Ann. Probab. 33(5):1643–1697, 2005. https://doi.org/10.1214/009117905000000233
K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209:437–476, 2000. https://doi.org/10.1007/s002200050027
Y. Baryshnikov, GUEs and queues, Probab. Theory Related Fields 119:256–274, 2001. https://doi.org/10.1007/PL00008760
J. Gravner, C. A. Tracy, H. Widom, Limit theorems for height fluctuations in a class of discrete space and time growth models, J. Stat. Phys. 102:1085–1132, 2001. https://doi.org/10.1023/A:1004879725949
R. P. Stanley, Enumerative Combinatorics, Vol. 2, Cambridge University Press, 1999 (the paper's reference [36] for the Cauchy identity). https://doi.org/10.1017/CBO9780511609589

9 thms1 active userReviewed

Combinatorics Linear Optimization Optimization·Captain: mikedeng1

Robust Branch-and-Cut-and-Price for the Capacitated Vehicle Routing Problem: The Integer Points of P1 ∩ P2 Are Exactly the CVRP Solutions, and the Dantzig–Wolfe Master Describes P1 ∩ P2Research Paper

Motivation

The capacitated vehicle routing problem (CVRP) asks for $K$ delivery routes from a depot that serve every client exactly once without exceeding a vehicle capacity, at minimum total length. It was introduced by Dantzig and Ramser in 1959 and is the reference problem of the vehicle routing literature: most exact methods for richer routing models (time windows, heterogeneous fleets, split deliveries) are first developed and benchmarked on it.

Exact CVRP algorithms are driven by the lower bound of a linear relaxation. Two families dominated before 2005. Branch-and-cut works with the edge variables $x_e$ and the rounded capacity inequalities (Lysgaard, Letchford and Eglese 2004, among others); its bound degrades as the number of vehicles grows. Lagrangean and column-generation methods work with q-routes, walks from the depot of bounded total demand that may revisit clients (Christofides, Mingozzi and Toth 1981). Fukasawa, Longo, Lysgaard, Poggi de Aragão, Reis, Uchoa and Werneck combine the two in one linear program over the intersection of the two polytopes, priced by column generation with every cut written on the edge variables. According to the abstract, the resulting branch-and-cut-and-price solves to optimality all instances from the literature with up to 135 vertices. The design is called robust because cuts are written on the edge variables $x$ and therefore never change the structure of the pricing problem.

This mission formalizes the formulation itself (§2 of the paper) and the two exact facts of its column generation (§3.1).

Setting

Let $G=(V,E)$ be an undirected graph on $V=\{0,1,\dots,n\}$ . Vertex $0$ is the depot; $V_+=\{1,\dots,n\}$ are the clients, client $i$ having a positive demand $d_i$ . Each edge has a length $\ell_e$ . There are $K$ vehicles of capacity $C$ , both positive integers.

A list of clients $r=(r_1,\dots,r_m)$ describes the closed walk $0\to r_1\to\cdots\to r_m\to 0$ . Its edge incidence $q^e(r)$ is the number of times the walk traverses $e$ (a one-client walk $0\to j\to 0$ traverses $\{0,j\}$ twice); its load is $d_{r_1}+\cdots+d_{r_m}$ , with repetitions.

A CVRP route visits pairwise distinct clients with load at most $C$ ; a CVRP solution is a family $R=(R_1,\dots,R_K)$ of routes visiting every client exactly once. Its edge vector is $\chi(R)_e=\sum_kq^e(R_k)$ .
A q-route without 2-cycles is a walk of load at most $C$ that may revisit clients but contains no subpath $i\to j\to i$ with $i\ne 0$ .

For $S\subseteq V$ , $\delta(S)$ is the set of edges with one end in $S$ , $x(\delta(S))=\sum_{e\in\delta(S)}x_e$ , and $k(S)=\lceil d(S)/C\rceil$ . The paper's constraints on $x\in\mathbb R^{E}$ and on weights $\lambda_j\ge 0$ of the q-routes $j$ are

\begin{aligned} &x(\delta(\{i\}))=2\ \ (i\in V_+)\ \ (1), && x(\delta(\{0\}))=2K\ \ (2), && x(\delta(S))\ge 2k(S)\ \ (S\subseteq V_+)\ \ (3),\\ &x_e\le 1\ \ (e\in E\setminus\delta(\{0\}))\ \ (4), && \textstyle\sum_jq^e_j\lambda_j=x_e\ \ (e\in E)\ \ (5), && \textstyle\sum_j\lambda_j=K\ \ (6). \end{aligned}

$P_1$ is $\{x\ge0:(1)\text{–}(4)\}$ ; $P_2$ is the set of $x\ge 0$ satisfying (1) together with some $\lambda\ge0$ satisfying (5), (6); the Explicit Master $P_3$ is the projection onto $x$ of the system (1)–(6) with one $\lambda$ . The Dantzig–Wolfe Master (DWM) is the LP in $\lambda$ alone obtained by substituting (5) into (1)–(4), giving the rows (8)–(11), with objective (7) $\sum_j\sum_e\ell_eq^e_j\lambda_j$ . The bounds are $L_i=\min_{x\in P_i}\ell^\top x$ .

Formalization targets

Goal: the formulation theorem

For a loop-free graph with positive demands and capacity, and arbitrary lengths:

x\in P_3\cap\mathbb Z^{E}\iff x=\chi(R)\ \text{for a CVRP solution }R, \qquad P_3=\{Q\lambda:\lambda\ \text{DWM-feasible}\}, \qquad L_1,\,L_2\ \le\ L_3\ \le\ \mathrm{OPT},

with (7) equal to $\ell^\top Q\lambda$ . The bounds are stated in lower-bound form: every lower bound of $\ell^\top x$ over $P_1$ or $P_2$ is one over $P_3$ , and every lower bound over $P_3$ is at most the cost of every solution.

Milestones

$P_3=P_1\cap P_2$ (p. 5).
Every CVRP route is a q-route without 2-cycles (p. 2).
Validity of (1)–(4): $\chi(R)\in P_1$ , with $\ell^\top\chi(R)$ the cost of $R$ (p. 4).
Validity of (5)–(6): $\chi(R)\in P_2$ , with the routes of $R$ as columns (p. 4).
Every integer point of $P_1$ is $\chi(R)$ for a solution $R$ (p. 4).
Constraint (6) is implied by (2) and (5) (p. 5).
The DWM (8)–(11) is (1)–(4) on $x=Q\lambda$ (p. 5).
A generic cut $\sum_ea_ex_e\ge b$ becomes $\sum_j(\sum_ea_eq^e_j)\lambda_j\ge b$ (p. 5).
Every integer point of $P_2$ is $\chi(R)$ for a solution $R$ (p. 4).
The reduced cost of a column is $\sum_e\bar c_eq^e$ (§3.1, p. 6).
Scaling: a q-route for demands $\lceil d_v/g\rceil$ and capacity $\lfloor C/g\rfloor$ is a q-route for $(d,C)$ (§3.1, p. 7).

Significance

The formulation theorem is what makes the algorithm exact: integer points of $P_3$ are solutions, so branching on $x$ terminates at an optimum, and $P_3$ is a relaxation, so $L_3$ is a valid bound that dominates both classical bounds. The DWM description is what makes it computable: $P_3$ is optimized by column generation over q-routes, and milestones 8 and 10 show that any cut on $x$ can be added without changing the pricing problem, which remains a shortest q-route problem with edge costs $\bar c_e$ .

The paper proves none of these claims formally; most are stated in a sentence, and milestone 9 is stated with "It can be shown" and no proof. To our knowledge none of them has a machine-checked proof. A formal development produces a library of walks, edge incidences, cut values and column families on a general graph that later missions on branch-cut-and-price (subset-row cuts, ng-routes, other routing variants) can import.

Difficulty

Most items are linear-algebra bookkeeping on finite sums, but they require a working theory of walks: edge incidences along a closed walk, the cut value of an incidence vector, and the fact that a walk from the depot crosses every client set an even number of times. The integrality statements (milestones 5 and 9 and goal part 1) are the hard part: an integer vector satisfying degree constraints need not come from routes through the depot, and the statements must exclude every other structure. For $P_2$ there are no capacity cuts at all, so the capacity of the routes must be recovered from the columns, and the paper states this case without proof. The obvious reduction "an integer point of $P_2$ is an integer combination of q-routes" fails: $\lambda$ may be fractional even when $x$ is integral.

Formalization scope

Vertices are Fin (n+1) with depot 0; edges are Sym2 (Fin (n+1)); the graph is an edge set E assumed loop-free where needed. Edge vectors are functions on all unordered pairs that vanish off E, which encodes $x\in\mathbb R^{|E|}$ . Demands $d$ , $K$ and $C$ are natural numbers; positive demands, $K>0$ and $C>0$ (the paper's standing assumptions, p. 1) are carried by the integrality statements and the goal, while $\ell\ge0$ is used by no statement and is omitted. Loads count repeated visits. The cut value $x(\delta(S))$ , the demand $d(S)$ and $k(S)=\lceil d(S)/C\rceil$ are the published definitions LysgaardCVRP.Shrink.cut, .demand and .roundedCapacityBound. The matrix $Q$ is replaced by finitely supported weights on client lists ranging over all q-routes without 2-cycles. $L_1,L_2,L_3$ and OPT are never real infima, since $P_3$ is empty for infeasible instances.

Three trivializations are ruled out by construction: $P_3$ is defined from the Explicit Master display, not as $P_1\cap P_2$ ; a CVRP solution is defined by its routes, not as an integer point of a polytope; and the columns are not a fixed finite list, which would turn $P_2$ into a restricted master.

The strictness of "CVRP routes $\subsetneq$ q-routes" (p. 2) depends on the instance and is not stated. Contributions of reusable lemmas on walks and cut values of incidence vectors are welcome, as are proofs of any milestone.

Selected references

R. Fukasawa, H. Longo, J. Lysgaard, M. Poggi de Aragão, M. Reis, E. Uchoa and R. F. Werneck, Robust branch-and-cut-and-price for the capacitated vehicle routing problem, Mathematical Programming 106 (2006); accepted manuscript. https://doi.org/10.1007/s10107-005-0644-x
N. Christofides, A. Mingozzi and P. Toth, Exact algorithms for the vehicle routing problem, based on spanning tree and shortest path relaxations, Mathematical Programming 20 (1981). https://doi.org/10.1007/BF01589353
J. Lysgaard, A. N. Letchford and R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming 100 (2004). https://doi.org/10.1007/s10107-003-0481-8
G. B. Dantzig and J. H. Ramser, The truck dispatching problem, Management Science 6 (1959). https://doi.org/10.1287/mnsc.6.1.80

17 thms1 active userReviewed

Algorithmic Game Theory Linear algebra·Captain: mikedeng1

Flows and Decompositions of Games: Harmonic and Potential Games 1: Every Finite Game Decomposes Uniquely into Potential, Harmonic and Nonstrategic ComponentsResearch Paper

Motivation

Potential games (Monderer and Shapley, 1996) are the finite games whose incentives are captured by a single function on strategy profiles: every unilateral change of strategy changes the deviator's payoff by exactly the change of a common potential. They have pure Nash equilibria, and natural learning dynamics such as better-reply and fictitious play converge in them. Most games are not potential games, however, and before Candogan, Menache, Ozdaglar and Parrilo there was no canonical way to say how far a given game is from one, or what the remainder looks like.

Their paper (arXiv:1005.2405; Math. Oper. Res. 36(3), 2011) answers this by viewing a game as a flow on a graph. The payoff differences between profiles that differ in one player's strategy form an edge flow on the game graph, and the classical Helmholtz (Hodge) decomposition of edge flows into gradient, harmonic and curl parts (Jiang, Lim, Yao, Ye, 2011) pulls back to a decomposition of the game itself. Every finite game becomes the sum of a potential game, a harmonic game and a component that carries no strategic information. The decomposition is the basis for the rest of the paper (equilibria of harmonic games, projections onto potential games, approximate equilibria) and for later work on dynamics in near-potential games.

Setting

Fix a finite set of players $\mathcal M$ and, for each player $m$ , a finite nonempty strategy set $E^m$ with $h_m = |E^m|$ elements. A strategy profile is $p = (p^m)_m \in E = \prod_m E^m$ , and $p^{-m}$ denotes the strategies of the players other than $m$ . A game is a family of utilities $u = (u^m)_m$ with $u^m : E \to \mathbb R$ , so the space of games is $\mathcal G_{\mathcal M,E} \cong C_0^{\mathcal M}$ , where $C_0 = \{E \to \mathbb R\}$ with $\langle \varphi,\psi\rangle_0 = \sum_p \varphi(p)\psi(p)$ .

Two profiles are $m$ -comparable if they are distinct and differ only in player $m$ 's strategy. The game graph has the profiles as nodes and an edge between comparable profiles. An edge flow is a function $X : E\times E\to\mathbb R$ that is antisymmetric on edges and zero off edges; the space $C_1$ of edge flows carries $\langle X,Y\rangle_1 = \tfrac12\sum_{(p,q)\text{ edge}} X(p,q)Y(p,q)$ . Triangular flows $C_2$ live on ordered 3-cliques.

The operators are: the gradient $(\delta_0\varphi)(p,q) = W(p,q)(\varphi(q)-\varphi(p))$ , with $W$ the edge indicator; the curl $(\delta_1X)(p,q,r) = X(p,q)+X(q,r)+X(r,p)$ on 3-cliques; the per-player gradient $(D_m\varphi)(p,q) = W^m(p,q)(\varphi(q)-\varphi(p))$ , with $W^m$ the indicator of $m$ -comparability; and $D : C_0^{\mathcal M}\to C_1$ , $Du = \sum_m D_m u^m$ , the flow of pairwise comparisons of $u$ . Adjoints are written ${}^*$ and Moore–Penrose pseudoinverses ${}^\dagger$ . The space $C_0^{\mathcal M}$ carries the unweighted inner product $\sum_m\langle u^m,v^m\rangle_0$ . Further, $\Delta_1 = \delta_1^*\delta_1+\delta_0\delta_0^*$ , $\Delta_{0,m} = D_m^*D_m$ , $\Pi_m = D_m^\dagger D_m$ , and $\Pi = \operatorname{diag}(\Pi_1,\dots,\Pi_M)$ .

A game is normalized if $\sum_{p^m} u^m(p^m,p^{-m}) = 0$ for all $p^{-m}$ and $m$ (Definition 4.1). The potential, harmonic and nonstrategic subspaces are (Definition 4.2)

\mathcal P = \{u \mid u = \Pi u,\ Du\in\operatorname{im}\delta_0\},\qquad \mathcal H = \{u \mid u = \Pi u,\ Du\in\ker\delta_0^*\},\qquad \mathcal N = \ker D .

Formalization targets

Goal: Theorem 4.1

\mathcal G_{\mathcal M,E} = \mathcal P\oplus\mathcal H\oplus\mathcal N,

and every game $u$ splits as $u = u_P + u_H + u_N$ with

u_P = D^\dagger\delta_0\delta_0^\dagger Du\in\mathcal P,\quad u_H = D^\dagger(I-\delta_0\delta_0^\dagger)Du\in\mathcal H,\quad u_N = (I-D^\dagger D)u\in\mathcal N,

where $\varphi = \delta_0^\dagger Du$ is a potential function of $u_P$ , i.e. $Du_P = \delta_0\varphi$ .

Milestones

Theorem 3.1 (Helmholtz decomposition), on an arbitrary finite graph: $C_1 = \operatorname{im}\delta_0\oplus\ker\Delta_1\oplus\operatorname{im}\delta_1^*$ , orthogonally, with $\ker\Delta_1 = \ker\delta_1\cap\ker\delta_0^*$ .
Lemma 4.1: $\Delta_{0,m} = h_m\Pi_m$ .
Lemma 4.2: $\ker D_m = \ker\Pi_m = \ker\Delta_{0,m}$ , with an explicit basis indexed by $E^{-m}$ .
Lemma 4.4 (i)–(v): $D_m^\dagger = \tfrac1{h_m}D_m^*$ ; $(\sum_iD_i)^\dagger D_j = (\sum_iD_i^*D_i)^\dagger D_j^*D_j$ ; $D^\dagger = [D_1^\dagger;\dots;D_M^\dagger]$ ; $\Pi = D^\dagger D$ ; $DD^\dagger\delta_0 = \delta_0$ .
Lemma 4.5: $u$ normalized $\iff$ $\Pi_mu^m = u^m$ for all $m$ $\iff$ $\Pi u = u$ $\iff$ $u\in(\ker D)^\perp$ .

Lemma 4.6 (the unique normalized game with the same pairwise comparisons is $\Pi u$ ) is included as a supporting theorem.

Significance

The decomposition turns questions about a game into questions about its three components. The potential component inherits the equilibrium and convergence theory of potential games. The harmonic component has a sharply different structure: harmonic games generically have no pure equilibrium, and in each of them the uniformly mixed profile is a mixed equilibrium. The nonstrategic component does not affect any equilibrium notion. The closed-form expressions also give the potential game closest to a given game, and with it bounds relating the approximate equilibria of the two games. The other missions of this series formalize those consequences; all of them rest on the operator layer and the subspaces defined here.

Theorem 4.1 is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces graph-flow infrastructure that Mathlib does not yet have: edge and triangular flows with their inner products, the combinatorial gradient and curl, the Helmholtz decomposition of a finite graph, and an operator Moore–Penrose pseudoinverse on finite-dimensional inner product spaces. The paper leaves Theorem 3.1 to the literature, so a full development needs a proof of it. The pseudoinverse identities of Lemma 4.4 also have a short appendix argument in the paper that a formal proof has to make complete.

Difficulty

The decomposition is not orthogonal decomposition along a single map. The subspaces $\mathcal P$ and $\mathcal H$ are defined through $\Pi$ , which is assembled player by player from the $D_m$ , while the flow conditions involve $\delta_0$ and the combined operator $D$ . Connecting the two requires the player operators to have mutually orthogonal ranges ( $D_k^*D_m = 0$ for $k\ne m$ ) and the explicit form of $D_m^*D_m$ as a scaled projection. Without these, $\Pi = D^\dagger D$ (Lemma 4.4 (iv)) and $DD^\dagger\delta_0 = \delta_0$ (Lemma 4.4 (v)) are not available, and they are what make the formulas for $u_P$ and $u_H$ land in $\mathcal P$ and $\mathcal H$ . A direct attempt to apply the Helmholtz decomposition to $Du$ produces a flow decomposition, not a game decomposition; the pullback through $D$ is not formal, because $D$ is neither injective nor surjective.

Formalization scope

Players form a Fintype ι; strategy sets are E : ι → Type with Fintype, DecidableEq and Nonempty instances, and $h_m$ is Fintype.card (E m). Profiles are ∀ m, E m, and $(q^m,p^{-m})$ is Function.update p m q. The game graph is a Mathlib SimpleGraph; comparability requires $p\ne q$ , so the graph has no loops, as the Laplacian (15) requires. $C_0$ is EuclideanSpace ℝ on profiles. $C_1$ and $C_2$ are type synonyms of the subspaces of antisymmetric (resp. alternating) functions, with inner products built from (7), including the factor $\tfrac12$ on $C_1$ . Lemma 4.4 (i) fails without it. The space of games is PiLp 2 of copies of $C_0$ , whose inner product is the unweighted sum used on p. 14, not the weighted inner product of the paper's Section 6. Adjoints are LinearMap.adjoint. The pseudoinverse is defined explicitly as the inverse of $L$ on $(\ker L)^\perp$ composed with the orthogonal projection onto $\operatorname{im}L$ .

$\mathcal P$ , $\mathcal H$ and $\mathcal N$ are defined by (28), not as the ranges of the component maps; the direct-sum part of the goal is stated independently of the formulas, so the goal cannot be satisfied by construction. Lemma 4.4 is split into five items, one per identity. "Orthogonal decomposition" in Theorem 3.1 is stated as pairwise orthogonality plus spanning. The paper's statements have no hypotheses beyond the setting, and none were added except nonemptiness of the strategy sets, which the paper assumes by writing $E^m = \{1,\dots,h_m\}$ .

Welcome contributions: a proof of the Helmholtz decomposition on a finite simple graph, general facts about the pseudoinverse (Penrose identities, $L^\dagger L$ is the projection onto $(\ker L)^\perp$ , invariance under rescaling of inner products), and the explicit adjoint formulas (12) and (22).

Selected references

O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Mathematics of Operations Research 36(3):474–503, 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044
X. Jiang, L.-H. Lim, Y. Yao, Y. Ye, Statistical Ranking and Combinatorial Hodge Theory, Mathematical Programming 127:203–244, 2011. https://arxiv.org/abs/0811.1067
R. Penrose, A generalized inverse for matrices, Mathematical Proceedings of the Cambridge Philosophical Society 51(3):406–413, 1955. https://doi.org/10.1017/S0305004100030401

13 thms1 active userReviewed

Operations Research

Missions

Robust Dynamic Programming 2: The Discounted Robust Value Function Is the Unique Fixed Point of the Robust Bellman OperatorResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 2(b)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Primal and Dual Linear Decision Rules in Stochastic and Robust Optimization 3: In Multistage Programs, the Primal and Dual Linear Decision Rule Problems Equal the LPs (4.2) and (4.6)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 22)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Machine Scheduling with Precedence Constraints 1: LP-Based Delayed List Scheduling Is a (1 + β)(1 + 1/β + max{1, (m − 1)Δ/m})-Approximation for P|r_j, prec|E[Σ w_j C_j]Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Primal and Dual Linear Decision Rules in Stochastic and Robust Optimization 1: With Fixed Recourse, the Primal and Dual Linear Decision Rule Problems Equal the LPs (2.3) and (2.8)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 10)

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Conditional Risk Mappings: A Positively Homogeneous Lower Semicontinuous Conditional Risk Mapping Is the Supremum of Countably Many Conditional ExpectationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 11)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Theoretical and Numerical Comparison of Relaxation Methods for Mathematical Programs with Complementarity Constraints 3: Kadrani et al. Relaxation Limits Are M-Stationary under MPEC-CPLDResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.5

Milestones, in proof order

Significance

Difficulty

Formalization scope

Selected references

A Branch-and-Cut Algorithm for the Dial-a-Ride Problem: The Generalized Order-Matching Inequality x(H) + Σ x(T_h) ≤ |H| + Σ|T_h| − 2m Is Valid for Every Feasible Route PlanResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 5 (p. 578)

Milestones (the steps of the proof of Proposition 5)

Companion statements

Significance

Difficulty

Formalization scope

Selected references

Validity of Heavy Traffic Steady-State Approximations in Generalized Jackson Networks: Scaled Stationary Queue Lengths Converge to the Stationary Distribution of the Reflected Brownian MotionResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8 (p. 18)

Milestones

Significance