Motivation

In an aggregative game, each player's cost depends on its own decision and on the sum of all players' decisions. That form appears in resource sharing, production, and network games: a player may know its own choice while lacking a central feed of the aggregate. A distributed algorithm therefore has to estimate the aggregate through local communication as it updates decisions. Koshal, Nedić, and Shanbhag study this setting and give both synchronous and gossip schemes in Distributed Algorithms for Aggregative Games on Graphs. This mission concerns their asynchronous scheme, in which a random pair communicates at each tick.

The question is whether irregular, local updates still find the game's equilibrium when no agent knows in advance how often it will be selected. Each agent uses its own update count to set its step length. The paper's Proposition 3 states almost-sure convergence under strict monotonicity, compact strategy sets, and a connected graph. The result is a convergence claim about the complete random process, including who wakes, whom they contact, which estimate they exchange, and which projected step they take.

Setting

There are $N\ge1$ agents. Agent $i$ chooses $x_i\in K_i\subseteq\mathbb R^n$, with $K_i$ nonempty, compact, and convex. A strategy profile is $x=(x_1,\ldots,x_N)$ in $K=\prod_i K_i$, and its aggregate is $\bar x=\sum_i x_i$. The map $F_i(x_i,u)$ is the player's first-order response when its own decision is $x_i$ and its aggregate argument is $u$. The game map is $\phi_i(x)=F_i(x_i,\bar x)$. A solution $x^*$ of the variational inequality $\mathrm{VI}(K,\phi)$ is feasible and satisfies

$$\sum_i\langle x_i-x_i^*,\phi_i(x^*)\rangle\ge0 \quad\text{for every }x\in K.$$

The paper obtains $F_i$ from differentiable convex player costs, making VI solutions Nash equilibria. The formal statements take $F_i$ as the primitive map used by the algorithm. Strict monotonicity means $\sum_i\langle\phi_i(x)-\phi_i(y),x_i-y_i\rangle>0$ for different feasible profiles $x,y$. Along with continuity and compact convex strategy sets, it makes the VI solution unique. The paper's Assumptions 1–3 also impose a uniform Lipschitz bound on how $F_i(x_i,u)$ changes with $u$.

Agents occupy a connected, undirected graph. At a discrete tick $k$, a uniformly selected agent $I^k$ contacts a neighbour $J^k$ with probability $p_{I^kJ^k}>0$ on every edge. The ordered pairs are independent across ticks. Each agent maintains an aggregate estimate $v_i^k$; the selected pair average their estimates to form $\hat v_i^k$. Those agents take a projected step using $F_i(x_i^k,N\hat v_i^k)$ and then add their decision change to the estimate. Other agents retain their decisions and estimates. Initially $v_i^0=x_i^0$. The number $\Gamma_k(i)$ counts agent $i$'s updates through tick $k$, and its step length at an update is $\alpha_{k,i}=1/\Gamma_k(i)$. Equations (23)–(29) of the paper define these operations.

Formalization targets

Goal: almost-sure equilibrium convergence

Under Assumptions 1–3 and connectedness of the gossip graph, Proposition 3 asserts that there is a unique $x^*$ solving $\mathrm{VI}(K,\phi)$ and that the generated process satisfies

$$\Pr\bigl(\lim_{k\to\infty}x^k=x^*\bigr)=1.$$

The goal includes existence and uniqueness of $x^*$, rather than conditioning convergence on a possibly nonexistent solution. Its random draws have the rate-one-clock law: $\Pr(I^k=i,J^k=j)=p_{ij}/N$.

Milestones

The five milestones record the VI's unique solution from the proof of Proposition 1, conservation of the agents' average estimate in Lemma 2, the almost-sure stepsize bounds of Lemma 7, their summability consequences in Corollary 1, and the mean-square gossip contraction in relations (30)–(31). They cover the equilibrium, tracking, step length, and network-mixing parts of the claim. Their source wording, indices, and PDF pages are attached to the mission items.

Significance

The result shows that a shared aggregate can be learned well enough through pairwise, random exchanges to reach the same equilibrium characterized by the centralized VI. Update counts permit agents to choose diminishing steps without a common iteration clock or a schedule ensuring equal participation on each finite interval. Connectedness and positive contact probabilities ensure every graph edge can carry information. The convergence assertion is almost sure, so it concerns individual sample paths outside a null set, rather than merely an average error.

Formalizing the result would connect finite graph gossip, random update counts, projected VI iteration, and almost-sure convergence in one reusable development. The paper proves Proposition 3; this mission supplies an open machine-checked target, not a claim that the result is unresolved mathematically. A proof would need honest probability statements for the draw law and summability and a projection interface that does not assign arbitrary values on empty sets. The VI existence and uniqueness milestone can also serve other compact, strictly monotone games.

Difficulty

Pairwise averaging preserves the mean estimate, but it does not make each agent's estimate equal to that mean at every step. A projected decision change immediately perturbs the local estimate again. The selected agents and their step lengths also depend on the same update history, so deterministic simultaneous-update arguments do not directly apply. The paper controls this interaction using update-count asymptotics, contraction of the random gossip matrix, and almost-sure summability. None of those conclusions follows from connectedness alone if a nominal edge has zero contact probability.

Formalization scope

Lean represents each decision in EuclideanSpace ℝ (Fin n) and profiles as functions on Fin N. The aggregate is a finite sum. A projection is the relation saying that the selected point lies in its set and minimizes Euclidean distance, rather than a total function with an arbitrary output on an empty set. The profile topology used for convergence is the finite product topology. For vectors indexed by agents, relations (30)–(31) use the explicit Euclidean coordinate norm; the default norm of Fin N → ℝ is a sup norm.

The continuous-time Poisson clocks are encoded through their induced independent discrete tick pairs and exact joint law. Initial decisions are fixed and feasible. The source allows random initial decisions; the formal goal covers every deterministic start. This restriction is recorded because the paper's stated random initialization would require an explicit independence relation with future clock draws. Tick indices start at zero in Lean; a selected agent has $\Gamma_k(i)\ge1$, so the value assigned to $1/0$ never drives an update. The positive-time series and bounds still begin at $k=1$.

The paper gives the Lipschitz condition on aggregate arguments only in the feasible aggregate set $\bar K$. Its algorithm can evaluate $F_i$ outside that set, as its own footnote acknowledges. This development explicitly extends that condition to all of $\mathbb R^n$ to make those evaluations controlled. The change is substantive and disclosed on each affected item; the preprint's Lemma 3 proof contains the corresponding domain gap. The goal assumes neither the stepsize estimates nor the network contraction nor convergence of the estimate errors; they remain mathematical work. Further contributions may formalize the omitted intermediate lemmas, or refine the initialization and domain assumptions while preserving a meaningful statement.

Selected references

• J. Koshal, A. Nedić, and U. V. Shanbhag, Distributed Algorithms for Aggregative Games on Graphs, Operations Research 64(3), 680–704, 2016. arXiv:1605.00267v2; DOI:10.1287/opre.2016.1501.

Model-free bounds for lookback options

A lookback option pays a function of the running maximum of the underlying asset over the life of the contract. When the prices of European call options of all strikes at the maturity are quoted, the risk-neutral law $\mu$ of the terminal price is known, but the law of the whole path is not. The robust (model-free) superhedging cost of the lookback payoff is the cheapest initial capital that, combined with a static position in the quoted calls and dynamic trading in the underlying, dominates the payoff in every model consistent with $\mu$.

Hobson (Finance Stoch. 1998) computed this cost for $g(x)=x$ by a pathwise inequality, and identified the extremal model through the Azéma–Yor solution of the Skorokhod embedding problem (Azéma–Yor 1979). Galichon, Henry-Labordère and Touzi (Ann. Appl. Probab. 2014, arXiv:1401.3921) recast model-free bounds as a dual stochastic control problem in which the marginal constraint is penalised by a Lagrange multiplier $\lambda$. Their Theorem 3.1 recovers Hobson's bound for every $C^1$ nondecreasing $g$ from that dual, with an explicit optimal multiplier and stopping time. The result is one of the founding examples of martingale optimal transport.

Setting

Let $B$ be a real Brownian motion with continuous paths and $B_0=0$, adapted to a filtration $(\mathcal F_t)_{t\ge0}$ with increments independent of the past, and let $X_t=X_0+B_t$ for a spot $X_0\in\mathbb R$. Write $X^*_\tau=\max_{t\le\tau}X_t$. Let $\mathcal T_\infty$ be the set of stopping times $\tau$ for which the stopped process $(X_{t\wedge\tau})_{t\ge0}$ is a uniformly integrable martingale.

The marginal is a probability measure $\mu$ on $\mathbb R$ with finite first moment and mean $\int x\,\mu(dx)=X_0$. Its call prices are $c(x)=\int(y-x)^+\mu(dy)$. The payoff is $\xi=g(X^*)$ with $g:\mathbb R\to\mathbb R_+$ of class $C^1$ and nondecreasing.

For a multiplier $\lambda:\mathbb R\to\mathbb R$ and $\tau\in\mathcal T_\infty$ set $J(\lambda,\tau)=\mathbb E[g(X^*_\tau)-\lambda(X_\tau)]$ and $u^\lambda(X_0,X_0)=\sup_{\tau\in\mathcal T_\infty}J(\lambda,\tau)$. The admissible multipliers are

$$\Lambda^\mu_0=\Big\{\lambda\in\mathbb L^1(\mu):\ \sup_{\tau\in\mathcal T_\infty}\mathbb E[\lambda(X_\tau)^-]<\infty\Big\},$$

and the reduced superhedging problem (3.7) is

$$U^\mu(\xi)=\inf_{\lambda\in\Lambda^\mu_0}\Big\{\int\lambda\,d\mu+u^\lambda(X_0,X_0)\Big\}.$$

The barycenter function is $b(x)=\int_{[x,\infty)}y\,\mu(dy)/\mu([x,\infty))$ for $\mu((x,\infty))>0$ and $b(x)=x$ otherwise. The Hardy–Littlewood transform $\mu^{HL}$ is the probability measure with

$$\mu^{HL}([y,\infty))=\inf_{\xi<y}\frac{c(\xi)}{y-\xi}.$$

The Azéma–Yor stopping time is $\tau^*=\inf\{t>0:X^*_t\ge b(X_t)\}$, and the candidate multiplier is

$$\lambda^*(x)=\int_{\ell^\mu}^{x}\!\int_{\ell^\mu}^{y}g'(b(\xi))\,\frac{b(d\xi)}{b(\xi)-\xi}\,dy ,$$

that is, the convex function vanishing below $\ell^\mu$ that solves the weak ODE (3.21) with $\psi=b^{-1}$.

Formalization targets

Goal: Theorem 3.1

If $\sup_{\tau\in\mathcal T_\infty}\mathbb E[g(X^*_\tau)]<\infty$ and $\mu^{HL}(g)=\int g\,d\mu^{HL}<\infty$, then

$$U^\mu(\xi)=\mu(\lambda^*)+J(\lambda^*,\tau^*)=\mu^{HL}(g).$$

The goal is the paper's theorem for the reduced problem (3.7), in its full two-equality form: the value, its attainment by $(\lambda^*,\tau^*)$, and its closed form.

Milestones

1. The Neumann condition (3.23) for Peskir's candidate $v^\psi$.
2. Lemma 3.1: $u^\lambda\le v^\psi$ for convex $\lambda\in\Lambda^\mu_0$ and every relaxed free boundary $\psi\in\Psi^\lambda$.
3. Step (1) of Lemma 3.2: $\mu(\lambda)-\lambda(X_0)=\int(c-c_0)\,d\lambda''$, with $c_0(x)=(X_0-x)^+$.
4. Lemma 3.2: $\mu(\lambda)+u^\lambda(X_0,X_0)\le g(X_0)+\int\varphi(\psi(m),m)g'(m)\,dm$.
5. The pointwise minimizations (3.27) and (3.28).
6. Steps (2) and (3) of Lemma 3.3: properties of $\lambda^*$, and the integration by parts giving $\mu^{HL}(g)$.
7. Lemma 3.3, the upper bound $U^\mu(\xi)\le\mu^{HL}(g)$.
8. The Azéma–Yor facts: $\tau^*\in\mathcal T_\infty$, $X_{\tau^*}\sim\mu$, $X^*_{\tau^*}\sim\mu^{HL}$.
9. The lower bound $U^\mu(\xi)\ge\mu^{HL}(g)$ of Section 3.4.

Significance

The theorem identifies the model-free price of a lookback payoff as an explicit functional of the call prices, $\mu^{HL}(g)$, and exhibits the extremal model (Brownian motion stopped at $\tau^*$) and the optimal static hedge ($\lambda^*$). It shows that the dual stochastic control formulation is sharp on a nontrivial path-dependent payoff, which is the template for later work on martingale optimal transport with path-dependent costs.

The result has been proved since 2014 (and Hobson's bound since 1998). It has not been formalized. A complete development would provide machine-checked versions of the Azéma–Yor embedding, the law of the maximum at the embedding, a verification theorem for a reflected optimal stopping problem with a nonsmooth obstacle, and the convex-analytic identities linking call prices to second-derivative measures. Each of these is reusable well beyond this paper.

Difficulty

The upper bound requires a verification argument for an optimal stopping problem of the pair $(X,X^*)$ with a reflection at the diagonal, where the candidate $v^\psi$ is only as regular as the convex multiplier $\lambda$: second derivatives are measures and the free boundary $\psi$ solves its ODE only in a relaxed sense. An Itô formula for $C^2$ functions does not apply; an Itô–Tanaka (local time) argument for concave functions of $X$, with the reflection term killed by the Neumann condition, is needed, followed by a localisation that uses uniform integrability and the integrability condition in $\Lambda^\mu_0$. The lower bound needs the Azéma–Yor embedding and the law of $X^*_{\tau^*}$, neither of which is in Mathlib; the naive appeal to "the embedding exists" does not give the joint law of the stopped value and the maximum.

Formalization scope

The Lean development lives in the namespace LookbackMOT.HL and uses Mathlib's IsBrownianReal, IsStoppingTime, stoppedProcess, stoppedValue, Martingale, UniformIntegrable and HasLaw. Committed conventions:

• What is formalized. The goal is the reduced problem (3.7), not the superhedging problem (2.6): (2.6) needs stochastic integrals, which Mathlib does not have. The bridge between them (Proposition 2.1, the claim (3.4), Proposition 3.1) is outside this mission. The theorem's hypothesis $\sup_{\mathbb P\in\mathcal P_\infty}\mathbb E^{\mathbb P}[\xi^+]<\infty$ is stated through Proposition 3.1 with $\lambda=0$ as $\sup_{\tau\in\mathcal T_\infty}\mathbb E[g(X^*_\tau)]<\infty$. The horizon $T$ disappears: the stopping problem is over $\mathcal T_\infty$ with time in $[0,\infty)$.
• Standing hypotheses. The Brownian motion lives on an arbitrary filtered probability space with everywhere-continuous paths and $B_0=0$; the paper's canonical space is one instance. The mean condition and integrability of $\mu$ (p. 7) are assumed throughout. The spot $X_0$ is any real number. $\mu([0,\infty))=1$ is assumed only in (3.27).
• Added conditions. Every $\tau\in\mathcal T_\infty$ is a.s. finite (implied by uniform integrability). Every $\lambda\in\Lambda^\mu_0$ is measurable.
• Expectations of payoffs are $\mathbb E[\varphi^+]-\mathbb E[\varphi^-]$ in the extended reals, with $\infty-\infty=-\infty$; value functions are extended reals.
• Derivatives. $\lambda'$ is the right derivative and $\lambda''$ its Stieltjes measure. The weak ODE (3.21) is used both as a change of variables ($\lambda''$ is the image of $g'(m)/(m-\psi(m))\,dm$ under $\psi$) and on intervals ($\lambda'(\psi(y_2))-\lambda'(\psi(y_1))=\int_{y_1}^{y_2}g'(m)/(m-\psi(m))\,dm$), the two forms the paper's proofs use.
• The multiplier $\lambda^*$. It is written as $\lambda^*(x)=\int_{X_0<m<r^\mu}g'(m)(x-b^{-1}(m))^+/(m-b^{-1}(m))\,dm$, the change of variables $m=b(\xi)$ in (3.14) and the solution of (3.21) with $\psi=b^{-1}$ that the proof of Lemma 3.3 uses. It agrees with the $b(d\xi)$ formula when $b$ is continuous; at the jumps of $b$ (atoms of $\mu$) the Lebesgue–Stieltjes reading of (3.14) can fail to be $\mu$-integrable.
• Measures given by identities. $\mu^{HL}$ and $\lambda''$ enter as measures satisfying their defining identities on intervals; each exists and is unique.
• Printed slips not copied. (3.12) prints the numerator $c(y)$; the formalization uses $c(\xi)$. $b$, $\mu^{HL}$ and $\lambda^*$ are extended from $x\ge0$ to all of $\mathbb R$ by the same formulas.

No trivializing reading is available. Payoff expectations are never Bochner integrals (which would be $0$ for non-integrable payoffs). $\tau\equiv0$ lies in $\mathcal T_\infty$ and $\lambda\equiv0$ in $\Lambda^\mu_0$, so neither the supremum nor the infimum is over an empty set. The predicates for $\mu^{HL}$ and $\lambda''$ are satisfiable (witnessed for $\mu=\delta_{X_0}$ in a sorry-free check). $X_\tau$ is only evaluated where $\tau<\infty$ a.s. Every division has a positive denominator on the sets that carry mass.

Contributions welcome: the Azéma–Yor embedding and the law of the maximum; an Itô–Tanaka or local-time calculus sufficient for concave functions of Brownian motion and its maximum; the call-price identities of convex analysis; and the analysis of $\mu^{HL}$.

Selected references

• A. Galichon, P. Henry-Labordère, N. Touzi, A stochastic control approach to no-arbitrage bounds given marginals, with an application to lookback options, Ann. Appl. Probab. 24 (2014) 312–336. https://arxiv.org/abs/1401.3921 (v1, the version cited)
• D. Hobson, Robust hedging of the lookback option, Finance Stoch. 2 (1998) 329–347. https://doi.org/10.1007/s007800050046
• J. Azéma, M. Yor, Une solution simple au problème de Skorokhod, Séminaire de Probabilités XIII, LNM 721 (1979) 90–115. https://doi.org/10.1007/BFb0070852
• G. Peskir, Optimal stopping of the maximum process: the maximality principle, Ann. Probab. 26 (1998) 1614–1640. https://doi.org/10.1214/aop/1022855875
• L. Carraro, N. El Karoui, J. Obłój, On Azéma–Yor processes, their optimal properties and the Bachelier–drawdown equation, Ann. Probab. 40 (2012) 372–400. https://arxiv.org/abs/0902.1328

Motivation

The price of anarchy (POA) of a game measures how much selfish behaviour costs: it is the ratio between the largest cost of an equilibrium and the cost of an optimal outcome, for a nonnegative objective such as the sum of the players' costs. Since Koutsoupias and Papadimitriou (1999) and Roughgarden and Tardos (2002), POA bounds have been proved for routing, scheduling, facility location, auctions and many other models, mostly for pure Nash equilibria.

Pure Nash equilibria need not exist, are hard to compute in general, and are not what players running learning algorithms converge to. A bound that holds only at pure Nash equilibria therefore says little about realized play. Roughgarden's paper (J. ACM 62(5), 2015; conference version STOC 2009) observes that most known POA proofs follow one template, the smoothness argument, and proves that any bound obtained this way extends automatically to much broader equilibrium concepts. This mission formalizes the static half of that result: the extension to coarse correlated equilibria (Theorem 3.2) and to their approximate versions (Theorem 4.1).

Timeline:

• 1999: Koutsoupias and Papadimitriou introduce the worst-case ratio of equilibria to optimum.
• 2005: Awerbuch–Azar–Epstein and Christodoulou–Koutsoupias prove the bound 5/2 for linear congestion games; their arguments are smoothness arguments in hindsight.
• 2009: Roughgarden (STOC) isolates smoothness and proves the extension theorems; the journal version (2015) adds the tightness results for congestion games.
• 2009–2015: smoothness is adapted to auctions (Syrgkanis–Tardos 2013) and to local and approximate variants.

Setting

A cost-minimization game has finitely many players $i$. Player $i$ chooses a strategy $s_i$ from an arbitrary set $S_i$; an outcome is a vector $s = (s_i)_i$, and player $i$ pays a real cost $C_i(s)$. Write $(s_i', s_{-i})$ for the outcome in which player $i$ switches to $s_i'$ and the others stay put. The joint cost is $C(s) = \sum_i C_i(s)$, assumed nonnegative.

An outcome $s$ is a pure Nash equilibrium if $C_i(s) \le C_i(s_i', s_{-i})$ for every $i$ and $s_i' \in S_i$. For $\epsilon \ge 0$ it is an $\epsilon$-Nash equilibrium if $C_i(s) \le (1+\epsilon) C_i(s_i', s_{-i})$.

A coarse correlated equilibrium is a probability distribution $\sigma$ over outcomes with

$$\mathbf{E}_{s\sim\sigma}[C_i(s)] \le \mathbf{E}_{s\sim\sigma}[C_i(s_i', s_{-i})] \quad\text{for every } i \text{ and } s_i' \in S_i,$$

and an $\epsilon$-coarse correlated equilibrium satisfies the same with a factor $(1+\epsilon)$ on the right. Every pure Nash, mixed Nash and correlated equilibrium is a coarse correlated equilibrium, and coarse correlated equilibria are exactly the limits of play in which every player has vanishing external regret.

The game is $(\lambda,\mu)$-smooth if for every two outcomes $s, s^*$

$$\sum_i C_i(s_i^*, s_{-i}) \le \lambda\, C(s^*) + \mu\, C(s).$$

The robust price of anarchy is $\rho(G) = \inf\{\lambda/(1-\mu) : \mu < 1,\ G \text{ is } (\lambda,\mu)\text{-smooth}\}$.

Formalization targets

Goal: Theorem 3.2 (static extension theorem)

For every game $G$ with robust POA $\rho(G)$, every coarse correlated equilibrium $\sigma$ and every outcome $s^*$,

$$\mathbf{E}_{s\sim\sigma}[C(s)] \le \rho(G)\cdot C(s^*).$$

Milestones

1. Claim (3)–(5), p. 5: in a $(\lambda,\mu)$-smooth game with $\lambda > 0$, $\mu < 1$, every pure Nash equilibrium $s$ satisfies $C(s) \le \frac{\lambda}{1-\mu} C(s^*)$ for an optimal $s^*$.
2. §4.1, p. 16: every $\epsilon$-Nash equilibrium satisfies $C(s) \le \frac{(1+\epsilon)\lambda}{1-\mu(1+\epsilon)} C(s^*)$ for an optimal $s^*$.
3. The chain (16)–(21), p. 13: for one fixed pair $(\lambda,\mu)$ with $\mu < 1$, $\mathbf{E}_{s\sim\sigma}[C(s)] \le \frac{\lambda}{1-\mu} C(s^*)$ for every coarse correlated equilibrium $\sigma$ and every outcome $s^*$.
4. Theorem 4.1, p. 16: for every $\epsilon$-coarse correlated equilibrium,

$$\mathbf{E}_{s\sim\sigma}[C(s)] \le \frac{(1+\epsilon)\lambda}{1-\mu(1+\epsilon)}\cdot C(s^*).$$

Significance

Theorem 3.2 says that the robust POA of a game bounds the expected cost of every coarse correlated equilibrium, which contains every other equilibrium concept in the hierarchy. Combined with the companion result for no-regret sequences (Theorem 3.3, mission II of this series), it makes POA bounds meaningful for learning dynamics: whenever players use no-regret algorithms, their average cost is within the robust POA of optimal. For linear congestion games, which are $(5/3, 1/3)$-smooth, it yields the bound $5/2$ for all coarse correlated equilibria at once. Theorem 4.1 shows that the bounds degrade gracefully when the equilibrium condition holds only approximately, which covers equilibria computed to finite accuracy.

The results are proved in the paper; their proofs are short. No machine-checked version is known to exist. The mission's value is a reusable, platform-wide definition layer for cost-minimization games, smoothness, the robust POA and the equilibrium hierarchy, on which later results can be stated: the bicriteria bounds of §4.2, the tightness theorem for congestion games (mission III), and smoothness bounds for specific models such as auctions, routing and scheduling.

Difficulty

The mathematics is linear: it uses only linearity of expectation and one rearrangement. The difficulty lies in the encoding. The robust POA is an infimum over a set that may be empty (then $\rho(G) = +\infty$ on the page) and need not be attained. Passing from the fixed-pair bound to the infimum uses $C(s^*) \ge 0$. Theorem 4.1's printed side condition $\epsilon < 1/\mu - 1$ is meaningless when $\mu = 0$ and reverses its meaning when $\mu < 0$. Each of these must be handled so that the formal statement is neither false nor vacuous.

Formalization scope

Players form a finite type with decidable equality, and strategy sets are arbitrary types with no finiteness assumed. Outcomes are dependent functions, and the deviation $(s_i', s_{-i})$ is Function.update s i s'ᵢ. Costs are real-valued, and $\lambda, \mu$ are unconstrained reals except $\mu < 1$. Probability distributions are finitely supported weight functions that are nonnegative with total mass $1$. Expectations are therefore finite sums with no integrability side conditions. This covers all finite games and all mixed and correlated equilibria of finite games, but not distributions with infinite support.

The robust POA is an extended-real (EReal) infimum over the smoothness pairs with $\mu < 1$, so it is $+\infty$ when no such pair exists, and the goal compares the expected cost with $\rho(G)\cdot C(s^*)$ in EReal. The goal carries two explicit hypotheses:

• the joint cost is nonnegative, which is the paper's standing assumption (§1, p. 2; §2.4, p. 10);
• some smoothness pair with $\mu < 1$ exists, so that $\rho(G) < +\infty$.

Without the second, a game with no smoothness pair and $C(s^*) = 0$ would be claimed to have expected cost at most $0$ (EReal sets $(+\infty)\cdot 0 = 0$), which the page does not assert. A formalization in which the distribution may have total mass $0$, or in which $\rho(G)$ is an infimum over all pairs rather than over the smoothness pairs with $\mu < 1$, trivializes or falsifies the goal, and is ruled out by the definitions.

In Theorem 4.1 and the $\epsilon$-Nash bound:

• "$\epsilon < 1/\mu - 1$" is encoded as $\mu(1+\epsilon) < 1$, which agrees with it for $0 < \mu < 1$;
• $\epsilon \ge 0$ is assumed, the implicit domain of an approximation parameter.

The $\epsilon$-coarse correlated equilibrium is the extension of (15) that the paper says is "defined in the same way" as $\epsilon$-Nash equilibria (p. 15). Remark 4.4 writes out the payoff analogue.

Claim (3)–(5) and the $\epsilon$-Nash bound keep the paper's hypotheses $\lambda > 0$ and optimality of $s^*$, although the inequalities hold without them. Example 4.2 is not posed: its printed bound $(5-5\epsilon)/(2-\epsilon)$ should read $(5+5\epsilon)/(2-\epsilon)$.

Contributions welcome:

• proofs of the four milestones and of the goal;
• a measure-theoretic version for distributions with infinite support, with explicit integrability hypotheses;
• reuse of the definitions in other smoothness results.

Selected references

• T. Roughgarden, Intrinsic Robustness of the Price of Anarchy, J. ACM 62(5), Article 32, 2015. https://doi.org/10.1145/2806883
• T. Roughgarden, Intrinsic Robustness of the Price of Anarchy, Proc. 41st ACM STOC, 513–522, 2009. https://doi.org/10.1145/1536414.1536485
• E. Koutsoupias, C. Papadimitriou, Worst-Case Equilibria, Proc. STACS, LNCS 1563, 404–413, 1999. https://doi.org/10.1007/3-540-49116-3_38
• G. Christodoulou, E. Koutsoupias, The Price of Anarchy of Finite Congestion Games, Proc. 37th ACM STOC, 67–73, 2005. https://doi.org/10.1145/1060590.1060600
• B. Awerbuch, Y. Azar, A. Epstein, The Price of Routing Unsplittable Flow, Proc. 37th ACM STOC, 57–66, 2005. https://doi.org/10.1145/1060590.1060599
• V. Syrgkanis, É. Tardos, Composable and Efficient Mechanisms, Proc. 45th ACM STOC, 211–220, 2013. https://doi.org/10.1145/2488608.2488635