Reinforcement Learning

Motivation

Policy iteration alternates two steps: evaluate the current policy, then replace it by a policy that is greedy with respect to the evaluated action values. The policy improvement theorem guarantees that each greedy step does not make the policy worse, and that the process stops only at an optimal policy. When the action values are estimated from experience rather than computed from a model, as in Monte Carlo control, a greedy policy is a problem: it never tries the actions it does not currently prefer, so their values are never re-estimated. Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., 2018), §5.4, resolve this without the unrealistic assumption of exploring starts by moving the policy only toward a greedy one, to an ε-greedy policy that keeps every action's probability at least ε/|A|.

The question this mission formalizes is whether policy iteration still works under that restriction. The book's answer (pp. 101–102) is yes, in a precise sense: an ε-greedy step never makes an ε-soft policy worse, and it fails to make it strictly better only when the policy is already the best among all ε-soft policies. This is the dynamic-programming fact that justifies on-policy first-visit Monte Carlo control for ε-soft policies, and more broadly every ε-greedy on-policy control scheme that is analysed with exact action values.

Setting

A finite Markov decision process has a finite state set S, a finite nonempty action set A used in every state, a finite reward set R ⊂ ℝ and dynamics p(s′, r | s, a) ≥ 0 with $\sum_{s', r} p(s', r \mid s, a) = 1$. A policy π gives, for each state s, a probability distribution π(· | s) on A. With a discount rate $0 \le \gamma < 1$, the state value $v_\pi(s)$ is the expected discounted return $\mathbb E_\pi[\sum_{k \ge 0} \gamma^k R_{t+k+1} \mid S_t = s]$, and the action value is

$$q_\pi(s, a) = \sum_{s', r} p(s', r \mid s, a)\,[r + \gamma v_\pi(s')].$$

For ε > 0, a policy is ε-soft if $\pi(a \mid s) \ge \varepsilon/|A|$ for all s and a. A policy π′ is ε-greedy with respect to $q_\pi$ if at each state some maximizer $A^*(s)$ of $q_\pi(s, \cdot)$ receives probability $1 - \varepsilon + \varepsilon/|A|$ and every other action receives $\varepsilon/|A|$; ties among maximizers are broken arbitrarily. A policy π is optimal among the ε-soft policies if it is ε-soft and $v_{\pi''}(s) \le v_\pi(s)$ for every ε-soft π″ and every state s.

The book's analysis uses a new environment with the same states, actions and rewards, in which with probability 1 − ε the chosen action is executed and with probability ε a uniformly random action replaces it:

$$\tilde p(s', r \mid s, a) = (1 - \varepsilon)\, p(s', r \mid s, a) + \sum_{a'} \frac{\varepsilon}{|A|}\, p(s', r \mid s, a').$$

Its optimal value function is written $\tilde v_*$.

Formalization targets

Goal: ε-greedy improvement with the equality case

For $0 \le \gamma < 1$, $0 < \varepsilon \le 1$, an ε-soft policy π and any ε-greedy policy π′ with respect to $q_\pi$,

$$v_{\pi'}(s) \ge v_\pi(s) \quad \text{for all } s, \qquad \text{and} \qquad v_{\pi'} = v_\pi \;\Longrightarrow\; \pi, \pi' \text{ are optimal among the ε-soft policies}.$$

The goal is stated in terms of the original MDP and ε-soft policies only; the new environment appears only in the milestones.

Milestones

1. Policy improvement theorem for stochastic policies (4.7)–(4.8), p. 78: $\sum_a \pi'(a \mid s) q_\pi(s, a) \ge v_\pi(s)$ for all s implies $v_{\pi'} \ge v_\pi$, strictly at every state where the hypothesis is strict.
2. Eq. (5.2), pp. 101–102: $\sum_a \pi'(a \mid s) q_\pi(s, a) = \frac{\varepsilon}{|A|}\sum_a q_\pi(s, a) + (1-\varepsilon)\max_a q_\pi(s, a) \ge v_\pi(s)$.
3. Characterization, p. 102: an ε-soft π is optimal among ε-soft policies if and only if $v_\pi = \tilde v_*$.
4. Uniqueness, p. 102: $\tilde v_*$ is the unique solution of the Bellman optimality equation with the altered transition probabilities $\tilde p$, and that equation splits as $(1-\varepsilon)\max_a(\cdot) + \frac{\varepsilon}{|A|}\sum_a(\cdot)$.
5. Fixed-point equation, p. 102: if $v_{\pi'} = v_\pi$, then $v_\pi(s) = (1-\varepsilon)\max_a q_\pi(s, a) + \frac{\varepsilon}{|A|}\sum_a q_\pi(s, a)$.

Significance

The result is what makes ε-greedy on-policy control a form of generalized policy iteration: monotone improvement at every step, and a characterization of where the process can stop. It also locates precisely what is lost by exploring, namely that the fixed point is optimal among ε-soft policies, not among all policies. The value $\tilde v_*$ of the new environment is the benchmark against which ε-greedy methods converge when action values are exact.

The book presents the argument informally and states the stochastic policy improvement theorem without proof ("we will not go through the details", p. 79). A formalization supplies the missing proof of the stochastic case, the identification of the best ε-soft policy value with the optimal value of a modified MDP, and the uniqueness of that value. As far as a search of the platform shows, no statement about ε-soft or ε-greedy policies has been formalized there; existing finite-MDP results (Bellman optimality in the Foundations of Machine Learning and Bertsekas series) use different reward models and do not cover the modified environment.

Difficulty

The improvement half follows from (5.2) and the policy improvement theorem, but both need work in the return-based model: the theorem requires comparing infinite discounted sums under two different Markov chains, and (5.2) uses the identity $v_\pi(s) = \sum_a \pi(a \mid s) q_\pi(s, a)$, which is a theorem about returns, not a definition. The equality half is where the obvious argument fails. The deterministic-policy argument of Chapter 4 shows that an unimproved greedy policy satisfies the ordinary Bellman optimality equation; here the unimproved policy satisfies a different equation, and nothing in the original MDP identifies its solution with the best ε-soft value. That identification needs two further facts: every policy of the new environment corresponds to an ε-soft policy of the original one with the same values, and conversely (at ε = 1 only the uniform policy is ε-soft); and the altered optimality equation has exactly one solution.

Formalization scope

Everything is stated in the namespace SuttonBartoRL.EpsSoft on a finite MDP with four-argument dynamics, one finite nonempty action set for all states (so $|A(s)| = |A|$, the book's footnote 3, p. 48), and a finite reward set. The conventions are:

• $v_\pi$ is defined from expected discounted returns as $\sum_k \gamma^k (P_\pi^k r_\pi)(s)$ with $0 \le \gamma < 1$; Bellman equations are theorems, never definitions. $q_\pi$ is the one-step lookahead (4.6) on this $v_\pi$.
• $\tilde v_*$ is the supremum of the new environment's policy values over all stochastic policies, a bounded family for $\gamma < 1$.
• ε ranges over (0, 1]: the book requires ε > 0, and for ε > 1 no ε-soft policy exists. The equality in (5.2) is stated without the book's intermediate division by 1 − ε, so the case ε = 1 is included.
• "Any ε-greedy policy" is encoded by quantifying over every choice of maximizer at every state.
• "Optimal among ε-soft policies" means ε-soft and pointwise at least as good as every ε-soft policy.

Defining $v_\pi$ as the solution of the Bellman expectation equation, or $\tilde v_*$ as the solution of the altered optimality equation, would make milestones 3–5 and the goal's equality half hold by definition; the formalization does neither. The goal is not the statement "$v_{\pi'} \ge v_\pi$" alone: the equality case is part of the book's claim and part of the goal.

The finite-MDP definitions duplicate those of other missions in this series and are expected to be merged later. Useful contributions include the Neumann-series identity $v_\pi = (I - \gamma P_\pi)^{-1} r_\pi$, the Bellman expectation equation, the contraction property of Bellman operators, and the correspondence between policies of the new environment and ε-soft policies of the original one; these are reusable for the other finite-MDP missions of the series.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §4.2 (pp. 76–79) and §5.4 (pp. 100–103). http://incompleteideas.net/book/the-book-2nd.html
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960 (policy iteration).
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, doi:10.1002/9780470316887.

Motivation

Policy gradient methods learn a parameterized policy $\pi(a \mid s, \theta)$ directly, by stochastic gradient ascent on a scalar performance measure $J(\theta)$, instead of deriving the policy from learned action values. They are how reinforcement learning handles continuous action spaces, stochastic optimal policies and prior knowledge built into the policy's form, and they underlie REINFORCE (Williams, 1992) and the actor–critic family. Every such method needs an estimate of $\nabla J(\theta)$. The difficulty is that $J$ depends on $\theta$ in two ways: through the action choices in each state, and through the distribution of states those choices produce. The second effect depends on the unknown environment dynamics.

The policy gradient theorem (Sutton, McAllester, Singh and Mansour, 2000; Marbach and Tsitsiklis, 2001) gives $\nabla J(\theta)$ as an expectation over the on-policy state distribution that involves no derivative of that distribution. Chapter 13 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) states it as Eq. (13.5), proves it in a box for the episodic case (p. 325) and in a second box for the continuing case (pp. 334–335), and builds REINFORCE, REINFORCE with baseline and actor–critic methods on it. This mission formalizes that chapter's theorem and the identities around it, in the book's own model.

Setting

A finite episodic MDP has a finite set $\mathcal S$ of nonterminal states, a terminal state, a finite action set $\mathcal A$, a finite reward set $\mathcal R \subset \mathbb R$ and dynamics $p(s', r \mid s, a)$: for each nonterminal $s$ and action $a$, a probability distribution over next state $s' \in \mathcal S^+ = \mathcal S \cup \{\text{terminal}\}$ and reward $r$. The terminal state is absorbing and pays nothing. Write $p(s' \mid s, a) = \sum_r p(s', r \mid s, a)$ and $r(s, a)$ for the expected reward.

A differentiable policy parameterization assigns to every $\theta \in \mathbb R^{d'}$ and state $s$ a distribution $\pi(\cdot \mid s, \theta)$ over actions, with $\theta \mapsto \pi(a \mid s, \theta)$ differentiable. Under $\pi_\theta$ the nonterminal states form a substochastic chain with matrix $P_\theta(s, s') = \sum_a \pi(a \mid s, \theta) p(s' \mid s, a)$; $\Pr(s \to x, k, \pi) = P_\theta^k(s, x)$. Episodes terminate when $\sum_{k} P_\theta^k(s, s') < \infty$ for all $s, s'$.

There is no discounting ($\gamma = 1$, p. 324). The state value $v_{\pi}(s) = \sum_{k \ge 0} (P_\theta^k r_\theta)(s)$ is the expected total reward from $s$, with $r_\theta(s) = \sum_a \pi(a\mid s,\theta) r(s,a)$; the action value $q_\pi(s,a)$ is the expected total reward after taking $a$ in $s$. The episode starts in a fixed state $s_0$, and the performance is $J(\theta) = v_{\pi_\theta}(s_0)$ (13.4). The expected number of visits to $s$ in an episode is $\eta(s) = \sum_{k \ge 0} \Pr(s_0 \to s, k, \pi)$, and the on-policy distribution is $\mu(s) = \eta(s) / \sum_{s'} \eta(s')$ (9.3).

In the continuing case there is no terminal state, $J(\theta) = r(\pi)$ is the average reward per step (13.15), $\mu$ is the steady-state distribution, and $v_\pi$, $q_\pi$ are differential values, defined from the return $\sum_k (R_{t+k+1} - r(\pi))$ (13.17).

Formalization targets

Goal: the policy gradient theorem, episodic case (13.5)

If episodes terminate under $\pi_{\theta_0}$, then $J$ is differentiable at $\theta_0$ and

$$\nabla J(\theta_0) = \sum_s \eta(s) \sum_a q_\pi(s,a)\, \nabla \pi(a \mid s, \theta_0) = \Big(\sum_{s'} \eta(s')\Big) \sum_s \mu(s) \sum_a q_\pi(s,a)\, \nabla \pi(a \mid s, \theta_0),$$

with $\sum_{s'} \eta(s') \ge 1$. The book writes $\nabla J(\theta) \propto \sum_s \mu(s) \sum_a q_\pi(s,a) \nabla \pi(a \mid s,\theta)$ and names the constant, the average length of an episode, in words (p. 326). The goal states it.

Milestones

1. Exercises 3.18–3.19 with $\gamma = 1$: $v_\pi(s) = \sum_a \pi(a\mid s) q_\pi(s,a)$ and $q_\pi(s,a) = \sum_{s',r} p(s',r\mid s,a)(r + v_\pi(s'))$.
2. The recursion $\nabla v_\pi(s) = \sum_a [\nabla\pi(a\mid s) q_\pi(s,a) + \pi(a\mid s) \sum_{s'} p(s'\mid s,a) \nabla v_\pi(s')]$, including the differentiability of $v_\pi$.
3. The unrolled gradient $\nabla v_\pi(s) = \sum_{x} \sum_{k=0}^\infty \Pr(s \to x, k, \pi) \sum_a \nabla\pi(a\mid x) q_\pi(x,a)$ for every $s$.
4. The theorem with a baseline (13.10): $\sum_a b(s) \nabla \pi(a\mid s,\theta) = 0$, hence $q_\pi$ may be replaced by $q_\pi - b$.
5. The log form behind REINFORCE: where $\pi(\cdot\mid s,\theta) > 0$, $\sum_a q_\pi(s,a) \nabla\pi(a\mid s,\theta) = \sum_a \pi(a\mid s,\theta) q_\pi(s,a) \nabla \ln \pi(a\mid s,\theta)$, and hence $\nabla J(\theta) = (\sum_{s'}\eta(s')) \sum_s \mu(s) \sum_a \pi(a\mid s,\theta) q_\pi(s,a) \nabla \ln \pi(a\mid s,\theta)$, the exact form of $\nabla J \propto \mathbb E_\pi[q_\pi(S_t,A_t) \nabla\pi(A_t\mid S_t,\theta)/\pi(A_t\mid S_t,\theta)]$.
6. Exercise 13.3, (13.9): for the linear soft-max, $\nabla \ln \pi(a\mid s,\theta) = x(s,a) - \sum_b \pi(b\mid s,\theta) x(s,b)$.
7. Exercise 13.4: the eligibility vectors of the Gaussian policy (13.19)–(13.20).
8. The continuing case: under ergodicity, $\nabla r(\pi_\theta) = \sum_s \mu(s) \sum_a \nabla\pi(a\mid s,\theta) q_\pi(s,a)$ with differential $q_\pi$.

Significance

The theorem turns $\nabla J$ into a quantity that can be sampled by following the policy: weighting states by $\mu$ is what visiting them under $\pi$ does, and the log form makes the action sum an expectation over $A_t \sim \pi$. REINFORCE (13.8), REINFORCE with baseline (13.11) and one-step and eligibility-trace actor–critic methods all rest on it, and so does their claim that the expected update is in the direction of the performance gradient (p. 329). The baseline identity is why a learned state value can reduce variance without introducing bias.

The results are proved, in the book and in the literature. What this mission adds is a machine-checked version in the book's model: random episode lengths with $\gamma = 1$, vector parameters $\theta \in \mathbb R^{d'}$, four-argument dynamics, and values defined from expected returns. The platform already has a proved finite-horizon policy gradient theorem (policy_gradient_finite_horizon, with a baseline and log-form companion) for a fixed horizon $T$, a scalar parameter $\theta \in \mathbb R$ and an expected-reward kernel; it does not cover the book's statement. The mission also makes explicit two points the text leaves informal: that episodes terminate, and what exact constant hides behind "$\propto$".

Difficulty

The book's proof is a formal manipulation: differentiate the Bellman equation, substitute it into itself, and "unroll" infinitely often. Two steps are not justified on the page. First, it presupposes that $\nabla v_\pi(s)$ exists; with $\gamma = 1$ the value is an infinite series whose convergence depends on $\theta$ through termination, so differentiability of $v_\pi$ at $\theta_0$ has to be established, and termination is assumed only at $\theta_0$. Second, "repeated unrolling" is a limit: after $n$ unrollings a remainder $\sum_x P_\theta^{n}(s,x) \nabla v_\pi(x)$ is left over, and it vanishes only because $P_\theta^n \to 0$. Differentiating the series for $v_\pi$ term by term is not an alternative shortcut without a uniform bound on the derivatives of $P_\theta^k$.

In the continuing case the corresponding obstacle is the differentiability of the steady-state distribution and of the differential values, which the book's proof uses without comment; here they are part of what is to be proved, from ergodicity at $\theta_0$ alone.

Formalization scope

• Model. $\mathcal S^+$ is Option S, with none the single terminal state (several terminal states can be merged, all having value 0). One action type for all states. $\theta$ lives in EuclideanSpace ℝ (Fin d), and $\nabla$ is Mathlib's gradient; conclusions are HasGradientAt, so differentiability is asserted, not assumed.
• Values from returns. $v_\pi$, $q_\pi$, $\eta$ are series in powers of $P_\theta$; Bellman equations are theorems (milestone 1). The continuing-case average reward and steady-state distribution are the limits of (13.15), and the differential values are the series of (13.17).
• Implicit hypotheses made explicit. Termination under $\pi_{\theta_0}$ is a hypothesis of every episodic result that involves values; the continuing case assumes the book's ergodicity (the limit of $\Pr\{S_t = s'\}$ exists and does not depend on $S_0$) at $\theta_0$. The positivity of $\pi(a \mid s,\theta_0)$ is assumed where a logarithm is differentiated.
• "∝". The episodic goal states the exact equality with the constant $\sum_{s'} \eta(s')$ and proves it is at least 1. A formalization of the form "$\exists c,\ \nabla J = c \cdot \ldots$" is ruled out: it holds with $c = 0$ and loses the book's constant.
• Fixed start state. $s_0$ is a fixed state, as in the book (p. 324); no start distribution.
• Not included. Convergence of REINFORCE or actor–critic under stochastic-approximation conditions (p. 329) rests on unstated conditions and is not an item. The baseline is a deterministic function of the state, not the random variable the book also allows.

Reusable infrastructure: the episodic value layer (substochastic chains, expected visits, termination) is needed by any undiscounted episodic RL result; the soft-max and Gaussian eligibility computations are needed by every policy-gradient algorithm. Proofs of any milestone, and general lemmas on the differentiability of values and stationary distributions of parameterized finite Markov chains, are welcome.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 13. http://incompleteideas.net/book/the-book-2nd.html
• R. S. Sutton, D. McAllester, S. Singh and Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, NeurIPS 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/464d828b85b0bed98e80ade0a5c43b0f-Abstract.html
• P. Marbach and J. N. Tsitsiklis, Simulation-Based Optimization of Markov Reward Processes, IEEE Transactions on Automatic Control 46(2), 2001. https://doi.org/10.1109/9.905687
• R. J. Williams, Simple Statistical Gradient-Following Algorithms for Connectionist Reinforcement Learning, Machine Learning 8, 1992. https://doi.org/10.1007/BF00992696

Motivation

An agent learning to control an unknown environment must balance rewards it can collect now against information that improves later decisions. In a finite Markov decision process (MDP), every action changes the distribution of the next state, so a mistaken transition estimate can affect decisions many steps later. Regret measures this loss against a policy that already knows the transition probabilities. The paper of Azar, Osband and Munos gives high-probability regret bounds for two variants of upper confidence bound value iteration (UCBVI) in finite-horizon reinforcement learning. This mission targets its Chernoff–Hoeffding variant, UCBVI-CH, whose bonus depends only on the horizon and the visit count. Theorem 1 improves the paper's cited earlier dependence on the number of states from $S$ to $\sqrt S$ in the leading term for sufficiently many interactions. Azar, Osband and Munos, 2017, pp. 2, 4–5.

The paper was released in 2017 alongside work on the attainable dependence of episodic regret on the horizon $H$, state count $S$, action count $A$, and total interaction time $T$. Its second algorithm, UCBVI-BF, uses a variance-dependent bonus and is the subject of the next mission in this series. UCBVI-CH has a simpler bonus and its own explicit bound, making it a distinct mathematical target. Azar, Osband and Munos, 2017, pp. 1–5.

Setting

The state set $\mathcal S$ and action set $\mathcal A$ are finite and nonempty, with cardinalities $S$ and $A$. A stationary transition kernel $P(y\mid x,a)$ gives the probability of moving to state $y$ after action $a$ in state $x$; each row is nonnegative and sums to one. The known, deterministic reward $R(x,a)$ lies in $[0,1]$. An episode lasts $H\ge1$ steps. The environment chooses its starting state $x_{k,1}$ before episode $k$ and may base that choice on earlier episodes. It cannot see the current episode's future random draws. Azar, Osband and Munos, 2017, §2 and Assumption 1, pp. 2–3.

A policy $\pi$ selects an action from the current state and the step number. Its value $V_h^\pi(x)$ is the expected sum of rewards from step $h$ through step $H$ when starting in state $x$. The terminal value is $V_{H+1}^\pi=0$, and $V_h^*(x)$ is the maximum of $V_h^\pi(x)$ over all such policies. Since the state, action and step sets are finite, this maximum is over a finite nonempty policy class. The paper's sentence describing $H-h$ rewards uses a shifted terminal convention; this series follows the $H$ reward steps of Algorithms 1–2. Azar, Osband and Munos, 2017, pp. 3–4.

At the start of episode $k$, UCBVI-CH forms visit counts $N_k(x,a,y)$ and $N_k(x,a)$ from earlier completed transitions. On a visited pair it uses the empirical row $\widehat P_k(y\mid x,a)=N_k(x,a,y)/N_k(x,a)$. Algorithm 2 computes values backward from zero at the terminal step. For a visited pair, $Q_{k,h}(x,a)$ is the minimum of the preceding episode's $Q_{k-1,h}(x,a)$, $H$, and the empirical Bellman value plus Algorithm 3's bonus. For an unvisited pair, $Q_{k,h}(x,a)=H$. A maximizing action is chosen at every state, including states outside the realized path. Azar, Osband and Munos, 2017, Algorithms 1–3, pp. 3–4.

Formalization targets

Theorem 1: UCBVI-CH regret

For $K$ episodes and $T=KH$, regret sums the gap $V_1^*(x_{k,1})-V_1^{\pi_k}(x_{k,1})$. The goal is the paper's printed bound, with its constants:

$$\Pr\!\left\{\operatorname{Regret}(K)>20H^{3/2}L\sqrt{SAK}+250H^2S^2AL^2\right\}\le\delta, \qquad L=\ln(5HSAT/\delta),\quad \delta>0.$$

Algorithm 3 itself uses $L_{\rm alg}=\ln(5SAT/\delta)$ in its bonus $7HL_{\rm alg}/\sqrt{N_k(x,a)}$. Both logarithms remain as printed. The probability is over the MDP's next-state draws, for every admissible starting-state rule and every way of breaking ties between maximizing actions. Azar, Osband and Munos, 2017, Algorithm 3, p. 4; Theorem 1, p. 5.

Supporting results

Four milestones retain the source's indexed attack path: the Bernstein bound (9) for the empirical value error, the count-deviation display before (11), Lemma 18 on optimism, and the weighted recursion displayed in the proof of Lemma 3. The last milestone preserves the signed weights that appear before the paper's final simplification. Azar, Osband and Munos, 2017, pp. 17, 20–21, 28.

Significance

Theorem 1 gives a finite-sample failure probability with explicit dependence on $H,S,A,K$ and $\delta$. It covers a learner whose initial state can change between episodes, a feature that matters in episodic learning where the experimenter does not fix a single starting distribution. For the regime stated after Theorem 1, the leading rate is $\widetilde O(H\sqrt{SAT})$. This is a result claimed by the paper; the present Lean declarations are open proof targets, not machine-checked proofs of that claim. Azar, Osband and Munos, 2017, p. 5.

Formalizing the result creates reusable finite objects for adaptive interaction: a constructed probability law on complete paths, empirical transition counts pooled across steps, a policy value defined by its expected reward, and confidence events with their domains stated explicitly. The concentration and optimism milestones can then be investigated independently of the final regret bound. The later UCBVI-BF mission uses the same paper's model with a different bonus. Azar, Osband and Munos, 2017, pp. 3–5, 14–17.

Difficulty

The visit count $N_k(x,a)$ is random and depends on earlier observations and decisions. A concentration inequality for a predetermined number of samples therefore does not immediately give a statement that holds at every episode start. The algorithm also reuses the previous episode's $Q$ estimate through a minimum. Any optimism claim must account for this dependence across episodes as well as the backward dependence across steps. In the regret analysis, the terms called martingale differences can have either sign, so replacing a positive weight by a larger common bound can reverse an inequality. These are concrete obstacles to the printed chain of estimates. Azar, Osband and Munos, 2017, pp. 4, 17, 20–21, 28.

Formalization scope

States, actions, steps, episodes and complete outcome arrays are finite. Probabilities are finite sums of products of transition rows. The transition-row predicate is a published general definition; this mission defines the paper-specific reward-bounded MDP, policies, UCBVI-CH recursion, and path law on top of it. The starting-state rule can inspect only earlier episodes. Greedy tie-breaking is universally quantified. $V^*$ is a maximum over policies, and the bonus is read only at positive counts. A model that assigns an arbitrary probability law, fixes one starting state, or omits Algorithm 2's minimum does not represent this target. Azar, Osband and Munos, 2017, pp. 2–4.

Lean uses steps $0,\dots,H-1$ and terminal index $H$ in place of the paper's algorithmic $1,\dots,H+1$. The appendix sometimes puts the terminal value at $H$. The weighted recursion therefore runs through the final reward step, rather than ending one step early. Its typical-state threshold is $4H^2L$, as required by (34)–(36), whereas Appendix B.1 prints $2H^2L$. The proof's correction term $c_4$ dominates its other terms under $A\ge2$, which is made explicit in that milestone. The printed (11) loses a factor of two from the count display before it; only the preceding display is a milestone. Lemma 18 is stated under the empirical-model part of the confidence event and $\delta\le1$, the domain on which its bonus comparison holds. The weighted milestone retains its coefficients because the bracketed martingale terms can be negative. Azar, Osband and Munos, 2017, pp. 14–17, 20–21, 28.

The goal retains Theorem 1's constant $20$. Appendix C.1 cites Lemmas 15 and 18, but the sketch of Lemma 15 does not track that constant explicitly. Formalizing the printed bound may therefore expose a gap in its proof; the mission records the claim without weakening its constants. Contributions establishing or repairing the explicit bound, as well as the four stated milestones and reusable finite concentration results, are within scope. Azar, Osband and Munos, 2017, pp. 5, 27, 29.

Selected references

• M. G. Azar, I. Osband and R. Munos, Minimax Regret Bounds for Reinforcement Learning, arXiv:1703.05449v2, 2017. Pinned preprint.

Why batch TD(0) and batch Monte Carlo disagree

Temporal-difference (TD) learning estimates the value of each state of a Markov reward process from observed experience, updating an estimate toward a target built from the next reward and the current estimate of the next state. Monte Carlo (MC) methods instead update toward the full observed return. Both are standard prediction methods in reinforcement learning, and their relationship is a recurring question of the field (Sutton 1988).

When only a finite amount of experience is available, a common practice is to present the same data repeatedly until the estimates stop changing. Chapter 6 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) uses this setting to explain why TD(0) is often faster: under such batch updating, both methods converge deterministically, but to different answers. Batch MC finds the least-squares fit to the observed returns; batch TD(0) finds the value function of the maximum-likelihood Markov model of the data, the certainty-equivalence estimate. The comparison appears in §6.3, Optimality of TD(0) (pp. 126–128), and is illustrated by Example 6.4, You are the Predictor. The book states these conclusions without proof. This mission formalizes them.

Setting

Let $\mathcal S$ be a finite set of nonterminal states and $\mathcal S^+ = \mathcal S \cup \{\text{terminal}\}$. An episode is a finite sequence $S_0, R_1, S_1, \dots, S_{T-1}, R_T, S_T$ with $S_0, \dots, S_{T-1} \in \mathcal S$, real rewards $R_1, \dots, R_T$, and $S_T$ terminal. A batch is a finite list of episodes. A visit of $s$ is an (episode, time $t < T$) pair with $S_t = s$, and $n(s)$ counts all visits (every-visit counting).

A value array $V : \mathcal S \to \mathbb R$ is extended by $V(\text{terminal}) = 0$. For a discount rate $\gamma \in [0,1]$, the return is $G_t = \sum_{k=t+1}^{T}\gamma^{k-t-1}R_k$ and the TD error is $\delta_t = R_{t+1} + \gamma V(S_{t+1}) - V(S_t)$.

Batch TD(0) with step size $\alpha$ computes the TD(0) increment for every visit in the batch and changes $V$ once, by their sum:

$$V_{m+1}(s) = V_m(s) + \alpha\sum_{\text{visits } t \text{ of } s}\big[R_{t+1} + \gamma V_m(S_{t+1}) - V_m(S_t)\big].$$

Batch constant-$\alpha$ MC is the same iteration with the increment $G_t - V_m(S_t)$.

The maximum-likelihood model of the batch has transition probabilities $\hat p(j \mid i) = N(i,j)/n(i)$, where $N(i,j)$ counts the observed transitions from $i$ to $j \in \mathcal S^+$, and expected rewards $\hat r(i,j)$ equal to the average reward observed on those transitions. With $\hat P = (\hat p(s'\mid s))_{s,s'\in\mathcal S}$ and $\hat r(s) = \sum_j \hat p(j\mid s)\hat r(s,j)$, the certainty-equivalence estimate is the value function of this Markov reward process,

$$\hat v(s) = \sum_{k\ge0}\gamma^k\big(\hat P^k\hat r\big)(s).$$

Formalization targets

Goal: batch TD(0) converges to the certainty-equivalence estimate

For every finite batch and every $\gamma \in [0,1]$, the series defining $\hat v$ converges, and there is $\bar\alpha > 0$ such that for all $\alpha \in (0,\bar\alpha)$ and all initial arrays $V_0$,

$$\lim_{m\to\infty} V_m(s) = \hat v(s)\quad\text{for every visited } s, \qquad V_m(s) = V_0(s)\ \text{otherwise}.$$

The limit depends neither on $\alpha$ nor on $V_0$ at visited states.

Milestones

1. (6.6): with $V$ held fixed, $G_t - V(S_t) = \sum_{k=t}^{T-1}\gamma^{k-t}\delta_k$.
2. Exercise 6.8: the same identity for action values, $\delta_t = R_{t+1} + \gamma Q(S_{t+1},A_{t+1}) - Q(S_t,A_t)$.
3. Least squares: the sample averages $\bar G(s)$ of the returns after the visits to $s$ minimize $\sum_{\text{visits}}(G_t - V(S_t))^2$ over all arrays $V$.
4. Batch MC: for small $\alpha$, batch constant-$\alpha$ MC converges to $\bar G(s)$ at every visited $s$.
5. Fixed points: the batch TD(0) increments vanish everywhere if and only if $V = \hat v$ on visited states.
6. Example 6.4: on the eight episodes $A,0,B,0$; $B,1$ (six times); $B,0$ with $\gamma = 1$, the certainty-equivalence estimate is $\hat v(A) = \hat v(B) = 3/4$ and batch TD(0) converges to it, while batch MC converges to $V(A) = 0$, $V(B) = 3/4$.

Significance

The result explains the empirical observation of Figure 6.2 in the book: batch TD(0) has lower error than batch MC on Markov data, because it computes the certainty-equivalence estimate, while batch MC fits the training returns. It also gives a precise meaning to the claim that TD methods approximate the certainty-equivalence solution with memory linear in the number of states, where computing it directly needs a model of quadratic size and cubic time (p. 128). Identity (6.6) is the starting point of the $n$-step and eligibility-trace methods of later chapters.

The comparison under repeated presentation of a finite training set goes back to Sutton 1988, but the textbook states the conclusions without proof, and no machine-checked version is known to exist. The formalization pins down every hypothesis the text leaves implicit: the step-size threshold, the treatment of unvisited states, every-visit counting, and the undiscounted case.

Difficulty

The fixed-point equation of batch TD(0) is $D(\hat r + \gamma\hat PV - V) = 0$ on visited states, with $D$ the diagonal of visit counts, and convergence of the iteration $V \mapsto V + \alpha D(\hat r + \gamma\hat P V - V)$ requires every eigenvalue of $D(I - \gamma\hat P)$ to have positive real part. For $\gamma < 1$ this follows from $\hat P$ being substochastic. For $\gamma = 1$, the case of Example 6.4, $\hat P$ is only substochastic and the naive contraction argument fails: invertibility of $I - \hat P$ must be derived from the structure of the data, since every episode ends in the terminal state. The matrix $D(I - \gamma\hat P)$ is not symmetric, so symmetric positive-definiteness arguments do not apply. The same issue makes convergence of the series defining $\hat v$ nontrivial at $\gamma = 1$.

Formalization scope

An episode is a Lean List (X × ℝ) of transitions $(S_t, R_{t+1})$, with the terminal state represented by none : Option X; a batch is a list of episodes; states form a Fintype. Values at the terminal state are $0$ by definition. The certainty-equivalence estimate is defined from returns as the series $\sum_k\gamma^k\hat P^k\hat r$, not as the solution of a Bellman equation, and its convergence is part of the goal, not assumed. "Sufficiently small $\alpha$" is an existential threshold $\bar\alpha > 0$ quantified before $\alpha$ and $V_0$; a statement for one fixed $\alpha$, or for some $\alpha$, would be weaker than the book's and is ruled out. Unvisited states receive no increment and keep their initial value; the goal records this rather than claiming convergence to $\hat v$ there. The standing assumption $\gamma \in [0,1]$ includes $\gamma = 1$. Every visit is counted in both the TD increments and the model; mixing first-visit and every-visit counts would make the goal false.

The mission needs only finite sums, matrix powers and limits of real sequences; Mathlib's Matrix and Filter.Tendsto suffice. A lemma that a nonnegative matrix whose rows reach an absorbing mass has spectral radius below one would be reusable beyond this mission, as would a convergence criterion for $V \mapsto V + \alpha(b - MV)$ when $M$ is a nonsingular M-matrix. Contributions of either kind, and of the elementary milestones 1–3, are welcome.

Selected references

• Richard S. Sutton and Andrew G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §6.1 and §6.3, pp. 119–129. http://incompleteideas.net/book/the-book-2nd.html
• Richard S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3, 9–44, 1988. https://doi.org/10.1007/BF00115009

Why policy improvement matters

Reinforcement learning methods search for good behaviour by alternating two activities: estimating how good the current behaviour is, and changing the behaviour in the direction those estimates suggest. Sutton and Barto call this pattern generalized policy iteration and use it as the organizing idea of their textbook (Sutton & Barto 2018, §4.6). Its mathematical justification is a single result of Chapter 4, the policy improvement theorem (p. 78): a comparison made one step ahead, at each state separately, certifies that a changed policy is at least as good everywhere. Policy iteration, value iteration, Monte Carlo control with ε-greedy policies (Chapter 5), Sarsa and Q-learning are all motivated by it.

The chapter's results go back to the foundations of dynamic programming: the Bellman optimality equation (Bellman 1957), and policy iteration with its finite termination for discounted finite Markov decision processes (Howard 1960). Standard modern treatments are Puterman 1994, Ch. 6, and Bertsekas 2012, Vol. II, Ch. 1.

Setting

A finite Markov decision process has a finite state set $\mathcal S$, a finite nonempty action set $\mathcal A$, a finite reward set $\mathcal R\subset\mathbb R$ and dynamics $p(s', r\mid s, a)$: for each state $s$ and action $a$, a probability distribution over the next state $s'$ and reward $r$ (Eqs. (3.2)–(3.3)). A policy $\pi$ gives probabilities $\pi(a\mid s)$ of choosing each action in each state; a deterministic policy is a map $\pi:\mathcal S\to\mathcal A$.

Fix a discount rate $0\le\gamma<1$. The state-value function of $\pi$ is the expected discounted return

$$v_\pi(s) = E_\pi\Big[\sum_{k=0}^\infty \gamma^k R_{t+k+1}\ \Big|\ S_t=s\Big],$$

and the action-value function is defined from it by (4.6):

$$q_\pi(s,a) = \sum_{s',r} p(s',r\mid s,a)\,\big[r+\gamma v_\pi(s')\big],$$

the value of taking $a$ once in $s$ and following $\pi$ afterwards. A policy is optimal if its value is at least that of every policy at every state, and the optimal value function is $v_*(s)=\max_\pi v_\pi(s)$. A deterministic policy $\pi'$ is greedy with respect to $q_\pi$ if $\pi'(s)\in\operatorname{argmax}_a q_\pi(s,a)$ for all $s$ (4.9).

Formalization targets

Goal: the policy improvement theorem, (4.7)–(4.8), p. 78

For deterministic policies $\pi,\pi'$,

$$\big(\forall s,\ q_\pi(s,\pi'(s))\ge v_\pi(s)\big)\ \Longrightarrow\ \big(\forall s,\ v_{\pi'}(s)\ge v_\pi(s)\big),$$

and at every state where the hypothesis is strict, the conclusion is strict at that same state.

Milestones

1. Iterative policy evaluation (4.5), p. 74. From any $v_0$, the iterates $v_{k+1}(s)=\sum_a\pi(a\mid s)\sum_{s',r}p(s',r\mid s,a)[r+\gamma v_k(s')]$ converge to $v_\pi$.
2. Greedy improvement (4.9), p. 79. A greedy $\pi'$ with respect to $q_\pi$ satisfies (4.7), hence $v_{\pi'}\ge v_\pi$.
3. The stochastic case, p. 79. For stochastic $\pi,\pi'$, with $q_\pi(s,\pi'(s))=\sum_a\pi'(a\mid s)q_\pi(s,a)$ as in (5.2), the theorem holds as stated, strictness included.
4. Equality forces optimality, p. 79. If a greedy $\pi'$ has $v_{\pi'}=v_\pi$, then $v_{\pi'}$ solves the Bellman optimality equation (4.1), $v_{\pi'}=v_*$, and $\pi$ and $\pi'$ are optimal.
5. Policy iteration, p. 80. For every sequence of deterministic policies with $\pi_{k+1}$ greedy with respect to $q_{\pi_k}$: each step is a strict improvement unless $\pi_k$ is optimal, and from some $K$ on every $\pi_k$ is optimal with $v_{\pi_k}=v_*$.
6. Value iteration (4.10), p. 83. $v_*$ is attained by one policy at all states, and from any $v_0$ the iterates $v_{k+1}(s)=\max_a\sum_{s',r}p(s',r\mid s,a)[r+\gamma v_k(s')]$ converge to $v_*$.

Significance

The results. The policy improvement theorem turns a local test into a global guarantee: it is enough to check, state by state, that one step of the new policy followed by the old one does no worse than the old one. Combined with the finiteness of the set of deterministic policies, it yields the finite termination of policy iteration and, with the equality case, the existence of a deterministic optimal policy. The stochastic form is what Chapter 5 invokes for ε-greedy control. Value iteration is the other classical way to compute $v_*$.

Formalizing them. All of these results are classical and proved in the literature cited above; they are not open. The textbook presents them informally ("we chose not to produce a rigorous formal treatment", p. xiii): the improvement theorem is argued by an unbounded chain of expansions, and the policy evaluation and value iteration convergence claims are stated without proof. The mission makes each claim precise with explicit hypotheses and asks for machine-checked proofs against the book's own model with four-argument dynamics and stochastic policies. Related platform results use different models (cost minimization with deterministic policies in Bertsekas's Dynamic Programming; an expected-reward kernel and an assumed fixed point in Foundations of Machine Learning), and none states the policy improvement theorem itself.

Difficulty

The book's proof expands $q_\pi$ with (4.6) and reapplies (4.7) indefinitely, ending with "$\le\cdots=v_{\pi'}(s)$". Made rigorous, the chain is an inequality between truncated returns plus a remainder $\gamma^n E_{\pi'}[v_\pi(S_{t+n})]$, and the passage to the limit needs the remainder to vanish and the truncated returns to converge to $v_{\pi'}$. Since $v_\pi$ is defined here as a series of expected rewards under the induced Markov chain, connecting it to the one-step quantities requires first establishing the Bellman equation for $v_\pi$ from that series. The strictness part does not follow from the weak inequality alone: strictness at one state must be shown to survive the averaging over later states, which requires tracking the contribution of the first step exactly. The policy iteration statement additionally requires handling ties: a greedy step taken from an optimal policy can move to a different optimal policy, so the sequence need not become constant.

Formalization scope

All objects live in the namespace SuttonBartoRL.DP. States and actions are finite types, actions nonempty where a maximum is taken; one action set serves all states (footnote 3, p. 48). Rewards form a finite set $\mathcal R\subset\mathbb R$, and the dynamics are a function $p(s',r\mid s,a)$ whose values off $\mathcal R$ are never used. Policies are stochastic; deterministic policies are embedded as policies that choose one action with probability one.

Committed conventions:

• Discount $0\le\gamma<1$ throughout. The book also allows $\gamma=1$ when "eventual termination is guaranteed" (p. 74) but never states that hypothesis precisely; the episodic case with a terminal state is out of scope. This is the only restriction relative to the text.
• $v_\pi$ from returns. $v_\pi(s)=\sum_k\gamma^k(P_\pi^k r_\pi)(s)$, with $P_\pi$ the state transition matrix of $\pi$ and $r_\pi$ its expected one-step reward. $q_\pi$ is defined by (4.6), as the book does. The Bellman equation (4.4) is not assumed. Defining $v_\pi$ as the fixed point of a Bellman operator would make the goal an order property of that operator and is excluded.
• $v_*$ is the real supremum over all stochastic policies; the value iteration item also asserts it is attained. Optimality of a policy means dominance over all stochastic policies.
• Greedy means $\pi'(s)$ is any maximizer of $q_\pi(s,\cdot)$; tie-breaking is arbitrary and may differ between iterations.
• Stochastic case. The book only says the theorem "carries through as stated"; the meaning $q_\pi(s,\pi'(s))=\sum_a\pi'(a\mid s)q_\pi(s,a)$ is taken from the book's (5.2), p. 101.
• Policy iteration is the idealized sequence with exact evaluation. The item does not claim that the boxed pseudocode on p. 80 stops, which it may fail to do under ties (Exercise 4.4, p. 82).
• Convergence of iterates is in the product topology on $\mathbb R^{\mathcal S}$, equivalent to the sup norm for finite $\mathcal S$.

In-place (asynchronous) sweeps (§4.5) and truncated policy iteration are not formalized.

Needed infrastructure: summability of discounted series of bounded expected rewards, the Bellman equation for $v_\pi$ derived from the return definition, contraction arguments in the sup norm on $\mathbb R^{\mathcal S}$, and finiteness of the set of deterministic policies. The definitions here duplicate those of the series' Chapter 3 mission and are intended to be merged with them; lemmas about $v_\pi$, the Bellman equation and contraction are reusable by every later mission of the series, and contributions of such lemmas are welcome.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 4. http://incompleteideas.net/book/the-book-2nd.html
• R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://press.princeton.edu/books/paperback/9780691146683/dynamic-programming
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960. https://mitpress.mit.edu/9780262080095/dynamic-programming-and-markov-processes/
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. II, 4th ed., Athena Scientific, 2012. http://www.athenasc.com/dpbook.html

Motivation

Stochastic approximation is the family of recursive algorithms that locate a zero of a vector field $h$ from noisy evaluations of it. Temporal-difference learning, Q-learning, actor–critic methods and stochastic gradient descent are all instances. In practice these algorithms are often run with a constant or bounded, non-vanishing stepsize: the iterate keeps adapting to new data and never freezes, at the price of never converging exactly. The natural question for such a scheme is quantitative: how far from the target does the iterate stay in the long run, and how does that distance scale with the stepsize?

Borkar and Meyn (SIAM J. Control Optim. 38(2), 2000) answer both halves of the question under one set of hypotheses. First, stability of a "fluid" ODE obtained by scaling $h$ at infinity implies that the iterates have bounded second moments, with no a priori boundedness or projection assumption. Second, if the ODE $\dot x = h(x)$ has a globally exponentially stable equilibrium $x^*$, the asymptotic mean-square error is of the order of the largest stepsize. The first result replaced the usual stochastic-Lyapunov-function verification in reinforcement-learning applications (Section 3 of the paper). This mission formalizes the bounded-stepsize branch of the paper. A companion mission (… I: Stability and Almost-Sure Convergence under Tapering Stepsizes) covers the vanishing-stepsize branch.

Setting

Fix $d \ge 1$ and a Lipschitz vector field $h : \mathbb{R}^d \to \mathbb{R}^d$. The stochastic approximation recursion (1.1) is

$$X(n+1) = X(n) + a(n)\big[h(X(n)) + M(n+1)\big], \qquad n \ge 0,$$

with a deterministic step sequence $\{a(n)\}$ and a noise sequence $\{M(n)\}$ on a probability space $(\Omega, \mathcal F, \mathsf P)$. The associated ODE (1.2) is $\dot x = h(x)$.

• The scaled fields are $h_r(x) = r^{-1} h(rx)$. Assumption (A1) asks that $h$ be Lipschitz, that $h_r(x) \to h_\infty(x)$ for every $x$ as $r \to \infty$, and that the origin be an asymptotically stable equilibrium of the fluid ODE $\dot x = h_\infty(x)$.
• Let $\mathcal F_n = \sigma(X(0), \dots, X(n))$. Assumption (A2) asks that $\{M(n)\}$ be a martingale difference sequence, $\mathsf E[M(n+1) \mid \mathcal F_n] = 0$, with conditional second moments $\mathsf E[\|M(n+1)\|^2 \mid \mathcal F_n] \le C_0(1 + \|X(n)\|^2)$ for a constant $C_0$.
• Assumption (BS), bounded stepsizes: $0 < \underline\alpha \le a(n) \le \bar\alpha < 1$ for all $n$, with $\underline\alpha < \bar\alpha$.
• The error (2.2) is $e(n) = \|X(n) - x^*\|$.

An equilibrium $x^*$ of (1.2) is globally asymptotically stable if it is Lyapunov stable and attracts every solution. It is globally exponentially asymptotically stable if there are $b$ and $\delta > 0$ with $\|x(t) - x^*\| \le b\,e^{-\delta t}\|x(0) - x^*\|$ for every solution.

The proofs compare the iterates with ODE solutions on a time grid: $t(n) = \sum_{i<n} a(i)$, blocks $T(j) = t(m(j))$ of length about $T$, the interpolated path $\psi$ of the iterates, its rescaled version $\phi_j = \psi/r(j)$ with $r(j) = \max(1, \|X(m(j))\|)$, and the ODE solutions $\hat\psi$, $\hat\phi_j$ restarted at each block.

Formalization targets

Goal: Theorem 2.3(ii)

Under (A1), (A2) and (BS), if $x^*$ is a globally asymptotically and globally exponentially asymptotically stable equilibrium of (1.2), there are $\alpha^* > 0$ and $b_2 < \infty$ such that for all $0 < \bar\alpha \le \alpha^*$ and every initial condition $X(0)$,

$$\limsup_{n \to \infty} \mathsf E\big[e(n)^2\big] \le b_2\, \bar\alpha .$$

The constant $b_2$ is uniform in the stepsizes and in $X(0)$. No rate constant is fixed: only the linear dependence on $\bar\alpha$ is asserted.

Milestones

1. Lemma 4.7. For fixed $T > 0$ there is $C_2$, independent of the stepsizes, with $\mathsf E[\|\phi_j(t) - \hat\phi_j(t)\|^2 \mid \mathcal F_{m(j)}] \le C_2\bar\alpha$ and $\mathsf E[\|\phi_j(t)\|^2 \mid \mathcal F_{m(j)}] \le C_2$ on every block.
2. Theorem 2.1(ii). There are $\alpha^* > 0$ and $C_1$ with $\limsup_n \mathsf E\|X(n)\|^2 \le C_1$ whenever $\bar\alpha < \alpha^*$.
3. Lemma 4.8. For $\bar\alpha \le \alpha^*$, $\sup_{t \ge 0} \mathsf E\|\hat\psi(t) - \psi(t)\|^2 \le C_3 \bar\alpha$.

Significance

The result. Theorem 2.1(ii) says that a stability property of a deterministic ODE at infinity controls a stochastic recursion in mean square, uniformly over initial conditions. Theorem 2.3(ii) turns this into an error bound: with a non-vanishing stepsize the iterate does not converge, but its mean-square distance from $x^*$ is eventually $O(\bar\alpha)$. This is the quantitative justification for constant-stepsize stochastic approximation in reinforcement learning and adaptive control, and it is the starting point of the trade-off between bias (small stepsize) and speed (large stepsize) discussed in Section 2.2 of the paper.

Formalizing it. The results are proved in the paper, partly by sketch: Lemma 4.8's proof refers to "familiar arguments using the Bellman–Gronwall lemma", and the paper writes several bounds as $O(\bar\alpha)$. A formal proof makes every constant and its dependence explicit, which the paper's quantifier order leaves partly implicit (see the scope section). No machine-checked proof of these results, or of any stochastic-approximation stability theorem in this generality, is known to exist.

Difficulty

The natural first argument, that the iterates track the ODE and the ODE converges, needs the iterates to be bounded. Bounded iterates are exactly what is being proved, so the argument is circular. The paper breaks the circularity by rescaling: on each block the iterate is divided by $r(j)$, so that on large scales it tracks the fluid ODE, whose stability contracts the norm by a fixed factor per block. Making this work in mean square requires conditional second-moment estimates that are uniform in the stepsize and the scale (Lemma 4.7). A second difficulty is that the stepsize does not vanish: the tracking error per block does not go to zero, and the goal's content is precisely that it is of order $\bar\alpha$ with a constant that does not depend on $\bar\alpha$.

Formalization scope

• The state space is EuclideanSpace ℝ (Fin d). ODE solutions are forward solutions: continuous on $[0,\infty)$ with right derivatives. Stability notions are the standard ones, with exponential stability in the form the proof of Theorem 2.3(ii) uses.
• The filtration is the natural filtration of the iterates. (A2) includes integrability of $M(n+1)$ and $\|M(n+1)\|^2$ so that the conditional expectations are meaningful. Each theorem quantifies over every probability space, every measurable process satisfying (1.1) and (A2), and every deterministic $X(0)$.
• Second moments, suprema and $\limsup$ are computed in $[0,\infty]$, so a bound is a genuine finiteness claim.
• Constant placement. $\alpha^*$, $C_1$ and $b_2$ depend only on $h$, $h_\infty$, $C_0$ (and $x^*$). $C_2$ depends in addition on $T$, and $C_3$ on $T$ and $X(0)$. None depends on the stepsizes. Theorem 2.3's page text puts $b_2$ after $\alpha$. Read literally, that would allow $b_2 = C_1/\bar\alpha$ and make the goal a restatement of Theorem 2.1(ii). The formal goal fixes $b_2$ before the stepsizes and the initial condition, as the proof ($16C_3\bar\alpha$) gives. $\alpha^*$ is existential in Theorem 2.3(ii) and Lemma 4.8 rather than tied to Theorem 2.1(ii)'s witness.
• The proof objects $\hat\psi$, $\hat\phi_j$ are characterized by predicates (initial value, continuity, ODE on the block). Lemmas 4.7 and 4.8 hold for every function satisfying them.
• Not included: Theorem 2.3(i) (its proof chooses a radius depending on $\bar\alpha$), Theorem 2.4 and the Markov-chain results of Section 4.3, and the asynchronous extension (Theorem 2.5). The deterministic ODE lemmas 4.1–4.4 belong to the companion mission.

Useful infrastructure, reusable beyond this mission: Bellman–Gronwall inequalities in discrete time (Lemma 4.3 of the paper), stability of scaled ODEs, and conditional second-moment estimates for martingale-difference-driven recursions. Contributions of any of these as separate lemmas are welcome.

Selected references

• V. S. Borkar and S. P. Meyn, The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning, SIAM J. Control Optim. 38(2):447–469, 2000. https://doi.org/10.1137/S0363012997331639
• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999. https://doi.org/10.1007/BFb0096509
• H. J. Kushner and G. G. Yin, Stochastic Approximation and Recursive Algorithms and Applications, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97441