Operations Research

Motivation

A single machine must process a set of jobs, each with a processing time and a due date, and the cost of a schedule depends on how late the jobs finish. Total tardiness is the classical criterion, but in many applications lateness is penalised more than proportionally: a job one week late costs more than twice a job half a week late, and a quadratic or other convex penalty describes this better. Hamilton Emmons's 1969 paper in Operations Research (DOI 10.1287/opre.17.4.701) derives dominance rules for total tardiness and then asks which of them survive when total tardiness is replaced by $\sum_J g(T_i)$ for an arbitrary convex nondecreasing loss $g$.

Timeline of the relevant results:

• 1955 — Jackson shows that ordering jobs by earliest due date (EDD) minimises the maximum lateness, and hence produces a schedule without late jobs whenever one exists.
• 1956 — Smith gives the ratio rule for weighted completion time and an adjacent-interchange criterion for pairs of jobs.
• 1969 — Emmons proves the precedence theorems for total tardiness that underlie later branch-and-bound and dynamic programming algorithms for $1\,||\,\sum T_j$, and shows (p. 713) that Theorems 2 and 3 and part of Theorem 1 extend to any sum of identical convex nondecreasing tardiness penalties.
• 1977 — Lawler's pseudo-polynomial algorithm for total tardiness builds on Emmons's conditions; the problem is later shown NP-hard (Du and Leung, 1990).

Setting

A finite set $J$ of jobs is to be sequenced on one machine. Job $J_i$ has a processing time $p_i\ge 0$ and a due date $d_i$. All jobs are available at time $0$, and the machine processes them one after another without idle time. A schedule is an ordering $l$ of the jobs of $J$. The completion time $C_i$ of $J_i$ in $l$ is the sum of the processing times of $J_i$ and of every job before it; its waiting (starting) time is $W_i=C_i-p_i$, and its tardiness is

$$T_i=\max(0,\,C_i-d_i).$$

A loss function $g:\mathbb R\to\mathbb R$, convex and nondecreasing on $[0,\infty)$, is fixed, the same for every job. The objective is $\sum_{i\in J} g(T_i)$, and a schedule is optimal if no schedule of $J$ has a smaller objective. With $g(T)=T$ this is total tardiness.

Where the paper uses job indices, the jobs are indexed in SPT order: $j<k$ implies $p_j<p_k$, or $p_j=p_k$ and $d_j\le d_k$. The notation $j\leftarrow k$ means that some optimal schedule has $J_j$ before $J_k$; for a set $A_k$ of jobs, $k\leftarrow A_k$ means that some optimal schedule has $J_k$ before every job of $A_k$, and $A_k'$ is the set of jobs of $J$ not in $A_k$. An EDD schedule sequences the jobs in nondecreasing order of due dates.

Formalization targets

Goal: Corollary 2.2* (p. 713)

If an EDD schedule $l$ of $J$ satisfies

$$W_i\le d_i\qquad\text{for every } i\in J,$$

then $l$ minimises $\sum_J g(T_i)$ over all schedules of $J$, for every $g$ convex and nondecreasing on $[0,\infty)$.

The goal fixes no constant and no particular $g$: it is a statement about the whole class of convex nondecreasing penalties.

Milestones (in attack order)

1. Convex exchange condition (p. 713): if $T_{ja}\le T_{jb}$, $T_{kb}\le T_{ka}$ (all nonnegative), $T_{ka}-T_{kb}\le T_{jb}-T_{ja}$ and $T_{jb}\ge T_{ka}$, then $g(T_{ka})-g(T_{kb})\le g(T_{jb})-g(T_{ja})$.
2. Theorem 1* (p. 713): for $j<k$, if $d_j\le d_k$ then $j\leftarrow k$.
3. Theorem 2* (p. 713): for $j<k$, if $k\leftarrow A_k$, $d_j>d_k$ and $d_j+p_j\ge\sum_{A_k'}p_i$, then $k\leftarrow j$.
4. Corollary 2.1* (p. 713): if $d_j=\max_i d_i$ and $d_j+p_j\ge\sum_J p_i$, then some optimal schedule ends with $J_j$.
5. Last-job reduction (proof of Corollary 2.2, p. 706): if some optimal schedule ends with $J_j$, any optimal schedule of $J\setminus\{J_j\}$ followed by $J_j$ is optimal for $J$.

Two further statements of the same section are included as items: Corollary 1.3* (the SPT schedule is optimal if it coincides with the EDD schedule) and Theorem 3 for the generalised objective.

Significance

The goal says that EDD is optimal for every convex nondecreasing tardiness penalty as long as no job starts after its due date. The classical sufficient condition, that at most one job is tardy, follows from Jackson's rule; Emmons's condition allows any or all jobs to be tardy, provided each is tardy by at most its own processing time. Because the conclusion holds for the whole class of penalties at once, an instance satisfying it needs no knowledge of $g$: total tardiness, total squared tardiness, and any other convex nondecreasing cost are minimised by the same sequence. Theorems 1* and 2* are the dominance rules that the paper's ordering procedure applies pairwise; they reduce the search space of branch-and-bound methods for convex tardiness objectives.

The results are proved in the paper (for $\sum g(T_i)$ the proofs are said to be "easily established" and omitted). None of them has, to our knowledge, a machine-checked proof. The mission produces formal statements and proofs of the generalised results, including the omitted ones, on top of a reusable single-machine model.

Difficulty

The total-tardiness proofs compare changes in tardiness additively: an interchange is good if the decrease in one job's tardiness is at least the increase in another's. For a convex $g$ this comparison is not enough, because a unit of tardiness costs more at higher tardiness levels; the changes must also occur at the right height on the curve, and part (b) of the proof of Theorem 1 fails for this reason. Each generalised argument therefore has to check, for every job whose tardiness changes, both the size and the location of the change, including jobs whose tardiness changes from zero to positive. Ties for the latest due date are a further obstacle: the printed proof of Corollary 2.1 cites Theorem 2, whose hypothesis $d_j>d_k$ is strict, so a job sharing the maximum due date is not covered by the argument as written, although the corollary is stated without excluding ties.

Formalization scope

Jobs are elements of a type $\iota$; the job set is a Finset $J$, processing times and due dates are real functions $p,d:\iota\to\mathbb R$. Where the paper's index matters, $\iota$ is linearly ordered and its order is the job index, together with the SPT-indexing hypothesis. A schedule is a duplicate-free list whose elements are exactly $J$, and completion times are the published single-machine definition MooreLateJobs.Shared.completionTime (Moore 1968), which starts the machine at time $0$ with no idle time. Optimality is against every schedule of $J$. The relation $j\leftarrow k$ is formalised as the existence of an optimal schedule with $J_j$ before $J_k$ (keeping the premise $k\leftarrow A_k$ in the conclusion where the theorem has one); the paper's cumulative reading of the notation is not formalised.

Standing assumptions and deviations:

• $g$ is convex and nondecreasing on $[0,\infty)$ only; the page's "increasing" is read as nondecreasing, as in the abstract. No smoothness, strict monotonicity or $g(0)=0$ is assumed.
• Processing times are assumed nonnegative; this is added (they are durations).
• The reduction $d_i<\sum_J p_i$ of p. 703 is not assumed, which makes the statements apply to more instances.
• "The EDD schedule" is any schedule with nondecreasing due dates; ties are arbitrary.

A trivializing formalization is ruled out: the goal requires optimality of the given EDD list against every schedule of $J$, not of some EDD list, and a sorry-free check shows its hypotheses hold on a two-job instance in which both jobs are tardy.

A complete development needs list lemmas for moving one job to a later position, the effect of such moves on completion times, and slope inequalities for convex functions on $[0,\infty)$. The schedule-manipulation lemmas are reusable for other single-machine sequencing results. Proofs of any milestone, of the two further items, and of general interchange lemmas are welcome.

Selected references

• H. Emmons, One-Machine Sequencing to Minimize Certain Functions of Job Tardiness, Operations Research 17(4):701–715, 1969. https://doi.org/10.1287/opre.17.4.701
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3:59–66, 1956. https://doi.org/10.1002/nav.3800030106
• E. L. Lawler, A "Pseudopolynomial" Algorithm for Sequencing Jobs to Minimize Total Tardiness, Annals of Discrete Mathematics 1:331–342, 1977. https://doi.org/10.1016/S0167-5060(08)70742-8
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• J. Du and J. Y.-T. Leung, Minimizing Total Tardiness on One Machine is NP-Hard, Mathematics of Operations Research 15(3):483–495, 1990. https://doi.org/10.1287/moor.15.3.483

Motivation

In the secretary problem, $n$ items with nonnegative values arrive one at a time in a uniformly random order, and an online algorithm must decide on each arrival, irrevocably, whether to keep it. The classical version keeps one item; the rule that observes a $1/e$ fraction of the arrivals and then takes the first item better than everything seen picks the best item with probability at least $1/e$ (Ferguson 1989).

Babaioff, Immorlica and Kleinberg (SODA 2007; journal version J. ACM 2018) introduced the matroid secretary problem: the kept set must be independent in a known matroid. It models online auctions in which the feasible sets of winners have matroid structure, for example hiring along the edges of a network without closing a cycle. They gave a $16$-competitive algorithm when the matroid is graphic, i.e. the items are the edges of a graph and a set is feasible when it contains no cycle.

Timeline for graphic matroids:

• 2007, Babaioff–Immorlica–Kleinberg: $16$-competitive.
• 2009, Babaioff–Dinitz–Gupta–Immorlica–Talwar (SODA 2009, Theorem 1.5): $3e\approx 8.15$-competitive, through a random reduction to partition matroids. This mission formalizes that result.
• 2009, Korula–Pál (ICALP 2009): $2e$-competitive, by a different reduction.

Setting

Let $G=(V,E)$ be a finite simple graph. Each edge $e$ has a value $v(e)\ge 0$. A set $S\subseteq E$ is independent in the graphic matroid of $G$ if the graph $(V,S)$ has no cycle. The offline optimum is

$$\mathrm{OPT}(G,v)=\max\Big\{\sum_{e\in S}v(e): S\subseteq E\ \text{acyclic}\Big\}.$$

The edges arrive in a uniformly random order. An algorithm sees each edge and its value on arrival and decides at once whether to select it. The selected set must be acyclic. The algorithm is $\alpha$-competitive if $\mathrm{OPT}(G,v)\le\alpha\cdot\mathbb E[\text{value of the selected set}]$ for every $G$ and every $v\ge 0$.

A partition matroid on a subset $U'\subseteq E$ is given by a family $P$ of nonempty, pairwise disjoint parts with union $U'$: a set is independent when it lies in $U'$ and meets each part at most once. Its max-weight base has value $\mathrm{val}(P,v)=\sum_{p\in P}\max_{e\in p}v(e)$.

Definition 5.1. A random partition $\mu$ (a probability distribution on such families, chosen from $G$ alone) is an $\alpha$-partition scheme if every partition in its support has only acyclic independent sets, and for every $v\ge 0$,

$$\mathrm{OPT}(G,v)\le \alpha\cdot\mathbb E_{P\sim\mu}[\mathrm{val}(P,v)].$$

The random partition of Lemma 5.3. Pick an edge $\{u,w\}$ uniformly at random. With probability $\tfrac12$ colour $u$ red and $w$ blue, otherwise the reverse. Colour every other vertex red or blue independently with probability $\tfrac12$. Each red vertex $x$ gets a part: the red-blue edges at $x$. Then repeat on the edges with both endpoints blue, with fresh randomness.

The algorithm. Draw the partition, let the edges arrive, and on each part run the classical secretary rule on that part's arrivals. Output all selected edges.

Formalization targets

Goal: Theorem 1.5

For every finite simple graph $G$ and every $v\ge 0$:

1. every possible output of the algorithm is an acyclic set of edges of $G$;

$$\mathrm{OPT}(G,v)\le 3e\cdot\mathbb E[\mathrm{ALG}].$$

Part 1 is needed for the statement to have content: an algorithm that selects every edge would otherwise satisfy part 2.

Milestones

• Section 2, p. 4. On $m\ge1$ arrivals, the classical rule selects the maximum with probability at least $1/e$.
• Theorem 5.4, first clause. For a fixed partition $P$, the per-part rule outputs a set independent in the partition matroid, and $\mathrm{val}(P,v)\le e\cdot\mathbb E_\pi[\mathrm{ALG}]$.
• Lemma 5.3, independence. Every partition the random construction can produce is a partition matroid on a subset of $E$, and each of its independent sets is a forest.
• Lemma 5.3. The construction is a $3$-partition scheme.
• Section 5, p. 10. Any $\alpha$-partition scheme for a graphic matroid, combined with the per-part rule, gives a feasible, $e\alpha$-competitive algorithm.

Significance

The theorem shows that the graphic matroid secretary problem admits a constant-competitive algorithm with a small explicit constant. It does so through a reduction: a random partition matroid that is feasible for the original matroid and loses only a constant factor in expectation. The reduction separates the combinatorics (Lemma 5.3) from the online part (Theorem 5.4). The same framework gives algorithms for uniform and transversal matroids and for the weighted and discounted variants on any matroid with an $\alpha$-partition property.

The result is proved in the paper; it has not been formalized. The mission contributes a machine-checked version of the reduction, a formal treatment of a recursively defined random partition, and the classical secretary bound in a reusable finite form. The constant $3e$ is not the best known for graphic matroids (Korula–Pál improve it to $2e$), so the formal goal is this algorithm's guarantee, not the best possible ratio.

Difficulty

The online half is routine once the classical bound is available: the relative order of the edges in each part is uniform, and the parts are disjoint. The difficulty is Lemma 5.3. The natural idea of using a fixed optimal forest to build the partition is ruled out because the partition must be chosen before the values are seen. The expectation bound must therefore hold for every valuation at once, for a law that depends on the graph only. The construction is recursive and random: its expected value is not a closed-form sum, and any bound has to be carried through the random sequence of blue-blue subgraphs. Feasibility needs an invariant across rounds: the parts created later live inside the blue-blue edges of every earlier round.

Formalization scope

• Graph. A SimpleGraph on a Fintype vertex type with decidable adjacency. The edges are G.edgeFinset, and acyclicity of $S$ is (SimpleGraph.fromEdgeSet S).IsAcyclic. Multigraphs are not covered.
• Values. Values are a real function v : Sym2 V → ℝ with ∀ e, 0 ≤ v e; only the values on edges matter.
• OPT is a Finset.sup' over acyclic subsets of the edge set. A partition is a finite family of nonempty, pairwise disjoint parts inside the edge set. Its max-weight base value is the sum of the part maxima.
• Random partition. A PMF defined by well-founded recursion on the number of edges. Empty parts are dropped, and edges with two red endpoints are discarded.
• Random order. The edges are numbered by a fixed enumeration. An arrival order is a permutation of the numbers, and expectation over the order is the average over all $|E|!$ permutations.
• Classical rule. It samples $\lfloor m/e\rfloor$ arrivals of a part with $m$ edges. Ties are broken by preferring the smaller edge number among equal values.
• Constants. Competitiveness is multiplicative ($\mathrm{OPT}\le 3e\cdot\mathbb E[\mathrm{ALG}]$), so a zero expectation is not a loophole.
• Ruling out trivial formalizations. In Definition 5.1 the random partition is fixed before the valuation, and the independence requirement holds for every partition in its support. A partition allowed to depend on $v$ would make every matroid $1$-partitionable.

A complete development needs the classical secretary bound in finite form, the uniformity of induced sub-orders of a uniform permutation, expectations of PMF.bind along a well-founded recursion, and facts about forests in SimpleGraph. The first two, and a general graphic-matroid layer, are reusable beyond this mission. Proofs of any milestone, alternative proofs of Lemma 5.3, and extensions to the uniform and transversal cases of Theorem 5.2 are welcome.

Selected references

• M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proc. 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.135
• M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007, pp. 434–443. https://dl.acm.org/doi/10.5555/1283383.1283429
• M. Babaioff, N. Immorlica, D. Kempe, R. Kleinberg, Matroid Secretary Problems, Journal of the ACM 65(6), 2018. https://doi.org/10.1145/3212512
• N. Korula, M. Pál, Algorithms for Secretary Problems on Graphs and Hypergraphs, ICALP 2009, LNCS 5556. https://doi.org/10.1007/978-3-642-02930-1_42
• T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493

Motivation

A group of $m$ individuals each hold a subjective probability distribution over the same $n$ outcomes, and one wants a single distribution representing their consensus. Averaging and convolution are the obvious candidates. Eisenberg and Gale (Ann. Math. Statist. 30(1), 1959) observe that a real institution already performs such an aggregation: the pari-mutuel method of betting on horse races, in which the final "track's odds" on a horse are proportional to the total amount bet on it.

The difficulty is circular. Each bettor wants to bet where the ratio of their own probability to the track probability is largest, but the track probabilities are only known after everyone has bet. The paper asks whether track probabilities and bets compatible with both the bettors' strategies and the pari-mutuel principle exist, and whether they are determined by the data. It answers yes on both counts for the probabilities, which gives a well-defined notion of pari-mutuel consensus.

The variational problem the paper introduces, maximizing $\sum_i b_i \log(\text{utility}_i)$, is now known as the Eisenberg–Gale convex program. It is the standard tool for computing equilibria of linear Fisher markets, and the pari-mutuel market is the special case in which every bettor's utility for a horse is their subjective win probability.

Setting

There are $m$ bettors $B_1,\dots,B_m$ and $n$ horses $H_1,\dots,H_n$.

• The subjective probability matrix $P=(p_{ij})$ is $m\times n$; $p_{ij}$ is the probability, in the opinion of $B_i$, that $H_j$ wins. Each row is a probability distribution: $p_{ij}\ge 0$ and $\sum_j p_{ij}=1$.
• Bettor $B_i$ has a budget $b_i>0$, with the unit of money chosen so that $\sum_i b_i=1$.
• Each column of $P$ contains at least one positive entry (a horse nobody believes in can be removed).

Unknowns are Greek. $\pi_j$ is the track probability of $H_j$ and $\beta_{ij}$ is the amount $B_i$ bets on $H_j$. Nonnegative $\pi_j,\beta_{ij}$ are equilibrium probabilities and bets when

$$\text{(1)}\ \sum_{j=1}^n\beta_{ij}=b_i,\qquad \text{(2)}\ \sum_{i=1}^m\beta_{ij}=\pi_j,\qquad \text{(3)}\ \text{if } \mu_i=\max_s\frac{p_{is}}{\pi_s}\text{ and }\beta_{ij}>0,\text{ then }\mu_i=\frac{p_{ij}}{\pi_j}.$$

(1) is the budget relation, (2) the pari-mutuel condition, and (3) says each bettor bets only on horses that maximize the subjective expectation $p_{ij}/\pi_j$.

The paper's variational problem is

$$\varphi(\xi)=\sum_{i=1}^m b_i\log\sum_{j=1}^n p_{ij}\xi_{ij}\quad\text{on}\quad D=\Big\{\xi:\ \xi_{ij}\ge0,\ \sum_{i=1}^m\xi_{ij}=1\ \text{for all } j\Big\},$$

with $\varphi=-\infty$ where an inner sum vanishes. From a maximizer $\bar\xi$ it builds $\pi_j=\max_i b_ip_{ij}/\sum_s p_{is}\bar\xi_{is}$ (6) and $\beta_{ij}=\bar\xi_{ij}\pi_j$ (7). In Lean the market is PariMutuel.Consensus.Market m n, equilibrium is Market.IsEquilibrium, and $\varphi$, $D$, the maximizer predicate, (6) and (7) are Market.phi, D m n, Market.IsPhiMaximizer, Market.trackProb, Market.bets.

Formalization targets

Goal: existence and uniqueness of equilibrium probabilities

$$\exists!\,\pi\in\mathbb R^n\ \ \exists\,\beta\in\mathbb R^{m\times n}:\ (\pi,\beta)\ \text{are equilibrium probabilities and bets}.$$

Only $\pi$ is unique; the paper notes that equilibrium bets need not be.

Milestones

1. $\varphi$ attains its maximum on $D$ at a point with every inner sum positive (p. 167).
2. $\partial\varphi/\partial\xi_{ij}=b_ip_{ij}/\sum_s p_{is}\xi_{is}$ wherever the inner sums are positive (p. 167).
3. (8): at a maximizer, $\bar\xi_{ij}>0$ implies $\pi_j=\partial\varphi/\partial\bar\xi_{ij}$ (p. 167).
4. Every $\pi_j$ of (6) is positive (p. 167).
5. EXISTENCE THEOREM: for every maximizer $\bar\xi$, (6)–(7) are equilibrium probabilities and bets (p. 167).
6. Every equilibrium has $\pi_j>0$ (p. 168).
7. For two equilibria, $\sum_k\bar\pi_k\bar\pi_k/\pi_k\le 1$ (p. 168).
8. If $\pi>0$, $\bar\pi\ge0$, both sum to 1 and $\sum_k\bar\pi_k^2/\pi_k\le1$, then $\bar\pi=\pi$ (p. 168).
9. UNIQUENESS THEOREM: equilibrium probabilities are unique (p. 168).

A further, non-milestone item states the referee's example (p. 168): with two bettors of equal budgets and two horses, if the first bettor's distribution is $(\tfrac12,\tfrac12)$, the equilibrium probabilities are $(\tfrac12,\tfrac12)$ whatever the second bettor believes.

Significance

The result makes pari-mutuel odds a well-defined function of the bettors' beliefs and budgets, so the consensus can be studied as a mathematical object; the referee's example shows it behaves very differently from averaging, since a single indifferent bettor can fix it. The existence proof replaces a fixed-point argument by a concave maximization, which is the origin of the Eisenberg–Gale program, later the basis of convex-programming and combinatorial algorithms for Fisher market equilibria.

The theorems are classical and fully proved in the paper. To the knowledge of this mission they have no machine-checked proof. The mission produces a formal pari-mutuel market model, the Eisenberg–Gale program with the correct treatment of $\log 0=-\infty$, and Lean proofs of existence and uniqueness. The platform's Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities missions (Vazirani–Yannakakis) concern a related Fisher-market model with rational piecewise-linear utilities.

Difficulty

The existence statement, as the paper proves it, has two delicate points. $\varphi$ is $-\infty$ on part of the boundary of $D$, so "continuous on a compact set" needs the extended-real reading, and a real-valued formalization must handle the boundary separately. The first-order condition (8) has to be derived from maximality on a polytope with equality constraints on columns, not from an unconstrained critical point.

For uniqueness, the natural first idea, strict concavity of $\varphi$, fails: $\varphi$ is concave but not strictly concave in $\xi$, and indeed equilibrium bets are not unique. Uniqueness has to be proved for the probabilities directly, for arbitrary equilibria and not only those built from a maximizer, and it needs positivity of all $\pi_j$, which the paper uses without proof.

Formalization scope

• Bettors are Fin m and horses Fin n, indexed from 0. All data are real. Every standing assumption (rows of $P$ are probability vectors, no zero column, $b_i>0$, $\sum_i b_i=1$) is a field of Market; $m\ge1$ follows from $\sum_ib_i=1$.
• Condition (3) is written multiplied out: $\beta_{ij}>0\Rightarrow p_{is}\pi_j\le p_{ij}\pi_s$ for all $s$. This equals (3) when $\pi>0$ and encodes the paper's $p/0=+\infty$ when some $\pi_s=0$. Positivity of $\pi$ is not part of the definition of equilibrium; it is milestone 6.
• $D$ has column sums one, as in (5).
• $\varphi$ is real-valued. A maximizer is a point of $D$ with positive inner sums that dominates every point of $D$ with positive inner sums; the excluded points have $\varphi=-\infty$ on the page. The max in (6) is Finset.sup' over the nonempty set of bettors.
• Ruled out: a version of (3) with real division ($x/0=0$) admits spurious equilibria with $\pi_s=0$ and makes uniqueness false; a maximizer defined with the raw real $\varphi$ ($\log0=0$) changes the set of maximizers; adding $\pi>0$ or $\sum_j\pi_j=1$ to the equilibrium definition weakens the goal.
• Needed infrastructure: compactness of $D$ and an argument handling the $-\infty$ boundary, one-variable derivatives of $\log$ of linear forms, and the equality case of the Cauchy–Schwarz inequality. Milestones 7–9 use no analysis and can be attacked independently of 1–5. Proofs of any milestone, and reusable lemmas on the Eisenberg–Gale program, are welcome.

Selected references

• E. Eisenberg and D. Gale, Consensus of subjective probabilities: the pari-mutuel method, The Annals of Mathematical Statistics 30(1):165–168, 1959. https://doi.org/10.1214/aoms/1177706369
• V. V. Vazirani and M. Yannakakis, Market equilibrium under separable, piecewise-linear, concave utilities, Journal of the ACM 58(3), 2011. https://doi.org/10.1145/1970392.1970394

Motivation

Thompson Sampling is the oldest heuristic for the multi-armed bandit problem: proposed by Thompson in 1933, it plays each arm with the posterior probability that the arm is the best one. It is simple to implement, performs well empirically (Chapelle and Li, NIPS 2011), and has been used in production systems such as click-through-rate prediction for search advertising. For a long time, however, no finite-time regret guarantee was known for it: the analyses available before 2012 gave only $o(T)$ regret.

Agrawal and Goyal (arXiv:1111.1797, COLT 2012) gave the first logarithmic bounds on the expected regret of Thompson Sampling. This mission formalizes their bound for the general case of $N$ arms (their Theorem 2). A companion mission of the same series formalizes their two-armed bound (Theorem 1), whose proof is independent.

Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least of order $\sum_i \frac{\Delta_i}{D(\mu_i\|\mu_1)}\ln T$. Auer, Cesa-Bianchi and Fischer (2002) showed that UCB1 achieves $O(\sum_i \ln T/\Delta_i)$ in finite time. Agrawal and Goyal (2012) proved $O((\sum_a 1/\Delta_a^2)^2\ln T)$ for Thompson Sampling with $N$ arms; Kaufmann, Korda and Munos (2012) and Agrawal and Goyal (2013) later proved the asymptotically optimal constant for Bernoulli rewards.

Setting

A stochastic $N$-armed bandit has arms $1,\dots,N$. Arm $i$, when played, yields a random reward drawn from a fixed distribution $\nu_i$ supported in $[0,1]$, with mean $\mu_i$; rewards of an arm are i.i.d. and independent of the other arms. Arm $1$ is assumed to be the unique optimal arm, $\mu_1>\mu_i$ for $i\ne1$, and $\Delta_i=\mu_1-\mu_i>0$ is the gap of arm $i$.

Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm $i$, a count $S_i$ of successes and $F_i$ of failures, both starting at $0$. In each round $t$ it draws $\theta_i(t)\sim\mathrm{Beta}(S_i+1,F_i+1)$ independently for every arm, plays $i(t)=\arg\max_i\theta_i(t)$, observes a reward $\tilde r_t\sim\nu_{i(t)}$, performs a Bernoulli trial with success probability $\tilde r_t$, and increments $S_{i(t)}$ on success and $F_{i(t)}$ on failure.

The expected regret in time $T$ is

$$\mathbb E[\mathcal R(T)]=\mathbb E\Big[\sum_{t=1}^T(\mu^*-\mu_{i(t)})\Big],\qquad \mu^*=\max_i\mu_i,$$

the expectation being over the rewards, the Bernoulli trials and the posterior samples.

The proof works with the reward stacks $Z_{i,m}$: the outcome of the $m$-th Bernoulli trial of arm $i$, all independent. Then $s(j)=\sum_{m\le j}Z_{1,m}$, the number of successes in the first $j$ plays of arm $1$, is a $\mathrm{Binomial}(j,\mu_1)$ random variable. The other objects of the proof are the threshold $L_i=24\ln T/\Delta_i^2$, the saturated set $C(t)$ of suboptimal arms with at least $L_i$ plays before round $t$, the intervals $I_j$ between the $j$-th and $(j+1)$-th plays of arm $1$, and the counts $\gamma_j$ and $V_j^{\ell,a}$ defined in §4.

Formalization targets

Goal: Theorem 2

There is an absolute constant $C>0$ such that for every $N\ge2$, every instance as above and every horizon $T\ge2$,

$$\mathbb E[\mathcal R(T)]\le C\Big(\sum_{a=2}^N\frac{1}{\Delta_a^2}\Big)^2\ln T .$$

$C$ does not depend on $N$, on the reward distributions or on $T$.

Milestones

1. Lemma 4: with $E(t)$ the event that every saturated arm's sample lies within $\Delta_i/2$ of its mean, $\Pr(E(t))\ge1-4(N-1)/T^2$, also conditionally on $s(j)=s$.
2. Lemma 5 (Eq. (7)): the expected regret from saturated arms inside $I_j$ is at most $\mathbb E\big[\mathbb E[\gamma_j+1\mid s(j)]\sum_a\Delta_a\mathbb E[\min\{X(j,s(j),\mu_a+\Delta_a/2),T\}\mid s(j)]\big]$.
3. Lemma 1: $\mathbb E[X(j,s,y)]=1/F^B_{j+1,y}(s)-1$, where $X(j,s,y)$ counts the trials before an independent $\mathrm{Beta}(s+1,j-s+1)$ sample exceeds $y$.
4. Lemma 3: a three-case bound on $\mathbb E[\mathbb E[\min\{X(j,s(j),y),T\}\mid s(j)]]$ in terms of the Bernoulli KL divergence $D$ between $y$ and $\mu_1$.

Significance

The result. Theorem 2 shows that Thompson Sampling, a randomized Bayesian heuristic, achieves regret logarithmic in the horizon for any number of arms with bounded rewards, matching the order in $T$ of the Lai–Robbins lower bound. Its dependence on the gaps, $(\sum_a\Delta_a^{-2})^2$, is worse than UCB1's; the paper's own Remark 1 and later work improve it. The proof introduced the device of bounding the waiting time between plays of the optimal arm through geometric variables with Beta-cdf parameters (Lemmas 1 and 3), which reappears in later analyses of Thompson Sampling.

Formalizing it. The theorem is proved on paper; it has not been machine-checked. Bandit theory in Lean (bandit environments, regret, UCB-type analyses) is still young, and no Beta–Bernoulli Thompson Sampling result is formalized. The mission produces a Lean model of Algorithm 2 for general $[0,1]$ rewards with the paper's stack coupling, the §4 bookkeeping of saturated arms and intervals, and the paper's lemmas as separate targets.

Difficulty

Two difficulties are specific to the $N$-armed analysis. First, the arm that competes with arm $1$ changes over time: the set of saturated arms grows, and which saturated arm is "best" depends on the history, so the waiting time between plays of arm $1$ cannot be compared with a single geometric variable as in the two-armed case. Second, the number $\gamma_j$ of rounds at which arm $1$'s sample is large but arm $1$ is not played is not independent of the counts $V_j^{\ell,a}$: both depend on the same posterior samples, and Lemma 5 needs a careful conditioning on the history to separate them. The obvious union bound over arms, treating each suboptimal arm as in the two-armed proof, fails because it ignores the interruptions by unsaturated arms, whose number is the source of the squared sum in the bound.

Formalization scope

• Probability space. Algorithm 2 is realized on a product of three independent i.i.d. tables: Beta draws indexed by (arm, round, successes, failures), rewards indexed by (arm, round) and uniform variables indexed by (arm, round); the Bernoulli trial of a round succeeds when the played arm's uniform variable is below its reward. The law of the run is that of Algorithm 2, which runs for every round $t=1,2,\dots$. $s(j)$ is the number of successful trials among the first $j$ plays of arm $1$ in this infinite run (possibly after the horizon $T$), so it is a $\mathrm{Binomial}(j,\mu_1)$ random variable for every $j$, as the paper's independent $Z_{1,m}$ make it. Ties in the arg max (probability $0$) go to the smallest index.
• Indexing. Arms are Fin N, and Lean arm 0 is the paper's arm $1$. Rounds are $0,\dots,T-1$; Lean round $t$ is the paper's round $t+1$. Sums over $a=2,\dots,N$ are sums over $a\ne0$.
• Expectations are lower Lebesgue integrals in $[0,\infty]$, which has no junk value for non-integrable functions. Conditional expectations given $s(j)$ are written as finite sums over the values of $s(j)$.
• The $O(\cdot)$. The paper writes $O(\cdot)$ in the sense of its footnote 1 ($f(n)\le c\,g(n)$ for $n\ge n_0$). The goal states it with one universal constant $C$, quantified before $N$, the instance and $T$, for every $T\ge2$. The explicit constants printed in App. D are not formalized: expanding the paper's Eq. (21) gives terms $288(N-1)(\ln T)\sum_a\Delta_a^{-2}$ and $48(N-1)^2$ where the paper prints $288(\ln T)\sum_i\Delta_i^{-2}$, and Eq. (22) drops a factor $\ln T$ in its $192/\Delta_a^2$ term. The $O(\cdot)$ claim does not depend on these slips; a statement pinned to the printed numerals might be false.
• Ruled out. A constant depending on $N$, on the means or on $T$; a fixed number of arms; Bernoulli rewards only; or any algorithm other than Algorithm 2 would each make the goal a different and weaker theorem. The statement quantifies over all $N\ge2$ and all reward distributions on $[0,1]$.
• Not included. Eq. (8), the bound $\sum_{j}\mathbb E[\gamma_j\mid s(j)]\le\sum_uL_u+4(N-1)$ "for all instantiations", is not a milestone: each term is conditioned on a different $s(j)$, and the pointwise reading does not follow from the argument given. Remark 1 (an alternate bound) and App. A (several optimal arms) are not part of this mission.
• Contributions welcome: Beta–Binomial identities, geometric waiting times, Hoeffding bounds for binomial cdfs, and the stopping-time arguments behind Lemma 5. Lemma 1 and Lemma 3 are shared with the two-armed mission of this series.

Selected references

• S. Agrawal and N. Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem, COLT 2012; arXiv:1111.1797v3, 2012. https://arxiv.org/abs/1111.1797
• W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25, 1933. https://doi.org/10.1093/biomet/25.3-4.285
• T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• O. Chapelle and L. Li, An empirical evaluation of Thompson Sampling, NIPS 2011. https://papers.nips.cc/paper/4321-an-empirical-evaluation-of-thompson-sampling
• E. Kaufmann, N. Korda and R. Munos, Thompson Sampling: an asymptotically optimal finite-time analysis, ALT 2012. https://arxiv.org/abs/1205.4217
• S. Agrawal and N. Goyal, Further optimal regret bounds for Thompson Sampling, AISTATS 2013. https://arxiv.org/abs/1209.3353

Motivation

A Markov decision problem models a system that is observed once per period and controlled by choosing an action: the action earns an immediate income and determines the probabilities of the next state. Inventory control, machine replacement, queue admission and many reinforcement-learning benchmarks are of this form. With future income discounted by a factor $\beta<1$, Howard (Dynamic Programming and Markov Processes, 1960) showed how to compute an optimal policy by policy improvement. The undiscounted problem ($\beta=1$) is harder, because total income is typically infinite.

David Blackwell's Discrete Dynamic Programming (Ann. Math. Statist. 33 (1962) 719–726) treats $\beta=1$ as a limit of $\beta<1$. Its Theorem 5 shows that some stationary policy is optimal simultaneously for all discount factors sufficiently close to $1$. Such policies are now called Blackwell optimal, and the result is the base of sensitive discount optimality (Veinott, 1969) and of the standard textbook treatment of average-reward problems (Puterman, Markov Decision Processes, 1994, Ch. 10).

Timeline. Howard (1960): policy iteration for discounted and average-reward finite problems. Blackwell (1962): Theorem 5 (Blackwell optimal stationary policies exist) and the characterization of nearly optimal stationary policies (Theorem 4, the subject of the companion mission). Miller and Veinott (Ann. Math. Statist. 40 (1969) 366–370), Veinott (Ann. Math. Statist. 40 (1969) 1635–1660): Laurent expansions of $V_\beta$ in $1-\beta$ and $n$-discount optimality.

Setting

There are finitely many states $s$ and a finite set $A$ of actions, every action available in every state. In state $s$, action $a$ yields income $i(s,a)\in\mathbb R$ (any sign) and moves the system to state $s'$ with probability $q(s'\mid s,a)$; each $q(\cdot\mid s,a)$ is a probability vector.

A decision rule is a function $f$ from states to actions; $F$ is the finite set of decision rules. A policy is a sequence $\pi=\{f_n,\ n=1,2,\dots\}$ in $F$: on day $n$, in state $s$, action $f_n(s)$ is used. Policies are deterministic and Markov but may change with time. The policy $(f,\pi)$ uses $f$ on day $1$ and then follows $\pi$; $f^{(\infty)}$ uses $f$ every day and is called stationary.

For $f\in F$, $r(f)$ is the vector $(i(s,f(s)))_s$ and $Q(f)$ the Markov matrix $(q(s'\mid s,f(s)))_{s,s'}$. With $Q_0(\pi)=I$ and $Q_n(\pi)=Q(f_1)\cdots Q(f_n)$, the return of $\pi$ at discount factor $0\le\beta<1$ is

$$V_\beta(\pi)=\sum_{n=0}^\infty \beta^n\,Q_n(\pi)\,r(f_{n+1}),$$

a vector indexed by the initial state. Vectors are compared coordinatewise; $w_1>w_2$ means $w_1\ge w_2$ and $w_1\ne w_2$.

A policy $\pi^*$ is $\beta$-optimal if $V_\beta(\pi^*)\ge V_\beta(\pi)$ for every policy $\pi$. Following §4 of the paper, a policy is optimal if it is $\beta$-optimal for all $\beta$ sufficiently near $1$.

Formalization targets

Goal: Theorem 5

There exist a decision rule $f$ and $\beta_0<1$ such that

$$V_\beta(f^{(\infty)})\ \ge\ V_\beta(\pi)\qquad\text{for all }\beta\in(\beta_0,1)\text{ and all policies }\pi.$$

One $f$ and one $\beta_0$ serve every competing policy and every $\beta\in(\beta_0,1)$.

Milestones

1. The composition rule $V_\beta(f,\pi)=L(f)V_\beta(\pi)$, with $L(f)w=r(f)+\beta Q(f)w$, and its $N$-fold version (§2).
2. Theorem 1: if $V_\beta(f,\pi^*)\le V_\beta(\pi^*)$ for all $f\in F$, then $\pi^*$ is $\beta$-optimal.
3. Theorem 2: if $V_\beta(f,\pi)>V_\beta(\pi)$ then $V_\beta(f^{(\infty)})>V_\beta(\pi)$.
4. Theorem 3 (policy improvement): if no action improves $f^{(\infty)}$ by one step, $f^{(\infty)}$ is $\beta$-optimal; otherwise switching to improving actions gives $g^{(\infty)}>f^{(\infty)}$.
5. Corollary: for each fixed $\beta\in[0,1)$ some stationary policy is $\beta$-optimal.
6. Each coordinate of $V_\beta(f^{(\infty)})$ is a rational function of $\beta$ on $[0,1)$ with nonvanishing denominator.
7. Some $f^*$ is $\beta$-optimal for a set of $\beta$'s having $1$ as a limit point.
8. If $V_\beta(f^{*(\infty)})\ge V_\beta(g^{(\infty)})$ for a set of $\beta$'s accumulating at $1$, then it holds for all $\beta$ near $1$.

Significance

The result. Theorem 5 shows that the infinitely many discounted problems near $\beta=1$ share a common optimal stationary policy. Such a policy is also optimal for the long-run average criterion, which settles the existence of average-optimal stationary policies in finite models without any recurrence assumption. It also justifies computing undiscounted solutions as limits of discounted ones, and it is the first case of the sensitive optimality criteria developed later.

Formalizing it. The theorem is classical and proved in the paper and in the textbooks; there is no machine-checked proof of it in Blackwell's model on the platform. A related open item, SennottDP.AvgFinite.prop_6_2_3_blackwell_optimal, states the textbook version for nonnegative costs and randomized history-dependent policies; the present mission is Blackwell's own formulation with incomes of either sign and deterministic Markov policies. A complete development also yields a verified policy improvement theorem (Theorem 3) and the rationality of discounted values in $\beta$, both reusable for any finite-state discounted model.

Difficulty

The Corollary gives, for each $\beta$, some optimal stationary policy, and $F$ is finite, so one $f^*$ is $\beta$-optimal for infinitely many $\beta$ accumulating at $1$. The obvious argument stops there: optimality on a sequence of $\beta$'s says nothing about the $\beta$'s in between, and a pointwise limit argument cannot produce a whole interval $(\beta_0,1)$. The step that fails is passing from "frequently" to "eventually", and it needs structural information about how $V_\beta$ depends on $\beta$, not just continuity. A second difficulty is the comparison class: optimality must hold against all time-dependent policies, not only the finitely many stationary ones, so the final step has to bring the Corollary back in for every $\beta$ near $1$.

Formalization scope

States and actions are finite nonempty Lean types St, Act; decision rules are functions St → Act and policies are sequences ℕ → St → Act, indexed from $0$ (π 0 is Blackwell's $f_1$). Incomes are real-valued with no sign restriction. The law of motion law s a s' $=q(s'\mid s,a)$ satisfies the published predicate IsTransitionKernel. $Q_n(\pi)$ is the ordered matrix product and $V_\beta(\pi)$ is the tsum of the series, which converges absolutely for $0\le\beta<1$; every statement at a fixed $\beta$ assumes $0\le\beta<1$, and nothing is stated for $\beta\ge1$. Vector inequalities are coordinatewise, and the strict order is "$\ge$ and $\ne$", not coordinatewise strict. "$\beta$ sufficiently near $1$" is "there is $\beta_0<1$ such that for every $\beta\in(\beta_0,1)$". The paper's §4 phrase $V_\beta(\pi)=U(\beta)$ is encoded as $\beta$-optimality, so no supremum over policies appears.

The word "optimal" has two meanings in the paper: at one fixed $\beta$ (§3, the Corollary) and for all $\beta$ near $1$ (§4, Theorem 5). The Lean development keeps them apart as IsBetaOptimal β and IsOptimal. A statement of Theorem 5 at a single $\beta$, with "there exists $\beta$", for a set of $\beta$'s accumulating at $1$, or against stationary policies only would be a different and weaker theorem; the goal rules all of these out.

Needed infrastructure: summation and shifting of the discounted series, Neumann series $(I-\beta Q)^{-1}=\sum_n\beta^nQ^n$ for stochastic $Q$, Cramer's rule to express $(I-\beta Q)^{-1}r$ as a ratio of polynomials in $\beta$, and the fact that a nonzero polynomial has finitely many roots. The policy improvement theorem and the rationality lemma are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• R. A. Howard, Dynamic Programming and Markov Processes, Technology Press and Wiley, 1960.
• A. F. Veinott Jr., Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999 (Proposition 6.2.3, Blackwell optimality for finite models). https://doi.org/10.1002/9780470317037

Motivation

Selfish routing and resource sharing are modelled by congestion games: each player picks a set of shared resources, and the cost of a resource grows with the number of players using it. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures how much worse the social cost of a worst Nash equilibrium is than the optimum. For non-atomic (infinitesimal) traffic with linear latencies, Roughgarden and Tardos (J. ACM 2002) showed the ratio is $4/3$. Christodoulou and Koutsoupias (STOC 2005) turned to finite (atomic, unweighted) congestion games, where each of $N$ players controls one indivisible unit of load, and determined the pure price of anarchy for linear latencies in four settings: asymmetric or symmetric strategy sets, and average or maximum social cost. Awerbuch, Azar and Epstein (STOC 2005) obtained the value $5/2$ for the asymmetric average case independently.

This mission covers the symmetric average-cost entry of that table (Sect. 3.2 of the paper). It shows that when all players share one strategy set, the ratio is not $5/2$ but $(5N-2)/(2N+1)$, which depends on the number of players and tends to $5/2$ only as $N\to\infty$.

Setting

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

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

(cost), and the social cost is $\mathrm{SUM}(A)=\sum_i c_i(A)$ (sumCost), $N$ times the average cost. A profile $A$ is a pure Nash equilibrium (IsPureNash) if $c_i(A)\le c_i(A_{-i},S)$ for every player $i$ and every $S\in\Sigma_i$, where $(A_{-i},S)$ replaces $A_i$ by $S$.

Latencies are linear (IsLinear) when $f_e(k)=a_ek+b_e$ with $a_e,b_e\ge0$. The game is symmetric (IsSymmetric) when all players have the same strategy set, $\Sigma_i=\Sigma$. The pure price of anarchy of a class of games is the supremum, over games in the class and pure Nash equilibria $A$, of $\mathrm{SUM}(A)/\mathit{opt}$, with $\mathit{opt}=\min_P\mathrm{SUM}(P)$.

Formalization targets

Goal: Theorems 3 and 4

For every $N\ge1$: every pure Nash equilibrium $A$ of every symmetric linear congestion game with $N$ players satisfies

$$\mathrm{SUM}(A)\le\frac{5N-2}{2N+1}\,\mathrm{SUM}(P)\quad\text{for every profile }P,$$

and some symmetric linear game with $N$ players has a pure Nash equilibrium $A$ and a profile $P$ with $\mathrm{SUM}(P)>0$ and equality. Together these state that the pure price of anarchy of the class is exactly $(5N-2)/(2N+1)$.

Milestones

1. Lemma 1: $\beta(\alpha+1)\le\frac13\alpha^2+\frac53\beta^2$ for nonnegative integers $\alpha,\beta$.
2. Theorem 3, proof: the Nash inequality of player $i$ against the strategy $P_j$ of any player $j$.
3. Theorem 3, proof: the bound on $N\,c_i(A)$ obtained by summing over $j$.
4. Theorem 3, proof: the bound on $\mathrm{SUM}(A)$ obtained by summing over $i$.
5. Theorem 3: the upper bound alone.
6. Theorem 4: the matching instances alone.

Significance

The result separates symmetric from asymmetric games for every finite number of players: for $N=2$ the symmetric bound is $8/5$, for $N=3$ it is $13/7$, against $5/2$ for asymmetric games with $N\ge3$ players. Theorem 4 shows the bound is tight, so the function $N\mapsto(5N-2)/(2N+1)$ is the exact answer, not an artefact of the proof. The asymptotic value $5/2$ coincides with the asymmetric one, which says that symmetry helps only by a vanishing amount for large populations. Later work on smoothness arguments (Roughgarden, STOC 2009) takes the $5/2$ bound of this paper as its central example.

The theorems are proved in the paper; the authors print the proofs for identity latencies $f_e(k)=k$ and state that they extend to $a_ek+b_e$. No machine-checked proof of these bounds is known to exist. This mission produces a statement for general affine latencies with nonnegative coefficients, the affine forms of the intermediate inequalities, and an explicit family of instances for every $N$, all of which are reusable for the other entries of the paper's table.

Difficulty

The upper bound requires combining the $N^2$ deviation inequalities (player $i$ against the strategy of each player $j$ in the comparison profile) and then bounding cross terms facility by facility; the step that needs care is that the bound of Lemma 1 holds for integer loads only and fails for real numbers, so any argument that relaxes loads to reals loses the constant. The asymmetric argument, which compares player $i$ only with its own optimal strategy $P_i$, gives $5/2$ and cannot see the dependence on $N$.

For the lower bound, the instance must be a Nash equilibrium against every strategy in the common strategy set, which contains the equilibrium strategies of all other players as well as the optimal ones. Exact equality of the ratio requires the block sizes to be tuned to $N$; verifying the equilibrium condition involves counting facilities shared by pairs and triples of players.

Formalization scope

Players are Fin N with $N\ge1$; facilities are an arbitrary finite type with decidable equality; strategies and profiles are Finsets of facilities, with feasibility a separate predicate. Latencies are real-valued functions of the natural-number load. Linear latencies are affine with nonnegative coefficients, as in Sect. 2 of the paper; the milestone inequalities carry the coefficients $a_e,b_e$ explicitly and reduce to the printed displays when $a_e=1$, $b_e=0$. The Nash condition is in cost form. Upper bounds are stated against every feasible profile $P$, which is equivalent to the bound on $\mathrm{SUM}(A)/\mathit{opt}$ without dividing by $\mathit{opt}$. All constants are computed in $\mathbb R$.

The lower bound requires $\mathrm{SUM}(P)>0$: without it the statement is satisfied by zero latencies or empty strategies, where both sides vanish. Symmetry is a hypothesis of the upper bound and a property of the instance; without it the upper bound is false, since asymmetric instances reach $5/2$.

A complete development needs finite-sum manipulations (double counting $\sum_j\sum_{e\in P_j}=\sum_e n_e(P)$), the integer inequality of Lemma 1, and an explicit facility type for the instance. The model layer is shared with the other missions of this series. Proofs of the milestones and alternative proofs of the bound are welcome.

Selected references

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

Motivation

A stochastic approximation algorithm is a recursion $x_{n+1}=x_n+\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$ with decreasing step sizes $\gamma_n$ and a noise term $U_{n+1}$. Recursions of this form appear in stochastic gradient methods, adaptive control, learning in games (fictitious play, reinforcement learning) and urn models. The ODE method compares the iterates with the solutions of $\dot x=F(x)$. In Benaïm's lecture notes (Benaïm 1999), the comparison is phrased through the continuous-time interpolated process $X$. Under standard noise conditions, $X$ is almost surely an asymptotic pseudotrajectory of the flow of $F$, and its limit set is almost surely internally chain transitive.

That theorem constrains where the process may end up. It does not say which of several candidate sets the process actually reaches. When the ODE has several attractors, for example several stable equilibria of a learning dynamic or several stable compositions of an urn, an application needs to know that each attractor is reached with positive probability. Section 7 of the notes answers this question. The answer is a criterion of attainability: if the process can, with positive probability and at arbitrarily late times, enter the basin of an attractor, then it converges to that attractor with positive probability.

Timeline.

• Kushner and Clark (1978) proved convergence statements for processes that visit a compact subset of the domain of attraction of an asymptotically stable equilibrium infinitely often.
• Arthur, Ermoliev and Kaniovski (1983) and Pemantle (1990) studied urn processes whose limit points depend on the trajectory.
• Benaïm (1997) and Duflo (1997, Random Iterative Models) developed the attainability argument for general stochastic approximation processes.
• Benaïm (1999) states it for arbitrary attractors of a semiflow on a locally compact metric space, under a single conditional shadowing condition (24).

Setting

Let $(M,d)$ be a metric space and let $\Phi=(\Phi_t)_{t\ge0}$ be a semiflow on $M$: a continuous map $(t,x)\mapsto\Phi_t(x)$ with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$.

• A set $A$ is invariant if $\Phi_t(A)=A$ for all $t\ge0$, and positively invariant if $\Phi_t(A)\subset A$.
• An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ on which $\operatorname{dist}(\Phi_tx,A)\to0$ uniformly. Its basin $B(A)$ is the set of points $x$ with $\operatorname{dist}(\Phi_tx,A)\to0$.
• A continuous curve $X:\mathbb R_+\to M$ is an asymptotic pseudotrajectory if $\sup_{0\le h\le T}d(X(t+h),\Phi_h(X(t)))\to0$ as $t\to\infty$, for every $T>0$.
• The limit set of $X$ is $L(X)=\bigcap_{t\ge0}\overline{X([t,\infty))}$.
• For $T>0$, $d_X(T)=\sup_{k\in\mathbb N}d(\Phi_T(X(kT)),X(kT+T))$.

Now let $X=(X(t))_{t\ge0}$ be a process on a probability space $(\Omega,\mathcal F,P)$ with continuous paths in $M$, adapted to a filtration $(\mathcal F_t)_{t\ge0}$. The standing assumption of Section 7 is that for all $\delta>0$, $T>0$ and $t\ge0$,

$$P\Big(\sup_{s\ge t}\ \sup_{0\le h\le T}d\big(X(s+h),\Phi_h(X(s))\big)\ge\delta\ \Big|\ \mathcal F_t\Big)\le w(t,\delta,T)\tag{24}$$

for a function $w\ge0$ with $w(t,\delta,T)\downarrow0$ as $t\to\infty$.

A point $p$ is attainable if $P(\exists s\ge t: X(s)\in U)>0$ for every $t>0$ and every open neighbourhood $U$ of $p$. $\mathrm{Att}(X)$ is the set of attainable points.

Formalization targets

Goal: Theorem 7.3, first statement

If $M$ is locally compact, $A$ is an attractor of $\Phi$, and $\mathrm{Att}(X)\cap B(A)\neq\emptyset$, then

$$P\big(L(X)\subset A\big)>0 .$$

This statement contains no constants and no rates, so it does not depend on how (24) is quantified for a particular algorithm.

Theorem 7.3, second statement

If $U$ is open and relatively compact with $\overline U\subset B(A)$, there are $T,\delta>0$, depending only on $U$ (and on $\Phi$, $A$), such that for every process satisfying the standing assumption and every $t\ge0$

$$P\big(L(X)\subset A\big)\ge\big(1-w(t,\delta,T)\big)\,P\big(\exists s\ge t:\ X(s)\in U\big).$$

Milestones

• Lemma 6.8. For a nonempty compact $K\subset B(A)$ there are $T,\delta>0$ such that every asymptotic pseudotrajectory with $X(0)\in K$ and $d_X(T)<\delta$ has $L(X)\subset A$.
• Lemma 7.1, in three parts:
  • $\mathrm{Att}(X)$ is closed;
  • it is positively invariant;
  • it contains $L(X)$ almost surely.

Significance

The result. Theorem 7.3 turns a question about the long-run limit of a random process into a question about where the process can go. Attainability is usually checked by a controllability argument: the noise can push the iterates in every direction. For urn processes with an urn function mapping the simplex into its interior, every point is attainable (Example 7.2 of the notes). Then every attractor of the mean ODE is reached with positive probability. Combined with nonconvergence results for unstable sets (Section 9 of the notes), this characterizes the possible limits of many learning and urn processes. Theorem 7.3 is the positive half of that picture.

Formalizing it. The theorem has a published proof (p. 32 of the notes) and no machine-checked version. A formal proof needs the following:

• a precise reading of the conditional shadowing condition (24) as a conditional expectation of an indicator;
• the stopping-time decomposition of the event $\{\exists s\ge t: X(s)\in U\}$ over dyadic times;
• the deterministic Lemma 6.8, which rests on the limit set theorem for precompact asymptotic pseudotrajectories (Theorem 5.7 of the notes, the subject of mission 1 of this series).

Difficulty

The obvious argument says: once $X$ enters a compact part of the basin, the flow carries it into $A$. That fails because $X$ is not a trajectory of the flow. Each window of length $T$ adds an error, and errors over infinitely many windows can push the process out of the basin.

Two things are needed instead:

• A uniform version of the deterministic statement, with $T$ and $\delta$ fixed in advance from the compact set alone. This is Lemma 6.8, which needs local compactness of $M$ and the structure of limit sets of asymptotic pseudotrajectories.
• A probabilistic step that applies (24) at the random time when $X$ first enters $U$. That time is not a stopping time on a continuum, and conditioning at it needs care.

A naive union bound over all times is useless: it does not use the conditional form of (24).

Formalization scope

• The semiflow is Mathlib's Flow ℝ≥0 M on a metric space; local compactness is LocallyCompactSpace M.
• The process is X : ℝ≥0 → Ω → M with continuous paths. The paper's alternative of càdlàg paths is not covered.
• Adaptedness is Borel measurability of $X(t)$ with respect to $\mathcal F_t$, for a Mathlib Filtration ℝ≥0. $P$ is a probability measure.
• The suprema in (24) and in $d_X(T)$ are computed in $[0,\infty]$ with the extended distance, so that "sup $\ge\delta$" and "sup $<\delta$" are exact even when the supremum is infinite or not attained.
• The conditional probability in (24) is the conditional expectation of the indicator of the event. The event is required to be measurable, so the condition cannot hold vacuously through a junk conditional expectation.
• $w$ is required to be both nonincreasing in $t$ and convergent to $0$.
• The events $\{L(X)\subset A\}$ and $\{\exists s\ge t: X(s)\in U\}$ are measured with $P$ as an outer measure, so no measurability hypothesis is added for them.
• In the second statement of Theorem 7.3, $T$ and $\delta$ are chosen before the probability space, the process, $w$ and $t$.
• Invariance in the definition of an attractor is the equality $\Phi_t(A)=A$, not inclusion.
• The almost-sure clause of Lemma 7.1 is stated for separable $M$. Without separability it cannot be proved in ordinary set theory.

These choices rule out the trivializing formalizations: a conditional-probability hypothesis that holds vacuously, invariance read as inclusion, constants $T,\delta$ that depend on the process or on $t$, and a probability bound $w$ without monotonicity.

A complete development needs:

• limit sets of asymptotic pseudotrajectories and the fact that an internally chain transitive set meeting the basin of an attractor lies in the attractor (shared with missions 1 and 5 of this series);
• measurability of path functionals of continuous processes;
• conditioning on events of the form $\{\tau=t_n(k)\}$ at dyadic times.

The first and second are reusable well beyond this mission. Contributions toward either, and alternative proofs of Lemma 6.8, are welcome.

Selected references

• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Benaïm, M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
• M. Benaïm, Vertex-reinforced random walks and a conjecture of Pemantle, Annals of Probability 25 (1997), 361–392. https://doi.org/10.1214/aop/1024404292
• M. Duflo, Random Iterative Models, Applications of Mathematics 34, Springer, 1997. https://doi.org/10.1007/978-3-662-12880-0
• H. J. Kushner, D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8
• C. Conley, Isolated Invariant Sets and the Morse Index, CBMS Regional Conference Series in Mathematics 38, AMS, 1978. https://doi.org/10.1090/cbms/038