Probability

Motivation

A retailer with a large catalogue but a limited display (a web page, a shelf, a search result) must decide which assortment of products to show each arriving customer. Customers choose among the displayed products or leave without buying, and the retailer does not know their preferences in advance; it learns them only from the purchases it observes. This is the MNL-Bandit problem of Agrawal, Avadhanula, Goyal and Zeevi (arXiv:1706.03880v2; Operations Research 67(5), 2019), in which customer choices follow the multinomial logit model, the workhorse of revenue management and marketing.

The same paper gives an epoch-based upper-confidence-bound policy whose regret is at most of order $\sqrt{NT\log NT}$ (its Theorem 1). This mission formalizes the matching lower bound, the paper's Theorem 2: under a constraint that at most $K$ products be displayed, no policy can have regret smaller than order $\sqrt{NT/K}$ on every instance. Lower bounds of this kind are what certify that an algorithm is near-optimal rather than merely good.

Timeline. The square-root lower bound for $N$-armed bandits goes back to Auer, Cesa-Bianchi, Freund and Schapire (2002), presented in the survey of Bubeck and Cesa-Bianchi (arXiv:1204.5721, 2012). Rusmevichientong, Shen and Shmoys (2010) and Sauré and Zeevi (2013) minimized regret under MNL choice with explore-then-exploit policies, obtaining $O(N^2\log^2T)$ and $O(N\log T)$ bounds for instances whose best and second-best assortments are well separated. Agrawal et al. (2017–2019) proved the instance-independent $\Omega(\sqrt{NT/K})$ lower bound formalized here; Chen and Wang (2017) later obtained $\Omega(\sqrt{NT})$ when $K<N/4$.

Setting

There are $n$ products. An instance consists of a no-purchase weight $v_0>0$, attraction parameters $v_1,\dots,v_n$ with $0\le v_i\le v_0$, and revenues $r_i\in[0,1]$. At each period $t=1,\dots,T$ the seller offers an assortment $S_t\subseteq\{1,\dots,n\}$ and observes a choice $c_t\in S_t\cup\{0\}$, where $0$ means no purchase. Under the multinomial logit (MNL) model,

$$p_i(S)=\frac{v_i}{v_0+\sum_{j\in S}v_j}\quad(i\in S\cup\{0\}),\qquad p_i(S)=0\ \text{otherwise},$$

and choices are independent across periods given the offered sets. The expected revenue of $S$ is $R(S,v)=\sum_{i\in S}r_iv_i/(v_0+\sum_{j\in S}v_j)$.

A policy chooses $S_t$ from the past assortments and choices, possibly at random. It satisfies the $K$-cardinality constraint if $|S_t|\le K$ always. Its regret over $T$ periods is

$$\mathrm{Reg}_\pi(T,v)=\mathbb E_\pi\Big(\sum_{t=1}^{T}R(S^*,v)-R(S_t,v)\Big),$$

where $S^*$ maximizes $R(\cdot,v)$ over assortments of at most $K$ products.

A randomized instance is a probability distribution over instances with common known revenues and a common no-purchase weight; the regret against it is averaged over the hidden attraction parameters, the choices and the policy's randomization.

Formalization targets

Goal: Theorem 2 (p. 14)

There is an absolute constant $C>0$ such that for all $n\ge2$, $1\le K\le n$ and $T\ge n$ there is a finitely supported randomized instance, chosen before the policy, such that every policy $\pi$ respecting the $K$-cardinality constraint satisfies

$$\mathbb E_{v}\big[\mathrm{Reg}_\pi(T,v)\big]\ge C\sqrt{\frac{nT}{K}} .$$

The constant is not fixed; any positive value suffices.

Milestones

The paper proves Theorem 2 in two cases.

1. Lemma E.1 (p. 57): the Bernoulli divergence bound $\mathrm{kl}(\alpha,\alpha+\epsilon)\le 4\epsilon^2/\alpha$ in the direction used by Lemma E.2.
2. Lemma E.2 (p. 57): for a guessing algorithm on $N\ge12$ coins and $t\le N\alpha/(60\epsilon^2)$, at least $N/3$ hiding places $j$ of the biased coin have $\mathcal P_j(a_t=j)\le 1/2$.
3. Lemma 5.1 (p. 15): on the Bernoulli instance $I_{\mathrm{MAB}}$ with $\epsilon=\frac1{100}\sqrt{N\alpha/T}$, every online algorithm has expected regret at least $\epsilon T/6$.
4. Lemma E.4 (p. 60): one period of MNL feedback on the instance $\hat I_{\mathrm{MNL}}$, where $\epsilon=\sqrt{1/(32T)}$, has divergence at most $4\epsilon^2$.
5. Lemma E.5 (p. 61): over $T$ periods the two choice laws of that instance have divergence at most $4T\epsilon^2$.

Items 1–3 serve the case $K<n$, which the paper reduces to a multi-armed bandit through the instance $I_{\mathrm{MNL}}$ of Definition 5.2 ($NK$ products in $N$ groups of $K$, one hidden group with larger attraction). Items 4–5 serve the case $K=n$ through the two-point instance $\hat I_{\mathrm{MNL}}$ of Definition E.1.

Significance

The theorem shows that the $\sqrt{T}$ growth of regret in assortment learning cannot be improved, and that the dependence on the number of products is polynomial: when the display size $K$ is fixed, the UCB policy of the same paper is optimal up to logarithmic factors (Remark 4). It separates what learning under the MNL model costs from what the combinatorics of the assortment adds, and the reduction it uses, simulating an assortment algorithm inside a bandit algorithm, is reusable for other choice-model bandits.

The result is proved in the paper, with its proof in Appendix E. To our knowledge neither the theorem nor its lemmas have been machine-checked. A formal proof has to repair several printed slips: Lemma 5.1's hypotheses do not exclude $\alpha$ close to $1$, where the bound fails; the proof of Lemma E.2 uses a form of Pinsker's inequality with a wrong constant; Lemma E.1 states one direction of the divergence and computes the other; and the constants of the $K=N$ case do not match. The formal statements here carry the corrected hypotheses, each disclosed in its note.

Difficulty

The obvious argument fails at the reduction. The bandit lower bound is a statement about algorithms that pull one arm per round, while an assortment policy offers $K$ products at once and sees a choice among them. Transferring the bound requires simulating MNL feedback from Bernoulli coins (Algorithm 2 of the paper), whose loop has a random length, and then relating the regret of the simulated assortment algorithm over a random number of calls to the bandit regret over $T$ pulls. The paper does this in expectation, and the constants have to be tracked through the random horizon.

A second difficulty is that the lower bound must hold for every policy, including randomized ones, against a single randomized instance fixed in advance. Bounding the regret of each deterministic policy separately is not enough unless the instance does not depend on the policy, which the statement requires. The change-of-measure steps (Lemmas E.2 and E.5) need a chain rule for the divergence between laws of adaptively generated histories.

Formalization scope

Products, periods and arms are 0-based (Fin n); a choice is Option (Fin n) with none the no-purchase alternative. Histories have finite length $T$, laws of histories are explicit products of policy weights and MNL (or Bernoulli) probabilities, and every expectation is a finite sum, so no measurability or integrability side conditions arise. The no-purchase weight $v_0$ is explicit (Definition 5.2 has $v_0=K$). $R(S^*,v)$ is a maximum over the finite, nonempty family $\{S:|S|\le K\}$.

Policies are behavioural: at every history they give a probability vector over assortments, which by Kuhn's theorem covers the paper's admissible policies with external randomization. The randomized instance is a finite list of instances with nonnegative weights summing to one; every support point has the same revenues and no-purchase weight, which are known to the seller. The quantifiers are in the paper's order: the constant first, then $n,K,T$, then the randomized instance, then every policy. A formalization with the policy quantified before the instance, with $C=0$ allowed, with varying known revenues across hidden support points, or with only deterministic policies, would be weaker and is ruled out.

Hypotheses added to the printed statements: $n\ge2$ and $K\ge1$ in Theorem 2 (the claim fails for $n=1$ and $K=0$); $0<\alpha$, $0<\epsilon$, $\alpha+\epsilon\le3/4$ in Lemma E.1; $0<\alpha$, $0<\epsilon$, $2\alpha+\epsilon\le1$ in Lemma E.2; $0<\alpha$, $2\alpha+\epsilon\le1$, $T\ge1$ in Lemma 5.1. Lemmas E.4 and E.5 use Definition E.1's $\epsilon=\sqrt{1/(32T)}$, with $T\ge1$ and $n\ge2$ so the instance is defined. Lemma E.5 is stated, as in its proof, for deterministic policies.

The development reuses three published definitions: the MNL revenue ChoiceCDLP.MNL.mnlObjective, the Bernoulli divergence RegretBandits.Stochastic.klBern, and the discrete Kullback–Leibler divergence FoundationsRL.GeneralDM.klDivDiscrete (valued in $[0,\infty]$). Proved platform results useful to solvers include Pinsker's inequality (BanditAlgorithm.pinsker_inequality_total_variation), the Bernoulli bound $d(p,q)\le(q-p)^2/(p(2-p-q))$ (BanditAlgorithm.bernoulli_relative_entropy_le_sq_div_of_add_le_one) and a divergence decomposition for bandits. A chain rule for the divergence of finite adaptive histories, and a formal version of the simulation of Algorithm 2, would be reusable beyond this mission; both are welcome as supporting lemmas.

Selected references

• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5):1453–1485, 2019; preprint arXiv:1706.03880v2. https://arxiv.org/abs/1706.03880 — DOI https://doi.org/10.1287/opre.2018.1832
• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://arxiv.org/abs/1204.5721
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• D. Sauré, A. Zeevi, Optimal Dynamic Assortment Planning with Demand Learning, Manufacturing & Service Operations Management 15(3), 2013. https://doi.org/10.1287/msom.2013.0429
• X. Chen, Y. Wang, A Note on a Tight Lower Bound for MNL-Bandit Assortment Selection Models, arXiv:1709.06109, 2017. https://arxiv.org/abs/1709.06109

Motivation

A convention is a pattern of behaviour that is customary because everyone expects everyone else to follow it: driving on the right, or which party yields at a narrow bridge. Peyton Young's The Evolution of Conventions (Econometrica 61 (1993) 57–84) asks how such a pattern can emerge from decentralized play. The players have limited memory and limited information, and nobody coordinates them. The paper's model, adaptive play, is now a standard dynamic of learning in games. It is the starting point of the stochastic-stability theory of equilibrium selection (Foster and Young 1990; Kandori, Mailath and Rob 1993), which builds on the perturbation theory of Freidlin and Wentzell (1984).

This mission covers the first half of the paper: §3 (the model) and §4 (convergence when the players make no mistakes). Before mistakes can be added and stochastically stable conventions selected, the unperturbed process must be shown to settle at all. Theorem 1 gives the condition under which it does.

Setting

Let $\Gamma$ be a game with finitely many players $i$, a finite nonempty strategy set $S_i$ for each player, and payoffs $u_i(s)$ for strategy tuples $s \in \prod_j S_j$. Write $(x, s_{-i})$ for $s$ with player $i$'s strategy replaced by $x$.

• A play is a strategy tuple. Fix a memory $m$ and a sample size $k$ with $1 \le k \le m$. The state $h \in H = (\prod_j S_j)^m$ is the sequence of the last $m$ plays, oldest first.
• A successor of $h$ is obtained by deleting the oldest play and appending a new one.
• A sample is a set of $k$ positions of $h$. Player $i$'s best reply to a sample $K$ maximizes the total payoff $\sum_{t \in K} u_i(x, (h_t)_{-i})$ against the sampled plays.
• A best-reply distribution gives, for each $i$ and $h$, a probability distribution $p_i(\cdot \mid h)$ on $S_i$ that is positive exactly on the strategies that are best replies to some sample of size $k$. The sampling law itself is arbitrary.
• Adaptive play $P^0$ is the Markov chain on $H$ that moves from $h$ to the successor with new play $s$ with probability $\prod_i p_i(s_i \mid h)$.
• A strict Nash equilibrium is a tuple $s$ from which every unilateral deviation is strictly worse. A convention is a state $(s, s, \dots, s)$ with $s$ a strict Nash equilibrium.
• The best-reply graph has an edge $s \to (x, s_{-i})$ whenever $x \ne s_i$ is a best reply of $i$ to $s_{-i}$. $\Gamma$ is weakly acyclic if from every $s$ a directed path leads to a sink. $L(s)$ is the length of a shortest such path from $s$ to a strict Nash equilibrium, and $L_\Gamma = \max_s L(s)$.

Formalization targets

Goal: Theorem 1 (p. 64)

If $\Gamma$ is weakly acyclic and $k \le m/(L_\Gamma + 2)$, then for every best-reply distribution and every initial state $h$,

$$\lim_{t\to\infty} \sum_{h' \text{ a convention}} \big((P^0)^t\big)_{hh'} = 1 .$$

Milestones

1. Absorbing states (§4, p. 62): $P^0_{hh} = 1$ if and only if $h$ is a convention.
2. Sinks (§4, p. 64): the sinks of the best-reply graph are exactly the strict Nash equilibria. Hence weak acyclicity means that one-player-at-a-time best replies can reach a strict equilibrium from every tuple.
3. A run of best replies (proof of Theorem 1, p. 64): if $m \ge 2k-1$, then with positive probability $k$ consecutive identical best replies to the last $k$ plays are appended.
4. Uniform bound (proof of Theorem 1, p. 65): there is $q > 0$ such that from every state a convention is reached within $M = kL_\Gamma + m$ periods with probability at least $q$.
5. Geometric tail (proof of Theorem 1, p. 64): such a uniform bound makes the probability of no convention after $rM$ periods at most $(1-q)^r$.
6. Example 2 (pp. 65–66, off the goal's path): in a Battle-of-the-Sexes game with complete sampling $k = m$, a perfectly miscoordinated history stays miscoordinated forever.

Significance

Theorem 1 identifies a class of games, the weakly acyclic ones, in which boundedly rational players who best-reply to small random samples of the past almost surely lock in to a strict pure equilibrium. The paper's examples of weakly acyclic games (p. 63) are pure coordination games and games with common interests in which no two strategy tuples are payoff equivalent. Absorption is in behaviour, not just in empirical frequencies. Example 2 shows that this fails for fictitious-play-like complete sampling, so the sampling ratio $k/m$ is a real ingredient. The absorbing states identified in the first milestone are the states among which the stochastic-stability analysis of the paper's later sections selects.

The result is proved in the paper. To the best of our knowledge no machine-checked version exists. The mission asks for a formal proof of Theorem 1 and its milestones for an arbitrary best-reply distribution. That generality is the paper's own: non-uniform sampling is explicitly allowed. A formal proof also pins down the memory bookkeeping in the paper's proof (look-backs of $2k-1$, $3k-1$ and $kr + 2k - 1$ periods), which the text checks only in words.

Difficulty

Adaptive play is a finite Markov chain. The obvious route through the generic theory of absorbing chains requires showing that a convention is reachable from every state, and that is where the argument becomes delicate. A best-reply path in the game cannot be followed directly: each player only sees a random sample, and the players who are not moving must keep playing their old strategies. The proof gets around this by having the non-moving players keep sampling older parts of the history, so those parts must still be in memory. This is what forces the bound $k \le m/(L_\Gamma+2)$. A uniform, state-independent constant is then needed to turn reachability into almost-sure convergence.

Formalization scope

Players form a finite type ι, strategies a family of finite nonempty types S i, and payoffs u : ι → (∀ i, S i) → ℝ. A state is Fin m → ∀ i, S i with position 0 the oldest play. A best-reply distribution is any p : ∀ i, H → S i → ℝ with the stated support. All statements quantify over every such p. Adaptive play is a Matrix H H ℝ, and "converges almost surely to a convention" is stated through matrix powers. That is equivalent to almost-sure absorption because conventions are absorbing. The condition $k \le m/(L_\Gamma+2)$ is $k(L_\Gamma+2) \le m$ in ℕ. $L(s)$ is an sInf on ℕ that is never empty under weak acyclicity.

The display (1) on p. 62 reads "the right-most element of $h$". The formalization uses the right-most element of the successor $h'$, the only reading under which the rule is meaningful.

The goal cannot be satisfied trivially. The sampling law is not fixed, the conclusion is a limit equal to $1$ from every initial state (not "with positive probability" or "along some path"), and the hypotheses are jointly satisfiable, for example by a $2\times2$ coordination game with uniform sampling. A best reply to a sample uses the joint empirical distribution of the sampled plays, not independent marginals.

A complete development needs elementary Markov-chain facts about matrix powers and absorbing sets, plus combinatorics of shifted histories. These parts are reusable for any finite-memory learning dynamic. Proofs of individual milestones are welcome independently.

Related platform work: stochastic fictitious play in potential games (StochFictPlay.*, Hofbauer–Sandholm 2002) and calibrated learning to correlated equilibrium (CalibratedCE.*, Foster–Vohra 1997) formalize other learning dynamics. The perturbed process and the selection of risk-dominant conventions are the subject of the sibling missions The Evolution of Conventions II and III.

Selected references

• H. P. Young, The Evolution of Conventions, Econometrica 61(1), 1993, 57–84. https://doi.org/10.2307/2951778
• D. Foster and H. P. Young, Stochastic Evolutionary Game Dynamics, Theoretical Population Biology 38, 1990, 219–232. https://doi.org/10.1016/0040-5809(90)90011-J
• M. Kandori, G. J. Mailath and R. Rob, Learning, Mutation, and Long Run Equilibria in Games, Econometrica 61(1), 1993, 29–56. https://doi.org/10.2307/2951777
• M. I. Freidlin and A. D. Wentzell, Random Perturbations of Dynamical Systems, Springer, 1984. https://doi.org/10.1007/978-1-4684-0176-9
• J. C. Harsanyi and R. Selten, A General Theory of Equilibrium Selection in Games, MIT Press, 1988.
• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2002, 2265–2294. https://doi.org/10.1111/1468-0262.00376
• 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

Motivation

Many models in economics, biology and computer science are finite Markov chains that have several absorbing states or recurrent classes, so their long-run behaviour depends on where they start. Adding a small amount of noise (mistakes, mutations, experimentation) makes the chain irreducible, and the noisy chain then has a unique stationary distribution. As the noise vanishes, that distribution concentrates on some of the original recurrent classes. The stochastically stable states are the ones that keep positive weight in the limit; they are the states the system spends nearly all its time in when the noise is small but nonzero.

H. Peyton Young's The Evolution of Conventions (Econometrica, 1993) proved a general finite-state characterization of these states, which he used to select among the equilibria of coordination games under adaptive play. The characterization rests on the theory of small random perturbations of Freidlin and Wentzell (1984), developed for diffusions, and on a combinatorial lemma of theirs expressing stationary distributions through spanning trees. Kandori, Mailath and Rob (1993) characterized the limit distribution by spanning trees on the whole state space for their model of learning with mutations; Young's Lemma 1 generalizes their Theorem 1 (p. 78), and his Lemma 2 reduces the computation to the much smaller graph of recurrent classes. Foster and Young (1990) introduced stochastic stability for evolutionary dynamics, and the equilibria it selects in $2\times 2$ games coincide with the risk-dominant equilibria of Harsanyi and Selten (1988).

Setting

Let $X$ be a finite set and $P^0$ the transition matrix of a Markov chain on $X$. A state $y$ is reachable from $x$ if $(P^0)^n_{xy} > 0$ for some $n \ge 0$; $x$ is recurrent if every state reachable from $x$ can reach $x$ back; the recurrent communication classes $X_1, \dots, X_J$ are the communication classes of recurrent states.

A family $(P^\varepsilon)_{\varepsilon \in (0,a]}$ of Markov chains on $X$ is a regular perturbation of $P^0$ if for all $x, y$:

• (6) $P^\varepsilon$ is aperiodic and irreducible for every $\varepsilon \in (0,a]$;
• (7) $P^\varepsilon_{xy} \to P^0_{xy}$ as $\varepsilon \to 0$;
• (8) if $P^\varepsilon_{xy} > 0$ for some $\varepsilon$, there is $r \ge 0$ with $0 < \lim_{\varepsilon \to 0} \varepsilon^{-r} P^\varepsilon_{xy} < \infty$.

The exponent $r = r(x,y)$ is the resistance of the transition $x \to y$. The graph $G$ has vertex set $X$ and an edge $(x,y)$ when $P^\varepsilon_{xy} > 0$ for all small $\varepsilon$, weighted by $r(x,y)$.

For $z \in X$, a $z$-tree is a spanning tree of edges of $G$ in which every $x \ne z$ has a unique directed path to $z$. The potential of $z$ is

$$\gamma(z) = \min_{T \in \mathcal T_z} \sum_{(x,y) \in T} r(x,y). \tag{9}$$

For classes $i \ne j$, $r_{ij}$ is the least resistance of a path in $G$ from $X_i$ to $X_j$. On the complete directed graph $\mathcal G$ with vertices $1, \dots, J$ and edge weights $r_{ij}$, the stochastic potential $\gamma_j$ of $X_j$ is the least total weight of a $j$-tree in $\mathcal G$.

Formalization targets

Goal: Theorem 4 (p. 78)

If $\mu^\varepsilon$ is the stationary distribution of $P^\varepsilon$ for $\varepsilon \in (0,a]$, then $\mu^\varepsilon \to \mu^0$ as $\varepsilon \to 0$, where $\mu^0$ is a stationary distribution of $P^0$, and

$$\mu^0_x > 0 \iff x \in X_j \text{ for some } j \text{ with } \gamma_j = \min_i \gamma_i .$$

Milestones, in the order of the paper's proof

1. Resistance (p. 77). The exponent in (8) is unique; a transition positive for some $\varepsilon$ is an edge of $G$; and the edges of zero resistance are exactly the transitions with $P^0_{xy} > 0$.
2. Markov chain tree formula (p. 79). For an aperiodic irreducible chain $P'$, $\mu'_z = p'_z / \sum_x p'_x$ with $p'_z = \sum_{T \in \mathcal T_z} \prod_{(x,y)\in T} P'_{xy}$ is the unique stationary distribution.
3. Lemma 1 (p. 78). $\mu^\varepsilon \to \mu^0$, $\mu^0$ is stationary for $P^0$, and $\mu^0_x > 0$ iff $\gamma(x) \le \gamma(y)$ for all $y$.
4. (p. 80) A stationary distribution of a finite chain vanishes on non-recurrent states.
5. (p. 80) All states of a recurrent class of $P^0$ have the same potential.
6. Lemma 2 (p. 80). $\gamma(x) = \gamma_j$ for every $x \in X_j$.

Significance

Theorem 4 turns a limit of stationary distributions into a finite optimization: compute least-resistance paths between the recurrent classes, then a minimum-weight arborescence on the reduced graph. The answer depends only on the orders of magnitude of the perturbations, not on their exact values, which is what makes the result usable when the noise model is known only qualitatively. It underlies the equilibrium-selection results of the same paper (risk dominance in $2\times 2$ coordination games, Theorem 3) and much of the later stochastic evolutionary game theory literature.

The result is proved in the paper, with the tree formula imported from Freidlin and Wentzell. As far as is known, none of it is formalized: Mathlib has irreducible and primitive nonnegative matrices but neither the Markov chain tree formula, aperiodicity, recurrent classes of a finite chain, nor minimum arborescences. A complete development would produce these as reusable components.

Difficulty

The first idea is to take the limit in $\mu^\varepsilon P^\varepsilon = \mu^\varepsilon$: compactness and (7) give that every limit point of $\mu^\varepsilon$ is stationary for $P^0$, but $P^0$ has many stationary distributions, so this neither proves convergence nor identifies the support. Both come from the tree formula, which makes $\mu^\varepsilon_z$ a ratio of sums of products whose orders of magnitude are read off from the resistances; the absence of cancellation (all terms are nonnegative) is essential. The second difficulty is Lemma 2: an optimal $x$-tree on the whole state space must be transformed, by the paper's tree surgery on junctions (pp. 80–83), into something comparable with a $j$-tree on the class graph without increasing its resistance. The easy inequality $\gamma(x_j) \le \gamma_j$ glues optimal paths and zero-resistance trees together; the reverse inequality is where the work lies.

Formalization scope

States form a Fintype X with decidable equality; chains are real matrices Matrix X X ℝ, row stochasticity is Matrix.rowStochastic, irreducibility is Mathlib's Matrix.IsIrreducible, and aperiodicity (every state has period 1) is defined in the mission. The family $P^\varepsilon$ is a function ℝ → Matrix X X ℝ constrained only on $(0, a]$; all limits are one-sided ($\varepsilon \to 0^+$), $\varepsilon^{-r}$ is the real power, and "$0 < \lim < \infty$" is a real limit $c > 0$. Distributions are row vectors and stationarity is $\mu A = \mu$. Trees are parent maps with edges pointing toward the root. Potentials, class resistances and stochastic potentials are infima in EReal, where an empty infimum is $+\infty$; under the hypotheses all of them are finite.

The goal quantifies over every regular perturbation, not a parametric family such as $(1-\varepsilon)P^0 + \varepsilon Q$, and over every family of stationary distributions of the $P^\varepsilon$ (unique by (6)). The recurrent classes are computed from $P^0$, not supplied as data, and $\gamma_j$ is computed on the class graph with weights $r_{ij}$; defining $\gamma_j$ as $\gamma(x)$ for some $x \in X_j$ would make Lemma 2 definitional and is ruled out.

Contributions welcome: the Markov chain tree formula and the uniqueness of stationary distributions for irreducible finite chains (both reusable well beyond this mission), recurrence and the support of stationary distributions, and the arborescence surgery of Lemma 2.

Selected references

• H. P. Young, The Evolution of Conventions, Econometrica 61(1), 1993, 57–84. https://doi.org/10.2307/2951778
• M. I. Freidlin and A. D. Wentzell, Random Perturbations of Dynamical Systems, Springer, 1984 (Ch. 6, Lemma 3.1). https://doi.org/10.1007/978-1-4684-0176-9
• M. Kandori, G. J. Mailath and R. Rob, Learning, Mutation, and Long Run Equilibria in Games, Econometrica 61(1), 1993, 29–56. https://doi.org/10.2307/2951777
• D. P. Foster and H. P. Young, Stochastic Evolutionary Game Dynamics, Theoretical Population Biology 38, 1990, 219–232. https://doi.org/10.1016/0040-5809(90)90011-J
• J. C. Harsanyi and R. Selten, A General Theory of Equilibrium Selection in Games, MIT Press, 1988. https://mitpress.mit.edu/9780262582384/
• Related missions on learning dynamics: StochFictPlay.* (Hofbauer and Sandholm 2002, stochastic fictitious play) and CalibratedCE.* (calibrated learning and correlated equilibrium).

Why arrival averages and time averages agree

Queueing analysis constantly moves between two kinds of long-run averages: the fraction of time a system spends in some set of states, and the fraction of arriving customers who find it there. Waiting-time formulas for the M/G/1 queue, blocking probabilities in loss systems and many decomposition arguments rest on the claim that, when arrivals form a Poisson process, the two coincide. This property is known as PASTA, Poisson Arrivals See Time Averages. It is used throughout queueing theory, inventory theory and the analysis of communication networks, usually without proof.

Before 1982 the property had been proved under strong extra structure:

• Strauch (1970) proved an instantaneous version, at a fixed time point, which does not by itself give limit theorems.
• Wolff (1970) proved a limit theorem for a stationary observed process, using particular properties of its interaction with the Poisson stream.
• Stidham (1972) proved a limit theorem for regenerative processes, under restrictions on how regeneration points relate to the arrivals.
• Wolff (1982), the source of this mission, proved the limit theorem with no stationarity, regeneration or ergodicity at all. The only link assumed between system and arrivals is that the system does not anticipate future arrivals. The proof uses Watanabe's (1964) martingale characterization of the Poisson process.
• Melamed and Whitt (1990) recast the result as one instance of a general "arrivals see time averages" (ASTA) principle for arbitrary point processes.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. On it live a process $N=\{N(t),t\ge0\}$, the state of a system, with values in an arbitrary measurable space, and a Poisson process $A=\{A(t),t\ge0\}$ at rate $\lambda>0$, counting customer arrivals in $(0,t]$. The interaction between $A$ and $N$ is unspecified: arrivals may change the state.

Fix a set $B$ of states with $\{N(t)\in B\}\in\mathcal F$ for every $t\ge0$, and define

$$U(t)=\mathbf 1\{N(t)\in B\},\qquad V(t)=t^{-1}\int_0^tU(s)\,ds,\qquad Y(t)=\int_0^tU(s)\,dA(s),\qquad Z(t)=\frac{Y(t)}{A(t)}.$$

$V(t)$ is the fraction of time in $[0,t]$ that $N$ is in $B$. $Y(t)$ is the number of arrivals up to $t$ who find $N$ in $B$, and $Z(t)$ is the fraction of arrivals who do.

The paths of $U$ are assumed left continuous with right-hand limits w.p. 1, so that an arrival is not counted as already present at its own arrival epoch. $U$ is assumed jointly measurable in $(\omega,t)\in\Omega\times[0,\infty)$. The single structural assumption is the Lack of Anticipation Assumption (LAA):

for each $t\ge0$, $\{A(t+u)-A(t),u\ge0\}$ and $\{U(s),0\le s\le t\}$ are independent.

The paper's proof of (6) uses this independence for every event of $\mathcal F_t$, the σ-field generated by $\{A(s),U(s);0\le s\le t\}$. The mission therefore states Theorems 1–2, (6), Lemma 1, (10) and Lemma 2 under lack of anticipation with respect to $\mathcal F_t$: for each $t\ge0$, $\{A(t+u)-A(t),u\ge0\}$ is independent of $\mathcal F_t$. This implies the printed LAA. The printed LAA together with independent increments does not give (6) or Lemma 1, because pairwise independence of the future from the past of $A$ and from the past of $U$ is not independence from their joint past.

Formalization targets

Goal: Theorem 1 (p. 225)

Under lack of anticipation (with respect to $\mathcal F_t$, see above), for every random variable $V(\infty)$,

$$V(t)\to V(\infty)\ \text{w.p. 1}\quad\Longleftrightarrow\quad Z(t)\to V(\infty)\ \text{w.p. 1},\qquad t\to\infty.$$

The limit may be random, and the theorem asserts nothing about whether either average converges. It asserts only that the two converge together, to the same limit.

Milestones

The proof in §2 passes through the following statements, which form the milestone list:

1. (2), (3): $E\{Y(t)\}=\lambda tE\{V(t)\}=\lambda E\{\int_0^tU(s)\,ds\}$.
2. (6): $E\{Y(t+h)-Y(t)\mid\mathcal F_t\}=\lambda E\{\int_t^{t+h}U(s)\,ds\mid\mathcal F_t\}$.
3. Lemma 1: $R(t)=Y(t)-\lambda tV(t)$ is a martingale.
4. (7): the second-moment bound $E\{R^2(t)\}\le\lambda t+2\lambda^2t^2$.
5. (10): the grid strong law $R(nh)/n\to0$ w.p. 1.
6. (11): the pathwise interpolation bound between grid points.
7. Lemma 2: $R(t)/t\to0$ w.p. 1.
8. The strong law $A(t)/t\to\lambda$ for the Poisson process.

Companion: Theorem 2 (p. 228)

For a Poisson process with bounded, integrable rate $\lambda(t)$ and $\Lambda(t)/t\to\bar\lambda\in(0,\infty)$, where $\Lambda(t)=\int_0^t\lambda(s)\,ds$, the same equivalence holds with $V(t)$ replaced by the rate-weighted average $\bar V(t)=\Lambda(t)^{-1}\int_0^tU(s)\lambda(s)\,ds$. Display (12), $E\{Y(t)\}=\int_0^tE\{U(s)\}\lambda(s)\,ds$, is its analogue of (3).

Significance

Theorem 1 justifies replacing customer averages by time averages, and conversely, in any model where arrivals are Poisson and the system does not anticipate them. Examples are queue-length distributions seen by arrivals in M/G/c systems, blocking probabilities in Erlang loss models, and state probabilities at arrival epochs in networks with Poisson external input. It needs no ergodic theory of the observed process: convergence of one average has to be established separately, by whatever means suit the model, and the theorem transfers it to the other. Lemma 2 also implies versions of PASTA under weaker modes of convergence (Remark 6).

The result has been proved for four decades and is textbook material. What this mission adds is a machine-checked proof. No formalization of Theorem 1 in a proof assistant is known. A complete development would also contain machine-checked versions of several standard facts not yet available in Mathlib:

• the strong law for the Poisson process;
• a strong law for square-integrable martingale differences;
• Stieltjes integration against a counting path.

Difficulty

The naive argument conditions on the arrival epochs and claims that each arrival "samples" the state at a uniformly random time. This fails because arrivals influence the state: after an arrival, a queue-length process is no longer independent of the arrival stream. LAA only says that the future increments of $A$ are independent of the past of $U$. The difficulty is to turn this one-sided independence into an almost-sure statement about long-run averages, along every path and at all times rather than only at fixed ones.

On the technical side, the expected-value identity (3) needs a limit of grid sums. That limit relies on left continuity: without it, $U(t)=\mathbf 1\{A \text{ jumps at } t\}$ satisfies LAA with $V\equiv0$ but $Z\equiv1$. The passage from expectations to a strong law needs a martingale structure and a second-moment bound, and the interpolation between grid times needs a pathwise argument.

Formalization scope

• Time and paths. Time is $\mathbb R$, and every hypothesis concerns $t\ge0$ only. Processes are maps $\mathbb R\to\Omega\to(\cdot)$. A Poisson process with intensity function $\lambda(\cdot)$ is a counting process $A:\mathbb R\to\Omega\to\mathbb N$ with $A(0)=0$, every path non-decreasing and right-continuous, Poisson-distributed increments with mean $\int_s^t\lambda$, and independent increments over any finite increasing sequence of times. The constant-rate case is Theorem 1's setting.
• The averages. $Y(t)$ is encoded as $\sum_{k=1}^{A(t)}U(T_k)$ over the arrival epochs $T_k=\inf\{s\ge0:A(s)\ge k\}$, which is the Lebesgue–Stieltjes integral $\int_{(0,t]}U\,dA$ with multiplicities. $Z(t)=0$ when $A(t)=0$, and $V(0)=0$; limits do not see these values.
• The standing hypotheses. These are carried as binders of the goal: measurability of $\{N(t)\in B\}$ for $t\ge0$, path regularity w.p. 1 (left continuity at $t>0$, right limits at $t\ge0$), joint measurability on $\Omega\times[0,\infty)$, and lack of anticipation as independence of the σ-field of future increments of $A$ from $\mathcal F_t$. The milestones (2), (3), (7) and (11) need less: (2) and (3) are stated under the printed LAA, and (7) and (11) under no independence assumption at all.
• The limit and the expectations. $V(\infty)$ is an arbitrary function $\Omega\to\mathbb R$, shared by both sides of the equivalence. Expectations in the milestones come with integrability conclusions, or are lower integrals in $[0,\infty]$, so that no identity holds through Lean's junk value $0$ for non-integrable functions.
• Ruled out. A formalization in which $V(\infty)$ is quantified separately on each side, which loses "to the same limit". A goal that assumes Lemma 2, (3) or the strong law $A(t)/t\to\lambda$ as a hypothesis. A definition of $Y$ that counts distinct jump times and not arrivals.

Welcome contributions:

• a reusable Poisson-process library: the strong law, square moments, independence of increments from a past σ-field;
• a martingale strong law of Feller's type;
• Stieltjes sums against counting paths.

All of these are useful well beyond this mission.

Selected references

• R. W. Wolff, Poisson Arrivals See Time Averages, Operations Research 30(2):223–231, 1982. https://doi.org/10.1287/opre.30.2.223
• S. Watanabe, On discontinuous additive functionals and Lévy measures of a Markov process, Japanese Journal of Mathematics 34:53–70, 1964. https://doi.org/10.4099/jjm1924.34.0_53
• B. Melamed and W. Whitt, On arrivals that see time averages, Operations Research 38(1):156–172, 1990. https://doi.org/10.1287/opre.38.1.156
• P. Brémaud and J. Jacod, Processus ponctuels et martingales: résultats récents sur la modélisation et le filtrage, Advances in Applied Probability 9(2):362–416, 1977. https://doi.org/10.2307/1426091
• S. Stidham, Regenerative processes in the theory of queues, with applications to the alternating-priority queue, Advances in Applied Probability 4(3):542–577, 1972.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.

Motivation

Many iterative algorithms update only part of a vector at a time. In a parallel implementation, one processor may read a value written several rounds earlier by another processor. Random observations also perturb each update. John N. Tsitsiklis's 1994 paper gives conditions under which such an asynchronous stochastic iteration still converges. The paper develops the result to analyze Q-learning, where state-action values are revised from sampled costs and successor states. Its general theorem also applies to iterative fixed-point calculations beyond that application.

The central issue is that a processor can choose which component to update after seeing the past, and its input can be stale. A convergence theorem that presumes a fixed update schedule or current data would miss both features. The paper's Assumptions 1–3 describe when delays, sampling noise, and random step sizes remain compatible with almost-sure convergence. Assumption 5 gives a weighted maximum norm contraction for the iteration map. Theorem 3 combines these conditions into the target of this mission.

Setting

Fix a positive integer $n$ and write $x(t)\in\mathbb R^n$ for the vector after round $t\ge0$. Let $F:\mathbb R^n\to\mathbb R^n$ be the map whose fixed point the iteration seeks. For component $i$, the step size $\alpha_i(t)$ lies in $[0,1]$, the noise is $w_i(t)$, and $\tau^i_j(t)\le t$ is the time from which component $j$ was read. Thus $x^i(t)$ has coordinates $x_j(\tau^i_j(t))$. With $\alpha_i(t)=0$ when component $i$ is idle, all rounds obey the single update equation

$$x_i(t+1)=x_i(t)+\alpha_i(t)\bigl(F_i(x^i(t))-x_i(t)+w_i(t)\bigr).$$

All quantities live on a probability space with law $\mathsf P$. The increasing filtration $\mathcal F(t)$ represents information available when the step sizes and delays are selected, before the round's noise is observed. Assumption 1 says every timestamp $\tau^i_j(t)$ tends to infinity almost surely: no fixed old value remains in use forever. Assumption 2 makes the initial state, chosen step sizes, delays, and noise measurable at the specified times; the noise has conditional mean zero, and its conditional second moment is bounded by a deterministic affine function of the largest squared iterate seen so far. Assumption 3 requires, for each component, divergent total step size and a square-summable step-size sequence, with a deterministic bound on all squared partial sums.

For a vector $v$ with strictly positive coordinates, the weighted maximum norm is $\|z\|_v=\max_i |z_i|/v_i$. Assumption 5 provides $x^*\in\mathbb R^n$ and $\beta\in[0,1)$ such that $\|F(x)-x^*\|_v\le\beta\|x-x^*\|_v$ for every $x$. Assumption 6, used in the boundedness milestone, requires the related growth bound $\|F(x)\|_v\le\beta\|x\|_v+D$ for some real $D$. The weighted norm permits different component scales.

Formalization targets

Boundedness under a weighted growth bound

Theorem 1 is the main intermediate target. Under Assumptions 1, 2, 3, and 6, it asserts

$$\mathsf P\!\left(\exists M\in\mathbb R\;\forall t,i,\ |x_i(t)|\le M\right)=1.$$

The bound $M$ may depend on the sample path. Lemmas 1–3 of the paper are milestones in its analysis: a scalar noisy recursion converges, its tails become uniformly small, and the pathwise bounds in the contradiction step hold.

Almost-sure convergence under a weighted contraction

The goal is Theorem 3, under Assumptions 1, 2, 3, and 5:

$$\mathsf P\!\left(\lim_{t\to\infty}x(t)=x^*\right)=1.$$

This theorem does not assume bounded iterates or Assumption 6 separately. Its proof uses Theorem 1 after deriving the needed growth bound from the contraction condition. Lemma 8 is the remaining milestone, comparing the coordinate iterates to an auxiliary deterministic recursion and a noise tail.

Significance

The result gives a fixed-point convergence guarantee when coordinates update at different times, delays can vary, and update choices can depend on past observations. In the paper's Q-learning application, these features describe exploratory sampling and possible parallel computation with old state-action values. For discounted problems, the associated Q-learning map contracts in the maximum norm, so Theorem 3 supplies the convergence step once the stochastic assumptions are checked (Tsitsiklis 1994, §7).

The mathematical results were proved in 1994; this mission asks for machine-checked proofs of their formal statements. Its reusable output would include a model of asynchronous noisy iteration, a scalar martingale-noise convergence lemma with random conditional variance bounds, and a precise interface between weighted contractions and pathwise convergence. The goal and milestone theorem files are currently statements with proof holes, while the definition file compiles without one.

Difficulty

A coordinate's next value depends on a vector assembled from observations at several earlier times. A direct estimate against the current error therefore does not close: the stale coordinates can reflect larger past errors. The noise condition is also tied to the largest iterate seen so far, so a deterministic global variance bound is unavailable before boundedness has been established. These two dependencies make the ordinary synchronous contraction argument insufficient. The scalar noise result and the pathwise comparison lemmas isolate the conditions needed for the boundedness and convergence statements.

Formalization scope

Vectors are functions Fin n → ℝ, with $n>0$; the source labels coordinates $1,\ldots,n$, while Fin n starts at zero. Function order is componentwise. The model sets $\alpha_i(t)=0$ on idle rounds and uses the paper's unified update equation. It does not store the sets of update times separately. The delay values on idle rounds are left arbitrary because they do not affect the update; the source chooses the current time there. All step sizes lie in $[0,1]$, and all delays are at most the current time, on every sample path.

The probability law is a probability measure. The filtration consists of increasing sub-σ-algebras. The iterate sequence is explicitly assumed adapted in the main theorems, matching the paper's use of $x(t)$ and its running maximum as $\mathcal F(t)$-measurable random variables. Conditional moment assumptions use integral inequalities over measurable sets, allowing generalized conditional expectations when the noise need not have a finite unconditional second moment. The conditional upper bound is required nonnegative almost surely, as the original inequality entails. Divergence and square summability use partial sums, so a non-summable series cannot receive a default value.

The maximum norm is the finite supremum of coordinate absolute values, and the weighted norm divides by the strictly positive coordinates of $v$. Almost-sure boundedness means a path-dependent finite bound on every coordinate and time. Pathwise Lemmas 3 and 8 are stated on a retained sample path, with the auxiliary quantities and hypotheses established at their locations in the paper; Lemma 8 uses the proof's translated and rescaled coordinates. These conventions rule out an empty coordinate type, junk integrals, and a vacuous boundedness claim. Contributions to the stated lemmas, their probabilistic infrastructure, and the final convergence proof are within scope.

Selected references

• John N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994), 185–202. DOI: 10.1023/A:1022689125041.

Motivation

Q-learning (Watkins, 1989) learns the optimal action values of a Markov decision problem from sampled transitions, without a model of the transition probabilities. At each step only one state–action pair is updated, with a noisy estimate of the Bellman operator evaluated at possibly outdated values of the other pairs. Watkins and Dayan (1992) gave a first convergence proof for discounted problems. Tsitsiklis (1994) and, independently, Jaakkola, Jordan and Singh (1994) placed Q-learning inside the theory of stochastic approximation: the Robbins–Monro scheme of iterating $x \leftarrow x + \alpha\,(F(x) - x + w)$ with decreasing stepsizes and zero-mean noise, here in an asynchronous form where different components are updated at different times using delayed information, as in the distributed iterations of Bertsekas and Tsitsiklis (1989).

Tsitsiklis's paper proves convergence with probability 1 under two structural hypotheses on the iteration mapping $F$: a weighted maximum-norm contraction (Theorem 3), which covers discounted Q-learning, and monotonicity (Theorem 2), which covers undiscounted (stochastic shortest path) problems, whose Bellman operator is monotone but in general not a contraction. This mission formalizes the monotone case.

Setting

A mapping $F:\mathbb R^n\to\mathbb R^n$ with components $F_1,\dots,F_n$ is given, and the goal is to solve $F(x)=x$. Time is discrete, $t=0,1,2,\dots$. The iterate $x(t)\in\mathbb R^n$ evolves by

$$x_i(t+1)=x_i(t)+\alpha_i(t)\bigl(F_i(x^i(t))-x_i(t)+w_i(t)\bigr),\qquad x^i(t)=\bigl(x_1(\tau^i_1(t)),\dots,x_n(\tau^i_n(t))\bigr),$$

where $\alpha_i(t)\in[0,1]$ is a stepsize ($\alpha_i(t)=0$ when component $i$ is not updated), $w_i(t)$ is noise, and $0\le\tau^i_j(t)\le t$ are delays: the update of component $i$ may read component $j$ as it was at an earlier time. All quantities are random variables on a probability space $(\Omega,\mathcal F,P)$ with an increasing sequence of σ-fields $\{\mathcal F(t)\}$, the history up to the choice of the stepsizes at time $t$.

Vector inequalities are componentwise and $e$ is the vector of ones. The paper's assumptions are:

• Assumption 1: every delay index $\tau^i_j(t)$ tends to infinity, with probability 1.
• Assumption 2: $x(0)$, $\alpha_i(t)$, $\tau^i_j(t)$ are $\mathcal F(t)$-measurable and $w_i(t)$ is $\mathcal F(t+1)$-measurable; $E[w_i(t)\mid\mathcal F(t)]=0$; and $E[w_i^2(t)\mid\mathcal F(t)]\le A+B\max_j\max_{\tau\le t}|x_j(\tau)|^2$ for deterministic constants $A,B$.
• Assumption 3: $\sum_t\alpha_i(t)=\infty$ and $\sum_t\alpha_i^2(t)\le C$ with probability 1, for a deterministic $C$.
• Assumption 4: $F$ is monotone ($x\le y\Rightarrow F(x)\le F(y)$), continuous, has a unique fixed point $x^*$, and $F(x)-re\le F(x-re)\le F(x+re)\le F(x)+re$ for all $x$ and all $r>0$.

In Lean the algorithm is the structure AsyncSA.Monotone.Algorithm with fields F, x, α, w, τ, and the assumptions are Assumption1–Assumption4.

Formalization targets

Goal: Theorem 2 (p. 189)

Under Assumptions 1–4, if $x(t)$ is bounded with probability 1, then

$$\lim_{t\to\infty}x(t)=x^*\qquad\text{with probability 1.}$$

Boundedness is a hypothesis, not a conclusion: for monotone $F$ it must be established separately (the paper does so for Q-learning in §7). The bound may differ between sample paths.

Milestones

1. Lemma 1 (p. 190): for a scalar recursion $W(t+1)=(1-\alpha(t))W(t)+\alpha(t)w(t)$ with martingale-difference noise whose conditional variance is bounded by an a.s. bounded $B(t)$, and stepsizes with $\sum\alpha=\infty$, $\sum\alpha^2\le C$, $W(t)\to0$ with probability 1.
2. Lemma 4 (p. 193): the sequences $U^{k+1}=(U^k+F(U^k))/2$, $U^0=x^*+re$, and $L^{k+1}=(L^k+F(L^k))/2$, $L^0=x^*-re$, satisfy $F(U^k)\le U^{k+1}\le U^k$ and $F(L^k)\ge L^{k+1}\ge L^k$.
3. Lemma 5 (p. 193): $U^k\to x^*$ and $L^k\to x^*$.
4. Lemma 6 (p. 194): on a sample path where $L^k\le x(t)\le U^k$ from time $t_k$ on and all delays exceed $t_k$ from time $t'_k$ on, $x_i(t)\le X_i(t)+W_i(t;t'_k)$, where $X_i$ relaxes from $U^k_i$ towards $F_i(U^k)$ and $W_i(t;t'_k)$ accumulates the noise from $t'_k$.
5. Lemma 7 (p. 195): under the choices of $\delta_k$ and $t''_k$ made on pp. 194–195, $x_i(t)\le U^{k+1}_i$ for all $t\ge t''_k$.

Significance

Theorem 2 is the convergence result for asynchronous stochastic approximation driven by a monotone mapping whose fixed point is unique. Its main application is Q-learning for stochastic shortest path problems with improper policies excluded, and more generally any learning scheme whose expected update is a monotone, sup-norm nonexpansive operator in the sense of (7) (dynamic programming operators are the standard examples). The same pattern, an a.s. bounded iterate plus a monotone mean map, recurs in later analyses of asynchronous and distributed learning algorithms.

The result has a published proof but, as far as the platform's catalog shows, no machine-checked one: there is no formalized asynchronous stochastic approximation theorem, and no formal Lemma 1 for random stepsizes and random conditional-variance bounds. A complete development provides the scalar almost-sure convergence lemma, the deterministic envelope argument for monotone maps, and the pathwise comparison steps, each of which is reusable.

Difficulty

The noise has a conditional variance that grows with the iterate, so it is neither bounded nor integrable a priori, and the stepsizes are random and chosen adaptively. The classical deterministic-bound argument for Lemma 1 does not apply directly. The iteration is not a contraction in any norm, so there is no Lyapunov function giving a geometric decrease, and the delays mean that the mapping is evaluated at a vector no single time index describes. Convergence has to be propagated from the deterministic envelopes $U^k,L^k$ to the random iterate through a sequence of random times, one envelope at a time, and each step requires the noise accumulated after a random time to be small uniformly in the remaining horizon.

Formalization scope

• Components are Fin n (0-based); vectors are Fin n → ℝ with the componentwise order, so Monotone F is Assumption 4(a) exactly. $re$ is r • 1.
• The update is stated in the paper's unified form for every $t$, with $\alpha_i(t)=0$ off the update times; the update sets $T^i$ are not represented. The paper sets $\tau^i_j(t)=t$ off $T^i$; the formalization leaves $\tau^i_j(t)$ free there, which is more general. $\alpha_i(t)\in[0,1]$ and $\tau^i_j(t)\le t$ hold on every sample path.
• Conditional expectations are generalized, written with set integrals (CondMeanZero, CondSqLe): $\int_S w\,dP=0$ for every $\mathcal F(t)$-set $S$ on which $w$ is integrable, and $\int_S w^2\,dP\le\int_S g^+\,dP$ in $[0,\infty]$. Mathlib's condExp is not used: it is $0$ for non-integrable functions and would make the noise assumptions vacuous.
• Series conditions use partial sums (divergence to $+\infty$; every partial sum at most $C$), never tsum, which is $0$ for non-summable sequences. The constants $A,B,C$ are chosen before the almost-sure quantifier; the bound on $x(t)$ is chosen after it.
• The paper treats $x(t)$ as determined by $\mathcal F(t)$ and uses this implicitly; Theorem 2 assumes it explicitly (Adapted).
• Lemma 1 leaves $W(0)$ unconstrained, as on the page. Lemmas 4 and 5 hold for every $r>0$. Lemmas 6 and 7 are pathwise: they fix one sample path and take the induction's objects ($k$, $t_k$, $t'_k$, $t''_k$, $X$, $\delta_k$) as given with exactly the properties the paper has established for them; they are not existential statements about these times.
• A trivializing formalization (junk conditional expectations, tsum for the series, a deterministic bound on $x(t)$, or a second unrelated $x^*$) is ruled out by the choices above.

Contributions welcome: a general almost-sure convergence theorem for Robbins–Monro recursions with generalized conditional moments (Lemma 1 and its tail version $W(t;t_0)$), and lemmas on monotone maps satisfying (7).

Selected references

• J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994) 185–202. https://doi.org/10.1023/A:1022689125041
• C. J. C. H. Watkins and P. Dayan, Q-learning, Machine Learning 8 (1992) 279–292. https://doi.org/10.1007/BF00992698
• T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994) 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
• D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. https://hdl.handle.net/1721.1/3719
• B. T. Poljak and Ya. Z. Tsypkin, Pseudogradient adaptation and training algorithms, Automation and Remote Control 34 (1973) 377–397.
• H. Robbins and S. Monro, A Stochastic Approximation Method, Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586

Motivation

Q-learning is the basic model-free algorithm of reinforcement learning: an agent that does not know the transition probabilities or the reward structure of a controlled Markov process learns the optimal action values from experience alone, by a one-line update applied after every observed transition. It was introduced in C. J. C. H. Watkins' 1989 thesis, and the convergence theorem posed here is the one proved in C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292 (doi:10.1023/A:1022676722315). Every later analysis of tabular temporal-difference control, and much of deep reinforcement learning's vocabulary, starts from this algorithm.

Timeline.

• 1989: Watkins' thesis introduces Q-learning and sketches a convergence argument.
• 1992: Watkins and Dayan publish the proof via the action-replay process, for bounded rewards, discount $0<\gamma<1$ and learning rates satisfying condition (3) at every state–action pair.
• 1994: Jaakkola, Jordan and Singh (Neural Computation 6) and Tsitsiklis (Machine Learning 16) give proofs through stochastic approximation for asynchronous iterations, with predictable random choices of state, action and step.
• Later work (Szepesvári 1997; Even-Dar and Mansour 2003) quantifies the convergence rate.

Setting

A finite controlled Markov process has a finite state set $X$, a finite nonempty action set $\mathfrak A$ (the same in every state), mean rewards $\mathcal R_x(a)$ and transition probabilities $P_{xy}[a]$. Rewards received $s$ steps later are discounted by $\gamma^s$ with $0<\gamma<1$. The optimal action-value function $Q^*$ is the unique solution of the Bellman optimality equation

$$Q^*(x,a)=\mathcal R_x(a)+\gamma\sum_y P_{xy}[a]\max_b Q^*(y,b).$$

In the $n$-th episode the agent observes a state $x_n$, performs an action $a_n$, observes the next state $y_n$ and a reward $r_n$ of mean $\mathcal R_{x_n}(a_n)$, and updates its table with a learning rate $\alpha_n$:

$$Q_n(x,a)=\begin{cases}(1-\alpha_n)Q_{n-1}(x,a)+\alpha_n\bigl[r_n+\gamma\max_b Q_{n-1}(y_n,b)\bigr]&(x,a)=(x_n,a_n),\\ Q_{n-1}(x,a)&\text{otherwise,}\end{cases}$$

from given initial values $Q_0$. Episodes need not form a single trajectory. Writing $n^i(x,a)$ for the episode of the $i$-th visit to $(x,a)$, the learning-rate condition is

$$\sum_{i=1}^\infty\alpha_{n^i(x,a)}=\infty,\qquad\sum_{i=1}^\infty\bigl[\alpha_{n^i(x,a)}\bigr]^2<\infty\qquad\forall x,a.\tag{3}$$

The proof uses the action-replay process (ARP): from the recorded episodes one builds a finite-horizon process with states $\langle x,n\rangle$ (a real state and a level $n$), in which taking $a$ at $\langle x,n\rangle$ replays a randomly chosen earlier episode that tried $a$ in $x$, emitting its reward and dropping to the level below that episode. Its expected one-step reward is $\mathcal R^{(n)}_x(a)$ and its aggregated transition probabilities are $P^{(n)}_{xy}[a]$.

Formalization targets

Goal: the Theorem (p. 282)

Given bounded rewards $|r_n|\le\mathcal R$, learning rates $0\le\alpha_n<1$ and (3),

$$Q_n(x,a)\to Q^*(x,a)\quad\text{as }n\to\infty,\ \forall x,a,\ \text{with probability }1.$$

Milestones (the paper's appendix, in attack order)

• Lemma A (p. 288): $Q_n(x,a)=Q^*_{\mathrm{ARP}}(\langle x,n\rangle,a)$ for all $a,x$ and $n\ge0$.
• Lemma B.1 (p. 289): the values of $s$ actions with and without a continuation policy differ by at most $\gamma^s\mathcal R/(1-\gamma)$.
• Lemma B.2 (p. 289): started high enough, the ARP strays below any level $l$ within $s$ actions with arbitrarily small probability.
• The stochastic-convergence theorem quoted in the proof of B.3 (p. 290): $X_{n+1}=X_n+\beta_n(\xi_n-X_n)$ with $\sum\beta_n=\infty$, $\sum\beta_n^2<\infty$ and bounded $\xi_n$ of mean $\Xi$ converges to $\Xi$ almost surely.
• Lemma B.3 (p. 290): almost surely $P^{(n)}_{xy}[a]\to P_{xy}[a]$ and $\mathcal R^{(n)}_x(a)\to\mathcal R_x(a)$.
• Lemma B.4 (p. 291): rewards within $\eta$ and transition rows within $\eta/\mathcal R$ give values of $s$ actions within $\eta s(s+1)/2$.

A further item states that the optimality equation has exactly one solution for $0\le\gamma<1$.

Significance

The result. The theorem is the first guarantee that an agent can find optimal behaviour in an unknown finite Markov decision process from samples, with a per-step cost independent of the model. It is the template for convergence results on SARSA, TD($\lambda$), double Q-learning and asynchronous value iteration, and it is the reference point against which finite-sample rates and function-approximation counterexamples are measured.

Formalizing it. The theorem has been proved since 1992–1994; this mission asks for a machine-checked proof. Two parts are reusable beyond Q-learning: the almost-sure convergence of scalar stochastic averaging with adapted steps (a Robbins–Siegmund type statement), and the perturbation bounds for finite-horizon values of Markov chains (B.1, B.4). The paper's own assembly in §3.2 bounds the error for each fixed action sequence and then passes to optimal behaviour; that passage is not justified on the page, so a complete development may route the final step differently. The milestones are the paper's lemmas as stated, with the corrections listed below.

Difficulty

The update touches one table entry at a time, at random times chosen by the agent, and its target $r_n+\gamma\max_b Q_{n-1}(y_n,b)$ depends on the current estimates, so the iteration is neither a plain average nor a contraction applied synchronously. Treating each entry as a separate Robbins–Monro average fails because the targets move with the other entries. The paper's device is to recognize $Q_n$ as exact optimal values of the ARP (Lemma A), which turns the analysis into showing that the ARP, viewed from a high level, behaves like the real process for many steps; the probabilistic content is then concentrated in Lemma B.3, and the deterministic content in B.1, B.2 and B.4.

Formalization scope

Everything lives in the namespace QLearning.Convergence, with one definitions module QLearning.Convergence.Setting. Conventions:

• $X$ and $\mathfrak A$ are Fintypes with decidable equality, $\mathfrak A$ is nonempty, and $\max_b$ is Finset.sup'. The process is a structure with R x a $=\mathcal R_x(a)$ and P x a y $=P_{xy}[a]$, rows nonnegative and summing to $1$.
• $Q^*$ enters the goal through the predicate IsOptimalQ M γ Q (the optimality equation), which has exactly one solution (separate item); it is not defined by a limit or a choice.
• Lean index $n$ is the paper's episode $n\ge1$; index $0$ of the episode data is unused and qIter … 0 $=Q_0$.
• Condition (3) is written over episodes: the learning rate charged to $(x,a)$ at episode $n$ is $\alpha_n$ if $(x_n,a_n)=(x,a)$ and $0$ otherwise; its partial sums tend to $+\infty$ and its squares are summable. This equals (3) and forces infinitely many visits.
• Probability model (pinned). The paper describes it in words only. On a filtered probability space, $x_n,a_n,\alpha_n$ are $\mathcal F_{n-1}$-measurable, $y_n,r_n$ are $\mathcal F_n$-measurable, $\Pr[y_n=y\mid\mathcal F_{n-1}]=P_{x_ny}[a_n]$, $\mathbb E[r_n\mid\mathcal F_{n-1}]=\mathcal R_{x_n}(a_n)$, $|r_n|\le\mathcal R$, $0\le\alpha_n<1$, and (3) holds almost surely. Fixed episode schedules with independent outcomes are a special case.
• The ARP deck at level $n$ includes card $n$ (as in the card game and Lemma A's proof); $P^{(n)}$ keeps the printed range of levels $1,\dots,n-1$; ARP optimality is over deterministic Markov policies of the ARP. Finite action sequences are lists of actions with $0$ terminal reward.
• Corrections disclosed in the items. B.1 is stated with $\le$ (the page's strict inequalities fail for a constant reward). B.4 assumes closeness of transition rows in $\ell^1$ and $s\ge1$: with the page's entrywise closeness the printed constant is false once $|X|\ge4$. The stochastic-convergence theorem is read with conditional mean $\Xi$ and adapted steps.

Trivializing formalizations are ruled out: the optimality predicate is satisfiable, conditional expectations are taken only of bounded measurable variables, the goal is the almost-sure statement under the probability model above rather than a pathwise or fixed-schedule one, and the ARP's optimal value is a supremum over policies, not the Q-learning recursion.

The development needs finite Markov chain values and contraction arguments (available in Mathlib in pieces), conditional expectations and almost-sure convergence for adapted sequences (Mathlib's martingale library), and the ARP construction above. Proofs of any milestone, alternative routes to the goal, and reusable lemmas on stochastic averaging are welcome. §4's extensions (absorbing undiscounted processes, multiple updates per episode) and equation (4) are not posed.

Selected references

• C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292. https://doi.org/10.1023/A:1022676722315
• C. J. C. H. Watkins, Learning from Delayed Rewards, PhD thesis, University of Cambridge, 1989.
• T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994), 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
• J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994), 185–202. https://doi.org/10.1007/BF00993306
• H. J. Kushner and D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8