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

Interior-point methods minimize a linear function $x\mapsto\langle c,x\rangle$ over a convex set $\mathcal K\subset\mathbb R^n$ by following the minimizers of $\langle c,x\rangle+\frac1t g(x)$ as $t\to\infty$, where $g$ is a self-concordant barrier for $\mathcal K$. Each Newton step of such a method shrinks $1/t$ by a factor $1-1/\sqrt\nu$, where $\nu$ is the self-concordance parameter of $g$, so $\nu$ controls the iteration count of every interior-point method built on $g$ (Nesterov and Nemirovski 1994; Nesterov 2004).

Timeline:

• 1994. Nesterov and Nemirovski construct the universal barrier for any convex body and show it is a $\nu$-self-concordant barrier with $\nu\le Cn$ for a universal constant $C$. They also show that $\nu\ge n$ is necessary for some bodies (the simplex, the cube).
• 2014–2015. Hildebrand (Math. Oper. Res. 2014) and Fox (Ann. Mat. Pura Appl. 2015) show that the canonical barrier of a convex cone has parameter equal to the dimension, which gives parameter $n+1$ for convex bodies.
• 2015. Bubeck and Eldan (arXiv:1412.1587, COLT 2015) show that the Fenchel dual of the log-Laplace transform of the uniform measure on $\mathcal K$, which they call the entropic barrier, is a $(1+o(1))n$-self-concordant barrier, with an explicit $o(1)$ term.

Beyond optimization, the entropic barrier is the mirror map that pairs naturally with the exponential-family sampling scheme in bandit linear optimization, which the paper discusses in its §3.1.

Setting

Let $\mathcal K\subset\mathbb R^n$ be a convex body: compact, convex, with non-empty interior $\operatorname{int}(\mathcal K)$. The log-Laplace transform of $\mathcal K$ is

$$f(\theta)=\log\left(\int_{x\in\mathcal K}\exp(\langle\theta,x\rangle)\,dx\right),\qquad\theta\in\mathbb R^n,$$

and the entropic barrier is its Fenchel dual

$$f^*(x)=\sup_{\theta\in\mathbb R^n}\ \langle\theta,x\rangle-f(\theta),\qquad x\in\operatorname{int}(\mathcal K).$$

For a function $g:\operatorname{int}(\mathcal K)\to\mathbb R$ write $\nabla g(x)[h]$, $\nabla^2g(x)[h,h]$, $\nabla^3g(x)[h,h,h]$ for its directional derivatives. Following Definition 1 of the paper:

1. $g$ is a barrier for $\mathcal K$ if $g(x)\to+\infty$ as $x\to\partial\mathcal K$;
2. a $C^3$ convex $g$ is self-concordant if $\nabla^3g(x)[h,h,h]\le2(\nabla^2g(x)[h,h])^{3/2}$ for all $x\in\operatorname{int}(\mathcal K)$, $h\in\mathbb R^n$;
3. it is $\nu$-self-concordant if moreover $\nabla g(x)[h]\le\sqrt{\nu\cdot\nabla^2g(x)[h,h]}$ for all such $x,h$.

The proof works with the canonical exponential family $p_\theta$, the probability measure with density $\exp(\langle\theta,x\rangle-f(\theta))\mathbb 1\{x\in\mathcal K\}$, its mean $x(\theta)$, covariance $\Sigma(\theta)$ and third central moment $T(\theta)$; with $Y=\langle\theta/\|\theta\|,X\rangle$ for $X\sim p_\theta$ and its density $\rho$; and with the section marginal $\lambda(y)=\mathrm{Vol}_{n-1}(\mathcal K\cap\{y\theta/\|\theta\|+\theta^\perp\})/\mathrm{Vol}(\mathcal K)$.

Formalization targets

Goal: Theorem 1

For every $n\ge80$ and every convex body $\mathcal K\subset\mathbb R^n$, $f^*$ is a $\nu$-self-concordant barrier for $\mathcal K$ with

$$\nu=(1+\varepsilon_n)\,n,\qquad\varepsilon_n=100\sqrt{\frac{\log n}{n}}.$$

Milestones, in attack order

1. Lemma 1 (p. 5): strict convexity of $f$, $f^*$; $\nabla f^*:\operatorname{int}(\mathcal K)\to\mathbb R^n$ is a bijection; $\nabla^2f=\Sigma$, $\nabla^3f=T$ (eqs. (4)–(5)); $\nabla^2f^*(x)=\Sigma(\theta(x))^{-1}$ (eq. (6)).
2. $f^*$ is a barrier (§4, p. 6).
3. Lemma 2 (p. 7): $\mathbb EX^3\le2(\mathbb EX^2)^{3/2}$ for a real centered log-concave $X$; its consequence $\mathbb E_{p_\theta}\langle X-x(\theta),h\rangle^3\le2(\mathbb E_{p_\theta}\langle X-x(\theta),h\rangle^2)^{3/2}$; $f^*$ is self-concordant (§4, pp. 6–7).
4. Reduction of (3) (p. 7): $f^*$ satisfies (3) with parameter $\nu$ iff $\langle\Sigma(\theta)\theta,\theta\rangle\le\nu$ for all $\theta$.
5. $\lambda$ is $n$-concave on its support (p. 9) and Lemma 5 (p. 9): $\varphi$ is $n$-concave iff $(\log\varphi)''\le-\frac1n((\log\varphi)')^2$.
6. Lemma 3 (p. 8): $\rho(y+y_0)=\rho(y_0)\zeta(y)e^{-y^2/(2\sigma^2)}$ on $[-M,M]$, with $\zeta\in[0,1]$ unimodal, $M=\sqrt{7n\log n}/\|\theta\|$, $\sigma^2=\frac{n}{\|\theta\|^2}\frac{1}{1-\sqrt{7\log(n)/n}}$; and its consequence (9): $\mathbb E(|Y-y_0|^2\mid|Y-y_0|\le M)\le\sigma^2$.
7. Lemma 4 (p. 8): $(1-2c(\varepsilon)\varepsilon\log^2(1/\varepsilon))\mathrm{Var}(X)\le\int_{x_1}^{x_2}(x-x_0)^2\lambda(x)dx\le\mathbb E(|X-x_0|^2\mid X\in[x_1,x_2])$ for log-concave $X$.
8. (7) (p. 7): $\mathrm{Var}(Y)\le\frac{n}{\|\theta\|^2}(1+\varepsilon_n)$.

Significance

The result. Theorem 1 gives, for every convex body, an explicit barrier whose parameter is $n$ up to a second-order term, against the $Cn$ of the universal barrier, and it is optimal up to that term because $\nu\ge n$ is necessary for some bodies. The barrier is defined by a single formula, its derivatives are moments of an explicit probability measure, and its parameter bound reduces to a variance bound for one-dimensional log-concave marginals. Lemmas 2 and 4 are self-contained facts about log-concave laws on $\mathbb R$ (a sharp third-moment bound and a variance-localization bound) that are usable outside this paper.

Formalizing it. The theorem is proved in the paper; nothing here is formalized elsewhere. The platform has a definition of self-concordance (reused here) and results for given self-concordant functions, but no universal or entropic barrier, no exponential family over a convex body, and no moment bounds for log-concave laws. A complete development produces machine-checked versions of the duality facts of Lemma 1, of the two log-concave lemmas, and of the Brunn–Minkowski consequence for section volumes. Two steps of the paper are sketched rather than proved in full: the end of the proof of Lemma 2 ("We omit further details of this proof", p. 12) and, in Lemma 4, a normalization step that cites a lemma stated for isotropic densities. A formal proof either fills or replaces them.

Difficulty

Self-concordance of $f^*$ reduces to self-concordance of $f$ by a general duality fact, and that reduces to Lemma 2; the difficulty there is the sharp constant $2$, since generic moment comparisons for log-concave laws give a worse constant. The parameter bound is the hard part. The obvious bound $\langle\Sigma(\theta)\theta,\theta\rangle\le Cn$ follows from standard concentration for log-concave measures, but any argument that loses a constant factor proves only the 1994 result. The $1+o(1)$ requires the one-dimensional marginal of the tilted measure to be compared with a Gaussian of variance $n/\|\theta\|^2$ to within a factor $1+O(\sqrt{\log n/n})$, using the fact that $\lambda$ is $n$-concave and not merely log-concave. The paper does this pointwise near the mode (Lemma 3) and controls the tails separately (Lemma 4). The pointwise argument assumes $\rho$ smooth, which holds for smooth bodies, and an approximation argument passes to general convex bodies.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so $n$ is the dimension, not a separate parameter. A convex body is compact, convex, with non-empty interior; a lower-dimensional set is excluded, which rules out a formalization in which the barrier and self-concordance clauses hold vacuously.

• $f^*$ is a real supremum. On $\operatorname{int}(\mathcal K)$ it is the true supremum; elsewhere Lean returns a junk value that no statement reads. The barrier property is a limit within $\operatorname{int}(\mathcal K)$ at every frontier point.

• Self-concordance (2) is the published ConvexOptimization.IsSelfConcordantOn on interior K, stated by line restrictions with an absolute value. It is equivalent to (2), because $h\mapsto-h$ flips the sign of the third derivative.

• The goal states the parameter as the explicit number $\nu=(1+100\sqrt{\log(n)/n})\,n$. The page says $\varepsilon_n\le100\sqrt{\log(n)/n}$, and (3) is monotone in $\nu$, so this is the same claim. An existential $\nu$ is not used.

• Corrections and implicit hypotheses:

  • Lemma 4 is stated for $0<\varepsilon<1$. The page says $\varepsilon>0$, but the statement is false for $\varepsilon\ge1$ and the paper applies it only with $\varepsilon<1$.
  • Lemma 5 assumes $\varphi>0$, which is implicit in $\zeta=\log\varphi$.
  • The reduction of (3) assumes $\nu\ge0$.
  • Lemma 3 and (9) carry the smoothness of $\rho$ (the paper's own without-loss-of-generality step on p. 7) as a hypothesis, and the theorem's range $n\ge80$.

• Section volumes use Mathlib's unnormalized $(n-1)$-dimensional Hausdorff measure. The normalization constant cancels in $\rho$ and does not affect $n$-concavity. $\lambda$ and $\rho$ are fixed pointwise functions, because Lemma 3 evaluates $\rho$ at a maximizer.

• Log-concavity on $\mathbb R$ is the published ConvexOptimization.LogConcaveOn on the whole line.

• Needed infrastructure that is reusable beyond this mission:

  • differentiation under the integral sign for exponential families on compact sets;
  • Fenchel duality for smooth strictly convex functions;
  • Brunn's concavity theorem for sections of convex bodies;
  • moment and tail bounds for log-concave densities on $\mathbb R$.

  Contributions to any of these, or proofs of single milestones, are welcome.

Selected references

• S. Bubeck, R. Eldan, The entropic barrier: a simple and optimal universal self-concordant barrier, COLT 2015; arXiv:1412.1587v3. https://arxiv.org/abs/1412.1587
• Y. Nesterov, A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• R. Hildebrand, Canonical barriers on convex cones, Mathematics of Operations Research 39:841–850, 2014.
• D. Fox, A Schwarz lemma for Kähler affine metrics and the canonical potential of a proper convex cone, Annali di Matematica Pura ed Applicata 194:1–42, 2015.
• B. Klartag, On convex perturbations with a bounded isotropic constant, Geometric and Functional Analysis 16(6):1274–1290, 2006.
• C. Borell, Convex set functions in d-space, Periodica Mathematica Hungarica 6(2):111–136, 1975.

Motivation

The k-server problem (Manasse, McGeoch and Sleator, 1990) is the central problem of online computation: $k$ servers sit on points of a metric space, requests arrive one at a time at points of the space, and each request must be served by moving a server to it, at a cost equal to the distance travelled. An online algorithm decides without knowing future requests; its quality is its competitive ratio, the worst-case ratio between its cost and the cost of an optimal offline schedule. Paging (caching) is the special case of a uniform metric, and weighted paging the case of a weighted star.

Timeline of the upper bounds for general metrics:

• 1990: Manasse, McGeoch and Sleator prove that every deterministic algorithm has ratio at least $k$ and conjecture that $k$ is achievable.
• 1991: Fiat, Rabani and Ravid give the first ratio depending on $k$ only (exponential in $k$).
• 1995: Koutsoupias and Papadimitriou prove that the work function algorithm is $(2k-1)$-competitive.
• For randomized algorithms against an oblivious adversary, the conjectured answer is $O(\log k)$, achieved for paging (Fiat et al., 1991), but until 2011 nothing better than the deterministic $2k-1$ was known for general metrics, even when the ratio may depend on the number of points $n$.
• 2011: Bansal, Buchbinder, Mądry and Naor give the first polylogarithmic bound, $O(\log^2 k\log^3 n\log\log n)$ (arXiv:1110.1580; J. ACM 62(5), 2015, DOI 10.1145/2783434), the result of this mission.

Setting

Let $(M,\mathrm{dist})$ be a finite metric space with $n$ points and $k$ a number of servers. A configuration $C:\{1,\dots,k\}\to M$ places server $i$ at $C(i)$. A deterministic online algorithm maps each prefix of the request sequence to a configuration that has a server at the last request; its cost on a sequence $\rho$ is the total distance travelled. $\mathrm{OPT}(C_0,\rho)$ is the least cost of any schedule serving $\rho$ from the initial configuration $C_0$. A randomized algorithm is a probability distribution over deterministic online algorithms, all starting at $C_0$; it is $c$-competitive if there is a constant $a$ such that its expected cost on every request sequence $\rho$ is at most $c\cdot\mathrm{OPT}(C_0,\rho)+a$.

The paper works with three auxiliary objects. A σ-HST is a rooted tree whose leaves are the points, in which all edges from a node to its children have one common length, equal to $1/\sigma$ times the length of the edge above that node; the distance between two leaves is the length of the tree path. A weighted σ-HST only requires that the edge above a non-root internal node be at least $\sigma$ times each edge below it. In the fractional k-server problem on a tree, the state is a vector $x$ of server probabilities on the leaves with $0\le x_i\le1$ and $\sum_i x_i=k$, a request at leaf $i$ forces $x_i=1$, and moving from $x$ to $x'$ costs $\sum_v W(v)\,|x'_v-x_v|$, where $x_v$ is the mass below node $v$ and $W(v)$ the length of the edge above $v$. In the allocation problem on a weighted star with weights $w_i$, requests carry a location $i^t$, a monotone cost vector $h^t(0)\ge\dots\ge h^t(k)\ge0$ (the cost of serving with $j$ servers there) and a server quota $\kappa(t)\le k$.

Formalization targets

Goal: Theorem 1

There is a universal constant $C>0$ such that for all $k\ge2$, every metric space $M$ with $n\ge3$ points and every initial configuration $C_0$, some randomized online algorithm starting at $C_0$ is

$$C\,\log^2 k\,\log^3 n\,\log\log n\text{-competitive.}$$

Milestones

In the order the proof uses them:

1. Claim 15: the fix-stage inequality behind the allocation algorithm's analysis.
2. Theorem 5: for every $0<\varepsilon\le1$, a fractional allocation algorithm whose hit cost is at most $(1+\varepsilon)(\mathrm{Opt}+w_{\max}g(\kappa))+a$ and whose movement cost is at most $O(\log(k/\varepsilon))(\mathrm{Opt}+w_{\max}g(\kappa))+a$, where $g(\kappa)=\sum_t|\kappa(t)-\kappa(t-1)|$.
3. Theorem 6: given such allocation algorithms, an $O(\ell\log(k\ell))$-competitive fractional k-server algorithm on every weighted σ-HST of depth $\ell$ with $\sigma=\Omega(\ell\log(k\ell))$.
4. Theorem 8: every σ-HST with $n$ leaves becomes a weighted σ-HST of depth $O(\log n)$ on the same leaves, with distances distorted by at most $2\sigma/(\sigma-1)$.
5. Lemma 25 and Theorem 24: on a σ-HST with $\sigma>5$, randomized states consistent with a changing fractional state can be maintained online at cost $O(c_t)$ per step.
6. Theorem 7: on a σ-HST with $\sigma>5$, a $c$-competitive fractional algorithm yields an $O(c)$-competitive randomized one.

Significance

The theorem broke the exponential gap between the $\Omega(\log k)$ lower bound and the $2k-1$ upper bound for randomized k-server, and showed that randomization helps on every finite metric, not only on uniform or specially structured ones. Its two-level method (a fractional algorithm on trees driven by per-node allocation problems, followed by an online rounding) became the template for later work, including the $O(\log^2 k)$ bound on HSTs of Bubeck, Cohen, Lee, Lee and Mądry (STOC 2018) and Lee's $O(\log^6 k)$ bound on general metrics (FOCS 2018).

The result is proved, in this paper. As far as is known it has no machine-checked proof. Formalizing it means formalizing the analysis of an online algorithm driven by a continuous-time process, a potential-function argument with exact constants, a tree contraction with a distortion bound, and an online randomized rounding against a transportation cost. The allocation, HST and rounding statements are reusable for other online problems on trees (metrical task systems, weighted paging).

Difficulty

For a deterministic or randomized algorithm on a tree, the natural recursion splits the servers of each node among its children. Coté, Meyerson and Poplawski showed that this works if each node solves an allocation problem with a strong guarantee: hit cost within a factor $1+\varepsilon$ of optimal. Integral allocation algorithms cannot achieve this; the integrality gap example of the paper (p. 8) gives a factor $\Omega(k)$. The fractional relaxation avoids the gap, but then the rounding step must keep a randomized state consistent with a fractional state at constant-factor cost, and the HSTs obtained from general metrics have depth growing with the aspect ratio, which a depth-dependent ratio cannot afford. Each of the three reductions (allocation to fractional k-server, deep HST to shallow weighted HST, fractional to randomized) loses only polylogarithmic or constant factors, and the main theorem needs all three at once.

Formalization scope

The k-server model, randomized algorithms and competitiveness are the published definitions KServer_model and KServer_randomized; competitiveness carries an additive constant fixed before the request sequence. Trees are finite rooted trees with a parent map, a depth function and positive edge lengths; points of the k-server problem are the leaves, and the theorems take an arbitrary finite metric space together with a bijection to the leaves and the hypothesis that the distance equals the tree distance. Fractional k-server states have exactly $k$ units of mass, each leaf at most $1$, and fractional algorithms are measured against the integral offline optimum. The allocation optimum is the integral optimum; cost vectors are finite, non-negative and non-increasing; the diameter of the star is $w_{\max}=\max_i w_i$. The cost of changing a randomized state is the transportation cost over couplings, with minimum-matching cost between configurations. Every $O(\cdot)$ is an explicit constant quantified before the instance, except that in Theorems 7 and 24 and Lemma 25 it may depend on $\sigma$.

Formalizations that make the targets trivial are excluded: the fractional state must place a full server on every request and stay in $[0,1]$, the benchmark is the integral optimum (not the algorithm's own or the fractional cost), and no constant may depend on $k$, $n$, the metric or the tree, since otherwise Theorem 1 would follow from the $2k-1$ bound.

The proof of Theorem 1 also uses the embedding of Fakcharoenphol, Rao and Talwar [18] of a finite metric into a distribution over σ-HSTs with expected distortion $O(\sigma\log_\sigma n)$. It is an external ingredient, not a result of this paper, and is not a milestone; contributions formalizing it (or Bartal's earlier embedding) are welcome, as are formalizations of the integral optimum's properties on trees (Lemmas 21–22 of the paper), which are not stated here.

Selected references

• N. Bansal, N. Buchbinder, A. Mądry, J. Naor, A Polylogarithmic-Competitive Algorithm for the k-Server Problem, arXiv:1110.1580v1, 2011; J. ACM 62(5), 2015. https://arxiv.org/abs/1110.1580, https://doi.org/10.1145/2783434
• M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, J. Algorithms 11, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
• E. Koutsoupias, C. Papadimitriou, On the k-server conjecture, J. ACM 42(5), 1995. https://doi.org/10.1145/210118.210128
• A. Fiat, R. Karp, M. Luby, L. McGeoch, D. Sleator, N. Young, Competitive paging algorithms, J. Algorithms 12, 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• J. Fakcharoenphol, S. Rao, K. Talwar, A tight bound on approximating arbitrary metrics by tree metrics, J. Comput. Syst. Sci. 69(3), 2004. https://doi.org/10.1016/j.jcss.2004.04.011
• A. Coté, A. Meyerson, L. Poplawski, Randomized k-server on hierarchical binary trees, STOC 2008. https://doi.org/10.1145/1374376.1374474

Motivation

Service parts supply chains are often limited by a capacitated resource, such as a production line or a repair shop, instead of by lead times alone. Once capacity binds, the classical tools for setting stock levels (Palm's theorem and the Poisson distribution of units in resupply) no longer apply, and the quantity that determines how much stock is needed is the shortfall: the amount by which the end-of-period inventory falls below its target because capacity was insufficient. Chapter 8 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) builds its tactical planning models for capacity-limited systems on the distribution of this random variable, and on a continuous-time repair queue in which item counts are geometric.

The shortfall recursion is the Lindley recursion of queueing theory (Lindley 1952), so its stationary law is the law of the maximum of a random walk with negative drift. The exponential tail of that maximum goes back to Cramér's work on ruin probabilities; for capacitated production–inventory systems it was stated by Glasserman (1997), whose theorem the book quotes as Theorem 11. Glasserman and Tayur (1995) used the shortfall to optimize base-stock levels in multi-echelon capacitated systems, and Roundy and Muckstadt (2000) studied the mass-exponential approximation that the theorem motivates.

Setting

A single item is produced in periods $n = 1, 2, \dots$ of an infinite horizon; at most $c$ units can be produced per period. The demand of period $n$ is $D_n$; the demands are nonnegative, independent and identically distributed, with generic demand $D$ and $E[D] < c$ (the standing assumption of Section 8.1.1).

Under the modified $(s-1, s)$ policy with target level $s$, the facility observes $D_n$ and produces $\min\{c, s - I_{n-1} + D_n\}$ units, where $I_n$ is the end-of-period net inventory and $I_0 = s$. The shortfall $V_n = s - I_n$ satisfies $V_0 = 0$ and

$$V_n = \left[V_{n-1} + D_n - c\right]^+ . \tag{8.1}$$

With the random walk $S_n = \sum_{k=1}^{n} (D_k - c)$ ($S_0 = 0$), the stationary shortfall is

$$V = \sup_{n \ge 0} S_n .$$

A law on $\mathbb R$ is lattice if it is concentrated on a progression $a + d\mathbb Z$ with $d > 0$.

In the discrete case ($c$ and $D$ integer valued) $(V_n)$ is a Markov chain on $\{0, 1, 2, \dots\}$ with transition probabilities $p_{ij}$ (p. 185). In the repair model of Section 8.3.1, reparable units of item $i$ arrive at rate $\lambda_i$, $\lambda = \sum_i \lambda_i$, a single exponential server repairs at rate $\mu > \lambda$, $N$ is the number of units in repair and $N_i$ the number of item-$i$ units, and $\eta_i = \lambda_i/(\mu - \lambda + \lambda_i)$.

Formalization targets

Goal: Theorem 11, corrected (p. 191)

Assume $E[e^{\alpha D}] < \infty$ for all $\alpha < \delta$, with $\delta > 0$; $P[D > c] > 0$; the law of $D$ is non-lattice; and $E[e^{-\alpha(c-D)}] = 1$ has a root in $(0, \delta)$. Then there are $\beta > 0$ and $\alpha > 0$ with

$$\frac{P\{V > v\}}{\beta e^{-\alpha v}} \to 1 \quad (v \to \infty), \qquad \alpha \text{ the unique positive root of } E\left[e^{-\alpha(c - D)}\right] = 1 .$$

The constant $\beta$ is left unspecified, as in the book.

Milestones, in attack order

1. Eq. (8.1): under the modified policy, $s - I_n = V_n$ for every $n$, independently of $s$.
2. Section 8.1.1: $V < \infty$ almost surely, $P\{V_n > v\} \to P\{V > v\}$ for every $v$, and the law of $V$ is stationary for (8.1).
3. Eq. (8.2): for $v > 0$, $P\{V_n > v\} = P\{D_n > v + c\} + E_D[1(d \le v + c)\, P\{V_{n-1} > v + c - d\}]$.
4. Theorem 11, second sentence: $E[e^{-\alpha(c-D)}] = 1$ has at most one positive root.
5. Section 8.1.2: with integer demand, $(V_n)$ is a Markov chain with transition probabilities $p_{ij}$.
6. Section 8.1.2: $\pi_i = \lim_n P\{V_n = i\}$ exists and solves $\pi\mathcal P = \pi$, $\sum_i \pi_i = 1$, $\pi_i \ge 0$.
7. Section 8.3.1: if $N$ is geometric with parameter $\lambda/\mu$ and $N_i$ given $N = j$ is binomial$(j, \lambda_i/\lambda)$, then $P[N_i = j] = (1 - \eta_i)\eta_i^j$.
8. Section 8.3.1: $\sum_{j > s} p_i(j) = \eta_i^{s+1}$, and the smallest cost-minimising stock level is the smallest $s$ with $\eta_i^{s+1} \le h_i/(h_i + b)$.

Significance

The exponential tail is the justification the book gives for approximating the shortfall by a mass-exponential law (an atom at zero plus an exponential tail), from which target stock levels and fill rates are computed in closed form. The decay rate $\alpha$ depends only on the demand law and the capacity, so the theorem also says how the stock needed for a given service level grows as utilization approaches one. The discrete-chain milestones justify the exact computation of the shortfall distribution behind the book's Table 8.1 and Figures 8.3–8.8. The geometric law of $N_i$ reduces the multi-item repair problem to independent newsvendor problems with an explicit solution.

The asymptotics of the random-walk maximum are proved in the literature (Cramér–Lundberg theory, Feller Vol. II, XII.5; Asmussen, Applied Probability and Queues, XIII.5); no machine-checked proof is known to exist. Mathlib has neither the Lindley recursion, nor ladder-height decompositions, nor the key renewal theorem for non-lattice laws. The printed Theorem 11 is not correct as stated (see Formalization scope), so the mission also records a corrected statement.

Difficulty

The central step of the goal is the passage from the random walk to an exact asymptotic. An exponential change of measure (Esscher tilt) with the root $\alpha$ turns $P\{V > v\}$ into an expectation under a law with positive drift, but it only yields the upper bound $P\{V > v\} \le e^{-\alpha v}$ (Lundberg's inequality); it does not show that $e^{\alpha v}P\{V > v\}$ converges, nor that the limit is positive. Convergence needs a renewal theorem for the overshoot of the tilted walk, which fails for lattice laws. That is why the non-lattice hypothesis cannot be dropped. For the milestones, the existence of the stationary law needs the reversal argument that identifies the law of $V_n$ with that of $\max_{k \le n} S_k$, plus the strong law of large numbers to show $V < \infty$ from $E[D] < c$.

Formalization scope

• Model. Demands are real, nonnegative, measurable, i.i.d. (iIndepFun plus IdentDistrib with $D_1$), integrable, with $E[D] < c$; these are fields of ShortfallModel. Periods are numbered from $1$ as in the book (demand 0 is an unused i.i.d. copy). The discrete case is a separate structure with $\mathbb N$-valued demand and capacity.
• Stationary shortfall. The book's "stationary distribution ... Let $V$ represent this random variable" is pinned to $V = \sup_{n \ge 0} S_n$, taken in $[0, \infty]$ and converted to a real number; milestone 2 proves that it is the limit law of $V_n$ from $V_0 = 0$ and a stationary law of (8.1). The discrete $\pi_i$ is pinned to $\lim_n P\{V_n = i\}$.
• Corrections to Theorem 11. The printed theorem is false. For integer demand $P\{V > v\}$ is a step function, and no $\beta e^{-\alpha v}$ is asymptotic to it. If $E[e^{\alpha D}]$ is finite only for $\alpha < \delta$, the equation $E[e^{-\alpha(c-D)}] = 1$ may have no root in $(0,\delta)$. The goal therefore adds two labelled hypotheses: a non-lattice demand law, and a root in $(0, \delta)$. The mass-exponential demand of Section 8.1.3 (an atom at $0$ plus a density) is non-lattice. The approximation $\beta \approx e^{-2(.583)(c-E(D))/\sigma}$ is not stated.
• Repair model. The M/M/1 queue is not built. The geometric law of $N$ (asserted on p. 202) and the binomial split of $N$ (quoted from Chapter 3) enter milestone 7 as hypotheses, exactly as the page's proof uses them. The stability condition $\lambda < \mu$, not written on the page, is a hypothesis. "The optimal $s_i$" is read as the smallest minimiser of the cost.
• Ruled out. Stating Theorem 11 with $\alpha$ or $\beta$ allowed to depend on $v$, with $\beta = 0$ (the ratio would be a division by zero, which Lean evaluates to $0$), or for a $V$ postulated to have an exponential tail proves nothing. Here $\beta, \alpha$ are quantified before $v$, both are asserted positive, and $V$ is constructed from the demands.
• Not formalized. The mass-exponential approximations (8.3)–(8.4), the Roundy–Muckstadt refinement, the fill-rate formula $\eta(s)$ (a definition, whose steady-state identity needs uniform integrability the book does not discuss), the random-capacity chain on p. 186, and the monotonicity of $s_i$ in $\mu$.
• Reusable infrastructure. Welcome: the Lindley recursion and its reversal identity, the Loynes existence theorem, Lundberg's inequality, and a non-lattice renewal theorem. All of these are needed well beyond this mission, in queueing (GI/G/1 waiting times) and ruin theory.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 8. https://doi.org/10.1007/b138879
• P. Glasserman, Bounds and asymptotics for planning critical safety stocks, Operations Research 45(2), 244–257, 1997. https://doi.org/10.1287/opre.45.2.244
• P. Glasserman and S. Tayur, Sensitivity analysis for base-stock levels in multiechelon production-inventory systems, Management Science 41(2), 263–281, 1995 (the book's reference [97]). https://doi.org/10.1287/mnsc.41.2.263
• R. O. Roundy and J. A. Muckstadt, Heuristic computation of periodic-review base stock inventory policies, Management Science 46(1), 104–109, 2000. https://doi.org/10.1287/mnsc.46.1.104.15131
• D. V. Lindley, The theory of queues with a single server, Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 277–289, 1952. https://doi.org/10.1017/S0305004100027638
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971, Chapter XII.
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003, Chapter XIII. https://doi.org/10.1007/b97236

Motivation

Large retailers hold point-of-sale and loyalty-card data that their suppliers cannot observe, and many of them sell access to it through data-sharing programs; others share the same data for free, or with only some suppliers (Shang, Ha & Tong 2016, §1). When two competing manufacturers sell through one common retailer, sharing a demand signal with a manufacturer changes how he sets his wholesale price, which in turn changes the retailer's margins and the rival's demand. Whether the retailer wants to share, with how many manufacturers, and at what price, is therefore a question about a multistage game with incomplete information.

Shang, Ha and Tong answer it for linear demand, a linear-expectation signal and quadratic production costs, under two contracting protocols. This mission covers the production economy case (marginal cost decreasing in volume, §6 of the paper), in which the retailer may have an incentive to share information even without payment. A companion mission covers production diseconomy (§5).

Setting

Two manufacturers $i \in \{0,1\}$ sell substitutable products through a common retailer. Demand for product $i$ is

$$q_i = a + \theta - (1+\phi)p_i + \phi p_j ,$$

where $p_i$ is the retail price, $\phi > 0$ measures competition intensity and $\theta$ is a demand shock with mean $0$ and variance $\sigma^2 > 0$. The retailer observes a demand signal $Y$ with $E[Y \mid \theta] = \theta$ and a linear-expectation structure $E[\theta \mid Y] = \beta Y$, where $\beta = \beta(t,\sigma)$ is the signal weight. Producing $q$ units costs $bq - c_e q^2$ with $c_e > 0$; the paper writes $c = -c_e$ and assumes $c_e < 2/(1+\phi)$ (the Assumption, p. 251). Retailing is costless.

The game has three stages.

1. Information contracting. Under concurrent contracting the retailer offers both manufacturers the same payment $T \ge 0$ for the signal; they decide simultaneously and play a Pareto-optimal pure equilibrium. Under sequential contracting she offers a payment $T_f$ to a first manufacturer $k$ and, after his decision, a payment $T_s$ to the other; the outcome is a subgame-perfect equilibrium (SPE). The retailer commits not to share for free after a rejection (§6.2).
2. Pricing. Given the information statuses $X_i \in \{I, U\}$, each manufacturer sets a wholesale price $w_i$ (a function of $Y$ if informed, a constant otherwise), then the retailer sets retail prices; the solution concept is Bayesian Nash equilibrium.
3. Demand realizes and profits are collected.

The ex ante profits of the pricing equilibrium are denoted $\pi_M(0)$, $\pi_M^U(1)$, $\pi_M^I(1)$, $\pi_M(2)$ for a manufacturer and $\pi_R(n)$ for the retailer, $n$ the number of informed manufacturers. $n_e^N$, $n_e^C$, $n_e^S$ denote the equilibrium number of informed manufacturers without contracting, under concurrent and under sequential contracting.

Formalization targets

Goal: Proposition 8(d)

For every $\phi > 0$ and $0 < c_e < 2/(1+\phi)$, pricing equilibria exist, concurrent outcomes and sequential SPEs exist, and for every concurrent outcome and every SPE (either first mover)

$$\Pi_R^C \le \Pi_R^S, \qquad \Pi_M^S \le \Pi_M^C ,$$

where $\Pi_R$ is the retailer's profit after side payments and $\Pi_M$ the manufacturers' total profit net of them. The second inequality is asserted for all $c_e$ except at most two values depending only on $\phi$. The comparisons about every pricing equilibrium family exclude the single value $c_e^* = (2+3\phi)/[(1+2\phi)(1+\phi)]$ (see Formalization scope). The paper says "higher"; the inequalities are weak because both sides coincide on intervals of positive length.

Milestones

1. Lemma 1: the pricing equilibrium exists and, for $c_e \ne c_e^*$, is unique and linear in $Y$ with explicit coefficients.
2. §4.2: the ex ante profits $\pi_M(\cdot)$ and $\pi_R(\cdot)$ in closed form.
3. Lemma 5(a)–(c) and Lemma 5(d): sign comparisons of these profits in $c_e$, with thresholds $1/(1+\phi)$, $(4+5\phi)/[(2+3\phi)(1+\phi)]$, $c_e^a$ and $c_e^N$.
4. Proposition 7: thresholds $c_e^C$, $c_e^S$ such that

$$n_e^Z = 0 \text{ for } c_e < \tfrac{1}{1+\phi}, \quad n_e^Z = 2 \text{ for } \tfrac{1}{1+\phi} \le c_e < c_e^Z, \quad n_e^Z = 1 \text{ for } c_e^Z \le c_e < \tfrac{2}{1+\phi}.$$

5. Proposition 6(b): the same structure for $n_e^N$ with a threshold $c_e^N$.
6. Proposition 8(a): $c_e^N < c_e^S \le c_e^C$.

Significance

Proposition 8(d) says that a common retailer who sells information prefers to sell it sequentially, and that the manufacturers bear the cost: sequential offers let her extract a larger payment from the first manufacturer, because his outside option depends on what she will do with the second. Together with Propositions 6 and 7 it explains why retailers under production economy share with only a subset of suppliers once economies of scale or competition are strong, and why a retailer may share data for free, a practice the diseconomy model cannot produce.

The results are proved in the paper, partly by "it is straightforward" arguments (the proofs of Lemmas 2–5 are omitted). No part of the paper is formalized. A formalization adds a machine-checked account of the equilibrium selection at the boundary payments, where the paper's case analysis is informal, and of the points at which the retailer is indifferent between outcomes.

Difficulty

The pricing stage is a Bayesian game with a continuum of strategies: an informed manufacturer's strategy is an arbitrary square-integrable function of the signal. Lemma 1's uniqueness needs the Assumption (without it the manufacturer's problem is not concave) and a conditional-expectation argument, not a finite-dimensional computation. The comparisons of Lemma 5 are sign conditions on rational functions of $(c_e, \phi)$ whose thresholds $c_e^a$, $c_e^N$ are implicit roots. The contracting stage is where the naive argument fails: at the boundary payments several equilibria give the retailer the same payoff but the manufacturers different payoffs, so "the" outcome is not well defined there, and a direct comparison of closed-form profits at the paper's selected equilibria does not cover every equilibrium.

Formalization scope

Lean represents manufacturers by Fin 2, statuses by an inductive type with informed and uninformed, and a pricing strategy by a function of the signal value. The committed conventions are these.

1. Admissible strategies are measurable with square-integrable $w_i(Y)$, and constant for an uninformed manufacturer; ex ante optimality over them is the Bayesian equilibrium condition.
2. The retailer's rule is a best response for every wholesale price pair and signal value, off path included.
3. The production cost is the uncapped quadratic $bq - c_e q^2$. The paper caps the quantity at $\bar q = b/(2c_e)$ but assumes the cap is reached with negligible probability (footnote 11, p. 251) and computes every result of §4.2 and §6 without it. The condition $b < a$ of that footnote is not imposed.
4. Contracting uses pure strategies, nonnegative payments, and no free-sharing move after a rejection.
5. A concurrent outcome is a payment and a pure equilibrium whose retailer payoff equals the supremum of her payoffs over Pareto-optimal equilibria. The supremum is not always attained: for large $c_e$ the paper's optimal payment $\pi_M^I(1) - \pi_M(0)$ makes $(U,U)$ an equilibrium that Pareto-dominates the one-informed outcome it selects.
6. Threshold statements take the two-clause form: the stated value of $n$ is attained on each region with its printed endpoints, and is the only value on the region's interior. Thresholds depend only on $\phi$ and are quantified before all other parameters.
7. The manufacturers' comparison in the goal excludes at most two values of $c_e$. At the thresholds $c_e^C$, $c_e^S$ outcomes with different manufacturer totals coexist, and the universal comparison fails.
8. A correction of the paper. At $c_e^* = (2+3\phi)/[(1+2\phi)(1+\phi)]$, which lies in $(1/(1+\phi), 2/(1+\phi))$, the slope of the best-response wholesale price (2) is exactly $-1$. The equations $w_i = \hat w_i(w_j)$ are then singular, and every status profile has a continuum of pricing equilibria (for $n = 0$, $w_{1,2} = \bar w \pm t$ for every $t$) whose ex ante profits differ. Lemma 1's uniqueness claim fails there, so do the §4.2 identities for every equilibrium family, and so does every statement built on them. Each statement that quantifies over all pricing equilibria therefore assumes $c_e \ne c_e^*$; existence is still asserted at $c_e^*$.

The ex ante profits in every statement are those of an equilibrium of the pricing game on the signal model, not the §4.2 closed forms; a formalization that defined them by the closed forms would reduce the goal to algebra and a $2 \times 2$ game, and is ruled out. The model layer (signal model, pricing equilibrium, payoff table, both contracting games) is shared, name for name, with the production diseconomy mission. Contributions are welcome on each milestone, and on reusable pieces: linear-expectation signals, and pointwise optimization under conditional expectation.

Selected references

• Shang W., Ha A. Y., Tong S., Information Sharing in a Supply Chain with a Common Retailer, Management Science 62(1):245–263, 2016. https://doi.org/10.1287/mnsc.2014.2127
• Ericson W. A., A note on the posterior mean of a population mean, Journal of the Royal Statistical Society B 31(2):332–334, 1969 (cited for the formula of $\beta(t,\sigma)$, which this mission does not use).
• Vives X., Oligopoly Pricing: Old Ideas and New Tools, MIT Press, 1999, §2.7.2.
• Li L., Information sharing in a supply chain with horizontal competition, Management Science 48(9):1196–1212, 2002. https://doi.org/10.1287/mnsc.48.9.1196.177

Motivation

Stochastic fictitious play is a basic model of learning in repeated games. Each period every player best responds to the empirical frequencies of the opponents' past play, after the player's payoffs have been hit by a fresh random shock. It was introduced by Fudenberg and Kreps (1993), is a standard object in the theory of learning in games (Fudenberg and Levine, The Theory of Learning in Games, 1998), and underlies the quantal-response and logit-learning models used in experimental economics and multi-agent reinforcement learning. The question is whether the players' beliefs settle down, and on what.

Potential games, in which all players receive the same payoff, cover pure coordination games and, after the usual payoff transformations, congestion games and weighted potential games. For them Hofbauer and Sandholm (Econometrica 70, 2002) proved that stochastic fictitious play converges almost surely, and that under a generic regularity condition the limit is a single linearly stable rest point of the perturbed best response dynamic.

Timeline. Fudenberg and Kreps (1993) and Kaniovski and Young (1995) established convergence in 2×2 games. Benaïm and Hirsch (1999) related the process to its mean ordinary differential equation and proved convergence in some $p$ player, two strategy games. Hofbauer (2000) and Hofbauer and Hopkins (2000) constructed Lyapunov functions for the deterministically perturbed dynamics. Hofbauer and Sandholm (2002) combined these with a representation theorem for random utility models and with Pemantle's (1990) nonconvergence theorem to obtain the result formalized here.

Setting

A $p$ player game has finite strategy sets $S^\alpha = \{0,\dots,n^\alpha-1\}$ and utilities $u^\alpha : S \to \mathbb R$ on pure profiles $S = \prod_\beta S^\beta$. The game is a potential game if $u^\alpha(s) = u^\beta(s)$ for all players and all profiles. Mixed profiles form $\Sigma = \prod_\alpha \Delta S^\alpha$, and player $\alpha$'s payoff vector is $U^\alpha_i(x^{-\alpha}) = \sum_{s:\,s^\alpha=i} u^\alpha(s)\prod_{\beta\ne\alpha}x^\beta_{s^\beta}$.

Player $\alpha$'s payoffs are perturbed by a random vector $\varepsilon^\alpha$ with a strictly positive density $f^\alpha$ on $\mathbb R^{n^\alpha}$. The choice function is $C^\alpha_i(\pi) = P(\arg\max_j \pi_j + \varepsilon^\alpha_j = i)$, assumed continuously differentiable, and the perturbed best response is $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$.

In standard stochastic fictitious play, shocks $\varepsilon^\alpha_t$ are independent over time and across players. From an arbitrary initial pure profile, at time $t+1$ each player plays a maximizer of $U^\alpha_k(Z_t^{-\alpha}) + (\varepsilon^\alpha_t)_k$, where the beliefs are the time averages

$$Z_t = \frac1t\sum_{u=1}^t \zeta_u .$$

The mean dynamic of this process is the perturbed best response dynamic

$$(P)\qquad \dot x^\alpha = \tilde B^\alpha(x^{-\alpha}) - x^\alpha .$$

A rest point $x^*$ of (P) is hyperbolic if every eigenvalue of $DF(x^*)$ restricted to the tangent space $\prod_\alpha \mathbb R^{n^\alpha}_0$ of $\Sigma$ has nonzero real part, and linearly stable if every such eigenvalue has negative real part. $RP(P)$ and $LS(P)$ denote the rest points and the linearly stable rest points.

By Theorem 2.1 of the paper, $C^\alpha(\pi) = \arg\max_{y\in\operatorname{int}\Delta}(y\cdot\pi - V^\alpha(y))$ for an admissible deterministic perturbation $V^\alpha$, so (P) coincides with the deterministically perturbed dynamic (PV), in which the argmax replaces $C^\alpha$.

Formalization targets

Goal: Theorem 6.1(iii)

For every potential game, every family of densities meeting the conditions above, every probability space, independent shock family and initial profile:

1. if the shocks are smooth enough that the $V^\alpha$ are $C^N$, $N = \sum_\alpha(n^\alpha-1)$, then

$$P\big(\omega(Z_t)\text{ is a connected subset of } RP(P)\big) = 1;$$

2. if every rest point of (P) is hyperbolic and the field of (P) is $C^2$, then

$$P\Big(\lim_{t\to\infty} Z_t \text{ exists and lies in } LS(P)\Big) = 1.$$

Milestones

In attack order: Theorem 2.1 (the representation), Proposition 4.1 (the function $\Pi(x) = \sum_s u^1(s)\prod_\alpha x^\alpha_{s^\alpha} - \sum_\alpha V^\alpha(x^\alpha)$ is a strict Lyapunov function for (PV)), the identification of the critical points of $\Pi$ with the rest points of (PV), Proposition 4.2 ($CR(PV) = RP(PV)$ under $C^N$ smoothness), Proposition 4.3 (under hyperbolicity $RP(PV)$ is finite and equals $CR(PV)$), and Lemmas A.5 and A.4 (a uniform nondegeneracy condition for the noise of the process).

Significance

The result. Theorem 6.1(iii) says that decentralised, boundedly rational learning in common-interest games does not cycle or wander: beliefs converge to a rest point of the perturbed dynamic, and generically to one that is linearly stable, hence a local maximizer of the perturbed potential $\Pi$. Rest points approximate Nash equilibria as the noise vanishes (Proposition 3.1 of the paper), so the theorem is a selection result for equilibria reached by learning. It is also a template for the stochastic-approximation analysis of learning algorithms whose mean dynamic has a Lyapunov function.

Formalizing it. The theorem is proved in the paper, but none of its ingredients is machine-checked: the random utility representation, chain recurrence of flows, Lyapunov arguments for (PV), and the stochastic-approximation step (Benaïm–Hirsch, Benaïm, Pemantle) are all absent from Mathlib and from this platform. A complete development produces a reusable stochastic-approximation layer, not only this theorem.

Difficulty

The obvious argument, "(P) has a strict Lyapunov function, so the process converges to its rest points", fails twice. First, a strict Lyapunov function does not by itself make every chain recurrent point a rest point (the paper cites counterexamples of Akin and of Benaïm); the step needs either Sard's theorem for a $C^N$ function or finiteness of the rest points, and the stochastic-approximation theory controls the process only through the chain recurrent set. Second, convergence to linearly stable points requires showing that the process avoids unstable rest points. This rests on Pemantle's theorem, whose nondegeneracy hypothesis must be verified uniformly over states and directions (Lemma A.4). Neither step follows from the ODE alone: the theorem is about the random process $Z_t$.

Formalization scope

Players are Fin p with p ≥ 2, strategies Fin (n α) with n α ≥ 1, and mixed profiles live in the ambient space (α : Fin p) → Fin (n α) → ℝ, on which every vector field is defined. Choice probabilities are probabilities of strict argmax events under volume.withDensity (f α). The process $Z_t$ is defined pathwise from the shocks, ties broken by the smallest index (a null event), and the theorem quantifies over every probability space and every independent shock family with the given laws. Derivatives of $V^\alpha$ are those of $V^\alpha$ composed with the projection onto the plane $\sum_i y_i = 1$. Eigenvalues are the complex roots of the characteristic polynomial of the derivative restricted to the tangent space of $\Sigma$. Solutions of a dynamic are differentiable curves on $[0,\infty)$ that stay in $\Sigma$, and chain recurrence uses $\varepsilon$-chains with times $t_i \ge 1$.

A formalization about the ODE (P) in place of the process $Z_t$, a fixed noise law such as logit, or convergence to $RP(P)$ in place of $LS(P)$ would prove a different and weaker statement. These are excluded.

Needed infrastructure: the random utility representation (mission I of this series), flows and chain recurrence of $C^1$ vector fields on compact sets, Sard's theorem for real-valued $C^N$ functions, and the stochastic-approximation theorems of Benaïm–Hirsch (1999, Thm 3.3), Benaïm (1999, Props. 5.3 and 6.4) and Pemantle (1990, Thm 1). The last three are reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376
• M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Fictitious Play in Perturbed Games, Games and Economic Behavior 29, 36–72, 1999. https://doi.org/10.1006/game.1999.0717
• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, 1–68, 1999. https://doi.org/10.1007/BFb0096509
• R. Pemantle, Nonconvergence to Unstable Points in Urn Models and Stochastic Approximations, Annals of Probability 18(2), 698–712, 1990. https://doi.org/10.1214/aop/1176990853
• D. Fudenberg and D. M. Kreps, Learning Mixed Equilibria, Games and Economic Behavior 5, 320–367, 1993. https://doi.org/10.1006/game.1993.1021
• J. Hofbauer and E. Hopkins, Learning in Perturbed Asymmetric Games, Games and Economic Behavior 52, 133–152, 2005. https://doi.org/10.1016/j.geb.2004.06.006