Motivation

The job shop scheduling problem asks for a nonpreemptive schedule of jobs on machines, each job a fixed sequence of operations with prescribed machines and processing times, that minimizes the time at which the last operation completes. It is one of the most studied hard problems of combinatorial optimization: even very constrained versions are strongly NP-hard (Lawler, Lenstra, Rinnooy Kan and Shmoys, 1993), and for any $\rho<5/4$ a $\rho$-approximation when the number of machines is part of the input would imply $\mathrm{P}=\mathrm{NP}$ (Williamson et al., 1997).

When the number $m$ of machines and the maximum number $\mu$ of operations per job are fixed, Jansen, Solis-Oba and Sviridenko (2003) gave a linear time approximation scheme, improving the earlier $(2+\varepsilon)$-approximation of Shmoys, Stein and Wein (1994). The scheme follows a pattern that recurs throughout scheduling approximation: split the jobs by length into a constant number of big jobs, which are scheduled by enumeration on a coarse time grid, and many tiny jobs, which are assigned fractionally to time intervals by a linear program, then rounded. The mathematical hinge of this pattern in the paper is Lemma 1: the interval linear program loses nothing against the optimum of the grid-restricted problem.

Setting

An instance has machines $M_1,\dots,M_m$ and jobs $J_1,\dots,J_n$. Job $J_j$ is a sequence of $\mu_j$ operations $O_{1j},\dots,O_{\mu_j j}$, processed in this order; $O_{ij}$ runs without interruption on machine $M_{\pi_{ij}}$ for $p_{ij}\ge 0$ time units, and $\mu=\max_j\mu_j$. A feasible schedule assigns start times $S_{ij}\ge 0$, with completion times $C_{ij}=S_{ij}+p_{ij}$, so that $C_{ij}\le S_{i+1,j}$ and two distinct operations on the same machine do not overlap. Its makespan is $\max_{ij}C_{ij}$, and $C^*_{\max}$ is the optimum makespan.

The load of $M_t$ is $P_t=\sum_{\pi_{ij}=t}p_{ij}$, with $P_{\max}=\max_tP_t$; the length of $J_j$ is $l_j=\sum_i p_{ij}$. Fix $0<\varepsilon<1$ and $\alpha$ with $\varepsilon^{\lceil m/\varepsilon\rceil}\le\alpha\le\varepsilon$. The jobs split into the big jobs $B=\{l_j\ge\alpha P_{\max}\}$, the small jobs $S=\{\alpha\varepsilon P_{\max}<l_j<\alpha P_{\max}\}$ and the tiny jobs $T=\{l_j\le\alpha\varepsilon P_{\max}\}$.

The horizon $H=(1+\mu m\varepsilon)mP_{\max}$ is cut into $N=\lceil m(1+\mu m\varepsilon)/(\alpha\varepsilon)\rceil$ equal intervals of the first type. A schedule is restricted if every operation of a big job starts at the beginning of one of them. The small jobs are removed, and $\widetilde C^*_{\max}$ is the optimum makespan of the restricted schedules of $B\cup T$.

Given a restricted schedule of the big operations, let $A$ be the set of their start and completion times, sorted as $a_1<\dots<a_{|A|}$, with $a_0=0$ and $a_{|A|+1}=C$. The intervals of the second type are $[a_k,a_{k+1})$, of length $\Delta_k$, and $\Delta_{tk}$ is $0$ if a big operation occupies machine $M_t$ during interval $k$ and $\Delta_k$ otherwise. For a tiny job, $K_j$ is the set of nondecreasing tuples $(k_1,\dots,k_{\mu_j})$ in $\{0,\dots,|A|\}$. The interval LP (3)–(5) asks for $x_{jK}\ge 0$ with

$$\sum_{K\in K_j}x_{jK}=1\ (J_j\in T),\qquad \sum_{J_j\in T}\sum_{K\in K_j}\sum_{i:\,k_i=k,\ \pi_{ij}=t}p_{ij}\,x_{jK}\le\Delta_{tk}\ \ \text{for all } t,k.$$

Formalization targets

Goal: Lemma 1

For $C=\widetilde C^*_{\max}$ the interval LP is feasible for some restricted schedule of the big operations:

$$\exists\,\sigma\ \text{feasible and restricted on } B:\quad a_{|A|}\le\widetilde C^*_{\max}\le(1+\mu m\varepsilon)mP_{\max}\ \text{ and (3)–(5) has a solution.}$$

Milestones

The milestones are the facts of Sections 2–2.2 on which the goal's objects rest, in attack order:

$$P_{\max}\le C^*_{\max},\qquad C^*_{\max}\le mP_{\max},$$ $$\exists k\in\{1,\dots,\lceil m/\varepsilon\rceil\}:\ \sum_{J_j\in S_k}l_j\le\varepsilon P_{\max}\quad(\alpha=\varepsilon^k),\tag{1}$$ $$|B|\le m/\alpha\le m\varepsilon^{-\lceil m/\varepsilon\rceil},$$ $$\text{restricted schedules exist and }\ \widetilde C^*_{\max}\le C^*_{\max}+\mu m\varepsilon P_{\max}\le(1+\mu m\varepsilon)C^*_{\max},$$ $$|A|\le 2\mu|B|\le 2\mu m/\alpha.\tag{2}$$

Significance

Lemma 1 is what makes the algorithm's search correct: among the constantly many grid schedules of the big operations, one admits a fractional placement of all tiny operations into the second-type intervals within length $\widetilde C^*_{\max}$. Together with the restriction bound it gives $C_{\min}\le\widetilde C^*_{\max}\le(1+\mu m\varepsilon)C^*_{\max}$ for the least feasible LP length $C_{\min}$, the starting point of the rounding and of the final approximation guarantee. The same big/tiny split with an interval LP recurs in later schemes for flow shops, open shops and multiprocessor tasks, and the definitions here (operation chains, loads, grid-restricted schedules, the interval LP) are the substrate those results would share.

The paper's proofs are informal: the restriction bound is a shifting argument stated in two sentences, and the proof of Lemma 1 is an iterative decomposition of a schedule into LP variables that is not spelled out at interval boundaries or for zero-length operations. No machine-checked formalization of job shop scheduling, of these bounds, or of the lemma is known to exist. This mission produces one for the O(·)-free core of Section 2.

Difficulty

The obvious reading of Lemma 1 ("take an optimal restricted schedule and read off the fractions") hides three steps. First, $\widetilde C^*_{\max}$ is defined as an infimum over a continuum of schedules, and an optimal restricted schedule has to be shown to exist. Second, the fractions of each tiny operation over the second-type intervals must be recombined into weights on nondecreasing tuples, one tuple per job, so that the equality (3) holds and each operation's mass in each interval is reproduced exactly; this is where the precedence between operations of one job enters. Third, the bound (4) needs that on any machine a second-type interval is either fully covered by one big operation or free of big operations, which relies on $A$ containing every start and completion time.

Formalization scope

Machines are Fin m, jobs Fin n, the operations of job $j$ are Fin (μ j), all 0-based; processing times are real and nonnegative, with no integrality or positivity assumed, and consecutive operations may share a machine. $\mu$ is defined as $\max_j\mu_j$. $P_{\max}$ is a maximum over the machines, the makespan a maximum over the operations of the scheduled jobs, and $C^*_{\max}$, $\widetilde C^*_{\max}$ are infima (sInf) of makespans over feasible, respectively feasible restricted, schedules. $\widetilde C^*_{\max}$ refers to the jobs $B\cup T$ with $P_{\max}$, $\alpha$, $\varepsilon$ of the full instance. $A$ is a set (duplicates collapse), sorted with Finset.orderEmbOfFin. A big operation is processed in interval $k$ when its execution interval meets $[a_k,a_{k+1})$ in positive length. The LP's range condition $C\in[a_{|A|},(1+\mu m\varepsilon)mP_{\max}]$ is part of the feasibility predicate. The hypotheses $m\ge2$, $\mu\ge1$ (stated in the paper), $\varepsilon<1$ and $P_{\max}>0$ (implicit in it) are explicit binders. Eq. (1) is stated with $1\le k\le\lceil m/\varepsilon\rceil$ where the paper writes $k\le m/\varepsilon$.

Not formalized. Theorems 1–3 of the paper (the algorithm is a PTAS, a linear time approximation scheme, and its preemptive variant) and Lemma 2 are statements about running time. They need a cost model, the Grigoriadis–Khachiyan LP solver and Sevastianov's algorithm as black boxes, and without a cost model their approximation half is witnessed by an optimal schedule. They are out of scope and are not stated in any form. In particular, "for every $\varepsilon$ there is a schedule of makespan at most $(1+\varepsilon)C^*_{\max}$" is trivially true and is not what this mission asks. The goal cannot be satisfied by a degenerate big-operation schedule: the schedule must be feasible, start on the grid, and finish by $\widetilde C^*_{\max}$, and the LP keeps the equality in (3), the monotone tuples and the right-hand side $\Delta_{tk}$.

Contributions welcome: proofs of the milestones, a proof that optimal restricted schedules exist (finitely many machine orders and grid positions), and a general lemma decomposing a chain of fractional interval assignments into monotone tuples, reusable for other interval-LP schemes.

Selected references

• K. Jansen, R. Solis-Oba, M. Sviridenko, Makespan minimization in job shops: A linear time approximation scheme, SIAM J. Discrete Math. 16(2):288–300, 2003. https://doi.org/10.1137/S0895480199363908
• D. B. Shmoys, C. Stein, J. Wein, Improved approximation algorithms for shop scheduling problems, SIAM J. Comput. 23(3):617–632, 1994. https://doi.org/10.1137/S0097539791220817
• S. V. Sevastianov, G. J. Woeginger, Makespan minimization in open shops: A polynomial time approximation scheme, Math. Programming 82:191–198, 1998. https://doi.org/10.1007/BF01585871
• D. P. Williamson et al., Short shop schedules, Operations Research 45(2):288–294, 1997. https://doi.org/10.1287/opre.45.2.288
• E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, D. B. Shmoys, Sequencing and scheduling: Algorithms and complexity, Handbooks in OR & MS 4:445–522, 1993. https://doi.org/10.1016/S0927-0507(05)80189-6

Motivation

Stochastic quasigradient (SQG) methods minimize an expectation $F(x)=E_\omega f(x,\omega)$ over a constraint set $X\subseteq\mathbb R^n$ when neither $F$ nor its gradient can be computed, only random vectors whose conditional mean is (close to) a subgradient. They are the workhorse of stochastic programming and, under the name stochastic gradient descent, of large-scale statistical learning. The classical convergence theory, going back to Robbins and Monro (1951) and to Ermoliev's quasi-Féjer analysis, asks the stepsizes to be chosen in advance with $\rho_s\to0$, $\sum\rho_s=\infty$, $\sum\rho_s^2<\infty$. Uryasev, in Chapter 18 of Numerical Techniques for Stochastic Optimization (Ermoliev and Wets, eds., 1988), points out that such programmed rules are slow in practice, and that practitioners want adaptive stepsizes computed on line from the observed directions.

Timeline:

• 1951: Robbins and Monro, stochastic approximation with programmed steps.
• 1976: Ermoliev, Methods of Stochastic Programming: the SQG projection method and its a.s. convergence through stochastic quasi-Féjer sequences.
• 1983: Mirzoakhmedov and Uryasev (Zh. Vychisl. Mat. i Mat. Fiz., cited as [7] in Ch. 18 and [14] in Ch. 17): Cesàro convergence of the weighted mean with $\rho_s\to0$ and $\sum\rho_s=\infty$ only, under the two measurability regimes. Chapter 17 states it as Theorem (ii); Chapter 18 as Theorem 1.
• 1988: Uryasev, Ch. 18, applies it to the adaptive rule (18.5) (Theorem 2).
• 1992: Polyak and Juditsky, averaging of iterates for smooth stochastic approximation, with optimal asymptotic variance.

Setting

Let $X\subseteq\mathbb R^n$ be nonempty, convex and compact, $C_1=\max_{x,y\in X}\|x-y\|$ its diameter, and $F$ convex on an open convex set $U\supseteq X$, with subdifferential $\partial F(x)$. The projection $\pi_X(y)$ is the point of $X$ nearest to $y$. On a probability space, the SQG method generates

$$x^{s+1}=\pi_X(x^s-\rho_s\xi^s),\qquad s=0,1,\dots\qquad(18.2)$$

from $x^0\in X$, where the direction $\xi^s$ is a stochastic quasigradient: $E(\xi^s\mid B_s)=F_x(x^s)+b^s$ with $F_x(x^s)\in\partial F(x^s)$, a bias $b^s$, and $B_s$ the $\sigma$-algebra induced by $(x^0,\dots,x^s,\xi^0,\dots,\xi^{s-1})$.

The adaptive stepsize rule of the chapter is, for fixed $a>1$, $\delta>0$ and $\rho_0>0$,

$$\rho_{s+1}=\rho_s\,a^{\langle\xi^{s+1},\,x^s-x^{s+1}\rangle-\delta\rho_s}\qquad(18.5).$$

The step grows when consecutive moves point the same way and shrinks otherwise. The weighted (Cesàro) averages are

$$\bar x^s=\sum_{\ell=0}^s\rho_\ell x^\ell\Big/\sum_{\ell=0}^s\rho_\ell\qquad(18.6).$$

The sequence $x^s$ is Cesàro convergent when $\bar x^s$ converges to the solution set.

Chapter 17 (Pflug) uses the same method for $f(x)=E_P\,q(x,\xi)$ over a closed convex $S\subseteq\mathbb R^k$, with $Y=\nabla q(X_n,\xi_n)$ from i.i.d. $\xi_n$ and stepsizes adapted to $\sigma(\xi_0,\dots,\xi_{n-1})$.

Formalization targets

Goal: Theorem 2 of Chapter 18

Under $\sup_s\|\xi^s\|<C_2$ (18.15), $\limsup\|b^s\|\le\bar b$ (18.16) and $\delta>C_2\limsup_s\inf_{h\in\partial F(x^s)}\|\xi^s-h\|$ (18.17), almost surely,

$$\limsup_{s\to\infty}\Big(F(\bar x^s)-\min_{x\in X}F(x)\Big)\le\bar b\,C_1,$$

and if $b^s\to0$ a.s., then $F(\bar x^s)\to\min_XF$ and all accumulation points of $\bar x^s$ are minimizers, almost surely.

Milestones

1. Chapter 17, Theorem (i): $\sum\rho_n=\infty$ and $\sum\rho_n^2<\infty$ a.s. imply $X_n\to x^*$ a.s.
2. Chapter 17, Theorem (ii): for convex $f$ and bounded $S$, $\rho_n\to0$ and $\sum\rho_n=\infty$ a.s. imply $\bar X_n\to x^*$ a.s.
3. Chapter 18, Theorem 1: for any stepsizes with $\rho_s>0$, $E\rho_s^2<\infty$, $\rho_s\to0$, $\sum\rho_s=\infty$ and measurability condition (1) or (2), $\limsup F(\bar x^s)-F(x^*)\le\bar bC_1$ a.s.
4. Chapter 18, Corollary: with $b^s\to0$, the accumulation points of $\bar x^s$ are solutions.
5. Eq. (18.18): $\|x^{s+1}-x^s\|\le\|\rho_s\xi^s\|\le\rho_sC_2$.
6. Proof of Theorem 2, step 1: the adaptive steps satisfy $\sum\rho_s=\infty$.
7. Proof of Theorem 2, step 2: under (18.17), $\rho_s\to0$.
8. End of step 2: $\rho_s\to0$ implies $\rho_{s+1}/\rho_s\to1$.

Significance

Theorem 2 is a convergence guarantee for a stepsize rule that is computed from the run itself. It needs no square summability of the steps, and it tolerates a nonvanishing bias at a cost linear in the bias. This is the regime of practical SQG codes; §18.4–18.5 of the chapter discuss implementation and numerical experiments. Theorem 1 isolates the reason: Cesàro convergence needs only $\rho_s\to0$ and $\sum\rho_s=\infty$. It also allows a stepsize that depends on the current direction, provided consecutive steps have ratio tending to $1$.

The volume proves none of the probabilistic results in full. Theorem 1 of Chapter 18 is cited from Uryasev's earlier report. Theorem 2 has an outline proof that reduces it to Theorem 1. Chapter 17 gives a sketch through the Robbins–Siegmund lemma. None of these results is formalized. The mission produces machine-checked statements of all of them, with the misprints of the page resolved, and it separates the pathwise part of the Theorem 2 argument (steps 1 and 2, which are deterministic) from the martingale part (Theorem 1).

Difficulty

The obvious route to a.s. convergence is the quasi-Féjer or Robbins–Siegmund argument. It controls $\|x^s-x^*\|^2$ and needs $\sum\rho_s^2\|\xi^s\|^2<\infty$, which is exactly what is not available here. The averaged analysis has to show that the martingale term $\sum_\ell\rho_\ell\langle\xi^\ell-E(\xi^\ell\mid B_\ell),x^*-x^\ell\rangle$ is $o(\sum_\ell\rho_\ell)$ almost surely, and that $\sum_\ell\rho_\ell^2\|\xi^\ell\|^2$ is $o(\sum_\ell\rho_\ell)$, when the stepsizes are themselves random. Under condition (2) of Theorem 1, $\rho_s$ is not even measurable with respect to the $\sigma$-algebra of the conditional expectation. So $E(\rho_s\xi^s\mid B_s)\ne\rho_sE(\xi^s\mid B_s)$, and the standard decomposition breaks. For the adaptive rule, the stepsizes are coupled to the iterates through the exponent. Neither $\sum\rho_s=\infty$ nor $\rho_s\to0$ is given, and both must be derived path by path.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Sequences are indexed from $0$. Chapter 17 is shifted by one against the page: its $X_n,\xi_n,\mathcal F_n$, $n\ge1$, become indices $n-1$. Conditional expectations are Mathlib's condExp with respect to the history $\sigma$-algebras of the definition file. Every $\limsup$ bound is written out as "for every $\varepsilon>0$, eventually $\dots\le\dots+\varepsilon$", or in (18.17) as a bound $L$ with $C_2L<\delta$. Expectations of squared norms are lower Lebesgue integrals. The deterministic proof steps (items 5 to 8) are stated for one sample path.

Readings of the page, each recorded in the item's Formalization Note:

• (18.17) prints $C_1$. The proof's estimate gives $(C_2C_s-\delta)\rho_s$, and only $C_2$ is invariant under rescaling of $\mathbb R^n$, so $C_2$ is stated.
• (18.5) has two forms that agree only without projection. The proof uses the second, $a^{\langle\xi^{s+1},x^s-x^{s+1}\rangle-\delta\rho_s}$, which is stated.
• (18.8) prints $F_s(x^s)$ for $F_x(x^s)$. (18.11) prints $E\rho_s^s$, read as $E\rho_s^2<\infty$.
• Theorem 2's "$F(x^s)-\min z\in XF(x)\to0$" is read as $F(\bar x^s)-\min_XF\to0$.
• The end of step 2 prints $\rho_{s+1}/\rho_s\to0$, read as $\to1$.
• Chapter 17, assumption (ii) prints $\|\nabla f(x)\|\le A+B\|x-x^*\|^2$. The proof uses $\|\nabla f(x)\|^2$, and the printed form makes part (i) false, so the squared form is stated. $\mathrm{Var}(Y_x)\le C$ is read as $E\|Y_x-EY_x\|^2\le C$.
• The Corollary adds lower semicontinuity of $F$ on $X$, without which it fails.
• $x^0\in X$ is assumed, and $\rho_0$ in Theorem 2 is a fixed positive number.

No explicit constants replace an O(·) or an unspecified "C": every constant appears in the book's statements.

A trivializing formalization states Theorem 2 for arbitrary stepsizes satisfying (18.10)–(18.13), which is Theorem 1 again. Here the stepsizes are tied to the iterates by (18.5), and the $\delta$ of (18.17) is the $\delta$ of the rule.

Needed infrastructure: a Robbins–Siegmund almost-supermartingale lemma, which Mathlib does not have; a strong law for martingale differences with random weights (Kronecker's lemma in its stochastic form); nonexpansiveness of the projection onto a closed convex set; and nonemptiness of the subdifferential of a finite convex function on an open set. The first two are reusable across stochastic approximation. Contributions of any of the milestones, or of these lemmas as separate theorems, are welcome.

Selected references

• G. Ch. Pflug, Stepsize Rules, Stopping Times and their Implementation in Stochastic Quasigradient Algorithms, in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer 1988, Ch. 17. https://doi.org/10.1007/978-3-642-61370-8
• S. Uryasev, Adaptive Stochastic Quasigradient Procedures, ibid., Ch. 18. https://doi.org/10.1007/978-3-642-61370-8
• Yu. Ermoliev, Stochastic Quasigradient Methods, ibid., Ch. 6. https://doi.org/10.1007/978-3-642-61370-8
• F. Mirzoakhmedov and S. P. Uryasev, Adaptive step size control for stochastic optimization algorithm, Zh. Vychisl. Mat. i Mat. Fiz. 23(6) (1983) 1314–1325 (in Russian); cited in the volume above, no online copy linked.
• H. Robbins and S. Monro, A Stochastic Approximation Method, Ann. Math. Statist. 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586
• H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• B. T. Polyak and A. B. Juditsky, Acceleration of Stochastic Approximation by Averaging, SIAM J. Control Optim. 30 (1992) 838–855. https://doi.org/10.1137/0330046

Motivation

Decisions under uncertainty are often required to satisfy a constraint $\theta \in \Theta_\delta$ that depends on a random parameter $\delta$, and requiring it for every possible $\delta$ is usually too conservative or infeasible. The scenario approach replaces the unknown distribution of $\delta$ by $N$ independent samples (scenarios) and enforces only the sampled constraints; its generalization theorem (Campi and Garatti, 2008) bounds the probability that the resulting decision violates a fresh constraint.

Enforcing all $N$ sampled constraints can still be costly: a few unusual scenarios may dominate the solution. A practitioner therefore often discards $k$ of the sampled constraints, optimally, greedily or at random, and re-solves. The question is what guarantee survives: the removed constraints were chosen by looking at the data, so the solution is biased towards points of higher risk. Campi and Garatti (2011) answered it with a bound that holds for every removal procedure. This mission formalizes that answer as it is presented in Chapter 3, Section 3.3 and Chapter 5, Section 5.3 of the textbook Introduction to the Scenario Approach (Campi and Garatti, SIAM/MOS 2018), together with its explicit corollary, Theorem 1.2. Applications include chance-constrained control, portfolio selection and prediction, where discarding scenarios trades a controlled amount of risk for a better cost.

Setting

A decision $\theta$ ranges over $\mathbb R^d$ (in Lean, EuclideanSpace ℝ (Fin d)), with a closed convex domain $\Theta$ and a linear cost $c^{\mathsf T}\theta$. An uncertain parameter $\delta$ takes values in a measurable space $\Delta$ with probability $\mathbb P$, and each $\delta$ determines a closed convex constraint set $\Theta_\delta$. The violation probability of a decision is

$$V(\theta) = \mathbb P\{\delta \in \Delta : \theta \notin \Theta_\delta\}.$$

Given independent samples $\delta_1,\dots,\delta_N$ with joint law $\mathbb P^N$, the scenario program minimizes $c^{\mathsf T}\theta$ over $\theta \in \Theta \cap \bigcap_{i=1}^N \Theta_{\delta_i}$. For a set $I$ of indexes, the program without the constraints in $I$ minimizes the same cost over $\Theta \cap \bigcap_{i \notin I} \Theta_{\delta_i}$; its solution is written $\theta^*_I$. A removal procedure selects, as a function of the whole sample, a set of $k$ indexes, and $\theta^*_k$ denotes the solution of the program without them. The procedure is required to output a solution that violates exactly the $k$ removed constraints (with probability one): a removed constraint that turns out to be satisfied is reinstated and another is removed. Two standing assumptions are used throughout: Assumption 3.4, that $\Theta$ and every $\Theta_\delta$ are convex and closed, and Assumption 3.6, that for every sample size $m$ and every sample the scenario program has exactly one solution.

Formalization targets

Goal: Theorem 3.9

For $N \ge d$, under Assumptions 3.4 and 3.6, for every removal procedure and every $\varepsilon \in [0,1]$,

$$\mathbb P^N\{V(\theta^*_k) > \varepsilon\} \le \binom{k+d-1}{k} \sum_{i=0}^{k+d-1} \binom Ni \varepsilon^i (1-\varepsilon)^{N-i}.$$

The bound depends on the problem only through $d$, and on the removal procedure not at all. For $k = 0$ it is Theorem 3.7.

Milestones

1. Theorem 3.7 (no removal): $\mathbb P^N\{V(\theta^*) > \varepsilon\} \le \sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$, used for the program with the $N-k$ kept constraints.
2. Eq. (5.11): up to a zero probability set, the event $\{V(\theta^*_k) > \varepsilon\}$ is contained in the union over all $k$-element index sets $I$ of the events "$\theta^*_I$ violates all constraints in $I$ and $V(\theta^*_I) > \varepsilon$".
3. Eq. (5.13): for a fixed $I$, the probability of that event equals $\int_{(\varepsilon,1]} \alpha^k F_V(d\alpha)$, where $F_V$ is the law of $V(\theta^*_I)$.
4. Eq. (5.14) and Theorem 3.9 for $d = 2$: the book's complete proof in the plane.
5. Eqs. (3.15)–(3.17) and the conclusion of Section 3.3.1: with the explicit level $\varepsilon_k$ of (1.9), the right-hand side of (3.13) is at most $\beta$.
6. Theorem 1.2: with probability at least $1-\beta$, $V(\theta^*_k) \le \varepsilon_k$, where

$$\varepsilon_k = \frac{k}{N} + \left[\frac{\sqrt k}{N} + \frac{\sqrt k+1}{N}\left((d-1)\ln(k+d-1) + \frac{d-1}{\sqrt k} + \ln\frac1\beta\right)\right].$$

Significance

Theorem 3.9 certifies every constraint-removal heuristic at once. Since the guarantee is the same for optimal, greedy and random removal, a user may pick the removal strategy purely for cost, and may inspect several values of $k$ before choosing, paying only a union bound over the values tried (Section 3.3). Theorem 1.2 turns the bound into an explicit rate: when $k/N$ is held fixed, the violation exceeds the empirical risk $k/N$ by a margin of order $\ln N/\sqrt N$, only slightly worse than the $1/\sqrt N$ rate for estimating the probability of a fixed event. The result also shows that the violation after removal concentrates around the target level, which is the basis of the book's comparison between sampling-and-discarding and simply using fewer scenarios (Example 3.10).

Theorem 3.9 is proved in the literature for general $d$ (Campi and Garatti, 2011); the textbook proves it for $d = 2$. To our knowledge no part of the scenario approach has a machine-checked proof. A formal development would supply the first verified version of the removal bound, a Lean treatment of solution maps of random convex programs, and reusable combinatorial and binomial-tail estimates.

Difficulty

The removed set is chosen after seeing the data, so the kept constraints are not an independent sample and Theorem 3.7 cannot be applied to $\theta^*_k$ directly. The argument must pass through all $\binom Nk$ fixed index sets and account for the event that the removed constraints are violated; a plain union bound that ignores this event loses a factor $\binom Nk$ and does not give (3.13). For a fixed index set, the probability that the $k$ removed scenarios are all violated involves the distribution of $V(\theta^*_I)$, which is only known to be dominated by a Beta law, so a stochastic-domination argument for the increasing function $\alpha \mapsto \alpha^k$ is needed. In general dimension the combinatorial constant $\binom{k+d-1}{k}$ comes from a sharper counting than the two-dimensional computation of Section 5.3, and that argument is in the cited paper rather than in the book.

Formalization scope

Decisions live in EuclideanSpace ℝ (Fin d), samples of size $m$ are maps Fin m → Δ with law Measure.pi (fun _ => P) for a probability measure P, and the violation is the real number (P {δ | θ ∉ Θδ δ}).toReal. Events over samples are compared in ℝ≥0∞ with ENNReal.ofReal of the book's right-hand side. The removal procedure is an arbitrary map I : (Fin N → Δ) → Finset (Fin N) with (I ω).card = k, and θk is a map that, for every sample, solves the program without the constraints in I ω, and violates each of them with probability one. The following implicit hypotheses of the book are written as binders:

• $d \ge 1$, $d \le N$, $k \le N$ and $\varepsilon \in [0,1]$;
• Assumption 3.6 for every $m$, including $m = 0$, and for every sample (not almost every);
• the removed constraints are violated with probability one (∀ᵐ ω ∂ℙ^N), the book's own hypothesis on p. 65, so (5.11) is an inclusion up to a null set as on the page; requiring the violation for every sample would be unsatisfiable for $1 \le k < N$ (on a sample with all $\delta_i$ equal a kept constraint coincides with a removed one) and would make the results vacuous;
• measurability, which the book glosses over (p. 33): the constraint relation $\{(\theta,\delta) : \theta \in \Theta_\delta\}$ is jointly measurable, the solution map of the scenario program with $m$ constraints is measurable for every $m$, and $\theta^*_k$ is measurable;
• for Theorem 1.2 and Section 3.3.1: $k \ge 1$ (formula (1.9) divides by $\sqrt k$), $N \ge 1$, $\beta \in (0,1)$; Section 3.3.1 additionally assumes $\varepsilon_k \le 1$, the range in which its chain of inequalities holds.

Theorem 1.2 is stated in the constraint formulation of Chapter 3, to which the book says it "straightforwardly generalizes" (p. 20), with the hypotheses of Theorem 3.9 from which Section 3.3.1 derives it. Eq. (5.14) and the closing display of Section 5.3 are stated for $d = 2$ only, as in the book.

A trivializing formalization is excluded: the removal procedure is universally quantified, the solutions are exact minimizers rather than arbitrary feasible points, and the event is the strict $V(\theta^*_k) > \varepsilon$; a statement for one fixed rule, or with $\theta^*_k$ unconstrained, would be a different theorem.

A complete development needs: product measures and Fubini over Fin N → Δ, reindexing of the kept constraints as a sample of size $N-k$, the Beta form of the binomial tail (the platform's binomial_upper_tail_eq_incomplete_beta is available), and stochastic domination for monotone integrands. Solution-map and violation infrastructure is shared with the sibling missions of this series. Contributions on any milestone, including the general-$d$ counting argument of the cited paper, are welcome.

Selected references

• M. C. Campi and S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018. https://doi.org/10.1137/1.9781611975444
• M. C. Campi and S. Garatti, A sampling-and-discarding approach to chance-constrained optimization: feasibility and optimality, Journal of Optimization Theory and Applications 148(2), 257–280, 2011. https://doi.org/10.1007/s10957-010-9754-6
• M. C. Campi and S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3), 1211–1230, 2008. https://doi.org/10.1137/07069821X
• G. C. Calafiore and M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5), 742–753, 2006. https://doi.org/10.1109/TAC.2006.875041

Motivation

The scenario approach turns an optimization problem under uncertainty into a finite, data-driven program: sample $N$ instances of the uncertain parameter, optimize against all of them, and certify how often the resulting design fails on a new instance. Its main guarantee (Theorem 3.7 of Campi and Garatti's Introduction to the Scenario Approach) bounds the probability of failure by a binomial tail in $N$ and in the number $d$ of optimization variables. To reach a failure level $\varepsilon$ with confidence $1-\beta$, the number of scenarios grows roughly like $\frac{2}{\varepsilon}\big(\ln\frac1\beta+d-1\big)$ (Theorem 1.1 of the book). The product of $d$ and $1/\varepsilon$ is what makes medium- and large-scale designs expensive: each scenario is one more constraint in the program that has to be solved.

FAST (Fast Algorithm for the Scenario Technique), introduced by Carè, Garatti and Campi in Operations Research 62 (2014), removes that product. It solves the program with a moderate number $N_1$ of scenarios and then, instead of re-optimizing, raises the returned cost level until it covers $N_2$ further scenarios. The book presents the algorithm and its guarantee, Theorem 8.5, in §8.3, and refers to the paper for the proof. This mission formalizes that guarantee.

Timeline:

• 2006, Calafiore and Campi: violation bounds for the solution of convex scenario programs.
• 2008, Campi and Garatti: the exact binomial bound, tight for fully supported problems (Theorem 3.7 of the book).
• 2014, Carè, Garatti and Campi: FAST and its two-stage bound, Eq. (8.5).
• 2018, Campi and Garatti's textbook, §8.3, the source of this mission.

Setting

Let $\Delta$ be a measurable space carrying a probability measure $\mathbb P$, and let $\ell(\nu,\delta)$ be a real loss of a decision $\nu\in\mathbb R^{d-1}$ under the uncertain parameter $\delta\in\Delta$. As a standing assumption of the book, $\ell(\cdot,\delta)$ is convex for every $\delta$.

Given scenarios $\delta_1,\dots,\delta_m$ drawn independently from $\mathbb P$, the scenario program (1.4) is

$$\min_{\nu\in\mathbb R^{d-1}}\ \Big[\max_{i=1,\dots,m}\ \ell(\nu,\delta_i)\Big].$$

Its solution is $\nu^*$ and its optimal value $\ell^*$. Assumption 3.6 requires that for every $m$ and every sample the solution exist and be unique. The pair $(\nu,\ell)$ has $d$ components, and $d$ is the number that enters every bound.

The risk (Definition 8.2) of a decision $\nu$ with cost level $\ell$ is

$$R(\nu,\ell)=\mathbb P\{\delta\in\Delta:\ \ell(\nu,\delta)>\ell\},$$

the probability that a new instance costs more than promised. It is the violation $V(\nu,\ell)$ of the epigraphic constraint $\ell\ge\ell(\nu,\delta)$.

FAST takes $N_1+N_2$ independent scenarios. It solves (1.4) with the first $N_1$ of them, obtaining $\nu^*_{N_1}$. In the detuning step it then sets

$$\ell^*_F=\max_{i=1,\dots,N_1+N_2}\ \ell(\nu^*_{N_1},\delta_i),$$

the smallest level that covers every scenario seen. The output is $(\nu^*_F,\ell^*_F)$ with $\nu^*_F=\nu^*_{N_1}$.

Formalization targets

Goal: Theorem 8.5, Eq. (8.5)

For every $\varepsilon\in[0,1]$,

$$\mathbb P^{N_1+N_2}\{V(\nu^*_F,\ell^*_F)>\varepsilon\}\ \le\ (1-\varepsilon)^{N_2}\sum_{i=0}^{d-1}\binom{N_1}{i}\varepsilon^i(1-\varepsilon)^{N_1-i}.$$

No relation between $N_1$ and $d$ is required. When $N_1<d$ the sum equals $1$ and the bound reads $(1-\varepsilon)^{N_2}$.

Milestone: Theorem 3.7 for program (1.4)

The first stage is an ordinary scenario program with $N_1$ scenarios. For $N\ge d$,

$$\mathbb P^N\{R(\nu^*,\ell^*)>\varepsilon\}\ \le\ \sum_{i=0}^{d-1}\binom{N}{i}\varepsilon^i(1-\varepsilon)^{N-i},$$

that is, $R(\nu^*,\ell^*)$ is dominated by a $B(d,N-d+1)$ distribution (recalled on p. 90).

Milestone: the $N_2$ rule

For $\varepsilon,\beta\in(0,1)$, $N_2\ge\frac1\varepsilon\ln\frac1\beta$ makes the right-hand side of (8.5) at most $\beta$ (p. 95).

Significance

The result. Theorem 8.5 makes the guarantee of the scenario approach cheap to obtain. With $N_1=Kd$ (the book suggests $K\approx20$) and $N_2\ge\frac1\varepsilon\ln\frac1\beta$, the total number of scenarios is $Kd+\frac1\varepsilon\ln\frac1\beta$. This is additive in $d$ and $1/\varepsilon$ rather than multiplicative, and the added $N_2$ scenarios cost only function evaluations, not a larger optimization. The price is suboptimality: $\ell^*_F$ is in general higher than the value a classical scenario program with the same confidence would return.

Formalizing it. The result is proved on paper, in the cited 2014 article; the book states it without proof. No part of the scenario theory has been machine-checked on this platform, as far as a search of the catalog shows. The mission produces a checked two-stage bound whose first stage is the loss-function form of Theorem 3.7, which is reusable by every mission of the series that works with program (1.4). The $N_2$ rule is an elementary but explicit sample-size certificate.

Difficulty

The obvious route treats the detuning step as a fresh scenario program with $N_1+N_2$ scenarios and applies Theorem 3.7 to it. That fails: $\nu^*_F$ is not the solution of that program, and Theorem 3.7 with $N_1+N_2$ scenarios gives a bound that is not of the product form (8.5). The level $\ell^*_F$ depends on all $N_1+N_2$ scenarios at once, including those that determined $\nu^*_{N_1}$, and the map $c\mapsto R(\nu,c)$ is monotone but need not be continuous, so the event $V(\nu^*_F,\ell^*_F)>\varepsilon$ is not a simple event about the new scenarios. Underneath the goal sits Theorem 3.7 itself, which is the main theorem of the book and whose proof occupies Chapter 5.

Formalization scope

Lean representation:

• The decision space $\mathbb R^{d-1}$ is EuclideanSpace ℝ (Fin n); the book's $d$ is written $n+1$, never with natural-number subtraction.
• A sample of size $m$ is ω : Fin m → Δ with law Measure.pi (fun _ => P), and the same $\mathbb P$ defines the risk. FAST draws one sample ω : Fin (N₁ + N₂) → Δ; its first stage is ω ∘ Fin.castAdd N₂.
• The maximum in (1.4) and in $\ell^*_F$ is Finset.sup' over a nonempty index set. $\ell^*_F$ runs over all $N_1+N_2$ scenarios, not over the $N_2$ new ones only.
• The risk is (P {δ | c < ℓ ν δ}).toReal, with the strict inequality of Definition 8.2 and the strict event $V>\varepsilon$ of (8.5). Probabilities of sample events are compared in ℝ≥0∞ through ENNReal.ofReal.
• The first-stage solution is a map νstar from samples to decisions, with the hypothesis that νstar ω₁ solves the program for every sample ω₁.

Hypotheses the book leaves implicit, stated explicitly:

1. $\ell(\cdot,\delta)$ is convex for every $\delta$ (standing assumption, p. 6).
2. Existence and uniqueness of the solution (Assumption 3.6) for every $m\ge1$ and every sample. The program with no scenario has no minimum, so $m=0$ is excluded.
3. $N_1\ge1$, since the first stage needs a scenario.
4. $\varepsilon\in[0,1]$; for $\varepsilon>1$ the factor $(1-\varepsilon)^{N_2}$ can be negative.
5. The loss is jointly measurable in $(\nu,\delta)$ and the first-stage solution map is measurable. The book glosses over measurability (p. 6, footnote 1; p. 33).

A formalization that bounds only the $N_2$ new scenarios is ruled out, because $\ell^*_F$ is defined as a maximum over all $N_1+N_2$ scenarios. So is one that takes $\ell^*_F$ as a free variable or drops Assumption 3.6: the goal is stated for the output of FAST as the book defines it.

A complete development needs the scenario program in loss form, product-measure conditioning on $\Delta^{N_1}\times\Delta^{N_2}$, and Theorem 3.7. The loss-form Theorem 3.7 is the reusable piece. Proofs of the milestones and of intermediate conditioning lemmas are welcome.

Selected references

• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM, 2018, §8.3 and Theorem 3.7. https://doi.org/10.1137/1.9781611975444
• A. Carè, S. Garatti, M. C. Campi, FAST—Fast Algorithm for the Scenario Technique, Operations Research 62(3):662–671, 2014. https://doi.org/10.1287/opre.2014.1257
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3):1211–1230, 2008. https://doi.org/10.1137/07069821X
• G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5):742–753, 2006. https://doi.org/10.1109/TAC.2006.875041

Motivation

Two-player turn-based stochastic games (2TBSGs) model a zero-sum contest on a finite graph with random transitions: in each state one player chooses an action, pays its cost, and a lottery chooses the next state. The minimizer and the maximizer both evaluate the total discounted cost. The model contains Markov decision processes (one player), simple stochastic games, mean-payoff and parity games (as limits or reductions), which makes it central to algorithmic game theory, verification and operations research. Shapley introduced discounted stochastic games in 1953 (PNAS).

The standard algorithm for solving them is strategy iteration, the two-player generalization of Howard's policy iteration (1960): improve player 1's strategy greedily against the best response of player 2, and repeat. Whether any algorithm solves 2TBSGs in strongly polynomial time was open for decades.

Timeline. Howard (1960) introduced policy iteration for MDPs. Rao, Chandrasekaran and Nair (1973) described strategy iteration for discounted stochastic games. Littman (1996) gave a polynomial but not strongly polynomial bound via value iteration. Ye (2011, Math. of OR) proved that policy iteration for discounted MDPs with a fixed discount factor is strongly polynomial, using the linear programming formulation of MDPs. Hansen, Miltersen and Zwick (2010, arXiv:1008.0530; J. ACM 2013) extended the bound to strategy iteration for 2TBSGs, where no LP formulation is available, and improved Ye's bound. Friedmann (2009) showed that without discounting, or with the discount factor as part of the input, strategy iteration can take exponentially many iterations.

Setting

A game $G$ has a finite set $S$ of $n$ states, split into the states $S_1$ of player 1 (the minimizer) and $S_2 = S \setminus S_1$ of player 2 (the maximizer), a finite set $A$ of $m$ actions of both players, and a discount factor $0 < \gamma < 1$. Each action $a$ has a source state $s(a)$, a probability distribution $P_{a,\cdot}$ over next states, and a cost $c(a) \in \mathbb{R}$. Every state $i$ has a nonempty set $A_i = \{a : s(a) = i\}$ of actions.

A positional strategy of player $j$ picks one action $\pi_j(i) \in A_i$ for every state $i \in S_j$; a profile is a pair $\pi = (\pi_1, \pi_2)$, viewed as a map $\pi : S \to A$. With $(P_\pi)_{i,j} = P_{\pi(i),j}$ and $(c_\pi)_i = c(\pi(i))$, the value vector

$$v_\pi = \sum_{k \ge 0} \gamma^k P_\pi^k c_\pi \in \mathbb{R}^S$$

is the expected total discounted cost from each initial state. Vectors are compared componentwise. A profile is optimal when each strategy is an optimal counter-strategy against the other, from every initial state simultaneously. All optimal profiles share one value vector $v^*$.

The Strategy-Iteration algorithm starts from a strategy $\sigma^0$ of player 1. In round $k$ it takes an optimal counter-strategy $\tau_2(\sigma^k)$ of player 2, evaluates $v^k = v_{\sigma^k,\tau_2(\sigma^k)}$, and lets $\sigma^{k+1}$ choose in every state $i \in S_1$ an action minimizing $c(a) + \gamma \sum_j P_{a,j} v^k_j$ over $A_i$. Ties are broken in favour of $\sigma^k$. It stops at the first $N \ge 1$ with $\sigma^N = \sigma^{N-1}$.

Formalization targets

Goal: Theorem 6.5

For every game, every map $\tau_2$ returning optimal counter-strategies, and every run from any initial strategy, the termination index $N$ exists, $(\sigma^N, \tau_2(\sigma^N))$ is optimal, and

$$N \le (m+1)\Big(1 + \log_{1/\gamma} \frac{n^2}{1-\gamma}\Big).$$

For a fixed $\gamma$ this is $O\big(\frac{m}{1-\gamma}\log\frac{n}{1-\gamma}\big)$ iterations. The explicit constant is the paper's statement, and the goal states it rather than the $O(\cdot)$ form.

Milestones

The milestone list follows the paper's lemma chain: Shapley's existence theorem (Thm 2.8); the linear-algebra form of values (Lemma 3.2); the modified costs $c^\pi = c - (J - \gamma P)v_\pi$ and their properties (Lemmas 3.6, 3.7); the flux vectors (Lemmas 3.10, 3.12); the contraction of the value iteration operator and geometric convergence (Lemmas 4.2, 4.8); monotonicity, correctness and the rate of strategy iteration (Lemmas 5.1, 5.2, 5.3, 5.5); and the combinatorial core (Lemmas 6.2, 6.3, 6.4).

Significance

The result. The theorem gives the first strongly polynomial algorithm for 2TBSGs with a fixed discount factor. The iteration count depends only on $n$, $m$ and $\gamma$, not on the bit length of the costs or probabilities. With $S_2 = \emptyset$ the map $\tau_2$ is trivial and the theorem is the MDP bound for Howard's policy iteration, improving Ye's bound. Together with Friedmann's lower bounds, it settles the complexity of strategy iteration: strongly polynomial for a fixed discount factor, exponential otherwise.

Formalizing it. The result is proved on paper; none of it is formalized in Lean. A formal development produces a reusable matrix-based theory of finite discounted games: value vectors through Neumann series, modified costs as potential transformations, the min/max Bellman operator as a sup-norm contraction, and the optimality certificate. These are the tools of discounted MDP theory, stated here for two players.

Difficulty

The obvious argument for termination is that the values strictly decrease, so no strategy repeats. That bounds the number of iterations only by the number of strategies, which is exponential in $n$. Value-iteration convergence gives a geometric rate for $\|v^k - v^*\|_\infty$ but no bound independent of the numerical data. What is needed is a combinatorial event: within every block of about $\log_{1/\gamma}(n^2/(1-\gamma))$ iterations, some action leaves the strategy for good. Ye's version of this step used LP duality, which has no counterpart for two players, so the game-theoretic substitutes (flux vectors, modified costs) have to carry it. In Lean, a further difficulty is the bookkeeping of an algorithm with an oracle, a tie-breaking rule and a termination index.

Formalization scope

• Game (TBSGStrategyIteration.Game): Fintype states and actions, S1 : Finset S (so $S_2$ is its complement), src, stochastic rows P, real costs c, and 0 < γ < 1; every $A_i$ is nonempty. The state set may be empty.
• Strategies: Strat1 G, Strat2 G (positional, on the owner's states), Profile G = Strat1 G × Strat2 G.
• Values: value G π is the tsum $\sum_k \gamma^k P_\pi^k c_\pi$ (always summable here). valueWith allows other cost vectors, for the modified values and the flux vectors (Definition 3.8, taken literally).
• Optimality: componentwise order on S → ℝ, against every alternative strategy.
• Norms: ‖·‖ on S → ℝ is Mathlib's sup norm. $\|\cdot\|_1$ is written out as $\sum_i |x_i|$. $\log_{1/\gamma}$ is Real.logb (1/γ).
• The algorithm (IsRun): an infinite sequence $\sigma : \mathbb{N} \to \Pi_1$ with (a) $\sigma^{k+1}$ greedy for $v^k$, and (b) $\sigma^{k+1} = \sigma^k$ whenever $\sigma^k$ is itself greedy. Clause (b) is Figure 1's "if possible $\sigma^{k+1} \leftarrow \sigma^k$", and the paper's per-state tie-breaking rule implies it. Without it the algorithm may cycle. The oracle $\tau_2$ is an arbitrary map with the hypothesis that each $\tau_2(\sigma)$ is an optimal counter-strategy against $\sigma$. The number of iterations is the first $N \ge 1$ with $\sigma^N = \sigma^{N-1}$ (IsTerminationIndex).
• Non-vacuity. The oracle hypothesis is satisfiable for every game, by Theorem 2.8, which is a milestone for that reason. Greedy steps with tie-breaking exist from every initial strategy, so the goal cannot hold vacuously through an unsatisfiable oracle or run.
• Lemma 6.4 correction. As printed, Lemma 6.4 fails for $k = N-1$ whenever $\log_{1/\gamma}(n^2/(1-\gamma)) < 1$, because $\sigma^N = \sigma^{N-1}$. The formal statement adds the hypothesis $k + 1 < N$, which is what the proof uses and all that Theorem 6.5 needs.
• Value-iteration lemmas (4.8, 5.5) are stated for every $k$ of the infinite iterate sequence; the paper's finite sequences are prefixes of it.

Contributions welcome: the Neumann-series identity for $I - \gamma P_\pi$ (Lemma 3.1 as substrate), the optimality condition, and the counting argument of Theorem 6.5. The definitions are reusable for any finite discounted MDP or turn-based game mission.

Selected references

• T. D. Hansen, P. B. Miltersen, U. Zwick, Strategy iteration is strongly polynomial for 2-player turn-based stochastic games with a constant discount factor, arXiv:1008.0530v1, 2010; J. ACM 60(1), 2013. https://arxiv.org/abs/1008.0530
• Y. Ye, The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate, Mathematics of Operations Research 36(4), 2011. https://doi.org/10.1287/moor.1110.0516
• L. S. Shapley, Stochastic games, PNAS 39(10), 1953. https://doi.org/10.1073/pnas.39.10.1095
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• O. Friedmann, An exponential lower bound for the parity game strategy improvement algorithm as we know it, LICS 2009. https://doi.org/10.1109/LICS.2009.27

PASTA and the Formulas of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds Palm calculus. Chapter 2 settles when a queue has a stationary regime. Chapter 3 is called simply Formulas, and it is what the first two chapters were for: it computes.

The pattern is always the same. A quantity of interest is observed two ways — from a clock fixed in time, and from an arriving customer — and Palm calculus converts between them. Little's law, the Pollaczek–Khinchin formula and the rate conservation principle are all instances.

The goal

Theorem 3.3.1 (p.211) is the one that says when the two views coincide.

This classical result of queueing theory states, in rough terms, that if the arrival point process is Poisson, operational characteristics of the system computed just before arrival times and at arbitrary times are the same (Poisson Arrivals See Time Averages). Some care must be exercised in the application of this principle, and we now give a precise statement, in the θ_t-framework.

E⁰_A[f(Z(0))] = E[f(Z(0))]                                                            (3.3.1)

for every F_t-predictable, flow-compatible {Z(t)} and every non-negative measurable f, whenever A admits the constant F_t-intensity λ; and, under ergodicity,

lim_N (1/N) Σ_{n=1}^N f(Z(T_n)) = lim_T (1/T) ∫_0^T f(Z(s)) ds .                       (3.3.2)

The "some care" is the word predictable. PASTA is false without it: an arrival that changes the state it then observes does not see the time average, and that is exactly what predictability — measurability for the F_t-predictable σ-field, generated by the sets (a,b] × A with A ∈ F_a — rules out.

The hypothesis is the constant F_t-intensity, not "A is Poisson". By Watanabe's theorem the two are equivalent, but that equivalence is a remark on the page and not part of this theorem.

Why it earns its place: Pollaczek–Khinchin

§3.4 derives formulas from conservation equations. Applying the rate conservation principle of Chapter 1 to Y(t) = e^{iuW(t)} in a GI/GI/1/∞ queue gives Takács' formula

iu E[e^{iuW(0)}] = λ E⁰_A[e^{iuW(0−)}] (E[e^{iuσ_0}] − 1) + iu(1 − ρ) ,                (3.4.44)

an identity between a stationary expectation and a Palm expectation of the workload just before an arrival. One substitution turns it into a closed form — and that substitution is PASTA. When the arrivals are Poisson, E⁰_A[e^{iuW(0−)}] = E[e^{iuW(0)}], and

E[e^{iuW(0)}] = iu(1 − ρ) / ( iu − λ(Ψ_σ(u) − 1) ) ,                                   (3.4.45)

the Pollaczek–Khinchin characteristic function formula. The most quoted formula in single-server queueing theory is one application of this mission's goal theorem.

The rest of the chapter

§3.1 carries Little's formula to fluid queues. Lemma 3.1.1 is the set identity that turns the fluid workload into an integral against the arrival measure — the same two instants described from the server's side and from the arrivals' side.

§3.2 applies Campbell's formula to rare events. Lemma 3.2.1 gives a closed form, in a countable-state Markov chain, for the mean time to make an excursion to a rare set and return; its two expressions count the same cycle rate from the two ends. Theorem 3.2.1 generalizes Keilson's asymptotic equivalence to a stationary θ_t-compatible process, replacing cycles by thinnings of the entrance processes of two disjoint sets.

§3.5 applies the stochastic intensity integration formula to a superposition of on-off fluid sources. Lemma 3.5.1 identifies a conditional expectation with a Palm expectation through Papangelou's theorem — the mean workload while a source is idle equals the mean workload that source sees when it wakes. Lemma 3.5.2 measures the gap between the two Palm expectations of the workload taken with respect to a source's start process and its fluid process.

What this mission provides

Nothing here is on the platform or in Mathlib. The nearest platform item, queueing_general_littles_law, is Stidham's deterministic sample-path law; its own docstring disclaims probability, expectation, stationarity, ergodicity and FIFO. Baccelli's L = λW is the Palm identity for a stationary ergodic marked point process, derived from the inversion formula (1.2.25) — an identity between an expectation under P and a Palm expectation under P⁰_N, not a pathwise limit. Different framework, different hypotheses, and neither implies the other.

Mathlib has filtrations and adapted processes but no predictability in the form this chapter needs, and no stochastic intensity.

Formalization scope

• PASTA carries both displays. (3.3.1) is an equality in [0, ∞] for every non-negative measurable f. (3.3.2) asserts that, P-almost surely, both averages converge in [0, ∞] to one common limit, so both limits exist. Predictability is measurability for the predictable σ-field P(F_t) of p.55. The concrete form Z(t,ω) = v(t, θ_t ω) of (1.8.1) is not used as the hypothesis, because for a general history it is strictly weaker. The hypothesis is the constant F_t-intensity, E[A(a,b] | F_a] = λ(b − a), and not "A is Poisson".
• Takács (3.4.44) and Pollaczek–Khinchin (3.4.45) are stated for every real u, and for u ≠ 0 respectively. Their hypotheses are the page's: σ_n is independent of W(T_n−) under P⁰_A, E⁰_A[e^{iuσ_0}] = E[e^{iuσ_0}], P(W(0) = 0) = 1 − ρ, and ρ < 1. The workload is a measurable, flow-compatible solution of Lindley's equation. (3.4.45) adds PASTA's hypotheses for {W(t−)}, and it asserts that its denominator is non-zero.
• Lemma 3.2.1 asserts both closed forms of E_α R. The chain is irreducible, F is non-empty, and hitting times are counted from time 0.
• Theorem 3.2.1 asserts the equality in (3.2.43), the convergence to 1, and E⁰_{F_n(→A)}[τ(F_n)] · Λ_n → 1. Its hypotheses are the section's standing ones: P is flow-invariant, {X(t)} is flow-compatible, and A and every F_n are regular and disjoint.
• Lemmas 3.5.1 and 3.5.2 are stated for the full on-off model of §3.5.3. The on-off point processes are independent, their on periods, off periods and fluid functions are i.i.d. and independent, P⁰_{A^i} is the Palm probability of the random measure A^i, and the workload is the stationary solution of the fluid-queue equation. Lemma 3.5.1 is an identity in [0, ∞]. Lemma 3.5.2 assumes that E⁰_{A^i}[W(0)] and the expectation defining C_i are finite.

A formalization that makes Palm probability an opaque measure with the formulas as axioms, or that weakens predictability to adaptedness, trivializes this mission or makes it false, and is out of scope.

Stationary Regimes of Stochastic Recurrences

Background

Chapter 2 of Baccelli and Brémaud's Elements of Queueing Theory asks when a queue has a stationary regime. §§2.1–2.4 answer it for the single-server and multiserver queues by Loynes' monotone construction. §§2.5 and 2.11 answer it for the general object those constructions are instances of: a stochastic recurrence

W_{n+1} = h(W_n, ξ_n),

driven by a sequence {ξ_n} compatible with an ergodic shift θ. Two questions arise, and this mission is about both.

Exact sampling, and what "exact" means

§2.5.3 treats the finite-state case. An ergodic transition matrix on E = {1, …, r} has a stationary law π, and the classical way to sample it is to run the chain and wait. That gives a sample whose law converges to π and is never equal to it.

Coupling from the past (Propp and Wilson, 1996) does better. Run one chain from every state, all sharing a single array {ξ_k(i)} of i.i.d. uniforms indexed by time and current state, started further and further in the past. Once two chains meet they stay together, so eventually all r coalesce before time 0 — and Theorem 2.5.1 says the common value they reach has the distribution π exactly. Theorem 2.5.2 makes it practical: if the updating function preserves a partial order with a least and a greatest state, and a single uniform sequence drives every chain, the two extremal chains funnel all the others and their coalescence suffices.

Neither theorem is a statement about a program. Each says that a random variable is almost surely finite, and that another has a distribution equal to π.

Renovating events: sufficient, and then necessary

§2.5.4 treats the general case, through Borovkov's idea. An event A_n is renovating of length m when, on it, W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}) — the sequence's value m steps ahead forgets where it came from. Theorem 2.5.3 turns a condition on how often renovating events occur into the existence of a finite stationary solution Z with Z ∘ θ = h(Z, ξ), and into strong backwards coupling: W_n ∘ θ^{-n} is not merely convergent to Z but equal to it after a finite random index.

Corollary 2.5.1 makes the limit independent of the initial condition — one stationary regime, reached from every starting point. Theorem 2.5.4 is the converse: for ℝ₊^K-valued recurrences with a constant initial condition, strong backwards coupling produces renovating events. So the method characterises stability rather than merely detecting it.

The saturation rule

§2.11 treats the multidimensional case, where the state is a vector and the natural models are monotone and homogeneous. Theorem 2.11.1, due to Crandall and Tartar, is the key that unlocks it: under homogeneity, monotone and non-expansive are the same property. That is what puts these models within reach of Kingman's subadditive ergodic theorem, and Theorem 2.11.2 collects the payoff — asymptotic growth rates γ̄ and γ_ exist, both almost surely and in L¹, and do not depend on the initial condition.

The goal

Queueing folklore has a rule of thumb for the stability of an open network: saturate the queues fed by the external stream, measure the departure intensity µ of the saturated system, and declare the network stable when λ < µ. The book is careful that this saturation rule "does not hold for all systems".

Theorem 2.11.3 (p.166), "the main result on the stability region", proves it for Monotone-Homogeneous-Separable networks:

If lim Z_{[-n,0]} → ∞ a.s., then λ γ(0) ≥ 1.    If λ γ(0) > 1, then lim Z_{[-n,0]} → ∞ a.s.

Here γ(c) is the growth rate of the network fed by the scaled process cN, so c = 0 places every arrival at the origin: γ(0) is exactly the saturated system's rate, and µ = γ(0)⁻¹.

Two implications, with a gap between ≥ 1 and > 1 that the book leaves open — as it leaves open the critical case ρ = 1 of Loynes' theorem. Closing it would assert more than is proved.

What this mission provides

Nothing here is on the platform or in Mathlib. There is no coupling from the past, no theory of renovating events, and no Crandall–Tartar theorem. Order/Hom/* has monotone maps and Topology/MetricSpace/* has LipschitzWith 1, which is the right ambient notion for non-expansiveness in the sup-norm, but the equivalence between them under homogeneity is absent.

Formalization scope

• The standing assumptions of §2.5.1 (p.104) are part of every §2.5.4 statement: (P⁰, θ) is ergodic and {ξ_n} is compatible with θ. The relation Z ∘ θ = h(Z, ξ) holds P⁰-a.s.
• Theorem 2.5.4 is stated for {W_n^{[C]}}, the sequence its proof on p.119 builds the renovating events for. The page prints {W_n^{[0]}} in the conclusion, and that version is false. Corollary 2.5.1 uses the renovating condition of (2.5.14), W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}), where the page prints W_n.
• Theorem 2.11.2 carries all four limits, a.s. and in expectation, for every integrable ℝ^K-valued random initial condition Y, under the book's linear lower bound E[X_n^{[0]}] > −Cn.
• The goal is stated on the Palm space of a stationary ergodic marked point process: T_0 = 0, T_n ∘ θ = T_{n+1} − T_1, ξ_n ∘ θ = ξ_{n+1}, E⁰τ_n = λ^{-1}, E⁰Z_n < ∞. The map X satisfies (2.11.16) (it depends only on the points and marks in the index window) and the four framework assumptions for every point process. γ(0) is the a.s. limit of Z_{[-n,-1]}(0·N)/n. Dropping the marks would reduce the theorem to deterministic service, and dropping the link between the points and θ makes the second implication false. Neither is done.
• Stating only one of the goal's two implications, or collapsing them into an equivalence, would be a different theorem. Both implications are stated, with the gap between ≥ 1 and > 1 left open.

The Loynes Stability Theorem and Coupling

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds a calculus for stationary queues. Chapter 2 asks the prior question: when is there a stationary queue at all?

The G/G/1/∞ queue is one server at unit rate, infinite waiting room, fed by a stationary marked point process {(T_n, σ_n)} — arrival epochs and required service times. Its workload W(t), the service still owed by the server, obeys Lindley's equation between arrivals:

W(t) = (W(T_n−) + σ_n − (t − T_n))⁺,    t ∈ [T_n, T_{n+1}).                          (2.1.6)

Nothing in that equation says a solution exists on the whole line, let alone a stationary one. The answer is a sharp criterion in the traffic intensity ρ = λE⁰_A[σ_0].

The goal

Theorem 2.1.1 (p.80), which the book calls "the fundamental result of stability". Under ρ < 1 there is a unique finite workload process on all of ℝ, compatible with the flow, and it is given explicitly by the Loynes supremum

W(0) = sup_{n ≤ 0} ( T_n + Σ_{i=n}^{0} σ_i )⁺ ,                                      (2.1.12)

with W(T_n−) = 0 for infinitely many negative and infinitely many positive n (2.1.13). If ρ > 1 there is no finite stationary workload process at all.

Each half earns its place. The supremum is what "the Loynes construction" means: look back from the origin, take the work brought by customers n, …, 0 less the time −T_n since elapsed, and maximise over how far back you look. The ρ > 1 half is what turns ρ < 1 from a sufficient condition into a criterion. The critical case ρ = 1 is an explicit non-result in the book — there "may or may not" be a stationary workload — and is deliberately absent from the statement.

The route, and what it produces on the way

§2.2 proves the theorem by Loynes' monotone scheme on the Palm space, and two of its steps are worth stating in their own right.

Lemma 2.2.1 (p.87) is the uniqueness engine: a non-negative, a.s. finite Z with Z − Z∘θ ∈ L¹(P⁰) has E⁰[Z − Z∘θ] = 0. Applied to the difference of two stationary solutions, it forces that difference to be invariant, and ergodicity then forces it to be zero.

Theorem 2.2.1 (p.90) runs the argument backwards. Its section is titled "Queueing Proof of the Ergodic Theorem", and it is exactly that: the queueing construction yields the pointwise ergodic theorem, in the ratio form

lim_n ( Σ_{i=0}^n σ∘θ^{-i} ) / ( Σ_{i=0}^n τ∘θ^{-i} ) = E⁰[σ]/E⁰[τ],    P⁰-a.s.

Mathlib has the mean (von Neumann) ergodic theorem and no pointwise one, so this is absent substrate rather than a restatement.

Three extensions

The multiserver queue (§2.3). With s servers and the least-loaded-server rule, the state is the ordered workload vector obeying the Kiefer–Wolfowitz recurrence, and the criterion becomes E⁰[σ] < s E⁰[τ] (Theorem 2.3.1, p.93). Here uniqueness fails: p.94 exhibits a two-point space with a whole interval of stationary solutions. What survives is that the solution set is bracketed — M_∞ is minimal, and V^∞_∞ is the largest finite solution (Theorem 2.3.2, p.95).

Coupling (§2.4). Theorem 2.4.1 (p.99) is what "reaches the stationary regime" means: if a sequence couples with a θ-compatible one, then the law of its whole shifted trajectory converges in variation to the stationary trajectory's. The proof is one inequality, |P̃_{X,k} − P̃_{Z,k}| ≤ P(N > k), and the finiteness of the coupling time.

The fluid queue (§2.7). Theorem 2.7.1 (p.131) replaces customers by two θ_t-compatible random measures, the arrivals A and the service capacity C, and recovers the Loynes supremum W(t) = sup_{u ≤ t}(A_{u,t} − C_{u,t}) under λ < µ — as the minimal solution, the book claiming no uniqueness here.

Formalization scope

• ρ = λE⁰_A[σ_0] takes values in [0, ∞], so an input with E⁰_A[σ_0] = ∞ has ρ = ∞ and falls under the non-existence half rather than being read as ρ = 0.
• The explicit formulas are carried: the Loynes supremum (2.1.12) with the boundedness of its set as a conclusion, the construction points (2.1.13), the ratio limit E⁰[σ]/E⁰[τ] of Theorem 2.2.1, the threshold s E⁰[τ] of Theorem 2.3.1, and the fluid supremum (2.7.7).
• Identities between random variables hold almost surely, as in the book: the workload equations, (2.1.12)–(2.1.13), (2.7.7), and the solutions of (2.3.2). A statement "for every sample point" would be false, because on a null invariant set of sample paths no finite solution exists.
• Uniqueness in Theorem 2.1.1 is among measurable, θ_t-compatible workload processes; maximality in Theorem 2.3.2 is among measurable finite solutions; the coupling time of Theorem 2.4.1 is a random variable. A formalization that dropped the explicit supremum, or the ρ > 1 half, would trivialize the goal and is ruled out.

What this mission provides

None of it is on the platform or in Mathlib. The nearest platform item, single_server_queueing_convergence_of_subcritical, presupposes a stationary workload and proves two-time finite-dimensional convergence to it; Theorem 2.1.1 constructs that workload, proves it unique, gives it in closed form, and adds the non-existence half. Different conclusion, different generality, different Mathlib revision.

Ergodicity and Stochastic Intensity

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory has two halves. The first builds Palm calculus from the Matthes definition of P⁰_N and reaches the Swiss army formula. This mission is the second: §§1.6, 1.8 and 1.9, which supply the two things the rest of the book runs on.

Ergodic theory, quoted

§1.6 states, in its own words, "the ergodic theory results to be used later in this book". Five of them, and the book proves none: Birkhoff's pointwise ergodic theorem in discrete (Theorem 1.6.1) and continuous time (Theorem 1.6.4), Kingman's sub-additive ergodic theorem (Theorem 1.6.2), and the extremal characterizations of ergodicity in both settings (Theorems 1.6.3 and 1.6.5) — ergodicity is exactly the impossibility of splitting an invariant probability into two distinct ones.

They are quoted, but they are not decoration. Kingman's theorem is what produces the asymptotic growth rates of Theorem 2.11.2 and the constant γ(c) on which the saturation rule rests. Birkhoff's theorem is what makes the time average in PASTA's (3.3.2) a well-defined object, and what the fluid Loynes theorem invokes for lim_{u→−∞}(A_{u,0} − C_{u,0}) = −∞.

None of the three analytic ones exists in Mathlib. Analysis/InnerProductSpace/MeanErgodic is the mean (von Neumann, L²) theorem, not almost-everywhere convergence, and there is no sub-additive ergodic theorem at all. The platform has neither.

Predictability, and why PASTA can be stated

§1.8 introduces the stochastic intensity: a point process N admits the (P, F_t)-intensity {λ(t)} when E[N(a,b] 1_A] = E[(∫_a^b λ(t)dt) 1_A] for A ∈ F_a. Around it sits the notion of a predictable process — one measurable with respect to the strict past.

Theorem 1.8.1 is the structural fact that makes predictability usable. For the internal history of a marked point process, every predictable process has the concrete form

Z(t, ω) = v(t, θ_t ω),    v(t, ·) F_{0−}-measurable.                                   (1.8.1)

That is why mission IV can take this form as PASTA's hypothesis rather than constructing a predictable σ-field: Theorem 1.8.1 says nothing is lost.

The goal

Theorem 1.8.2 (p.61), §1.8.4, Watanabe's characterization of Poisson processes. For a history F_t = F_t^N ∨ G and a G-measurable, locally integrable {λ(t)}, if N admits the F_t-intensity {λ(t)} then N is a G-conditional Poisson process:

E[ e^{iuN(a,b]} | G ∨ F^N_a ] = exp{ (e^{iu} − 1) ∫_a^b λ(t) dt } .                    (1.8.12)

A stochastic intensity that carries no information beyond G forces the process to be Poisson conditionally on G, with the compensator as the parameter — and the conditional characteristic function is the exact Poisson one, not an approximation. With G trivial and λ constant this is the ordinary Poisson process, which is the equivalence Remark 3.3.1 of Chapter 3 invokes to explain the name PASTA. The book: "This result plays a role in queueing theory, especially for proving that some streams in a queueing network are or are not Poissonian."

Palm probability meets stochastic intensity

§1.9 asks whether the stochastic intensity is the same under P and under P⁰_N — whether the two probabilities describe the same dynamics. Theorem 1.9.1 says yes, on ℝ₊: the same process {λ(t)} serves both.

Theorem 1.9.2 is Papangelou's theorem, and it is the deepest statement of the section: N admits a stochastic intensity if and only if P⁰_N ≪ P on F_{0−}, and then λ(t) = (μ ∘ θ_t)λ with μ the Radon–Nikodým derivative. A dynamic property and a static one turn out to be the same thing.

Theorem 1.9.3 is Mecke's characterization: N is Poisson exactly when P ≡ P⁰_N on F_{0−}. The view from a point of the process and the view from a deterministic instant agree on the strict past precisely when the process has no memory. It follows in one line from the two theorems before it.

What this mission provides

Four of the five missions in this series import the Chapter 1 substrate; this one adds the two pieces they need from its second half — ergodic theory and the stochastic intensity. Nothing here is on the platform, and Mathlib has filtrations and adapted processes but no predictability in this form, no stochastic intensity, no pointwise ergodic theorem and no Kingman.

Formalization scope

Every result is stated in the book's strength, with the book's standing definitions as binders. A discrete flow is a bijective, measurable, P⁰-preserving map (p.46); a continuous flow is jointly measurable in (t, ω) (p.3, clause (a)). A history compatible with the flow satisfies θ_t F_s = F_{s−t} (p.57), and an F_t-intensity is a non-negative, measurable, locally integrable, adapted process (p.58). The limits of Theorems 1.6.1, 1.6.2 and 1.6.4 are asserted to exist; Kingman's constant h̄ lies in ℝ ∪ {−∞} and is identified with inf_n (1/n) E⁰[h_n], the means being extended reals so that E⁰[h_n] = −∞ is not read as 0. Theorems 1.6.3, 1.6.5, 1.9.2 and 1.9.3 are equivalences, and Theorem 1.9.2 carries the closed form λ(t) = (μ ∘ θ_t)λ with μ = dP⁰_N/dP on F_{0−}. The goal's conclusion is the exact conditional characteristic function (1.8.12); a formalization that only asserted some conditional Poisson law, or conditioned on G alone, would not be this theorem.

Motivation

A public facility (a fire station, a hospital, a server) is to be placed on a road network, and the people it serves report their own locations. When the planner wants to minimise the distance to the farthest user (the minimax or egalitarian objective, in the sense of Rawls), each user has an incentive to misreport so as to pull the facility towards themselves. Mechanism design without money asks which location rules make truthful reporting a dominant strategy, and how much of the optimal objective such rules must give up. Procaccia and Tennenholtz (EC 2009) introduced this approximation viewpoint for points on a line; Schummer and Vohra (J. Econom. Theory 2002) characterised the strategyproof deterministic rules on networks.

Alon, Feldman, Procaccia and Tennenholtz (Math. Oper. Res. 2010) study the minimax on general networks. Choosing a fixed agent's location (dictatorship) is strategyproof and loses at most a factor 2 on any network. On a circle they give a randomized strategyproof mechanism with ratio $3/2$. On trees a simple randomized mechanism achieves $2-2/(n+2)$. This mission is about their matching negative result: on trees, no strategyproof randomized mechanism does better than $2-o(1)$.

Setting

A network $G$ is a metric space whose points are the vertices of a graph and every point inside its edges; the distance $d(a,b)$ is the length of the shortest path. There are $n$ agents; a location profile is $x=(x_1,\dots,x_n)\in G^n$. A randomized mechanism $f$ maps each profile to a probability distribution $f(x)$ over $G$, the location of the facility. An agent at $a$ bears the cost $\operatorname{cost}(P,a)=\mathbb E_{y\sim P}[d(a,y)]$, and the maximum cost of $P$ for the profile $x$ is

$$\operatorname{mc}(P,x)=\mathbb E_{y\sim P}\Big[\max_{i} d(x_i,y)\Big].$$

The mechanism is strategyproof (SP) if no agent can lower its own cost by reporting another point: for all $x$, $i$ and $x_i'\in G$, $\operatorname{cost}(f(x),x_i)\le\operatorname{cost}(f(x_i',x_{-i}),x_i)$. The benchmark is the best deterministic location, $\mathrm{OPT}(x)=\min_{z\in G}\operatorname{mc}(\delta_z,x)$.

The network of the theorem is the tree $G(m,k)$: an edge of length $1$ joins two roots $l^0$ and $r^0$; below each root hangs a complete $m$-ary tree of depth $k$ whose edges from level $d$ to level $d+1$ have length $2^d$. The profiles used are the paper's $x^0,x^1,\dots,x^k$: $x^0$ puts $n/2$ agents on each root, and $x^{d+1}$ moves the $n/(2m^d)$ agents at a chosen left vertex $l^d$ on level $d$ to its $m$ children, equally.

Formalization targets

Goal: Theorem 4.1 with its explicit constant

For $m\ge2$, $k\ge1$, $n\ge1$ with $2m^k\mid n$, and every SP randomized mechanism $f$ on $G(m,k)$ for $n$ agents, there is a profile $x$ with $\mathrm{OPT}(x)>0$ and

$$\operatorname{mc}(f(x),x)\ \ge\ \Big(2-\frac1{2^k}-\frac4m\Big)\,\mathrm{OPT}(x).$$

The paper states the bound as $2-O(1/2^{\sqrt{\log n}})$; the displayed form is what its proof establishes (p. 526), and $k=\Theta(\sqrt{\log n})$, $m=\Theta(n^{1/k})$ turn it into the $O(\cdot)$ form.

Milestones

1. Strategyproofness preserves $\mathbb E[d(f(x^1),l^0)]\ge 1/2$ when the agents leave $l^0$ (p. 524).
2. For every point $y$ with $d(y,l^0)\ge1/2$: $\sum_{j=1}^m d(y,l^1_j)\ge(3m-2)/2$ (p. 525).
3. Lemma B.1: some left vertex $l^k$ on level $k$ has $\mathbb E[d(f(x^k),l^k)]\ge\frac{2^{k+1}-1}{2}-\frac{2^{k+1}-(k+2)}{m}$ (p. 525).
4. The expected maximum cost $\operatorname{mc}(f(x^k),x^k)$ is at least the same bound (p. 526).
5. Under $x^k$ the deterministic facility at $l^{k-1}$ has maximum cost exactly $2^{k-1}$ (p. 526).

Significance

The result. Dictatorship already achieves ratio $2$ on every network, and on trees the best known SP mechanism improves this only to $2-2/(n+2)$. Theorem 4.1 shows that this is essentially optimal: randomization, which buys a factor $3/2$ on the circle, buys almost nothing on trees once the tree is allowed to branch widely. It separates two natural network classes by their strategyproof approximability, and the paper notes that trees of bounded branching factor escape the construction, which leaves that class as the open case.

Formalizing it. The result is proved in the paper and has no machine-checked proof. The mission produces a checked lower bound for all SP randomized mechanisms on a continuous network, quantified over arbitrary probability measures and arbitrary deviations, together with a reusable model of facility location with strategic agents on a metric network and an explicit construction of a weighted metric tree.

Difficulty

The bound holds against every mechanism, so no mechanism is analysed: the only handle on $f$ is the SP inequality, applied along a chain of unilateral deviations whose length is the number of agents moved. The chain must be organised so that the bound on one expected distance survives each level of the tree, and the pointwise geometric inequality on the tree must be turned into a bound on expectations under an arbitrary distribution that may put mass inside edges. The final comparison needs the exact optimum of a specific profile and exact arithmetic on the resulting ratio. Restricting the facility to vertices, or assuming the mechanism is anonymous or continuous, would change the class of mechanisms and is not allowed.

Formalization scope

• The network is HardTree m k, the tree $G(m,k)$ realised isometrically inside $\ell^1$ (one coordinate per edge), with the subspace metric (equal to shortest-path length on the embedded tree) and the Borel σ-algebra. Edge interiors are points of the space. Vertices are vertex s w for a side s and a word w over Fin m.
• Agents are Fin n; a mechanism is any function (Fin n → HardTree m k) → ProbabilityMeasure (HardTree m k); strategyproofness quantifies over every profile, agent and point of the tree. No measurability, anonymity or continuity of $f$ is assumed. cost and mc are Bochner integrals of bounded continuous functions; $\mathrm{OPT}$ is optMc, an infimum over all points.
• Explicit constant: the paper's $2-O(1/2^{\sqrt{\log n}})$ is stated as $2-1/2^k-4/m$ on $G(m,k)$, the bound its proof yields on p. 526. The asymptotic form in $n$ is not stated: the paper assumes $2m^k\mid n$ "for ease of exposition" and does not treat the leftover agents for general $n$, so the divisibility is a hypothesis.
• The paper's "without loss of generality $\mathbb E[d(f(x^0),l^0)]\ge1/2$" is a hypothesis of milestones 1, 3 and 4 only; the goal covers both cases.
• A trivializing reading is ruled out: the goal requires $\mathrm{OPT}(x)>0$, so a profile with all agents at one point (where both sides vanish) is not a witness.
• A complete development needs basic facts about the $\ell^1$ tree metric (distances along paths, compactness), integrals of bounded continuous functions against probability measures, and the arithmetic of the bound. The model file and the tree construction are reusable for other facility-location results on trees.

Selected references

• N. Alon, M. Feldman, A. D. Procaccia, M. Tennenholtz, Strategyproof Approximation of the Minimax on Networks, Mathematics of Operations Research 35(3):513–526, 2010. https://doi.org/10.1287/moor.1100.0457
• A. D. Procaccia, M. Tennenholtz, Approximate Mechanism Design without Money, Proc. 10th ACM Conference on Electronic Commerce, 177–186, 2009. https://doi.org/10.1145/1566374.1566401
• J. Schummer, R. V. Vohra, Strategy-proof Location on a Network, Journal of Economic Theory 104(2):405–428, 2002. https://doi.org/10.1006/jeth.2001.2807
• N. Alon, M. Feldman, A. D. Procaccia, M. Tennenholtz, Strategyproof Approximation Mechanisms for Location on Networks, 2009. https://arxiv.org/abs/0907.2049