Reinforcement Learning

Why finite-horizon reinforcement learning needs a variance-sensitive bound

An agent can learn to act in an unknown environment by repeatedly running a finite episode, observing the states reached after its actions, and updating its model of the environment. The agent must trade off rewards in the current episode against information that may improve later decisions. A regret bound measures the cumulative value lost relative to an optimal policy that knows the true transition probabilities. Its dependence on the number of states, actions, episode steps, and interactions says how much exploration that uncertainty can force.

Azar, Osband, and Munos study this question for a finite-horizon Markov decision process with known, bounded rewards and an unknown, stationary transition kernel. Their UCBVI algorithm estimates action values from observed transitions and adds an exploration bonus. Their second version, UCBVI-BF, uses the empirical variance of the next-state value in that bonus. Their Theorem 2 gives an explicit high-probability regret bound whose leading dependence on the horizon is smaller than the bound they give for the simpler UCBVI-CH bonus. The paper states that, in a sufficiently long-run regime, its leading order matches the cited lower-bound scale up to logarithmic factors. This mission targets the explicit theorem, including its lower-order terms, rather than only that asymptotic comparison.

The MDP, interaction, and algorithm

Let $\mathcal S$ and $\mathcal A$ be nonempty finite state and action sets with cardinalities $S$ and $A$. A stationary transition kernel $P(y\mid x,a)$ is a probability distribution on next states $y$ for every current state $x$ and action $a$. The reward $R(x,a)$ is deterministic, known to the learner, and lies in $[0,1]$. These are the conditions of Assumption 1 and §2. Episodes have $H\ge1$ steps; $K$ episodes comprise $T=KH$ interactions.

A policy $\pi$ chooses an action for each state and step. Its value $V_h^\pi(x)$ is the expected reward from step $h$ through the final step when the state at $h$ is $x$; the terminal value is $V_{H+1}^\pi=0$. The optimal value $V_h^*(x)=\sup_\pi V_h^\pi(x)$ ranges over all deterministic policies of this form. At the start of episode $k$, the environment may choose the initial state using the completed episodes. The learner then fixes a policy $\pi_k$, observes transitions during the episode, and updates counts for the next episode. Its regret is

$$\operatorname{Regret}(K)=\sum_{k=1}^{K}\bigl(V_1^*(x_{k,1})-V_1^{\pi_k}(x_{k,1})\bigr).$$

For each state-action pair, $N_k(x,a,y)$ counts transitions to $y$ in episodes before $k$, and $N_k(x,a)=\sum_yN_k(x,a,y)$. When the latter is positive, $\widehat P_k(y\mid x,a)=N_k(x,a,y)/N_k(x,a)$. The count $N'_{k,h}(y)$ records previous episodes whose state at step $h$ was $y$. Algorithms 2 and 4 compute optimistic $Q_{k,h}$ backward from zero terminal value, take a minimum with the previous episode's $Q$ estimate and with $H$, and choose a maximizing action at every state. Previously unseen pairs receive $Q_{k,h}=H$. The Bernstein–Freedman bonus uses the empirical variance of $V_{k,h+1}$ under $\widehat P_k$ and an additional term based on $N'_{k,h+1}$; the algorithm uses $L_{\rm alg}=\ln(5SAT/\delta)$.

Formalization targets

The goal is Theorem 2 on p. 5. For any MDP and interaction described above and every $\delta>0$, write $L=\ln(5HSAT/\delta)$. The target is the exact bad-event form of the printed high-probability bound:

$$\Pr\!\left\{\operatorname{Regret}(K)>30HL\sqrt{SAK}+2500H^2S^2AL^2+4H^{3/2}\sqrt{KL}\right\}\le\delta.$$

The milestone list contains three empirical-transition deviations from the proof of Lemma 1: Eq. (9) for a value-weighted transition error, the displayed count bound before Eq. (11), and Eq. (12) for the full transition row's $\ell_1$ error. It also contains Lemma 2's variance comparison and Eq. (26), which relates cumulative conditional next-value variance to the variance of an episode return. These are source-indexed targets, with their printed constants retained.

What the result and its formalization supply

The theorem gives a quantitative guarantee for a particular executable decision rule: its regret grows sublinearly in $K$ in the leading term, with explicit dependence on $S$, $A$, and $H$. The result lets one compare the horizon dependence of a variance-sensitive bonus with a value-agnostic bonus under the same finite-horizon model. It also fixes which logarithm belongs in the algorithm and which appears in the reported bound; replacing either changes the claim.

A formal proof would connect a fully specified adaptive interaction to its finite probability law, empirical counts, backward value iteration, and the stated high-probability conclusion. The local prior-art search found reusable transition-kernel vocabulary and general concentration tools, but no published formal statement of this exact UCBVI-BF algorithm or theorem. The mission's finite path and variance definitions can also support other episodic reinforcement-learning bounds that use conditional variance.

Where the difficulty lies

The bonus is computed using a value function that itself depends on earlier observations and the same episode's backward recursion. A concentration inequality for a fixed transition row and a fixed test function therefore does not directly control every value estimate encountered by the algorithm. The number of samples in a row is also random and changes with the learner's past actions. The regret compares a policy's value at an environment-chosen initial state with a supremum over all policies, while the learner's greedy action must be defined at states it never visits. These dependencies are the central obstacle to turning local concentration statements into the episode-level bound.

Formalization scope and conventions

The Lean model uses finite sums rather than measure theory. A published predicate supplies the stationary, real-valued transition kernel; a local MDP adds the known deterministic reward. State and action types are finite and nonempty. Policies are deterministic and depend on the step. The supremum defining $V^*$ ranges over their finite function type. A theorem quantifies over every maximizing tie-breaking rule and every initial-state rule that reads only completed episodes. The probability of an event is constructed as a sum over finite outcome sequences, each weighted by the product of true transition probabilities. Counts use all past transitions and no current or future outcomes. These choices rule out a trivialization that assumes the desired law or optimizes over an unbounded class of arbitrary functions.

Lean indexes the $H$ steps from zero, while the paper indexes them from one. The last observed next state is kept because Algorithm 4 counts states at the terminal index $H+1$. At $N'_{k,h+1}(y)=0$, Algorithm 4's quotient is interpreted as infinite and the capped term is $H^2$; Lean's ordinary division by zero would incorrectly produce zero. The algorithm uses $L_{\rm alg}=\ln(5SAT/\delta)$, while Theorem 2's bound uses $L=\ln(5HSAT/\delta)$. For Eq. (26), the appendix ends its sums at $H-1$ under a shifted terminal convention; the local statement includes all $H$ reward steps and the terminal value $V_{H+1}=0$ used by Algorithm 2. The milestone text remains the printed text. The count milestone is the display before Eq. (11), since Eq. (11) drops a factor of $2$ under the square root present in that display.

Theorem 2 retains its printed $2500H^2S^2AL^2$ term. The appendix's displayed Lemma 13 calculation does not reproduce that second-order constant when propagated to Lemma 14; this is a source proof gap, not a hypothesis of the theorem. Work on the probability normalization, random-count concentration, adaptive value estimates, variance identity, and a valid route to the printed explicit constants is welcome. A proof with altered constants or an asymptotic-only conclusion would be a different target.

Selected references

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

Motivation

A Markov decision process (MDP) is solved for one model of its dynamics and rewards, but in practice that model is estimated from data, and a policy that is optimal for the estimate can perform poorly on the true system (Mannor et al., 2007). Robust MDPs address this by evaluating a policy against the worst model in an uncertainty set $\mathcal U$ (Iyengar, 2005; Nilim and El Ghaoui, 2005; Wiesemann, Kuhn and Rustem, 2013). Robust planning, however, solves an inner optimization over $\mathcal U$ at every Bellman update, which is expensive and does not scale to learning settings.

A separate line of work regularizes the policy (entropy, KL, Tsallis penalties) and observes empirically that regularized policies are robust to perturbations (Geist, Scherrer and Pietquin, 2019). Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) make this precise: for uncertainty sets centred at a nominal model, the robust value function is the solution of a regularized problem posed on the nominal model alone, with a regularizer that is the support function of the uncertainty set. This mission formalizes that equivalence: Proposition 3.1, Theorem 3.1 and Theorem 4.1 of the paper.

Setting

Let $\mathcal S$ and $\mathcal A$ be finite sets of states and actions, $\mathcal A$ nonempty, and $\mathcal X := \mathcal S\times\mathcal A$. Fix a discount factor $\gamma\in(0,1)$ and a strictly positive initial distribution $\mu_0\in\Delta_{\mathcal S}$. A transition kernel $P$ assigns to every pair $(s,a)$ a probability distribution $P(\cdot\mid s,a)$ on $\mathcal S$; a reward is $r\in\mathbb R^{\mathcal X}$. A policy $\pi\in\Delta_{\mathcal A}^{\mathcal S}$ assigns to every state an action distribution $\pi_s$.

For $v\in\mathbb R^{\mathcal S}$ write $r^\pi(s) = \sum_a\pi_s(a)r(s,a)$, $P^\pi(s'\mid s) = \sum_a\pi_s(a)P(s'\mid s,a)$, and define the evaluation Bellman operator

$$T^\pi_{(P,r)}v := r^\pi + \gamma P^\pi v .$$

The inner product on $\mathbb R^{\mathcal S}$ is $\langle v,\mu\rangle = \sum_s v(s)\mu(s)$, and the support function of a set $C\subseteq\mathbb R^{\iota}$ is $\sigma_C(y) = \max_{a\in C}\langle a,y\rangle$.

Given a set $\mathcal U$ of models $(P,r)$, the robust Bellman operator is

$$[T^{\pi,\mathcal U}v](s) := \min_{(P,r)\in\mathcal U}T^\pi_{(P,r)}v(s),$$

and the robust value function $v^{\pi,\mathcal U}$ is its fixed point. Around a nominal model $(P_0,r_0)$, an s-rectangular uncertainty set $\mathcal U = (P_0+\mathcal P)\times(r_0+\mathcal R)$ is given by sets $\mathcal P_s\subseteq\mathbb R^{\mathcal X}$ and $\mathcal R_s\subseteq\mathbb R^{\mathcal A}$, one per state: its models are $P(s'\mid s,a) = P_0(s'\mid s,a)+P_s(s',a)$ and $r(s,a) = r_0(s,a)+r_s(a)$, with $P_s\in\mathcal P_s$ and $r_s\in\mathcal R_s$ chosen independently for each $s$. Finally $[v\cdot\pi_s](s',a) := v(s')\pi_s(a)$.

Formalization targets

Goal: Theorem 4.1 (general robust MDP)

For $\mathcal U = (P_0+\mathcal P)\times(r_0+\mathcal R)$ and every policy $\pi$, $T^{\pi,\mathcal U}$ has a unique fixed point $v^{\pi,\mathcal U}$, and it is the optimal solution of

$$\max_{v\in\mathbb R^{\mathcal S}}\langle v,\mu_0\rangle\quad\text{s.t.}\quad v(s)\le T^\pi_{(P_0,r_0)}v(s)-\sigma_{\mathcal R_s}(-\pi_s)-\sigma_{\mathcal P_s}(-\gamma v\cdot\pi_s)\quad\forall s\in\mathcal S. \tag{2}$$

Milestones

1. Proposition 3.1. For any uncertainty set $\mathcal U = \mathcal P\times\mathcal R$ with $\mathcal P$ a nonempty compact set of kernels and $\mathcal R$ a nonempty compact set of rewards, $v^{\pi,\mathcal U}$ is the optimal solution of the robust program \max_{v}\langle v,\mu_0\rangle\quad\text{s.t.}\quad v\le T^\pi_{(P,r)}v\ \ \forall(P,r)\in\mathcal U. \tag{$P_{\mathcal U}$}
2. Theorem 3.1. For $\mathcal U=\{P_0\}\times(r_0+\mathcal R)$, $v^{\pi,\mathcal U}$ is the optimal solution of $\max_v\langle v,\mu_0\rangle$ s.t. $v(s)\le T^\pi_{(P_0,r_0)}v(s)-\sigma_{\mathcal R_s}(-\pi_s)$ for all $s$.
3. Robust counterpart (proof of Theorem 4.1, App. B.1). For every $v$ and $s$,

$$\max_{(P,r)\in\mathcal U}\{v(s)-r^\pi(s)-\gamma P^\pi v(s)\} = \sigma_{\mathcal P_s}(-\gamma v\cdot\pi_s)+\sigma_{\mathcal R_s}(-\pi_s)+v(s)-T^\pi_{(P_0,r_0)}v(s).$$

Theorem 3.1 is the special case $\mathcal P_s=\{0\}$ of the goal; it is listed separately because it is the paper's statement that policy regularization is equivalent to reward uncertainty.

Significance

The goal says that a robust MDP with s-rectangular uncertainty in both reward and transitions is a regularized MDP on the nominal model, with two regularizers: a policy regularizer $\sigma_{\mathcal R_s}(-\pi_s)$ coming from reward uncertainty, and a regularizer $\sigma_{\mathcal P_s}(-\gamma v\cdot\pi_s)$ coming from transition uncertainty that depends on both the policy and the value. For ball-shaped sets these support functions are explicit ($\alpha^r_s\|\pi_s\|$ and $\alpha^P_s\gamma\|v\|\|\pi_s\|$, Corollary 4.1 of the paper), which leads to the twice regularized (R²) Bellman operators of Section 5 and to robust planning at the cost of non-robust planning. Theorem 3.1 also explains why standard policy regularizers (negative entropy, KL, Tsallis) yield robustness: each is the support function of a reward uncertainty set.

The results are proved in the paper (appendices A.1, A.2, B.1); none has a machine-checked proof. The mission produces formal statements and proofs of the equivalence, the robust Bellman operator's fixed-point theory for stochastic policies and general compact uncertainty sets, and a closed-form robust counterpart that later R² results can import. The paper's printed proof of Proposition 3.1 treats $T^{\pi,\mathcal U}$ as linear in one step; a formal proof settles the statement independently of that step.

Difficulty

The obvious argument reads Proposition 3.1 as linear-programming duality, as for a single MDP. That fails: $T^{\pi,\mathcal U}$ is a minimum of affine maps, hence concave and not affine, and the feasible set of $(P_{\mathcal U})$ is an intersection of infinitely many half-space systems; the argument has to go through monotonicity and contraction of $T^{\pi,\mathcal U}$, which in turn requires every model in $\mathcal U$ to be a genuine transition kernel. For the goal, the paper invokes Fenchel–Rockafellar duality to evaluate the inner maximum; the work in Lean is to separate the maximum over the product set $\mathcal U$ into per-state maxima, which needs the s-rectangular structure and attainment of every maximum (compactness), and to track the index order of the perturbation $P_s(s',a)$ against the kernel $P(s'\mid s,a)$.

Formalization scope

• States and actions are finite types, A nonempty; values are S → ℝ ordered pointwise; a transition array is P : S → A → S → ℝ with P s a s' $=P(s'\mid s,a)$, and the kernel property is the published IsTransitionKernel; $P^\pi(s'\mid s)$ is the published InducedTransition. A policy has π s ∈ stdSimplex ℝ A for every s.
• Perturbations $P_s$ are functions S × A → ℝ indexed $(s',a)$, as in the paper's $\mathbb R^{\mathcal X}$; rewards perturbations are A → ℝ.
• Minima and maxima (in $T^{\pi,\mathcal U}$ and in $\sigma$) are real sInf/sSup. Every theorem assumes the sets nonempty and compact, so these are attained; nothing is quantified over an unbounded set.
• The robust value function is encoded as the fixed point of $T^{\pi,\mathcal U}$, and each theorem asserts its existence and uniqueness. The paper's definition $v^{\pi,\mathcal U}(s)=\min_{(P,r)\in\mathcal U}v^\pi_{(P,r)}(s)$ (p. 4) coincides with it for rectangular sets by a cited result; the proofs use only the fixed-point property. For the non-rectangular sets of Proposition 3.1 the pointwise minimum can be strictly larger than the fixed point and is then not the optimum of $(P_{\mathcal U})$, so the fixed point is the object the proposition is true for.
• "The optimal solution" means: feasible, objective-maximal, and the unique maximizer (uniqueness uses $\mu_0>0$).
• Disclosed hypotheses: $\mathcal U=\mathcal P\times\mathcal R$ with $\mathcal P$, $\mathcal R$ nonempty and compact and every transition in $\mathcal P$ a kernel (Prop. 3.1); $\mathcal P_s$, $\mathcal R_s$ nonempty and compact and every perturbed row $P_0(\cdot\mid s,a)+P_s(\cdot,a)$ in $\Delta_{\mathcal S}$ (Thm 4.1); reward sets rectangular in Thm 3.1, as its proof uses. These are the robust-MDP standing assumptions of p. 4 ($\mathcal P\subseteq\Delta^{\mathcal X}_{\mathcal S}$) and what makes "min" and "max" well defined.
• Not drafted: Corollary 4.1, whose ℓ²-ball $\mathcal P_s$ contains perturbations that leave the simplex, so $P_0+\mathcal P$ is not a set of kernels; Corollary 3.1 and Proposition 3.2 (consequences after the goal; Prop. 3.2 depends on an unspecified policy parametrization).
• A formalization that asserts only that the feasible sets of $(P_{\mathcal U})$ and (2) coincide, or that drops the kernel condition or the existence of the fixed point, does not count: the goal names the robust value function and its optimality.
• "Convex" in the statement of Theorem 4.1 is descriptive and is not part of the formal goal.

Contributions welcome: the monotone-contraction fixed-point lemma for $T^{\pi,\mathcal U}$ and the per-state separation of maxima over rectangular sets are reusable for any robust MDP mission.

Selected references

• E. Derman, M. Geist, S. Mannor, Twice regularized MDPs and the equivalence between robustness and regularization, NeurIPS 2021. arXiv:2110.06267v1
• G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. doi:10.1287/moor.1040.0129
• A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. doi:10.1287/opre.1050.0216
• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov decision processes, Mathematics of Operations Research 38(1), 2013. doi:10.1287/moor.1120.0566
• M. Geist, B. Scherrer, O. Pietquin, A theory of regularized Markov decision processes, ICML 2019. PMLR 97
• S. Mannor, D. Simester, P. Sun, J. N. Tsitsiklis, Bias and variance approximation in value function estimates, Management Science 53(2), 2007. doi:10.1287/mnsc.1060.0614

Motivation

Stochastic approximation is the family of recursive algorithms that locate a zero of a function observed only through noisy evaluations. It goes back to Robbins and Monro (1951) and today underlies stochastic gradient descent, temporal-difference learning, Q-learning and actor–critic methods in reinforcement learning, and models of learning by boundedly rational agents.

The standard analysis is the O.D.E. method (Ljung 1977; see Kushner and Yin 1997): the interpolated iterates are compared with the solutions of an ordinary differential equation, and convergence of the algorithm follows from the stability of that ODE. The method has one well-known gap. It assumes, rather than proves, that the iterates remain bounded with probability one. In applications this stability hypothesis is often the hardest part: for asynchronous Q-learning and adaptive critic algorithms, almost sure boundedness had been proved only for discounted cost or after adding a projection step (Borkar and Meyn, p. 460).

Borkar and Meyn (SIAM J. Control Optim. 38 (2000)) close this gap with a scaling argument borrowed from the fluid-model approach to the stability of queueing networks (Dai 1995; Dai and Meyn 1995). They show that boundedness itself follows from the asymptotic stability of the origin for a second, "fluid-limit" ODE obtained by rescaling the drift. This mission formalizes that stability theorem for tapering step sizes, and the convergence theorem that follows from it.

Setting

Fix $d\ge 0$ and work in $\mathbb R^d$ with the Euclidean norm. Let $h:\mathbb R^d\to\mathbb R^d$ and let $\{a(n)\}_{n\ge0}$ be a deterministic sequence of positive step sizes. On a probability space $(\Omega,\mathcal F,\mathsf P)$, random vectors $X(n)$ and $M(n)$ satisfy the stochastic approximation recursion

$$X(n+1) = X(n) + a(n)\big[h(X(n)) + M(n+1)\big], \qquad n\ge0. \tag{1.1}$$

Its mean ODE is $\dot x = h(x)$ (1.2). For $r>0$ the scaled field is $h_r(x)=h(rx)/r$, with the scaled ODE $\dot x = h_r(x)$ (1.4).

• (A1) $h$ is Lipschitz; $h_r(x)\to h_\infty(x)$ as $r\to\infty$ for every $x$; and the origin is an asymptotically stable equilibrium of the fluid-limit ODE $\dot x = h_\infty(x)$ (1.5).
• (A2) With $\mathcal F_n$ the history of the iterates up to time $n$, $\{M(n)\}$ is a martingale difference sequence, $\mathsf E[M(n+1)\mid\mathcal F_n]=0$, and for some constant $C_0<\infty$, $\mathsf E[\|M(n+1)\|^2\mid\mathcal F_n]\le C_0(1+\|X(n)\|^2)$.
• (TS) Tapering step sizes: $0<a(n)\le1$, $\sum_n a(n)=\infty$, $\sum_n a(n)^2<\infty$.

A point $x^*$ is globally asymptotically stable for $\dot x = h(x)$ if it is a Lyapunov-stable equilibrium and every solution converges to it.

Formalization targets

Goal: Theorem 2.2 (almost sure convergence)

Under (A1), (A2) and (TS), if $\dot x=h(x)$ has a unique globally asymptotically stable equilibrium $x^*$, then for every initial condition $X(0)\in\mathbb R^d$,

$$X(n)\longrightarrow x^* \qquad \text{almost surely.}$$

The goal contains no constants and no rates, only the qualitative conclusion.

Milestone: Theorem 2.1 (i) (almost sure boundedness)

Under (A1), (A2) and (TS), for every initial condition,

$$\sup_n \|X(n)\| < \infty \qquad \text{almost surely.}$$

Milestones: the lemmas of Section 4.1

• Lemma 4.1: the fluid-limit ODE is globally exponentially asymptotically stable.
• Lemma 4.2: the piecewise ODE solutions $\hat\phi$, $\phi^\infty$ used for comparison are bounded by a constant independent of the initial condition.
• Lemma 4.3 (i), (ii): two discrete Bellman–Gronwall inequalities.
• Lemma 4.4: for large scale $r$, every solution of $\dot x = h_r(x)$ from the unit ball is $\epsilon$-small on a window $[T,T+1]$.
• Lemma 4.5: the rescaled iterates have uniformly bounded second moments, and the rescaled noise sum $\xi$ is an $L^2$-bounded martingale.
• Lemma 4.6: almost surely the rescaled interpolated iterates $\phi$ track $\hat\phi$ and stay bounded.

Significance

The result. Theorem 2.1 (i) turns the stability hypothesis of the O.D.E. method into a checkable condition on a deterministic ODE. Theorem 2.2 then gives convergence to $x^*$ with no a priori boundedness assumption. The paper applies this to reinforcement learning, obtaining the first convergence proof for asynchronous Q-learning and adaptive critic algorithms for average-cost Markov decision processes (the asynchronous extension, Theorem 2.5, is sketched in the paper and is not part of this mission). The same fluid-limit criterion is now a textbook tool; see Borkar, Stochastic Approximation: A Dynamical Systems Viewpoint (2008), Chapter 3.

Formalizing it. The theorems are proved in the paper, and the proofs are short but rely on several standard facts stated informally: uniform convergence of $h_r$ to $h_\infty$ on compact sets, continuous dependence of ODE solutions on initial data and on the vector field, and the martingale convergence theorem. No machine-checked version of the O.D.E. method or of this stability criterion is known to exist. A formal development would give a verified link between discrete-time stochastic recursions, martingale convergence in Mathlib, and the stability theory of Lipschitz ODEs.

Difficulty

The obvious approach is to compare the iterates with solutions of $\dot x = h(x)$ over windows of fixed ODE time and to control the accumulated noise by martingale convergence. This fails without boundedness: the noise bound in (A2) grows with $\|X(n)\|$, so the deviation from the ODE can only be controlled relative to the current size of the iterate, and nothing prevents the iterates from escaping to infinity.

A second difficulty is that the hypothesis (A1) concerns only the fluid limit $h_\infty$, which describes the drift at infinite scale. It says nothing directly about $h$ at any finite state, and nothing about the noise. Any argument therefore has to transfer information from the limit $r\to\infty$ to the recursion at random, path-dependent scales, uniformly over those scales, while the noise is controlled only relative to the current size of the iterate. In Lean this involves ODE comparison and Gronwall estimates on a random partition of the time axis, conditional second-moment estimates for a rescaled recursion, and a vector-valued $L^2$ martingale convergence argument, none of which is available off the shelf for this setting.

Formalization scope

The state space is EuclideanSpace ℝ (Fin d). An ODE solution is a forward solution on $[0,\infty)$: the derivative is taken within $[0,\infty)$ at each $t\ge0$, which makes solutions continuous there. Stability notions are the standard ones (Lyapunov stability; asymptotic, global asymptotic and global exponential stability, the last in the form $\|x(t)-x^*\|\le b e^{-\delta t}\|x(0)-x^*\|$). All vector fields in the mission are Lipschitz, so forward solutions exist and are unique, and quantifying over "every solution" is meaningful.

The filtration in (A2) is the natural filtration of the iterates. Because $a(n)>0$, it carries the same information as the paper's $\sigma(X(i),M(i),i\le n)$. (A2) includes integrability of $M(n+1)$ and $\|M(n+1)\|^2$, so that the conditional expectations are meaningful. The theorems quantify over every probability space and every noise process satisfying (A2); the goal and Theorem 2.1 (i) take a deterministic initial condition, as the paper does. Stating the goal for a particular noise model (no noise, or i.i.d. noise) would be a different and much weaker theorem, and is ruled out. "$\sup_n\|X(n)\|<\infty$" is boundedness above of the set of norms, not a real supremum, which Lean sets to $0$ on unbounded sets. Second-moment suprema in Lemma 4.5 are taken in $[0,\infty]$.

The proof objects of Section 4.1 (time grid $t(n)$, blocks $m(j)$ and $T(j)$, scales $r(j)$, the interpolation $\phi$, the rescaled iterates and noise sum) are separate definitions built from the step sizes and the sample path, as on the page. The piecewise ODE solutions $\hat\phi$ and $\phi^\infty$ are characterized by a predicate, and the lemmas hold for every function satisfying it.

Useful infrastructure, reusable beyond this mission: Lipschitz ODE comparison and continuous-dependence estimates in Mathlib's ODE library, uniform convergence of $h_r$ on compact sets, the discrete Gronwall lemmas, and $L^2$-bounded vector-valued martingale convergence. Contributions are welcome on any milestone. The two Gronwall lemmas and Lemma 4.1 are self-contained entry points.

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
• H. Robbins and S. Monro, A Stochastic Approximation Method, Ann. Math. Statist. 22(3):400–407, 1951. https://doi.org/10.1214/aoms/1177729586
• L. Ljung, Analysis of Recursive Stochastic Algorithms, IEEE Trans. Automat. Control 22(4):551–575, 1977. https://doi.org/10.1109/TAC.1977.1101561
• H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997. https://doi.org/10.1007/978-1-4899-2696-8
• J. G. Dai, On Positive Harris Recurrence of Multiclass Queueing Networks: A Unified Approach via Fluid Limit Models, Ann. Appl. Probab. 5(1):49–77, 1995. https://doi.org/10.1214/aoap/1177004828
• J. G. Dai and S. P. Meyn, Stability and Convergence of Moments for Multiclass Queueing Networks via Fluid Limit Models, IEEE Trans. Automat. Control 40(11):1889–1904, 1995. https://doi.org/10.1109/9.471210
• V. S. Borkar, Stochastic Approximation: A Dynamical Systems Viewpoint, Cambridge University Press / Hindustan Book Agency, 2008. https://doi.org/10.1007/978-93-86279-38-5

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.

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

Motivation

Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They are among the most widely used methods in reinforcement learning, from REINFORCE (Williams 1992) and the policy gradient theorem to natural policy gradient and trust-region methods. The objective is not concave in the policy, even when the policy is a raw table of action probabilities, so standard optimization theory guarantees at best convergence to a stationary point, and it was long unclear whether or how fast these methods find an optimal policy.

Agarwal, Kakade, Lee and Mahajan (JMLR 2021) give a systematic answer for the tabular and function-approximation settings. This mission formalizes their warm-up result, Theorem 4.1: projected gradient ascent over the simplex of stochastic policies reaches an $\epsilon$-optimal policy after a number of iterations polynomial in the sizes of the MDP, the effective horizon $1/(1-\gamma)$, $1/\epsilon$, and a distribution mismatch coefficient. The gradient domination idea it rests on goes back to the analysis of conservative policy iteration by Kakade and Langford (2002) and to Scherrer and Geist (2014).

Setting

A finite discounted MDP consists of finite sets $\mathcal S$ of states and $\mathcal A$ of actions, a transition kernel $P(s'\mid s,a)$, rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in[0,1)$. A policy $\pi$ assigns to each state a probability distribution $\pi(\cdot\mid s)$ over actions. Its value from a start state $s_0$ is

$$V^\pi(s_0)=\mathbb E\Big[\sum_{t=0}^\infty\gamma^t r(s_t,a_t)\,\Big|\,s_0\Big],\qquad a_t\sim\pi(\cdot\mid s_t),\ s_{t+1}\sim P(\cdot\mid s_t,a_t),$$

and for a start distribution $\rho$, $V^\pi(\rho)=\sum_s\rho(s)V^\pi(s)$. The action value is $Q^\pi(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ and the advantage is $A^\pi(s,a)=Q^\pi(s,a)-V^\pi(s)$. The discounted state visitation distribution is $d^\pi_\rho(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr^\pi(s_t=s\mid s_0\sim\rho)$. An optimal policy $\pi^\star$ maximizes $V^\pi(s)$ at every state simultaneously; $V^\star=V^{\pi^\star}$.

In the direct parameterization the parameter is the table itself, $\pi_{s,a}=\pi(a\mid s)$, a point of the product simplex $\Delta(\mathcal A)^{|\mathcal S|}\subseteq\mathbb R^{\mathcal S\times\mathcal A}$. The algorithm optimizes $V^\pi(\mu)$ for a chosen start distribution $\mu$ by projected gradient ascent

$$\pi^{(t+1)}=P_{\Delta(\mathcal A)^{|\mathcal S|}}\big(\pi^{(t)}+\eta\nabla_\pi V^{(t)}(\mu)\big),$$

where $P_{\Delta(\mathcal A)^{|\mathcal S|}}$ is the Euclidean projection and $V^{(t)}=V^{\pi^{(t)}}$. Performance is measured under a possibly different distribution $\rho$, and the distribution mismatch coefficient $\|d^{\pi^\star}_\rho/\mu\|_\infty$ (componentwise ratio) measures how well $\mu$ covers the states an optimal policy visits from $\rho$.

Formalization targets

Goal: Theorem 4.1

With step size $\eta=(1-\gamma)^3/(2\gamma|\mathcal A|)$, from any initial policy, for every $\rho\in\Delta(\mathcal S)$ and $\epsilon>0$,

$$\min_{t\le T}\big\{V^\star(\rho)-V^{(t)}(\rho)\big\}\le\epsilon\qquad\text{whenever}\qquad T>\frac{64\gamma|\mathcal S||\mathcal A|}{(1-\gamma)^6\epsilon^2}\Big\|\frac{d^{\pi^\star}_\rho}{\mu}\Big\|_\infty^2 .$$

Milestones, in the order of the proof

1. Lemma 3.2 (performance difference): $V^\pi(s_0)-V^{\pi'}(s_0)=\frac1{1-\gamma}\mathbb E_{s\sim d^\pi_{s_0}}\mathbb E_{a\sim\pi(\cdot\mid s)}[A^{\pi'}(s,a)]$.
2. (7), the gradient of the direct parameterization: $\partial V^\pi(\mu)/\partial\pi(a\mid s)=\frac1{1-\gamma}d^\pi_\mu(s)Q^\pi(s,a)$.
3. Lemma 4.1 (gradient domination): $V^\star(\rho)-V^\pi(\rho)\le\frac1{1-\gamma}\|d^{\pi^\star}_\rho/\mu\|_\infty\max_{\bar\pi}(\bar\pi-\pi)^\top\nabla_\pi V^\pi(\mu)$, together with the sharper form with $d^\pi_\mu$ in place of $(1-\gamma)\mu$.
4. Lemma D.3 (smoothness): $\|\nabla_\pi V^\pi(s_0)-\nabla_\pi V^{\pi'}(s_0)\|_2\le\frac{2\gamma|\mathcal A|}{(1-\gamma)^3}\|\pi-\pi'\|_2$.
5. Theorem E.1(3) (Beck 2017, Theorem 10.15): projected gradient descent with step $1/\beta$ on a $\beta$-smooth function over a closed convex set has $\min_{t<T}\|G^\eta(x_t)\|\le\sqrt{2\beta(f(x_0)-f(x^*))}/\sqrt T$, with $G^\eta$ the gradient mapping.
6. Proposition B.1: a gradient mapping of norm at most $\epsilon$ at $\pi$ makes the next iterate $\pi^+$ $\epsilon(\eta\beta+1)$-stationary over feasible unit directions.

Significance

The theorem shows that, for the simplest constrained parameterization, a first-order method finds a globally optimal policy at a polynomial rate in spite of non-concavity. The guarantee holds for every performance distribution $\rho$ at once, and it isolates the role of exploration in a single quantity, the mismatch coefficient; Section 4.3 of the paper shows that without a well-covering $\mu$ gradient methods can need exponentially many steps. Lemma 4.1 and the smoothness bound are reused across the rest of the paper, and the performance difference lemma underlies essentially all of its analyses.

All results here are proved in the paper, with Theorem E.1 and Theorem E.2 cited from Beck (2017) and Ghadimi–Lan (2016). None of them has a machine-checked proof on the platform. A formal development provides a verified link between the policy gradient expression of the direct parameterization and a standard nonconvex projected-gradient rate, and a reusable formal library of discounted visitation distributions, the performance difference identity, and projected gradient methods on Euclidean spaces.

Difficulty

The obvious argument, "projected gradient ascent converges to a stationary point, and stationary points are optimal", fails on both counts as stated. Stationary points of $V^\pi(\mu)$ need not be optimal when $\mu$ does not cover the relevant states; the quantitative replacement is gradient domination, which only controls suboptimality through the mismatch coefficient. The convergence rate itself requires smoothness of the value as a function of the policy table, which is a bound on second derivatives of a matrix inverse $(I-\gamma P_\pi)^{-1}$ with the dependence $(1-\gamma)^{-3}$ and the factor $|\mathcal A|$ made explicit. Finally, the near-stationarity delivered by the gradient-mapping rate is at the next iterate, not the current one, which is why the conclusion is over $t\in\{0,\dots,T\}$. On the Lean side, the value is an infinite series in the policy entries, so its differentiability and the exact gradient formula have to be established for a function defined on the whole parameter space.

Formalization scope

Policies are parameter vectors in EuclideanSpace ℝ (S × A), so norms are $\ell_2$ and Mathlib's gradient is $\nabla_\pi$; the objective $\pi\mapsto V^\pi(\mu)$ is defined on the whole space and is only ever evaluated, with its gradient, at policies. The MDP layer (transition kernels, policies, $V^\pi$, $Q^\pi$, occupation distributions, optimal policies) is the published FoundationsML.ReinforcementLearning library; $V^\pi$ is the unnormalized discounted sum. The projection is any map satisfying the nearest-point property. The optimal policy is a hypothesis IsOptimalPolicy (optimal from every state), not a supremum over all functions.

Conventions committed to:

• The mismatch coefficient is any constant $D$ with $d^{\pi^\star}_\rho(s)\le D\mu(s)$ for all $s$; this avoids Lean's $x/0=0$ and is equivalent to the page's statement when the coefficient is finite.
• $\gamma>0$ and $\epsilon>0$ are explicit hypotheses of the goal (the step size divides by $\gamma$, the threshold by $\epsilon$).
• The goal concludes $\exists\,t\le T$. The printed $\min_{t<T}$ fails at $T=1$ (one state, two actions with rewards $1$ and $0$, $\gamma=0.001$, $\epsilon=1/2$, initial policy on the bad action); the proof on p. 50 establishes the range $0\le t\le T$.
• Proposition B.1 bounds the directions feasible at $\pi^+$, as its proof does; Theorem E.1 assumes smoothness on $C$ only and uses the radicand $2\beta(f(x_0)-f(x^*))$ of Beck and of p. 49.

A formalization that defines the update through formula (7), that assumes gradient domination or smoothness as hypotheses of the goal, or that takes the gradient off the simplex where the value series may diverge, would trivialize the goal; the goal mentions none of these, and (7) is a milestone theorem.

A complete development needs: summability and differentiability of the value series near the simplex; the performance difference lemma; the Euclidean projection inequality on a closed convex set; the descent lemma for functions smooth on a convex set; and the gradient-mapping argument. The projection and gradient-mapping results are independent of reinforcement learning and reusable. Contributions to any milestone are welcome, as are proofs of Theorem E.2 (Ghadimi–Lan) as a stepping stone to Proposition B.1.

Selected references

• A. Agarwal, S. M. Kakade, J. D. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22(98), 2021; arXiv:1908.00261v5. https://arxiv.org/abs/1908.00261
• A. Beck, First-Order Methods in Optimization, MOS-SIAM Series on Optimization, SIAM, 2017. https://doi.org/10.1137/1.9781611974997
• S. Ghadimi, G. Lan, Accelerated gradient methods for nonconvex nonlinear and stochastic programming, Mathematical Programming 156, 2016. https://doi.org/10.1007/s10107-015-0871-8
• S. Kakade, J. Langford, Approximately optimal approximate reinforcement learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• B. Scherrer, M. Geist, Local Policy Search in a Convex Space and Conservative Policy Iteration as Boosted Policy Search, ECML PKDD 2014, pp. 35–50 (arXiv version: https://arxiv.org/abs/1306.1520)
• R. J. Williams, Simple statistical gradient-following algorithms for connectionist reinforcement learning, Machine Learning 8, 1992. https://doi.org/10.1007/BF00992696

Motivation

The lost-sales inventory problem with lead times is a basic model of operations management. A retailer reviews one product's stock each period and places an order that arrives $L$ periods later. Demand that cannot be met from stock on hand is lost, and the retailer pays a holding cost $h$ per unit left on the shelf and a penalty $p$ per unit of lost demand. The optimal policy depends on the whole pipeline of outstanding orders, so the state space grows with $L$, and the problem is computationally hard for long lead times. Simple base-stock (order-up-to) policies are therefore the standard heuristic, and Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science 2009) showed they are asymptotically optimal as the lost-sales penalty grows.

Agrawal and Jia (arXiv:1905.04337) study the learning version, in which the demand distribution is unknown and only sales, not demands, are observed. They give an algorithm whose regret against the best base-stock policy is $\tilde O(L\sqrt T)$, improving the earlier bound of Zhang, Chao and Shi, which grows exponentially in $L$. The improvement rests on one structural fact: started from two different states, the base-stock system accumulates expected costs that differ by an amount linear in $L$ and independent of the horizon. That fact, Lemma 2.5 of the paper, is the goal of this mission.

Setting

Fix a lead time $L\ge 0$ and a base-stock level $x$. A state is a vector $\mathbf s=(s(0),s(1),\dots,s(L))$ of real numbers. Its entry $s(0)$ is the on-hand inventory after the current period's arrival, and $s(1),\dots,s(L)$ are the outstanding orders, $s(L)$ the most recent. Under a base-stock policy with level $x$ the states lie in

$$\mathcal S^x=\Big\{\mathbf s : s(i)\ge 0\ \text{for all } i,\ \sum_{i=0}^{L}s(i)=x\Big\}.$$

In each period $t$ a demand $d_t\ge 0$ is drawn, independently across periods, from a distribution $F$ on $[0,\infty)$. The sales are $y_t=\min\{s_t(0),d_t\}$ and the on-hand inventory is $I_t=s_t(0)$. The policy reorders exactly what was sold, so for $L\ge 1$ the next state is

$$\mathbf s_{t+1}=\big(s_t(0)-y_t+s_t(1),\ s_t(2),\ \dots,\ s_t(L),\ y_t\big),$$

and for $L=0$ the state $(x)$ never changes. The pseudo-cost of period $t$ is $C^x_t=h(s_t(0)-y_t)-p\,y_t$, and the value over horizon $T$ from the start state $\mathbf s$ is

$$V^x_T(\mathbf s)=\mathbb E\Big[\sum_{t=1}^{T}C^x_t\ \Big|\ \mathbf s_1=\mathbf s\Big].$$

Along a demand path, $n^x_T(\mathbf s)=\sum_{t=1}^T y_t$ is the total sales and $m^x_T(\mathbf s)=\sum_{t=1}^T I_t$ the total on-hand inventory.

States are compared by the order of Definition B.1: $\mathbf s'\succeq\mathbf s$ if $\mathbf s'-\mathbf s=\delta$ with $\sum_i\delta_i=0$ and some $0\le k\le L-1$ such that $\delta_i\ge 0$ for $i\le k$ and $\delta_i\le 0$ for $i>k$. Thus $\mathbf s'$ holds the same total, shifted toward the shelf. The state $\hat{\mathbf s}=(x,0,\dots,0)$ dominates every state of $\mathcal S^x$.

Formalization targets

Goal: Lemma 2.5 (p. 8)

For every $x$, every horizon $T$, all costs $h,p\ge 0$, every demand law $F$ and all $\mathbf s,\mathbf s'\in\mathcal S^x$,

$$V^x_T(\mathbf s)-V^x_T(\mathbf s')\le 36\max(h,p)\,L\,x .$$

The constant is the paper's printed one. The proof's last display gives $18(h+p)Lx$, a stronger bound, which is deliberately not the goal.

Milestones (Appendix B and the proof of Lemma 2.5)

All of the following hold for $L\ge 1$, along any single demand path that drives both chains:

1. Lemma B.2 (p. 20). If $\mathbf s'_1\succeq\mathbf s_1$ then for $t\le L+1$ the cumulative sales satisfy $Y'_t-Y_t\le\max_{0\le k\le t-1}(\delta_0+\dots+\delta_k)$.
2. Lemma B.3 (p. 20). If moreover $I'_t\ge I_t$ for $t=1,\dots,L+1$, then $n_T(\mathbf s'_{L+1})=n_T(\mathbf s_{L+1})$ for every $T$.
3. Lemma B.5 (p. 21). At the successive first crossing times $\sigma_i,\tau_i$ of Definition B.4, the state order alternates: $\mathbf s'_{\sigma_i}\succeq\mathbf s_{\sigma_i}$ and $\mathbf s'_{\tau_i}\preceq\mathbf s_{\tau_i}$ whenever these times exist.
4. Lemma B.6 (p. 21). If $\mathbf s'\succeq\mathbf s$ in $\mathcal S^x$ then $|n^x_T(\mathbf s')-n^x_T(\mathbf s)|\le 3x$.
5. Lemma B.7 (p. 23). If $\mathbf s'\succeq\mathbf s$ in $\mathcal S^x$ then $|m^x_T(\mathbf s)-m^x_T(\mathbf s')|\le 6Lx$.
6. Proof of Lemma 2.5 (p. 9). $\hat{\mathbf s}\succeq\mathbf s$ for every $\mathbf s\in\mathcal S^x$.
7. Proof of Lemma 2.5 (p. 9). $|V^x_T(\mathbf s)-V^x_T(\hat{\mathbf s})|\le 9(h+p)Lx$.

Significance

Lemma 2.5 bounds the dependence of the base-stock chain's finite-horizon cost on its starting state, uniformly in the horizon. In the paper it yields three consequences: the long-run average cost (the loss) of a base-stock policy does not depend on the initial state (Lemma 2.6), the bias of the chain is bounded by $36\max(h,p)Lx$ (Lemma 2.8), and finite-horizon average costs concentrate around the loss (Lemma 2.10). These feed the regret bound of Theorem 1.3. The lemma is also a statement about the base-stock lost-sales system alone, without any learning, so it is of independent interest for coupling arguments on lost-sales chains.

The paper's proof is complete on paper, but nothing in it has a machine-checked proof. Neither the lost-sales base-stock chain with lead times started from an arbitrary pipeline state nor any of the coupling lemmas of Appendix B is formalized elsewhere. This mission produces a checked proof of the goal and of the pathwise comparison lemmas. Theorem 1.3 is not posed: its supporting lemmas rely on limits whose existence the paper settles only by an informal discretization (Remark 4).

Difficulty

The obvious argument couples the two chains on a common demand path and waits until they coalesce. Coalescence is guaranteed only after $L$ consecutive periods of zero demand, an event of probability exponentially small in $L$, so this argument gives a bound exponential in $L$. That is the bound of earlier work.

The linear bound needs a finer pathwise accounting. The two coupled chains do not stay ordered: the one that starts with more inventory on the shelf sells more at first, then runs short and sells less. The order $\succeq$ between the two states alternates along a sequence of times, and the sales gained in one phase must be shown to be lost again in the next, so that the cumulative difference stays bounded by a constant multiple of $x$ for every horizon. Turning this alternation into a bound requires tracking how the pipeline vectors evolve between alternation times, including the boundary cases in which the chains coalesce or the horizon ends inside a phase.

Formalization scope

All declarations live in the namespace LostSalesLearning.ValueGap. A state is a function Fin (L + 1) → ℝ, a demand path is a function ℕ → ℝ≥0, and time is 0-based: traj s d 0 is the paper's $\mathbf s_1$, traj s d t is $\mathbf s_{t+1}$, and $\sum_{t=1}^T$ is a sum over Finset.range T. The demand law $F$ is a probability measure on ℝ≥0, and the demand path has the product law Measure.infinitePi (fun _ => F). The value is the expectation of the summed pseudo-costs, which equals Definition 2.4 by the tower property and is the form used in the paper's proof.

Committed conventions:

• The costs satisfy $h\ge 0$ and $p\ge 0$, the reading of "per unit holding cost and per unit lost sales penalty".
• No assumption is placed on $F$. The paper's assumptions $F(0)>0$ and bounded demand belong to other results.
• The goal holds for every $L\ge 0$; the Appendix B milestones carry $L\ge 1$, as Appendix B does.
• The order $\succeq$ is Definition B.1 verbatim, with the equal-sum clause and the split index $k\le L-1$.
• The pathwise milestones quantify over every demand path and drive both chains with the same path.
• The first crossing times of Definition B.4 are represented by alternationTimes; an absent next crossing is none.

Two trivializing formalizations are ruled out. A comparison of the two values on different or fixed demand paths would be a different statement: the goal compares two expectations under the same law, and each pathwise milestone uses one common path. A Bochner integral of a non-integrable function would be $0$. The integrand here is measurable and bounded by $T(h+p)x$ on $\mathcal S^x$, so the values are genuine expectations.

A complete development needs the elementary dynamics of the chain, including invariance of $\mathcal S^x$ and the shift of trajectories, which is reusable for other lost-sales models. It also needs the alternation times of Definition B.4, and measurability of the trajectory in the demand path. Proofs of individual milestones, alternative proofs of the goal, and sharper constants as separate statements are all welcome.

Selected references

• S. Agrawal and R. Jia, Learning in Structured MDPs with Convex Cost Functions: Improved Regret Bounds for Inventory Management, arXiv:1905.04337v1, 2019. https://arxiv.org/abs/1905.04337
• W. T. Huh, G. Janakiraman, J. A. Muckstadt and P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0945
• H. Zhang, X. Chao and C. Shi, Closing the Gap: A Learning Algorithm for Lost-Sales Inventory Systems with Lead Times, Management Science 66(5), 2020. https://doi.org/10.1287/mnsc.2019.3288
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887