Operations Research

Motivation

Retailers accept large volumes of returned merchandise, and a common default is the full refund: a buyer who is unhappy with a product brings it back and gets the whole price back. Many consumers only learn how much they value a product after they have it at home — clothes that do not fit, a gadget that does not suit the buyer's needs. A returns policy therefore plays two roles at once. It raises the buyer's willingness to pay before purchase, and after purchase it decides which units stay with consumers and which go back to the seller to be salvaged.

Xuanming Su's paper Consumer Returns Policies and Supply Chain Performance (SSRN 1020451; published in Manufacturing & Service Operations Management 11(4), 2009, doi:10.1287/msom.1080.0240) puts this effect into a newsvendor model with random demand. The earlier literature it builds on, notably Che (1996) and Davis, Gerstner and Hagerty (1995), asked whether a seller should offer full refunds or no returns at all. Su's model makes the refund amount a separate decision variable. The answer it gives is closed-form and sharp: the optimal refund equals the salvage value. This mission formalizes Sections 3–4 of the paper: the single-seller model, the full-refund benchmark, and the optimal partial refund.

Setting

A seller stocks a quantity $q \ge 0$ before a selling season at unit cost $c$. Unsold and returned units are salvaged at value $s$. Market demand is a nonnegative random variable $X$ with law $D$, distribution function $F$ and $\bar F = 1 - F$. Each consumer who buys learns a valuation $V$ after purchase. Valuations are i.i.d. with law $\nu$ and finite mean $\mu = EV$, and the standing assumption is $\mu > c > s \ge 0$.

The seller chooses a price $p$, a quantity $q$ and a refund $r$. Once a consumer has bought, they keep the product if $V \ge r$ and return it otherwise. The keep and return probabilities are

Before purchase a consumer's expected utility from buying is $E\max(V, r)$, so this is the reservation price. Every consumer buys if $p \le E\max(V, r)$ and nobody buys otherwise (the demand rule (6)). With $E\min(X, q)$ the expected sales of a stock $q$, the seller's expected profit (7)–(8) is

and $-(c-s)q$ otherwise. Two special cases serve as benchmarks. Under full refunds ($r = p$) every consumer buys and the profit is $\Pi_{\text{full}}(p,q) = (p-s)\bar G(p)E\min(X,q) - (c-s)q$, from (1)–(2). Under no returns the price is $\mu$ and the profit is $\Pi_{\text{no}}(q) = (\mu - s)E\min(X,q) - (c-s)q$, from (3). Social welfare (12)–(13) is the sum of consumer surplus and seller profit, $SW(p,q,r) = \int_{[r,\infty)}(v-s)\,d\nu(v)\cdot E\min(X,q) - (c-s)q$, again subject to the demand rule.

Formalization targets

Goal: Proposition 2 (p. 11)

With $p^* = E\max(V,s)$, $r^* = s$ and any $q^*$ satisfying

the triple $(p^*, q^*, r^*)$ maximizes $\Pi$ over all prices, all refunds and all quantities $q \ge 0$:

Milestones

1. The reservation price splits as $E\max(V,r) = rG(r) + \int_{[r,\infty)} v\,d\nu$, which is the step (28)→(29) of the proof (p. 26).
2. At $p = E\max(V,r)$ the per-unit margin $(p-s)\bar G(r) + (p-r)G(r)$ equals $\int_{[r,\infty)}(v-s)\,d\nu$, displays (27)–(30), p. 26.
3. This integral is maximized at $r = s$ (p. 26).
4. Hence $(E\max(V,s), s)$ maximizes the margin subject to $p \le E\max(V,r)$, the first step of the proof (p. 26).
5. The newsvendor critical fractile, a reference to a proved platform theorem (p. 26).
6. Proposition 1(i) (p. 9): under full refunds, $p^* \in \arg\max_p (p-s)\bar G(p)$ with $\bar F(q^*) = (c-s)/((p^*-s)\bar G(p^*))$ is optimal.
7. Proposition 1(ii) at $s = 0$ (p. 26): with nonnegative valuations, no returns beats every full-refund policy.
8. Corollary 1 (p. 12): the inequality $(p-s)\bar G(p) \le E\max(V,s) - s$ (p. 26), and its consequence that partial refunds earn at least the full-refund profit and, for strictly increasing $F$, stock at least as much.
9. Corollary 2 (p. 13): the triple of Proposition 2 also maximizes social welfare.

Significance

The result separates two things that a full refund ties together: the price and the refund. Setting $r = s$ sends every unit back to its more valuable use. Consumers who value the product above its salvage value keep it, and the rest return it to be salvaged. The price $E\max(V,s)$ then extracts the whole expected surplus. Consequences follow directly. Partial refunds dominate both full refunds and no returns (Corollary 1). They raise the stocking quantity, which benefits an upstream manufacturer paid per unit ordered. With valuation uncertainty resolved only after purchase, the monopoly outcome is welfare-maximizing (Corollary 2). Section 5 of the paper, formalized in the companion mission, uses Proposition 2's triple as the first-best target that supply chain contracts must implement.

The results are proved on paper with short arguments in Appendix A of the paper. None of them has a machine-checked proof. The mission's contribution is a formal model of consumer returns with the demand rule built in, plus checked versions of Propositions 1–2 and Corollaries 1–2 for general valuation laws (with atoms), not only densities.

Difficulty

The paper's proof treats the problem as separable: first maximize the margin over $(p, r)$, then solve a newsvendor problem in $q$. Two steps that are routine on paper need care. First, the margin bound must hold over the whole constrained region $p \le E\max(V, r)$, including refunds above the price and negative prices. It rests on comparing $\int_{[r,\infty)}(v-s)\,d\nu$ with $\int_{[s,\infty)}(v-s)\,d\nu$, which needs the closed half-line convention to hold up at atoms of $\nu$. Second, the newsvendor step must be done for a demand law that may have atoms, where $\bar F$ has no inverse. Without the demand rule the problem is not separable at all: formula (8) alone is unbounded in $p$. Without nonnegativity of demand and quantity it is unbounded in the other direction.

Formalization scope

Lean represents all prices, refunds, costs, quantities and profits as real numbers. The valuation law is a probability measure ν on ℝ with integrable identity, so a density is not required. The demand law is a probability measure D on ℝ with D (Set.Iio 0) = 0. $\bar G(r)$ is (ν (Set.Ici r)).toReal and $G(r)$ is (ν (Set.Iio r)).toReal, following the page's tie rule (keep iff $V \ge r$). $E\min(X,q)$ is SupplyChainTheory.expSales D q from the published module SupplyChainTheory_contracts, and $\bar F$ is 1 - ProbabilityTheory.cdf D. Printed page numbers equal PDF page numbers throughout the source.

Committed conventions and readings:

• Demand rule inside the objectives. Profit and welfare are zero-demand cash flows when $p > E\max(V,r)$.
• Nonnegativity. Stocking quantities range over $q \ge 0$ and demand is nonnegative. Both are the page's words ("stocking quantity", "a mass of infinitesimal consumers"), and without them the profit is unbounded.
• Salvage value. $0 \le s$, as on p. 26.
• Optimality, not uniqueness. Every optimum is stated as optimality of the page's closed-form triple. Uniqueness fails when $\nu$ has gaps: if $\nu$ puts no mass on $[s, r)$, the refund $r$ is optimal too.
• No continuity of $F$ for the goal. The goal assumes no continuity of $F$. Existence of $q^*$ is not claimed.
• Corollary 1, quantity part. The quantity comparison assumes $F$ strictly increasing on $[0,\infty)$, which the proof's $\bar F^{-1}$ presumes. Without it the statement is false.
• Proposition 1(ii) at $s = 0$. This case assumes nonnegative valuations. The "sufficiently low" form of Proposition 1(ii) is not formalized.

A trivializing formalization is ruled out: $p^*$ and $r^*$ are the explicit values $E\max(V,s)$ and $s$, not an argmax chosen by Classical.choose. The maximization ranges over all $(p, r)$ and all $q \ge 0$, not a set restricted to $r = s$. The returned-units cash flow $(p - r + s)G(r)$ appears in the profit.

The newsvendor step reuses the proved platform theorem SupplyChainTheory.chain_optimal_fractile. The other pieces needed are elementary lemmas on integrals over half-lines and the concavity of $q \mapsto E\min(X,q)$. They are reusable for any newsvendor-type model. Proofs of any milestone, and a general-law newsvendor optimality lemma that does not need a continuous $F$, are welcome.

Selected references

• X. Su, Consumer Returns Policies and Supply Chain Performance, SSRN working paper 1020451, version of August 2008. https://ssrn.com/abstract=1020451 — published in Manufacturing & Service Operations Management 11(4), 2009. https://doi.org/10.1287/msom.1080.0240
• Y.-K. Che, Customer Return Policies for Experience Goods, Journal of Industrial Economics 44(1), 1996. https://doi.org/10.2307/2950560
• S. Davis, E. Gerstner, M. Hagerty, Money Back Guarantees in Retailing: Matching Products to Consumer Tastes, Journal of Retailing 71(1), 1995. https://doi.org/10.1016/0022-4359(95)90010-1

Motivation

Prediction with expert advice asks a learner to predict a binary label on each of a sequence of trials, after seeing the predictions of a pool of candidate functions, and to make few more mistakes than the best member of the pool. Littlestone and Warmuth's The Weighted Majority Algorithm (Inform. and Comput. 108, 1994) gave the deterministic algorithm WM and its randomized variant WMR, and proved worst-case bounds that hold for every sequence of trials, with no probabilistic assumption on the data. Their §8 asks how good such bounds can possibly be when the data contain anomalies: disagreements with a candidate function, counted relative to the best-fitting member of the pool. Such disagreements can arise from noise in the instances or labels, or from instances that do not determine the label.

For the randomized algorithm WMR the expected number of mistakes grows, by Corollary 6.1 of the paper, at rate $\ln(1/\beta)/(1-\beta)$ per anomaly, which tends to $1$ as $\beta \to 1$. Theorem 8.2 shows that no randomized learner, however it is built, can do better than rate $1$: an adversary who fixes the sequence in advance can force half the noise-free optimum plus one expected mistake per anomaly. Together with the deterministic counterpart, Theorem 8.1 (rate $2$), it locates the cost of label noise in online learning exactly. Mistake-bound lower bounds of this kind are a standard reference point for the analysis of online classification and of the expert-advice algorithms descended from WM (Cesa-Bianchi and Lugosi, Prediction, Learning, and Games, 2006).

Timeline: Littlestone (1988) characterized the optimal noise-free mistake bound $\mathrm{opt}(F,0)$ by complete mistake trees (the Littlestone dimension); Littlestone and Warmuth (FOCS 1989; journal version 1994) introduced WM and WMR and proved Theorems 8.1 and 8.2.

Setting

Let $X$ be an arbitrary domain and $F$ a pool of functions $X \to \{0,1\}$, finite or infinite. A trial is a pair $(x,y)$ with $x\in X$ and $y\in\{0,1\}$; a sequence of trials is a finite list $\mathcal S = ((x_1,y_1),\dots,(x_T,y_T))$, in which an instance may repeat with different labels. The number of anomalies of $\mathcal S$ with respect to $f$ is $\#\{t : f(x_t)\ne y_t\}$, and $S_\eta$ is the collection of sequences for which some $f\in F$ has at most $\eta$ anomalies.

A deterministic algorithm maps the past trials and the current instance to a predicted label; $M_A(\mathcal S)$ counts its wrong predictions, and

A randomized algorithm uses random choices independent of the sequence. On a fixed sequence its behaviour at trial $t$ is summarized by $p_t\in[0,1]$, the probability that it predicts $1$ given the preceding instances and labels and the current instance; its expected number of mistakes is $\sum_t |p_t - y_t|$, and

the infimum ranging over all maps $A$ from (past trials, current instance) to $p_t \in [0,1]$.

Formalization targets

Goal: Theorem 8.2 (p. 252)

For every pool $F$ with $|F|>1$ and every integer $\eta\ge 0$,

Both sides live in $[0,\infty]$; when $\mathrm{opt}(F,0)=\infty$ the statement says $\mathrm{opt}_{\mathrm{RAND}}(F,\eta)=\infty$.

Milestone: complete mistake trees (§8, p. 251)

"For any pool of functions $F$ there exists a complete $\mathrm{opt}(F,0)$-mistake tree" ([Lit88]). On the platform this is the proved Lemma 21.7 of Shalev-Shwartz and Ben-David, $M_{\mathrm{SOA}}(F)\le \mathrm{Ldim}(F)$, together with Lemma 21.6, $\mathrm{Ldim}(F) \le M_A(F)$ for every $A$; a tree shattered by $F$ is a complete mistake tree.

Significance

The theorem shows that the expected-mistake bound of WMR is optimal in its dependence on the number of anomalies: its coefficient of $\eta$ approaches $1$, and no randomized learner achieves a smaller one on every pool with two or more functions. It also quantifies the advantage of randomization: the deterministic rate is $2$ (Theorem 8.1), the randomized rate is $1$, and the noise-free term halves. The lower bound is obliviously adversarial, since the sequence is chosen before any coin is tossed, so it applies equally to the stronger model in which the adversary adapts to the learner's predictions.

The result has been proved since 1994. To our knowledge it has no machine-checked proof; the platform holds the Littlestone-dimension characterization of the noise-free optimum (Shalev-Shwartz and Ben-David, Chapter 21) but no statement about anomalies or randomized lower bounds. This mission formalizes the definitions of anomalies, $\mathrm{opt}(F,\eta)$ and $\mathrm{opt}_{\mathrm{RAND}}(F,\eta)$, and the theorem.

Difficulty

An adversary against a randomized learner cannot react to its predictions: the whole sequence, instances and labels, must be fixed in advance, so the adaptive adversary that proves the deterministic bound is not directly available. The lower bound must instead come from the learner's prediction probabilities, which depend only on the sequence prefix; the content of the theorem is that this information is enough to construct, for every learner, one fixed sequence that stays inside $S_\eta$ while forcing the stated expected count. Taking the infimum over learners inside an extended-real supremum over sequences of every length adds bookkeeping when $\mathrm{opt}(F,0)$ is infinite.

Formalization scope

Sequences are Fin T → X × Bool for every T : ℕ. Deterministic algorithms, the mistake count, shattered trees and the Littlestone dimension are reused from the published definition UnderstandingML_Online (OnlineAlg, mistakes, ShattersTree, ldim, soa); randomized algorithms are its OnlineAlgR X := List (X × Bool) → X → ℝ restricted by IsRandAlg to values in $[0,1]$, and the expected mistake count is its cumLoss. $\eta$ is a natural number. $\mathrm{opt}(F,\eta)$ takes values in ℕ∞ and $\mathrm{opt}_{\mathrm{RAND}}(F,\eta)$ in ℝ≥0∞; the paper's "minimum" is read as an infimum. $|F|>1$ is F.Nontrivial, which admits infinite pools.

The reduction of randomized algorithms to probability maps is the main modelling choice: on a fixed sequence the expected number of mistakes of any algorithm whose randomization is independent of the sequence equals $\sum_t|p_t-y_t|$, and every map with values in $[0,1]$ is realized by such an algorithm, so the two infima coincide. Dropping the constraint $p_t\in[0,1]$, or quantifying only over deterministic algorithms, gives a different quantity and is ruled out.

Needed: the definitions above, and the existence of a complete $\mathrm{opt}(F,0)$-mistake tree, available through the proved platform theorems on ldim and soa. Lemmas relating mistakes along a path of a shattered tree to ldim, and a reusable statement that an oblivious adversary can force expected loss $\tfrac12$ per trial, would serve other lower bounds in the Littlestone–Warmuth series and in online learning generally. Contributions of such lemmas are welcome.

Selected references

• N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2):212–261, 1994. https://doi.org/10.1006/inco.1994.1009
• N. Littlestone, Learning Quickly When Irrelevant Attributes Abound: A New Linear-Threshold Algorithm, Machine Learning 2:285–318, 1988. https://doi.org/10.1007/BF00116827
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 21. https://doi.org/10.1017/CBO9781107298019
• N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921

Motivation

Monotone comparative statics asks when the optimal choice of an agent moves in a predictable direction as a parameter of the problem changes: does a firm hire more of every input when the output price rises, does a monopolist raise its price when its marginal cost rises? Topkis (1978) gave a cardinal answer: if the objective $f(x,t)$ is supermodular in the choice $x$ and has increasing differences in $(x,t)$, the set of maximizers is nondecreasing in $t$. Milgrom and Shannon (1994) replaced these conditions by ordinal ones, quasisupermodularity and the single crossing property, and showed in their Monotonicity Theorem that the ordinal conditions are both necessary and sufficient for the argmax to be monotone in the parameter and the constraint set.

Supermodularity is therefore never necessary for monotone comparative statics. Theorem 10 of Milgrom and Shannon identifies a setting where it is: when the objective must keep the ordinal properties after adding an arbitrary linear price term $p\cdot x$ (or subtracting an arbitrary nonnegative cost $w\cdot x$), the only objectives that qualify are the supermodular ones. This is the situation of a price-taking firm whose revenue or cost is linear in its activity levels, and the result explains why supermodularity is the natural assumption in such models even though the ordinal theory does not require it.

Setting

Let $X$ be a lattice: a partially ordered set in which every two elements $x, y$ have a least upper bound $x \vee y$ (join) and a greatest lower bound $x \wedge y$ (meet). On $\mathbb{R}^n$ the order is componentwise, so $x \vee y$ and $x \wedge y$ are the componentwise maximum and minimum; on a product $\mathbb{R}^n \times \mathbb{R}$ the order is the product order. For $p, x \in \mathbb{R}^n$, $p \cdot x = \sum_i p_i x_i$.

A function $g : X \to \mathbb{R}$ is supermodular if $g(x) + g(y) \le g(x \vee y) + g(x \wedge y)$ for all $x, y \in X$. It is quasisupermodular if, for all $x, y \in X$, (i) $g(x) \ge g(x \wedge y)$ implies $g(x \vee y) \ge g(y)$, and (ii) $g(x) > g(x \wedge y)$ implies $g(x \vee y) > g(y)$.

Let $T$ be a partially ordered set and $f : X \times T \to \mathbb{R}$. The function $f$ has increasing differences in $(x, t)$ if for $x' \ge x''$ the difference $f(x', t) - f(x'', t)$ is nondecreasing in $t$. It has the single crossing property in $(x; t)$ if for all $x' > x''$ and $t' > t''$, $f(x', t'') > f(x'', t'')$ implies $f(x', t') > f(x'', t')$, and $f(x', t'') \ge f(x'', t'')$ implies $f(x', t') \ge f(x'', t')$. The function $f$ is quasisupermodular in $x$ if $f(\cdot, t)$ is quasisupermodular for every $t$, and nondecreasing in $x$ if $f(\cdot, t)$ is nondecreasing for every $t$.

In the Lean development the domain $\mathbb{R}^n$ is Fin n → ℝ, $f$ is curried as f : (Fin n → ℝ) → ℝ → ℝ, $p \cdot x$ is p ⬝ᵥ x, and supermodularity and increasing differences are the published Supermodularity.Monotonicity.SupermodularOn and IncreasingDifferencesOn with the domain Set.univ.

Formalization targets

Goal: Theorem 10 (p. 166)

Let $f : \mathbb{R}^n \times \mathbb{R} \to \mathbb{R}$. Then

and, if $f$ is nondecreasing in $x$,

Here "$f$ is supermodular" means supermodular on the lattice $\mathbb{R}^n \times \mathbb{R}$, jointly in $(x,t)$.

Milestones

1. Every supermodular function on a lattice is quasisupermodular (p. 164, remark after Theorem 5).
2. Every function with increasing differences in $(x, t)$ has the single crossing property in $(x; t)$ (same remark).
3. If $g + p\cdot x$ is quasisupermodular on $\mathbb{R}^n$ for every $p \in \mathbb{R}^n$, then $g$ is supermodular (the converse step of the proof of Theorem 10).
4. The first sentence of Theorem 10 on its own.

Significance

The result. The Monotonicity Theorem shows that the ordinal conditions are exactly what monotone comparative statics needs for a single objective. Theorem 10 shows that the cardinal conditions are exactly what is needed for a family of objectives closed under linear prices. It separates two questions that are often conflated: whether a particular optimization problem has monotone solutions (ordinal), and whether a model's monotonicity conclusion is robust to the prices or costs the modeller adds to it (cardinal). The second sentence specializes to the economically common case of nonnegative input costs, where the restriction to $w \ge 0$ is offset by the monotonicity of $f$.

Formalizing it. The result is proved in the paper, with the converse direction given in detail only for the step "supermodular in $x$" and the remaining cases left as "similar arguments". The mission produces machine-checked proofs of both equivalences, including the cases the paper does not write out: the recovery of increasing differences from the single crossing property under all price perturbations, and the recovery under the sign restriction $w \ge 0$. No part of Milgrom and Shannon's paper was found formalized on the platform when this mission was drafted; Topkis's supermodularity theory is partly available on the platform as the Supermodularity.* series.

Difficulty

The forward direction is a chain of short implications. The content is in the converse: from purely ordinal information about many functions one must recover a cardinal inequality. The single crossing property and quasisupermodularity only compare values of one function at two points, so a single perturbation can never yield an inequality between sums of four values; the argument must choose, for each violating configuration, a price vector that makes two of the four values tie, and the choice must be compatible with the sign constraint $w \ge 0$ in the second statement. That compatibility is where the hypothesis that $f$ is nondecreasing in $x$ enters, and without it the second equivalence fails. A second subtlety is the decomposition of joint supermodularity on $\mathbb{R}^n \times \mathbb{R}$ into supermodularity in $x$ and increasing differences in $(x,t)$, which the paper uses without statement; the platform does not yet have it.

Formalization scope

• $\mathbb{R}^n$ is Fin n → ℝ with Mathlib's pointwise order and lattice operations; $n \ge 0$ is arbitrary. The product $\mathbb{R}^n \times \mathbb{R}$ carries Mathlib's product order.
• $f : \mathbb{R}^n \times \mathbb{R} \to \mathbb{R}$ is curried. "$f$ is supermodular" is read as joint supermodularity on $\mathbb{R}^n \times \mathbb{R}$, as the paper's proof confirms ("If $f$ is supermodular in $(x, t)$ …"); with supermodularity in $x$ only, the "if" direction would be false.
• Quasisupermodularity and the single crossing property are the paper's definitions verbatim: strict comparisons $x' > x''$, $t' > t''$ in the single crossing property, both the weak and the strict implication in both notions, and quantification over all ordered pairs. The paper's single crossing property is stated for a lattice $X$; the Lean definition only uses the order.
• The quantifier over $p$ (and over $w \ge 0$) is universal and covers both properties at once. The second equivalence keeps $- w\cdot x$ with $w \ge 0$ componentwise and has "nondecreasing in $x$" as its hypothesis only.
• Trivializing formalizations are ruled out: an existential quantifier over $p$, supermodularity in $x$ only on the right-hand side, merging the two sentences with $p = -w$, or dropping the monotonicity hypothesis would each state a different, false or weaker theorem.
• The definitions QuasiSupermodularOn and SingleCrossing are shared with the two sibling missions on Milgrom and Shannon's Theorems 4 and 8 and will be merged with them. A lemma decomposing supermodularity on a product lattice into supermodularity in each factor and increasing differences would be reusable well beyond this mission; contributions of such general lattice lemmas are welcome.

Selected references

• P. Milgrom and C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479
• D. M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 305–321, 1978. https://doi.org/10.1287/opre.26.2.305
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

Motivation

When many users share a network and each routes its own traffic selfishly, the outcome is a Nash equilibrium rather than a centrally optimized assignment. Koutsoupias and Papadimitriou, in Worst-case equilibria (STACS 1999; journal version 2009), proposed to measure the loss caused by this lack of coordination by the worst-case ratio between the social cost of an equilibrium and the social optimum. The ratio, first called the coordination ratio and now the price of anarchy, became a central quantity of algorithmic game theory, studied for routing, scheduling, congestion games, auctions and network design.

The paper analyses the simplest setting in which the question is nontrivial: agents sending traffic over parallel links, which is the same as scheduling independent jobs on parallel machines with the jobs choosing their machines. For two identical links it determines the price of anarchy exactly.

Timeline.

• 1999: Koutsoupias and Papadimitriou introduce the model and the measure; on two identical links the price of anarchy is $3/2$, and on $m$ identical links it is $\Omega(\log m/\log\log m)$, with a nonmatching upper bound in the conference version.
• 2002: Czumaj and Vöcking, and independently Koutsoupias, Mavronicolas and Spirakis, show that this lower bound is tight for $m$ identical links, $\Theta(\log m/\log\log m)$; Czumaj and Vöcking also give tight bounds for links of different speeds.

Setting

There are $n$ agents and $m$ identical parallel links. Agent $i$ has an amount of traffic $w_i>0$ to send over one link. A pure profile $s=(j_1,\dots,j_n)\in\{1,\dots,m\}^n$ assigns a link to each agent; the load of link $j$ is $\ell_j(s)=\sum_{k:\,j_k=j}w_k$, and the cost of agent $i$ is $\ell_{j_i}(s)$, the traffic on its own link.

A mixed strategy of agent $i$ is a probability distribution $(p_i^1,\dots,p_i^m)$ on the links; the agents randomize independently, so $s$ occurs with probability $\prod_i p_i^{j_i}$. The cost to agent $i$ of a mixed profile $p$ is its expected cost $c_i$. The profile $p$ is a Nash equilibrium if no agent can lower its expected cost by changing its own distribution while the others keep theirs.

The expected traffic on link $j$ is $M^j=\sum_i p_i^jw_i$, and the cost of agent $i$ when its traffic is assigned to link $j$ is $c_i^j=w_i+\sum_{k\ne i}p_k^jw_k=M^j+(1-p_i^j)w_i$.

The social cost of $p$ is the expected maximum load,

and the social optimum $\mathrm{opt}$ is the least maximum load over all pure assignments, the optimum of the $m$-way partition problem for $w_1,\dots,w_n$.

The proof of the main theorem uses two further quantities: the contribution probability $q_i$, the probability that agent $i$ is on the (lexicographically first) link of maximum load, and the collision probability $t_{ik}=\sum_jp_i^jp_k^j$ of agents $i$ and $k$.

Formalization targets

Goal: Theorem 3

For any number $n$ of agents with positive traffics and $m=2$ identical links, every Nash equilibrium $p$ satisfies

Milestones

In the order the proof of Theorem 3 uses them:

1. Equation (2): $c_i^j=w_i+\sum_{k\ne i}p_k^jw_k=M^j+(1-p_i^j)w_i$ for every mixed profile.
2. The support property: at an equilibrium agent $i$ uses only links minimizing $c_i^j$, and $c_i=\min_jc_i^j$.
3. The lower bounds $\mathrm{opt}\ge\max\{w_i,\ \sum_kw_k/m\}$.
4. Theorem 2 with (6): at every equilibrium on $m$ identical links,

5. $\mathrm{cost}=\sum_iq_iw_i$.
6. Inequality (7): $q_i+q_k\le1+t_{ik}$ for distinct agents $i,k$.
7. $c_i=w_i+\sum_{k\ne i}t_{ik}w_k$.
8. On two links, at every equilibrium, $\sum_{k\ne i}q_kw_k\le\big(\tfrac32-q_i\big)\sum_{k\ne i}w_k$.

Companion items

The second sentence of Theorem 1 (on two links some equilibrium has $\mathrm{cost}=\tfrac32\,\mathrm{opt}>0$), which shows the goal is tight, and the fact from its proof that the uniform profile $p_i^j=1/m$ of $m$ unit agents on $m$ links is an equilibrium.

Significance

Theorem 3 and the instance of Theorem 1 show that on two identical links selfish randomized routing never costs more than $50\%$ above the optimum, whatever the number of agents and their traffics, and that this factor is attained. Theorem 2 gives a per-agent guarantee for any number of links: the expected cost an individual agent experiences at any equilibrium is within $2-1/m$ of the optimum, the same factor as Graham's list-scheduling bound. Together they separate the individual and the social view: individual costs stay within a constant, while the expected maximum load, the social cost, can be a factor $\Omega(\log m/\log\log m)$ above the optimum.

The results are proved in the paper. As far as is known they have not been machine-checked. Formalizing them produces a verified model of mixed equilibria in load balancing games, with the social cost as an expected maximum over the product distribution, which is the starting point of the later literature on links with speeds, on general congestion games and on smoothness arguments. The intermediate identities (the contribution and collision probabilities) are reusable for any expected-maximum bound over independent random assignments.

Difficulty

The social cost is an expectation of a maximum over $m^n$ outcomes, and the equilibrium probabilities are given only implicitly, as the solution of a linear system determined by the agents' supports. The natural first idea, to bound the expected maximum load by the maximum expected load $\max_jM^j$, fails: the expected maximum can be much larger, and bounding it is exactly what makes the problem hard (for $m$ links it grows like the maximum occupancy of $m$ balls in $m$ bins). Computing the equilibrium probabilities explicitly does not help either; the paper gives them for two links and notes it does not see how to use them to bound the social cost. The argument has to relate the per-agent expected costs, which the equilibrium condition controls, to the expected maximum, which it does not control directly.

Formalization scope

Agents are Fin n and links Fin m (the goal uses Fin 2); the paper's agent $i$ and link $j$ are indices $i-1$, $j-1$. A mixed profile is p : Fin n → Fin m → ℝ with p i j $=p_i^j$. The game is built on the published definitions agt_games (AGT.IsMixedNash, AGT.expectedPayoff, AGT.profileProb). That vocabulary maximizes payoffs, so the payoff of an agent is minus the load of its link, and the expected cost is minus the expected payoff. The equilibrium is the full mixed Nash condition, including that each $p_i$ is a probability distribution; the support description is a milestone, not the definition. The social cost is the expected maximum load over the product distribution, never the maximum expected load. $\mathrm{opt}$ is a minimum over pure assignments, with the number of links an explicit argument. The lexicographically first maximum link is the lowest-indexed link of maximum load.

Traffics are positive, as in the paper's model; some milestones need only nonnegative traffics or no sign condition, and say so. Statements over $m$ links assume $m\ge1$. Price-of-anarchy statements are inequalities $\mathrm{cost}\le c\cdot\mathrm{opt}$ for every equilibrium, never a quotient $\mathrm{cost}/\mathrm{opt}$, whose value at $\mathrm{opt}=0$ would be a junk $0$. A formalization in which the social cost is $\max_jM^j$, or in which the equilibrium is only a support condition without the requirement that the $p_i$ be distributions, would trivialize or falsify the goal and is ruled out by these definitions.

A complete development needs finite sums over the $m^n$ pure profiles, marginalization of product distributions, and the case analysis of the final step. The marginalization lemmas (summing out the other agents, collision probabilities of independent choices) are reusable beyond this mission. Proofs of the milestones, alternative arguments for Theorem 3, and a proof of Theorem 2 for its own sake are all welcome.

Page numbers are those of the PDF file of the journal version; it prints a page number only on its first page.

Selected references

• E. Koutsoupias and C. Papadimitriou, Worst-case equilibria, STACS 1999, LNCS 1563, pp. 404–413. https://doi.org/10.1007/3-540-49116-3_38 (this mission cites the authors' journal version of 2009, Computer Science Review 3(2), 65–69, https://doi.org/10.1016/j.cosrev.2009.04.003)
• A. Czumaj and B. Vöcking, Tight bounds for worst-case equilibria, SODA 2002, pp. 413–420; ACM Transactions on Algorithms 3(1), 2007. https://doi.org/10.1145/1186810.1186814
• E. Koutsoupias, M. Mavronicolas and P. Spirakis, Approximate equilibria and ball fusion, Theory of Computing Systems 36, 683–693, 2003. https://doi.org/10.1007/s00224-003-1131-5
• R. L. Graham, Bounds on multiprocessing timing anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. https://doi.org/10.1137/0117039

Motivation

A controller of a finite Markov chain often cares about more than one long-run quantity: an inventory manager wants a high average profit while keeping the long-run fraction of stock-outs below a target; a communication network maximizes throughput subject to bounds on average delay or power. Such problems are constrained Markov decision problems: maximize one average reward while other averages, all linear in the long-run frequencies of state-action pairs, are kept below given bounds. Unlike unconstrained problems, they need not have a pure stationary optimal policy, and in general not even a stationary one.

Derman (Finite State Markovian Decision Processes, 1970, Ch. 7) treated the case in which every stationary policy induces a chain with one ergodic class, and solved it by linear programming. Derman and Veinott (1972) proposed a decomposition algorithm for the general multichain case, remarking that until the faces of the relevant polytope are known, routine use of the simplex method is not possible. Section 4.7 of Kallenberg's 1983 monograph (CWI repository) describes that polytope explicitly for the multichain case and derives from one linear program an optimal Markov policy, with conditions under which a stationary optimal policy can be read off. Kallenberg notes that Veinott knew the characterization of the polytope by 1973.

Setting

A finite Markov decision model has a finite state set $E$, for each state $i$ a finite nonempty set $A(i)$ of actions, rewards $r_{ia}$ and transition probabilities $p_{iaj}\ge0$ with $\sum_j p_{iaj}=1$. A policy $R$ chooses, at each time $t=1,2,\dots$, an action in $A(i_t)$ at random, with probabilities that may depend on the entire history $(i_1,a_1,\dots,a_{t-1},i_t)$. Special classes are the Markov policies $C_M$ (the rule at time $t$ ignores the past), the stationary policies $C_S$, written $\pi^\infty$ (one rule $\pi$, with $\pi_{ia}\ge0$ and $\sum_a\pi_{ia}=1$, at every time), and the pure stationary policies $C_D$, written $f^\infty$ with $f(i)\in A(i)$. All policies form the class $C$.