All missions

Motivation

Facility location models decide where to open depots, warehouses or service centres and which customers each one serves. Classical models assume that an open facility always works. In practice facilities are disrupted by weather, strikes, power loss or supplier failure, and a network designed for normal operation can become very expensive when its nearest facilities go down. Reliable facility location models place facilities so that the sum of the fixed cost and the expected transportation cost, taken over random facility failures, is minimal.

Cui, Ouyang and Shen (UCTC-FR-2010-02, 2010; published as Oper. Res. 58(4):998–1011) study the case in which each site fails independently with its own probability. The most direct model of this situation is a scenario-based stochastic program: list every pattern of failures, give it its probability, and let each customer be served optimally in each pattern. That program has $2^J$ scenarios for $J$ candidate sites and cannot be written down for realistic $J$. The paper proposes instead a compact formulation in which each customer receives an ordered list of backup facilities ("levels") and the probability that each level is the one that serves her is carried by a small set of recursive variables. This mission is about the claim that the compact model loses nothing.

The level-assignment technique comes from Snyder and Daskin (Transp. Sci. 39(3):400–416, 2005), who treated the case of one common failure probability for all sites. The uniform-probability model of Snyder and Shen's textbook is on the platform as SupplyChainTheory_disruptions; it is a different model (one $q$, no cap on the number of levels) and is not reused here.

Setting

There are $I$ customers $i = 0,\dots,I-1$ with demand rates $\lambda_i \ge 0$ and $J$ candidate sites $j = 0,\dots,J-1$ with fixed costs $f_j$ and failure probabilities $0 \le q_j < 1$. Failures are independent. Shipping one unit from site $j$ to customer $i$ costs $d_{ij}$, and each unit of missed demand of customer $i$ costs a penalty $\phi_i$. An emergency facility with index $J$ never fails ($q_J = 0$), costs nothing to open ($f_J = 0$), and "serves" at the penalty cost $d_{iJ} = \phi_i$.

The compact model (RUFL). Each customer is assigned to facilities at levels $r = 0,\dots,R$, with $R \ge 1$; a level-$r$ facility serves her exactly when all her facilities at levels $0,\dots,r-1$ have failed. The variables are $X_j\in\{0,1\}$ (site $j$ open), $Y_{ijr}\in\{0,1\}$ (facility $j$ is customer $i$'s level-$r$ facility) and $P_{ijr}$, the probability that $j$ serves $i$ at level $r$. Constraints (1b)–(1d) say that each level holds one facility until the emergency facility appears, which happens exactly once, and that only open sites are used, each at most once. Constraints (1e)–(1f) fix $P$: $P_{ij0} = 1-q_j$ and $P_{ijr} = (1-q_j)\sum_{k<J}\frac{q_k}{1-q_k}P_{i,k,r-1}Y_{i,k,r-1}$. The objective is

$$\Phi(X,Y,P) = \sum_{j=0}^{J-1} f_jX_j + \sum_{i=0}^{I-1}\sum_{j=0}^{J}\sum_{r=0}^{R}\lambda_i d_{ij}P_{ijr}Y_{ijr}.$$

The scenario model (SSP). A scenario is $\omega\in\Omega=\{0,1\}^J$, with $\delta_{j\omega}=1$ if site $j$ operates in $\omega$ (and $\delta_{J\omega}=1$ always). Its probability is $p_\omega = \prod_{j<J}(1-q_j)^{\delta_{j\omega}}q_j^{1-\delta_{j\omega}}$. With $Y_{ij\omega}\in\{0,1\}$ (customer $i$ served by $j$ in $\omega$), (SSP) minimizes

$$\Psi(X,Y) = \sum_{j=0}^{J-1} f_jX_j + \sum_{i=0}^{I-1}\sum_{j=0}^{J}\sum_{\omega\in\Omega}\lambda_i d_{ij}p_\omega Y_{ij\omega}$$

subject to $\sum_{j=0}^{J}Y_{ij\omega}=1$ and $Y_{ij\omega}\le\delta_{j\omega}X_j$ for regular $j$.

Formalization targets

Goal: Proposition 1 (p. 10)

If $R = J$, both programs have optimal solutions, and for every optimal $(X,Y,P)$ of (RUFL) and every optimal $(X',Y')$ of (SSP),

$$\Phi(X,Y,P) = \Psi(X',Y').$$

The paper states this as "formulation (1a)–(1g) is equivalent to the stochastic programming formulation that covers all failure scenarios"; its proof shows equality of optimal values, and that is the reading formalized.

Milestones (Appendix A.1, pp. 32–34)

1. Scenario-probability identity. For distinct regular sites $j(0),\dots,j(r-1)$ and a facility $j(r)$ not among them, the scenarios in which $j(0),\dots,j(r-1)$ fail and $j(r)$ operates have total probability

$$\sum_{\omega\in\Omega(i,r)}p_\omega = (1-q_{j(r)})\prod_{\ell=0}^{r-1}q_{j(\ell)}.$$

2. (RUFL) → (SSP). Every (RUFL)-feasible $(X,Y,P)$ has an (SSP)-feasible $(X,Y')$ with $\Psi(X,Y') = \Phi(X,Y,P)$, for any $R$.
3. Normalization. Some optimal solution of (SSP), with the same $X$, serves every customer in every scenario by her closest operating open facility, ties to the lowest index.
4. (SSP) → (RUFL). If $R = J$, every normalized (SSP)-feasible $(X,Y)$ has a (RUFL)-feasible $(X,Y',P')$ with $\Phi(X,Y',P') = \Psi(X,Y)$.

Significance

The proposition says that, with enough levels, the compact model is exact: its optimal value is the true minimum expected cost over all failure patterns. The compact model has $O(IJR)$ variables and constraints against $O(IJ2^J)$ for (SSP), and after the standard linearization of the products $P_{ijr}Y_{ijr}$ it is an ordinary mixed-integer program to which the paper's Lagrangian relaxation applies. For $R<J$ the paper notes the compact model is in general not equivalent; Proposition 1 is the anchor that says what the parameter $R$ trades away.

The result is proved in the paper; as far as we know it has not been formalized. The work here is to formalize that proof: the product-measure computation behind milestone 1, the two explicit solution maps, and the exchange argument behind the normalization. The probability identity for "first success in an ordered list of independent trials" and the scenario-to-level bookkeeping are reusable for other reliability models built on Snyder–Daskin levels.

Difficulty

The cost identities are routine once the right bookkeeping is in place; the obstacle is that bookkeeping. In direction (RUFL) → (SSP) one must show that the recursion (1e)–(1f), which multiplies by $q_k/(1-q_k)$ and sums over all regular $k$, collapses to the closed product $(1-q_{j(r)})\prod_{\ell<r}q_{j(\ell)}$ along a customer's assigned list, using that (1b)–(1d) put exactly one facility on each level until the emergency facility and that (1c) forbids repeats. Then the sum over the $2^J$ scenarios must be regrouped by the first operating facility on that list, which needs milestone 1 on a product space.

The converse direction is where $R=J$ enters, and the naive attempt fails: an arbitrary optimal (SSP) solution may serve a customer by different, equally good facilities in different scenarios in ways that no single ordered list reproduces. The normalization step removes this freedom; only after it can one read off a single list per customer, and $R=J$ guarantees that this list (all open sites no farther than the penalty, then $J$) fits on the available levels.

Formalization scope

Indices are 0-based; facilities are Fin (J+1) with Fin.last J the emergency facility, and levels are Fin (R+1). The extended data $d_{iJ}=\phi_i$, $q_J=0$, and the conventions $\delta_{J\omega}=1$, $X_J=1$ are definitions, not hypotheses. Scenarios are Fin J → Bool and $p_\omega$ is the explicit finite product; no measure theory is involved, and (17a) is a finite sum. Binary variables are real numbers constrained to $\{0,1\}$. $R = J$ is expressed by taking the instance type Instance I J J; with the standing $R\ge 1$ this means $J\ge1$. Demand rates are nonnegative; no sign is assumed on $d$, $\phi$ or $f$.

Two printed constraints are corrected, and the formalization commits to the corrections. The first sum in (1b) is printed over the regular sites $j\le J-1$; it runs here over all $J+1$ facilities, as the paper's own reading of (1b) requires. Constraint (17c) is printed as $\sum_i Y_{ij\omega}\le\delta_{j\omega}X_j$, which gives each site a capacity of one customer per scenario and makes Proposition 1 false; it is stated here per customer, $Y_{ij\omega}\le\delta_{j\omega}X_j$.

The goal asserts existence of optimal solutions of both programs before comparing their values, so it cannot hold vacuously. Contributions welcome: proofs of the milestones, a general lemma on the probability that the first success among independent Bernoulli trials occurs at a given position, and an existence-of-optimum lemma for finite binary programs.

Selected references

• X. Cui, Y. Ouyang, Z.-J. M. Shen, Reliable Facility Location Design under the Risk of Disruptions, UCTC-FR-2010-02, University of California Transportation Center, 2010; Operations Research 58(4):998–1011, 2010. https://doi.org/10.1287/opre.1090.0801
• L. V. Snyder, M. S. Daskin, Reliability models for facility location: the expected failure cost case, Transportation Science 39(3):400–416, 2005. https://doi.org/10.1287/trsc.1040.0107
• H. D. Sherali, A. Alameddine, A new reformulation-linearization technique for bilinear programming problems, Journal of Global Optimization 2(4):379–410, 1992. https://doi.org/10.1007/BF00122429

Why backup assignments matter

A facility location plan decides which sites to open and which customers each site serves. Real facilities fail: plants are shut by strikes, warehouses by floods, distribution centres by power outages. When a customer's facility is down, she is served by a backup facility, or not served at all at a penalty. Reliable facility location chooses sites and backup assignments together, minimizing fixed costs plus the expected transportation and penalty cost over the random failures.

Snyder and Daskin (2005) introduced the level-assignment formulation in which every customer receives a ranked list of facilities, and they assumed all sites fail with the same probability. Cui, Ouyang and Shen (2010) allow each site its own failure probability $q_j$, which is the realistic case: a site in a flood plain and a site inland do not fail equally often. Their compact mixed-integer program (RUFL) is the subject of this mission.

Timeline.

• Snyder and Daskin (2005), Transportation Science 39(3): level-assignment formulation of the reliability P-median and UFL problems, equal failure probability $q$; consecutive assignments are ordered by distance in an optimal solution.
• Snyder and Shen, Fundamentals of Supply Chain Theory, Theorem 9.10 (textbook treatment): the same ordering for the reliable fixed-charge location problem with $0<q<1$ and positive demands.
• Cui, Ouyang and Shen (2010), UCTC-FR-2010-02 / Operations Research 58(4): site-dependent failure probabilities $q_j$, a cap $R$ on the number of levels, and Proposition 2, the ordering result for this model.

The model (RUFL)

There are customers $i = 0,\dots,I-1$ with demand rates $\lambda_i$, and candidate sites $j = 0,\dots,J-1$ with fixed costs $f_j$ and failure probabilities $0 \le q_j < 1$; failures are independent. Shipping one unit from $j$ to $i$ costs $d_{ij}$, and each unserved unit of customer $i$ costs a penalty $\phi_i$. An emergency facility with index $J$ represents non-service: $f_J = 0$, $q_J = 0$ and $d_{iJ} = \phi_i$.

Each customer is assigned at levels $r = 0,\dots,R$, $R\ge 1$. Her level-$r$ facility serves her exactly when all her facilities at levels $0,\dots,r-1$ have failed. The variables are $X_j\in\{0,1\}$ (site $j$ open), $Y_{ijr}\in\{0,1\}$ (facility $j$ is customer $i$'s level-$r$ facility) and $P_{ijr}$, the probability that $j$ serves $i$ at level $r$. (RUFL) minimizes

$$\Phi(X,Y,P) = \sum_{j=0}^{J-1} f_jX_j + \sum_{i=0}^{I-1}\sum_{j=0}^{J}\sum_{r=0}^{R}\lambda_i d_{ij}P_{ijr}Y_{ijr}$$

subject to: at every level a customer has exactly one facility unless she has already reached the emergency facility (1b); only open sites are used, each at most once (1c); the emergency facility is assigned exactly once (1d); and the probabilities follow the transition equations

$$P_{ij0} = 1-q_j,\qquad P_{ijr} = (1-q_j)\sum_{k=0}^{J-1}\frac{q_k}{1-q_k}P_{i,k,r-1}Y_{i,k,r-1}\quad (1\le r\le R).$$

So if a customer's levels are $j_0, j_1, \dots$, then $P_{i j_r r} = (1-q_{j_r})\,q_{j_0}\cdots q_{j_{r-1}}$.

Formalization targets

Goal: Proposition 2

Assume $\lambda_i > 0$ for every customer and $q_k > 0$ for every regular site. In every optimal solution $(X,Y,P)$ of (RUFL),

$$Y_{ijr} = 1,\ Y_{ik,r+1} = 1 \ \Longrightarrow\ d_{ij}\le d_{ik}\qquad (0\le r,\ r+1\le R,\ 0\le j,k\le J),$$

where $d_{iJ} = \phi_i$.

Milestones (the proof of Appendix A.2)

1. Swap identity. If $(X,Y,P)$ is feasible with $Y_{ijr} = Y_{ik,r+1} = 1$ for regular $j,k$, exchanging $j$ and $k$ and recomputing $P$ gives a feasible solution whose cost changes by

$$\lambda_i(1-q_k)(d_{ik}-d_{ij})P_{ijr}.$$

2. Emergency case. If instead $k = J$, moving $J$ up to level $r$ and dropping $j$ gives a feasible solution whose cost changes by $\lambda_i P_{ijr}(\phi_i - d_{ij})$.
3. Positivity. If every regular $q_k>0$, an assigned facility has $P_{ijr}>0$.

Significance

Proposition 2 says that for a given set of facilities assigned to a customer, the optimal order of the levels depends only on the distances, not on the failure probabilities. A solution method may therefore sort each customer's assigned facilities by distance instead of searching over orders. The paper's Lagrangian subproblem (RSP$_i$) uses exactly this: "following a similar argument to Proposition 2" (§3.3.1, p. 13), its objective depends only on the set of facilities chosen, which is what makes the set function of Proposition 3 (a separate mission of this series) well defined. The proposition does not say that the $R$ nearest open facilities are the right ones: the paper's Example 1 (p. 11) shows a farther but more reliable facility can be optimal.

The result is proved in the paper; no machine-checked proof exists. The equal-probability special case is published on Prove2Me as SupplyChainTheory.rflp_ordered_assignments (Snyder–Shen Theorem 9.10), in a different model (one $q$, no level cap). This mission adds the site-dependent case with a level cap, and it makes explicit two hypotheses the printed statement omits.

Difficulty

The exchange argument is short on paper, but its bookkeeping is exactly where a formal proof has to work. The paper's modified $P'$ keeps the old values at unlisted indices, and that array does not satisfy the transition equations, so feasibility of the swapped solution has to be shown with the recomputed probabilities, level by level, including the fact that levels after $r+1$ are unchanged. The emergency case is dismissed in one sentence; its cost change must be computed. Finally, "$<0$" needs $\lambda_i>0$ and $P_{ijr}>0$; the naive reading of the printed proposition, with $q_j = 0$ allowed, is false, because a level-0 facility that never fails leaves all later levels with probability zero and in arbitrary order.

Formalization scope

Indices are 0-based. Facilities are Fin (J+1) with the emergency facility Fin.last J; levels are Fin (R+1); the extended data $d_{iJ}=\phi_i$, $q_J=0$ are definitions. $X$, $Y$, $P$ are real arrays, with (1g) requiring $X$, $Y$ to be $0$ or $1$. Constraint (1b) is printed with its first sum ending at $J-1$; it is formalized with the sum over all $j \le J$, the reading the paper's own explanation of (1b) gives. "Optimal" means feasible with objective at most that of every feasible solution; the feasible set is nonempty (send every customer to $J$ at level 0), so the goal is not vacuous. Proposition 2 carries the hypotheses $\lambda_i>0$ and $q_k>0$; without them it is false, and a statement that dropped them would be unprovable rather than trivial. The level $r$ ranges over $0\le r\le R-1$, the range in which level $r+1$ exists.

The development needs only finite sums and a recursion over levels; no measure theory is required. The recomputed probabilities transProb and the two moves swapY, emergencyUpY are reusable for any exchange argument on this formulation. Proofs of the milestones, of the goal, and of the equivalence of the transition equations with the closed product form are welcome.

Selected references

• Cui, T., Ouyang, Y., Shen, Z.-J. M., Reliable Facility Location Design under the Risk of Disruptions, UCTC-FR-2010-02, University of California Transportation Center, 2010; published in Operations Research 58(4):998–1011, 2010. https://doi.org/10.1287/opre.1090.0801
• Snyder, L. V., Daskin, M. S., Reliability Models for Facility Location: The Expected Failure Cost Case, Transportation Science 39(3):400–416, 2005. https://doi.org/10.1287/trsc.1040.0107
• Snyder, L. V., Shen, Z.-J. M., Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, §9.6. https://doi.org/10.1002/9781119584445

Motivation

Many decision problems in operations research ask for the best element of a finite set of alternatives when each alternative's cost is random: which projects to fund when resource use is uncertain, which crew pairings to fly when delays are random, which items to pack into a knapsack whose overflow is penalized. The expected cost is rarely available in closed form, because it is a high-dimensional integral over the distribution of the random data. The sample average approximation (SAA) method replaces the expectation by an average over a random sample and solves the resulting deterministic problem with a standard discrete optimization routine. The method is widely used in stochastic programming (see Shapiro, Dentcheva and Ruszczyński, Lectures on Stochastic Programming, SIAM 2009, Ch. 5, https://doi.org/10.1137/1.9780898718751).

Kleywegt and Shapiro (preprint; published with Homem-de-Mello as SIAM J. Optim. 12(2):479–502, 2002, https://doi.org/10.1137/S1052623499363220) ask why the method works so well for discrete problems. Their answer is a large-deviations statement: when the feasible set is finite, the probability that the SAA problem returns a wrong answer decays exponentially in the sample size. This mission formalizes that result, Proposition 2.2 of the two-author preprint, together with its consistency companion, Proposition 2.1.

Setting

Let $\mathcal S$ be a nonempty finite set, $W$ a random element of a measurable space $\mathcal W$, and $G : \mathcal S \times \mathcal W \to \mathbb R$ such that $G(x,\cdot)$ is measurable and $\mathbb E|G(x,W)| < \infty$ for every $x \in \mathcal S$. The true problem (1.1) is

$$v^* = \min_{x \in \mathcal S} g(x), \qquad g(x) = \mathbb E\, G(x, W).$$

Let $W^1, W^2, \dots$ be an independent, identically distributed sample with the law of $W$. The sample average function and the SAA problem (2.1) are

$$\hat g_N(x) = \frac1N \sum_{n=1}^N G(x, W^n), \qquad \hat v_N = \min_{x \in \mathcal S} \hat g_N(x).$$

For $\varepsilon \ge 0$, the $\varepsilon$-optimal sets are $\mathcal S^\varepsilon = \{x \in \mathcal S : g(x) \le v^* + \varepsilon\}$ and $\hat{\mathcal S}^\varepsilon_N = \{x \in \mathcal S : \hat g_N(x) \le \hat v_N + \varepsilon\}$; at $\varepsilon = 0$ they are the optimal sets $\mathcal S^*$ and $\hat{\mathcal S}_N$. Two numbers drive the analysis: the maximal deviation $\delta_N = \max_{x \in \mathcal S}|\hat g_N(x) - g(x)|$ of (2.2), and the well-conditioning number

$$\alpha(\varepsilon) = \min_{x \in \mathcal S \setminus \mathcal S^\varepsilon} g(x) - v^* - \varepsilon$$

of (2.3), the gap between the $\varepsilon$-optimal solutions and the rest.

For a real random variable $X$ with moment generating function $M(t) = \mathbb E\, e^{tX}$ and logarithmic moment generating function $\Lambda(t) = \log M(t) \in (-\infty, +\infty]$, the rate function is $I(z) = \sup_{t \ge 0}\{tz - \Lambda(t)\}$. Assumption A requires that for every $x \in \mathcal S$ the moment generating function of $G(x, W)$ be finite in a neighbourhood of $t = 0$.

Formalization targets

Goal: Proposition 2.2

Under Assumption A, for every $\varepsilon \ge 0$ there is $\gamma > 0$ with

$$\limsup_{N \to \infty} \frac1N \log\Big[1 - P\big(\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon\big)\Big] \le -\gamma. \tag{2.5}$$

The constant $\gamma$ is not specified: it depends on $\alpha(\varepsilon)$ through rate functions and cannot be computed before the problem is solved. The goal asserts only its existence, which is the paper's claim.

Milestones

1. $\alpha(\varepsilon) > 0$ whenever $\mathcal S \setminus \mathcal S^\varepsilon \ne \emptyset$ (2.3).
2. $\delta_N < \alpha(\varepsilon)/2$ implies $\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon$.
3. The union bound $1 - P(\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon) \le \sum_{x \in \mathcal S} P\{|\hat g_N(x) - g(x)| \ge \alpha(\varepsilon)/2\}$.
4. The large-deviations upper bound (2.4): $\frac1N \log P(Z_N \ge a) \le -I(a)$ for i.i.d. averages $Z_N$.
5. $I(a) > 0$ for $a$ above the mean, when $M$ is finite near $0$.
6. Under Assumption A, $P\{|\hat g_N(x) - g(x)| \ge r\} \le e^{-N\gamma_x} + e^{-N\gamma'_x}$ with $\gamma_x, \gamma'_x > 0$.

Companions

Proposition 2.1 ($\hat v_N \to v^*$ w.p.1, and $\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon$ w.p.1 for $N$ large enough), the almost-sure convergence $\delta_N \to 0$ of (2.2), the singleton consequence ($\mathcal S^\varepsilon = \{x^*\}$ implies $\hat{\mathcal S}^\varepsilon_N = \{x^*\}$ eventually), the facts $I(\mu) = 0 = \min I$, the Example of §3.2 showing that a sample size $N > k/2$ can be required, and the computation $\alpha(0) = \min_i c_i$ on the hypercube with best value $1/k^{1/p}$ (§4).

Significance

Proposition 2.2 explains the practical behaviour of the SAA method on discrete problems: an exact optimal solution of the true problem is obtained with probability approaching one exponentially fast, so a moderate sample often suffices even when the number of feasible solutions is astronomically large. It is the basis of the paper's replication argument (§3.2: the probability of success $p(N)$ of one SAA replication tends to one exponentially fast) and identifies $\alpha(\varepsilon)$ as the quantity that governs the difficulty of a stochastic discrete problem, which the numerical study of §4 then examines. Later sample-size estimates for SAA (Shapiro, Dentcheva and Ruszczyński 2009, §5.3) refine the same argument into explicit, non-asymptotic bounds.

The result is proved in the paper. The mission produces a machine-checked proof of it and of its ingredients, including a Lean statement of the Cramér–Chernoff upper bound with the rate function $I$ in the extended reals and the positivity of $I$ above the mean under a local moment condition. To our knowledge none of these is formalized on the platform or in Mathlib in this form.

Difficulty

The argument is short on paper; the formal difficulty is in the large-deviations step. Mathlib has the Chernoff inequality $P(X \ge a) \le e^{-ta}\,\mathbb E e^{tX}$ and the factorization of moment generating functions of independent sums, but the step from there to $\frac1N \log P(Z_N \ge a) \le -I(a)$ requires passing to a supremum over $t$ in the extended reals, handling $t$ where $M(t) = \infty$, and the case $P(Z_N \ge a) = 0$. The positivity $I(a) > 0$ requires $\Lambda'(0) = \mu$, i.e. differentiating the moment generating function at an interior point of its domain. A naive attempt that works with real logarithms fails at probability zero, where $\log 0$ is not $-\infty$, and an attempt that bounds $\delta_N$ by Chebyshev's inequality gives only a polynomial rate.

Formalization scope

The feasible set is a Finset of an arbitrary type X, assumed nonempty; minima and maxima over it are Finset.inf' and Finset.sup', so they are attained. The sample is a sequence W : ℕ → Ω → 𝒲 of measurable maps on a probability space, mutually independent (iIndepFun) and identically distributed with W 0; the paper's $W^n$ is W (n - 1), and $g(x)$ is the expectation of $G(x, W^1)$. Measurability of $G(x,\cdot)$ is Borel measurability. Logarithms of probabilities are ENNReal.log, with $\log 0 = -\infty$, and the limit superior in (2.5) is taken in the extended reals; this is the paper's convention and it makes the goal correct when $\mathcal S^\varepsilon = \mathcal S$, where the event is sure. Assumption A is stated as integrability of $e^{tG(x,W)}$ for $t$ near $0$, not through the value of Mathlib's mgf, which is $0$ where the expectation is infinite. The logarithmic moment generating function is the published definition BellWilliams2001.ThresholdPolicy.logMGF (extended-real valued, $+\infty$ off the domain of $M$), and $I$ is the supremum over $t \ge 0$ only, as on p. 3. Wherever $\alpha(\varepsilon)$ appears, the nonemptiness of $\mathcal S \setminus \mathcal S^\varepsilon$ is a hypothesis; the goal does not mention $\alpha$ and needs none.

A trivializing formalization is ruled out: with Real.log the event "$\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon$ is sure" would give $\log 0 = 0$ and make the goal false, and a rate function built from mgf would count infinite moment generating functions as $\Lambda = \log 0 = 0$; neither encoding is used.

A complete development needs the Cramér–Chernoff bound for i.i.d. sums with an extended-real rate function, differentiability of the moment generating function at interior points, and the strong law of large numbers applied to finitely many functions. The large-deviations items (milestones 4 and 5, and $I(\mu) = 0$) are stated for an arbitrary i.i.d. real sequence and are reusable beyond this mission. Proofs of any item, including the optional examples, are welcome.

Selected references

• A. J. Kleywegt and A. Shapiro, The sample average approximation method for stochastic discrete optimization, preprint (two-author version), https://edoc.hu-berlin.de/server/api/core/bitstreams/2dcf2d5b-5fb9-44d1-b36a-5e378c803717/content. Published with T. Homem-de-Mello in SIAM J. Optim. 12(2):479–502, 2002. https://doi.org/10.1137/S1052623499363220
• A. Dembo and O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751

Motivation

Randomized load balancing asks how much a dispatcher gains from a little information. In the supermarket model, jobs arrive at $n$ servers and each job inspects a few servers chosen at random before joining one. With one random choice every server is an independent M/M/1 queue, and the expected time a job spends in the system is $1/(1-\lambda)$ at load $\lambda$. With two choices it is exponentially smaller as $\lambda \to 1^-$. This "power of two choices" underlies the design of distributed schedulers, hashing schemes and server farms, where querying every server is too expensive but querying two is cheap.

Timeline:

• 1994/1999. Azar, Broder, Karlin and Upfal proved the static version, balanced allocations: throwing $n$ balls into $n$ bins with $d \ge 2$ choices per ball gives a maximum load of $\log\log n/\log d + O(1)$ w.h.p., against $\Theta(\log n/\log\log n)$ for one choice (SIAM J. Comput. 1999).
• 1996. Vvedenskaya, Dobrushin and Karpelevich derived the dynamic limiting equations for $d = 2$ and showed convergence of their trajectories to the fixed point, without a rate (Problems of Information Transmission 32(1), 1996).
• 1996/2001. Mitzenmacher, independently, introduced the limiting system for general $d$, proved doubly exponential tails along every trajectory and exponential convergence to the fixed point in a weighted $L_1$ potential, and derived the limiting expected time $T_d(\lambda)$ (IEEE TPDS 2001). This mission formalizes Section 2 of that paper.

Setting

Customers arrive as a Poisson stream of rate $\lambda n$, $0<\lambda<1$, at $n$ FIFO servers. Each customer chooses $d$ servers independently and uniformly at random with replacement and joins the one holding the fewest customers; service times are exponential with mean $1$. Let $s_i(t)$ be the fraction of servers holding at least $i$ customers at time $t$.

A state is a sequence $s = (s_0, s_1, s_2, \dots)$ of reals with $s_0 = 1$, $s_i \ge 0$ and $s_0 \ge s_1 \ge s_2 \ge \cdots$. The empty state has $s_0 = 1$ and $s_i = 0$ for $i \ge 1$. As $n \to \infty$ the tails follow the limiting system

$$\frac{ds_i}{dt} = \lambda\,(s_{i-1}^d - s_i^d) - (s_i - s_{i+1}) \quad (i \ge 1), \qquad s_0 = 1. \tag{1}$$

A trajectory is a map $t \mapsto s(t)$, $t \ge 0$, whose values are states and whose coordinates satisfy (1) (from the right at $t = 0$). Throughout, $d \ge 2$ is an integer.

The fixed point is $\pi_i = \lambda^{(d^i - 1)/(d - 1)}$, so $\pi_0 = 1$, $\pi_1 = \lambda$, $\pi_2 = \lambda^{1+d}$. A customer arriving in state $s$ becomes the $i$-th customer of its queue with probability $s_{i-1}^d - s_i^d$ and then waits for $i$ services, so the expected time it spends in the system is

$$E(s) = \sum_{i=1}^{\infty} i\,(s_{i-1}^d - s_i^d).$$

The target constant is

$$T_d(\lambda) = \sum_{i=1}^{\infty} \lambda^{\frac{d^i - d}{d-1}}.$$

Formalization targets

Goal: Corollary 2

For $d \ge 2$ and $0 < \lambda < 1$, $T_d(\lambda) < \infty$, and:

$$\text{if } s_j(0) = 0 \text{ for some } j, \text{ then } E(s(t)) \xrightarrow[t\to\infty]{} T_d(\lambda);\qquad \text{if } s(0) \text{ is empty, then } E(s(t)) \le T_d(\lambda) \ \ \forall t \ge 0.$$

The hypothesis $s_j(0) = 0$ holds for every initial state that comes from a finite system.

Milestones, in the order the proof uses them

• Lemma 2. $\pi$ is the unique fixed point of (1) with $\sum_{i\ge1} s_i < \infty$.
• Theorem 2. If $s_j(0) = 0$ for some $j$, there are constants $N \ge 1$, $0<\alpha<1$, $\beta>1$, $\gamma>0$, independent of $t$, with $s_i(t) \le \gamma\,\alpha^{\beta^i}$ for all $i \ge N$, $t \ge 0$. From the empty state, $s_i(t) \le \pi_i$ for all $i$ and $t \ge 0$.
• Theorem 3. There are weights $w_i \ge 1$ such that $\Phi(t) = \sum_{i\ge1} w_i |s_i(t) - \pi_i|$ satisfies $\Phi(t) \le c_0 e^{-\delta t}$ ($\delta > 0$) whenever $\Phi(0) < \infty$, and in particular whenever $s_j(0) = 0$ for some $j$.
• Corollary 1. Under the conditions of Theorem 3 (weights $w_i \ge 1$ fixed before the trajectory, with $\Phi(0) < \infty$, or $s_j(0) = 0$ for some $j$), $\sum_{i\ge1} |s_i(t) - \pi_i| \le c_0 e^{-\delta t}$.
• Proof of Corollary 2, display. $\sum_{i\ge1} i(s_{i-1}^d - s_i^d) = \sum_{i\ge0} s_i^d$ for a state with $s_i \to 0$.
• Lemma 4. The drift of (1) is Lipschitz in $\ell^1$ on states, with constant $2 + 2d\lambda$.

Significance

The comparison $T_1(\lambda) = 1/(1-\lambda)$ against $T_d(\lambda)$ is the quantitative content of the power of two choices: the companion mission shows $T_d(\lambda)/\log T_1(\lambda) \to 1/\log d$ as $\lambda \to 1^-$, an exponential improvement. Corollary 2 is what connects that number to the dynamics: it says the fixed point's expected time is actually reached from realistic initial states, and is an upper bound from an empty start. Theorem 2's comparison argument and Theorem 3's weighted potential are reused across the mean-field analysis of load-balancing variants (threshold policies, heterogeneous servers, work stealing), so the formal statements here are templates for that literature.

All results are proved in the paper (Theorem 3's proof is written out for $d = 2$ with a remark that it extends). None has a machine-checked proof that we know of. The work is formalizing the known arguments for all $d \ge 2$, including the parts the paper delegates to a citation: quasimonotone comparison for countable ODE systems in Theorem 2, and the upper right Dini derivative handling of $|\epsilon_i|$ in Theorem 3.

Difficulty

The system is infinite-dimensional, so standard finite-dimensional ODE comparison and Lyapunov theorems do not apply as stated. Theorem 2 rests on a monotonicity property (raising the initial tails raises them for all time) that the paper justifies by a coupling intuition and a citation to a comparison theorem for quasimonotone systems; that theorem must be supplied for $\ell^\infty$-bounded countable systems. The plain $L_1$ distance is nonincreasing along trajectories but does not decay exponentially by a direct estimate; the weights $w_i$ must be built so that every coordinate's contribution to $d\Phi/dt$ is dominated by $-\delta w_i |\epsilon_i|$, while staying geometrically bounded so that $\Phi(0) < \infty$ under the doubly exponential tails of Theorem 2. Exchanging $t \to \infty$ with the infinite sum defining $E$ needs uniform tail control, which is again Theorem 2.

Formalization scope

• Namespace PowerTwoChoices.Limit; λ is lam : ℝ, $d : ℕ$ with $2 \le d$, $0 < \lambda < 1$ in every theorem.
• A state is x : ℕ → ℝ with x 0 = 1, nonnegative and antitone. A trajectory is s : ℝ → ℕ → ℝ, a state for every $t \ge 0$, with HasDerivWithinAt on Set.Ici 0 for each coordinate $i \ge 1$: right derivative at $t = 0$, two-sided for $t > 0$.
• Exponents are natural numbers: $\pi_i = \lambda^{\sum_{k<i} d^k}$, and $T_d$'s $i$-th term is $\lambda^{\sum_{1\le k<i} d^k}$.
• $\Phi$, the $L_1$ distance, $E$ and $T_d$ are sums in $[0,\infty]$, so a divergent series is $\infty$, never a default $0$. "Converges exponentially" (Definition 2) means $\Phi(t) \le c_0 e^{-\delta t}$ for all $t \ge 0$ with real $c_0$ and $\delta > 0$; $\delta$ may depend on the trajectory. The paper's $d(t)$ is renamed l1Dist.
• Time is real and $t \to \infty$ is Filter.atTop.
• Every theorem quantifies over trajectories; existence of a trajectory from a given state (Picard iteration, cited by the paper) is not part of the mission. The class is nonempty: the constant trajectory at $\pi$ is one.
• Ruled out: summing $E$ or $T_d$ as a real tsum (a divergent series would make the upper bound free and the limit attainable by a junk $0$), dropping the summability condition in Lemma 2 ($(1,1,\dots)$ is also a fixed point), choosing Theorem 3's weights after the trajectory, and stating anything for $d = 2$ only.
• Needed infrastructure: comparison principles for quasimonotone countable ODE systems, Dini-derivative Grönwall estimates, and interchange of limits and $\ell^1$ sums. All of these are reusable beyond this mission, and contributions of such lemmas as separate theorems are welcome.

Selected references

• M. Mitzenmacher, The Power of Two Choices in Randomized Load Balancing, IEEE Transactions on Parallel and Distributed Systems 12(10), 2001, pp. 1094–1104. https://doi.org/10.1109/71.963420
• Y. Azar, A. Z. Broder, A. R. Karlin, E. Upfal, Balanced Allocations, SIAM Journal on Computing 29(1), 1999, pp. 180–200. https://doi.org/10.1137/S0097539795288490
• N. D. Vvedenskaya, R. L. Dobrushin, F. I. Karpelevich, Queueing System with Selection of the Shortest of Two Queues: An Asymptotic Approach, Problems of Information Transmission 32(1), 1996, pp. 15–27.
• T. G. Kurtz, Approximation of Population Processes, SIAM, 1981. https://doi.org/10.1137/1.9781611970333

Motivation

Telephone call centers are large service systems: hundreds of agents answer callers who wait in a queue and hang up when their patience runs out. Staffing them is a trade-off between the cost of agents and the quality of service, and in large centers both the efficiency (agents busy almost all the time) and the service level (most callers answered almost immediately) can be high at once. Garnett, Mandelbaum and Reiman (M&SOM 4(3), 2002) study the simplest model that captures customer abandonment, the Erlang-A or $M/M/N+M$ queue, and derive approximations for it in the regime where the number of agents is large.

Their Theorem 2 is the process-level justification of these approximations: the queue-length process, centred at the number of agents and scaled by its square root, converges to a one-dimensional diffusion. The steady-state performance formulas of the paper (delay probability, abandonment probability, waiting times) are computed from this diffusion and its stationary law.

Timeline.

• Halfin and Whitt (1981) proved the corresponding limit for the $M/M/N$ queue without abandonment, in the regime $\sqrt N(1-\rho_N) \to \beta$ with $\beta > 0$ (Oper. Res. 29(3)). The limit is a diffusion with drift $-\mu(\beta + x)$ below $0$ and constant drift $-\mu\beta$ above.
• Fleming, Stolyar and Simon (1994) conjectured the limit with abandonment, with a slightly different centering, and proved the weak limit of the stationary distributions.
• Garnett, Mandelbaum and Reiman (2002) state the process limit for $0 < \theta < \infty$ as Theorem 2, with the extensions $\theta = 0$ and $\theta = \infty$ as Theorem 2* in Appendix C.

Setting

Fix a service rate $\mu > 0$. For each $N \ge 1$ the $N$-th system has $N$ statistically identical agents, Poisson arrivals of rate $\lambda_N > 0$, exponential service times of rate $\mu$, an unlimited waiting room served first come, first served, and exponential patience of rate $\theta_N > 0$ for every caller. A caller whose wait in queue reaches their patience abandons and does not return. The number of callers in the system, $Q_N(t)$, is a birth–death process on $\{0, 1, 2, \dots\}$ with birth rate $\lambda_N$ and death rate $\min(k, N)\mu + (k-N)^+\theta_N$ in state $k$. Its initial value $Q_N(0)$ is an arbitrary random variable.

The traffic intensity is $\rho_N = \lambda_N/(N\mu)$. The centred and scaled process is

$$q_N(t) = \frac{Q_N(t) - N}{\sqrt N}, \qquad t \ge 0 .$$

When $q_N \ge 0$ it counts waiting callers and when $q_N \le 0$ it counts idle agents, both in units of $\sqrt N$.

For $\beta \in \mathbb R$ and $\theta > 0$, the drift is the piecewise-linear function

$$f(x) = \begin{cases} -\mu(\beta + x), & x \le 0,\\ -(\mu\beta + \theta x), & x > 0,\end{cases}$$

and the limit diffusion $q$ solves $dq(t) = f(q(t))\,dt + \sqrt{2\mu}\,db(t)$, where $b$ is a standard Brownian motion independent of $q(0)$. The noise is additive, so this means: $q$ has continuous paths and $q(t) = q(0) + \int_0^t f(q(s))\,ds + \sqrt{2\mu}\,b(t)$ for all $t \ge 0$. Below $0$ it behaves like an Ornstein–Uhlenbeck process with restraining force $\mu$, above $0$ like one with restraining force $\theta$.

Formalization targets

Goal: Theorem 2 (p. 216)

Assume

$$\lim_{N\to\infty}\sqrt N(1-\rho_N) = \beta \in (-\infty,\infty), \qquad \lim_{N\to\infty}\theta_N = \theta \in (0,\infty),$$

and $q_N(0) \Rightarrow \nu$ for a probability law $\nu$ on $\mathbb R$. Then

$$q_N \Rightarrow q \quad\text{in } D[0,\infty),$$

where $q$ is the solution of $dq = f(q)\,dt + \sqrt{2\mu}\,db$ with $q(0) \sim \nu$, and this solution is unique in law.

Milestone: the limit equation is well posed (Theorem 2, p. 216)

On every probability space with a standard Brownian motion $b$ and an independent initial value $X_0$, the equation has a solution adapted to $\sigma(X_0, b(s): s \le t)$, and any two solutions with the same $b$ and initial value are indistinguishable.

Milestone: infinitesimal moments (Appendix C, p. 224)

The infinitesimal expectation $\mu_N(x)$ and variance $\sigma_N^2(x)$ of $q_N$ at the point $x$, as displayed on p. 224, satisfy

$$\lim_{N\to\infty}\mu_N(x) = f(x), \qquad \lim_{N\to\infty}\sigma_N^2(x) = 2\mu \qquad (x \in \mathbb R).$$

Significance

The result. Theorem 2 is the basis for the paper's QED (quality- and efficiency-driven) approximations $Q_N \approx N + q\sqrt N$, which give explicit formulas for the probability of delay, the probability of abandonment and the waiting-time distribution in terms of $\beta$, $\mu$ and $\theta$. Unlike the $M/M/N$ case, $\beta$ may be of either sign: abandonment keeps the system stable even when the offered load exceeds the number of agents. The resulting square-root staffing rule $N = R + \beta\sqrt R$, with $R = \lambda/\mu$, is used in call-center practice.

Formalizing it. The result is proved in the paper by Stone's criteria for birth–death processes, with uniqueness of the limit equation delegated to the literature. No many-server process limit exists on Prove2Me or in Mathlib. A formal proof would give the first machine-checked heavy-traffic process limit for a many-server queue, and the infrastructure (Poisson time-change representation of a birth–death process, path-space weak convergence to a continuous diffusion, well-posedness of a Lipschitz additive-noise SDE) would serve every other diffusion limit in queueing theory.

Difficulty

The infinitesimal-moment computation is elementary; it identifies the limit but does not prove convergence. The hard step is the passage from generator convergence to weak convergence of processes on $D[0,\infty)$: tightness of $\{q_N\}$ in the Skorokhod space, which needs control of the jumps (of size $1/\sqrt N$) and of the unbounded state space, and identification of every limit point as a solution of the equation, which needs uniqueness of the limit. A pointwise limit of the drifts at each fixed $x$ is not enough: the convergence has to be controlled locally uniformly along the paths. A finite-dimensional limit at fixed times is weaker than the theorem.

Formalization scope

• Queue. $Q_N$ is realized by the time-change representation of Mandelbaum, Massey and Reiman (1998), cited by the paper: $Q_N(t) = Q_N(0) + A(\lambda_N t) - S(\mu\int_0^t \min(Q_N(s), N)\,ds) - R(\theta_N \int_0^t (Q_N(s)-N)^+\,ds)$, with $A, S, R$ independent unit-rate Poisson processes independent of $Q_N(0)$. This has the birth–death law above.
• Time. Paths are functions on $\mathbb R$; every condition is imposed for $t \ge 0$ only. Brownian time is $\mathbb R_{\ge 0}$.
• Indexing. $N$ is both the index and the number of agents; every hypothesis on the $N$-th system is imposed for $N \ge 1$. $\lambda_N$, $\theta_N$ are real sequences and $\mu$ is fixed.
• Weak convergence. All $Q_N$ live on one probability space, which is no loss since only their laws matter. $q_N(0) \Rightarrow \nu$ is convergence of $E\,g(q_N(0))$ for every bounded continuous $g$. $q_N \Rightarrow q$ is stated in coupling form (Skorokhod representation with almost-sure uniform convergence on compact time intervals), which is equivalent to $J_1$ weak convergence when the limit is continuous.
• Limit. The SDE is pathwise (Lebesgue integral, no Itô integral). Brownian motion is Mathlib's IsBrownianReal with every path continuous and every coordinate measurable. $q(0)$ is independent of $b$, which is implicit in the paper. The goal asserts existence of a solution with $q_N \Rightarrow q$ and uniqueness of its law; dropping the uniqueness clause, fixing $\nu$ to a point mass, restricting to $\beta > 0$, $\mu = 1$, $\theta = \mu$, or the stationary case is a different theorem.
• Infinitesimal moments. Defined exactly as displayed, with $\lfloor\cdot\rfloor$ the integer part. The display is printed for $\theta = 0$; the milestone is its $0 < \theta < \infty$ instance with the limit $f$ of Theorem 2, pointwise in $x$.
• Not covered. The cases $\theta = 0$ and $\theta = \infty$ of Theorem 2* and the interchange of limits (Part 2).

Contributions welcome: a Poisson time-change existence theorem, tightness criteria in $D[0,\infty)$, well-posedness of Lipschitz SDEs with additive noise, and the martingale-problem approach to identifying limits.

Selected references

• O. Garnett, A. Mandelbaum, M. Reiman, Designing a Call Center with Impatient Customers, Manufacturing & Service Operations Management 4(3):208–227, 2002. https://doi.org/10.1287/msom.4.3.208.7753
• S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• P. J. Fleming, A. Stolyar, B. Simon, Heavy Traffic Limit for a Mobile Phone System Loss Model, Proc. 2nd Int. Conf. on Telecommunication Systems Modeling and Analysis, 1994.
• A. Mandelbaum, W. A. Massey, M. I. Reiman, Strong Approximations for Markovian Service Networks, Queueing Systems 30:149–201, 1998. https://doi.org/10.1023/A:1019112920622
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658

Motivation

A correlated equilibrium (Aumann 1974) is a probability distribution over strategy profiles of a game such that no player gains by deviating from a recommended strategy, given the recommendation. It is the solution concept of choice when players can condition on common signals, and its set is a convex polytope defined by linear inequalities, which makes it computationally tractable in a way that Nash equilibrium is not. A natural question in learning in games is whether simple adaptive behaviour by individual players, each using only their own payoffs and the observed history, leads to it.

Hart and Mas-Colell (2000) answer this with regret matching: each player switches away from their last action with probabilities proportional to the regret for not having played other actions in the past. They show that if every player uses this rule, the empirical distribution of play converges almost surely to the set of correlated equilibria. The procedure and its analysis became standard references for no-regret learning, internal (swap) regret, and the counterfactual-regret-minimization algorithms used in large imperfect-information games.

Timeline. Foster and Vohra (1997) obtained convergence to correlated equilibria by calibrated forecasting. Fudenberg and Levine (1999) gave conditionally consistent procedures with the same consequence. Hart and Mas-Colell (2000) gave the regret-matching procedure (2.2), in which a player's probabilities depend on regrets only, together with a Blackwell-approachability variant (their Theorem A, the subject of the companion mission 2 of this series).

Setting

A finite game $\Gamma=(N,(S^i)_{i\in N},(u^i)_{i\in N})$ has a finite set of players $N$, a finite strategy set $S^i$ for each player, and payoffs $u^i:S\to\mathbb R$ on $S=\prod_i S^i$. A probability distribution $\psi$ on $S$ is a correlated $\varepsilon$-equilibrium if for every player $i$ and all $j,k\in S^i$

$$\sum_{s:\,s^i=j}\psi(s)\,[u^i(k,s^{-i})-u^i(s)]\le\varepsilon ;$$

a correlated equilibrium is the case $\varepsilon=0$.

The game is played at $t=1,2,\dots$, producing a history $h_t=(s_1,\dots,s_t)$. For $j,k\in S^i$ the regret of player $i$ is

$$D^i_t(j,k)=\frac1t\sum_{\tau\le t:\,s^i_\tau=j}[u^i(k,s^{-i}_\tau)-u^i(s_\tau)],\qquad R^i_t(j,k)=\max\{D^i_t(j,k),0\}:$$

the average gain player $i$ would have had by playing $k$ every time they played $j$. Fix $\mu$ with $\mu>2M^i(m^i-1)$ for every $i$, where $M^i\ge|u^i|$ and $m^i=|S^i|$. Under regret matching (2.2), if player $i$ last played $j$, then at $t+1$ they play each $k\ne j$ with probability $R^i_t(j,k)/\mu$ and repeat $j$ with the remaining probability; the first-period mixed actions are arbitrary, and given the history the players randomize independently. The empirical distribution of play is $z_t(s)=\frac1t|\{\tau\le t:s_\tau=s\}|$.

Formalization targets

Goal: the Main Theorem

Almost surely, $z_t$ converges to the set of correlated equilibria:

$$P\Big(\forall\varepsilon>0\ \exists T\ \forall t>T\ \exists\psi\ \text{correlated equilibrium with } \operatorname{dist}(z_t,\psi)<\varepsilon\Big)=1 .$$

This is convergence to a set, not to a point; the paper notes that $z_t$ need not converge.

Milestones

They follow the Appendix proof:

• the PROPOSITION (§3), a deterministic equivalence: $\limsup_t R^i_t(j,k)\le\varepsilon$ for all $i$ and $j\ne k$ iff $z_t$ converges to the set of correlated $\varepsilon$-equilibria;
• positivity of the diagonal of the transition matrix $\Pi_t$ of (2.2);
• Steps M1–M11, with the two LEMMAs used in the proofs of M4 and M7.

The squared distance $\rho_t=\sum_{j\ne k}[R_t(j,k)]^2$ satisfies a block recursion (M1). The cross term is rewritten through the transition probabilities (M2) and compared with a stationary auxiliary process (M3–M5). It then factors into a difference of consecutive matrix powers (M6), which is small (M7). This gives

$$E[(t+v)^2\rho_{t+v}\mid h_t]\le t^2\rho_t+O(v^3+tv^{1/2})\qquad\text{(M8)}.$$

Along $t_n=\lfloor n^{5/3}\rfloor$ this gives $\rho_{t_n}\to0$ a.s. (M9–M10), and then $R_t(j,k)\to0$ a.s. (M11). A companion item states the strong law for dependent variables that M10 cites.

Significance

The result. The Main Theorem shows that correlated equilibrium is reached by uncoupled play: each player needs only their own payoff function and the history of play, and nothing about the others' payoffs. Steps M10–M11 give more than the goal, namely that every player's internal regrets vanish almost surely. The procedure underlies later work on swap regret, calibrated learning and regret-minimization algorithms for extensive-form games.

Formalizing it. The result is proved in the paper. As far as a search of the platform and the local index shows, it has no machine-checked proof. The mission asks for one, following the paper's eleven steps. Several pieces are general and reusable: a bound on consecutive powers of a stochastic matrix with positive diagonal (LEMMA, proof of M7); a perturbation bound for multi-step transition probabilities (LEMMA, proof of M4); and a strong law of large numbers for martingale differences with general normalizing sequences, which Mathlib does not have in this form.

Difficulty

The natural approach is Blackwell approachability: show that the expected regret vector moves toward the nonpositive orthant in one step. It fails here. The one-step condition holds when a player uses an invariant distribution of $\Pi_t$, which is the procedure of Theorem A, but regret matching uses a row of $\Pi_t$ instead. The cross term of the one-step recursion therefore does not vanish.

The proof has to work over blocks of $v$ periods. Within a block the players' choices are not independent given $h_t$, because the transition probabilities change with time. The paper therefore compares the play with a process whose transitions are frozen at time $t$. The matrix-power estimate cannot use convergence of $\Pi_t^w$, since only the diagonal of $\Pi_t$ is known to be positive and $\Pi_t$ may be reducible or periodic in its off-diagonal structure. The block length must also balance the errors $w^2/t$ and $w^{-1/2}$, which is why the subsequence $t_n=\lfloor n^{5/3}\rfloor$ appears.

Formalization scope

Players form a Fintype ι, strategies form Fintypes S i, each nonempty, and a profile is a function ∀ i, S i. $\Delta(Q)$ is Mathlib's stdSimplex. Time is 0-based: play τ is $s_{\tau+1}$, and a history is a tuple Fin t → ∀ i, S i. Regrets, $z_t$, $\Pi_t$ and $\rho_t$ are deterministic functions of a finite history. Every statement has $t\ge1$, because the Lean value at $t=0$ is a default. A play of a behaviour profile on a probability space (IsPlay) is a sequence of profile-valued random variables with measurable level sets whose conditional law given any history of positive probability is the product of the players' mixed actions. Statements quantify over every probability space carrying a play, and conditional quantities given $h_t$ assume $P[h_t]>0$. The auxiliary $\hat s$-process is encoded by its explicit law, a power of the product transition matrix. The paper's $O(\cdot)$ (footnote 34) is a constant chosen after the game, $M$ and $\mu$ and before the initial play, the probability space and the play. Distances on $\mathbb R^S$ are sup distances.

The hypotheses are exactly footnote 5's: $|u^i|\le M^i$ and $\mu>2M^i(m^i-1)$, with one $\mu$ for all players. The goal requires every player to follow (2.2). If other players may play arbitrarily the statement is false (§4(d)), so IsPlay constrains all of them. The goal is stated with an existential correlated equilibrium at distance less than $\varepsilon$, not with a distance to a possibly empty set, so no encoding makes it vacuous.

Disclosed choices:

• the LEMMA of M7 is stated with a constant that depends only on a lower bound on the diagonal, which is what the proof gives and what M7 uses;
• the PROPOSITION states $\limsup\le\varepsilon$ as "for every $\delta>0$, eventually $\le\varepsilon+\delta$";
• the strong law assumes each $X_n$ is measurable and in $L^2$.

Contributions are welcome at every milestone. The two LEMMAs and the strong law are self-contained and independent of the game.

Selected references

• S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68(5) (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153
• R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• D. P. Foster and R. V. Vohra, Calibrated Learning and Correlated Equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
• D. Fudenberg and D. K. Levine, Conditional Universal Consistency, Games and Economic Behavior 29 (1999), 104–130. https://doi.org/10.1006/game.1998.0705
• D. Blackwell, An Analog of the Minimax Theorem for Vector Payoffs, Pacific Journal of Mathematics 6 (1956), 1–8. https://doi.org/10.2140/pjm.1956.6.1
• M. Loève, Probability Theory II, 4th ed., Springer (1978), Theorem 32.1.E.