Probability

Motivation

A process on a shared-memory multiprocessor that finds a lock held must decide what to do while it waits. It can spin, repeatedly testing the lock and occupying its processor, or it can block, giving the processor to another process and paying a fixed context-switch cost $C$ to be descheduled and later restored. Spinning is cheap when the lock is released soon; blocking is cheap when the wait is long. The waiting time is not known in advance, so the choice has to be made on-line. This is the spin-block problem, studied by Karlin, Manasse, McGeoch and Owicki in Competitive Randomized Algorithms for Nonuniform Problems (Algorithmica 11, 1994, doi:10.1007/BF01189993), §4. Mathematically it is the continuous form of the ski-rental problem, and the same rent-or-buy structure recurs in power-down policies and in TCP acknowledgement (Karlin, Kenyon, Randall, STOC 2001).

Timeline:

• Karlin, Manasse, Rudolph and Sleator (1988, doi:10.1007/BF01762111) introduced competitive analysis of snoopy caching and showed that $2$ is the optimal deterministic factor there. The spin-block analogue is recorded in the 1994 paper (pp. 558–559): spinning for time $C$ and then blocking is $2$-competitive, and no deterministic algorithm does better.
• Karlin, Manasse, McGeoch and Owicki (SODA 1990; Algorithmica 1994) found the optimal randomized factors for snoopy caching and spin-block. For spin-block, Theorem 10 (p. 559) gives $e/(e-1)\approx1.582$ against an oblivious adversary. Theorem 9 (p. 559) shows that against an adaptive on-line adversary randomization does not help: the factor stays $2$.

Setting

Fix a context-switch cost $C>0$. A lock wait is described by its release time $\tau\ge0$. An algorithm handling the wait chooses a blocking time $b\in[0,\infty]$: it spins until time $b$ and then blocks ($b=\infty$: never block). The cost of the wait is

$$\mathrm{waitCost}_C(b,\tau)=\begin{cases}\tau,&\tau\le b,\\ b+C,&b<\tau,\end{cases}$$

so a lock released exactly at the blocking time costs $\tau$. The optimal off-line algorithm, which knows $\tau$, pays $\min(\tau,C)$.

An input is a finite sequence $\sigma=(\tau_0,\dots,\tau_{n-1})$ of lock waits. A deterministic on-line algorithm chooses the blocking time of wait $j$ as a function of $\tau_0,\dots,\tau_{j-1}$, the release times it has already observed. Its cost $C_A(\sigma)$ is the sum of the wait costs, and the off-line cost is $C_{opt}(\sigma)=\sum_j\min(\tau_j,C)$.

A randomized on-line algorithm is a probability distribution over deterministic on-line algorithms: a probability space $(I,\mu)$ and a deterministic algorithm $A_i$ for each $i\in I$, with $i\mapsto C_{A_i}(\sigma)$ measurable for every $\sigma$. Its expected cost is $\mathbf{E}C_A(\sigma)=\int C_{A_i}(\sigma)\,d\mu(i)$. Following §1 of the paper, $A$ is $c$-competitive against an oblivious adversary if there is a constant $a$ with

$$\mathbf{E}C_A(\sigma)\le c\cdot C_{opt}(\sigma)+a\qquad\text{for every input }\sigma .$$

The adversary is oblivious: it fixes $\sigma$ before the algorithm's random choices are made.

The paper's algorithm blocks at a random time with cumulative distribution

$$\pi(t)=\begin{cases}\dfrac{e^{t/C}-1}{e-1},&0\le t\le C,\\[1ex] 1,&t>C,\end{cases}$$

where $\pi(t)$ is the probability of blocking before time $t$.

Formalization targets

Goal: Theorem 10 (p. 559)

For every $C>0$:

$$\Big(\forall A\ \forall c,\ A\ \text{is } c\text{-competitive}\ \Rightarrow\ c\ge\tfrac{e}{e-1}\Big)\quad\text{and}\quad\exists A,\ A\ \text{is } \tfrac{e}{e-1}\text{-competitive}.$$

Milestones

1. Expected cost of one wait (§4.1, p. 560). For a blocking time with law $\nu$ and release time $\tau$,

$$\mathbf{E}\,\mathrm{waitCost}_C(b,\tau)=\pi(\tau)\,C+\int_0^\tau(1-\pi(t))\,dt,\qquad \pi(t)=\nu\{b<t\}.$$

2. The ratio of the paper's distribution (§4.1, p. 560). With the $\pi$ above, for all $\tau\ge0$,

$$\pi(\tau)\,C+\int_0^\tau(1-\pi(t))\,dt\le\tfrac{e}{e-1}\min(\tau,C).$$

3. Theorem 10, first claim: the lower bound $c\ge e/(e-1)$ for every $c$-competitive randomized algorithm.
4. Theorem 10, second claim: existence of an $e/(e-1)$-competitive randomized algorithm.

Significance

Theorem 10 settles the randomized competitive ratio of the continuous ski-rental problem: $e/(e-1)$ is achievable and cannot be improved by any on-line algorithm, randomized or not, against an oblivious adversary. The same constant is the limit of the paper's snoopy-caching ratios $e_p/(e_p-1)$ as the block size grows, and it recurs in randomized rent-or-buy problems and in on-line primal-dual analyses.

The result is proved in the literature, and the mission's work is to formalize it. The platform has related material but not this statement: Primal-Dual Online Algorithms I: Fractional Ski Rental proves a deterministic, fractional, discrete-day bound (PrimalDualOnline.SkiRental.fractional_competitive), which is a different model and contains no lower bound. A complete formalization produces a reusable model of randomized on-line algorithms with history-dependent decisions and an exact lower bound for them.

Difficulty

The upper bound per lock wait is an explicit computation. The difficulty lies elsewhere. First, the on-line algorithm is allowed to adapt to the release times of all previous waits, so a bound for a single wait does not by itself bound a sequence: the randomized algorithm must be assembled so that each wait is handled with the right blocking law, whatever happened before. Second, the lower bound is a statement about every randomized algorithm and must survive the additive constant $a$: a single hard lock wait proves nothing, because $a$ absorbs any bounded loss. It has to be shown that on long sequences of waits every algorithm loses a factor $e/(e-1)$ on average. The natural first idea, to exhibit one bad release time for each algorithm, fails for randomized algorithms facing an oblivious adversary.

Formalization scope

All objects live in the namespace NonuniformCompetitive.SpinBlock. Release times are ℝ≥0, blocking times ℝ≥0∞, wait costs ℝ≥0∞, and the off-line cost is real. Committed conventions:

• $C>0$ is a hypothesis of every theorem (the paper's "some large cost $C$"); at $C=0$ blocking at once is free and the lower bound fails.
• A tie $b=\tau$ costs $\tau$; this matches "$\pi(t)$ is the probability that the algorithm blocks sometime before time $t$".
• Inputs are finite sequences of lock waits and competitiveness carries the additive constant $a$ of §1 (p. 543). A formalization with a single wait and no additive constant would be a different, easier lower bound and is ruled out.
• The on-line algorithm sees the release times of earlier waits (the information used by the paper's adaptive algorithms, p. 561). This enlarges the class of algorithms: it strengthens the lower bound and does not affect the upper bound.
• A randomized algorithm is a mixed strategy whose cost on each fixed input is measurable in the random outcome; the expected cost is a lower Lebesgue integral. Without measurability the lower integral would not be the expectation and the upper bound would become easier than the paper's.
• Milestone 1 is stated for every blocking law, not only for the paper's $\pi$. Milestone 2 keeps the paper's inequality, although equality holds.

Infrastructure a complete development needs: Lebesgue integrals of functions of a random variable (the layer-cake formula), interval integrals of the exponential, the construction of a probability measure on $[0,\infty]$ with a prescribed continuous distribution function, and a Yao-type averaging argument over finitely supported input distributions for the lower bound. The model of randomized on-line algorithms with history-dependent decisions is reusable for other rent-or-buy problems. Contributions welcome: proofs of the milestones, and intermediate lemmas such as the discretised lower bound for a fixed step $C/p$.

Selected references

• A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994), 542–571. doi:10.1007/BF01189993
• A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3 (1988), 79–119. doi:10.1007/BF01762111
• A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.
• A. R. Karlin, C. Kenyon, D. Randall, Dynamic TCP Acknowledgement and Other Stories about e/(e−1), STOC 2001, 502–509. doi:10.1145/380752.380845
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal–Dual Approach, Foundations and Trends in Theoretical Computer Science 3 (2009). doi:10.1561/0400000024

Motivation

Approximate policy iteration and policy gradient methods are the two classical families of reinforcement learning algorithms that work with approximate, sampled information instead of an exact model. Kakade and Langford (ICML 2002) observed that neither family answers three basic questions: is there a performance measure that is guaranteed to improve at every step, how hard is it to verify that an update improves it, and what performance is reached after a reasonable number of updates. Greedy approximate policy iteration can make the policy worse when the value estimates are slightly wrong at a few states, and policy gradient methods can stall on plateaus where estimating the gradient needs an enormous number of samples.

Their answer is conservative policy iteration: instead of jumping to a greedy policy, move only a controlled fraction of the way toward it, with a step size chosen from an estimate of how much the greedy policy helps. The paper proves that this update improves a restart-distribution performance measure monotonically, terminates after a number of iterations that depends only on the reward range and the target accuracy, and stops at a policy that the greedy oracle can no longer improve by much. The idea is the direct ancestor of trust-region and proximal policy optimization methods (TRPO, Schulman et al. 2015; PPO, Schulman et al. 2017), whose improvement bounds are refinements of the paper's Theorem 4.1.

Setting

A finite Markov decision process has a finite nonempty set of states $S$, a finite nonempty set of actions $A$, transition probabilities $P(s';s,a)$ (for each state $s$ and action $a$, a probability distribution over next states $s'$), a reward function $\mathcal R : S\times A\to[0,R]$ with $R>0$, and a discount factor $0\le\gamma<1$. A stochastic policy $\pi(a;s)$ gives, for each state $s$, a probability distribution over actions.

The normalized value of $\pi$ from $s$ is $V_\pi(s) = (1-\gamma)E[\sum_{t\ge0}\gamma^t\mathcal R(s_t,a_t)\mid\pi,s]$, where $s_0=s$, $a_t\sim\pi(\cdot\,;s_t)$, $s_{t+1}\sim P(\cdot\,;s_t,a_t)$; it lies in $[0,R]$. The state-action value is $Q_\pi(s,a) = (1-\gamma)\mathcal R(s,a)+\gamma E_{s'\sim P(s';s,a)}[V_\pi(s')]$ and the advantage is $A_\pi(s,a) = Q_\pi(s,a)-V_\pi(s)\in[-R,R]$.

For a state distribution $\mu$ (a restart distribution), the discounted future state distribution is $d_{\pi,\mu}(s) = (1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s;\pi,\mu)$ (eq. (2.1)), and the performance measure is $\eta_\mu(\pi) = E_{s\sim\mu}[V_\pi(s)]$.

The policy advantage of a policy $\pi'$ with respect to $\pi$ and $\mu$ is

$$\mathbb A_{\pi,\mu}(\pi') = E_{s\sim d_{\pi,\mu}}\big[E_{a\sim\pi'(a;s)}[A_\pi(s,a)]\big],$$

and $\mathrm{OPT}(\mathbb A_{\pi,\mu}) = \max_{\pi'}\mathbb A_{\pi,\mu}(\pi')$. The conservative update (4.1) is $\pi_{new} = (1-\alpha)\pi+\alpha\pi'$ with $\alpha\in[0,1]$. An $\varepsilon$-greedy policy chooser $G_\varepsilon$ (Definition 4.3) returns, for every policy $\pi$, a policy $\pi'$ with $\mathbb A_{\pi,\mu}(\pi')\ge\mathrm{OPT}(\mathbb A_{\pi,\mu})-\varepsilon$.

Conservative policy iteration (§5) starts from any policy and repeats: call $G_\varepsilon(\pi,\mu)$ to get $\pi'$; form an $\frac\varepsilon3$-accurate estimate $\hat{\mathbb A}$ of $\mathbb A_{\pi,\mu}(\pi')$ from $\mu$-restarts; if $\hat{\mathbb A}<\frac{2\varepsilon}3$, stop and return $\pi$; otherwise apply (4.1) with $\alpha = \frac{(1-\gamma)(\hat{\mathbb A}-\varepsilon/3)}{4R}$ and repeat.

Formalization targets

Goal: Theorem 4.4 (p. 5)

With probability at least $1-\delta$, conservative policy iteration (i) strictly improves $\eta_\mu$ with every policy update, (ii) stops after at most $72R^2/\varepsilon^2$ policy updates, and (iii) returns a policy $\pi$ with

$$\mathrm{OPT}(\mathbb A_{\pi,\mu}) < 2\varepsilon.$$

The estimation step is represented by its guarantee: each reached loop's estimate fails to be $\frac\varepsilon3$-accurate with probability at most $\delta/(N+1)$, $N=\lfloor72R^2/\varepsilon^2\rfloor$.

Milestones

Lemma 6.1 (p. 6), the performance difference identity:

$$\eta_\mu(\tilde\pi)-\eta_\mu(\pi) = \frac1{1-\gamma}E_{(a,s)\sim\tilde\pi d_{\tilde\pi,\mu}}[A_\pi(s,a)].$$

Theorem 4.1 (p. 4), with $\varepsilon=\max_s|E_{a\sim\pi'(a;s)}[A_\pi(s,a)]|$ and all $\alpha\in[0,1]$:

$$\eta_\mu(\pi_{new})-\eta_\mu(\pi)\ge\frac{\alpha}{1-\gamma}\Big(\mathbb A-\frac{2\alpha\gamma\varepsilon}{1-\gamma(1-\alpha)}\Big).$$

Corollary 4.2 (p. 5): if $\mathbb A\ge0$, the step size $\alpha=\frac{(1-\gamma)\mathbb A}{4R}$ gives

$$\eta_\mu(\pi_{new})-\eta_\mu(\pi)\ge\frac{\mathbb A^2}{8R}.$$

Significance

Theorem 4.4 is the first guarantee of its kind for approximate reinforcement learning: the number of iterations is bounded by $72R^2/\varepsilon^2$, independent of the number of states and of the restart distribution, and every iteration provably helps. Lemma 6.1 is the standard performance difference lemma, used throughout the analysis of policy optimization, including natural policy gradient and trust-region methods; Theorem 4.1 is the prototype of the "surrogate objective minus a penalty" bound that TRPO refines.

These results are proved in the paper. As far as a search of the platform shows, none is formalized: the platform's finite-horizon performance difference lemma (Foster and Rakhlin's Lemma 13) is a different statement, for episodic problems with non-stationary policies. This mission produces machine-checked versions of the discounted performance difference identity, the conservative improvement bound with its exact constants, and the high-probability termination and quality guarantee of the algorithm, all on top of an explicit infinite-horizon model rather than an assumed Bellman equation.

Difficulty

The obvious argument for the improvement bound expands $\eta_\mu(\pi_{new})$ to first order in $\alpha$; that only gives $\frac{\alpha}{1-\gamma}\mathbb A+O(\alpha^2)$ with an unspecified constant, which cannot fix a step size. The exact bound needs control of how far the state distribution of the mixed policy drifts from that of the old policy, uniformly in time, and the performance difference identity is only useful once the states are weighted by the new policy's distribution. On the formal side, $V_\pi$ and $d_{\pi,\mu}$ are infinite discounted series, so summability, exchanges of sums and the identities $\sum_s d_{\pi,\mu}(s)=1$ and $\sum_a\pi(a;s)A_\pi(s,a)=0$ must all be established from the definitions. For Theorem 4.4, the algorithm is a random process whose policies depend on all earlier estimates; the argument has to be made pathwise on the event that every reached loop is accurate, together with a union bound over the loops that can be reached.

Formalization scope

Policies are functions π : S → A → ℝ with π s a the paper's $\pi(a;s)$, and P s a s' is $P(s';s,a)$; both are constrained by the published predicates IsPolicy and IsTransitionKernel. $V_\pi$ is $(1-\gamma)$ times the published series PolicyValue, so values are normalized as in the paper. $\mathrm{OPT}$ is a real supremum over all stochastic policies; the set is nonempty and bounded, and the maximum is attained. Every theorem carries the standing assumptions of §2: finite nonempty $S$ and $A$, a transition kernel, rewards in $[0,R]$ with $R>0$, $0\le\gamma<1$, and a state distribution $\mu$. In Corollary 4.2, $R$ is any upper bound on the rewards rather than necessarily the attained maximum.

In Theorem 4.4 the run is formalized pathwise, driven by arbitrary real random estimates on a probability space; the conclusion bounds the probability of the failure event by $\delta$. Two deviations from the printed statement are disclosed. First, (ii) is stated for policy updates: the proof bounds updates, and the algorithm calls $G_\varepsilon$ once more than it updates, so "at most $72R^2/\varepsilon^2$ calls" is off by one. Second, the per-loop failure budget is $\delta/(N+1)$, which covers the $N+1$ loops that may be reached. The Hoeffding estimate (5.1) is not formalized: as printed it concerns the $\frac\varepsilon6$-biased target, and its role is taken by the accuracy hypothesis. The step size is clipped at $1$, which never binds when the estimate is accurate. No trivializing reading is available: the accuracy hypothesis is satisfied by a perfect estimator and a $0$-greedy chooser exists, so the theorem is not vacuous, and strict improvement at every update is required, not merely nonnegative change.

Pages are PDF pages; the paper has no printed page numbers.

A complete development needs summability and algebra of discounted occupation measures, the performance difference identity, and a union bound over the loops of a random process; the first two are reusable for any discounted policy-optimization result. Proofs of the milestones in any order are welcome.

Selected references

• S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002. https://dl.acm.org/doi/10.5555/645531.656005
• J. Schulman, S. Levine, P. Moritz, M. Jordan, P. Abbeel, Trust Region Policy Optimization, ICML 2015. https://arxiv.org/abs/1502.05477
• J. Schulman, F. Wolski, P. Dhariwal, A. Radford, O. Klimov, Proximal Policy Optimization Algorithms, 2017. https://arxiv.org/abs/1707.06347
• D. J. Foster and A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, 2023. https://arxiv.org/abs/2312.16730

Motivation

Scheduling jobs with release dates on one machine to minimize the total weighted completion time, written $1|r_j|\sum w_jC_j$, is strongly NP-hard even with unit weights (Lenstra, Rinnooy Kan & Brucker, 1977). It is a basic model of scheduling theory and a standard testbed for approximation algorithms built on linear programming relaxations. Several LP relaxations give lower bounds for it (Dyer & Wolsey, 1990; Queyranne, 1993), and the question how far these bounds can be from the optimum is also a question about the quality of branch-and-bound methods that use them.

Timeline, as surveyed in Table 1 of Goemans, Queyranne, Schulz, Skutella & Wang (2002):

• Phillips, Stein & Wein (Math. Programming, 1998) introduce converting a preemptive schedule into a nonpreemptive one by list scheduling, and the notion of $\alpha$-points; for the weighted problem their bound is $16+\epsilon$.
• Hall, Shmoys & Wein (SODA 1996) obtain 4; Schulz (IPCO 1996) and Hall, Schulz, Shmoys & Wein (Math. Oper. Res., 1997) obtain 3; Chakrabarti et al. obtain $2.8854+\epsilon$, and a combination of methods gives $2.4427+\epsilon$.
• Goemans (SODA 1997) orders jobs by $\alpha$-points of the LP schedule: $\alpha=1/\sqrt2$ gives $1+\sqrt2\approx2.4143$, a uniformly random $\alpha$ gives 2.
• Chekuri, Motwani, Natarajan & Stein (SIAM J. Comput., 2001) use random $\alpha$-points of an arbitrary preemptive schedule and obtain $e/(e-1)$ for unit weights, relative to the preemptive optimum rather than an LP value.
• Goemans, Queyranne, Schulz, Skutella & Wang (2002) prove $1.7451$ for the best common $\alpha$ and $1.6853$ for job-dependent random $\alpha_j$, both relative to the LP value $Z_R$. Afrati et al. (FOCS 1999) later give a polynomial-time approximation scheme, which does not bound the LP relaxations.

This mission formalizes the $1.6853$ result, the paper's main theorem.

Setting

There are $n$ jobs $N=\{0,\dots,n-1\}$. Job $j$ has an integral processing time $p_j>0$, an integral release date $r_j\ge0$ and a weight $w_j>0$. The jobs are indexed so that $w_0/p_0\ge w_1/p_1\ge\dots\ge w_{n-1}/p_{n-1}$.

The LP schedule is the preemptive schedule that at every moment processes the available (released, unfinished) job of smallest index. Since the data are integral, it is determined slot by slot: in $[\tau,\tau+1)$ it runs the smallest-index job $j$ with $r_j\le\tau$ and work left, or idles. Let $A^{LP}_j\subseteq\mathbb R$ be the set of times at which it processes $j$. The mean busy time of $j$ is

$$M^{LP}_j=\frac1{p_j}\int_{A^{LP}_j}t\,dt .$$

The mean busy time relaxation (R) has a variable $M_j$ per job:

$$Z_R=\min\Bigl\{\sum_j w_j\bigl(M_j+\tfrac12p_j\bigr)\ :\ \sum_{j\in S}p_jM_j\ge p(S)\bigl(r_{\min}(S)+\tfrac12p(S)\bigr)\ \text{for all nonempty }S\subseteq N\Bigr\},$$

with $p(S)=\sum_{j\in S}p_j$ and $r_{\min}(S)=\min_{j\in S}r_j$. $Z_R$ is a lower bound on the optimum of $1|r_j|\sum w_jC_j$.

For $0<\alpha\le1$ the $\alpha$-point $t_j(\alpha)$ is the first time at which $j$ has been processed for $\alpha p_j$ units in the LP schedule; $t_j(0^+)$ is the start time of $j$. For a vector $\boldsymbol\alpha\in(0,1]^n$, the $(\alpha_j)$-schedule processes the jobs nonpreemptively, as early as possible, in nondecreasing order of $t_j(\alpha_j)$; $C^{\boldsymbol\alpha}_j$ is the completion time of $j$ in it.

Let $\gamma\approx0.4835$ be the solution in $(0,1)$ of $\gamma+\ln(2-\gamma)=e^{-\gamma}\bigl((2-\gamma)e^{\gamma}-1\bigr)$, and set

$$\delta=\gamma+\ln(2-\gamma)\approx0.8999,\qquad c=1+\frac{e^{-\gamma}}{\delta},\qquad g(\alpha)=\begin{cases}(c-1)e^\alpha&0<\alpha\le\delta,\\0&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 3.9 (p. 185)

$c<1.6853$, and if $\alpha_1,\dots,\alpha_n$ each have density $g$ and are pairwise independent, then $\sum_j w_jC^{\boldsymbol\alpha}_j$ is integrable and

$$\mathbb E\Bigl[\sum_j w_jC^{\boldsymbol\alpha}_j\Bigr]\le c\cdot Z_R .$$

The bound is against the constant $c$ defined by the formula; the decimal $1.6853$ appears only in the separate inequality $c<1.6853$.

Milestones

1. Theorem 2.5 (p. 173): $M^{LP}$ is an optimal solution of (R), so $Z_R=\sum_jw_j(M^{LP}_j+\tfrac12p_j)$.
2. Eq. (3.1) (p. 176): $M^{LP}_j=\int_0^1t_j(\alpha)\,d\alpha$.
3. Corollary 3.2 (p. 179): $C^{\boldsymbol\alpha}_j\le t_j(\alpha_j)+\sum_{k:\alpha_k\le\eta_k(\alpha_j)}(1+\alpha_k-\eta_k(\alpha_j))p_k$, where $\eta_k(\alpha_j)$ is the fraction of $k$ processed by $t_j(\alpha_j)$.
4. Eq. (3.10) (p. 182): $M^{LP}_j=t_j(0^+)+\sum_{k\in N_2}(1-\mu_k)p_k+\tfrac12p_j$, where $N_2$ is the set of jobs processed between the start and completion of $j$ and $\mu_k$ is the fraction of $j$ processed before $k$ starts.
5. Eq. (3.11) (p. 183): the bound of Corollary 3.2 split over $N_1=N\setminus(N_2\cup\{j\})$ and $N_2$.
6. Lemma 3.11 (p. 185): $g$ is a probability density on $(0,1]$, and (i) $\int_0^\eta g(\alpha)(1+\alpha-\eta)\,d\alpha\le(c-1)\eta$, (ii) $(1+E_g[\alpha])\int_\mu^1g(\alpha)\,d\alpha\le c(1-\mu)$ for $\eta,\mu\in[0,1]$.

Significance

Theorem 3.9 gives a randomized algorithm for $1|r_j|\sum w_jC_j$ whose expected cost is at most $1.6853$ times the optimum, and a variant of it runs on-line (Theorem 3.14). Since $Z_R$ is a lower bound, it also shows that the relaxation (R), and the preemptive time-indexed relaxation (D), which has the same value, is within a factor $1.6853$ of the optimum (Corollary 3.10). The paper's Section 3.6 shows the gap of these relaxations can approach $e/(e-1)\approx1.5819$, so the bound is not far from what this relaxation can give.

The result is proved on paper; no machine-checked proof exists, and no part of this theory (LP schedule, $\alpha$-points, list scheduling from a preemptive schedule) is on the platform. The mission produces, besides the goal, a reusable formal account of $\alpha$-point scheduling: the LP schedule as a concrete object, the identity between mean busy times and average $\alpha$-points, and the deterministic completion-time bound of Corollary 3.2, which underlies many later $\alpha$-point analyses.

Difficulty

The obvious argument, bounding $C^{\boldsymbol\alpha}_j$ by Corollary 3.2 and integrating each $\alpha_k$ independently against $g$, does not work directly: the set of jobs $k$ with $\alpha_k\le\eta_k(\alpha_j)$ depends on $\alpha_j$, and the two effects of the random $\alpha_k$ pull in opposite directions (a small $\alpha_k$ shrinks the terms $1+\alpha_k-\eta_k$, a large one removes terms from the sum). The analysis needs the structure of the LP schedule around job $j$ (equations (3.9)–(3.11)) to separate the jobs whose $\eta_k$ is constant in $\alpha_j$ from those for which it jumps from $0$ to $1$, and then a density tuned to both at once. The claim is made under pairwise independence only, so no product structure of the random vector is available. On the formal side, the LP schedule, $\alpha$-points and list scheduling are defined from scratch, and the measure-theoretic content (integrability of a piecewise-constant function of $\boldsymbol\alpha$, conditioning under pairwise independence) is real work.

Formalization scope

Jobs are Fin n (0-based), $p$ and $r$ are natural numbers and $w$ is real. The ordering by $w_j/p_j$ is a hypothesis of every statement about the LP schedule, which is defined by the smallest-index rule; under that hypothesis the two coincide. The LP schedule is defined slot by slot, which is exact for integral data. Processing is represented by sets of times, not indicator functions. $t_j(\alpha)$ is an infimum over times, $t_j(0^+)=\inf A^{LP}_j$, and the $(\alpha_j)$-schedule is the closed form $C^{\boldsymbol\alpha}_j=\max_{k\preceq j}\bigl(r_k+\sum_{k\preceq i\preceq j}p_i\bigr)$ of list scheduling in lexicographic (α-point, index) order. $Z_R$ is the real infimum of the objective over the feasible set of (R), which is nonempty and bounded below for $w\ge0$. The random vector is any probability measure on $\mathbb R^n$ whose coordinate laws all equal the law with density $g$ and whose coordinates are pairwise independent; the product measure is one example, but the theorem is for all of them. $\gamma$ is any solution in $(0,1)$ of its equation.

A trivializing formalization is ruled out: the expectation is asserted together with integrability (a non-integrable integrand would have Bochner integral $0$), $g$ is supported on $(0,\delta]$ so every $\alpha_j$ lies in $(0,1]$ almost surely, and the bound is against $Z_R$ defined from (R), not against an expression that already contains Theorem 2.5.

Running times ($O(n\log n)$, $O(n^2)$), derandomization, the counting results (Proposition 3.8, Lemma 3.12) and the on-line variant are not formalized. Lemma 3.1 on the auxiliary $(\alpha_j)$-Conversion schedule is not a milestone; Corollary 3.2 is stated directly for the $(\alpha_j)$-schedule.

Contributions welcome: proofs of the milestones in any order; general lemmas on list scheduling and $\alpha$-points of preemptive schedules, which are reusable beyond this mission; and the measure-theoretic step from pairwise independence to the conditional bound on $\mathbb E[C^{\boldsymbol\alpha}_j\mid\alpha_j]$.

Selected references

• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella, Y. Wang, Single machine scheduling with release dates, SIAM J. Discrete Math. 15(2):165–192, 2002. https://doi.org/10.1137/S089548019936223X
• C. Phillips, C. Stein, J. Wein, Minimizing average completion time in the presence of release dates, Math. Programming 82:199–223, 1998.
• L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Math. Oper. Res. 22:513–544, 1997. https://doi.org/10.1287/moor.22.3.513
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM–SIAM SODA, 591–598, 1997.
• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31:146–166, 2001. https://doi.org/10.1137/S0097539797327180
• M. E. Dyer, L. A. Wolsey, Formulating the single machine sequencing problem with release dates as a mixed integer program, Discrete Appl. Math. 26:255–270, 1990.
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Ann. Discrete Math. 1:343–362, 1977.

Motivation

Minimizing the total weighted completion time $\sum_j w_j C_j$ of jobs with release dates on a single machine, written $1\,|\,r_j\,|\,\sum w_j C_j$ in scheduling notation, is strongly NP-hard. It is one of the basic models of machine scheduling, and it has served as a test case for a general technique in approximation algorithms: solve a linear programming relaxation, read off a preemptive schedule, and convert it into a nonpreemptive one using $\alpha$-points, the times at which a given fraction of each job has been processed. Phillips, Stein and Wein (doi:10.1007/BF01585872) introduced ordering jobs by points of a preemptive schedule; Goemans (SODA 1997, reference [11] of the paper below) and Chekuri, Motwani, Natarajan and Stein (doi:10.1137/S0097539797327180) showed that choosing $\alpha$ at random improves the guarantee.

Goemans, Queyranne, Schulz, Skutella and Wang (doi:10.1137/S089548019936223X) combine two LP relaxations, shown to have equal value, with carefully chosen random $\alpha$. This mission formalizes their Theorem 3.5: when a single $\alpha$ is drawn from a truncated exponential density, the resulting schedule costs in expectation at most $c < 1.7451$ times the LP lower bound.

Timeline:

• 1998: Phillips, Stein and Wein give the first constant-factor approximation (ratio $2$) for the unit-weight problem $1\,|\,r_j\,|\,\sum C_j$ by converting a preemptive schedule.
• 1997: Goemans (SODA) introduces randomly chosen $\alpha$-points for the weighted problem, the conference precursor of the paper formalized here.
• 2001: Chekuri, Motwani, Natarajan and Stein give a randomized $e/(e-1) \approx 1.58$-approximation for the unit-weight problem.
• 2002: Goemans, Queyranne, Schulz, Skutella and Wang give $1.7451$ for a single random $\alpha$ (Theorem 3.5) and $1.6853$ for job-dependent random $\alpha_j$ (Theorem 3.9), both against the same LP bound.
• 1999: Afrati et al. (doi:10.1109/SFFCS.1999.814574) give a polynomial-time approximation scheme for the problem. It is not LP-based, so the LP-relative factors of Theorems 3.5 and 3.9 remain of interest as bounds on the relaxations' integrality gaps.

Setting

There are $n$ jobs $N = \{1, \dots, n\}$. Job $j$ has an integral processing time $p_j > 0$, an integral release date $r_j \ge 0$ and a weight $w_j > 0$. The jobs are indexed so that $w_1/p_1 \ge w_2/p_2 \ge \cdots \ge w_n/p_n$.

A preemptive schedule gives each job a set $A_j \subseteq [r_j, \infty)$ of processing times of measure $p_j$, the sets pairwise disjoint. The mean busy time of $j$ is $M_j = \frac{1}{p_j}\int_{A_j} t\,dt$.

The LP schedule is the preemptive schedule that always processes the available job of smallest index, which under the indexing above is the available job of largest ratio $w_j/p_j$. Its mean busy times are $M^{LP}_j$.

The mean busy time relaxation (R) minimizes $\sum_j w_j (M_j + \tfrac12 p_j)$ subject to $\sum_{j \in S} p_j M_j \ge p(S)\big(r_{\min}(S) + \tfrac12 p(S)\big)$ for every nonempty $S \subseteq N$, where $p(S) = \sum_{j\in S} p_j$ and $r_{\min}(S) = \min_{j\in S} r_j$. Its optimal value is $Z_R$, a lower bound on the optimum of $1\,|\,r_j\,|\,\sum w_j C_j$.

For $0 < \alpha \le 1$, the $\alpha$-point $t_j(\alpha)$ is the first time at which $j$ has received $\alpha p_j$ units of processing in the LP schedule, and $t_j(0^+)$ is its start time. The $\alpha$-schedule processes the jobs nonpreemptively, each as early as possible, in nondecreasing order of $t_j(\alpha)$; $C^\alpha_j$ is the completion time of $j$ in it. More generally, the $(\alpha_j)$-schedule orders the jobs by $t_j(\alpha_j)$ for a vector $\boldsymbol\alpha = (\alpha_j)$.

Let $0 < \gamma < 1$ solve $1 - \frac{\gamma^2}{1+\gamma} = \gamma + \ln(1+\gamma)$ ($\gamma \approx 0.4675$), and set

$$c = \frac{1+\gamma}{1+\gamma-e^{-\gamma}}, \qquad \delta = 1 - \frac{\gamma^2}{1+\gamma}, \qquad f(\alpha) = \begin{cases}(c-1)e^{\alpha} & 0 < \alpha \le \delta,\\ 0 & \text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 3.5

If $\alpha$ is drawn with density $f$, then $c < 1.7451$, the expectation below is finite, and

$$\mathbb E_f\Big[\sum_{j} w_j C^\alpha_j\Big] \le c \cdot Z_R .$$

Milestones

1. Theorem 2.5: $M^{LP}$ is an optimal solution to (R), so $Z_R = \sum_j w_j (M^{LP}_j + \tfrac12 p_j)$.
2. Eq. (3.1): $M^{LP}_j = \int_0^1 t_j(\alpha)\,d\alpha$.
3. Corollary 3.2: $C^{\boldsymbol\alpha}_j \le t_j(\alpha_j) + \sum_{k:\,\alpha_k\le\eta_k(\alpha_j)} (1+\alpha_k-\eta_k(\alpha_j))\,p_k$, where $\eta_k(\alpha_j)$ is the fraction of $k$ processed by $t_j(\alpha_j)$ in the LP schedule.
4. Eq. (3.10): $M^{LP}_j = t_j(0^+) + \sum_{k\in N_2}(1-\mu_k)p_k + \tfrac12 p_j$, where $N_2$ is the set of jobs processed between the start and the completion of $j$ and $\mu_k$ the fraction of $j$ done before $k$ starts.
5. Eq. (3.11): the bound of Corollary 3.2 rewritten in terms of $N_1$, $N_2$ and $\mu_k$.
6. Lemma 3.6: $f$ is a density on $[0,1]$ with $\int_0^\eta f(\alpha)(1+\alpha-\eta)\,d\alpha \le (c-1)\eta$ and $\int_\mu^1 f(\alpha)(1+\alpha)\,d\alpha \le c(1-\mu)$ for $\eta, \mu \in [0,1]$.

Significance

Theorem 3.5 is a randomized $1.7451$-approximation for $1\,|\,r_j\,|\,\sum w_j C_j$, and simultaneously a bound on the integrality gap of (R): every instance has $\mathrm{OPT} \le 1.7451\, Z_R$. The paper also derandomizes it: there are at most $n$ distinct $\alpha$-schedules (its Proposition 3.8), and the best of them can be found in $O(n^2)$ time. The paper remarks that the truncated exponential density is optimal for its analysis and that the factor is tight for it.

On the formal side, the mission produces a reusable model of single-machine preemptive schedules, the LP schedule, $\alpha$-points and list scheduling, and the first machine-checked instance of the $\alpha$-point rounding technique that recurs across scheduling approximation. The result itself is proved in the paper; no machine-checked proof of it or of the LP-schedule identities (3.1), (3.10) is known to exist.

Difficulty

The obvious approach, bounding each $C^\alpha_j$ separately by a multiple of $t_j(\alpha)$, gives only the factor $\max\{1 + 1/\alpha, 1 + 2\alpha\}$ for fixed $\alpha$ (Theorem 3.3 of the paper), which is at least $1+\sqrt2$. The improvement needs the precise structure of the LP schedule around each job: which jobs interrupt $j$ ($N_2$) and which do not ($N_1$), and how the fraction $\eta_k(\alpha)$ of each other job depends on $\alpha$. Turning this structure into exact identities for piecewise-constant, piecewise-linear functions of $\alpha$ defined through a recursively built schedule is the bulk of the formal work. The analytic part (Lemma 3.6) is elementary but depends on the specific equation that defines $\gamma$.

Formalization scope

Jobs are Fin n (0-based) with $p, r : \texttt{Fin } n \to \mathbb N$ and real weights. The sortedness $w_j/p_j \ge w_k/p_k$ for $j \le k$, positivity $p_j > 0$ and $w_j > 0$ are hypotheses of every theorem about the LP schedule. Because the data are integral, the LP schedule is defined slot by slot on unit intervals $[\tau, \tau+1)$; a job's processing set is a finite union of such intervals. $\alpha$-points are infima over reals, and every statement restricts $\alpha$ to $(0,1]$. The $(\alpha_j)$-schedule's completion times are given by the closed form of list scheduling, $C_j = \max_{k \preceq j}(r_k + \sum_{k \preceq i \preceq j} p_i)$, with ties of $\alpha$-points broken by index (they do not occur for $\alpha \in (0,1]$). $Z_R$ is the infimum of the objective of (R) over its feasible set. The random $\alpha$ has law $f(\alpha)\,d\alpha$ on $\mathbb R$, and the expectation is a Lebesgue integral.

The goal asserts integrability of $\alpha \mapsto \sum_j w_j C^\alpha_j$ together with the bound, so the inequality cannot hold through the convention that a non-integrable function has integral $0$. The bound is against $Z_R$ defined from (R), not against $\sum_j w_j (M^{LP}_j + \tfrac12 p_j)$, which would build Theorem 2.5 into the goal; and the density's support $(0,\delta]$ is written out, so no mass is placed outside $(0,1]$. The running-time claims are not formalized, and the uniqueness of $\gamma$ is not asserted: the statements hold for every solution in $(0,1)$.

Useful infrastructure: finite unions of intervals and their measures, monotone piecewise-linear functions and their integrals, and list-scheduling identities. Contributions to any milestone, and general lemmas about the LP schedule (it is a preemptive schedule, has no idle time inside a job's span, processes interrupting jobs completely), are welcome.

Selected references

• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella, Y. Wang, Single Machine Scheduling with Release Dates, SIAM J. Discrete Math. 15(2):165–192, 2002. doi:10.1137/S089548019936223X
• C. Phillips, C. Stein, J. Wein, Minimizing average completion time in the presence of release dates, Math. Programming 82:199–223, 1998. doi:10.1007/BF01585872
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM-SIAM SODA, 591–598, 1997 (no DOI; reference [11] of Goemans et al. 2002).
• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31(1):146–166, 2001. doi:10.1137/S0097539797327180
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, Proc. 40th IEEE FOCS, 32–43, 1999. doi:10.1109/SFFCS.1999.814574

Motivation

A buyer and a seller negotiate over a single indivisible good. Each knows what the good is worth to them but not what it is worth to the other side, and each shades their offer to exploit the other's uncertainty. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this as a one-shot game in which both parties submit sealed offers simultaneously and a sale takes place at a weighted average of the two offers whenever the buyer's offer is at least the seller's.

The weight $k$ is a design parameter: $k = 1$ lets the buyer set the price, $k = 0$ the seller, and $k = 1/2$ splits the difference. For values uniform on a common interval the paper computes an explicit equilibrium for every $k$ (its Example 1) and then asks the questions a designer of the rule cares about: how often does trade happen, who gains when $k$ moves, and which $k$ maximises the expected gains of the two parties together. The answers are the subject of this mission.

The example became a benchmark for bilateral trade. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) proved that no mechanism can guarantee efficient trade with two-sided private information, and that for uniform values the split-the-difference equilibrium of this game attains the largest expected gains from trade of any mechanism. The numbers $9/32$ and $\tfrac{9}{64}\bar v$ below are therefore the second-best benchmarks against which later work on the $k$-double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) measures inefficiency.

Setting

A seller with reservation price $v_s$ and a buyer with reservation price $v_b$ each know their own value. The two values are drawn independently and uniformly on $[0, \bar v]$, with $\bar v > 0$; this law, written $\mathrm{unif}(\bar v)$, is also each player's belief about the other's value ($F_s(v) = F_b(v) = v/\bar v$ in the paper).

Under the Bargaining Rule with parameter $k \in [0,1]$, the seller asks $s$ and the buyer offers $b$. If $b \ge s$ the good is sold at price $P = kb + (1-k)s$, the seller earns $P - v_s$ and the buyer earns $v_b - P$; otherwise both earn zero. Ties trade.

An offer strategy maps a value to an offer. The strategies of Example 1(a) are

$$S(v_s) = \frac{v_s}{2-k} + \frac{1-k}{2}\bar v \quad\text{for } 0 \le v_s \le \tfrac{2-k}{2}\bar v, \qquad S(v_s) \ge \text{the same expression for } \tfrac{2-k}{2}\bar v < v_s \le \bar v,$$ $$B(v_b) = \frac{v_b}{1+k} + \frac{k(1-k)}{2(1+k)}\bar v \quad\text{for } \tfrac{1-k}{2}\bar v \le v_b \le \bar v, \qquad B(v_b) \le \text{the same expression for } 0 \le v_b < \tfrac{1-k}{2}\bar v.$$

A pair $(S, B)$ with these four properties is said to have the shape of Example 1(a) (IsExample1Pair k v̄ S B). On the two inequality ranges a seller asks too much, or a buyer bids too little, for any trade to occur, so the strategy there is free apart from the bound.

For such a pair, with $(v_s, v_b) \sim \mathrm{unif}(\bar v) \otimes \mathrm{unif}(\bar v)$, the trade probability is $\Pr[S(v_s) \le B(v_b)]$ (tradeProb), and the ex ante expected profits — taken before either value is drawn, as the paper specifies on p. 843 — are

$$\pi_s = \mathbb E\bigl[\mathbf 1\{S(v_s) \le B(v_b)\}\,(kB(v_b) + (1-k)S(v_s) - v_s)\bigr],\qquad \pi_b = \mathbb E\bigl[\mathbf 1\{S(v_s) \le B(v_b)\}\,(v_b - kB(v_b) - (1-k)S(v_s))\bigr]$$

(sellerExAnte, buyerExAnte).

Formalization targets

Goal: Example 1(c)(iii), total expected profit

For $0 \le k \le 1$, $\bar v > 0$ and every pair of the shape of Example 1(a),

$$\pi_s + \pi_b = \frac{\bar v}{16}(1+k)(2-k),$$

and as a function of $k \in [0,1]$ this total attains its maximum $\tfrac{9}{64}\bar v$ at $k = 1/2$. The goal is the paper's efficiency statement: among these equilibria, splitting the difference maximises expected group profit.

Milestones

1. Example 1(b). $\Pr[S(v_s) \le B(v_b)] = \dfrac{-k^2 + k + 2}{8}$, with maximum $9/32$ at $k = 1/2$.
2. Example 1(c)(i). $\pi_s(k) = \dfrac{\bar v}{48}(2-k)^2(1+k)$, strictly decreasing in $k$ on $[0,1]$.
3. Example 1(c)(ii). $\pi_b(k) = \dfrac{\bar v}{48}(1+k)^2(2-k)$, strictly increasing in $k$ on $[0,1]$.

The goal is the sum of milestones 2 and 3 together with a one-variable maximisation; milestone 1 describes the trade region over which both profits are integrated.

Significance

The formulas answer the design question for the rule. Moving $k$ toward the buyer's offer makes the price rule look more favourable to the seller, yet milestone 2 shows the seller's equilibrium profit falls and milestone 3 shows the buyer's rises: the paper (p. 844) uses this to show that an intuition which ignores the players' strategic response is mistaken. The comparison with truthful offers, which would trade with probability $1/2$ and earn expected group profit $\bar v/6$, quantifies the cost of strategic misrepresentation: at best $9/32$ and $\tfrac{9}{64}\bar v$.

The paper states these results as "straightforward computations" and prints no derivation. As far as is known, none of them has a machine-checked proof. A formalization settles the constants against the exact strategies of Example 1(a), including the non-linear no-trade branches the paper allows, and provides a worked example of computing trade probabilities and expected payoffs under a product of uniform laws, reusable for other double-auction and bilateral-trade examples.

Difficulty

The computation is elementary on paper, but the equilibrium strategies are only partly specified: on the seller's high range and the buyer's low range the offers are arbitrary functions subject to a bound, and need not be measurable. The obvious approach — substitute the linear formulas and integrate — is valid only after showing that these free branches never trade, so that the trade event and both integrands agree almost everywhere with their linear versions. The resulting integrals are over a product of two conditioned Lebesgue measures, not over Lebesgue measure on the plane, and the trade region depends on $k$ through both strategies. The monotonicity claims hold only on $[0,1]$ (the seller's cubic is not monotone on $\mathbb R$), and the derivative of each profit vanishes at an endpoint of the interval.

Formalization scope

Values are real numbers; the uniform law on $[0, \bar v]$ is Lebesgue measure conditioned on the interval (volume[|Icc 0 v̄]), and the joint law of $(v_s, v_b)$ is the product measure, with pairs ordered $(v_s, v_b)$. The trade probability is the real number (P {p | S p.1 ≤ B p.2}).toReal; the profits are Bochner integrals over the product. Ties trade. The results are ex ante, not conditional on a player's own value. Every theorem assumes $0 \le k \le 1$ and $\bar v > 0$. Maxima are stated with IsMaxOn on $[0,1]$ plus the value at $k = 1/2$; monotonicity with StrictAntiOn/StrictMonoOn on $[0,1]$.

The statements do not assume that $(S, B)$ is an equilibrium; they are computations about any pair of the shape of Example 1(a). That this pair is an equilibrium is Example 1(a) itself, the goal of a companion mission. No measurability of $S$ or $B$ is assumed: the free branches never trade, so each integrand agrees almost everywhere with a bounded measurable function and the integrals are the paper's expectations. A formalization that assumes $S$ and $B$ linear everywhere, or that integrates over a single uniform variable, proves a different statement.

A complete development needs: the reduction of the trade event and the integrands to their linear versions on $[0,\bar v]^2$; Fubini for the product of conditioned measures; evaluation of polynomial integrals over a triangle; and elementary calculus on cubics. Lemmas on integrating over products of uniform laws are reusable. Contributions of intermediate lemmas, such as the explicit trade region, are welcome.

Selected references

• K. Chatterjee and W. Samuelson, Bargaining under Incomplete Information, Operations Research 31(5):835–851, 1983. https://doi.org/10.1287/opre.31.5.835
• R. B. Myerson and M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2):265–281, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• M. A. Satterthwaite and S. R. Williams, Bilateral Trade with the Sealed Bid k-Double Auction: Existence and Efficiency, Journal of Economic Theory 48(1):107–133, 1989. https://doi.org/10.1016/0022-0531(89)90120-8
• W. Leininger, P. B. Linhart and R. Radner, Equilibria of the Sealed-Bid Mechanism for Bargaining with Incomplete Information, Journal of Economic Theory 48(1):63–106, 1989. https://doi.org/10.1016/0022-0531(89)90121-X

Motivation

Models of learning in games, and discrete choice models in econometrics, describe an agent who does not always pick the best alternative. Two descriptions of such an agent are standard. In the additive random utility model (McFadden 1981; Anderson, de Palma and Thisse 1992) the agent maximizes payoffs perturbed by random shocks. In the deterministic perturbation model (Fudenberg and Levine 1998) the agent chooses a probability vector and pays a deterministic, strictly convex cost for it. The logit choice rule arises from both: from i.i.d. extreme-value shocks, and from the entropy cost $V(y) = \eta \sum_j y_j \ln y_j$.

Hofbauer and Sandholm (Econometrica 70 (2002)) show that the second description is general enough to cover the first for every shock distribution with a strictly positive density, not only for logit. Their analysis of stochastic fictitious play rests on this: the deterministic representation provides the perturbed payoff functions from which Lyapunov functions for the learning dynamics are built, for arbitrary noise. This mission formalizes that discrete choice theorem, Theorem 2.1 of the paper, together with the steps of its proof.

Setting

Fix $n \ge 1$ alternatives $A = \{1, \dots, n\}$ with base payoffs $\pi = (\pi_1, \dots, \pi_n) \in \mathbb{R}^n$. A random vector $\varepsilon = (\varepsilon_1, \dots, \varepsilon_n)$ has a strictly positive density $f : \mathbb{R}^n \to \mathbb{R}$, whose law does not depend on $\pi$. The agent chooses the alternative whose total payoff $\pi_j + \varepsilon_j$ is largest, which gives the choice probability function $C : \mathbb{R}^n \to \mathbb{R}^n$,

$$C_i(\pi) = P\big(\operatorname{argmax}_j\, \pi_j + \varepsilon_j = i\big).$$

The probability simplex is $\Delta A = \{x \in \mathbb{R}^n_+ : \sum_j x_j = 1\}$, with relative interior $\operatorname{int}(\Delta A)$ (all coordinates positive) and tangent space $\mathbb{R}^n_0 = \{z \in \mathbb{R}^n : \sum_j z_j = 0\}$.

A deterministic perturbation is a function $V : \operatorname{int}(\Delta A) \to \mathbb{R}$. Because $V$ lives on the relative interior, its gradient $\nabla V(y)$ is the vector of $\mathbb{R}^n_0$ with $V(y + hz) = V(y) + (\nabla V(y) \cdot z) h + o(h)$ for all $z \in \mathbb{R}^n_0$, and its second derivative $D^2 V(y)$ is a quadratic form on $\mathbb{R}^n_0$. The perturbation is admissible if $V$ is twice continuously differentiable along the simplex, $D^2V(y)$ is positive definite on $\mathbb{R}^n_0$ for every $y$, and $\|\nabla V(y)\| \to \infty$ as $y$ approaches the boundary of $\Delta A$.

Formalization targets

Goal: Theorem 2.1

If $\varepsilon$ has a strictly positive density and $C$ is continuously differentiable, then there is an admissible $V$ such that, for every $\pi \in \mathbb{R}^n$,

$$C(\pi) = \operatorname*{argmax}_{y \in \operatorname{int}(\Delta A)} \big( y \cdot \pi - V(y) \big),$$

with a unique maximizer. The perturbation $V$ is one function serving all payoff vectors at once.

Milestones

The milestones are the steps of the paper's proof (pp. 5–7), in order:

1. Eq. (4). $DC(\pi)$ is symmetric, $\partial C_i/\partial \pi_j = \partial C_j / \partial \pi_i$, and its off-diagonal terms are strictly negative.
2. Eq. (5). $\partial C_i/\partial \pi_i = -\sum_{j \ne i} \partial C_j/\partial \pi_i$, and $DC(\pi)\mathbf{1} = 0$.
3. Eq. (6). $z \cdot DC(\pi) z > 0$ whenever $z$ is not proportional to $\mathbf{1}$.
4. Shift invariance and injectivity. $C(\pi + c\mathbf{1}) = C(\pi)$, and $C$ is one-to-one on $\mathbb{R}^n_0$.
5. Range observation. If the payoffs $\pi_j$, $j \in J$, stay bounded while the others tend to $+\infty$, then $C_j(\pi) \to 0$ for $j \in J$.
6. Convex potential. There is $W : \mathbb{R}^n \to \mathbb{R}$ with $\nabla W \equiv C$, strictly convex on $\mathbb{R}^n_0$.
7. Range. $C$ takes values in $\operatorname{int}(\Delta A)$, and $C(\mathbb{R}^n_0) = \operatorname{int}(\Delta A)$.

Significance

The result. Theorem 2.1 lets any smooth additive random utility model be replaced by an optimizing agent with a strictly convex, boundary-repelling cost. In the paper this is the bridge from the perturbed best response dynamic to a deterministic perturbed-payoff formulation, which yields Lyapunov functions for zero-sum games, games with an interior evolutionarily stable strategy, and potential games (§4 of the paper), and so the almost sure convergence of stochastic fictitious play under general noise (Theorem 6.1). Without it those convergence results would be restricted to noise distributions whose choice rule has a known deterministic representation, essentially logit. The paper also shows (Proposition 2.2) that the converse fails when $n \ge 4$: deterministic perturbations generate strictly more choice rules than random utility.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it is known. The mission asks for a formal proof of Theorem 2.1 and the seven steps above. Along the way it requires symmetric Jacobians of probability integrals, a gradient-field potential on $\mathbb{R}^n$, and the Legendre transform of a strictly convex function restricted to a hyperplane. None of these is currently packaged in Mathlib in the needed form.

Difficulty

The obvious argument is to take $V$ to be the Legendre transform of the potential $W(\pi) = \mathbb{E}\max_j(\pi_j + \varepsilon_j)$ and read off the first-order conditions. Three steps of that argument are not routine. First, the derivative identity (4) is a change of variables inside an $(n-1)$-fold integral over a moving region, and its strict sign needs the density to be positive on the relevant hyperplane sections. Second, the Legendre transform is well defined on all of $\operatorname{int}(\Delta A)$ only if $C$ maps $\mathbb{R}^n_0$ onto the whole open simplex. The paper takes this from Theorem 26.5 of Rockafellar (1970), whose hypotheses (essential smoothness, strict convexity, identification of the conjugate's domain) must be checked here. Third, positive definiteness of $D^2V$ and the gradient blow-up at the boundary are statements about the inverse of $C$ on $\mathbb{R}^n_0$. They need an inverse function argument on a subspace and a properness argument, not only pointwise convexity.

Verifying that $C(\pi)$ satisfies the first-order condition for one fixed $\pi$ does not suffice: the goal requires a single $V$ for all $\pi$, and a unique maximizer.

Formalization scope

Alternatives are indexed by Fin n with $n \ge 1$; vectors are Fin n → ℝ with its sup norm. The density is a real function $f$ that is continuous, strictly positive at every point, and has $\int f = 1$; the law of $\varepsilon$ is Lebesgue measure weighted by $f$. The paper's formula (4) evaluates $f$ on hyperplanes, which is meaningful for a continuous $f$. Without continuity the theorem can fail: a density that is positive everywhere but tends to zero near a hyperplane can make $C$ continuously differentiable with a vanishing off-diagonal derivative, and then no twice differentiable $V$ represents $C$. Continuous differentiability of $C$ is a hypothesis, as in the paper, stated as ContDiff ℝ 1 of the map $\pi \mapsto C(\pi)$. The event "$i$ is the argmax" uses strict inequalities; ties have probability zero.

$V$ is a function on $\mathbb{R}^n$ of which only the values on $\operatorname{int}(\Delta A)$ enter. Its smoothness and second derivative are taken in the chart $z \mapsto V(y + z)$ on the subspace $\mathbb{R}^n_0$. $\nabla V(y)$ is the tangent gradient of the paper's footnote 3, not an ambient gradient of an extension. The boundary blow-up is stated uniformly: for every $M$ there is $\delta > 0$ such that every tangent gradient at an interior point with some coordinate below $\delta$ has norm above $M$.

The goal cannot be satisfied trivially. $V$ must be chosen before $\pi$, all three admissibility conditions are part of the definition, and the maximizer must be unique. Weakening any of these (a $V$ depending on $\pi$, a $V$ without second derivatives, a non-strict maximum) changes the theorem.

Reusable infrastructure: differentiation of choice probabilities under a density, potentials of symmetric $C^1$ vector fields on $\mathbb{R}^n$, and Legendre duality for strictly convex functions on a subspace. Contributions of any of these as separate lemmas are welcome, as are alternative proofs of the milestones, for instance obtaining the potential directly as $\mathbb{E}\max_j(\pi_j + \varepsilon_j)$.

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 (theorem numbers and pages here follow the authors' manuscript of February 21, 2002).
• D. Fudenberg and D. K. Levine, The Theory of Learning in Games, MIT Press, 1998.
• S. P. Anderson, A. de Palma and J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992.
• D. McFadden, Econometric Models of Probabilistic Choice, in C. F. Manski and D. McFadden (eds.), Structural Analysis of Discrete Data with Econometric Applications, MIT Press, 1981.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173