Completed

Markov Chain Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times VIII: Path Coupling and Approximate CountingTextbook

Motivation

The coupling method of Mission III asks for a coupling of two copies of a chain from every pair of starting states — often painful to construct globally. Chapter 14 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) replaces that global demand by a local one. The path coupling technique of Bubley and Dyer says: put a connected graph structure on the state space, and couple one step of the chain only across edges; if each edge contracts in expectation, contraction propagates automatically along paths to arbitrary pairs of distributions. The bookkeeping runs through the transportation metric (Kantorovich distance) between distributions, whose theory — attainment by an optimal coupling, the triangle inequality — is developed on the way. The chapter's payoff is the sharpest elementary bound for sampling proper colorings (Theorem 14.8: the Glauber dynamics mixes in $O(n\log n)$ steps once $q>2\Delta$ ), and, through the sampling-to-counting reduction of Jerrum–Valiant–Vazirani, a polynomial-time approximation algorithm for counting colorings — the paradigm of the Markov chain Monte Carlo method as an algorithmic tool.

Setting

All chains live on a finite state space $V$ with a transition matrix $P$ ; $P^t(x,\cdot)$ is the time- $t$ distribution from $x$ , $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$ the total variation distance, $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$ the worst-case distance to the stationary distribution $\pi$ , and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$ the mixing time. A coupling of distributions $\mu,\nu$ is a distribution $q$ on $V\times V$ with marginals $\mu$ and $\nu$ .

Given a metric-like cost $\rho$ on pairs of states, the transportation metric between two distributions is the cheapest expected cost of moving one onto the other:

\rho_K(\mu,\nu)=\min\Bigl\{\sum_{x,y}\rho(x,y)\,q(x,y)\;:\;q\ \text{a coupling of}\ \mu,\nu\Bigr\}.

Given a connected graph structure $G$ on the state space with edge lengths $\ell\ge1$ , the path metric $\rho(x,y)$ is the least total length of a $G$ -path from $x$ to $y$ .

For the colorings application: a $q$ -coloring of the vertices of a graph is proper when adjacent vertices receive distinct colors, and the Glauber dynamics on proper colorings picks a uniform vertex and re-samples its color uniformly among the colors legal there; its stationary distribution is uniform on the proper colorings. Throughout, $n$ is the number of vertices and $\Delta$ the maximum degree of the graph being colored.

Formalization targets

Goal

Theorem 14.8, the capstone of Chapter 14: for the Glauber dynamics on proper $q$ -colorings, if $q>2\Delta$ then

t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl\lceil\frac{q-\Delta}{q-2\Delta}\;n\,\bigl(\log n-\log\varepsilon\bigr)\Bigr\rceil.

Milestones

Lemma 14.3 and Remark 14.2 — the transportation distance is attained by an optimal coupling, and satisfies the triangle inequality (so it is a genuine metric on distributions).
Theorem 14.6, path coupling (Bubley–Dyer) — if for every edge $\{x,y\}$ of a connected graph structure there is a coupling of the one-step distributions $P(x,\cdot),P(y,\cdot)$ contracting the path metric by $e^{-\alpha}$ in expectation, then one step of the chain contracts the transportation metric of arbitrary distribution pairs by $e^{-\alpha}$ .
Corollary 14.7 — under the same hypotheses, $d(t)\le e^{-\alpha t}\,\mathrm{diam}(V)$ and $t_{\mathrm{mix}}(\varepsilon)\le\lceil(\log\mathrm{diam}(V)-\log\varepsilon)/\alpha\rceil$ , where $\mathrm{diam}(V)$ is the largest path-metric distance between two states.
Theorem 14.12, approximate counting — for $q>2\Delta$ there is a randomized estimator, computed from an explicit polynomial number of independent uniform random seeds, which with probability at least $1-\eta$ estimates the number of proper $q$ -colorings within a $(1\pm\varepsilon)$ factor: rapid sampling yields rapid approximate counting.

Significance

The results. Path coupling converted the coupling method from an art into a calculus: one bounds a single-edge contraction constant, and the machinery does the rest. It is the standard tool for Glauber dynamics on colorings, independent sets, and other constraint-satisfaction models, and the $q>2\Delta$ colorings bound is its flagship application. Theorem 14.12 is the discrete embodiment of the Jerrum–Valiant–Vazirani equivalence between approximate counting and sampling — the conceptual foundation of the entire MCMC approach to $\#\mathrm P$ -hard counting problems.

Formalizing them. Mathlib has no transportation/Kantorovich metric in the finite setting, no path coupling, and nothing on approximate counting. The transportation-metric layer (optimal couplings, triangle inequality) is reusable far beyond this mission — it is the finite Wasserstein distance. The path-coupling theorem feeds directly into Mission IX (Ising) and is quoted throughout modern mixing literature.

Difficulty

The transportation metric asks for minimization over the (compact) polytope of couplings: attainment is a finite-dimensional compactness argument, and the triangle inequality requires gluing two optimal couplings along their common marginal — the classic construction that must be carried out with explicit finite sums here. Path coupling itself is an induction along geodesics of the path metric, with the subtlety that the composite coupling produced along a path need not be optimal, only admissible; the bookkeeping of the contraction constant through the induction is exactly the kind of argument Lean keeps honest. Theorem 14.8 instantiates the machinery: the single-edge coupling for colorings needs a careful case analysis of the proposed recolorings at the two endpoints (matching legal colors bijectively), and the contraction constant $(q-2\Delta)/(q-\Delta)$ emerges from counting disagreeing proposals. Theorem 14.12 layers a probabilistic-amplification argument (medians of means over independent runs) on top of the mixing bound; its combinatorial core — expressing $|\Omega|^{-1}$ as a telescoping product of marginal probabilities — is elementary but notation-heavy, and the formal statement quantifies over explicit seed spaces, so the whole estimator is a finite object.

Formalization scope

The transportation metric is an sInf over coupling costs (the coupling polytope is nonempty for genuine distributions, and attainment is part of the milestone, so the junk value never propagates); the path metric is an sInf over walk lengths in a connected graph. The Glauber dynamics on colorings is the restriction to proper colorings of the single-site heat-bath chain of Mission II, matching §3.3 of the book; its state space is the subtype of proper colorings, nonempty whenever $q>2\Delta$ (a fact the hypotheses of the goal supply). Mixing-time upper bounds are stated with the book's explicit ceilings, so no rounding slack is hidden. In Theorem 14.12 the estimator is presented concretely as a function of finitely many uniform seeds, and "with probability $\ge1-\eta$ " is a counting inequality over the seed space — no measure theory enters. Contributions of intermediate lemmas (optimal-coupling gluing, geodesic decompositions, colorings edge-coupling) are welcome and will be reused by Mission IX.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
R. Bubley, M. Dyer, Path coupling: a technique for proving rapid mixing in Markov chains, FOCS 1997. https://doi.org/10.1109/SFCS.1997.646111
M. Jerrum, A very simple algorithm for estimating the number of k-colorings of a low-degree graph, Random Structures Algorithms 7 (1995). https://doi.org/10.1002/rsa.3240070205
M. Jerrum, L. Valiant, V. Vazirani, Random generation of combinatorial structures from a uniform distribution, Theoret. Comput. Sci. 43 (1986). https://doi.org/10.1016/0304-3975(86)90174-X

9 thms4 active usersReviewed

Completed

Markov Chain Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times VI: Networks, Hitting Times, and Cover TimesTextbook

Motivation

A reversible Markov chain is an electrical network: states are nodes, and the conductance $c(x,y)=\pi(x)P(x,y)$ turns hitting probabilities into voltages and hitting times into resistances. This dictionary, going back to Kakutani and popularized by Doyle and Snell, converts probabilistic estimates into the physical laws of circuits — series/parallel reduction, energy minimization, monotonicity under edge removal. Chapters 9–11 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop the dictionary and its two crown results: the commute time identity of Chandra–Raghavan–Ruzzo–Smolensky–Tiwari, $\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)=c_G\,R(a\leftrightarrow b)$ , and the Matthews method bounding cover times by hitting times with harmonic-number precision.

Setting

A network is a symmetric nonnegative conductance function $c$ on pairs of vertices; the associated walk moves with probabilities

P(x,y)=c(x,y)/c(x)

where $c(x)=\sum_y c(x,y)$ , and $c_G=\sum_x c(x)$ . A function $h$ is harmonic at $x$ if $h(x)=\sum_y P(x,y)h(y)$ . The voltage with boundary values $1$ at $a$ and $0$ at $z$ is $W(x)=\mathbb P_x\{\tau_a<\tau_z\}$ , the harmonic extension of its boundary data; the current flowing out of $a$ has strength $\|I\|=\sum_y c(a,y)\,[W(a)-W(y)]$ , and the effective resistance is $R(a\leftrightarrow z)=\|I\|^{-1}$ . A flow from $a$ to $z$ is an antisymmetric edge function obeying the node law off $\{a,z\}$ ; its energy is $\mathcal E(\theta)=\sum_e\theta(e)^2/c(e)$ . Hitting times $\tau_S=\min\{t\ge0:X_t\in S\}$ , their expectations, the Green's function $G_{\tau_z}(a,x)$ , the maximal hitting time $t_{\mathrm{hit}}$ , and the cover time $t_{\mathrm{cov}}$ (expected time to visit every state, maximized over starts) all use the trajectory calculus of Mission I.

Formalization targets

Goal

\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)\;=\;c_G\,R(a\leftrightarrow b).

This is Proposition 10.6, the commute time identity — the exact bridge between the probabilistic and electrical sides, and the engine of the transience/recurrence theory of Mission XII.

Milestones

Reversibility and stationarity of the network walk with $\pi(x)=c(x)/c_G$ (§9.1); Proposition 9.1 (existence and uniqueness of harmonic extensions with given boundary values, $h(x)=\mathbb E_x f(X_{\tau_B})$ ); Lemma 9.6 (the Green's function identity $G_{\tau_z}(a,a)=c(a)R(a\leftrightarrow z)$ ); Theorem 9.10 (Thomson's principle: $R(a\leftrightarrow z)$ is the minimal energy of a unit flow, attained); Theorem 9.12 (Rayleigh monotonicity: lowering conductances raises effective resistance); Lemma 10.1 (the random target lemma: $\sum_y\mathbb E_a(\tau_y)\pi(y)$ does not depend on $a$ ); Corollary 10.8 (the resistance triangle inequality); Theorem 11.2 (Matthews: $t_{\mathrm{cov}}\le t_{\mathrm{hit}}\,(1+\tfrac12+\dots+\tfrac1n)$ ); Proposition 11.4 (the matching Matthews lower bound over subsets).

Significance

The results. The commute time identity computes hitting times from circuit reductions — this is how hitting times on trees, tori and glued graphs are actually evaluated — and, through Thomson and Rayleigh, makes them monotone under graph operations, something invisible probabilistically. The Matthews bounds pin cover times up to a $\log n$ factor in complete generality; they are the tool behind cover-time results for lamplighter groups in Mission XI's sequel. Green's function identities feed Mission XII's recurrence theory, where $R(a\leftrightarrow\infty)$ decides transience.

Formalizing them. Mathlib has graph Laplacians but no electrical network theory: no effective resistance, no flows, no energy, no Thomson/Rayleigh, no hitting or cover times. This mission publishes that layer over the trajectory calculus of Mission I. It is the most reusable single block of the series outside Missions I–II: effective resistance on finite networks is of independent interest to combinatorics (spanning trees, spectral sparsification) well beyond mixing times.

Difficulty

The identity chain behind the goal runs: Green's function of the stopped walk $\to$ escape probability $\mathbb P_a\{\tau_z<\tau_a^+\}=\bigl(c(a)R(a\leftrightarrow z)\bigr)^{-1}$ (via harmonic uniqueness) $\to$ the Aldous–Fill occupation identity $G_\tau(a,x)=\mathbb E_a(\tau)\pi(x)$ for stopping times with $X_\tau=a$ — each step is a manipulation of infinite series of trajectory sums whose exchange steps (splitting a path at its first visit, last-exit decompositions) need summability from Mission I's Lemma 1.13. Thomson's principle is a finite-dimensional convex minimization: existence of the minimizer needs a compactness or completing-the-square argument, and the identification of the minimizer with the current flow needs the cycle law; the naive "differentiate the energy" route must be made exact. Matthews' method is a clean but genuinely clever argument — a uniformly random ordering of targets and the harmonic-number telescoping; the formal cost is the exchangeability of the randomized order against the chain, handled combinatorially.

Formalization scope

Networks are functions $c:V\times V\to\mathbb R$ with a symmetry-and-nonnegativity predicate; loops are permitted; connectivity enters as irreducibility of the induced walk. The voltage is defined probabilistically as $\mathbb P_x\{\tau_a<\tau_z\}$ (the book's harmonic characterization is Proposition 9.1); $R(a\leftrightarrow z)$ is the reciprocal of the explicit current strength, with total division junk when $a,z$ are disconnected — statements carry irreducibility so this does not arise. Energy counts each undirected edge once, formalized as half the ordered double sum, and $0^2/0=0$ handles absent edges. Cover times are tail sums of the explicit event "some state unvisited". The Matthews lower bound is stated with an arbitrary lower bound $m$ for the pairwise hitting times of the subset $A$ — equivalent to the book's min over pairs and easier to instantiate.

Welcome contributions: series/parallel reduction laws, the cycle and node law API for flows, escape-probability lemmas — all reused in Mission XII's infinite-network arguments.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
P. G. Doyle, J. L. Snell, Random Walks and Electric Networks, MAA, 1984. https://arxiv.org/abs/math/0001057
A. K. Chandra, P. Raghavan, W. L. Ruzzo, R. Smolensky, P. Tiwari, The electrical resistance of a graph captures its commute and cover times, STOC 1989. https://doi.org/10.1145/73007.73062
P. Matthews, Covering problems for Markov chains, Ann. Probab. 16 (1988). https://doi.org/10.1214/aop/1176991894

15 thms4 active usersReviewed

Completed

Experimental Design Operations Research Reinforcement Learning+1·Captain: Shuze Chen

Treatment Locality in A/B TestingResearch Paper

Modern A/B tests must infer lifetime treatment effects — e.g. customer lifetime value under a new feature — from short-horizon experiment data. Chen, Simchi-Levi and Wang (arXiv:2407.19618) model the experiment as a Markov decision process and exploit a structural fact of many practical interventions: the treatment is local, modifying the system at a single crucial state only. This mission formalizes the core asymptotic theory of the paper: for any differentiable estimator built from the experiment's transition and reward statistics, information sharing — pooling across test arms the samples collected away from the treated state — keeps the estimator asymptotically normal with the same asymptotic bias and never increases its asymptotic variance (Theorem 9), and is asymptotically efficient among unbiased estimators (Theorem 5). The route runs through a Markov chain central limit theorem with the asymptotic variance identified as the autocovariance series, and the linearization/delta method for functionals of chain statistics.

42 thms4 active users

Completed

Markov Chain Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary DistributionTextbook

Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary Distribution

Motivation

Finite Markov chains are the basic model for memoryless random dynamics: card shuffles, random walks on graphs and groups, Monte Carlo samplers, and queueing systems are all chains on a finite state space. The single most used fact about them is that an irreducible chain has exactly one stationary distribution — a probability vector $\pi$ with $\pi = \pi P$ — and that this $\pi$ is strictly positive and encodes the long-run behaviour of the chain through the return-time identity $\pi(x) = 1/\mathbb{E}_x(\tau_x^+)$ . Every later result in the theory of mixing times (convergence theorems, coupling bounds, spectral methods, cutoff) is a statement about the distance of the chain from this $\pi$ , so nothing in the subject can be formalized before this mission is.

This mission is the first in a series formalizing D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times (AMS, 2009), covering Chapters 1–2: the basic vocabulary of finite chains (stochastic matrices, irreducibility, period, reversibility, time reversal, random walks on graphs and groups) and the classical examples of Chapter 2 (gambler's ruin, coupon collecting, the reflection principle for simple random walk on $\mathbb{Z}$ ). Later missions in the series build on the definitions published here.

Setting

A chain on a finite state space $\Omega$ is presented by its transition matrix, a matrix $P \in \mathbb{R}^{\Omega\times\Omega}$ with nonnegative entries whose rows sum to $1$ . A distribution is a row vector $\mu$ with nonnegative entries summing to $1$ ; one step of the chain carries $\mu$ to $\mu P$ , and the $t$ -step transition probabilities are the entries of the matrix power $P^t$ .

The chain is irreducible if for all states $x, y$ there is a $t$ with $P^t(x,y) > 0$ . The period of a state $x$ is $\gcd\,\mathcal{T}(x)$ where $\mathcal{T}(x) = \{t \ge 1 : P^t(x,x) > 0\}$ , and the chain is aperiodic if every state has period $1$ . A distribution $\pi$ is stationary if $\pi P = \pi$ , and $\pi$ and $P$ are in detailed balance (the chain is reversible) if $\pi(x)P(x,y) = \pi(y)P(y,x)$ for all $x,y$ .

Trajectory events over a finite horizon are finite sums of path weights: a length- $t$ trajectory is a function $\omega : \{0,\dots,t\} \to \Omega$ , with weight $\prod_{i<t} P(\omega_i, \omega_{i+1})$ conditional on its starting state. The tail probability $\mathbb{P}_x\{\tau_z^+ > t\}$ of the first hitting time $\tau_z^+ = \min\{t \ge 1 : X_t = z\}$ is the sum of the weights of the trajectories from $x$ that avoid $z$ at times $1,\dots,t$ , and expectations of hitting times are recovered by the tail-sum formula $\mathbb{E}(Y) = \sum_{t\ge0} \mathbb{P}\{Y > t\}$ , formalized as a tsum over $t$ .

Formalization targets

Goal

$\text{$P$ stochastic and irreducible on a finite nonempty $\Omega$} \;\Longrightarrow\; \exists!\, \pi,\ \pi = \pi P .$

This is Corollary 1.17 of the book. It asserts only existence and uniqueness, leaving the finer structure of $\pi$ to the milestones; it is the weakest statement on which the rest of the series can stand, which is why it is the goal.

Milestones toward and around the goal

The milestone list follows the book's own route: well-definedness of the period (Lemma 1.6), positivity of some matrix power for irreducible aperiodic chains (Proposition 1.7), finiteness of expected hitting times (Lemma 1.13), existence of a positive stationary distribution together with

\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1

(Proposition 1.14), constancy of harmonic functions (Lemma 1.16), stationarity from detailed balance (Proposition 1.19), the stationary and reversible measure $\pi(x) = \deg(x)/2|E|$ of simple random walk on a graph (Examples 1.12 and 1.20), the time reversal $\hat P$ and its path-reversal identity (Proposition 1.22), and the random walks on finite groups of Section 2.6 (Propositions 2.12–2.14). From Chapter 2 the list adds the gambler's ruin formulas $\mathbb{P}_k\{X_\tau = n\} = k/n$ and $\mathbb{E}_k(\tau) = k(n-k)$ (Proposition 2.1), the coupon collector expectation $n\sum_{k\le n} 1/k$ and tail bound $e^{-c}$ (Propositions 2.3 and 2.4), and the reflection principle and the bound $\mathbb{P}_k\{\tau_0 > r\} \le 12k/\sqrt{r}$ for simple random walk on $\mathbb{Z}$ (Lemma 2.18 and Theorem 2.17).

Significance

The result itself. Existence and uniqueness of $\pi$ is the pivot on which the entire quantitative theory turns: it defines the target of convergence, and the identity $\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1$ ties the stationary measure to return times, which later missions use for hitting-time and cover-time results. Detailed balance is the practical tool by which stationary measures of graph and group walks are computed, and the Chapter 2 examples (gambler's ruin, coupon collecting, reflection) are the standard building blocks reused throughout the book — the coupon collector bound, for instance, is exactly the estimate behind the $n \log n + cn$ analysis of the top-to-random shuffle in a later mission of this series.

Formalizing it. Mathlib currently has no theory of finite Markov chains: no stochastic-matrix predicate, no stationary distribution, no periodicity, no hitting times. Everything proved in this mission is new formal mathematics, and the definition layer published here (mm_basic, mm_path, mm_classical) is the shared foundation that all twelve subsequent missions of the series import. All results are classical and have textbook proofs; none has a machine-checked proof.

Difficulty

The delicate point is the existence proof. The natural first idea — extract $\pi$ from an eigenvector of $P^{\mathsf T}$ for eigenvalue $1$ , or invoke a fixed-point theorem — either does not give positivity and nonnegativity without further work, or uses compactness machinery (Brouwer) that is unavailable. The book's proof instead builds $\tilde\pi(y) = \mathbb{E}_z(\text{visits to } y \text{ before } \tau_z^+)$ and verifies $\tilde\pi P = \tilde\pi$ by reindexing trajectory sums; formalizing it requires managing infinite series of path sums (summability from the geometric tail bound of Lemma 1.13, exchanging tsum with finite sums, splitting a trajectory at its last step). The uniqueness half is linear algebra via constancy of harmonic functions (Lemma 1.16), which is elementary but requires a maximum-principle argument over a finite state space. The reflection principle and Theorem 2.17 are finite combinatorics on $\pm 1$ paths — the bijection is easy to describe and fiddly to implement.

Formalization scope

States form a Fintype with decidable equality; chains are Matrix V V ℝ with the row-stochasticity predicate IsStochastic; distributions are functions V → ℝ with the predicate IsDist. Everything is distribution-side: no probability space or measure theory is used. The period is formalized as $\sup\{d : d \mid t \text{ for all } t \in \mathcal{T}(x)\}$ , which equals $\gcd \mathcal{T}(x)$ when $\mathcal{T}(x) \neq \varnothing$ and takes the junk value $0$ otherwise. Expectations of hitting times are tsums of tail probabilities, with the usual junk value $0$ for non-summable families — the statements are arranged (e.g. multiplicatively, $\pi(x)\cdot\mathbb{E}_x(\tau_x^+) = 1$ ) so that junk values cannot make them vacuously true. Existence statements carry a Nonempty V hypothesis; irreducibility on the empty space is vacuous, and without nonemptiness the goal would be false, not trivial. The coupon collector and the walk on $\mathbb{Z}$ are presented directly by their driving randomness (uniform draws Fin t → Fin n, uniform sign strings Fin r → Bool), so those probabilities are elementary counting; in particular the reflection principle is stated as an equality of cardinalities of sets of sign strings — this is equivalent to the probabilistic statement because all $2^r$ strings are equally likely.

Contributions welcome beyond the milestone list: simp lemmas for the definition layer, the taboo-matrix representation of avoidance probabilities (useful for Lemma 1.13), and any interface lemmas connecting pathWeight sums to matrix powers — these will be reused by every later mission in the series.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
J. R. Norris, Markov Chains, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9780511810633
D. Aldous, J. A. Fill, Reversible Markov Chains and Random Walks on Graphs, 2002 (unfinished monograph). https://www.stat.berkeley.edu/~aldous/RWG/book.html

20 thms4 active usersReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

The Price of Anarchy of Finite Congestion Games V: The Mixed Price of Anarchy of the Average Social Cost Is at Most (3+sqrt 5)/2Research Paper

Motivation

When many self-interested users share resources whose cost grows with use (links of a network, servers, machines), each user picks the option that is cheapest for them given what the others do, and the resulting equilibrium can be worse for the group than a centrally planned allocation. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures this loss as the worst ratio between the social cost of an equilibrium and the optimal social cost. Congestion games (Rosenthal 1973) are the standard finite model of such resource sharing: they always have pure Nash equilibria, and they cover atomic routing, load balancing and many network design questions.

Timeline of the linear-latency case:

2002: Roughgarden and Tardos (J. ACM) bound the price of anarchy of nonatomic selfish routing with linear latencies by $4/3$ .
2005: Awerbuch, Azar and Epstein (STOC 2005) and, independently, Christodoulou and Koutsoupias (STOC 2005) show that for atomic (finite) congestion games with linear latencies the pure price of anarchy of the total cost is $5/2$ . Awerbuch, Azar and Epstein also obtain $(3+\sqrt5)/2 \approx 2.618$ for weighted players.
2005: Christodoulou and Koutsoupias observe that their argument for $5/2$ extends to mixed Nash equilibria, at the price of the larger constant $(3+\sqrt5)/2$ (their Theorem 14, the goal of this mission).

Setting

A congestion game consists of a finite set $N$ of players, a finite set $E$ of facilities, for each player $i$ a collection $\Sigma_i$ of pure strategies, each a subset of $E$ , and for each facility $e$ a latency function $f_e : \mathbb N \to \mathbb R$ . In a pure profile $A = (A_1, \dots, A_n)$ , $A_i \in \Sigma_i$ , the load $n_e(A)$ is the number of players whose set contains $e$ , and player $i$ pays

c_i(A) = \sum_{e \in A_i} f_e\bigl(n_e(A)\bigr).

The social cost of a pure profile is $\mathrm{SUM}(A) = \sum_{i\in N} c_i(A)$ ( $N$ times the average cost). Latencies are linear: $f_e(k) = a_e k + b_e$ with $a_e, b_e \ge 0$ .

A mixed strategy $p_i$ of player $i$ is a probability distribution on $\Sigma_i$ . The players randomize independently, so the pure profile $s$ occurs with probability $\Pr(s) = \prod_j p_j(s_j)$ . Player $i$ 's expected cost is $\mathbb E[c_i] = \sum_s \Pr(s)\, c_i(s)$ , and the expected load of $e$ is $\mathbb E[n_e] = \sum_s \Pr(s)\, n_e(s)$ . A mixed profile is a mixed Nash equilibrium if no player can lower their expected cost by switching unilaterally to another distribution on their strategies. The social cost of a mixed profile is the sum of the expected costs, $\mathrm{SUM}(p) = \sum_i \mathbb E[c_i]$ .

In Lean: CongestionGame ι E with fields strategies and latency, load, cost, IsProfile, sumCost, IsLinear, expCost, expLoad, mixedSumCost and IsMixedNash, all in the namespace CongestionPoA.Mixed; lotteries and independent randomization come from the platform definition agt_games (AGT.IsLottery, AGT.profileProb, AGT.IsMixedNash).

Formalization targets

Goal: Theorem 14

For every congestion game with linear latencies, every mixed Nash equilibrium $p$ and every pure profile $P$ with $P_i \in \Sigma_i$ ,

\sum_{i\in N} \mathbb E[c_i] \;\le\; \frac{3+\sqrt5}{2}\,\mathrm{SUM}(P).

Taking $P$ optimal, the mixed price of anarchy of the average social cost is at most $(3+\sqrt5)/2$ .

Milestones

Lemma 3 (corrected). For real $x \ge 0$ and integer $y \ge 0$ , $y(x+1) \le \frac{\sqrt5-1}{4}x^2 + \frac{\sqrt5+5}{4}y^2$ .
Deviation inequality (Theorem 1's proof, mixed). At a mixed Nash equilibrium, for every player $i$ ,

\mathbb E[c_i] \le \sum_{e\in P_i}\bigl(a_e(\mathbb E[n_e]+1) + b_e\bigr).

Summing step (Theorem 1's proof, mixed).

\sum_i \mathbb E[c_i] \le \sum_{e\in E} n_e(P)\bigl(a_e(\mathbb E[n_e]+1) + b_e\bigr).

Significance

The bound says that randomization by the players cannot make linear congestion games much worse than pure play: the loss stays within a constant factor independent of the number of players and facilities. Mixed equilibria matter because they always exist in every finite game and because they model populations of users whose individual choices are not known in advance. The same authors report (PDF p. 2) extending these bounds to correlated equilibria with the same values, which places the mixed bound in a hierarchy of equilibrium notions whose worst cases coincide.

The result is proved in the paper, in one sentence that defers to the proof of Theorem 1. The work here is a complete machine-checked version: the expected-cost layer for congestion games on top of agt_games, the deviation and summing inequalities under product distributions, and the corrected Lemma 3. The paper prints Lemma 3 for all nonnegative reals $x, y$ , where it is false (at $x = 0$ , $y = 1/10$ the left side is $0.1$ and the right side about $0.018$ ); the formal statement keeps $y$ an integer, which is how the lemma is used. No formalization of congestion-game price-of-anarchy bounds was on the platform when this mission was drafted.

Difficulty

The pure proof compares $n_e(P)(n_e(A)+1)$ with $n_e(A)^2$ and $n_e(P)^2$ through an integer inequality (Lemma 1). Under a mixed equilibrium the equilibrium side is an expectation, so the cost of a facility is no longer a function of one integer load, and Lemma 1's constant $1/3$ is not available for real arguments: a real-variable version is needed, and the constant degrades from $5/2$ to $(3+\sqrt5)/2$ . A second obstacle is bookkeeping: the deviating player's load changes only on their own deviation, while the other players' randomization stays independent, and the expected cost of a player has to be related to expected facility loads, which uses linearity of the latencies in an essential way. The naive idea of applying Theorem 1 to each pure profile in the support of the equilibrium fails, because those profiles are not themselves Nash equilibria.

Formalization scope

Players and facilities are finite types ι and E; profiles are functions ι → Finset E, with feasibility IsProfile a separate predicate. Latencies are real-valued on natural-number loads, and "linear" means affine with nonnegative coefficients, $f_e(k) = a_e k + b_e$ ; the paper displays only the identity latency $f_e(k)=k$ and states that its proofs extend. Mixed strategies are real weight functions on the finite strategy type $\Sigma_i$ ; independence is built into AGT.profileProb; Nash deviations range over all lotteries, which is equivalent to pure deviations. agt_games maximizes payoffs, so the game is passed to it with payoff $-c_i$ . The goal is stated against every feasible pure profile rather than as a ratio, so no division by an optimum that may be $0$ occurs. The social cost is the expected sum of the players' costs; the paper's second option, $\sum_e \mathbb E[n_e^2]$ , is not part of this mission. A version with correlated distributions on profiles, or one that bounds the cost of an "averaged" profile instead of the expected cost, is a different statement and does not discharge the goal.

A complete development needs elementary finite-sum manipulation of product distributions (marginals of AGT.profileProb, expectations of loads), and a Jensen-type inequality $(\mathbb E[n_e])^2 \le \mathbb E[n_e^2]$ for finite distributions. The expectation lemmas for congestion games are reusable for the other mixed results of the literature (weighted games, polynomial latencies). Proofs of the milestones, of the expectation layer, and alternative arguments are all welcome.

Selected references

G. Christodoulou, E. Koutsoupias, The Price of Anarchy of Finite Congestion Games, STOC 2005, pp. 67–73. https://doi.org/10.1145/1060590.1060600
B. Awerbuch, Y. Azar, A. Epstein, The Price of Routing Unsplittable Flow, STOC 2005, pp. 57–66. https://doi.org/10.1145/1060590.1060599
E. Koutsoupias, C. Papadimitriou, Worst-case Equilibria, STACS 1999, LNCS 1563, pp. 404–413. https://doi.org/10.1007/3-540-49116-3_38
R. W. Rosenthal, A Class of Games Possessing Pure-Strategy Nash Equilibria, International Journal of Game Theory 2 (1973), pp. 65–67. https://doi.org/10.1007/BF01737559
T. Roughgarden, É. Tardos, How Bad Is Selfish Routing?, Journal of the ACM 49 (2002), pp. 236–259. https://doi.org/10.1145/506147.506153

7 thms3 active usersReviewed

Linear Optimization Machine Learning Statistics·Captain: mikedeng1

The Dantzig Selector: Statistical Estimation When p Is Much Larger than n 2: Oracle Inequality within a Logarithmic Factor of the Ideal Mean Squared ErrorResearch Paper

Motivation

Many regression problems have far more unknown coefficients $p$ than observations $n$ : gene expression studies with tens of samples and thousands of genes, imaging from few measurements, nonparametric curve recovery from a finite number of noisy samples. Estimation is hopeless in general, but becomes possible when the parameter is sparse, that is, has few nonzero entries. Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) proposed the Dantzig selector, an estimator computed by a single linear program, and showed that its squared error is within a logarithmic factor of what an oracle that knew which coefficients matter could achieve.

The estimator became one of the two standard $\ell_1$ methods for high-dimensional regression, alongside the Lasso; the comparison of the two by Bickel, Ritov and Tsybakov (arXiv:0801.1095, 2009) is built on it. This mission targets the paper's main result, the oracle inequality (Theorem 1.2). A companion mission covers the simpler $\ell_2$ bound for sparse parameters (Theorem 1.1).

Setting

Observations follow the linear model

y = X\beta + z,

where $X\in\mathbb R^{n\times p}$ is a deterministic design matrix with columns $X_1,\dots,X_p$ , each of Euclidean norm $\|X_j\|_{\ell_2}=1$ ; $\beta\in\mathbb R^p$ is an unknown deterministic parameter; and $z=(z_1,\dots,z_n)$ has independent $N(0,\sigma^2)$ coordinates, $\sigma>0$ . The vector $\beta$ is $S$ -sparse if at most $S$ of its entries are nonzero.

Two constants of $X$ measure how close sparse sets of columns are to being orthonormal. The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ such that $(1-\delta)\|c\|_{\ell_2}^2\le\|Xc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2$ for every $c$ supported on at most $S$ indices. The restricted orthogonality constant $\theta_{S,S'}$ (defined for $S+S'\le p$ ) is the smallest $\theta\ge0$ with $|\langle Xc,Xc'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ whenever $c,c'$ are supported on disjoint sets of sizes at most $S$ and $S'$ . Below $\delta:=\delta_{2S}$ and $\theta:=\theta_{S,2S}$ .

For a tuning level $\lambda_p>0$ , a Dantzig selector $\hat\beta$ is any solution of

\min_{\tilde\beta\in\mathbb R^p}\|\tilde\beta\|_{\ell_1}\quad\text{subject to}\quad\|X^*(y-X\tilde\beta)\|_{\ell_\infty}=\sup_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\sigma .

The ideal mean squared error is $\sum_{i=1}^p\min(\beta_i^2,\sigma^2)$ : the risk of an oracle that keeps exactly the coordinates above the noise level.

Formalization targets

Goal: Theorem 1.2 (pp. 8–9)

Let $t>0$ , $a\ge0$ , and $\lambda_p:=(\sqrt{1+a}+t^{-1})\sqrt{2\log p}$ . If $\beta$ is $S$ -sparse and $\delta_{2S}+\theta_{S,2S}<1-t$ , then with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ every Dantzig selector obeys

\|\hat\beta-\beta\|_{\ell_2}^2\le C_2^2\cdot\lambda_p^2\cdot\Big(\sigma^2+\sum_{i=1}^p\min(\beta_i^2,\sigma^2)\Big),

with the explicit constant (1.14)

C_2=\frac{2C_0}{1-\delta-\theta}+\frac{2\theta(1+\delta)}{(1-\delta-\theta)^2}+\frac{1+\delta}{1-\delta-\theta},\qquad C_0=2\sqrt2\Big(1+\frac{1-\delta^2}{1-\delta-\theta}\Big)+\Big(1+\frac1{\sqrt2}\Big)\frac{(1+\delta)^2}{1-\delta-\theta}.

Milestones

Lemma 3.2: $\|X\beta\|_{\ell_2}\le\sqrt{1+\delta}\,(\|\beta\|_{\ell_2}+(2S)^{-1/2}\|\beta\|_{\ell_1})$ for every $\beta$ .
Lemma A.1 (dual sparse reconstruction, $\ell_2$ version): for $c$ supported on $|T|\le2S$ , a vector $\beta$ on $T$ whose correlations $\langle X\beta,X_j\rangle$ equal $c_j$ on $T$ and are small off $T$ except on an exceptional set of size at most $S$ , with bounds (6.1)–(6.6).
Corollary A.2 ( $\ell_\infty$ version): the same without exceptional set, constants $1/(1-\delta-\theta)$ .
Corollary A.3 (constrained thresholding): an $S$ -sparse $\beta$ with $\|\beta\|_{\ell_2}<\lambda\sqrt S$ splits as $\beta'+\beta''$ with $\beta'$ small in $\ell_2$ and $\ell_1$ and $\|X^*X\beta''\|_{\ell_\infty}<\frac{1-\delta^2}{1-\delta-\theta}\lambda$ .
Gaussian tail bound (Section 3, p. 15): $P(\sup_j|\langle z,X_j\rangle|>u)\le2p\,\varphi(u)/u$ for standard Gaussian noise.
Lemma 3.1: the $\ell_2$ mass of $h$ on $T_0$ and its top $S$ positions outside $T_0$ is controlled by $\|X^T_{T_{01}}Xh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$ .

Significance

The result. Theorem 1.2 says that a single linear program, which knows neither the support of $\beta$ nor which coefficients exceed the noise, matches the oracle risk $\sum_i\min(\beta_i^2,\sigma^2)$ up to a factor $O(\log p)$ , uniformly over $S$ -sparse parameters and with explicit, nonasymptotic constants. For coefficients well below the noise level it is far sharper than the $\sigma^2 S\log p$ bound of Theorem 1.1. It is the template for later oracle inequalities for $\ell_1$ -penalized estimators under restricted isometry or restricted eigenvalue conditions.

Formalizing it. The theorem is proved in the paper, but parts of the argument are only sketched: Corollary A.2 refers to the 2005 Decoding by Linear Programming paper for its convergence argument, and Corollary A.3's $\ell_1$ bound is printed with a constant its own proof does not deliver. A machine-checked proof settles these steps. The restricted isometry and orthogonality constants used here are already published on the platform from the decoding series; the appendix lemmas on dual vectors are reusable for any compressed-sensing result in that framework. No formalization of the Dantzig selector's oracle inequality is known to us.

Difficulty

The natural proof compares $\hat\beta$ with the hard-thresholded parameter $\beta^{(1)}$ that keeps only the large coefficients: if $\beta^{(1)}$ were feasible for the Dantzig constraint, the analysis of Theorem 1.1 would apply directly. It is not feasible in general, because the small coefficients $\beta^{(2)}$ , though individually below the noise level, can add up to a large correlation $X^*X\beta^{(2)}$ . The central difficulty is to split $\beta^{(2)}$ into a part with controlled $\ell_1$ and $\ell_2$ norm and a part invisible to the constraint; this requires constructing dual vectors with prescribed correlations (Lemma A.1, Corollary A.2), via an iterative, geometrically convergent correction. The probabilistic part is a Gaussian tail estimate plus a union bound, and the bookkeeping of constants must be carried through exactly.

Formalization scope

Vectors are functions Fin p → ℝ, the design is Matrix (Fin n) (Fin p) ℝ, and the noise is a family z : Fin n → Ω → ℝ of mutually independent random variables (iIndepFun) each with law gaussianReal 0 σ². $\delta_{2S}$ and $\theta_{S,2S}$ are the published CandesTao.Decoding.restrictedIsometryConst X (2*S) and restrictedOrthogonalityConst X S (2*S) (infima, absolute value in the orthogonality condition). Domain: $S\ge1$ and $3S\le p$ (the paper defines $\theta_{S,S'}$ for $S+S'\le p$ ), which forces $p\ge3$ and $\log p>0$ . A Dantzig selector is any $\ell_1$ minimizer over the feasible set; the $\ell_\infty$ constraint is a bound on every coordinate.

The goal bounds from above the (outer) probability of the bad event "no Dantzig selector exists, or some Dantzig selector violates (1.13)". Because the event includes non-existence, a definition no vector satisfies cannot make the theorem vacuous; and the constant $C_2$ is the printed (1.14), evaluated at $\delta_{2S}$ , $\theta_{S,2S}$ of $X$ , not a free constant chosen after the fact.

Corrected constant: Corollary A.3 is stated with $\|\beta'\|_{\ell_1}\le2\frac{1+\delta}{1-\delta-\theta}\|\beta\|_{\ell_2}^2/\lambda$ , the bound its proof gives once Corollary A.2 is applied at an integer sparsity level; the printed statement omits the factor $2$ . Corollary A.2 carries Lemma A.1's standing hypothesis $\delta+\theta<1$ . The deterministic lemmas (3.1, 3.2, A.1–A.3) assume nothing about column norms, since their statements do not need it.

Useful infrastructure: monotonicity of $\delta_S$ and $\theta_{S,S'}$ in their indices (the proof applies the lemmas at a smaller sparsity level), the Gaussian tail bound $1-\Phi(u)<\varphi(u)/u$ , existence of minimizers of the Dantzig linear program, and a sorting/blocking toolkit for "the $S$ largest positions". Proofs of individual milestones are welcome independently.

Selected references

E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6):2313–2351, 2007. arXiv:math/0506081v3, doi:10.1214/009053606000001523
E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12):4203–4215, 2005. arXiv:math/0502327, doi:10.1109/TIT.2005.858979
P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4):1705–1732, 2009. arXiv:0801.1095, doi:10.1214/08-AOS620
D. Donoho and I. Johnstone, Ideal spatial adaptation by wavelet shrinkage, Biometrika 81(3):425–455, 1994. doi:10.1093/biomet/81.3.425

11 thms3 active usersReviewed

Linear Optimization Machine Learning Statistics·Captain: mikedeng1

The Dantzig Selector: Statistical Estimation When p Is Much Larger than n 1: ℓ2 Error Bound for Sparse Parameters under the Uniform Uncertainty PrincipleResearch Paper

Motivation

In many statistical applications the number of unknown parameters $p$ is far larger than the number of observations $n$ : gene-expression studies with tens of samples and thousands of genes, imaging problems with fewer measurements than pixels, and nonparametric curve estimation from finitely many noisy samples. Least squares is useless in this regime, since the system $X\beta=y$ is underdetermined. If the parameter is sparse (only a few of its entries are nonzero), estimation becomes possible, and the question is how accurate a computationally tractable estimator can be.

Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) introduced the Dantzig selector, an estimator computed by a linear program, and proved that its squared error is within a factor of order $\log p$ of the error of an oracle that knows where the nonzero entries are. The paper, with its discussion in the same issue, is one of the founding results of high-dimensional sparse regression, alongside the Lasso analysis of Bickel, Ritov and Tsybakov (arXiv:0801.1095).

Timeline. Candès and Tao (2005, arXiv:math/0502327) showed that $\ell_1$ minimization recovers a sparse vector exactly from noiseless data when the restricted isometry constants of the design satisfy $\delta_S+\theta_{S,S}+\theta_{S,2S}<1$ . The Dantzig selector paper (first posted 2005, published 2007) carried this to Gaussian noise, with the $\ell_2$ error bound formalized here (Theorem 1.1) and an oracle inequality (Theorem 1.2). Bickel, Ritov and Tsybakov (2009) replaced the restricted isometry hypothesis by weaker restricted eigenvalue conditions and showed that the Lasso and the Dantzig selector behave alike.

Setting

Observe $y\in\mathbb R^n$ from the linear model

y=X\beta+z ,

where $X\in\mathbb R^{n\times p}$ is a deterministic design matrix with columns $X_1,\dots,X_p$ , each of Euclidean norm $\|X_j\|_{\ell_2}=1$ ; $\beta\in\mathbb R^p$ is an unknown deterministic parameter; and $z=(z_1,\dots,z_n)$ is a vector of independent $N(0,\sigma^2)$ random variables with $\sigma>0$ . The vector $\beta$ is $S$ -sparse if at most $S$ of its entries are nonzero.

For $T\subseteq\{1,\dots,p\}$ let $X_T$ be the submatrix of the columns indexed by $T$ . The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ with

(1-\delta)\|c\|_{\ell_2}^2\le\|X_Tc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2

for all $|T|\le S$ and all coefficient vectors $c$ ; the restricted orthogonality constant $\theta_{S,S'}$ (for $S+S'\le p$ ) is the smallest $\theta\ge0$ with $|\langle X_Tc,X_{T'}c'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ for all disjoint $T,T'$ with $|T|\le S$ , $|T'|\le S'$ .

Given a tuning parameter $\lambda_p>0$ , the Dantzig selector $\hat\beta$ is any solution of

\min_{\tilde\beta\in\mathbb R^p}\|\tilde\beta\|_{\ell_1}\quad\text{subject to}\quad\|X^*(y-X\tilde\beta)\|_{\ell_\infty}=\max_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\cdot\sigma .

Formalization targets

Goal: Theorem 1.1

Let $S\ge1$ , $3S\le p$ , $\beta$ $S$ -sparse, and $\delta_{2S}+\theta_{S,2S}<1$ . For every $a\ge0$ , with $\lambda_p=\sqrt{2(1+a)\log p}$ , with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ the program has a solution and every solution satisfies

\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot\lambda_p^2\cdot S\cdot\sigma^2,\qquad C_1=\frac{4}{1-\delta_{2S}-\theta_{S,2S}} .

For $a=0$ this is $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot(2\log p)\cdot S\cdot\sigma^2$ , display (1.10) of the paper. The constant is the one the paper's proof establishes (see Formalization scope).

Milestones

The cone constraint (3.2): if $\|\beta+h\|_{\ell_1}\le\|\beta\|_{\ell_1}$ and $\beta$ vanishes off $T_0$ , then $\|h_{T_0^c}\|_{\ell_1}\le\|h_{T_0}\|_{\ell_1}$ .
The tube constraint (3.3): with unit-normed columns, if $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$ and $\hat\beta$ is feasible, then $\|X^*X(\hat\beta-\beta)\|_{\ell_\infty}\le2\lambda_p$ .
Lemma 3.1 (under the section’s unit-column assumption): an $\ell_2$ bound on $h$ over $T_0\cup T_1$ ( $T_1$ the $S$ largest entries of $h$ off $T_0$ ) in terms of $\|X_{T_{01}}^TXh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$ , and $\|h\|_{\ell_2}^2\le\|h\|_{\ell_2(T_{01})}^2+S^{-1}\|h\|_{\ell_1(T_0^c)}^2$ .
The deterministic core: with $\sigma=1$ , on the event $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$ , every Dantzig selector satisfies $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\lambda_p^2S$ .
The Gaussian tail bound: for standard normal $z$ and $Z_j=\langle z,X_j\rangle$ , $\mathbb P(\sup_j|Z_j|>u)\le2p\,\varphi(u)/u$ with $\varphi(u)=(2\pi)^{-1/2}e^{-u^2/2}$ .

Significance

The result. Theorem 1.1 shows that an estimator computable by linear programming reaches, up to the factor $2\log p$ and the constant $C_1^2$ , the squared error $S\sigma^2$ that least squares would attain if the support of $\beta$ were known in advance, even when $p\gg n$ . The factor $\log p$ is the price of not knowing the support; the paper argues (p. 5) that, apart from this factor, (1.10) is unimprovable in general. The bound is non-asymptotic, with an explicit constant and an explicit failure probability, and it holds for every $S$ -sparse $\beta$ simultaneously in the sense that the good event (the noise being nearly orthogonal to every column) does not depend on $\beta$ . Its deterministic part, Lemma 3.1, is reused verbatim in the proof of the paper's oracle inequality (Theorem 1.2) and became a standard tool in compressed sensing.

Formalizing it. The result is proved, and to our knowledge no machine-checked proof exists. A formalization produces a checked version of the cone-and-tube argument behind most $\ell_1$ -recovery guarantees, a Lean statement of the restricted isometry machinery for noisy data, and a checked Gaussian maximal inequality usable for other high-dimensional estimators. It also settles the exact constant: the paper prints $C_1=4/(1-\delta_S-\theta_{S,2S})$ , while its proof gives $\delta_{2S}$ in place of $\delta_S$ .

Difficulty

Lemma 3.1 is the main obstacle. The obvious approach bounds $\|h\|_{\ell_2}$ directly through restricted isometry, and it fails because the error $h$ is not sparse: it spreads over all $p$ coordinates, and restricted isometry controls $X$ only on vectors with at most $2S$ nonzero entries. The two constraints (3.2) and (3.3) only say that $h$ is concentrated in $\ell_1$ on the $S$ coordinates of $T_0$ and that $X^*Xh$ is small coordinatewise, and turning that into an $\ell_2$ bound on all of $h$ is where the work lies. In Lean this requires bookkeeping that is routine on paper: ordering the coordinates of $h$ off $T_0$ by magnitude, with ties and a possibly incomplete last group of coordinates, and working with the span of a selected set of columns. On the probabilistic side, the tail bound needs the law of $\langle z,X_j\rangle$ (a weighted sum of independent Gaussians), a sharp Gaussian tail estimate of Mills-ratio type, and a union over $p$ events. A cruder sub-Gaussian bound $2e^{-u^2/2}$ would not give the stated failure probability.

Formalization scope

Indices are Fin n and Fin p; vectors are functions into ℝ. The norms, the column $X_j$ and the constants $\delta_S$ , $\theta_{S,S'}$ are the published definitions CandesTao_Decoding_Norms and CandesTao_Decoding_RestrictedIsometry (the smallest admissible constants, via sInf), from the formalization of Candès and Tao's Decoding by Linear Programming. The noise is a family z : Fin n → Ω → ℝ on a probability space, mutually independent (iIndepFun), each coordinate with law gaussianReal 0 σ². The $\ell_\infty$ constraint is coordinatewise. A Dantzig selector is any minimizer; uniqueness is not assumed. Section 3 works with $\sigma=1$ ; the goal is stated for general $\sigma>0$ .

Committed conventions and corrections:

Corrected constant. Theorem 1.1 is printed with $C_1=4/(1-\delta_S-\theta_{S,2S})$ , but the proof (pp. 18–19) applies Lemma 3.1, whose $\delta$ is $\delta_{2S}$ . Since $\delta_S\le\delta_{2S}$ , the printed constant is stronger than what is proved. The goal and the deterministic core are stated with $C_1=4/(1-\delta_{2S}-\theta_{S,2S})$ .
Domain. $1\le S$ and $3S\le p$ , because $\theta_{S,2S}$ is defined only for $S+2S\le p$ . This forces $p\ge3$ and $\log p>0$ .
Failure event. The probability bounded is that of the set where no Dantzig selector exists or some Dantzig selector violates the bound. A version that only constrains existing solutions, or that assumes the feasible set is nonempty, would be weaker. The bound is strict, as in the paper's "exceeding", and is on the outer measure, so no measurability of the event is assumed.
Standing assumptions are binders: unit-normed columns, independent Gaussian noise, deterministic $X$ and $\beta$ .

A trivializing formalization is excluded: the hypothesis $\delta_{2S}+\theta_{S,2S}<1$ is on the actual least constants of $X$ , not on free parameters, and it is satisfiable (for instance by $X=I_p$ , where both constants vanish).

Needed infrastructure: sums of independent real Gaussians (Mathlib has gaussianReal and its convolution), a Mills-ratio tail bound, a sorting-based block decomposition of a Finset, and orthogonal projection onto the span of finitely many columns. The block decomposition and the tail bound are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 3.1.

Selected references

E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6) (2007), 2313–2351. arXiv:math/0506081, doi:10.1214/009053606000001523
E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12) (2005), 4203–4215. arXiv:math/0502327
P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4) (2009), 1705–1732. arXiv:0801.1095

9 thms3 active usersReviewed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Air Travel Demand and Airline Seat Inventory Management I: Marginal Seat Allocation Among Distinct Fare ClassesTextbook

Why airlines allocate seats by fare class

An airline sells the seats of one flight leg at several prices. Low fares fill seats that would otherwise fly empty; high fares are bought by passengers who book late and cannot be predicted exactly. Seat inventory control decides how many seats each fare class may sell. Peter Belobaba's 1987 MIT dissertation (MIT Flight Transportation Laboratory Report R87-7) gave the probabilistic treatment of this problem that became the expected marginal seat revenue (EMSR) method, which was in use across the airline industry for decades.

This mission formalizes the first, simplest model of the thesis: distinct (non-nested) fare-class inventories on a single leg, where a seat assigned to a class may be sold only in that class or not at all. The thesis surveys this model in Sect. 4.2 (pp. 84–94), where an integer-programming formulation from McDonnell-Douglas and its solution by ranking marginal values are described (p. 90), and develops it probabilistically in Sect. 5.1 (pp. 102–107).

Setting

A leg has capacity $n$ seats (the thesis also writes $C$ ). There are finitely many fare classes $i$ . Class $i$ has an average fare $f_i \ge 0$ and receives a random number of requests $r_i \in \{0,1,2,\dots\}$ , with law $p_i$ . The seats are split into allocations $S_i \in \mathbb{N}$ , one per class.

With $S$ seats, a class books requests until its seats run out, so its bookings and spill (refused requests) are

b = \min(r, S), \qquad l = (r - S)^+ \qquad \text{(Eq. (5.3))}.

The expected revenue of class $i$ is $\bar R_i(S_i) = f_i \cdot \bar b_i(S_i)$ with $\bar b_i(S_i) = E[\min(r_i,S_i)]$ , and the leg's expected revenue is $\bar R = \sum_i \bar R_i(S_i)$ (Eq. (5.9)). Write

\bar P_i(S) = P[r_i \ge S], \qquad \mathrm{EMSR}_i(S) = f_i \cdot \bar P_i(S) \qquad \text{(Eqs. (5.11), (6.1), (6.2))},

the expected marginal seat revenue of the $S$ -th seat of class $i$ . The value of the $k$ -th seat of class $i$ in the integer program of p. 90 is $m_i(k) = \mathrm{EMSR}_i(k)$ , $k = 1, \dots, n$ .

Formalization targets

Goal: the $n$ largest marginal values give the optimal booking limits (p. 90)

Let $T$ be any set of $n$ pairs $(i,k)$ , $1 \le k \le n$ , such that every $m_i(k)$ with $(i,k) \in T$ is at least every $m_j(l)$ with $(j,l) \notin T$ , and let $S^T_i = \#\{k : (i,k) \in T\}$ . Then $\sum_i S^T_i = n$ and

\sum_i f_i\, E[\min(r_i, S_i)] \;\le\; \sum_i f_i\, E[\min(r_i, S^T_i)] \qquad \text{for every } S \text{ with } \textstyle\sum_i S_i \le n .

The goal fixes no distribution, number of classes or fare ordering, and it holds for every tie-breaking among equal marginal values.

Milestones

Eq. (5.6): $\bar b_i(S) + \bar l_i(S) = \bar r_i$ for requests of finite mean.
Eq. (5.11): $\bar R_i(S) - \bar R_i(S-1) = f_i \cdot P[r_i \ge S]$ for $S \ge 1$ .
Eqs. (6.1)–(6.2): $\bar P_i$ and $\mathrm{EMSR}_i$ are non-increasing in $S$ .
Eq. (4.5): the 0–1 vector equal to $1$ on a set of $n$ largest $m_i(k)$ is an optimal solution of the linear program $\max \sum_{i,k} X_{ik} m_i(k)$ subject to $\sum X_{ik} \le n$ , $0 \le X_{ik} \le 1$ .
Eq. (5.13), discrete form: an allocation of exactly $C$ seats maximises $\bar R$ among such allocations if and only if some $\lambda$ satisfies $\mathrm{EMSR}_i(S_i) \ge \lambda$ whenever $S_i \ge 1$ and $\mathrm{EMSR}_i(S_i + 1) \le \lambda$ , for all $i$ .

Significance

The goal is the reason distinct-inventory allocation is computationally easy: a revenue-maximising allocation is obtained by sorting $n \times (\text{number of classes})$ numbers, with no search over allocations. The same marginal-value principle underlies the EMSR rules for nested classes in the rest of the thesis, and the identity (5.11) is the link between an expected-revenue function and its marginal seat values used throughout revenue management. Milestone 5 is the integer form of the Lagrangian condition of Eq. (5.13); the thesis states it only for a continuous relaxation, and its equality form is generally unattainable with integer seats.

These results are classical and their proofs are elementary; to our knowledge none of them has been machine-checked. The mission produces a reusable formal model of a single-leg, distinct-inventory allocation problem with integer demand (bookings, spill, revenue and marginal values of a PMF ℕ), and checked statements of the marginal-allocation principle for it.

Difficulty

The thesis argues with continuous densities and derivatives, setting $\partial \bar R / \partial S_i$ equal across classes. That argument does not transfer to integer seats: the derivative of a step-shaped expected-revenue function does not exist, equality of marginal values across classes generally fails at every integer allocation, and the tail probability must be $P[r \ge S]$ rather than the $P[r > S]$ of Eq. (5.2) for the marginal identity to hold. The integer statements need their own exchange argument. A second subtlety is ties: "the $n$ largest values" is not unique, and the goal must hold for every admissible choice, including choices in which a class's selected seat numbers are not an initial segment $\{1, \dots, S_i\}$ .

Formalization scope

All declarations live in the namespace SeatInventory.Distinct. Conventions:

Integer demand. The law of class $i$ 's requests is d i : PMF ℕ; expectations are series over $\mathbb{N}$ . The thesis's continuous densities are replaced by this discrete model, which the thesis itself requires for seat allocations (p. 103).
Tail convention. $\bar P(S) = P[r \ge S]$ , as in Eq. (6.2) and the prose of Eq. (5.11) ("the probability of selling $S_i$ or more seats"), not the $P[r > S]$ of Eq. (5.2).
Seat numbers start at 1, and the pairs $(i,k)$ range over $k \in \{1, \dots, n\}$ , as the 600 variables of a 150-seat, four-class problem on p. 90 indicate.
Nonnegative fares $f_i \ge 0$ are assumed in every statement that needs them; with a negative fare the capacity constraint $\sum S_i \le n$ would not bind and the claims fail.
Finite mean of the requests is assumed explicitly for Eq. (5.6); the thesis assumes it silently. Expected bookings are bounded and need no assumption.
Capacity. The goal and the LP compare against allocations with $\sum_i S_i \le n$ (the LP's constraint); milestone 5 compares allocations of exactly $C$ seats (Eq. (5.8)).
No independence assumption. Expected revenue of distinct inventories depends only on each class's marginal law, so the statements take one law per class.
"Decreasing" is non-increasing. The thesis's justification in Sect. 6.1.1 gives only monotonicity; strict decrease fails for bounded demand.
LP integrality. "The solution will be integer" is stated as: the indicator of every set of $n$ largest values is optimal. With ties the LP also has fractional optima.

The expected revenue in the goal is computed from the booking rule $\min(r_i, S_i)$ ; it is not defined as a sum of marginal values, and the optimal allocation is not defined as an argmax of $\bar R$ . Either shortcut would make the goal a tautology and is ruled out.

Needed infrastructure: tail sums of a PMF ℕ, telescoping of $E[\min(r, S)]$ , and a finite exchange argument for sums of the $n$ largest values of a function on a finite set; the last two are reusable for any separable concave resource-allocation problem. Contributions of proofs of any milestone, and of a verified sorting routine that produces a set of $n$ largest values, are welcome.

Selected references

P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT Flight Transportation Laboratory Report R87-7, 1987 (no DOI).
P. P. Belobaba, Airline yield management: an overview of seat inventory control, Transportation Science 21(2), 63–73, 1987. https://doi.org/10.1287/trsc.21.2.63
P. P. Belobaba, Application of a probabilistic decision model to airline seat inventory control, Operations Research 37(2), 183–197, 1989. https://doi.org/10.1287/opre.37.2.183
K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134

8 thms3 active usersReviewed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

A Polylogarithmic-Competitive Algorithm for the k-Server Problem: Randomized k-Server Is O(log² k · log³ n · log log n)-Competitive on Every n-Point MetricResearch Paper

Motivation

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

Timeline of the upper bounds for general metrics:

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

Setting

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

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

Formalization targets

Goal: Theorem 1

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

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

Milestones

In the order the proof uses them:

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

14 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Correlated Equilibrium as an Expression of Bayesian Rationality I: Bayes Rationality at Every State Yields Exactly the Correlated Equilibrium DistributionsResearch Paper

Motivation

Nash equilibrium is the standard solution concept for strategic games, but it is usually justified by appeal to what players "would" do once they somehow coordinate on a profile. Correlated equilibrium, introduced by Aumann (J. Math. Econ. 1, 1974), enlarges the set of outcomes by letting players condition their actions on correlated private signals. In Correlated Equilibrium as an Expression of Bayesian Rationality (Econometrica 55, 1987), Aumann gave the concept a decision-theoretic foundation: if the players share a common prior over the states of the world and each player maximizes expected utility given his information at every state, then what they play is a correlated equilibrium — and every correlated equilibrium arises this way. The result is a standard entry point to the epistemic foundations of game theory, and correlated equilibria are central in algorithmic game theory because no-swap-regret learning dynamics converge to them (Foster–Vohra 1997; Hart–Mas-Colell 2000).

Timeline:

1974, Aumann: correlated equilibrium defined, in a measure-theoretic model with subjective probabilities and information σ-fields.
1987, Aumann: the Main Theorem (Bayes rationality at every state under a common prior implies correlated equilibrium play) and its converse, in a finite model with information partitions.

Setting

A game $G$ in strategic form has players $i$ , action sets $S^i$ , action $n$ -tuples $s\in S=S^1\times\dots\times S^n$ , and payoffs $h^i(s)\in\mathbb R$ .

A correlated strategy $n$ -tuple is a function $f:\Gamma\to S$ on a finite probability space $(\Gamma,q)$ , with $q\ge 0$ and $\sum_\gamma q(\gamma)=1$ . Its expected payoff is $Eh^i(f)=\sum_\gamma q(\gamma)h^i(f(\gamma))$ . For $g^i:\Gamma\to S^i$ , the profile $(f^{-i},g^i)$ replaces player $i$ 's coordinate of $f$ by $g^i$ . The function $f$ is a correlated equilibrium (Definition 2.1) if

Eh^i(f)\ \ge\ Eh^i(f^{-i},g^i)\qquad(2.2)

for every player $i$ and every $g^i$ that is a function of $f^i$ (i.e. $g^i=\varphi\circ f^i$ ). The distribution of $f$ assigns to each $s\in S$ the number $q\{f^{-1}(s)\}$ , and a correlated equilibrium distribution (c.e.d.) is the distribution of some correlated equilibrium.

An information system consists of a finite set $\Omega$ of states of the world, a common prior $p$ on $\Omega$ , an information partition $\mathcal P^i$ of $\Omega$ for each player, and action functions $\mathbf s^i:\Omega\to S^i$ with $\mathbf s=(\mathbf s^1,\dots,\mathbf s^n)$ , each $\mathbf s^i$ constant on the elements of $\mathcal P^i$ (each player knows his own action). For a random variable $x$ , $E(x\mid\mathcal P^i)(\omega)$ is the $p$ -average of $x$ over the element of $\mathcal P^i$ containing $\omega$ . Player $i$ is Bayes rational at $\omega$ if

E\big(h^i(\mathbf s)\mid\mathcal P^i\big)(\omega)\ \ge\ E\big(h^i(\mathbf s^{-i},a)\mid\mathcal P^i\big)(\omega)\quad\text{for every }a\in S^i .

Formalization targets

Goal: Main Theorem with its converse

Q\ \text{is a c.e.d. of }G\iff\exists\ \text{information system }(\Omega,p,(\mathcal P^i),\mathbf s):\ \text{every player is Bayes rational at every state, and } Q(a)=p\{\mathbf s=a\}\ \forall a.

This is the two-sided statement the paper announces in its introduction (p. 2) and closes in Sect. 4d (p. 11): "under Bayesian rationality, the set of all information systems corresponds precisely to the set of all correlated equilibria."

Milestones

Main Theorem, proof: summing the cell-wise inequalities over the partition, $Eh^i(\mathbf s^{-i},g^i)\le Eh^i(\mathbf s)$ for $g^i$ constant on the cells of $\mathcal P^i$ .
Main Theorem, proof: $\mathbf s$ itself is a correlated equilibrium on $(\Omega,p)$ .
Main Theorem (p. 7): the distribution of $\mathbf s$ is a c.e.d.
Sect. 4d: in the system generated by $f$ (partitions generated by $f^i$ ), Bayes rationality everywhere is equivalent to (2.2).
Sect. 4d: every correlated equilibrium is realized by a Bayes-rational information system with the same distribution.

The mission also states, as a supporting lemma without a milestone, the cell-wise step of the proof of the Main Theorem: Bayes rationality at every state gives $E(h^i(\mathbf s^{-i},g^i)\mid P)\le E(h^i(\mathbf s)\mid P)$ on every cell $P$ for $g^i$ constant on cells.

Significance

The theorem identifies correlated equilibrium as the outcome of individual Bayesian decision making under a common prior, without any assumption that players randomize or that their choices are independent. It shows that the Nash equilibrium's independence requirement is not implied by rationality alone, and it is the template for later epistemic characterizations of solution concepts. On the computational side, correlated equilibrium distributions form a polytope described by linear inequalities (the companion mission of this series), which is why they are the tractable equilibrium notion in algorithmic game theory.

The result is proved in the paper; it has no machine-checked formalization known to this mission. Formalizing it pins down the exact role of the standing assumptions — finiteness, a common prior, measurability of each player's action with respect to his own partition, rationality at every state — and of the conditional expectation on cells of probability zero. The definitions (information systems, Bayes rationality, correlated equilibria as functions on a finite probability space) are reusable for later formalizations of the paper's Sect. 5 (subjective correlated equilibrium) and of other epistemic results.

Difficulty

The mathematics is short; the difficulty lies in the bookkeeping that the paper's notation hides. The hypothesis is interim (a conditional inequality at each state), while Definition 2.1 is ex ante (an unconditional inequality). Passing between them requires the law of total expectation over a partition whose cells may have probability zero, where conditional expectations are undefined. Deviations in Definition 2.1 are functions of $f^i$ , not arbitrary maps, and must be shown constant on cells, which uses measurability of $\mathbf s^i$ . A tempting first idea — that rationality against every fixed action already gives rationality against every deviation — fails without measurability: a player who does not know his own action could be rational at each state against constant deviations while a deviation $\varphi\circ\mathbf s^i$ varies inside his cells. The converse direction needs an information system that satisfies every axiom of the goal's right-hand side, not just one that is Bayes rational.

Formalization scope

Players form a finite type ι with decidable equality; action sets S i are arbitrary types (the paper's finiteness of $S^i$ is not used); payoffs are h : ι → (∀ i, S i) → ℝ.
Probability spaces are finite types with a real weight vector satisfying AGT.IsLottery (from the published definition agt_games). State spaces and the witnessing probability spaces of a c.e.d. range over Type; for finite sets this loses nothing.
Partitions are Setoids. The Common Prior Assumption is built into the information system, which has a single prior. Measurability of each action function is a field of the structure.
Conditional expectation on a cell is a ratio of finite sums; on a cell of probability zero Lean returns $0$ , so Bayes rationality at such states holds vacuously. The prior is not required to have full support. This matches the paper, whose argument multiplies each cell inequality by the cell's probability.
Deviations in Definition 2.1 are exactly the compositions $\varphi\circ f^i$ ; neither all maps nor only constant maps. A c.e.d. requires a genuine probability vector, ruling out the trivializing reading in which the zero weight function witnesses every $Q$ .
Contributions welcome: proofs of the milestones, a general law-of-total-expectation lemma for finite partitions, and lemmas relating distr to sums over action profiles.

Selected references

R. J. Aumann, Correlated Equilibrium as an Expression of Bayesian Rationality, Econometrica 55 (1987), no. 1, 1–18. https://doi.org/10.2307/1911154
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
S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68 (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153

9 thms3 active usersReviewed

Markov Chain Operations Research Stochastic Systems·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems XIII: Lyapunov Criteria and z Standard Markov Chains with CostsTextbook

Motivation

Average cost control of queues rests on a small amount of Markov chain theory: when does a chain with costs have a well defined long-run average cost, and how can that be checked for a concrete model with an unbounded state space? Appendix C of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) collects this material for countable state spaces and packages it in one hypothesis, the $z$ standard chain. Chapters 7–10 of the book verify this hypothesis for the Markov chains induced by stationary policies in admission, routing and service-rate control models, and use its consequences to prove existence of average cost optimal policies.

The tools are Lyapunov functions in the sense of Foster (1953): a nonnegative function on the states whose expected one-step change is negative away from a finite set. Foster's criterion for positive recurrence, and its refinements bounding expected first passage times and costs, are the standard way to verify stability of queueing networks (Meyn and Tweedie, Markov Chains and Stochastic Stability, 1993/2009).

Setting

A Markov chain $\Gamma$ on a countable set $S$ is given by transition probabilities $P_{ij}\ge 0$ with $\sum_j P_{ij}=1$ . $X_t$ is the state at time $t$ and $P^{(t)}_{ij}$ the $t$ -step transition probability ( $P^{(0)}_{ij}=\delta_{ij}$ ). State $i$ leads to $j$ if $P^{(t)}_{ij}>0$ for some $t\ge0$ ; states that lead to each other communicate, which partitions $S$ into communicating classes.

For a nonempty $G\subseteq S$ the first passage time from $i$ is $T_{iG}=\min\{t\ge1: X_t\in G\}$ given $X_0=i$ , and $m_{iG}=E[T_{iG}]\in[0,\infty]$ ; $m_{ij}$ is the case $G=\{j\}$ and $m_{ii}$ the expected return time. The taboo probability $_G P^{(t)}_{ik}$ is the probability of going from $i$ to $k$ in $t$ steps without visiting $G$ at the intermediate times, and $_G u_{ik}$ is the expected number of visits to $k$ at times $0\le t<T_{iG}$ . A state is transient if $P(T_{ii}<\infty)<1$ and positive recurrent if $m_{ii}<\infty$ ; a positive recurrent class is a communicating class of positive recurrent states. The steady state probability is $\pi_j=(m_{jj})^{-1}$ (zero when $m_{jj}=\infty$ ).

Each state carries a finite cost $C(i)\ge0$ . The expected average cost over $[0,n-1]$ from $i$ is

J^{(n)}_i=\frac1n\,E\Big[\sum_{t=0}^{n-1}C(X_t)\,\Big|\,X_0=i\Big]=\frac1n\sum_{t=0}^{n-1}\sum_j P^{(t)}_{ij}C(j),

$c_{iG}$ is the expected cost $E[\sum_{t=0}^{T_{iG}-1}C(X_t)\mid X_0=i]$ of a first passage (defined when $m_{iG}<\infty$ ), and $J_R=\sum_{j\in R}\pi_jC(j)$ is the average cost on a positive recurrent class $R$ . The chain is $z$ standard (Definition C.2.5) if for a distinguished state $z$

m_{iz}<\infty\quad\text{and}\quad c_{iz}<\infty\qquad\text{for all } i\in S.

Formalization targets

Goal: Proposition C.2.6

If $\Gamma$ is $z$ standard, then $S$ is the union of a positive recurrent class $R\ni z$ and a set of transient states, $J_R<\infty$ , and

\lim_{n\to\infty}J^{(n)}_i=J_R\qquad\text{for every } i\in S.

The statement fixes no constants: it asserts that the average cost exists, is finite, and does not depend on the initial state.

Milestones

Proposition C.1.2: $\pi$ is the unique stationary distribution of a positive recurrent class, and $\pi_j=e_{ij}/m_{ii}=\pi_ie_{ij}$ .
Proposition C.1.4: the first-step equations (C.2)–(C.4) for taboo probabilities, visit counts and $m_{iG}$ ; $\sum_{i\in G}\pi_im_{iG}=1$ for $G$ inside a positive recurrent class; $m_{ij}<\infty$ within such a class.
Proposition C.1.5: if $\sum_jP_{ij}[y(j)-y(i)]\le-\epsilon$ off $G$ , then $m_{iG}\le y(i)/\epsilon$ .
Corollary C.1.6: the same with $G=\{z\}$ and $\sum_jP_{zj}y(j)<\infty$ makes $z$ positive recurrent.
Proposition C.2.1: on a positive recurrent class, $J^{(n)}_i\to J_R=c_{ii}/m_{ii}$ .
Proposition C.2.2: $c_{iG}=\sum_kC(k)\,{}_Gu_{ik}$ , the first-step equation (C.13), and $J_R=\sum_{i\in G}\pi_ic_{iG}$ .
Proposition C.2.3 and Corollary C.2.4: the cost drift condition $\sum_jP_{ij}[r(j)-r(i)]\le-C(i)$ off a finite set bounds $c_{iG}\le r(i)+Fm_{iG}$ , and gives $c_{zz}<\infty$ .
Remark C.2.7: the hypotheses of C.1.6 and C.2.4 together imply the chain is $z$ standard; so do irreducibility, positive recurrence and finite average cost.

Significance

Proposition C.2.6 is what makes the $z$ standard hypothesis useful: an average cost criterion that is a genuine limit, finite, and independent of the initial state, even for chains with transient states and unbounded state spaces. Every average cost optimality result of the book that works with a stationary policy's induced chain (the (SEN) and (BOR) assumption sets, the approximating-sequence method, the continuous-time chapter) calls on this proposition or on the Lyapunov criteria of Remark C.2.7 to establish its hypotheses for queueing models.

All results of the mission are classical and proved in the literature; parts are stated in the book without proof and referred to Chung (1967), Grassmann et al. (1985) and renewal theory. None of them has been machine-checked in this form as far as the platform and Mathlib show: Mathlib has kernels and Ionescu-Tulcea trajectories but no countable-state Markov chain classification, no first passage calculus, and no Foster–Lyapunov criterion. Existing platform results on countable chains (the Levin–Peres–Wilmer series) treat irreducible chains without costs. A complete development here produces a reusable library of first passage identities, Foster–Lyapunov bounds for times and costs, and average cost limits on reducible chains.

Difficulty

The Lyapunov bounds (C.1.5, C.2.3) are telescoping arguments, but they require a clean handling of truncated passages and of sums that may be infinite: (C.7) is an inequality between possibly divergent series, and the step "iterate $n$ times and let $n\to\infty$ " must be made rigorous for $[0,\infty]$ -valued expectations.

The central difficulty is part (iii) of the goal for transient initial states. On the class $R$ , the limit of $J^{(n)}_i$ is a renewal reward theorem over successive returns to $z$ ; from a transient state the first cycle has a different law, so a delayed renewal reward argument is needed, and it has to cover the case where costs are unbounded. The obvious approach, bounding $J^{(n)}_i$ between $J_R$ and the average over the first $n$ steps of the chain started in $z$ , fails because $P^{(t)}_{ij}$ need not converge (periodic classes) and because finite $c_{iz}$ does not bound individual cost terms. Proposition C.1.2's uniqueness and the Kac-type identity of C.1.4(iv) likewise need the full cycle decomposition of a positive recurrent class.

Formalization scope

The chain is a structure MC S with P : S → S → ℝ≥0∞ and ∑' j, P i j = 1, over a countable type S; costs are C : S → ℝ≥0. Probabilities and expectations are ℝ≥0∞-valued sums over finite paths Fin (t+1) → S, so every quantity is defined without summability side conditions and may be $\infty$ . The first passage time is $T_{iG}\ge1$ ; $m_{iG}$ is the expectation of $T_{iG}$ from its law (and $\infty$ when $P(T_{iG}<\infty)<1$ ), not defined by the recursion (C.4), so that (C.4) is a theorem. $_Gu_{ik}$ counts visits at times $0\le t<T_{iG}$ . $c_{iG}$ is computed over first passage paths and is used only when $m_{iG}<\infty$ , as in the book. $\pi_j$ is $(m_{jj})^{-1}$ , which the book states equals the Cesàro limit $\lim_nQ^{(n)}_{jj}$ . $J^{(n)}_i$ is meaningful for $n\ge1$ , and limits are taken in $[0,\infty]$ . The drift conditions $\sum_jP_{ij}[y(j)-y(i)]\le-\epsilon$ and $\sum_jP_{ij}[r(j)-r(i)]\le-C(i)$ are written in the equivalent additive form $\sum_jP_{ij}y(j)+\epsilon\le y(i)$ , which is equivalent for finite $y$ and makes the case $\sum_jP_{ij}y(j)=\infty$ fail, as it does in the book.

A trivializing formalization, such as defining $m_{iG}$ or $c_{iG}$ by the equations (C.4) or (C.13), defining $J_R$ as the limit of $J^{(n)}_i$ , or allowing a $z$ standard chain whose return time or return cost to $z$ is infinite, is ruled out: $z$ standard requires $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$ including $z$ , and each quantity is defined from path probabilities.

Needed infrastructure: path-sum manipulation in $[0,\infty]$ (first-step and last-step decompositions), the ratio limit / renewal reward theorem for a positive recurrent class, and the delayed version for transient starts. The first passage calculus and the Lyapunov bounds are reusable by the book's other chapters on average cost, which state the $z$ standard property for policy-induced chains. Contributions of lemmas on path sums and of an independent renewal reward library are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix C, pp. 292–302. doi:10.1002/9780470317037
K. L. Chung, Markov Chains with Stationary Transition Probabilities, 2nd ed., Springer, 1967. doi:10.1007/978-3-642-62015-7
F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953), 355–360. doi:10.1214/aoms/1177728976
S. P. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, 2nd ed., Cambridge University Press, 2009. doi:10.1017/CBO9780511626630
D. P. Heyman and M. J. Sobel, Stochastic Models in Operations Research, Vol. I, McGraw-Hill, 1982.

12 thms3 active usersReviewed

Completed

Analysis·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems XII: A Tauberian Theorem Linking Abel and Cesàro Means of Nonnegative SeriesTextbook

Motivation

In the theory of Markov decision chains two cost criteria dominate: the discounted cost, in which a cost incurred at time $n$ is weighted by $\alpha^n$ for a discount factor $\alpha \in (0,1)$ , and the average cost, the long-run cost per unit time. A standard route to average cost optimal policies is to solve the discounted problem and let $\alpha \to 1^-$ . That route needs a precise link between the two criteria for a single sequence of expected costs $u_0, u_1, u_2, \dots \ge 0$ : the discounted cost multiplied by $1-\alpha$ on one side, the running average on the other. Appendix A.4 of Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) supplies this link as Theorem A.4.2, and the book invokes it whenever it passes from discounted to average cost (for instance in Chapter 6, where it is applied to $u_n = E_\theta[C(X_n, A_n)]$ ).

The result belongs to classical summability theory.

Abelian direction. Convergence of averages implies convergence of the power-series (Abel) means: a consequence of Abel's and Frobenius's theorems on power series (19th century).
Tauber (1897). The first converse, under a growth condition on the terms.
Hardy and Littlewood (1914). The converse for Cesàro means of nonnegative terms, the "Hardy–Littlewood Tauberian theorem".
Karamata (1930). A short proof of that converse by polynomial approximation, reproduced in Titchmarsh, The Theory of Functions (1939, pp. 227–229). The book follows this proof.
Widder (1941). The continuous-time (Laplace transform) version.
Sennott (1986b). A proof of the discrete statement, cited by the book as its source for Theorem A.4.2.

Setting

Let $u_0, u_1, u_2, \dots$ be nonnegative terms $u_n \in [0, \infty]$ with $u_0 < \infty$ . For $\alpha \in [0, \infty)$ the power series

U(\alpha) = \sum_{n=0}^{\infty} \alpha^n u_n \in [0, \infty]

always has a sum, possibly $+\infty$ , because its partial sums increase. Its radius of convergence is $R = (\limsup_{n} u_n^{1/n})^{-1} \in [0,\infty]$ . The partial sums are $w_n = \sum_{k=0}^{n-1} u_k$ for $n \ge 1$ . Two ways of averaging the sequence are compared:

the Cesàro means $w_n / n$ , as $n \to \infty$ ;
the Abel means $(1-\alpha) U(\alpha)$ , as $\alpha \to 1^-$ (from below).

For the constant sequence $u_n \equiv B$ both equal $B$ . In the Lean development these are U, radius, w, cesaroMean and abelMean in the namespace SennottDP.Tauberian, all valued in ℝ≥0∞. The proof also uses the function $r$ of Fig. A.1, equal to $0$ on $(0, e^{-1})$ and to $1/x$ on $[e^{-1}, 1)$ .

Formalization targets

Goal: Theorem A.4.2

\liminf_{n\to\infty} \frac{w_n}{n} \le \liminf_{\alpha\to 1^-} (1-\alpha)U(\alpha) \le \limsup_{\alpha\to 1^-} (1-\alpha)U(\alpha) \le \limsup_{n\to\infty} \frac{w_n}{n}, \tag{A.28}

and the following are equivalent: (i) all terms in (A.28) are equal and finite; (ii) $\lim_n w_n/n$ exists and is finite; (iii) $\lim_{\alpha \to 1^-} (1-\alpha)U(\alpha)$ exists and is finite.

No growth or boundedness condition on $u_n$ is assumed: nonnegativity is the only Tauberian condition.

Milestones

Remark A.3.3: the geometric series. $R = 1$ , $U(\alpha) = B/(1-\alpha)$ and $B\sum_n n\alpha^n = B\alpha/(1-\alpha)^2$ .
Remark A.3.1: inside the radius of convergence, $U$ is differentiable term by term, and the derived series has the same radius.
Eq. (A.31): $\big(\sum \alpha^n\big) U(\alpha) = \sum_n \alpha^n w_{n+1} = U(\alpha)/(1-\alpha)$ .
Eq. (A.28): the Abelian inequalities on their own.
Eq. (A.26): $\int_0^1 r = 1$ .
Lemma A.4.1: continuous $s^* \le r \le s$ with integrals within $\varepsilon$ of $1$ .
Eqs. (A.35)–(A.36): if the Abel means tend to $L < \infty$ , then $(1-\alpha)\sum_n \alpha^n u_n f(\alpha^n) \to L\int_0^1 f$ for $f(x) = x^k$ .
The same statement for every $f$ continuous on $[0,1]$ .
The same statement for $f = r$ .
Example A.5.1: a $0/1$ block sequence with $\liminf w_n/n = 1/2$ and $\limsup w_n/n = 2/3$ (Choice One) or $1$ (Choice Two), for which the middle inequality of (A.28) is strict.

Significance

The result itself. Theorem A.4.2 lets every statement about $\lim_{\alpha\to1^-}(1-\alpha)V_\alpha$ for a discounted value be read as a statement about long-run average cost, and conversely. The strict cases of Example A.5.1 show why the book must work with $\liminf$ and $\limsup$ rather than limits: average costs of policies need not exist as limits, even for bounded costs.

Formalizing it. Mathlib contains Abel's theorem for convergent series (Mathlib/Analysis/Complex/AbelLimit.lean) and Cesàro convergence of convergent sequences, but no Tauberian theorem. The pinned checkout has no file mentioning "Tauberian", and neither does the platform. The mathematics has been proved since 1914. Formalizing it here adds:

a machine-checked Hardy–Littlewood–Karamata theorem for nonnegative $[0,\infty]$ -valued sequences;
the $\liminf$ / $\limsup$ comparison (A.28) with infinite values allowed;
a reusable component for the average cost chapters of this series.

Difficulty

The Abelian inequalities (A.28) follow from rearranging the series. The converse (iii) ⇒ (ii) does not: the first idea, recovering $w_n/n$ from $(1-\alpha)U(\alpha)$ at $\alpha = 1 - 1/n$ , fails, because knowing $U$ near $1$ controls only weighted averages of all the $u_k$ , not a sharp truncation. Some positivity argument is unavoidable, since the converse fails for signed sequences (for example $u_n = (-1)^n n$ ). The sharp truncation at $n \approx (-\ln\alpha)^{-1}$ corresponds to the discontinuous weight $r$ . Passing from polynomial weights to the jump function $r$ requires uniform approximation together with the nonnegativity of the $u_n$ at every step.

The infinite values add bookkeeping. A single $u_{n_0} = \infty$ makes every term of (A.28) infinite, and $R < 1$ forces $U(\alpha) = \infty$ on $(R,1)$ .

Formalization scope

Conventions the statements commit to:

Values. Terms $u : \mathbb{N} \to [0,\infty]$ (ℝ≥0∞) with $u_0 \ne \infty$ . $U$ , the Abel means, $w_n$ and the Cesàro means are ℝ≥0∞-valued, with ℝ≥0∞ sums (no summability side conditions).
Limits. $\liminf$ and $\limsup$ are those of the complete lattice $[0,\infty]$ , never real liminf. "Exists and is finite" means convergence in $[0,\infty]$ to some $L \ne \infty$ .
Discount factor. $\alpha \in \mathbb{R}_{\ge 0}$ , and $\alpha \to 1^-$ is the filter 𝓝[<] 1.
Index $n = 0$ . $n \to \infty$ is atTop on $\mathbb{N}$ ; the value $w_0/0 = 0$ is irrelevant.
The equivalence is List.TFAE.
The function $r$ . Its value at the jump is $r(e^{-1}) = e$ (Fig. A.1).
Continuity. In Lemma A.4.1 and in the continuous-weight step, continuity is required on the closed interval $[0,1]$ , which is what the Weierstrass approximation step uses. The book writes " $(0,1)$ ".
Finite terms. Remark A.3.1 is stated for finite terms, which the book's discussion of the radius presumes.

A trivializing formalization is ruled out. Real-valued $\liminf$ / $\limsup$ would make (A.28) hold by junk values on unbounded sequences; hypotheses such as boundedness of $u_n$ would replace the theorem by an easier special case; and a definition of "exists and is finite" allowing $L = \infty$ would make (ii) hold for $u_n = n$ . None of these is used. As sanity checks: for $u_n \equiv 1$ all four terms of (A.28) equal $1$ , and for $u_n = n$ all equal $\infty$ and (i)–(iii) all fail.

A complete development needs:

Cauchy products of $[0,\infty]$ -valued power series;
the Weierstrass approximation theorem, which Mathlib has (polynomialFunctions.topologicalClosure);
interval integrals of step-like functions;
$\liminf$ / $\limsup$ manipulation along 𝓝[<] 1.

Reusable beyond this mission: the ℝ≥0∞ power-series toolkit and the Karamata argument for general continuous weights (milestone 8). Contributions welcome: proofs of any milestone, and alternative proofs of (iii) ⇒ (ii).

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix A.3–A.5, pp. 279–287. https://doi.org/10.1002/9780470317037
E. C. Titchmarsh, The Theory of Functions, 2nd ed., Oxford University Press, 1939, pp. 227–229 (Karamata's proof).
J. Karamata, "Über die Hardy–Littlewoodschen Umkehrungen des Abelschen Stetigkeitssatzes", Mathematische Zeitschrift 32 (1930), 319–320.
G. H. Hardy and J. E. Littlewood, "Tauberian theorems concerning power series and Dirichlet's series whose coefficients are positive", Proc. London Math. Soc. (2) 13 (1914), 174–191.
D. V. Widder, The Laplace Transform, Princeton University Press, 1941.
L. I. Sennott, "A new condition for the existence of optimum stationary policies in average cost Markov decision processes — unbounded cost case", Proc. 25th IEEE Conference on Decision and Control, Athens, 1986, pp. 1719–1721 (cited by the book as Sennott 1986b).
T. M. Liggett and S. A. Lippman, "Short notes: Stochastic games with perfect information and time average payoff", SIAM Review 11 (1969), 604–607. https://doi.org/10.1137/1011093

14 thms3 active usersReviewed

Completed

Analysis·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems XI: The Generalized Dominated Convergence Theorem for Approximating DistributionsTextbook

Motivation

Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) studies Markov decision chains with countably many states, finite action sets and unbounded nonnegative costs. Its main computational device, the approximating sequence method (Definition 2.5.1, p. 28), replaces the countable state space $S$ by an increasing sequence of state spaces $S_N$ and the transition law out of each state by distributions $P_j(N)$ on $S_N$ that converge pointwise to the original law. Every convergence argument of that method has the same shape: a sum $\sum_{j\in S_N} P_j(N)\,u(j,N)$ , an expected cost or value under the $N$ -th approximating model, must be shown to converge to $\sum_{j\in S} P_j\,u(j)$ , or at least to satisfy a one-sided bound in the limit.

Appendix A, Sections A.1–A.2 (pp. 270–278), collects the analysis results used for this. The author proves them for sums over countable sets rather than general integrals, so they need no measure theory, and the proofs of the discounted-cost and average-cost approximation theorems (Chapters 4 and 8) cite them. This mission formalizes that appendix section as a self-contained unit.

Setting

Let $S$ be a countable set and $(P_j)_{j\in S}$ a probability distribution on $S$ : $P_j\ge 0$ and $\sum_j P_j=1$ . Values of functions are extended reals in $[-\infty,\infty]$ , with the convention $0\cdot\infty=0$ . For $u:S\to[-\infty,\infty]$ , the weighted sum is

\sum_{j\in S}P_j\,u(j)=\sum_{j\in S}P_j\,u^+(j)-\sum_{j\in S}P_j\,u^-(j),

which is well defined, in $(-\infty,\infty]$ , whenever the negative parts have finite weighted sum. In Lean this is wsum P u.

A family of approximating distributions for $(P_j)$ consists of

an increasing sequence of subsets $S_0\subseteq S_1\subseteq\cdots$ of $S$ with $\bigcup_N S_N=S$ ;
for each $N$ , a probability distribution $(P_j(N))_{j\in S_N}$ on $S_N$ ;
pointwise convergence $\lim_{N\to\infty}P_j(N)=P_j$ for every $j\in S$ .

Since the sets increase to $S$ , a fixed state $j$ lies in $S_N$ for every large $N$ , so $\liminf_N u(j,N)$ and $\lim_N u(j,N)$ make sense for a function $u(j,N)$ defined only for $j\in S_N$ . In Lean these three conditions are the structure ApproxDist P SN Q, with Q N j $=P_j(N)$ .

Formalization targets

Goal: Theorem A.2.6 (Generalized Dominated Convergence Theorem), p. 278

Under the approximating-distribution hypotheses, let $u(j,N)$ and $w(j,N)$ be finite with $|u(j,N)|\le w(j,N)$ for $j\in S_N$ , let $u(j,N)\to u(j)$ and $w(j,N)\to w(j)$ for every $j$ , and assume

\lim_{N\to\infty}\sum_{j\in S_N}P_j(N)\,w(j,N)=\sum_{j\in S}P_j\,w(j)<\infty.

Then

\lim_{N\to\infty}\sum_{j\in S_N}P_j(N)\,u(j,N)=\sum_{j\in S}P_j\,u(j).

Milestones, in the book's order

Proposition A.1.3: $\liminf$ commutes with a minimum over a finite nonempty set; $\lim$ does too when all limits exist.
Proposition A.1.5: $\liminf_N\sum_{j\in G}u(j,N)\ge\sum_{j\in G}\liminf_N u(j,N)$ for finite $G$ and $u>-\infty$ , when the right side has no indeterminate form.
Proposition A.1.7: the same inequality for countable sums of $[0,\infty]$ -valued terms.
Proposition A.1.8: the same, with the left sum over $S_N$ increasing to $S$ .
Proposition A.1.10: $\liminf u_n\le\liminf w_n/n\le\limsup w_n/n\le\limsup u_n$ for $w_n=\sum_{k<n}u_k$ .
Proposition A.2.1 (Fatou's lemma): $\liminf_N\sum_jP_j u(j,N)\ge\sum_jP_j\liminf_N u(j,N)$ for $u\ge -L$ .
Theorem A.2.3 (dominated convergence, with a convergent dominating sequence $w(j,N)$ ) and Corollary A.2.4 (fixed dominating function).
Proposition A.2.5 (generalized Fatou's lemma):

\liminf_{N\to\infty}\sum_{j\in S_N}P_j(N)\,u(j,N)\ \ge\ \sum_{j\in S}P_j\,\liminf_{N\to\infty}u(j,N)\qquad(u\ge -L\text{ on }S_N).

Corollary A.2.7: bounded convergence under approximating distributions.

Significance

The results. Proposition A.2.5 and Theorem A.2.6 are the two limit interchanges the approximating sequence method needs. The generalized Fatou inequality gives the lower bound on limits of value functions of the approximating models, and the generalized dominated convergence theorem identifies the limit of expected costs when a dominating function is available. Corollary A.2.7 gives the bounded case, and Proposition A.1.3 moves limits inside the minimization of an optimality equation. Proposition A.1.10 compares Cesàro averages with the sequence itself, which the average-cost chapters use.

Formalizing them. All statements are classical and proved in the book. A.1.7, A.2.1, A.2.3 and A.2.4 are, after translation, instances of Mathlib's Fatou lemma (MeasureTheory.lintegral_liminf_le) and dominated convergence theorem for a discrete measure. The mission states them in the book's discrete, extended-real form so later chapters can cite them by number. The versions in which the distribution and its support change with $N$ (A.2.5–A.2.7) are not in Mathlib in this form; the generalized dominated convergence theorem appears in the measure-theoretic literature (Royden, Real Analysis, Ch. 4) but has no Lean formalization. None of these statements has been formalized for this book.

Difficulty

For the generalized results, Mathlib's Fatou lemma and dominated convergence theorem do not apply directly: they fix one measure, while here both the weights $P_j(N)$ and the support $S_N$ change with $N$ . The dominating function $w(j,N)$ also changes with $N$ and is not integrable uniformly in $N$ ; only the convergence of its expectations is assumed. For small $N$ , $\sum_{j\in S_N}P_j(N)w(j,N)$ may even be infinite, and then $\sum_{j\in S_N} P_j(N)u(j,N)$ has no value.

A second difficulty is bookkeeping in the extended reals. Lower limits may be $\pm\infty$ , products use $0\cdot\infty=0$ , and a sum with a $+\infty$ term and a $-\infty$ term is undefined. The inequality of Proposition A.1.5 holds only when that indeterminate form is excluded. The bound $u\ge -L$ in A.2.1 and A.2.5 cannot be dropped: Examples A.1.9 and A.2.2 of the book show the inequalities fail without it.

Formalization scope

Types. $S$ is any type with [Countable S]. Probabilities are ℝ≥0∞-valued with ∑' j, P j = 1, and $P_j(N)$ is Q N j. Extended-real values are EReal, and nonnegative extended values (A.1.7, A.1.8) are ℝ≥0∞. Limits and lower and upper limits are along atTop in ℕ. The book's $N\ge N_0$ convention (Remark A.1.2) needs nothing extra, since only large $N$ matter.
Sums over $S_N$ are sums over $S$ of (SN N).indicator (Q N) times the function. Values of $u(j,N)$ and $P_j(N)$ for $j\notin S_N$ never enter any statement, and the hypotheses on $u$ ( $u\ge -L$ , $|u|\le w$ ) are imposed only on $S_N$ , as in the book.
Weighted sums are wsum, the difference of the weighted positive and negative parts, each in [0,∞]. When both are infinite the book's sum is undefined and wsum returns $-\infty$ . Every sum used in a hypothesis or conclusion is defined, except possibly for finitely many $N$ in limit statements, where it does not matter.
Limits of $u(j,N)$ and $w(j,N)$ are taken in EReal, since the book allows extended-real limits (p. 271). The hypotheses force them to be finite wherever $P_j>0$ .
Ruled out. Statements in which wsum returns its junk value $-\infty$ could make an inequality trivial. Every left-hand side here is a lower limit of sums whose negative parts are bounded, or a limit of eventually defined sums, so no statement holds only because of that junk value. Real-valued tsum with its junk value $0$ is not used anywhere.
Welcome contributions. A proof of A.1.7 from lintegral_liminf_le for the counting measure, and lemmas relating wsum to Mathlib's tsum and to integrals against Measure.sum (fun j => P j • dirac j), can be reused by the other missions of this series.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Appendix A, pp. 270–278. https://doi.org/10.1002/9780470317037
H. L. Royden, Real Analysis, 3rd ed., Macmillan, 1988, Chapter 4 (Fatou's lemma, generalized Lebesgue convergence theorem).
The Mathlib Community, The Lean Mathematical Library, CPP 2020, https://doi.org/10.1145/3372885.3373824 (MeasureTheory.lintegral_liminf_le, MeasureTheory.tendsto_integral_of_dominated_convergence).

12 thms3 active usersReviewed

Dynamic Programming Operations Research Stochastic Systems·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems X: Average Cost Optimization of Continuous Time Markov Decision ChainsTextbook

Motivation

Many queueing systems evolve in continuous time: customers arrive according to a Poisson process, services take exponentially distributed times, and a controller may change the service rate, admit or reject customers, or route them whenever the state changes. Minimizing the long-run average cost of such a system is a standard problem in the control of queues (Lippman 1975; Puterman 1994, Ch. 11; Sennott 1999, Ch. 10). The continuous time model does not fit directly into the discrete time theory of Markov decision chains developed in the earlier chapters of Sennott's book, because time spent in a state now matters and the natural average cost is a ratio of expected cost to expected elapsed time.

This mission formalizes Sections 10.1–10.4 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999): the elementary properties of the exponential distribution, the continuous time Markov decision chain and its average cost, a reduction of the continuous time problem to an auxiliary discrete time Markov decision chain, and the theorem stating that finite state approximating sequences of the auxiliary chain compute optimal average costs and optimal stationary policies of the continuous time chain. The chapter closes with an explicit average cost computation for the M/M/1 queue with service rate control.

Setting

A random variable $X$ has the exponential distribution with rate $\mu>0$ if $P(X\le t)=1-e^{-\mu t}$ for $t\ge0$ . A function $r(\delta)$ is $o(\delta)$ if $r(\delta)/\delta\to0$ as $\delta\to0^+$ .

A continuous time Markov decision chain (CTMDC) $\Psi$ has a countable state space $S$ and, for each $i\in S$ , a finite nonempty action set $A_i$ . Choosing $a\in A_i$ in state $i$ incurs an instantaneous cost $G(i,a)\ge0$ and a cost rate $g(i,a)\ge0$ in effect until the next transition. The time until the next transition is exponential with rate $\nu(i,a)>0$ , so its mean is $\tau(i,a)=1/\nu(i,a)$ ; the next state is $j$ with probability $P_{ij}(a)$ , where $P_{ii}(a)=0$ . A policy $\theta$ chooses, at each transition, an action (possibly at random) from the history of past states, actions and sojourn times; a stationary policy $e$ chooses $e(i)$ in state $i$ . With $C_n$ the cost and $T_n$ the time of the first $n$ transition periods, the average cost and the minimum average cost are

J^\Psi_\theta(i)=\limsup_{n\to\infty}\frac{E_\theta[C_n\mid X_0=i]}{E_\theta[T_n\mid X_0=i]},\qquad J^\Psi(i)=\inf_\theta J^\Psi_\theta(i).

Assumption (CTB) requires constants $\tau$ and $B$ with $0<\tau<\inf_{i,a}\tau(i,a)\le\sup_{i,a}\tau(i,a)\le B<\infty$ . The auxiliary MDC $\Delta$ has the same states and actions, costs $C(i,a)=G(i,a)\nu(i,a)+g(i,a)$ , and transition probabilities $P^*_{ij}(a)=\tau\nu(i,a)P_{ij}(a)$ for $j\ne i$ , $P^*_{ii}(a)=1-\tau\nu(i,a)$ . Its average cost $J^\Delta_\theta(i)=\limsup_n n^{-1}\sum_{t<n}E_\theta[C(X_t,Y_t)]$ and minimum average cost $J^\Delta(i)$ are those of Chapter 2. Assumption (CTAC) is $J^\Delta(\cdot)\le J^\Psi(\cdot)$ .

An approximating sequence $(\Delta_N)_{N\ge N_0}$ for $\Delta$ uses finite state spaces $S_N$ increasing to $S$ and transition probabilities $P^*_{ij}(a;N)$ on $S_N$ converging to $P^*_{ij}(a)$ . The (AC) assumptions ask for constants $J^N$ and functions $r^N$ on $S_N$ solving

J^N+r^N(i)=\min_{a\in A_i}\Big\{C(i,a)+\sum_{j\in S_N}P^*_{ij}(a;N)\,r^N(j)\Big\},\qquad i\in S_N,\ N\ge N_0,\tag{10.21}

with $\limsup_N r^N(i)<\infty$ , $\liminf_N r^N(i)\ge-Q$ for a constant $Q\ge0$ , and $\limsup_N J^N=:J^*<\infty$ , $J^*\le J^\Delta(i)$ .

Formalization targets

Goal: Theorem 10.3.3

Under (CTB), (CTAC) and the (AC) assumptions for an approximating sequence of $\Delta$ :

J^*=\lim_{N\to\infty}J^N\ \text{exists and}\ J^\Delta(i)=J^\Psi(i)=J^*\quad(i\in S),

and every limit point $e^*$ of a sequence $e^N$ of stationary policies realizing the minimum in (10.21) satisfies $J^\Delta_{e^*}=J^\Delta$ and $J^\Psi_{e^*}=J^\Psi$ . The goal leaves the chain, the approximating sequence and the constants of (CTB) arbitrary.

Milestones

Proposition 10.1.2: $P(X>x+y\mid X>y)=P(X>x)$ for $x,y>0$ , and $P(X\le\delta)=\mu\delta+o(\delta)$ .
Proposition 10.1.3: for independent exponentials, $P(X_1\le\delta,X_2\le\delta)=o(\delta)$ , $P(X_1<X_2)=\mu_1/(\mu_1+\mu_2)$ , and $\min(X_1,X_2)$ is exponential with rate $\mu_1+\mu_2$ .
Lemma 10.3.1: if $z$ is bounded below and $Z\tau(i,e)+z(i)\ge G(i,e)+g(i,e)\tau(i,e)+\sum_jP_{ij}(e)z(j)$ for all $i$ (10.15), then $J^\Psi_e\le Z$ .
Lemma 10.3.2: $(Z,w)$ satisfies $Z+w(i)\ge C(i,e)+\sum_jP^*_{ij}(e)w(j)$ (10.20) if and only if $(Z,\tau w)$ satisfies (10.15).
Proposition 10.4.1: in the M/M/1 queue with arrival rate $\lambda$ , holding cost $H(i)=Hi$ and service cost rate $c(a)$ , the policy that always serves at rate $a>\lambda$ has average cost $\rho_ac(a)+H\rho_a/(1-\rho_a)$ , $\rho_a=\lambda/a$ .

Significance

The goal theorem turns the average cost control of a continuous time chain on an infinite state space into a finite computation: solve the optimality equation (10.21) of a finite truncation of the auxiliary chain, let the truncation grow, and read off the optimal average cost and an optimal stationary policy of the original continuous time chain. The auxiliary chain is the book's form of uniformization, and the result is what licenses the numerical study of the M/M/1 service rate control problem in Section 10.4 and of the M/M/K and polling models in Sections 10.5–10.6. Proposition 10.4.1 gives the closed-form benchmark against which the computed optimal policy is compared.

The results are proved in the book, some with details left to the reader (Lemma 10.3.2(ii), Problem 10.10), and the goal rests on Theorem 8.1.1 and Lemma 7.2.1 of the same book. None of them has, as far as a search of Mathlib and the Prove2Me catalogue shows, a machine-checked proof: Mathlib provides the exponential law (ProbabilityTheory.expMeasure) and its distribution function, but not memorylessness or the minimum of independent exponentials, and no continuous time Markov decision model. A formalization would supply these, together with a checked average cost comparison between a continuous time chain and its discrete time auxiliary chain.

Difficulty

The obvious argument compares the two chains policy by policy, but the policy classes differ: a policy for $\Delta$ may change action in every time slot, including slots where the state does not change, while a policy for $\Psi$ acts only at transitions and may use the observed sojourn times. Only the stationary policies coincide. The lower bound $J^\Psi\ge J^*$ therefore cannot be obtained by transferring policies, and it is exactly what Assumption (CTAC) supplies. The upper bound requires passing from the discrete time inequality (10.20) for the limit point $e^*$ to a bound on a ratio of expected cost to expected time in continuous time, where the denominator depends on the policy; the uniform bounds of (CTB) on the mean sojourn times are what control it. Inside Lemma 10.3.1 the function $z$ is only bounded below, so the telescoping of expectations must be justified without integrability of $z$ from above.

Formalization scope

The state space is a countable type S, actions a type Act, and action sets A i : Finset Act; the CTMDC and MDC structures hold data, and their axioms (nonempty action sets, nonnegative costs, positive rates, stochastic transition rows with $P_{ii}(a)=0$ ) are separate predicates. Transition probabilities are ℝ≥0∞-valued; costs, rates and the functions $z,w,r^N$ are real. Expected costs, expected times and all average costs are ℝ≥0∞-valued, so $+\infty$ is a legitimate value, and they are compared with real constants in EReal; the limits superior and inferior of (AC) are taken in EReal. The expected cost of $n$ transition periods under a general policy is a recursion over the periods in which the sojourn time is integrated against expMeasure ν(i,a) and the next state is drawn independently from $P_{i\cdot}(a)$ ; policies are measurable in the past sojourn times. In (10.15) and (10.20) the convergence of the series is part of the inequality. The strict inequality $\tau<\inf\tau(i,a)$ of (CTB) is kept strict (as a positive margin); weakening it to $\le$ would make $P^*_{ii}(a)$ vanish or turn negative.

The average cost $J^\Psi_\theta$ is a ratio of expectations, not the expectation of a ratio, and the infimum $J^\Psi$ ranges over history dependent randomized policies that may use sojourn times; replacing either by a stationary-only class, or dropping (CTAC), gives a different theorem.

A complete development needs: expected rewards of a chain with exponential holding times, the average cost theory of Chapter 8 for the auxiliary chain (Theorem 8.1.1 and Lemma 7.2.1, restated here as needed), and renewal-reward reasoning for Proposition 10.4.1. The exponential-distribution lemmas are reusable beyond this mission and are welcome as independent contributions.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, John Wiley & Sons, 1994. https://doi.org/10.1002/9780470316887
S. A. Lippman, Applying a new device in the optimization of exponential queuing systems, Operations Research 23(4), 687–710, 1975. https://doi.org/10.1287/opre.23.4.687
D. Gross and C. M. Harris, Fundamentals of Queueing Theory, 3rd ed., John Wiley & Sons, 1998.

10 thms3 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems IX: Bounded Mean Residual Lifetimes Imply Finite Moments of All OrdersTextbook

Motivation

In a discrete-time queue the service of a customer lasts a random number $Y$ of slots. When such a system is modelled as a Markov decision chain (Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, DOI 10.1002/9780470317037, Chapter 9), the state must record how much service is still owed, and the controller only observes that a service has lasted $s$ slots and is not yet finished. The relevant random quantity is then the residual life $Y_s$ : the remaining service time given that $s$ slots have elapsed without completion. Verifying the book's average cost assumptions for such a model requires bounds on expected first passage times and costs, and these reduce to moment bounds on $Y$ and on the residual lives $Y_s$ .

Section 9.2 isolates a single condition that makes those bounds available: the expected remaining service time is bounded uniformly in the elapsed time. The concept of mean residual life comes from reliability theory, where $Y$ is the lifetime of a component and $E[Y_s]$ is its expected remaining lifetime at age $s$ . This mission formalizes Section 9.2 of the book, together with the moment computation for batch arrivals (Lemma 9.5.2) that the same verification uses.

Setting

Let $Y$ be a random variable with values in $\{1,2,3,\dots\}$ and distribution $u_y = P(Y = y)$ , $y \ge 1$ . Write $F(y) = P(Y \le y)$ and $F^*(y) = P(Y > y) = 1 - F(y)$ for $y \ge 0$ , so $F(0) = 0$ and $F^*(0) = 1$ . The $k$ -th moment is

E[Y^k] = \sum_{y \ge 1} y^k u_y \in [0,\infty].

For $s \ge 0$ with $F^*(s) > 0$ , the residual life $Y_s$ has distribution

P(Y_s = y) = P(Y = s + y \mid Y > s) = \frac{u_{s+y}}{F^*(s)}, \qquad y \ge 1,

with $Y_0 = Y$ ; its tail is $F^*_s(y) = F^*(s+y)/F^*(s)$ , and $E[Y_s]$ is the mean residual lifetime.

The distribution of $Y$ has bounded mean residual lifetimes (BMRL- $U$ , Definition 9.2.4) if there is a finite constant $U$ with

E[Y_s] \le U \qquad \text{for every } s \ge 0 \text{ with } F^*(s) > 0,

and it is BMRL if it is BMRL- $U$ for some $U$ .

Three families appear by name: the geometric distribution $\mathrm{geo}(\mu)$ of the number of Bernoulli( $\mu$ ) trials to the first success, $P(Y=y) = \mu(1-\mu)^{y-1}$ ; the negative binomial $\mathrm{neg\,bin}(\mu, r)$ of the number of trials to the $r$ -th success, $P(Y = y) = \binom{y-1}{r-1}\mu^r(1-\mu)^{y-r}$ for $y \ge r$ ; and the truncated Poisson $\mathrm{trun\,Pois}(\lambda)$ , $P(Y=y) = \frac{e^{-\lambda}}{1-e^{-\lambda}}\frac{\lambda^y}{y!}$ for $y \ge 1$ .

For Lemma 9.5.2, batches of customers arrive in each slot; the batch sizes $X_1, X_2, \dots$ are independent with common distribution $p_j$ , mean $\lambda = \sum_j j p_j$ and second moment $\lambda^{(2)} = \sum_j j^2 p_j$ , and $X(s) = X_1 + \dots + X_s$ is the number of arrivals in $s$ slots.

Formalization targets

Goal: Proposition 9.2.5

If the distribution of $Y$ is BMRL, then

E[Y^k] < \infty \qquad \text{for every } k.

The goal fixes no constant: it asserts only that a uniform first-moment bound on the residual lives forces every moment of $Y$ to be finite.

Milestones

Proposition 9.2.1. $E[Y] = \sum_{y=0}^\infty F^*(y)$ and, for $k \ge 2$ ,

E[Y^k] = 1 + \sum_{z=0}^{k-1}\binom{k}{z}\left[\sum_{y=1}^\infty y^z F^*(y)\right]. \tag{9.4}

Remark 9.2.2. For $k \ge 2$ , $E[Y^k] < \infty$ if and only if $\sum_y y^{k-1}F^*(y) < \infty$ .
Proposition 9.2.3. For a positive integer $k$ , $E[Y^k] < \infty$ implies $E[Y_s^k] < \infty$ for all $s \ge 0$ .
Proposition 9.2.6. The geometric ( $0<\mu<1$ ), negative binomial ( $0<\mu<1$ , $r \ge 2$ ) and truncated Poisson ( $\lambda > 0$ ) distributions are BMRL.
Lemma 9.5.2. Under $\lambda^{(2)} < \infty$ ,

E[X(s)] = \lambda s, \qquad E[(X(s))^2] = \lambda^{(2)}s + \lambda^2 s(s-1). \tag{9.25}

Significance

The result itself. Proposition 9.2.5 turns a condition that is easy to check for concrete service distributions, and natural for services (a service whose expected remaining duration grows without bound as it goes on is undesirable), into the moment bounds that the average cost analysis consumes. With Proposition 9.2.6 it shows that the most common unbounded service distributions on $\{1,2,\dots\}$ have finite moments of all orders; with Lemma 9.5.2 it supplies the linear and quadratic growth of expected arrivals and their second moments that the verification of the (WAC) assumptions for the batch-arrival queue of Example 9.3.1 needs (Section 9.5). Every bounded distribution is BMRL as well (the book's Problem 9.3).

Formalizing it. All results here are proved in the book; none has a machine-checked proof on the platform or in Mathlib, which has geometric and Poisson distributions but no residual lives, negative binomial or truncated Poisson laws. A complete development gives a reusable tail-sum calculus for moments of $\mathbb N$ -valued random variables in $[0,\infty]$ , a residual-life construction for discrete distributions, and the BMRL property of three standard families. The platform's mean residual life order (the "Stochastic Orders II" mission, Shaked–Shanthikumar) compares two variables; BMRL is a uniform bound on one variable's residual lives and is not an order, so none of that material states these results.

Difficulty

BMRL controls only first moments, of the conditional laws $Y_s$ ; the goal asks for moments of every order of $Y$ itself. Bounding $E[Y^k]$ by expanding $E[Y_s]$ for each fixed $s$ gives nothing, because each single bound is compatible with a heavy tail: the uniformity in $s$ is essential. The residual lives are also only defined where $P(Y > s) > 0$ , so every argument must handle distributions with bounded support separately. Proposition 9.2.6 requires explicit control of ratios of tail sums for three families; for the negative binomial and truncated Poisson the tails have no closed form.

Formalization scope

$Y$ is represented by its law, a function $u : \mathbb N \to [0,\infty]$ with $\sum_y u_y = 1$ and $u_0 = 0$ (IsDistOnPos). $F^*$ , moments and residual-life moments are ℝ≥0∞-valued series; an infinite moment is $+\infty$ and "finite" means $< \infty$ . No Bochner integral is used, so a finite-moment conclusion cannot hold vacuously through an integrability default.
The residual life $Y_s$ is defined by (9.7) and is used only where $F^*(s) > 0$ ; BMRL- $U$ is required exactly at those $s$ , and $U$ is a finite nonnegative real. A formalization requiring the bound at every $s$ with a junk value of $E[Y_s]$ where $F^*(s) = 0$ is ruled out: the definitions never divide by $F^*(s) = 0$ in a used position, and bounded distributions remain BMRL.
The geometric and negative binomial laws count trials (support starting at $1$ and $r$ ), not failures as Mathlib's geometricPMF does.
Lemma 9.5.2 is stated on a probability space with measurable, mutually independent (iIndepFun) batch sizes of common law $p$ , expectations as lower Lebesgue integrals, and only assumption (BA1), $\lambda^{(2)} < \infty$ , which is the part of the book's (BA) that concerns arrivals.
Welcome contributions: the tail-sum identity (9.4) and its reindexing lemmas, the residual-life tail formula (9.8) and moment formula (9.9), each as a separate lemma; and proofs that the three named families are probability distributions on their supports.

Selected references

Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Section 9.2 (pp. 202–206) and Section 9.5 (pp. 214–215). DOI 10.1002/9780470317037
Moshe Shaked and J. George Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Section 2.A (the mean residual life order). DOI 10.1007/978-0-387-34675-5

8 thms3 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems IV: Average Cost Optimal Stationary Policies Exist for Finite State SpacesTextbook

Why average cost on finite state spaces

Controlled queues, inventories and communication links are run for a long time, and the quantity an operator usually cares about is the long-run average cost per period rather than a discounted total. The average cost criterion is harder to work with than the discounted one: its value is a $\limsup$ of Cesàro means, it is not given by a contraction, and for general (history dependent, randomized) policies the limit need not exist. Chapter 6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) treats the case of a finite state space, where the strongest results hold: an average cost optimal policy exists, can be taken stationary, and can be obtained as a limit of discount optimal policies as the discount factor tends to one.

The results go back to D. Blackwell, "Discrete dynamic programming", Ann. Math. Statist. 33 (1962), who showed that for finite states and actions some stationary policy is discount optimal for all discount factors close to one. Such a policy is now called Blackwell optimal. Sennott's Chapter 6 derives average cost optimality of this policy and the multichain average cost optimality equation from it, in the notation used throughout the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$ , a finite nonempty action set $A_i$ in each state $i$ , nonnegative finite costs $C(i,a)$ , and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a) = 1$ . A policy $\theta$ chooses the action at time $t$ from a distribution $\theta(\cdot \mid h_t)$ on $A_{i_t}$ that may depend on the whole history $h_t = (i_0,a_0,\ldots,i_t)$ . A stationary policy $f$ always chooses a fixed action $f(i) \in A_i$ in state $i$ .

With $X_t, A_t$ the state and action at time $t$ and $X_0 = i$ , define

the discounted cost $V_{\theta,\alpha}(i) = \sum_{t \ge 0} \alpha^t E_\theta[C(X_t,A_t)]$ for $0<\alpha<1$ , and the discounted value function $V_\alpha(i) = \inf_\theta V_{\theta,\alpha}(i)$ ;
the $n$ horizon cost $v_{\theta,n}(i) = \sum_{t=0}^{n-1} E_\theta[C(X_t,A_t)]$ ;
the average cost $J_\theta(i) = \limsup_n v_{\theta,n}(i)/n$ , its $\liminf$ version $J^*_\theta(i)$ , and the minimum average cost $J(i) = \inf_\theta J_\theta(i)$ .

All infima range over all general policies, and every quantity may equal $+\infty$ . A policy is $\alpha$ discount optimal if $V_{\theta,\alpha} = V_\alpha$ , and average cost optimal if $J_\theta = J$ .

For a stationary policy $f$ on a finite state space, the induced Markov chain splits into positive recurrent classes $R_1,\ldots,R_K$ and transient states. With $p_k(i)$ the probability of reaching $R_k$ from $i$ , distinguished states $z_k \in R_k$ , and $W_\alpha(i) = \sum_k p_k(i) V_\alpha(z_k)$ , the relative value function is $w_\alpha(i) = V_\alpha(i) - W_\alpha(i)$ .

Formalization targets

Goal: Proposition 6.2.3

For an MDC with a finite state space there are $\alpha_0 \in (0,1)$ and one stationary policy $f$ such that $f$ is $\alpha$ discount optimal for every $\alpha \in (\alpha_0,1)$ , $f$ is average cost optimal, and

J(i) = \lim_{\alpha\to 1^-} (1-\alpha) V_\alpha(i) = \lim_{n\to\infty} \frac{v_{f,n}(i)}{n}, \qquad i \in S.

Milestones

Proposition 4.5.3. For finite $S$ and stationary $e$ , $\alpha \mapsto V_{e,\alpha}(i)$ is a finite, continuous, rational function on $(0,1)$ .
Proposition 6.1.1. For every policy on a countable state space,

J^*_\theta(i) \le \liminf_{\alpha\to1^-}(1-\alpha)V_{\theta,\alpha}(i) \le \limsup_{\alpha\to1^-}(1-\alpha)V_{\theta,\alpha}(i) \le J_\theta(i),

with three equivalent conditions for equality. 3. Proposition 6.2.2. For finite $S$ and stationary $e$ , $J_e(i) = \lim_{\alpha\to1^-}(1-\alpha)V_{e,\alpha}(i) = \lim_n v_{e,n}(i)/n$ . 4. Proposition 4.5.1, Proposition 4.5.4, Corollary 4.5.5. The power series structure of $V_{\theta,\alpha}$ in $\alpha$ ; monotonicity and left continuity of $V_\alpha$ ; continuity under bounded costs. 5. Theorem 6.3.1. For the policy $f$ of the goal, $\lim_{\alpha \to 1^-} w_\alpha(i) = w(i)$ exists, and

J(i) + w(i) = C(i,f) + \sum_j P_{ij}(f) w(j) \ \ge\ \min_{a} \Big\{C(i,a) + \sum_j P_{ij}(a) w(j)\Big\},

together with the limit identities (i)–(iii) and the optimality criterion (v). 6. Proposition 6.3.3. $V_\alpha(i) = J(i)/(1-\alpha) + w^*(i) + \varepsilon_\alpha(i)$ with $\varepsilon_\alpha(i) \to 0$ as $\alpha \to 1^-$ .

Significance

The goal says that on a finite state space nothing is gained by randomizing or by remembering the past when minimizing average cost, and that the minimum average cost is the vanishing-discount limit of the discounted value function. This justifies computing average cost optimal policies through discounted problems and value iteration, the route taken in the rest of Chapter 6 and, via approximating sequences, for countable state spaces in Chapters 7 and 8. Theorem 6.3.1 supplies an optimality equation without any unichain or communication assumption. The book's Example 6.3.2 shows that the inequality in that equation can be strict, and that a stationary policy attaining the minimum need not be optimal.

The results are classical and proved in the book. No machine-checked version of them is known to exist. The platform has average-reward results for unichain finite MDPs with Markov policies (the Puterman series) and an average-cost optimality equation under recurrence assumptions (the Bertsekas series). Neither covers existence of a Blackwell optimal policy against the class of all history dependent randomized policies, or the multichain equation. A formal development also yields reusable infrastructure: the law of a controlled process under a general policy, first passage quantities of finite chains, and the Abelian inequality between Abel and Cesàro means of a nonnegative sequence.

Difficulty

The obvious argument picks, for each $\alpha$ , a stationary discount optimal policy $f_\alpha$ and lets $\alpha \to 1$ . Finiteness of the set of stationary policies gives one policy that is optimal along some sequence $\alpha_n \to 1$ , but not on an interval. Excluding infinite switching between two policies requires the analytic structure of $\alpha \mapsto V_{f,\alpha}(i)$ (Proposition 4.5.3), which in turn rests on matrix inversion of $I - \alpha P$ . Passing from the discounted criterion to the average one requires an Abelian inequality for nonnegative series whose terms may be infinite (Proposition 6.1.1), and comparison against general policies rules out any argument that works only within stationary or Markov policies. For Theorem 6.3.1 the difficulty is the multichain structure: the relative value function has to be assembled class by class from first passage times and costs, and its limit must be identified.

Formalization scope

States form a type S; [Countable S] for Section 4.5 and Proposition 6.1.1, [Fintype S] from Section 6.2 on, as in the book. Actions form a type Act with A i : Finset Act nonempty. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞.
A general policy is a function of the list of past state-action pairs (most recent first) and the current state, giving a distribution on A i. Stationary policies embed as degenerate policies. The law of the process is built from this data, and every infimum ranges over all general policies.
$V_{\theta,\alpha}$ , $V_\alpha$ , $v_{\theta,n}$ , $J_\theta$ , $J^*_\theta$ , $J$ are in ℝ≥0∞, so $+\infty$ is represented. $\alpha \to 1^-$ is the filter 𝓝[<] 1. On a finite state space these quantities are finite. The real valued objects of Section 6.3 ( $w_\alpha$ , $w$ , $w^*$ , equation (6.6)) are therefore formed with toReal, and this switch from ℝ≥0∞ to ℝ happens only in Theorem 6.3.1 and Proposition 6.3.3.
The objects of Section 6.3 ( $p_k$ , $m_{i|k}$ , $c_{i|k}$ , $\pi_s$ , $W_\alpha$ ) are defined from $f$ . The distinguished states are a hypothesis quantified over.
A trivializing formalization would take the infimum over stationary policies only, let the optimal policy depend on $\alpha$ , or state rationality as an equation p/q without requiring $q \ne 0$ . Each is excluded here: $J$ and $V_\alpha$ are infima over all general policies, one pair $(\alpha_0,f)$ is quantified before all $\alpha$ , and the denominator is required to be nonzero on $(0,1)$ .

Useful infrastructure includes rational functions of one real variable and their finitely many sign changes, the resolvent $(I-\alpha P)^{-1}$ of a stochastic matrix, the Abelian inequality for $[0,\infty]$ -valued sequences, and renewal-reward identities for finite chains. Contributions of general lemmas on these topics are welcome, as are proofs of individual milestones.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
D. Blackwell, "Discrete dynamic programming", Annals of Mathematical Statistics 33 (1962), 719–726. https://doi.org/10.1214/aoms/1177704593
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

13 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Stochastic Systems·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems II: The Discount Optimality EquationTextbook

Motivation

Control problems for queueing systems (admission control, routing, service rate selection, inventory replenishment) are naturally modelled as Markov decision chains with a countable state space, such as the number of customers in a buffer, and with costs that grow without bound in the state, such as holding costs proportional to queue length. The expected discounted cost criterion is the first infinite horizon criterion applied to such models, and it is also the tool through which the average cost criterion is treated later in the same book (Chapters 6–8 of Sennott's text reach average cost optimal policies through limits of discounted problems as the discount factor tends to one).

Classical treatments of discounted dynamic programming assume bounded costs, under which the dynamic programming operator is a contraction and has a unique bounded fixed point. That assumption fails for queueing models. This mission formalizes Chapter 4, Sections 4.1–4.4, of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999), which develops the discounted theory for nonnegative, possibly unbounded costs, where value functions may be infinite.

Timeline of the underlying theory:

1965. Blackwell (Ann. Math. Statist. 36) establishes the discounted theory with bounded rewards.
1966. Strauch (Ann. Math. Statist. 37) treats "negative" dynamic programming, the case of nonpositive rewards (equivalently nonnegative costs), with no boundedness assumption.
1977–1978. Bertsekas (SIAM J. Control Optim. 15) and Bertsekas and Shreve (Stochastic Optimal Control: The Discrete-Time Case) give the abstract monotone-mapping framework covering both cases.
1999. Sennott's text states the countable-state, finite-action, nonnegative-cost discounted theory in the form used for queueing control, with general history-dependent randomized policies.

Setting

A Markov decision chain $\Delta$ has a countable state space $S$ ; for each state $i$ a finite nonempty action set $A_i$ ; for each $a \in A_i$ a nonnegative finite cost $C(i,a)$ and a probability distribution $(P_{ij}(a))_{j \in S}$ of the next state. A policy $\theta$ chooses the action at time $n$ at random from a distribution $\theta(\cdot \mid h_n)$ on $A_{i_n}$ that may depend on the entire history $h_n = (i_0, a_0, \dots, a_{n-1}, i_n)$ . A stationary policy $f$ always chooses $f(i) \in A_i$ in state $i$ ; for it one writes $C(i,f) = C(i,f(i))$ and $P_{ij}(f) = P_{ij}(f(i))$ .

Fix a discount factor $\alpha \in (0,1)$ . For an initial state $i$ and a policy $\theta$ , the $n$ -horizon cost with terminal cost zero and the infinite horizon discounted cost are

v_{\theta,\alpha,n}(i) = \sum_{t=0}^{n-1} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i], \qquad V_{\theta,\alpha}(i) = \sum_{t=0}^{\infty} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i],

and the value functions are $v_{\alpha,n}(i) = \inf_\theta v_{\theta,\alpha,n}(i)$ and $V_\alpha(i) = \inf_\theta V_{\theta,\alpha}(i)$ , infima over all policies. All of these lie in $[0,\infty]$ . A policy is discount optimal if $V_{\theta,\alpha} = V_\alpha$ . The discount optimality equation is

W(i) = \min_{a \in A_i} \Big\{ C(i,a) + \alpha \sum_j P_{ij}(a) W(j) \Big\}, \qquad i \in S. \tag{4.9}

With $W = V_\alpha$ , $B_i(\alpha)$ denotes the set of actions attaining the minimum at $i$ .

Formalization targets

Goal: Theorem 4.1.4

$V_\alpha$ solves (4.9); every $W : S \to [0,\infty]$ solving (4.9) satisfies $V_\alpha \le W$ ; and every stationary policy $f_\alpha$ with

C(i,f_\alpha) + \alpha \sum_j P_{ij}(f_\alpha) V_\alpha(j) = \min_a \Big\{ C(i,a) + \alpha \sum_j P_{ij}(a) V_\alpha(j) \Big\} \quad \text{for all } i

is discount optimal. No boundedness of costs and no finiteness of $V_\alpha$ is assumed.

Milestones

In attack order: Lemma 4.1.1 ( $v_{\theta,\alpha,n} \uparrow V_{\theta,\alpha}$ ); Proposition 4.1.2 (a supersolution of the one-policy equation dominates $v_{e,\alpha,n} + \alpha^n E_e[W(X_n)]$ and $V_{e,\alpha}$ ); Corollary 4.1.3 (a supersolution of the optimality inequality dominates $V_{f,\alpha} \ge V_\alpha$ ); then, beyond the goal, Corollary 4.1.5 ( $\alpha^n E_{f_\alpha}[V_\alpha(X_n) \mid X_0 = i] \to 0$ where $V_\alpha(i) < \infty$ ), Proposition 4.2.2 and Corollary 4.2.4 (conditions under which a solution of (4.9) equals $V_\alpha$ ), Proposition 4.3.1 ( $v_{\alpha,n} \uparrow V_\alpha$ , and limit points of finite horizon optimal stationary policies are discount optimal) and Proposition 4.4.1 (optimal policies are exactly those concentrated on the sets $B_{i}(\alpha)$ along histories of positive probability).

Significance

Theorem 4.1.4 is the foundation for everything in the book that concerns discounted costs: it produces an optimal stationary deterministic policy, identifies $V_\alpha$ among the many solutions of (4.9) (Example 4.2.1 of the book gives a one-parameter family of finite solutions), and underlies value iteration (Proposition 4.3.1) and the approximating-sequence method of Sections 4.6–4.7. The average cost results of Chapters 6–8 are proved from it by letting $\alpha \to 1$ . Proposition 4.4.1 describes the full set of optimal policies, including randomized and history-dependent ones.

These are known results with published proofs. The contribution of this mission is a machine-checked development of the discounted theory for countable state spaces with unbounded costs and infinite values, over the general policy class. Related statements on the platform (the monotone-mapping propositions of Bertsekas 1977 in the MonotoneDP missions, and bounded-cost or finite-state discounted results) use different models and are open; no machine-checked proof of the present statements is known to this mission.

Difficulty

The contraction argument that settles the bounded case is unavailable: with unbounded costs the operator in (4.9) has many fixed points, and $V_\alpha$ can equal $+\infty$ at some states, so neither uniqueness of fixed points nor subtraction of values is available. The optimality equation compares the infimum over all history-dependent randomized policies with a one-step minimum, so the general policy class and the law of the process under it must be handled directly; restricting attention to Markov or stationary policies begs the question. Every limit exchange (monotone limits of finite horizon costs, the passage to limit points of policies in Proposition 4.3.1) takes place in $[0,\infty]$ , where finite-valued arguments do not transfer verbatim.

Formalization scope

The Lean development lives in the namespace SennottDP.Discounted. Conventions:

The state space is a type S with [Countable S]; actions form a type Act and A i : Finset Act is nonempty. Costs are ℝ≥0; transition probabilities are ℝ≥0∞ with ∑' j, P i a j = 1 for a ∈ A i.
A history at time $n$ is a pair Fin (n+1) → S, Fin n → Act; a policy assigns to every history a distribution on the action set of its last state. The probability of a history is the product of the policy and transition probabilities; expectations are ℝ≥0∞ sums over histories, so no integrability conditions arise.
All values ( $v_{\theta,\alpha,n}$ , $V_{\theta,\alpha}$ , $v_{\alpha,n}$ , $V_\alpha$ , and the competing solutions $W$ ) are ℝ≥0∞-valued; $0 \cdot \infty = 0$ . The discount factor is α : ℝ≥0 with 0 < α and α < 1. Terminal costs are zero.
$V_\alpha$ and $v_{\alpha,n}$ are infima over the type of all general policies. Defining them over stationary policies only would make the optimality of $f_\alpha$ a tautology; that formalization is ruled out.
Proposition 4.4.1: the book states the equivalence without a finiteness assumption, but its necessity argument needs $V_\alpha < \infty$ , and necessity fails otherwise. Sufficiency is stated in general and necessity under $V_\alpha < \infty$ everywhere.

Useful infrastructure, reusable by the later missions of this series (approximating sequences, average cost): the shift of a general policy after its first step, the Chapman–Kolmogorov identity for the history law, and the computation $E_f[W(X_{n+1})] = E_f[\sum_j P_{X_n j}(f) W(j)]$ for stationary policies. Contributions of such lemmas, and proofs of any milestone, are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Chapter 4. https://doi.org/10.1002/9780470317037
D. Blackwell, Discounted dynamic programming, Annals of Mathematical Statistics 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
R. E. Strauch, Negative dynamic programming, Annals of Mathematical Statistics 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM Journal on Control and Optimization 15 (1977), 438–464. https://doi.org/10.1137/0315031
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

12 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Stochastic Systems·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems I: Finite Horizon Optimality and Approximating SequencesTextbook

Motivation

Controlled queueing systems (admission control, routing, service-rate selection) are naturally modelled as Markov decision chains whose state is a buffer content and therefore ranges over a countably infinite set. Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, DOI 10.1002/9780470317037) develops the dynamic programming theory for exactly this setting: countable state space, finite action sets, nonnegative and possibly unbounded costs, and value functions that are allowed to be infinite. The book's computational method, the approximating sequence method (ASM), replaces the infinite chain by a sequence of finite truncations and asks when optimal values and policies of the truncations converge to those of the original chain.

This mission is the first of a series on the book. It covers Chapter 3, finite horizon optimization, together with the model of Chapter 2 and three results from Appendices A and B that the chapter uses. The finite horizon theory is the entry point: it is where the book's general policy class, its extended-valued cost criteria and its approximating sequences are first used together.

Setting

A Markov decision chain $\Delta$ has a countable state space $S$ ; for each $i \in S$ a finite nonempty action set $A_i$ ; a finite cost $C(i,a) \ge 0$ ; and for each $a \in A_i$ a transition distribution $(P_{ij}(a))_{j \in S}$ . A history at time $t$ is $h_t = (i_0, a_0, \dots, i_{t-1}, a_{t-1}, i_t)$ , and a general policy $\theta$ chooses the action at time $t$ from a distribution $\theta(\cdot \mid h_t)$ on $A_{i_t}$ : it may use the whole history and may randomize. Stationary policies $f$ ( $f(i) \in A_i$ ) and deterministic Markov policies (a stationary policy for each time) are special cases.

Fix a finite terminal cost $F \ge 0$ and a discount factor $0 < \alpha \le 1$ ( $\alpha = 1$ is the undiscounted case). The $n$ horizon expected discounted cost of $\theta$ from initial state $i$ is

v_{\theta,\alpha,n}(i) = \sum_{t=0}^{n-1} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i] + \alpha^n E_\theta[F(X_n) \mid X_0 = i],

and the value function is $v_{\alpha,n}(i) = \inf_\theta v_{\theta,\alpha,n}(i)$ over all general policies. Both may be $+\infty$ . A policy is optimal for the $n$ horizon if it attains $v_{\alpha,n}(i)$ at every $i$ . For $n \ge 1$ put $u_{\alpha,n}(i,a) = C(i,a) + \alpha \sum_j P_{ij}(a) v_{\alpha,n-1}(j)$ and let $B_i(\alpha,n)$ be the set of $a \in A_i$ minimizing it.

An approximating sequence $(\Delta_N)_{N \ge N_0}$ has finite nonempty state spaces $S_N$ increasing to $S$ , the same actions and costs, and transition distributions $P_{ij}(a;N)$ on $S_N$ converging to $P_{ij}(a)$ as $N \to \infty$ . Its value functions are $v^N_{\alpha,n}$ . In an augmentation type approximating sequence, the probability $P_{ir}(a)$ of leaving $S_N$ to $r$ is redistributed over $S_N$ by an augmentation distribution $q_j(i,a,r,N)$ . Assumption FH( $\alpha$ , $n$ ) requires $\limsup_N v^N_{\alpha,n}(i)$ to be finite and at most $v_{\alpha,n}(i)$ for every $i$ . A stationary policy $e$ is a limit point of stationary policies $e^N$ if, along a subsequence, $e^{N_r}(i) = e(i)$ eventually for each $i$ .

Formalization targets

Goal: Theorem 3.2.3

For fixed $n \ge 1$ ,

\Big(\forall i:\ \lim_{N\to\infty} v^N_{\alpha,n}(i) = v_{\alpha,n}(i) < \infty\Big) \iff \mathrm{FH}(\alpha,n),

and under either condition every limit point $e_n$ of stationary policies $e^N_n$ with $e^N_n(i) \in B^N_i(\alpha,n)$ satisfies $e_n(i) \in B_i(\alpha,n)$ for all $i \in S$ .

Milestones

Proposition A.1.1: a probability average of $u$ is at least $\min u$ , with equality iff the distribution is concentrated on the minimizers.
Theorem 3.1.2: the finite horizon optimality equation $v_{\alpha,n}(i) = \min_a u_{\alpha,n}(i,a)$ , and the characterization of all optimal general policies.
Corollary 3.1.4: choosing $f_{n-t}(i) \in B_i(\alpha,n-t)$ yields an optimal deterministic Markov policy.
Proposition 2.5.6: the augmentation (2.19) defines an approximating distribution.
Lemma 3.2.2: $v^N_{\alpha,0} \to v_{\alpha,0}$ and $\liminf_N v^N_{\alpha,n} \ge v_{\alpha,n}$ .
Propositions B.3 and B.5: sequences of stationary policies, for $\Delta$ or for $(\Delta_N)$ , have limit points.
Propositions 3.3.1, 3.3.2 and 3.3.4: three sufficient conditions for FH( $\alpha$ , $n$ ), namely bounded costs, an augmentation sending excess probability to a finite set, and the augmentation inequality (3.20).

Significance

Theorem 3.1.2 is the finite horizon dynamic programming equation in the generality the rest of the book needs: the value function is an infimum over history-dependent randomized policies, and the equation holds with infinite values allowed. Its characterization of optimal policies is Bellman's principle of optimality in necessary-and-sufficient form. Corollary 3.1.4 shows that deterministic Markov policies suffice. The discounted chapter builds on these results, since its value function is the limit of finite horizon ones, and so does the value iteration algorithm of the average cost chapters.

Theorem 3.2.3 is the finite horizon case of the approximating sequence method. It says exactly when finite truncations give the right answer, and it reduces the question to Assumption FH, for which Section 3.3 gives checkable conditions. The same structure (a lim inf inequality, a lim sup assumption, a limit point of optimal truncated policies) recurs for the discounted and the average cost criteria in later chapters.

The results are proved in the book. None of them is formalized: the platform has finite horizon dynamic programming only for Markov policies, abstract monotone mappings or finite reward-maximizing MDPs, and nothing on approximating sequences. A formalization contributes a Lean model of Markov decision chains with general policies and extended-valued criteria, which the later missions of the series restate and can merge with this one.

Difficulty

The obvious proof of the optimality equation conditions on the first action and state and then applies the induction hypothesis to the rest of the trajectory. With general policies the rest of the trajectory is governed by a continuation policy that depends on the first state and action, and the decomposition of the path law into a first step and a continuation must be proved from the definition of the process, not assumed. Infinite values also make the "only if" direction delicate: a strict inequality between expected costs becomes an equality once both sides are infinite.

For approximating sequences, the natural idea is to pass to the limit in the optimality equation of $\Delta_N$ . This fails in general. Example 3.2.1 of the book has $\lim_N v^N_{1,2}(0) = 2 > 1 = v_{1,2}(0)$ , because truncation moves probability onto states of high cost and dominated convergence is not available. Only the lim inf inequality holds for free, through a generalized Fatou lemma for approximating distributions. The lim sup side is exactly what Assumption FH supplies. The limit point argument then needs the compactness statement of Appendix B and the fact that a lim inf can be passed through a minimum over a finite set.

Formalization scope

The state space is a type S with [Countable S], the actions a type Act, and A i : Finset Act is nonempty. Costs are ℝ≥0, transition probabilities ℝ≥0∞ summing to 1 over S, and all values and expectations are in ℝ≥0∞, so infima over policies are lattice infima and +∞ is a genuine value. A history is the list of past state–action pairs, most recent first, with the current state, and a policy gives a distribution on A i for every history. Expectations are sums over histories of the path probabilities $\prod \theta(a_s \mid h_s) P_{i_s i_{s+1}}(a_s)$ , which is the book's (2.6) and (2.9), not the dynamic programming recursion. The discount factor satisfies $0 < \alpha \le 1$ in every statement. An approximating sequence is indexed by $N \in \mathbb N$ with a start level $N_0$ ; its value functions are set to $0$ for the finitely many $N$ at which a given state is not yet in $S_N$ , which does not affect limits.

The optimality equation must not be made definitional by defining $v_{\theta,\alpha,n}$ or $v_{\alpha,n}$ through the recursion (3.2). The policy class must not be restricted to deterministic Markov policies either, since that would make the characterization in Theorem 3.1.2 a different statement. Theorem 3.1.2(ii)(2) is stated with the guard $v_{\alpha,n}(i) < \infty$ ; the book omits it, and without it the "only if" direction is false (see the item's note).

A complete development needs the first-step decomposition of the path law under a general policy, the generalized Fatou lemma for approximating distributions (Proposition A.2.5, a milestone of the Appendix A mission of this series), and lim inf / lim sup manipulations in ℝ≥0∞. The model definitions are reusable by every later mission of the series. Contributions are welcome at every milestone, including proofs of the definitional sanity facts (for instance $v_{\theta,\alpha,0} = F$ ).

Selected references

Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994 (the standard reference for finite horizon dynamic programming with history-dependent randomized policies).
Richard Bellman, Dynamic Programming, Princeton University Press, 1957.

14 thms3 active usersReviewed

Completed

Optimal Transport·Captain: Lucas

Monge–Kantorovich Duality (Yao 2023)Research Paper

Motivation

Optimal transport asks for the cheapest way to move one distribution of mass onto another. Monge posed the problem in 1781 for maps; Kantorovich (1942) relaxed it to transference plans (couplings), turning it into an infinite-dimensional linear program with a dual: maximize the total revenue $\int\psi\,d\mu+\int\varphi\,d\nu$ of pickup and delivery prices that never exceed the cost, $\psi(x)+\varphi(y)\le c(x,y)$ . The equality of the two values — Monge–Kantorovich duality — underlies much of modern optimal transport, with uses in economics (matching markets, principal–agent problems), probability, and PDE.

This mission formalizes the duality theorem and its proof as presented in Colin Yao, Monge–Kantorovich and Transportation Theory (paper dated September 10, 2023), whose proof follows Villani's Optimal Transport: Old and New and, for the weak inequality, Galichon's Optimal Transport Methods in Economics.

Setting

$X$ and $Y$ are Polish spaces (separable, completely metrizable) with their Borel σ-algebras; $\mu$ and $\nu$ are Borel probability measures on $X$ and $Y$ ; $c : X\times Y\to[0,\infty)$ is a continuous cost function.

A transference plan is a probability measure $\pi$ on $X\times Y$ with marginals $\mu$ and $\nu$ ; $\Pi(\mu,\nu)$ denotes the set of such plans.
The Kantorovich problem is $\min_{\pi\in\Pi(\mu,\nu)}\int c\,d\pi$ .
The dual problem is $\sup\{\int\psi\,d\mu+\int\varphi\,d\nu\}$ over bounded continuous $\psi,\varphi$ with $\psi(x)+\varphi(y)\le c(x,y)$ everywhere.
A set $\Gamma\subseteq X\times Y$ is $c$ -cyclically monotone if $\sum_{i=1}^N c(x_i,y_i)\le\sum_{i=1}^N c(x_i,y_{i+1})$ (with $y_{N+1}=y_1$ ) for all finite families of points of $\Gamma$ ; a plan is $c$ -cyclically monotone if it is concentrated on such a set.
The $c$ -conjugate of $\psi$ is $\psi^c(y)=\inf_x(c(x,y)-\psi(x))$ ; $\psi$ is $c$ -concave if $\psi(x)=\inf_y(c(x,y)-\varphi(y))$ for some $\varphi$ ; its $c$ -subdifferential is $\partial_c\psi=\{(x,y):\psi^c(y)+\psi(x)=c(x,y)\}$ .

Formalization targets

Goal (Theorem 4.1)

\min_{\pi\in\Pi(\mu,\nu)}\int_{X\times Y}c\,d\pi=\sup_{\substack{\psi\in C_b(X),\ \varphi\in C_b(Y)\\ \psi(x)+\varphi(y)\le c(x,y)}}\Big(\int_X\psi\,d\mu+\int_Y\varphi\,d\nu\Big),

including existence of a minimizing plan; the common value may be $+\infty$ .

Milestones (in the order of the source)

Weak duality, inequality (3.1): $\inf\ge\sup$ .
Proposition 4.4: a $c$ -cyclically monotone plan exists between uniform empirical measures.
Lemma 4.16: plans with marginals in tight families form a tight family.
Proposition 4.17: a $c$ -cyclically monotone plan exists for general marginals.
Proposition 4.22: the support of a $c$ -cyclically monotone plan lies in $\partial_c\psi$ for a $c$ -concave $\psi$ (bounded $c$ ).
Theorem 4.25: $(\psi^c)^c=\psi$ for $c$ -concave $\psi$ .
Proposition 4.31: duality for bounded continuous $c$ .
Theorem 4.32: $\int f\,d\mu=\int f\,d\pi$ for a plan with marginal $\mu$ .

Significance

Duality converts a minimization over measures into a maximization over functions; it characterizes optimal plans by the complementary-slackness condition that they are concentrated on $\{\psi(x)+\varphi(y)=c(x,y)\}$ , and it is the entry point to Brenier's theorem, the Kantorovich–Rubinstein formula for the Wasserstein-1 distance, and the economic applications discussed in Section 5 of the source. The result is classical and proved in the literature; the work here is to formalize the known proof and to supply reusable infrastructure (couplings, $c$ -cyclical monotonicity, $c$ -transforms) on top of Mathlib's measure theory.

Difficulty

The weak inequality is a short integration argument; the reverse inequality is where the work lies. Finite-dimensional linear-programming duality does not pass to general measures directly: one must produce a cyclically monotone plan as a limit of discrete approximations (tightness and Prokhorov's theorem, closedness of the cyclic-monotonicity condition under weak convergence), build a potential $\psi$ from chains of cost differences, and control measurability and integrability of $\psi$ and $\psi^c$ . Passing from bounded to unbounded nonnegative costs requires an additional approximation argument, which the source only sketches (Section 4.5).

Formalization scope

Lean namespace MongeKantorovichYao; one definition file provides transference plans, $c$ -cyclical monotonicity, $c$ -conjugates, $c$ -concavity and $c$ -subdifferentials. Conventions: marginals are pushforwards along the projections; $c$ -conjugates are extended-real infima (no default values); the transport cost in the goal is the $[0,\infty]$ -valued integral of the nonnegative cost, and both sides of the goal are compared in the extended reals, so the infinite-cost case is included and no integrability hypothesis is added. The dual side ranges over bounded continuous functions with the constraint imposed at every point. Proposition 4.22 is stated for bounded $c$ (as used in Proposition 4.31), since with unbounded costs a real-valued potential need not exist. Infrastructure that may be missing from Mathlib: Prokhorov-type compactness of tight families of probability measures, weak convergence of empirical measures, and lower semicontinuity of $\pi\mapsto\int c\,d\pi$ .

Selected references

C. Villani, Optimal Transport: Old and New, Grundlehren der mathematischen Wissenschaften 338, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
A. Galichon, Optimal Transport Methods in Economics, Princeton University Press, 2016.
L. V. Kantorovich, On the translocation of masses, Dokl. Akad. Nauk SSSR 37 (1942).

10 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Numerical Techniques for Stochastic Optimization V: Asymptotic Optimality of List Scheduling for the Machine Investment ProblemTextbook

Motivation

Two-stage stochastic integer programs combine the two hardest features of mathematical programming: uncertainty in the data and integrality of the decisions. Even evaluating the objective of such a program at a single first-stage decision requires the expected optimal value of an NP-hard combinatorial problem. Chapter 8 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by A. H. G. Rinnooy Kan and L. Stougie, argues that for many such problems the way forward is probabilistic analysis: the random optimal value of the second-stage problem often converges, after normalization, to a simple function of the problem parameters, and that function can replace the intractable expectation.

The chapter illustrates this on the machine investment problem: first buy $m$ identical machines at cost $c$ each, knowing only the distribution of the processing times of $n$ jobs, then schedule the jobs once their processing times are revealed so as to minimize the makespan. This mission formalizes the chapter's analysis of that example: the almost sure asymptotics of the optimal makespan (8.13), its expectation version, and the asymptotic clairvoyance of the resulting two-stage heuristic.

Setting

Let $p_1, p_2, \dots$ be processing times: independent, identically distributed, nonnegative random variables on a probability space $(\Omega, \mathcal F, P)$ with mean $\mu = \mathbb E p_1 > 0$ and finite second moment $\mathbb E p_1^2 < \infty$ . The instance with $n$ jobs uses the first $n$ of them.

An assignment of the $n$ jobs to $m \ge 1$ identical machines is a map $\sigma : \{1, \dots, n\} \to \{1, \dots, m\}$ . The load of machine $i$ is $\sum_{j : \sigma(j) = i} p_j$ and the makespan of $\sigma$ is its largest load. The minimum makespan is

C^*_n(m) = \min_{\sigma} \max_{i=1,\dots,m} \sum_{j:\ \sigma(j) = i} p_j ,

and the machine investment problem is to minimize $Z_n(m) = cm + \mathbb E\, C^*_n(m)$ over integers $m$ (8.9).

List scheduling takes the jobs in the order $1, \dots, n$ and assigns each to the first available machine, a machine of least current load (lowest index on ties). Its makespan is $C^H_n(m)$ . Write $S_n = \sum_{j=1}^n p_j$ and $p_{\max} = \max_{j \le n} p_j$ .

For §8.3, the estimate $Z'_n(m) = cm + n\mu/m$ is minimized over integers by the heuristic first-stage decision $m^{H1}_n$ , the better of $\lfloor\sqrt{n\mu/c}\rfloor$ and $\lceil\sqrt{n\mu/c}\rceil$ . A clairvoyant decision maker who sees the processing times first chooses $m^\circ_n(\omega) \ge 1$ minimizing $cm + C^*_n(m)$ .

Formalization targets

Goal: Eq. (8.13)

For machine counts $m = m(n) \ge 1$ with $m(n) = O(\sqrt n)$ ,

P\Bigl\{ \lim_{n\to\infty} \frac{C^*_n(m)}{n\mu/m} = 1 \Bigr\} = 1 .

The machine count is allowed to grow with $n$ ; this is the regime the first-stage heuristic lives in, since $m^{H1}_n$ is of exact order $\sqrt n$ .

Milestones

Eq. (8.10): the deterministic sandwich $S_n/m \le C^*_n(m) \le C^H_n(m) \le S_n/m + p_{\max}$ , divided by $n\mu/m$ .
Eq. (8.11): the strong law of large numbers, $(S_n - n\mu)/(n\mu) \to 0$ almost surely (a published platform theorem).
Lemma 8.1 (i): $p_{\max}/\sqrt n \to 0$ almost surely.
Eq. (8.12): $m\, p_{\max}/(n\mu) \to 0$ almost surely when $m = O(\sqrt n)$ .
Lemma 8.1 (ii): $\mathbb E\, p_{\max}/\sqrt n \to 0$ .
p. 207: $\mathbb E\, C^*_n(m)/(n\mu/m) \to 1$ when $m = O(\sqrt n)$ .
p. 211, asymptotic clairvoyance: almost surely

\lim_{n\to\infty} \frac{c\, m^{H1}_n + C^{H2}_n(m^{H1}_n)}{c\, m^\circ_n + C^*_n(m^\circ_n)} = 1 ,

where $C^{H2}_n$ is the list-scheduling makespan.

Significance

Result (8.13) says that the optimal value of an NP-hard problem, rescaled, is almost surely asymptotic to the elementary function $n\mu/m$ of the data and the first-stage decision. Its expectation version replaces the intractable term $\mathbb E\,C^*_n(m)$ in (8.9) by $n\mu/m$ , and the clairvoyance statement shows that the heuristic built on that replacement loses asymptotically nothing, not even against a decision maker with full information. The chapter presents the example as the template for vehicle routing and location problems preceded by an investment decision.

All results here are classical and proved in the literature cited by the chapter (Lemma 8.1 is quoted from Feller without proof; the chapter refers to Dempster et al. for the asymptotic optimality of the two-stage heuristic and to Lenstra et al. for the notion of asymptotic clairvoyance). None of them has, to our knowledge, a machine-checked proof. The mission produces a formal model of identical-machine makespan scheduling and of list scheduling, the extreme-value estimates of Lemma 8.1 for square-integrable i.i.d. sequences, and the full chain from the strong law to (8.13).

Difficulty

The deterministic part is elementary on paper, but list scheduling is a recursively defined procedure, and its makespan bound has to be established for that recursion rather than for a picture like the chapter's Figure 8.3. The probabilistic core is Lemma 8.1: the strong law controls $S_n/n$ , but the error term $m\, p_{\max}/(n\mu)$ is of order $p_{\max}/\sqrt n$ once $m$ grows like $\sqrt n$ , and the strong law says nothing about maxima. With a fixed number of machines the whole statement would reduce to the strong law; the growth $m(n) = O(\sqrt n)$ is exactly where the second moment is needed. For the clairvoyance statement, the clairvoyant choice $m^\circ_n$ is a random, unstructured minimizer, so its value must be bounded below without knowing where the minimum is attained.

Formalization scope

Processing times are one sequence p : ℕ → Ω → ℝ, 0-based (the book's $p_j$ is p (j-1)), with each p j measurable, the family mutually independent (iIndepFun), identically distributed with p 0, pointwise nonnegative, p 0 ^ 2 integrable and ∫ p 0 = μ with μ > 0. Nonnegativity and $\mu > 0$ are not printed in the book; they are implicit in "processing times" and in the division by $n\mu$ . Machines are Fin m; a schedule is an assignment Fin n → Fin m, which is faithful because jobs are non-preemptive, machines identical and there are no precedence constraints.

The book writes " $m = 0(\sqrt n)$ "; this is read as $m$ a function of $n$ with $m(n) \ge 1$ and (fun n => (m n : ℝ)) =O[atTop] (fun n => √n). Stating (8.13) for a fixed $m$ would trivialize it into the strong law and is ruled out. " $\Pr\{\lim \dots = 1\} = 1$ " means that almost surely the limit exists and equals $1$ . Expectations are Bochner integrals of functions that are measurable and bounded by $S_n$ , hence integrable. List scheduling uses the index order and breaks ties towards the lowest machine index; both are admissible instances of the book's "arbitrary fixed order" and "first available machine". In the clairvoyance statement the minimum is over $m \ge 1$ (the book writes $m \in \mathbb N$ ; no machine cannot process any job, and the Lean value $C^*_n(0)$ is an empty-infimum convention). No explicit constants replace an O(·): the statements are limits and the O-hypothesis is carried as stated.

Out of scope: (8.14) and the p. 210 expectation statement, which need a positive density at $0$ and whose proof the book calls "far from easy", and the dynamic programming recursion of §8.3.

Needed infrastructure: finite maxima and minima of measurable functions, extreme-value estimates for square-integrable i.i.d. sequences (Lemma 8.1), and Mathlib's strong law. The makespan and list-scheduling definitions are reusable for other identical-machine scheduling results; alternative proofs of Lemma 8.1 and sharper forms of the clairvoyance statement are welcome.

Selected references

A. H. G. Rinnooy Kan, L. Stougie, "Stochastic Integer Programming", in Yu. Ermoliev, R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 8, pp. 201–213. https://doi.org/10.1007/978-3-642-61370-8
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, 3rd edition, Wiley, 1968 (cited by the chapter for Lemma 8.1).
M. A. H. Dempster, M. L. Fisher, L. Jansen, B. J. Lageweg, J. K. Lenstra, A. H. G. Rinnooy Kan, "Analysis of heuristics for stochastic programming: results for hierarchical scheduling problems", Mathematics of Operations Research 8 (1983) 525–537. https://doi.org/10.1287/moor.8.4.525
J. K. Lenstra, A. H. G. Rinnooy Kan, L. Stougie, "A framework for the design and analysis of hierarchical planning systems", Annals of Operations Research 1 (1984) 23–42. https://doi.org/10.1007/BF01874451
R. L. Graham, "Bounds on multiprocessing timing anomalies", SIAM Journal on Applied Mathematics 17 (1969) 416–429. https://doi.org/10.1137/0117039

11 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Numerical Techniques for Stochastic Optimization III: Stochastic Quasi-Féjer Sequences and the Stochastic Quasigradient Projection MethodTextbook

Motivation

Many optimization problems in operations research have an objective that is an expectation, $F^0(x)=E f^0(x,\omega)$ , over a random parameter $\omega$ whose distribution is known only through samples or is too complex to integrate. Two-stage stochastic programs, inventory and reliability models, and simulation-based design all have this form. Neither $F^0$ nor its subgradients can be evaluated exactly, but a random vector whose conditional mean is close to a subgradient is often cheap to compute: a sample subgradient of $f^0(\cdot,\omega)$ , or a finite-difference quotient of two sampled values.

Stochastic quasigradient (SQG) methods, developed by Ermoliev and co-workers in Kiev from the late 1960s, use such vectors in place of subgradients. They extend the stochastic approximation procedures of Robbins–Monro (1951) and Kiefer–Wolfowitz (1952) to nonsmooth convex objectives, general convex constraints, and directions whose conditional mean is biased by a vanishing amount. This mission formalizes the basic convergence theory of the simplest SQG method, the projection method, as presented by Yu. Ermoliev in Chapter 6 of the IIASA volume Numerical Techniques for Stochastic Optimization (Springer 1988).

Timeline (as cited in the chapter's bibliography).

1951–1954: Robbins and Monro, Kiefer and Wolfowitz, Dvoretzky and Blum prove convergence of stochastic approximation for unconstrained smooth problems.
1962–1967: Shor introduces the generalized gradient (subgradient) method; Ermoliev (Kibernetika 4, 1966) and Polyak (Soviet Math. Doklady 8, 1967) prove its convergence.
1967–1969: Ermoliev and Nekrylova introduce stochastic subgradients; Ermoliev ("On the stochastic quasi-gradient method and stochastic quasi-Feyer sequences", Kibernetika 2, 1969) introduces stochastic quasi-Féjer sequences.
1976: Ermoliev's monograph Stochastic Programming Methods (Nauka) contains the proof of Theorem 6.1 (p. 98).
1988: the survey chapter formalized here presents the projection method, Theorems 6.1 and 6.2, and an efficiency estimate for the averaged iterate.

Setting

Let $X\subseteq\mathbb R^n$ be a nonempty convex compact set and $F^0:\mathbb R^n\to\mathbb R$ convex and continuous on $X$ . The optimal set is $X^*=\{x\in X: F^0(x)\le F^0(y)\ \forall y\in X\}$ . The projection onto $X$ is $\pi_X(y)=\operatorname{argmin}\{\|y-x\|^2:x\in X\}$ .

On a probability space, the stochastic quasigradient projection method produces random vectors $x^0,x^1,\dots$ by

x^{s+1}=\pi_X\big[x^s-\rho_s\,\xi^0(s)\big],\qquad s=0,1,\dots \tag{6.11}

where $\rho_s\ge0$ is a step size and $\xi^0(s)$ a random direction. Write $E\{\cdot\mid x^0,\dots,x^s\}$ for conditional expectation given the history $\sigma(x^0,\dots,x^s)$ . The direction is a stochastic quasigradient if, for every $x^*\in X^*$ ,

F^0(x^*)-F^0(x^s)\ge\big\langle E\{\xi^0(s)\mid x^0,\dots,x^s\},\,x^*-x^s\big\rangle+\gamma_0(s)\quad\text{a.s.}, \tag{6.12}

where the error $\gamma_0(s)$ is a function of the history. If the conditional mean of $\xi^0(s)$ is a subgradient plus a bias $b^0(s)$ , then (6.12) holds with $\gamma^0(s)=-\langle b^0(s),x^*-x^s\rangle$ (6.13).

A sequence of random vectors $z^0,z^1,\dots$ is a stochastic quasi-Féjer sequence for $Z\subseteq\mathbb R^n$ if $E\|z^0\|^2<\infty$ and there are random $r_s\ge0$ with $\sum_s E r_s<\infty$ such that for all $z\in Z$

E\{\|z-z^{s+1}\|^2\mid z^0,\dots,z^s\}\le\|z-z^s\|^2+r_s. \tag{6.14}

Formalization targets

Goal: Theorem 6.2

If, with probability 1, $\rho_s\ge0$ and $\sum_s\rho_s=\infty$ , and

\sum_{s=0}^\infty E\{\rho_s|\gamma_0(s)|+\rho_s^2\|\xi^0(s)\|^2\}<\infty, \tag{6.15}

then with probability 1 the iterates converge and $\lim_s x^s\in X^*$ .

Milestones

Theorem 6.1 (a)–(c). For a stochastic quasi-Féjer sequence for $Z$ : $\|z-z^{s+1}\|^2$ converges a.s. and $E\|z-z^s\|^2$ is bounded, for each $z\in Z$ ; accumulation points exist a.s. (for $Z\ne\emptyset$ ); and a.s. $Z$ lies in the hyperplane equidistant from any two distinct accumulation points outside $Z$ .
Eq. (6.13). Biased stochastic subgradients satisfy (6.12).
One-step inequality (p. 145): $E\{\|x^*-x^{s+1}\|^2\mid\cdot\}\le\|x^*-x^s\|^2+2\rho_s\langle E\{\xi^0(s)\mid\cdot\},x^*-x^s\rangle+E\{\rho_s^2\|\xi^0(s)\|^2\mid\cdot\}$ for $x^*\in X$ .
Quasi-Féjer property (p. 145): the iterates of (6.11) form a stochastic quasi-Féjer sequence for $X^*$ .
Efficiency estimate (p. 147), for deterministic $\rho_k$ and $\bar x^s=\sum_{k\le s}\rho_kx^k/\sum_{k\le s}\rho_k$ :

E F^0(\bar x^s)-F^0(x^*)\le\Big(2\sum_{k=0}^s\rho_k\Big)^{-1}\Big[E\|x^*-x^0\|^2+\sum_{k=0}^s E\big(2\rho_k|\gamma_0(k)|+\rho_k^2\|\xi^0(k)\|^2\big)\Big].

Significance

Theorem 6.2 is the prototype convergence theorem for SQG methods. Its hypotheses allow random step sizes chosen from the history, nonsmooth objectives, and directions with a bias that vanishes fast enough; its conclusion is convergence of the iterates themselves to a single optimal point, not only convergence of function values or of $\operatorname{dist}(x^s,X^*)$ . The later chapters of the same volume (adaptive step sizes, Chapters 17–18; nonstationary problems, §6.4) reuse the same framework. Theorem 6.1 isolates the probabilistic content in a form that applies to any algorithm with a quasi-Féjer inequality. The efficiency estimate gives a non-asymptotic accuracy bound for the averaged iterate.

The results are classical and proved in the literature: Theorem 6.1 in Ermoliev (1976, p. 98), Theorem 6.2 in this chapter (pp. 145–146). To our knowledge none of them has a machine-checked proof. Mathlib has conditional expectations and the a.s. martingale convergence theorem, but no Robbins–Siegmund-type almost-supermartingale lemma and no stochastic subgradient method. A formal proof of this mission would supply both.

Difficulty

The deterministic argument for projected subgradient methods compares $\|x^*-x^{s+1}\|$ with $\|x^*-x^s\|$ for a fixed $x^*$ . In the stochastic setting this comparison holds only in conditional mean, with a perturbation $r_s$ that is random, and the distances converge only almost surely, with an exceptional null set that depends on $x^*$ . Since $X^*$ is typically uncountable, "for every $x^*$ , almost surely" does not immediately give "almost surely, for every $x^*$ ", and it is the second form that identifies a single limit. A second difficulty is that $\sum\rho_s(F^0(x^s)-F^0(x^*))<\infty$ only yields a subsequence along which $F^0$ approaches its minimum; passing from there to convergence of the whole sequence is exactly what part (c) of Theorem 6.1 is for.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The probability space is an arbitrary measurable space with a probability measure. $\pi_X$ is a chosen minimizer of $\|y-x\|^2$ over $X$ (unique for nonempty closed convex $X$ ). The history is the $\sigma$ -algebra generated by $x^0,\dots,x^s$ ; $\rho_s$ and $\gamma_0(s)$ are measurable with respect to it.
Directions $\xi^0(s)$ are integrable and random vectors are measurable; conditional expectations are Mathlib's condExp. The quasi-Féjer definition requires square integrability of every $z^s$ (implied by the book's definition when $Z\ne\emptyset$ ), so no conditional expectation is taken of a non-integrable function.
$X\ne\emptyset$ and $x^0\in X$ are stated; $Z\ne\emptyset$ is added in Theorem 6.1 (b), which is false without it.
$\gamma_0(s)$ does not depend on $x^*$ ; the $x^*$ -dependent error of (6.13) is dominated on a bounded $X$ by $\|b^0(s)\|\operatorname{diam}X$ .
(6.15) keeps its mixed form: $\rho_s\ge0$ and $\sum\rho_s=\infty$ almost surely, and a deterministic sum of expectations (lower Lebesgue integrals) finite.
Explicit constants. The book's " $C$ " in the efficiency estimate is instantiated from its proof: $2$ on $\rho_k|\gamma_0(k)|$ and $1$ on $\rho_k^2\|\xi^0(k)\|^2$ . The unspecified $C$ before the quasi-Féjer sentence is replaced by the existence of summable $r_s$ .
Typo corrections. The one-step inequality on p. 145 prints $\rho_sE\{\|\xi^0(s)\|^2\mid\cdot\}$ ; it is $\rho_s^2$ . The efficiency estimate on p. 147 omits $E$ before the last sum; it is restored. " $\rho_k$ independent of $(x^0,\dots,x^k)$ " is read as deterministic step sizes.
A trivializing formalization is excluded: the goal does not replace $\xi^0(s)$ by an exact subgradient, does not set $\gamma_0\equiv0$ , and concludes convergence of $x^s$ to a point of $X^*$ rather than $\operatorname{dist}(x^s,X^*)\to0$ .
Reusable infrastructure: a Robbins–Siegmund lemma for nonnegative almost-supermartingales, the nonexpansiveness of $\pi_X$ , and Theorem 6.1 itself, which applies to any quasi-Féjer algorithm (Chapter 6 §6.4 and Chapters 17–18 of the same book). Contributions of these general lemmas are welcome.

Selected references

Yu. Ermoliev, "Stochastic Quasigradient Methods", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 6, §6.1–6.2 (pp. 141–147). https://doi.org/10.1007/978-3-642-61370-8
Yu. Ermoliev, "On the stochastic quasi-gradient method and stochastic quasi-Feyer sequences", Kibernetika 2 (1969) (in Russian; English translation in Cybernetics). Reference [3] of the chapter.
Yu. Ermoliev, Stochastic Programming Methods, Nauka, Moscow, 1976 (in Russian); Theorem 6.1 is on p. 98. Reference [5] of the chapter.
H. Robbins and D. Siegmund, "A convergence theorem for non negative almost supermartingales and some applications", in J. S. Rustagi (ed.), Optimizing Methods in Statistics, Academic Press, 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
H. Robbins and S. Monro, "A stochastic approximation method", Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586

10 thms3 active usersReviewed

Completed

Number Theory Quantum Information Theoretical Computer Science·Captain: mikedeng1

Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer 3: The Success Probability of Quantum Order FindingResearch Paper

Motivation

The security of the RSA cryptosystem rests on the assumed difficulty of factoring large integers, and the best known classical algorithms for factoring run in super-polynomial time. In 1994 Peter Shor showed that a quantum computer can factor an $n$ -digit integer in time polynomial in $n$ (Shor, SIAM J. Comput. 1997; conference version FOCS 1994). The algorithm has two parts. A classical reduction, due to Miller (1976), turns factoring into order finding: given $x$ coprime to $n$ , find the least $r \ge 1$ with $x^r \equiv 1 \pmod n$ . The quantum part solves order finding.

This mission formalizes the quantum part as Shor analyzes it in §5 of the journal paper: the construction of the quantum state, the probability of each measurement outcome, and the classical post-processing that reads $r$ off the measured value. The paper's claim is that one run of this procedure returns $r$ with probability at least $\varphi(r)/3r$ .

Timeline:

1976: Miller reduces factoring to order finding (with randomization).
1985–1994: Deutsch, Bernstein–Vazirani and Simon give the quantum Fourier sampling ideas the algorithm builds on.
1994: Shor's FOCS paper introduces the factoring and discrete logarithm algorithms.
1997: the SIAM J. Comput. version gives the analysis formalized here, with $q$ the power of $2$ in $[n^2, 2n^2)$ .

Setting

Fix an integer $n \ge 2$ and an integer $x$ coprime to $n$ . Its order $r$ is the least $r \ge 1$ with $x^r \equiv 1 \pmod n$ ; since $x$ is a unit, $r \le \varphi(n) < n$ . Let $q = 2^l$ be the power of $2$ with $n^2 \le q < 2n^2$ .

A quantum state on two registers, the first holding $0 \le a < q$ and the second a residue $y \in \mathbb{Z}/n$ , is a complex vector $\psi(a, y)$ indexed by the basis states $|a, y\rangle$ . Measuring it returns $|a, y\rangle$ with probability $|\psi(a, y)|^2$ .

The Fourier matrix $A_q$ is the $q \times q$ matrix with entries $(A_q)_{a,c} = q^{-1/2}\exp(2\pi i a c/q)$ , with rows indexing inputs and columns outputs. The algorithm

prepares $\frac{1}{q^{1/2}}\sum_{a=0}^{q-1}|a\rangle|x^a \bmod n\rangle$ (eq. (5.2)),
applies $A_q$ to the first register, obtaining $\frac1q\sum_{a,c}\exp(2\pi iac/q)|c\rangle|x^a \bmod n\rangle$ (eq. (5.4)),
measures, obtaining some $|c, y\rangle$ ,
rounds $c/q$ to the nearest fraction with denominator smaller than $n$ .

The observed $c$ gives us $r$ if some fraction with lowest-terms denominator below $n$ is within $1/2q$ of $c/q$ , and every such fraction has lowest-terms denominator exactly $r$ . In the Lean development these objects are preFourierState, finalState, outcomeProb and yieldsOrder, in the namespace ShorAlgorithms.OrderFinding, and the shared definition ShorAlgorithms.Shared.fourierMatrix.

Formalization targets

Goal: success probability at least $\varphi(r)/3r$

For all sufficiently large $n$ , with $x$ , $r$ and $q$ as above,

\Pr\bigl[\text{the observed } c \text{ gives us } r\bigr] \;=\; \sum_{c\ \text{gives}\ r}\ \sum_{y \in \mathbb{Z}/n} |\Psi(c, y)|^2 \;\ge\; \frac{\varphi(r)}{3r},

where $\Psi$ is the state (5.4). The threshold on $n$ is uniform in $x$ and $q$ ; it is the paper's "for sufficiently large $n$ " from the per-state bound.

Milestones

Eqs. (5.5)–(5.6). For $0 \le k < r$ , the probability of $|c, x^k\rangle$ equals $\left|\frac1q\sum_{b=0}^{\lfloor (q-k-1)/r\rfloor}\exp(2\pi i(br+k)c/q)\right|^2$ .
Eq. (5.11). For $n$ past a threshold, every $|c, x^k\rangle$ with $-r/2 \le rc - dq \le r/2$ for some integer $d$ has probability at least $1/3r^2$ .
Eq. (5.13). If $n^2 \le q$ , at most one fraction with denominator below $n$ lies within $1/2q$ of $c/q$ .
p. 1500. Such a fraction is a convergent of the continued fraction of $c/q$ .
p. 1501. At least $\varphi(r)$ values of $c$ are within $1/2q$ of some $d/r$ with $\gcd(d, r) = 1$ ; with the $r$ distinct values of $x^k$ this gives at least $r\varphi(r)$ states $|c, x^k\rangle$ , and each such $c$ gives us $r$ .

Significance

The goal is the quantitative statement behind "order finding is in bounded-error quantum polynomial time": since $\varphi(r)/r \ge \delta/\log\log r$ for a constant $\delta$ (Hardy and Wright, Thm. 328), $O(\log\log r)$ repetitions find $r$ with high probability, and Miller's reduction then factors $n$ . Without the bound, the algorithm is a procedure with no guarantee.

The result is proved, in the paper and in textbooks (Nielsen and Chuang, 2000, §5.3), usually with a phase-estimation analysis rather than Shor's direct count. What this mission adds is a machine-checked proof of Shor's own argument, with his choice of $q$ and his constants, starting from the state built by applying $A_q$ to (5.2). Formal proofs of idealized versions exist elsewhere, for instance in the exact-period model where $r$ divides $q$ and the output is uniform on $r$ peaks, but that model removes the approximation that the $1/3r^2$ bound is about. Legendre's theorem on continued fractions is already on the platform (FamousTheorems.legendre_continued_fraction_theorem) and is included as a reference item.

Difficulty

The obvious route is to compute the output distribution in closed form. That works only when $r$ divides $q$ ; here $q$ is a power of $2$ and $r$ is arbitrary, so the amplitudes are geometric sums of $\lfloor (q-k-1)/r\rfloor + 1$ terms whose phases do not cancel exactly. The per-state bound $1/3r^2$ requires a lower bound on such a sum that is uniform in $r$ , $c$ and $k$ , with error terms of order $1/q$ controlled against a main term of order $1/r^2$ . The constant $1/3$ leaves only a small margin below the limiting value $4/\pi^2 \approx 0.405$ , so the errors must be bounded explicitly, not merely shown to vanish.

The second difficulty is the counting: distinct coprime numerators $d$ must give distinct outcomes $c$ in $[0, q)$ , and each good $c$ must determine $r$ uniquely, which uses $r < n$ and $n^2 \le q$ .

Formalization scope

Conventions the statements commit to:

States are functions Fin q × ZMod n → ℂ; the matrix convention is row = input, so applying $A_q$ to the first register gives the amplitude $\sum_a \psi(a, y)(A_q)_{a,c}$ at $(c, y)$ .
The final state is built by applying $A_q$ to the state (5.2); the closed forms (5.5) and (5.6) are theorems, not definitions. No normalization hypothesis is assumed.
Probabilities are squared moduli; the probability of the event " $c$ gives us $r$ " sums over all $y \in \mathbb{Z}/n$ , which is exact because $y$ that are not powers of $x$ have probability zero.
$x$ is a natural number with $\gcd(x, n) = 1$ ; $r$ is orderOf (x : ZMod n). $q$ enters through the three hypotheses $q = 2^l$ , $n^2 \le q$ , $q < 2n^2$ , not through a function of $n$ .
Fractions are rationals, and "in lowest terms" is Rat.den.
Thresholds "for sufficiently large $n$ " are $\exists N,\ \forall n \ge N$ , with $N$ quantified before $x$ , $q$ , $c$ and $k$ .
Condition (5.11) is stated in its equivalent form (5.12), with an integer $d$ .
Printed slip. Eq. (5.13)'s justification says "Because $q > n^2$ ", but $q$ was chosen with $n^2 \le q$ , and $q = n^2$ when $n$ is a power of $2$ . The uniqueness claim holds under $n^2 \le q$ , and that is what is stated.

Typing the closed form (5.4)–(5.6) in as the definition of the final state would make milestone 1 trivial and hide whether the probability model is the paper's; the definitions exclude this by construction.

Not stated: the polynomial running time of any step, the $O(\log\log r)$ repetition count (no explicit constant), the reversible modular exponentiation of §3, and the post-processing heuristics on p. 1501. Needed infrastructure: bounds on geometric exponential sums, Euler's totient, Diophantine approximation by fractions with bounded denominator, and Mathlib's continued fractions. Lemmas on geometric sums of roots of unity and on the order of units mod $n$ are reusable in the companion discrete logarithm mission.

Selected references

P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172
P. W. Shor, Algorithms for quantum computation: discrete logarithms and factoring, Proc. 35th FOCS, 1994. https://doi.org/10.1109/SFCS.1994.365700
G. L. Miller, Riemann's hypothesis and tests for primality, J. Comput. System Sci. 13(3):300–317, 1976. https://doi.org/10.1016/S0022-0000(76)80043-8
G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 5th ed., Oxford, 1979 (Ch. X, continued fractions; Thm. 328).
M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge, 2000. https://doi.org/10.1017/CBO9780511976667

12 thms3 active usersReviewed

Linear Optimization Operations Research Theoretical Computer Science·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems IV: The Optimal Randomized Two-Server Ratio 1652/1069 on the 3-4-5 TriangleResearch Paper

Motivation

The $k$ -server problem is a basic model of on-line decision making. $k$ mobile servers move in a metric space, requests for points arrive one at a time, and each request has to be covered by a server before the next one arrives. The cost is the total distance the servers move. The problem includes paging, caching and disk-head scheduling as special cases (Manasse, McGeoch, Sleator 1990). An on-line algorithm is judged by its competitive factor: how much its cost can exceed that of an off-line algorithm that knows the whole request sequence in advance.

For randomized algorithms against an oblivious adversary (one that fixes the whole request sequence before the algorithm flips any coins), the best-understood case is paging, which is the $k$ -server problem on a uniform metric space. There the optimal factor is the harmonic number $H_k=\sum_{i=1}^k 1/i$ . Fiat et al. proved the lower bound (1991) and McGeoch and Sleator the matching upper bound (1991). Karlin, Manasse, McGeoch and Owicki (Algorithmica 11, 1994, §5) asked whether $H_k$ -competitive algorithms also exist when the metric space is not uniform. They answered no, already for two servers on three points: on certain triangles the optimal randomized factor is strictly larger than $H_2 = 3/2$ . This mission formalizes their Theorem 13, which gives the exact optimal factor on the triangle with edge lengths 3, 4 and 5.

Timeline:

1990: Manasse, McGeoch and Sleator introduce the $k$ -server problem; $k$ is the deterministic optimum for $k=2$ .
1991: Fiat, Karp, Luby, McGeoch, Sleator and Young prove the $H_k$ lower bound for randomized paging. McGeoch and Sleator give an $H_k$ -competitive paging algorithm.
1994: Karlin, Manasse, McGeoch and Owicki determine the optimal randomized two-server factors on the isosceles triangles $1$ - $d$ - $d$ (Theorem 12) and on the 3-4-5 triangle (Theorem 13, the ratio $1652/1069$ ). Both exceed $3/2$ .

Setting

Let $M$ be a metric space with exactly three points $a, b, c$ , where $d(a,b)=3$ , $d(a,c)=5$ and $d(b,c)=4$ . A configuration $C$ gives the positions of two labelled servers in $M$ . A request sequence $\sigma$ is a finite list of points of $M$ .

A deterministic on-line algorithm assigns to each prefix of a request sequence a configuration, in which the last request is covered. Its configuration after a prefix therefore cannot depend on later requests. Its initial configuration is the one it assigns to the empty prefix, and its cost $C_A(\sigma)$ on $\sigma$ is the total distance its servers move while serving $\sigma$ request by request.

The optimal off-line cost $C_{opt}(\sigma)$ from an initial configuration $C_0$ is the infimum, over all schedules that start at $C_0$ and cover each request of $\sigma$ in turn, of the total distance moved.

A randomized on-line algorithm $A$ is a probability distribution over deterministic on-line algorithms, all starting at $C_0$ . The cost on each fixed $\sigma$ is required to be measurable in the random choice, and $\mathbf{E}C_A(\sigma)$ is the expected cost. $A$ is $\rho$ -competitive against an oblivious adversary if there is a constant $a$ such that for every request sequence $\sigma$ ,

\mathbf{E}C_A(\sigma) \le \rho\cdot C_{opt}(\sigma) + a .

These are the definitions of p. 543 of the paper. They are the platform's published KServer_model and KServer_randomized, which this mission reuses unchanged: KServer.RandomizedAlgorithm 2 M and A.IsCompetitiveFrom C₀ ρ.

Formalization targets

Goal: Theorem 13

For every initial configuration $C_0$ of the two servers,

\Big(\forall A,\ \forall \rho,\ A \text{ is } \rho\text{-competitive from } C_0 \Rightarrow \rho \ge \tfrac{1652}{1069}\Big)\ \wedge\ \Big(\exists A,\ A \text{ is } \tfrac{1652}{1069}\text{-competitive from } C_0\Big).

The first claim is quantified over all randomized algorithms, so it also covers deterministic ones (point masses). The second claim asks for one algorithm. Together they say that $1652/1069 \approx 1.545$ is the exact optimal randomized factor on this triangle.

Milestones

The phase LP lower bound (p. 568). Twelve linear constraints in nine probabilities $\pi_1,\dots,\pi_9$ , three potentials $\Phi_{ab},\Phi_{ac},\Phi_{bc}$ and a ratio $\alpha$ , one constraint for each possible phase of the request sequence, of the form

\text{A's cost} \le \alpha\cdot(\text{opt's cost}) + \Phi_{\text{initial}} - \Phi_{\text{final}}.

Every real solution has $\alpha \ge 1652/1069$ . 2. The LP attainment (p. 568). The paper's printed probabilities lie in $[0,1]$ , and with suitable potentials they satisfy all twelve constraints at $\alpha = 1652/1069$ . 3. Theorem 13, first claim: the lower bound for every randomized algorithm. 4. Theorem 13, second claim: a $1652/1069$ -competitive randomized algorithm exists.

Significance

The result. Theorem 13 shows that the $H_k$ behaviour of randomized paging does not carry over to general metric spaces. Two servers on a three-point space already force a factor above $3/2$ . The value is exact, which makes this triangle a test case for any general theory of randomized $k$ -server algorithms on small metric spaces. With Theorem 12 (the isosceles triangles, a companion mission of this series), it is one of the few non-uniform metric spaces with a known optimal randomized factor.

Formalizing it. The result has been proved since 1994. To our knowledge there is no machine-checked proof. The paper derives both bounds from two framework theorems for phase-based algorithms: Theorem 3 (an LP lower bound for phase-based algorithms bounds every algorithm) and Theorem 2 (a lazy phase-based algorithm with LP bound $\alpha$ is $\alpha$ -competitive). The phase tables themselves (which phases can occur and what they cost) are stated without detailed proof. A formal proof has to supply both framework arguments for this space and verify the phase tables, as well as the finite linear algebra of milestones 1 and 2. The milestones isolate the exact-arithmetic core so that it can be closed independently of the probabilistic part.

Difficulty

The two LP milestones are finite exact-arithmetic facts. The hard part is linking them to Theorem 13.

For the lower bound, an algorithm need not be phase-based at all. Its probabilities may depend on the whole history, not only on the current phase, and it may leave the configuration of the off-line optimum at the end of a phase. The obvious attempt is to fix one hard request sequence and compare costs, but that cannot work: randomization defeats any single sequence. The reduction from arbitrary algorithms to phase-based ones (the paper's Theorem 3) is the substantive step.

For the upper bound, the printed probabilities describe the algorithm's marginal position after each prefix of a phase. They have to be realized as a single probability distribution over deterministic on-line algorithms that is lazy (it moves only to serve a request) and whose expected cost per phase equals the table's entry. On top of this, the LP accounting has to be turned into a bound on arbitrary request sequences, including partial phases and a start away from the optimum's configuration.

Formalization scope

Model. The platform definitions KServer_model and KServer_randomized are used unchanged. Servers are labelled (Config 2 M = Fin 2 → M). A deterministic algorithm is a function of the request prefix, which makes it on-line by construction. A randomized algorithm is a mixed strategy with a probability measure and a measurability field, and its expected cost is the lower Lebesgue integral of the nonnegative cost. The off-line optimum is a real infimum over schedules from $C_0$ ; the set is nonempty and bounded below by $0$ . Competitiveness allows any real additive constant.
The triangle is given by hypotheses on an arbitrary metric space: every point equals $a$ , $b$ or $c$ , and $d(a,b)=3$ , $d(a,c)=5$ , $d(b,c)=4$ . These hypotheses are satisfiable ( $3+4\ge5$ ) and force three distinct points.
Initial configuration. Both claims are stated for every initial configuration $C_0$ , including both servers on one point. The paper does not fix the start; the additive constant absorbs it.
LP milestones. The thirteen LP variables are free reals, with no box $0\le\pi_i\le 1$ , exactly as the paper permits. This makes milestone 1 stronger than the boxed version; the minimum is the same either way. The twelve constraints are written out one per hypothesis, in the table's order, with the potential difference $\Phi_{\text{initial}} - \Phi_{\text{final}}$ on the right. In milestone 2 the potentials are existentially quantified, since the paper names none.
Not stated. The paper's Theorems 2 and 3 (the phase framework) and the phase tables are not separate milestones. Milestone 1 feeds the first claim through Theorem 3, and milestone 2 feeds the second claim through Theorem 2. Contributions formalizing phase-based algorithms, laziness and the LP-bound reduction for finite metric spaces would be reusable for Theorem 12 and Theorem 14 of the same paper.
Ruled out. The lower bound is not restricted to deterministic or to phase-based algorithms, and it is not stated as "one sequence defeats every algorithm". The constant is exactly $1652/1069$ , not an approximation, and the attainment claim is not weakened to "for some initial configuration".

Selected references

A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994) 542–571. https://doi.org/10.1007/BF01189993
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, Journal of Algorithms 11 (1990) 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, Journal of Algorithms 12 (1991) 685–699. https://doi.org/10.1016/0196-6774(91)90041-V
L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6 (1991) 816–825. https://doi.org/10.1007/BF01759073

7 thms3 active usersReviewed

Linear Optimization Operations Research Theoretical Computer Science·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems III: The Optimal Randomized Two-Server Ratio on the 1-d-d Isosceles TriangleResearch Paper

Motivation

The k-server problem of Manasse, McGeoch and Sleator (J. Algorithms 11 (1990)) asks how $k$ mobile servers in a metric space should respond, on-line, to a sequence of requests at points of the space, each of which must be covered by a server. It is the central model of on-line computation: paging is the special case of a uniform metric, and many caching and scheduling problems reduce to it. For two servers the deterministic picture is complete: the optimal competitive ratio is $2$ on every metric space with at least three points.

Randomization changes the picture, and the smallest nontrivial case already shows how. On the equilateral triangle the optimal randomized ratio against an oblivious adversary is $3/2$ . Karlin, Manasse, McGeoch and Owicki (Algorithmica 11 (1994) 542–571) computed the exact optimal randomized ratio for several nonuniform triangles, where the distances differ, and showed that it depends on the geometry. Their Theorem 12 settles the whole family of isosceles triangles with edge lengths $1$ , $d$ , $d$ . These exact values are among the few known optimal randomized ratios for server problems.

Timeline:

1990: Manasse, McGeoch and Sleator introduce the $k$ -server problem and prove the deterministic two-server ratio is $2$ .
1990–1994: Karlin, Manasse, McGeoch and Owicki submit this paper (received August 1990, revised September 1991) and publish it in Algorithmica in 1994, with the isosceles-triangle ratios of Theorem 12 and the 3-4-5 triangle ratio $1652/1069$ of Theorem 13.
Later: Karloff, Rabani and Ravid extend the technique to $\Omega(\log\log k)$ and $\Omega(\log k)$ randomized lower bounds (cited on p. 564); Bubeck, Coester and Rabani (STOC 2023) refute the randomized $k$ -server conjecture.

Setting

Fix an integer $d\ge1$ . The isosceles triangle $M$ has three points $a$ , $b$ , $c$ with

\operatorname{dist}(a,b)=1,\qquad \operatorname{dist}(a,c)=\operatorname{dist}(b,c)=d.

A configuration $C:\{0,1\}\to M$ places two labelled servers on points of $M$ . A deterministic on-line algorithm assigns to every finite request sequence $\sigma=(r_1,\dots,r_n)$ a configuration, computed from $\sigma$ alone and covering the last request; its value on the empty sequence is its initial configuration. Its cost $C_A(\sigma)$ is the total distance its servers move while serving $\sigma$ request by request. The off-line optimum $C_{opt}(\sigma)$ from an initial configuration $C_0$ is the least total movement of any schedule that starts at $C_0$ and covers each request in turn, knowing $\sigma$ in advance.

A randomized algorithm is a probability distribution on deterministic on-line algorithms; its expected cost is $\mathbf{E}C_A(\sigma)$ . It is $\rho$ -competitive against an oblivious adversary from $C_0$ if every algorithm in its support starts at $C_0$ and there is a constant $a$ such that

\mathbf{E}C_A(\sigma)\le\rho\cdot C_{opt}(\sigma)+a\qquad\text{for every request sequence }\sigma.

The request sequence is fixed in advance and does not react to the algorithm's coin flips.

Write $e_p=(1+1/p)^p$ and

\alpha_d=\frac{e_{2d-1}+1/4d}{(e_{2d-1}-1)+1/2d},\qquad e_{2d-1}=\left(\frac{2d}{2d-1}\right)^{2d-1}.

In Lean this is NonuniformCompetitive.Isosceles.isoscelesRatio d.

Formalization targets

Goal: Theorem 12

For every $d\ge1$ and every initial configuration $C_0$ :

\forall A,\ \forall\rho,\quad A\text{ is }\rho\text{-competitive from }C_0\ \Longrightarrow\ \rho\ge\alpha_d,

\exists A:\ A\text{ is }\alpha_d\text{-competitive from }C_0.

The two claims are also milestones of their own (no_better_ratio, ratio_attained).

The phase LP (§5, pp. 565–566)

For free real $\pi_1,\dots,\pi_{2d-1}$ and real $\alpha$ with

(\pi_k)2d+\sum_{i=1}^k(1-\pi_i)\le\alpha k\ \ (1\le k<2d),\qquad 2d+\sum_{i=1}^{2d-1}(1-\pi_i)+\tfrac12\le\alpha\cdot2d,

one has $\alpha\ge\alpha_d$ (lp_lower_bound); and $\pi_k=(\alpha_d-1)\big((2d/(2d-1))^k-1\big)$ , $\pi_{2d}=1$ is nondecreasing from $\pi_1\ge0$ to $1$ and makes every constraint an equality (lp_attained).

The limit remark (§5, p. 566)

\alpha_1<\alpha_2<\alpha_3<\cdots,\qquad \lim_{d\to\infty}\alpha_d=\frac{e}{e-1}

(ratio_increases_to_e_ratio).

Significance

The theorem gives an exact optimal randomized ratio for an infinite family of metric spaces. It shows that the optimal randomized two-server ratio is not a constant: it runs from $3/2$ on the equilateral triangle to $e/(e-1)\approx1.582$ as the triangle becomes long and thin, where the problem resembles ski rental. With the deterministic ratio $2$ , it quantifies exactly how much randomization gains on these spaces.

The results are proved in the paper; none is formalized on Prove2Me, and no machine-checked proof of them is known. A formal proof would require the paper's phase framework (Theorems 1–3 and the appendix's Theorem 15) for server problems, which this mission does not state separately, and a concrete randomized algorithm as a measurable mixed strategy. Both would be reusable for Theorem 13 (the 3-4-5 triangle) and for other exact ratios on small metric spaces.

Difficulty

The phase LP milestones are finite real arithmetic. The difficulty is the passage between them and the goal. The lower bound must hold for every randomized algorithm, not only phase-based lazy ones: an arbitrary algorithm may condition on the whole history, move non-lazily, and randomize in ways that do not reduce to the probabilities $\pi_k$ . The paper handles this with Theorem 3, which says that the LP bound of phase-based algorithms bounds the competitive factor of all algorithms; its proof uses an averaging argument over histories that must be made rigorous. The upper bound needs a mixed strategy over infinitely many phases, with measurable costs, an explicit additive constant covering the first partial phase from an arbitrary initial configuration, and an accounting of $C_{opt}$ across phase boundaries.

Formalization scope

The model is the platform's published KServer_model and KServer_randomized (reference items): labelled servers Fin 2 → M; a deterministic on-line algorithm as a map from request prefixes to configurations; a randomized algorithm as a probability measure over deterministic algorithms, with the cost of each fixed sequence measurable in the random outcome; expected cost as a lower Lebesgue integral in $[0,\infty]$ ; the off-line optimum as a real infimum over schedules from $C_0$ (nonempty and bounded below by $0$ ); and IsCompetitiveFrom A C₀ c with a real additive constant.

Committed conventions:

The triangle is any metric space whose points are exactly $a,b,c$ at distances $1,d,d$ , with $d$ a natural number and $d\ge1$ . Every such space is isometric to the paper's triangle; at $d=0$ it would not be a triangle.
Both claims are stated for every initial configuration, including both servers on one point. The paper treats the initial state $\{a,b\}$ separately and absorbs the first partial phase into the additive constant.
The lower bound quantifies over all randomized algorithms (deterministic ones are point masses), never over phase-based ones only.
In the LP milestones the $\pi_k$ are free reals, as printed; no box $0\le\pi_k\le1$ is imposed.
"Grows" in the limit remark is read as strictly increasing.
The paper prints the recurrence on p. 565 as $\pi_k=\frac{\alpha-1+(\pi_{k-1})2d-1}{2d}$ ; the equations $(*)$ give $\pi_k=\frac{\alpha-1+2d\,\pi_{k-1}}{2d-1}$ . The recurrence is not used; the closed form printed on p. 566 is correct and is the one stated.

Without the measurability field of a randomized algorithm the lower integral would under-report expected cost and the attainment claim would become easier than the paper's; the published definition includes it. The lower bound is not vacuous: the triangle hypotheses are satisfiable for every $d\ge1$ .

Welcome contributions: a formal version of the phase framework (Theorems 1–3, 15) for finite metric spaces, reusable across missions III and IV; a measurable construction of phase-based randomized algorithms; and proofs of the LP milestones.

Selected references

A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994) 542–571. https://doi.org/10.1007/BF01189993
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11 (1990) 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
H. Karloff, Y. Rabani, Y. Ravid, Lower Bounds for Randomized k-Server and Motion-Planning Algorithms, SIAM J. Comput. 23 (1994) 293–312. https://doi.org/10.1137/S0097539792224838
S. Bubeck, C. Coester, Y. Rabani, The Randomized k-Server Conjecture Is False!, STOC 2023. https://arxiv.org/abs/2211.05753

9 thms3 active usersReviewed

Algorithmic Game Theory Dynamical Systems Stochastic Systems·Captain: mikedeng1

On the Global Convergence of Stochastic Fictitious Play IV: Almost Sure Convergence in Supermodular Games with a Unique Rest PointResearch Paper

Motivation

Fictitious play is the oldest model of learning in games: each player repeatedly best-responds to the empirical frequencies of the opponents' past play. Stochastic fictitious play adds random payoff disturbances before each choice, so that players choose smoothed ("perturbed") best responses. It is a standard model in economics and in the study of learning in games (Fudenberg and Levine, 1998), and its long-run behavior is described through a deterministic mean dynamic, the perturbed best response dynamic, using stochastic approximation theory (Benaïm and Hirsch, 1999).

Supermodular games model strategic complementarities: the gain from moving to a higher strategy increases when opponents move to higher strategies. They arise in coordination, oligopoly and macroeconomic models (Milgrom and Roberts, 1990; Vives, 1990). Hofbauer and Sandholm (Econometrica 2002) show that in such games stochastic fictitious play converges almost surely whenever its mean dynamic has a unique rest point. This mission formalizes that result and the chain of lemmas behind it (Section 5 and the Appendix of the paper).

Timeline. Benaïm and Hirsch (1999) observed that supermodular games with exactly two strategies per player yield strongly monotone perturbed best response dynamics. Hofbauer and Sandholm (2002) extended this to any number of strategies by introducing stochastic dominance coordinates, and proved Theorem 6.1(iv). Benaïm (2000) supplied the low-dimensional convergence theorem used for the dimension ≤ 2 clause.

Setting

A $p$ player normal form game gives player $\alpha$ an ordered finite strategy set $S^\alpha = \{0,\dots,n^\alpha - 1\}$ and a utility $u^\alpha$ on pure profiles. $\Sigma = \prod_\alpha \Delta S^\alpha$ is the set of mixed profiles, and player $\alpha$ 's payoff vector is $U^\alpha_i(x^{-\alpha}) = \sum_{s:\, s^\alpha = i} u^\alpha(s) \prod_{\beta \ne \alpha} x^\beta_{s^\beta}$ .

The game is strictly supermodular if for all distinct players $\alpha \ne \beta$ and all profiles $s, \hat s$ with $s^\alpha > \hat s^\alpha$ and $s^{-\alpha} = \hat s^{-\alpha}$ , the difference $u^\alpha(s) - u^\alpha(\hat s)$ is strictly increasing in $s^\beta = \hat s^\beta$ .

Each player $\alpha$ has a shock density $f^\alpha$ on $\mathbb R^{n^\alpha}$ , strictly positive, whose choice function $C^\alpha_i(\pi) = P(\operatorname{argmax}_j \pi_j + \varepsilon_j = i)$ is continuously differentiable. The perturbed best response is $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$ , and the perturbed best response dynamic is

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

$RP(\mathrm P)$ is its set of rest points in $\Sigma$ and $CR(\mathrm P)$ its chain recurrent set.

In standard stochastic fictitious play the shocks $\varepsilon^\alpha_t$ have densities $f^\alpha$ and are independent over time and across players. From an arbitrary initial pure profile $\zeta_1$ , each player at time $t+1$ plays the pure strategy maximizing $U^\alpha_k(Z_t^{-\alpha}) + (\varepsilon^\alpha_t)_k$ , where $Z_t = \frac1t \sum_{u \le t} \zeta_u$ is the vector of empirical frequencies.

The stochastic dominance coordinates are $(T^\alpha x^\alpha)_i = \sum_{j > i} x^\alpha_j \in \mathbb R^{n^\alpha - 1}$ , the mass on strategies above $i$ ; $T x \le T y$ means each $y^\alpha$ stochastically dominates $x^\alpha$ . In these coordinates (P) becomes a dynamic (T) on $T(\Sigma)$ .

Formalization targets

Goal: Theorem 6.1(iv), unique rest point clause

For a strictly supermodular game with $p \ge 2$ players and shock densities as above, if $RP(\mathrm P) = \{x^*\}$ then

P\Big(\lim_{t\to\infty} Z_t = x^*\Big) = 1,

on every probability space, for every independent shock family with the given densities and every initial profile.

Milestones

Lemma A.2, eq. (14), Lemma A.3 and eqs. (17)–(18): the order-theoretic and differential facts behind monotonicity.
Theorem 5.1: $T^{-\alpha} y^{-\alpha} \ge T^{-\alpha} x^{-\alpha} \Rightarrow T^\alpha \tilde B^\alpha(y^{-\alpha}) \ge T^\alpha \tilde B^\alpha(x^{-\alpha})$ .
Theorem 5.2: there are rest points $\underline x, \bar x$ with $RP(\mathrm P) \subseteq [\underline x, \bar x]$ .
Proposition 5.3: (P) and (T) are linearly conjugate.
Theorem 5.4: (T) is cooperative and irreducible.
Corollary 5.5(i)–(ii): (P) is strongly monotone, and $CR(\mathrm P) \subseteq [\underline x, \bar x]$ , so $CR(\mathrm P) = \{x^*\}$ when the rest point is unique.

Significance

The result gives global almost-sure convergence of a stochastic learning process in a broad class of games with many strategies, where earlier results needed two strategies per player or specific payoff structures. It also shows which properties of the choice function matter: only eqs. (17)–(18), not the symmetry of its derivative used for potential and zero-sum games.

The paper's proof is complete but relies on outside results: stochastic approximation (Benaïm–Hirsch 1999, Benaïm 1999), monotone dynamical systems (Smith 1995), and the inclusion of the chain recurrent set in the global attractor (Robinson 1995). None of these, nor the Hofbauer–Sandholm theorem itself, is formalized in any proof assistant as far as known. The mission produces a machine-checked version of the theorem and of the Section 5 monotonicity theory.

Difficulty

The monotonicity lemmas are finite-dimensional calculus and summation by parts. The substantial steps are elsewhere. Strong monotonicity of a cooperative irreducible system (Corollary 5.5(i)) is a theorem of monotone dynamical systems that Mathlib does not have, and it must hold on the closed, non-open state space $T(\Sigma)$ . The step from the ODE to the random process needs the stochastic approximation theorem: the empirical frequencies are an asymptotic pseudotrajectory of (P), and their limit set is almost surely internally chain transitive. Knowing that $x^*$ is globally asymptotically stable for (P) does not by itself give almost-sure convergence of $Z_t$ . The limit set of the random process must be related to the chain recurrent set of (P), which is where Corollary 5.5(ii) enters.

Formalization scope

Players are Fin p, strategies Fin (n α) (0-based, same order as the paper), with every $n^\alpha \ge 1$ . Mixed profiles live in the ambient space $\prod_\alpha \mathbb R^{n^\alpha}$ with the sup norm. The fields of (P) and (T) are defined on the whole ambient space, so partial derivatives are ordinary Fréchet derivatives. Densities are $[0,\infty]$ -valued. Solutions are forward solutions staying in the state space. The chain recurrent set quantifies over solutions, which are unique here because the fields are $C^1$ . The process $Z_t$ is defined pathwise from the shocks, with ties in the argmax broken by the smallest index (a null event). Densities may differ across players.

A statement about the ODE (P), or about a single noise law such as logit, would be a different and much weaker theorem. The goal is about the random process $Z_t$ , on every probability space carrying independent shocks with the given densities. Irreducibility and strong monotonicity additionally assume that two distinct players each have at least two strategies; when one player owns every stochastic dominance coordinate and has at least two of them, supermodularity holds vacuously while irreducibility fails.

A complete development needs: random utility choice functions and their derivatives; monotone and cooperative ODE theory on convex sets; the chain recurrent set and the global attractor; stochastic approximation for processes with step size $1/t$ . The last three are reusable well beyond this mission. Contributions to any milestone, and general-purpose lemmas on cooperative systems or stochastic approximation, are welcome.

Selected references

J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70 (2002), 2265–2294. https://doi.org/10.1111/1468-0262.00376 (formalized from the authors' manuscript of February 21, 2002)
M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Repeated Games, Games and Economic Behavior 29 (1999), 36–72. https://doi.org/10.1006/game.1997.0636
M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer (1999). https://doi.org/10.1007/BFb0096509
M. Benaïm, Convergence with Probability One of Stochastic Approximation Algorithms Whose Average is Cooperative, Nonlinearity 13 (2000), 601–616. https://doi.org/10.1088/0951-7715/13/3/305
H. L. Smith, Monotone Dynamical Systems, AMS Mathematical Surveys and Monographs 41 (1995). https://doi.org/10.1090/surv/041
P. Milgrom and J. Roberts, Rationalizability, Learning, and Equilibrium in Games with Strategic Complementarities, Econometrica 58 (1990), 1255–1277. https://doi.org/10.2307/2938316
D. Fudenberg and D. K. Levine, The Theory of Learning in Games, MIT Press (1998).

17 thms3 active usersReviewed

Probability

Missions

Markov Chains and Mixing Times VIII: Path Coupling and Approximate CountingTextbook

Motivation

Setting

Formalization targets

Goal

Milestones

Significance

Difficulty

Formalization scope

Selected references

Markov Chains and Mixing Times VI: Networks, Hitting Times, and Cover TimesTextbook

Motivation

Setting

Formalization targets

Goal

Milestones

Significance

Difficulty

Formalization scope

Selected references

Treatment Locality in A/B TestingResearch Paper

Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary DistributionTextbook

Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary Distribution

Motivation

Setting

Formalization targets

Goal

Milestones toward and around the goal

Significance

Difficulty

Formalization scope

Selected references

The Price of Anarchy of Finite Congestion Games V: The Mixed Price of Anarchy of the Average Social Cost Is at Most (3+sqrt 5)/2Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 14

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Dantzig Selector: Statistical Estimation When p Is Much Larger than n 2: Oracle Inequality within a Logarithmic Factor of the Ideal Mean Squared ErrorResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.2 (pp. 8–9)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Dantzig Selector: Statistical Estimation When p Is Much Larger than n 1: ℓ2 Error Bound for Sparse Parameters under the Uniform Uncertainty PrincipleResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Air Travel Demand and Airline Seat Inventory Management I: Marginal Seat Allocation Among Distinct Fare ClassesTextbook

Why airlines allocate seats by fare class

Setting

Formalization targets

Goal: the nnn largest marginal values give the optimal booking limits (p. 90)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Polylogarithmic-Competitive Algorithm for the k-Server Problem: Randomized k-Server Is O(log² k · log³ n · log log n)-Competitive on Every n-Point MetricResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Goal: the $n$ largest marginal values give the optimal booking limits (p. 90)