Reinforcement Learning

Motivation

Reinforcement learning with a generative model (a simulator that returns an independent next state for any queried state–action pair) is the standard setting for measuring how many samples are needed to plan in an unknown Markov decision process. The simplest algorithm is model-based planning: query each pair $N$ times, build the empirical transition kernel, and plan in the resulting empirical MDP. Azar, Munos and Kappen (2013) showed that $\widetilde O\big(\frac{|\mathcal S||\mathcal A|}{(1-\gamma)^3\varepsilon^2}\big)$ total samples suffice and are necessary, but only for $\varepsilon \le 1/\sqrt{(1-\gamma)|\mathcal S|}$. Agarwal, Kakade and Yang (2020) extended the range to $\varepsilon \le 1/\sqrt{1-\gamma}$. A sample size barrier remained: for larger $\varepsilon$, no algorithm was known to be minimax optimal with fewer than $\frac{|\mathcal S||\mathcal A|}{(1-\gamma)^2}$ samples.

Li, Wei, Chi and Chen (arXiv:2005.12900v8, Operations Research, 2024) remove the barrier: the sample size is minimax optimal over the full range $0 < \varepsilon \le 1/(1-\gamma)$. They give two planners. The first (Theorem 1) perturbs the rewards slightly at random. The second, the subject of this mission, leaves the rewards unchanged and instead chooses among near-optimal actions by a randomized but structured rule.

Timeline:

• 2013: Azar–Munos–Kappen, minimax sample complexity of model-based planning for $\varepsilon \le 1/\sqrt{(1-\gamma)|\mathcal S|}$.
• 2018: Sidford, Wang, Wu, Yang and Ye, a model-free variance-reduced method, minimax for $\varepsilon \le 1$.
• 2020: Agarwal–Kakade–Yang, model-based planning minimax for $\varepsilon \le 1/\sqrt{1-\gamma}$, via absorbing MDPs.
• 2020 (v1) – 2024: Li–Wei–Chi–Chen, the full range $\varepsilon \le 1/(1-\gamma)$ (this paper).

Setting

A finite discounted MDP $\mathcal M = (\mathcal S,\mathcal A,P,r,\gamma)$ has states $\mathcal S$, actions $\mathcal A = \{1,\dots,|\mathcal A|\}$, a transition kernel $P(\cdot\mid s,a)$, rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in(0,1)$. A deterministic policy $\pi:\mathcal S\to\mathcal A$ has value $V^\pi(s)$, the expected discounted sum of rewards from $s$, and Q-function $Q^\pi(s,a) = r(s,a) + \gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$. The optimal value is $V^\star(s) = \max_\pi V^\pi(s)$ and $Q^\star = r + \gamma P V^\star$.

The data are $N$ independent next states $s^i_{s,a}\sim P(\cdot\mid s,a)$ for every pair, and the empirical kernel is $\widehat P(s'\mid s,a) = \frac1N\sum_i \mathbb 1\{s^i_{s,a} = s'\}$. The empirical MDP $\widehat{\mathcal M} = (\mathcal S,\mathcal A,\widehat P,r,\gamma)$ has optimal functions $\widehat Q^\star$ and $\widehat V^\star$.

The conservative planner (Algorithm 2) draws a threshold $\varsigma\sim\mathrm{Unif}(0,\xi)$ independently of the data and plays

$$\widehat\pi_{\mathrm c}(s) := \min\{a\in\mathcal A : \widehat Q^\star(s,a) > \widehat V^\star(s) - \varsigma\},$$

the smallest-indexed action whose empirical Q-value is within $\varsigma$ of optimal.

Formalization targets

Goal: Theorem 2

There are universal constants $c_0, c_1 > 0$ such that, for every MDP as above, every $\delta > 0$ and $0 < \varepsilon \le \frac1{1-\gamma}$, with $\xi = \frac{c_1(1-\gamma)\varepsilon}{|\mathcal S|^5|\mathcal A|^5}$ and

$$N \ge \frac{c_0\log\big(\frac{|\mathcal S||\mathcal A|}{(1-\gamma)\varepsilon\delta}\big)}{(1-\gamma)^3\varepsilon^2},$$

with probability at least $1-\delta$ over the data and $\varsigma$,

$$\forall (s,a):\qquad V^{\widehat\pi_{\mathrm c}}(s)\ge V^\star(s)-\varepsilon \quad\text{and}\quad Q^{\widehat\pi_{\mathrm c}}(s,a)\ge Q^\star(s,a)-\gamma\varepsilon.$$

The constants are left unspecified, as in the paper.

Milestones

The paper's own steps, in the order of §6.4:

1. Lemma 7: $\widehat V^{\pi^\star} - \widehat V^{\widehat\pi_{\mathrm c}} \le \frac{\xi}{1-\gamma}\mathbf 1$.
2. Lemma 3 and (88): the $(s,a)$-absorbing MDPs reproduce $Q^\star$ at the right reward and depend Lipschitz-continuously on it.
3. (56): a point of a finite net gives an absorbing MDP within $\omega$ of $\widehat Q^\star$.
4. Lemma 8: with probability $1-\delta$ over $\varsigma$, the near-optimal action sets are unchanged by any perturbation of size $\frac{\xi\delta}{8|\mathcal S||\mathcal A|}$.
5. (57): consequently $\widehat\pi_{\mathrm c}$ coincides with the conservative policy of every nearby absorbing MDP.
6. Lemmas 2 and 1: the policy-evaluation bounds used for the remaining terms of (53).

Significance

Theorem 2 shows that the minimax sample size $\widetilde O\big(\frac{|\mathcal S||\mathcal A|}{(1-\gamma)^3\varepsilon^2}\big)$ is reachable over the whole range of $\varepsilon$ without altering the reward function: a planner can keep the model it estimated and only change how it breaks near-ties. The guarantee covers both value and Q-function suboptimality, and with a sample size proportional to $1/(1-\gamma)$ rather than $1/(1-\gamma)^2$ in the large-$\varepsilon$ regime it allows a coarse but correct policy to be computed from very few samples.

None of these results is formalized. The mission produces a machine-checked account of the decoupling argument for data-dependent policies (absorbing MDPs, nets, stability of the tie-breaking rule), which the companion missions on Theorems 1 and 3 share. The paper omits the last step of the proof of Theorem 2 ("follows from an identical argument as in the proof of Theorem 1"); a formal proof has to supply it, including the analogue of Lemma 5 for $\widehat\pi_{\mathrm c}$, which the paper does not state.

Difficulty

The policy $\widehat\pi_{\mathrm c}$ depends on all the data, so the standard concentration argument for a fixed policy (Lemma 1) does not apply to $\widehat V^{\widehat\pi_{\mathrm c}} - V^{\widehat\pi_{\mathrm c}}$. A union bound over all $|\mathcal A|^{|\mathcal S|}$ deterministic policies costs a factor $|\mathcal S|$ in the sample size, which is exactly the barrier. The leave-one-out construction removes the samples of one pair $(s,a)$ from the policy; it works only if the policy is stable under the small change of $\widehat Q^\star$ that this causes. The greedy policy is not stable when two actions nearly tie. The conservative rule is stable with high probability over $\varsigma$ (Lemma 8), but only because it takes the smallest near-optimal action: the set $\{a : \widehat Q^\star(s,a) > \widehat V^\star(s)-\varsigma\}$ is stable, and a rule that picked an arbitrary member of it would not be.

Formalization scope

All declarations live in the namespace BreakingSample.Conservative. The MDP layer reuses the platform's FoundationsML.ReinforcementLearning definitions (IsTransitionKernel, PolicyValue, QFunction); deterministic policies enter as point-mass stochastic policies, and $V^\star$ is the maximum over the finite set of maps $\mathcal S\to\mathcal A$. Norms are sup norms on finite function types. The order on $\mathcal A$ is an arbitrary linear order on a finite type.

Probability: a data set is a map $\mathcal S\times\mathcal A\times\mathrm{Fin}\,N\to\mathcal S$ with the product law, so probabilities of data events are finite sums. The threshold $\varsigma$ has the uniform law on $[0,\xi]$; joint probabilities are $\sum_x \mathbb P(x)\,\mathrm{Unif}(0,\xi)\{\varsigma : (x,\varsigma)\in E\}$, with the outer measure for non-measurable sections. "With probability at least $1-\delta$" is stated as an upper bound $\delta$ on the probability of the failure event. Because the policy defined by (10) is a predicate on policies, the conclusion is stated for every policy satisfying (10). The universal constants are quantified before all types and parameters. The goal adds $N>0$, the standing assumption of (3); "the same assumptions of Theorem 1" is formalized with the goal's own constants $c_0, c_1$.

A trivializing formalization is ruled out: $\widehat\pi_{\mathrm c}$ is the smallest-index rule of (10), not an arbitrary policy within $\varsigma$ of optimal, and $\varsigma$ is random, not fixed.

Infrastructure that a complete development needs and that is reusable: Bellman optimality for finite MDPs with deterministic policies and real rewards, the resolvent identities, Bernstein's inequality for the empirical kernel, the absorbing-MDP construction, and the analogue of Lemma 5 for the conservative policy. Proofs of any milestone, and of the policy-evaluation lemmas, are welcome.

Selected references

• G. Li, Y. Wei, Y. Chi, Y. Chen, Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model, Operations Research, 2024; arXiv:2005.12900v8. https://arxiv.org/abs/2005.12900
• M. G. Azar, R. Munos, H. J. Kappen, Minimax PAC bounds on the sample complexity of reinforcement learning with a generative model, Machine Learning 91, 2013. https://doi.org/10.1007/s10994-013-5368-1
• A. Agarwal, S. Kakade, L. F. Yang, Model-Based Reinforcement Learning with a Generative Model is Minimax Optimal, COLT 2020. https://arxiv.org/abs/1906.03804
• A. Sidford, M. Wang, X. Wu, L. F. Yang, Y. Ye, Near-Optimal Time and Sample Complexities for Solving Markov Decision Processes with a Generative Model, NeurIPS 2018. https://arxiv.org/abs/1806.01492

Motivation

Reinforcement learning with large or continuous state spaces relies on function approximation: value functions are represented as functions of a $d$-dimensional feature map instead of tables indexed by states. Before 2019, regret guarantees for exploration with function approximation either needed strong assumptions (deterministic dynamics, a generative model) or applied only to tabular problems. Jin, Yang, Wang and Jordan (arXiv:1907.05388, COLT 2020) showed that in a linear MDP, where transitions and rewards are linear in known features, an optimistic version of least-squares value iteration, LSVI-UCB, has regret $\tilde O(\sqrt{d^3H^3T})$, with no dependence on the number of states or actions (Theorem 3.1).

Exact linearity is rarely satisfied by features chosen in practice. A guarantee that collapses under a small modelling error would say little about real use, and a naive adaptation of linear-bandit methods can break down entirely when the model is wrong. Theorem 3.2 of the same paper addresses this: if the MDP is only $\zeta$-approximately linear, LSVI-UCB with an episode-dependent bonus still has sublinear regret plus an additive term linear in $\zeta T$. This mission formalizes that result. A companion mission formalizes Theorem 3.1.

Setting

An episodic MDP has a measurable state space $\mathcal S$, a finite action set $\mathcal A$, a horizon $H$, and for each step $h\in[H]$ a transition kernel $\mathbb P_h(\cdot\mid x,a)$ and a reward $r_h:\mathcal S\times\mathcal A\to[0,1]$. A policy $\pi$ chooses an action $\pi(x,h)$ at state $x$ and step $h$. Its value functions satisfy the Bellman equation

$$Q^\pi_h(x,a)=r_h(x,a)+\int V^\pi_{h+1}\,\mathrm d\mathbb P_h(\cdot\mid x,a),\qquad V^\pi_h(x)=Q^\pi_h(x,\pi(x,h)),\qquad V^\pi_{H+1}=0,$$

and $V^\star_h(x)=\max_aQ^\star_h(x,a)$ is the optimal value, with $Q^\star$ defined by the same recursion.

A feature map $\phi:\mathcal S\times\mathcal A\to\mathbb R^d$ with $\|\phi\|\le1$ makes the MDP $\zeta$-approximately linear (Assumption B) if for every step $h$ there are signed measures $\mu_h=(\mu_h^{(1)},\dots,\mu_h^{(d)})$ on $\mathcal S$ and a vector $\theta_h$ with

$$\big\|\mathbb P_h(\cdot\mid x,a)-\langle\phi(x,a),\mu_h(\cdot)\rangle\big\|_{\mathrm{TV}}\le\zeta,\qquad|r_h(x,a)-\langle\phi(x,a),\theta_h\rangle|\le\zeta$$

for all $(x,a)$, together with the normalization $\|\theta_h\|\le\sqrt d$ and a $\sqrt d$ bound on the masses of $\mu_h$. At $\zeta=0$ this is a linear MDP.

LSVI-UCB (Algorithm 1) plays $K$ episodes. In episode $k$, with data $\phi^\tau_h=\phi(x^\tau_h,a^\tau_h)$ from earlier episodes, it computes backwards from $Q^k_{H+1}\equiv0$

$$\Lambda^k_h=\sum_{\tau<k}\phi^\tau_h(\phi^\tau_h)^\top+\lambda I,\qquad w^k_h=(\Lambda^k_h)^{-1}\sum_{\tau<k}\phi^\tau_h\big[r_h(x^\tau_h,a^\tau_h)+\max_aQ^k_{h+1}(x^\tau_{h+1},a)\big],$$ $$Q^k_h(x,a)=\min\big\{\langle w^k_h,\phi(x,a)\rangle+\beta_k\|\phi(x,a)\|_{(\Lambda^k_h)^{-1}},\,H\big\},$$

and then acts greedily, $a^k_h=\arg\max_aQ^k_h(x^k_h,a)$. An adversary may choose each initial state $x^k_1$. The regret after $K$ episodes is

$$\mathrm{Regret}(K)=\sum_{k=1}^K\big[V^\star_1(x^k_1)-V^{\pi_k}_1(x^k_1)\big],$$

where $\pi_k$ is the greedy policy of episode $k$. Throughout, $T=KH$ and $\iota=\log(2dT/p)$.

Formalization targets

Goal: Theorem 3.2

There are absolute constants $c,C>0$ such that for every $\zeta$-approximately linear MDP, every $p\in(0,1)$ and every run of LSVI-UCB with $\lambda=1$ and $\beta_k=c\,(d\sqrt\iota+\zeta\sqrt{kd})H$, with probability at least $1-p$,

$$\mathrm{Regret}(K)\le C\Big(\sqrt{d^3H^3T\iota^2}+\zeta dHT\sqrt\iota\Big).$$

The constants are not fixed numerically, so improvements of the constants in the proof do not invalidate the target.

Milestones

The milestones follow Appendix C: the approximate linearity of $Q^\pi$ (Lemma C.1) and the bound on its weights (Lemma C.2); the trace inequality D.1 and the adversarial-noise bound C.4; the self-normalized concentration bound D.3 (published) and the concentration event of Lemma C.3; the key estimate C.5; approximate optimism C.6; the recursive formula C.7; and the elliptical potential lemma D.2 (published) with the bonus-sum bound (21)–(24).

Significance

Theorem 3.2 shows that the regret of LSVI-UCB degrades gracefully under misspecification: the extra cost is of order $\zeta dHT\sqrt\iota$, linear in $T$ because of the bias of linear approximation and negligible when $\zeta\lesssim1/\sqrt T$. The paper also converts it into a PAC guarantee with an additive $\tilde O(\zeta dH^2)$ error. It is a reference point for later work on misspecified linear bandits and RL, which asks how far the linear term can be improved.

The result is proved on paper; no machine-checked proof is known. The formalization supplies an episodic MDP on a general measurable state space, LSVI-UCB as a function of the observed data, and its interaction with an adaptive adversary on a filtered probability space. These are shared with the companion mission on Theorem 3.1 and are reusable for other optimistic algorithms with linear function approximation. At $\zeta=0$ the goal specializes to Theorem 3.1 under the same normalization; this is a consistency check, not a dependency.

Difficulty

The central difficulty is that the regression targets $r_h+V^k_{h+1}(x^\tau_{h+1})$ depend on the data through $V^k_{h+1}$, which is computed from all earlier episodes. A martingale concentration bound for a fixed function does not apply. Lemma C.3 needs a bound that holds uniformly over the class of functions LSVI-UCB can produce, which requires a covering-number argument whose size depends on $\beta_k$; that is why the constant $C$ must be independent of $c_\beta$ and $c_\beta$ is chosen afterwards. Under misspecification a second error appears: the deviations $r_h-\langle\phi,\theta_h\rangle$ and $(\mathbb P_h-\langle\phi,\mu_h\rangle)V$ are not mean-zero and can be adversarial, so they cannot be concentrated away. Lemma C.4 absorbs them into the bonus at the price of the $\zeta\sqrt{kd}$ term in $\beta_k$. Optimism then holds only up to an error that accumulates over the horizon (Lemma C.6).

Formalization scope

• Indices are 1-based, as on the page; values and estimates are $0$ outside $1\le h\le H$.
• Values: $V^\pi$ and $V^\star$ are defined by the Bellman recursions (1) and (2), not by $\sup_\pi$.
• Measurability: the state space is a bare measurable space. Features $\phi(\cdot,a)$ are assumed measurable, and lemmas about a policy $\pi$ assume it measurable, so that every integral is meaningful.
• Actions: $\mathcal A$ is finite and nonempty. Argmax ties are broken towards the least action of a fixed linear order on $\mathcal A$.
• Interaction: the run is a process adapted to an arbitrary filtration, with actions given by Algorithm 1 and the next-state law holding conditionally on the past. The initial states are only required to be adapted.
• Probability statements: "with probability $1-p$" is "the bad set has (outer) measure at most $p$".
• Constants: $c$ and $C$ are quantified before all types, dimensions, horizons, $\zeta$, $p$ and runs. The hypotheses $d,H,K\ge1$ and $0\le\zeta\le1$ are stated.
• Assumption B measures the TV distance by the total variation norm $|\nu|(\mathcal S)$. The page's normalization $\|\mu_h(\mathcal S)\|\le\sqrt d$ is replaced by the same bound on the vector of total variations $(|\mu_h^{(i)}|(\mathcal S))_i$, because Lemma C.2 is false under the printed form; the replacement implies the printed condition and holds for tabular MDPs.
• Lemma C.7 carries the $+4H\zeta$ term that its own proof derives; the printed statement omits it. Theorem 3.2 is unaffected.

Lemmas C.3 and C.5 are formalized as printed. Their proofs use $\sup_x|V^k_{h+1}(x)|\le H$, which Algorithm 1 does not enforce from below; a solver may find that one of them needs an additional argument.

A formalization in which the goal assumes the event $\mathfrak E$, the optimism of Lemma C.6 or the recursion of Lemma C.7, or in which the run does not fix the actions to Algorithm 1's, would be trivial or false; the goal assumes none of these. Contributions are welcome on the linear-algebra lemmas (D.1, C.4, (21)–(24)), on measurability of the LSVI-UCB estimates, and on the covering argument behind Lemma C.3.

Selected references

• C. Jin, Z. Yang, Z. Wang, M. I. Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020; arXiv:1907.05388v2, 2019. https://arxiv.org/abs/1907.05388
• Y. Abbasi-Yadkori, D. Pál, C. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
• L. F. Yang, M. Wang, Sample-Optimal Parametric Q-Learning Using Linearly Additive Features, ICML 2019; arXiv:1902.04779. https://arxiv.org/abs/1902.04779

Motivation

Value iteration solves a Markov decision process by repeatedly applying the Bellman backup to a table of state values. When the state space is too large for a table, the values are stored in a function approximator instead: each backup is followed by a fit, and the fitted function is backed up again. This approximate value iteration is the basis of fitted dynamic programming and of much of reinforcement learning, and it was known in the early 1990s to diverge for common approximators such as linear regression and neural networks (Boyan and Moore, 1995, cited in the report as [BM95]).

Gordon's technical report (Stable Function Approximation in Dynamic Programming, CMU-CS-95-103, 1995; conference version at ICML 1995) identified a class of approximators, the averagers (k-nearest-neighbour, kernel averaging, linear and bilinear interpolation on a grid), for which the combination is stable. For discounted problems stability follows from a norm argument. For nondiscounted problems, where the backup contracts only in a weighted norm, that argument fails, and the report proves convergence by a different route: approximate value iteration is exact value iteration on a derived MDP. This mission formalizes that route and its conclusion, Corollary 4.1 (p. 11).

Setting

A finite nondiscounted Markov decision process $M$ has non-goal states $x=1,\dots,n$, a finite nonempty action set $U(x)$ at each state, an expected one-step cost $c_{xa}$, and transition probabilities $p_{axy}\ge 0$ with $\sum_y p_{axy}\le 1$. The missing mass $1-\sum_y p_{axy}$ is the probability of moving to a cost-free absorbing goal state, which the paper calls state $1$. A value function is a vector $V\in\mathbb R^n$; the goal's value is $0$. The parallel value backup is

$$(T_M V)(x)=\min_{a\in U(x)}\Bigl[c_{xa}+\sum_y p_{axy}V(y)\Bigr],$$

and with a discount factor $\gamma$ the sum is multiplied by $\gamma$. A policy $\mu$ chooses an admissible action at each state; it is proper if, from every starting state, the probability of having reached the goal after $t$ steps tends to $1$.

An averager $A$ consists of constants $k_y$, nonnegative weights $\beta_y$ and nonnegative weights $\beta_{yz}$ ($z$ ranging over all states, the goal included) with $\beta_y+\sum_z\beta_{yz}=1$. Its mapping is $M_A(V)(y)=\beta_yk_y+\sum_z\beta_{yz}V(z)$. Two operators $M_F$ and $T$ are compatible if $(M_F\circ T)^k(V_0)$ converges from every initial guess $V_0$.

The derived MDP $M'$ has the same states and actions, transition probabilities $p'_{axz}=\sum_y p_{axy}\beta_{yz}$ to non-goal states $z$, the rest of the mass going to the goal, and costs $c'_{xa}=c_{xa}+\gamma\sum_{y}p_{axy}\beta_yk_y$.

The states are layered by distance from the goal: $S_1=\{1\}$, $U_k=\bigcup_{j<k}S_j$, and $S_k$ is the set of states outside $U_k$ from which every action reaches $U_k$ with positive probability. Write $k(x)$ for the index of the layer containing $x$. The averager is self-weighted for $M$ if for every state $y$ either $\beta_y>0$ or $\beta_{yx}>0$ for some state $x$ with $k(x)\le k(y)$.

Formalization targets

Goal: Corollary 4.1 (p. 11)

If every policy of $M$ is proper and $A$ is self-weighted for $M$, then for every initial guess $V_0$ both

$$(M_A\circ T_M)^k(V_0)\quad\text{and}\quad(T_M\circ M_A)^k(V_0)$$

converge as $k\to\infty$. The first is the page's "$T_M$ and $M_A$ are compatible", the second its "approximate value iteration … will converge".

Milestones

1. Theorem 4.1 (Derived MDP, p. 7): $T_{M'}=T_M\circ M_A$, for every discount factor and for the nondiscounted backup.
2. Exhaustiveness (p. 10, after [BT89]): if all policies of $M$ are proper, every state lies in some layer $S_k$.
3. $M'$ terminates (p. 10): if all policies of $M$ are proper and $A$ is self-weighted, there is $m>0$ such that under every policy of $M'$ and from every state the goal is reached within $m$ steps with positive probability; in particular every policy of $M'$ is proper.
4. Theorem 2.3 (p. 4), in its all-policies-terminate case: value iteration converges from any initial guess. This is the published, proved item BertsekasDP.ssp_main_theorem.

A further item, Theorem 6.1 (p. 12), says the limit is $V^*$ when the optimal value function is a fixed point of $M_A$, under self-weighting or under positive costs with $k\ge 0$.

Significance

The corollary gives a checkable, purely combinatorial condition on the approximator and the transition graph under which fitted value iteration on a stochastic shortest path problem cannot diverge. Weight decay ($\beta_y>0$ everywhere) and any averager that only ever averages a state's value with values no farther from the goal satisfy it. The derived-MDP identity, Theorem 4.1, is the tool the rest of the report builds on (§5, §6.1, Appendix A): it reduces questions about approximate dynamic programming with averagers (convergence, the limit's error, the online Q-learning variant) to questions about an ordinary MDP.

The results are proved in the report, in prose. They have no machine-checked version. The formal development needed here is a finite stochastic shortest path theory (proper policies, the layer partition, termination bounds) on top of the published model BertsekasSSPModel and the proved BertsekasDP.ssp_main_theorem.

Difficulty

The obvious argument fails. If all policies of $M$ are proper, $T_M$ contracts in some weighted max norm, and $M_A$ is a nonexpansion in the unweighted max norm, but $M_A$ can expand the weighted norm, so the composition need not contract. Figure 4 of the report gives a three-state chain and an averager, replacing $V(2)$ by $V(3)$, for which approximate value iteration diverges. The proof therefore has to go through $M'$ and show that self-weighting makes $M'$ terminate under every policy. That is a probabilistic statement about all, possibly nonstationary, policies of a new process, derived from a layer structure of the old one. Exhaustiveness of the layers itself needs a policy-construction argument.

Formalization scope

The MDP is the published BertsekasSSPModel n C: non-goal states Fin n, a finite action type C with admissible sets M.U i, costs M.g, and transition probabilities M.p whose deficit is the probability of termination. Gordon's state 1 is this implicit termination state: its value is $0$ by construction, and where the partition and the averager's goal weight need to name it, it is none : Option (Fin n). This realises the page's two "without loss of generality" steps (state 1 cost-free and absorbing; $\beta_1=1$, $k_1=0$). The nondiscounted backup is BertsekasSSPBellmanOp M, the discounted one BertsekasDiscountedBellmanOp M γ.

The averager acts on whole value functions over the state set. An approximator that fits only a sample $X_0$ of states is the special case $\beta_{yx}=0$ for $x\notin X_0$. "All policies proper" quantifies over stationary policies μ : Fin n → C with admissible actions, as on p. 3. Self-weightedness is stated through layer membership, which agrees with the page's $k(x)$ whenever the partition is exhaustive (milestone 2). Theorem 6.1 takes $V^*$ as a real fixed point of the backup; under either of its cases such a fixed point is unique and optimal. Convergence is in $\mathbb R^n$, which is the same as convergence in max norm.

The goal's hypotheses concern $M$ and $A$ only. A formalization that assumed properness of the derived MDP, dropped the "every action" quantifier in the layers (making the partition and self-weighting weaker notions), or dropped $k(x)\le k(y)$ (making every averager with a positive weight self-weighted) would be a different theorem.

Reusable beyond this mission: the layer partition and its exhaustiveness, and the termination bound for the derived model, are general finite stochastic shortest path facts. Contributions to any milestone are welcome, and so are proofs of the definitions-level lemmas they rely on.

Selected references

• G. J. Gordon, Stable Function Approximation in Dynamic Programming, Technical Report CMU-CS-95-103, Carnegie Mellon University, 1995. Conference version in Proceedings of the 12th International Conference on Machine Learning (ICML), 1995. https://doi.org/10.1016/B978-1-55860-377-6.50040-2
• D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. ([BT89] in the report.)
• D. P. Bertsekas and J. N. Tsitsiklis, An Analysis of Stochastic Shortest Path Problems, Mathematics of Operations Research 16(3), 1991. https://doi.org/10.1287/moor.16.3.580
• J. A. Boyan and A. W. Moore, Generalization in Reinforcement Learning: Safely Approximating the Value Function, Advances in Neural Information Processing Systems 7, Morgan Kaufmann, 1995. ([BM95] in the report.)

Motivation

Reinforcement learning in a changing environment has a difficulty that is absent from a fixed Markov decision process: transition data gathered earlier may describe a different system from the one the decision maker currently faces. A learning algorithm therefore estimates transitions from a recent window of observations. The estimate comes with a confidence region, a set of transition laws consistent with the data at a chosen statistical radius. In the general nonstationary setting studied by Cheung, Simchi-Levi and Zhu, their algorithm widens this region to ensure that it can contain a model whose states remain readily reachable. Such a model is needed for the paper's dynamic regret analysis. Section 7 isolates a structural condition under which widening is unnecessary: every destination is reachable from every state with a uniformly positive one-step probability under a suitable action. Cheung, Simchi-Levi and Zhu, §7.

This mission formalizes Proposition 4 of that paper, the precise claim that the original, unwidened transition region contains a model with a controlled diameter. It is one of three separate missions for the paper. The result supports the paper's no-widening variant of its learning algorithm; it is not a claim that every model in the confidence region has small diameter. Cheung, Simchi-Levi and Zhu, Proposition 4.

Setting

There are finitely many states $\mathcal S$ and, for each state $s$, a nonempty finite set $\mathcal A_s$ of permitted actions. At each time $t\in[T]$, the system has a reward $r_t(s,a)\in[0,1]$ and a probability distribution $p_t(\cdot\mid s,a)$ for the next state. The distribution may change with $t$. A trajectory records the observed state $s_q$, chosen action $a_q$, and successor state $s_{q+1}$ at each time $q$. These are the model primitives in §2.2. Cheung, Simchi-Levi and Zhu, pp. 6–7.

An episode begins at $\tau(m)$ and uses a window of length $W$. At time $t$ in that episode, $N_t(s,a)$ counts how often the pair $(s,a)$ appears between $(\tau(m)-W)\vee1$ and $t-1$; $N_t^+(s,a)=\max\{1,N_t(s,a)\}$. The empirical row $\hat p_t(\cdot\mid s,a)$ counts observed successors and divides by $N_t^+(s,a)$. The corresponding average true row $\bar p_t$ averages the time-varying transition probabilities over the same visits. Both are zero vectors when there are no visits. Cheung, Simchi-Levi and Zhu, equations (3) and (5).

Write $SA=\sum_s|\mathcal A_s|$, so this is the number of allowed state-action pairs. At confidence level $\delta$, the transition radius is $\operatorname{rad}_{p,t}(s,a)=2\sqrt{2S\log(SAT/\delta)/N_t^+(s,a)}$. The region $H_{p,t}(s,a;\eta)$ consists of probability vectors within $\ell_1$ distance $\operatorname{rad}_{p,t}(s,a)+\eta$ of $\hat p_t$. Here $\eta=0$ means no widening. The estimation event $E_p$ bounds the $\ell_1$ distance between $\bar p_t$ and $\hat p_t$ by that radius for each allowed pair. Cheung, Simchi-Levi and Zhu, pp. 12, 14.

For a stationary transition model and policy $\pi$, the hitting time $\Lambda(s'\mid\pi,s)$ counts transitions until the first arrival at $s'$ after starting at $s$. This includes the first return time when $s=s'$. Its diameter is $D=\max_{s,s'}\min_\pi\mathbb E[\Lambda(s'\mid\pi,s)]$. Infinite expectations are possible in the definition. Cheung, Simchi-Levi and Zhu, Definition 1.

Formalization targets

Goal: Proposition 4

Assumption 2 supplies $\zeta>0$ and an allowed action $a_{(s,s')}$ for every ordered pair of states, fixed across time, such that $p_t(s'\mid s,a_{(s,s')})\ge\zeta$ for all $t\in[T]$. Conditional on $E_p$, Proposition 4 says that for every time in the horizon there exists a transition model $p$ whose every allowed row belongs to $H_{p,t}(s,a;0)$ and whose diameter obeys

$$D(\mathcal S,\mathcal A,p)\le\bar D:=\frac1\zeta.$$

The target is existential: the region need only contain one such model at each time. The milestone list follows the two cases in the proof of Lemma 13, the lemma's model existence claim, and the expected hitting-time bound in the proof of Proposition 4. Cheung, Simchi-Levi and Zhu, pp. 21, 49–50.

Significance

Proposition 4 identifies a condition under which the algorithm can use $\eta=0$ while retaining a uniform diameter guarantee for at least one plausible transition model. The paper uses this to analyze a no-widening version of its dynamic regret bound, and later applies that viewpoint to inventory control. Without a bounded-diameter model in the region, the diameter-dependent regret argument does not apply in the same form. Cheung, Simchi-Levi and Zhu, §7.

The proposition and its appendix proof are known results of the paper. This mission asks for a machine-checked account of the exact confidence region, its pathwise estimation event, Lemma 13, and the diameter claim. A general finite MDP with probability-valued transition rows is already available as the published FiniteMDPLearning definition; the paper-specific window estimators and its return-time diameter still need formal proofs. The paper's headline Theorems 1–4 are not posed here because their displayed bounds hide constants in $\widetilde O(\cdot)$ notation. Cheung, Simchi-Levi and Zhu, p. 6 and Theorems 1–4.

Difficulty

The obvious idea that the true transition law belongs to the confidence region can fail under drift: the region is centered on recent observations, while the law at the current time may differ from the laws that generated those observations. Even the average true row has a special case. At an unvisited pair, equation (5) sets it to the zero vector, which is not a probability distribution and therefore is not a member of the simplex-valued confidence region. The existence claim must cover visited and unvisited pairs while preserving one-step reachability for all targets under a single transition law. Cheung, Simchi-Levi and Zhu, pp. 12, 49–50.

The diameter also uses the paper's first-arrival-after-start convention. A library travel time that is zero when source equals target misses the return-time cases and would weaken the stated conclusion. Cheung, Simchi-Levi and Zhu, Definition 1.

Formalization scope

States and actions are Fin S and Fin A; permitted actions are state-dependent finite sets. Extra MDP rows for disallowed actions are never consulted. The finite MDP type supplies valid probability rows and bounded rewards. Hitting times and the diameter use extended nonnegative reals, so infinite values are represented without a default real value. The diameter ranges over allowed deterministic stationary policies and over all ordered state pairs, including equal pairs. Time is zero-based in Lean: paper time $t\in[T]$ is index $t-1<T$, and the paper's window becomes the half-open interval [τm-W,t). The paper's $N^+$ is at least one, so its estimators never divide by zero. A result at arbitrary $t$ with $\tau_m\le t<T$ covers every episode time without assuming any additional episode schedule property.

The Lean statement makes two domain conditions explicit: $S>1$ and $0<\delta<1$. These ensure the paper's claim that the radius at an unvisited pair is at least one; it can fail when $S=1$ and the confidence level is close to one. Assumption 2 is required for every time in the horizon, with $\zeta>0$. The event $E_p$ is the $\ell_1$ estimation inequality at the selected time. The paper writes it as membership of $\bar p_t$ in a simplex-valued region for every pair, but that literal wording is false at an unvisited pair because $\bar p_t=0$ there. At visited pairs, the inequality and membership agree. This convention is disclosed in the definition item and keeps the theorem meaningful on ordinary early trajectories.

The region is centered at the exact empirical $\hat p_t$, uses $\eta=0$, and constrains every allowed row of the constructed model. The diameter uses its full extended-real value, and $\zeta$ is strictly positive; dropping any of these clauses would change the claim. Reusable contributions include finite-state hitting-time estimates and windowed transition estimation identities. Proofs of the four milestones and the goal, as well as small lemmas connecting the published MDP measure to successive transition rows, are welcome.

Selected references

• W. C. Cheung, D. Simchi-Levi and R. Zhu, Non-Stationary Reinforcement Learning: The Blessing of (More) Optimism, arXiv:1906.02922v4, 2020; published as Nonstationary Reinforcement Learning: The Blessing of (More) Optimism, Management Science, 2023. arXiv
• T. Jaksch, R. Ortner and P. Auer, Near-optimal Regret Bounds for Reinforcement Learning, Journal of Machine Learning Research 11, 2010. JMLR

Why changing environments matter

A reinforcement-learning agent chooses actions while learning how those actions affect future states. In a stationary model, observations collected long ago remain relevant to the current transition law. In a nonstationary Markov decision process, rewards and transition probabilities may change at each round. Old observations can then bias an estimate even when the agent has collected many samples. The challenge is to keep learning from recent observations without becoming blind to actions that the agent has not tried recently. Cheung, Simchi-Levi and Zhu study this tension for finite-state average-reward learning and introduce confidence widening in their SWUCRL2-CW algorithm Cheung et al., §4.

The paper's broad regret theorems suppress constants inside asymptotic notation. Proposition 2 gives an explicit one-round inequality that exposes the roles of estimation error, temporal variation, confidence widening, and the diameter of a plausible transition model. This mission targets that proposition and the stated auxiliary results used around it Cheung et al., pp. 14, 38–41.

The finite changing MDP

Let $\mathcal S$ be a finite state set. Each state $s$ has a nonempty finite set $\mathcal A_s$ of permitted actions. At round $t$, taking action $a\in\mathcal A_s$ in state $s$ gives expected reward $r_t(s,a)\in[0,1]$ and moves to state $s'$ with probability $p_t(s'\mid s,a)$. The one-step variation $B_{r,t}$ is the greatest change $|r_{t+1}(s,a)-r_t(s,a)|$ over permitted pairs; $B_{p,t}$ is the corresponding greatest $\ell_1$ distance between transition rows. These definitions make no stationarity assumption Cheung et al., pp. 6, 33.

At the start $\tau(m)$ of an episode, the algorithm counts visits to each pair in a recent window of length $W$. It divides empirical sums by $N^+=\max\{1,N\}$, where $N$ is the visit count. Thus an unvisited pair has estimated reward and transition vector equal to zero. Reward confidence sets lie in $[0,1]$; transition confidence sets lie in the probability simplex and use an $\ell_1$ radius enlarged by a nonnegative parameter $\eta$. Write $\operatorname{rad}_{r,\tau(m)}(s,a)$ and $\operatorname{rad}_{p,\tau(m)}(s,a)$ for their respective radii. The algorithm chooses a stationary policy $\tilde\pi_{\tau(m)}$ and an optimistic model, gain $\tilde\rho_{\tau(m)}$, and bias $\tilde\gamma_{\tau(m)}$ from extended value iteration Cheung et al., pp. 11–13.

The diameter of a transition model is the largest, over ordered source and target states, of the smallest expected number of transitions needed to reach the target under a stationary policy. Source equal to target means a return time after at least one transition. The round-$t$ optimal gain $\rho_t^*$ is the value of the stationary occupancy-measure linear program for $(r_t,p_t)$ with only permitted actions. From the window's first round through the round before $t$, let $\operatorname{var}_{r,t}$ and $\operatorname{var}_{p,t}$ be the sums of the corresponding one-step variations Cheung et al., pp. 8, 14, 33.

Formalization targets

The main target is Proposition 2. Condition on the local reward and transition estimation events at $\tau(m)$. Assume that the widened transition confidence sets contain every permitted row of an MDP of diameter at most $D$. For a round in which $a_t=\tilde\pi_{\tau(m)}(s_t)$, the target is

$$\begin{aligned} \rho_t^*-r_t(s_t,a_t)\le{}&\sum_{s'}p_t(s'\mid s_t,a_t)\tilde\gamma_{\tau(m)}(s')-\tilde\gamma_{\tau(m)}(s_t)+\frac1{\sqrt{\tau(m)}}\\ &+2\operatorname{var}_{r,t}+4D(\operatorname{var}_{p,t}+\eta)\\ &+2\operatorname{rad}_{r,\tau(m)}(s_t,a_t)+4D\operatorname{rad}_{p,\tau(m)}(s_t,a_t). \end{aligned}$$

The five milestones are the paper's Lemmas 2–5 and displayed inequality (32): a dual-bias span bound, a drift estimate for window averages, bounded optimistic bias, optimism under drift, and a transition-value error bound. Their exact constants are part of the targets Cheung et al., pp. 33, 38–39.

What the result supplies

Proposition 2 separates the per-round change in optimal gain from the cost of the current action. Its first term tracks changes in the optimistic bias along transitions; the other terms identify window drift, reward and transition estimation, and widening. This decomposition can be summed across episodes when analyzing the algorithm. The result has a concrete role even though the later horizon-wide theorem is given in asymptotic notation Cheung et al., pp. 14, 41.

The paper proves these claims mathematically. The mission asks for machine-checked proofs of the explicit statements and for reusable definitions of finite nonstationary MDP variation, window estimators, confidence sets, occupancy gain, and hitting-time diameter. The source's Theorems 1–4 are not posed here: their displayed bounds hide constants in $\widetilde O(\cdot)$ and, in one case, use an unspecified $O(\delta)$ failure probability Cheung et al., pp. 14–25. This proposal supplies statements for solvers; it does not claim that these new statements already have machine-checked proofs.

Where the difficulty lies

The current model need not resemble the model that generated every observation in the window. A direct stationary confidence argument cannot control the resulting temporal error. The challenge is especially visible at a pair with no recent visits: its comparison transition vector is zero, although a genuine transition row has total mass one. The paper's Lemma 3, read literally for every pair, fails in that case. The mission states its positive-count condition explicitly while keeping the proposition and the later optimism and transition milestones valid at unvisited pairs Cheung et al., pp. 12, 38–40.

There is a separate issue with the printed dual-bias lemma. Feasibility alone permits an arbitrarily large dual gain and does not force the asserted $2D$ span bound. The mission adds $\rho\le2$ to Lemma 2 and records the change for audit. The EVI output is represented by its selected-model membership, bias normalization, optimism, and near-optimality properties; this is the contract stated for the algorithm's output, rather than a formal execution of extended value iteration Cheung et al., pp. 13, 33, 35–36.

Formalization scope

States and ambient actions are Fin S and Fin A; permitted actions are state-dependent finite subsets. The setup has $S>1$, $0<\delta<1$, $\eta\ge0$, and a nonempty action set at each state. Time is zero-based in Lean, while the paper's rounds are one-based; in particular its $1/\sqrt{\tau(m)}$ is represented by $1/\sqrt{\tau_m+1}$. Counts and confidence sets are evaluated at the episode start. Variations continue up to the target round. The estimation events are assumed at the episode start, which is the only time used by these statements.

Hitting times and diameter take values in extended nonnegative reals, so an unreachable target does not acquire a false finite diameter. The diameter includes return times and minimizes over deterministic stationary policies. The confidence-radius product $SA$ counts actual permitted pairs. At an unvisited pair, the comparison averages remain zero and $N^+=1$; the large confidence radii under the stated bounds are essential. The local transition event uses the $\ell_1$ error condition: literal membership of the zero comparison vector in a simplex would make the paper's event fail. The printed coordinatewise maxima in Property 1 imply the standard joint-distribution optimism condition used here. The free $(s,a)$ printed in the last radius of Proposition 2 means $(s_t,a_t)$, as the proof's context confirms Cheung et al., pp. 12, 14, 36, 40–41.

Two milestones carry a pinned hypothesis because the printed statement is false without it: Lemma 2 assumes the dual gain satisfies $\rho\le 2$ (an arbitrary feasible $\rho$ can make the bias span exceed $2D$), and Lemma 3 assumes the pair was visited in the episode-start window (at an unvisited pair the comparison averages are zero). Proposition 2 is stated for every round $t\ge\tau(m)$ before the horizon at which the action is the episode policy's choice, which covers the rounds of episode $m$; the coefficient $4D$ of $\eta$ is kept as printed.

The witness MDP has genuine probability rows in the widened sets and a diameter bound. The EVI tuple obeys both stated properties, and the chosen action obeys its policy. These conditions prevent an unconstrained bias, a spurious zero diameter, a confidence event at the wrong time, or a reward bound for an unrelated action. The published FiniteMDPLearning model supplies probability rows and rewards in $[0,1]$; its different travel-time convention is not substituted for the paper's diameter. Contributions to the MDP linear program, finite-state hitting times, window-average inequalities, and confidence-region geometry are all useful beyond this mission.

Selected references

• W. C. Cheung, D. Simchi-Levi and R. Zhu, Non-Stationary Reinforcement Learning: The Blessing of (More) Optimism, arXiv:1906.02922v4, 2020; published as Nonstationary Reinforcement Learning: The Blessing of (More) Optimism, Management Science, 2023. Preprint; journal DOI.
• T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, Journal of Machine Learning Research 11, 2010. Article.

Motivation

Reinforcement learning in a changing environment needs a benchmark that remains meaningful when the transition law and rewards vary from round to round. For a stationary Markov decision process (MDP), the optimal long-run average reward is a standard benchmark. In a nonstationary MDP, summing those stationary optima across rounds is convenient, but it need not equal the best expected reward achievable over the whole horizon: today's action changes tomorrow's state. Cheung, Simchi-Levi and Zhu use Proposition 1 to quantify this gap in their analysis of nonstationary reinforcement learning (preprint, pp. 7–8). This mission formalizes that proposition and the explicit estimates in its proof.

The paper develops algorithms for MDPs with drifting rewards and transitions. Its oracle comparison is useful before any algorithm is chosen: it relates a sum of local, stationary benchmarks to the reward of every non-anticipatory policy, including policies that adapt to the observed trajectory. This separates a property of the environment from the performance of a learning rule. The paper was published in Management Science in 2023; this mission follows the numbered statements and pages of the authors' pinned arXiv preprint (Cheung et al., 2020, pp. 6–8).

Setting

A finite nonstationary MDP has a finite state set $\mathcal S$, a nonempty available-action set $\mathcal A_s$ at each state $s$, and a horizon of $T$ rounds. At round $t$, taking action $a\in\mathcal A_s$ in state $s$ gives a stochastic reward with mean $r_t(s,a)\in[0,1]$ and moves to a new state according to the probability distribution $p_t(\cdot\mid s,a)$. A non-anticipatory policy selects an allowed action using the current state and observations from previous rounds. The target concerns expected sums of the mean rewards, so the distributional shape of the reward noise does not enter its formula (preprint, §2.2, pp. 6–7).

The one-step reward variation $B_{r,t}$ is the largest value of $|r_{t+1}(s,a)-r_t(s,a)|$ over allowed state–action pairs. The transition variation $B_{p,t}$ is the largest $\ell_1$ distance between the corresponding transition distributions. Their variation budgets are $B_r=\sum_{t=1}^{T-1}B_{r,t}$ and $B_p=\sum_{t=1}^{T-1}B_{p,t}$, exactly as in equation (1). The budgets are computed from the MDP sequence; they are not independent inputs to the theorem (preprint, p. 6, (1)).

For the stationary MDP at round $t$, $\rho_t^*$ is its optimal long-run average reward. The mission represents it as the optimum of the paper's occupancy linear program (15), whose variables are nonnegative state–action occupancies, satisfy flow balance, and sum to one. A diameter $D_t$ bounds the least expected hitting time between any two states under an allowed stationary policy. The paper's Definition 1 includes equal initial and target states, so this includes a return time. Assumption 1 requires a finite diameter at every round; $D_{\max}$ is a common bound on those diameters (preprint, pp. 7–8, Definition 1 and Assumption 1; p. 33, (15)).

Formalization targets

Proposition 1: the oracle gap

Write $B=B_r+2D_{\max}B_p$. For $0<B\le T$ and the necessary small-budget condition $BT\ge1$, the target is

$$\sum_{t=1}^{T}\rho_t^*\ge \mathbb E^{\Pi}\!\left[\sum_{t=1}^{T}r_t(s_t,a_t)\right] -4(D_{\max}+1)\sqrt{BT}$$

for every initial state and every allowed non-anticipatory policy $\Pi$. Quantifying over every policy expresses the paper's maximum over policies without introducing a supremum over an unbounded real-valued function space. The first five targets follow Appendix A.2: a bounded optimal dual potential, the gain-drift inequality (18), the pathwise dual inequality (19), the window inequality (23), and the full-horizon inequality (24). Their constants and index ranges are part of the targets (preprint, pp. 8, 33–34).

Significance

The result gives a finite-horizon comparison between two different benchmarks. The sum of stationary gains is additive over time, while the best expected cumulative reward accounts for how actions alter later states. Proposition 1 says that their difference is controlled by variation and diameter under its hypotheses. This is the paper's justification for using the additive oracle in its dynamic-regret definition; the authors note that the later algorithmic bounds are larger than this comparison term (preprint, p. 8, text after Proposition 1).

The mathematical result is already claimed in the paper. This mission asks for a machine-checked version with explicit finite-horizon distributions, the occupancy LP, the diameter convention, and the drift sums. The new Lean statements currently have placeholders for their proofs; the imported finite-MDP definitions are already published. A completed development would provide reusable code for time-dependent MDP trajectory laws and for comparing stationary LP values as a model drifts. It would also make the precise domain of the square-root bound reviewable independently of the algorithms in the remainder of the paper.

Difficulty

The stationary gain $\rho_t^*$ is not a per-round reward guarantee. An action can collect reward now and put the process in a state whose future reward is poor, so summing stationary optima does not directly bound a nonstationary trajectory. Conversely, treating each round as an independent stationary experiment discards the state dependence that the policy exploits. The diameter controls the cost of that dependence, and variation controls changes between the stationary problems. The proof must connect these objects while preserving the exact factors $2D_{\max}$, $2W$, and $4TD_{\max}/W$ in Appendix A.2 (preprint, pp. 33–35).

There is also a small-budget obstruction in the printed Proposition 1. Its stated $0<B\le T$ permits $BT<1$, where the displayed inequality is false: a two-state, one-action example with a slowly returning state, $T=2$, and reward drift $10^{-12}$ has an oracle sum near $2/11$ while the proposed lower bound on that sum is near $1$. The mission therefore adds $BT\ge1$ and records the difference from the page. Inequality (24), posed separately, retains the paper's every-integer-window form and needs no such pin.

Formalization scope

States and actions are Fin S and Fin A; available actions form a nonempty Finset at each state, and $S>0$. The imported FiniteMDPLearning structure supplies reward rows in $[0,1]$ and transition probability rows. It has rows for actions unavailable at a particular state; all mathematical maxima, LP constraints, policy restrictions, and drift formulas use only allowed pairs. The source's time $t\in\{1,\ldots,T\}$ is stored at Lean index $t-1$. No value of the MDP sequence after the horizon enters a stated budget or reward sum.

The occupancy LP has a nonempty bounded feasible-value set under the standing MDP assumptions; its real supremum denotes $\rho^*$. Hitting times and diameters use extended nonnegative reals to retain infinity, rather than silently converting an infinite hitting time to zero. The diameter includes same-state return times and minimizes over deterministic stationary policies; such policies attain the hitting-time minimum. The policy used for cumulative reward is a history-dependent randomized kernel on state–action histories. Conditioning an action rule that also observes past rewards on that history yields the same state–action trajectory law. The nonstationary measure samples the next state with the current round's transition law and is a probability measure.

The fixed $D_{\max}$ is constrained to bound every round's diameter; it is not an unrelated parameter. The stated $BT\ge1$ pin rules out the false small-budget case. In (23), the paper's last-window drift sum includes $B_{\cdot,T}$, which equation (1) does not define; the formal sum retains all defined terms through $T-1$. The goal and milestones do not weaken $\rho_t^*$, restrict the policy class to a convenient subclass, or omit a time step. Contributions on LP duality, finite-horizon trajectory expectations, hitting-time bounds, and drift inequalities are useful beyond this proposition. The paper's headline Theorems 1–4 are not posed here because their $\widetilde O$ notation hides constants (preprint, p. 6, §2.1).

Selected references

• W. C. Cheung, D. Simchi-Levi and R. Zhu, Non-Stationary Reinforcement Learning: The Blessing of (More) Optimism, arXiv:1906.02922v4, 2020; published as Nonstationary Reinforcement Learning: The Blessing of (More) Optimism, Management Science, 2023. Preprint; published article.
• T. Jaksch, R. Ortner and P. Auer, Near-Optimal Regret Bounds for Reinforcement Learning, Journal of Machine Learning Research 11, 2010. Article. The source paper cites its diameter and bias-span results in Definition 1 and Appendix A.1.
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. Book. The source paper cites it for the average-reward occupancy LP on p. 33.

Motivation

Regret bounds for reinforcement learning in a single, non-episodic Markov decision process (MDP) are stated in terms of the diameter $D$ of the MDP: the worst expected time needed to travel between two states when the travel policy is chosen well. UCRL2 (Jaksch, Ortner and Auer, 2010) achieves regret $\tilde O(DS\sqrt{AT})$, against a lower bound of $\Omega(\sqrt{DSAT})$, by planning in an extended MDP, whose action set lets the planner also pick a transition law from a confidence set. Posterior-sampling methods replace the confidence set with random samples from a posterior. Agrawal and Jia (arXiv:1705.07041v3, published in Mathematics of Operations Research, 2023) show that such a method attains a high-probability worst-case regret bound of $\tilde O(DS\sqrt{AT})$ for every communicating MDP (their Theorem 1).

Their analysis plans in an extended MDP built from finitely many sampled transition vectors. Optimal-gain policies of that MDP are only useful if it is itself communicating with a diameter comparable to $D$, so the paper needs a deterministic statement: if every state-action pair has a sample that is optimistic about travel times, the diameter of the extended MDP is at most $D/(1-\delta)$. This mission formalizes that statement, Lemma 5.6 of the paper (p. 12), together with three claims from its proof.

Setting

A finite MDP $\mathcal M$ has a finite state set $\mathcal S$ of size $S$, a finite action set $\mathcal A$ of size $A$, a probability vector $P_{s,a}\in\Delta^{S}$ for each state $s$ and action $a$, and rewards $r_{s,a}\in[0,1]$. A deterministic policy is a map $\pi:\mathcal S\to\mathcal A$; under $\pi$ the state process is the Markov chain with transition rows $P_{s,\pi(s)}$.

For states $s'$ and $s$, $T^{\pi}_{s'\to s}\in[0,\infty]$ is the expected number of steps to reach $s$ when starting at $s'$ and following $\pi$. It is $0$ when $s'=s$. The diameter is

$$D(\mathcal M)=\max_{s\neq s'}\ \min_{\pi:\mathcal S\to\mathcal A} T^{\pi}_{s\to s'},$$

and $\mathcal M$ is communicating when $D(\mathcal M)<\infty$ (Definitions 1–3, p. 3). For a target $s$, the vector $E^{s}$ collects the minimum expected times, $E^{s}_{s'}=\min_{\pi}T^{\pi}_{s'\to s}$, so $E^{s}_{s}=0$.

The extended MDP (§3, p. 5) starts from $\psi$ probability vectors $Q^{1}_{s,a},\dots,Q^{\psi}_{s,a}$ for every pair $(s,a)$. In the algorithm these are posterior samples, but here they are arbitrary. The extended MDP $\tilde{\mathcal M}$ has the same states and, for every action $a$, the actions $a^{1},\dots,a^{\psi}$. Taking $a^{j}$ in $s$ gives reward $r_{s,a}$, and the next state is drawn from $Q^{j}_{s,a}$. Its diameter $D(\tilde{\mathcal M})$ is defined as above, minimizing over policies $\tilde\pi:\mathcal S\to\{a^{j}\}$.

Formalization targets

Goal: Lemma 5.6

Let $\delta\in[0,1)$. Suppose that for every target state $s$, every state $s'$ and every action $a$ there is a sample index $j$ with

$$Q^{j}_{s',a}\cdot E^{s}\ \le\ P_{s',a}\cdot E^{s}+\delta. \tag{16}$$

Then

$$D(\tilde{\mathcal M})\ \le\ \frac{D(\mathcal M)}{1-\delta}.$$

Milestones (claims of the proof, p. 13)

1. In a communicating MDP with at least one action, for every target $s_2$ there is one deterministic policy $\pi$ with $T^{\pi}_{s'\to s_2}=E^{s_2}_{s'}$ for every $s'$.
2. First-step analysis: for every policy $\pi$ and $s\neq s_2$,

$$T^{\pi}_{s\to s_2}=1+\sum_{s'\neq s_2}P_{s,\pi(s)}(s')\,T^{\pi}_{s'\to s_2}.$$

3. Comparison (display (17)): if $E\in[0,\infty]^{\mathcal S}$ satisfies $1+\sum_{s'\neq s_2}Q_{s,\tilde\pi(s)}(s')E_{s'}\le E_s+\delta$ for all $s\neq s_2$, then $(1-\delta)\,T^{\tilde\pi}_{s\to s_2}\le E_s$ for all $s\neq s_2$.

Significance

The result. Lemma 5.6 turns a per-pair, one-sided condition on samples into a global bound on the diameter. Agrawal and Jia combine it with their Lemma 5.7, which shows that (16) holds with $\delta\le 1/2$ with high probability for their posterior samples. Together these give $D(\tilde{\mathcal M}^{k})\le 2D$ in every epoch, which is what lets the bias span of the sampled MDP enter their regret analysis. The lemma is deterministic and makes no use of how the samples were drawn, so it applies to any optimistic-sampling or perturbation scheme that produces vectors satisfying (16).

Formalizing it. The lemma is proved in the paper; no machine-checked version exists. The paper's proof assumes that every sampled entry is strictly positive ("drawn from Dirichlet distribution") so that the absorbing chain and its fundamental matrix are well defined. That assumption fails for the simple optimistic samples of the same algorithm, which can have zero entries. The statements here drop it, so a formal proof also settles the general case. Milestones 1 and 2 are standard facts about minimum expected hitting times (stochastic shortest paths) that the platform's finite-MDP library does not yet contain. They are reusable for any diameter-based regret analysis.

The main regret bound (Theorem 1) is not posed. Its constants are hidden in $O(\cdot)$, and the algorithm's parameters are given only up to $\Theta(\cdot)$.

Difficulty

The paper's argument inverts $I-Q^{\dagger}_{\tilde\pi}$ and uses the nonnegativity of the fundamental matrix of an absorbing chain. Without positive entries the policy $\tilde\pi$ can have closed classes that avoid the target, so $I-Q^{\dagger}_{\tilde\pi}$ can be singular and the matrix argument does not apply as written. The comparison has to be made with expected travel times that may be infinite.

A second obstacle is that (16) constrains only the minimizing vectors $E^{s}$ of the true MDP. The bound therefore needs a policy of $\mathcal M$ whose travel times equal $E^{s_2}$ from every state at once, not merely from the starting state $s_1$. The existence of such a uniformly optimal deterministic policy is not immediate from the definition of the diameter, which minimizes separately for each pair of states.

Finally, the platform's expected travel time is defined through finite-horizon trajectory laws, so first-step analysis is a Markov-property computation on those measures. It does not follow from the definition by unfolding alone.

Formalization scope

• Library. The mission reuses the published definitions FiniteMDPLearning (namespace BanditAlgorithm): FiniteMDP S A, mdpTravelTime M f src tgt (the expected hitting time minus one, valued in $[0,\infty]$, equal to $T^{f}_{src\to tgt}$), and mdpDiameterENN M (Definition 2 verbatim, valued in $[0,\infty]$). The mission's own definitions file adds extendedMDP, extendedAction and minTravel (the vector $E^{s}$).
• Indexing. States, actions and samples are 0-based (Fin S, Fin A, Fin ψ). The action $a^{j}$ of the extended MDP is finProdFinEquiv (a, j) : Fin (A * ψ). The epoch index $k$ plays no role and is dropped.
• Extended values. Travel times, diameters, the vectors $E^{s}$ and the inner products $Q\cdot E^{s}$ are computed in $[0,\infty]$ with $0\cdot\infty=0$. The bound $D/(1-\delta)$ is division in $[0,\infty]$ by the positive real $1-\delta$, with $\delta\in[0,1)$ as δ : ℝ≥0, δ < 1.
• Quantifiers of (16). The printed (16) uses the letter $s$ both for the target of $E^{s}$ and for the state in $P_{s,a}$. The proof applies it at the current state with a different target, so the goal quantifies the target separately: for every target, state and action there is a sample.
• Pinned hypotheses. Milestone 1 assumes $D(\mathcal M)<\infty$ (the paper's "$\mathcal M$ has diameter $D$") and $A\ge1$. The goal assumes neither: if $D(\mathcal M)=\infty$ its bound is trivially true, so it generalizes the paper's statement. No statement assumes positivity of the sampled entries or any distribution of the samples.
• Ruled-out trivializations. An extended MDP whose transitions ignore $j$ or $Q$, an $E^{s}$ that is not the infimum over policies, a hypothesis comparing $Q$ and $P$ against different vectors, and a real-valued conclusion through a truncation with junk value $0$ for non-communicating MDPs would each make the goal vacuous or different. None is used.
• Useful existing result. The platform has the proved drift criterion BanditAlgorithm.mdp_travel_time_le_of_lyapunov_drift (a real-valued nonnegative $V$ with $\sum_{s'}P_{s,f(s)}(s')V(s')+1\le V(s)$ off the target bounds the travel time by $V$), which covers the case $\delta=0$ of milestone 3 for finite $E$.
• Welcome contributions. Proofs of the three milestones and of the goal; a general first-step (Markov property) lemma for mdpMeasure; an existence theorem for uniformly optimal deterministic policies of minimum expected hitting time.

Selected references

• S. Agrawal and R. Jia, Posterior sampling for reinforcement learning: worst-case regret bounds, arXiv:1705.07041v3, 2020; published as Optimistic posterior sampling for reinforcement learning: worst-case regret bounds, Mathematics of Operations Research, 2023. https://arxiv.org/abs/1705.07041
• T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/jaksch10a.html
• D. P. Bertsekas and J. N. Tsitsiklis, An analysis of stochastic shortest path problems, Mathematics of Operations Research 16(3), 1991. https://doi.org/10.1287/moor.16.3.580
• C. M. Grinstead and J. L. Snell, Introduction to Probability, American Mathematical Society, 2nd revised edition, 1997 (Chapter 11, absorbing Markov chains). https://math.dartmouth.edu/~prob/prob/prob.pdf
• T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020 (Chapter 38, MDPs and the diameter). https://tor-lattimore.com/downloads/book/book.pdf

Motivation

The Decision-Estimation Coefficient (DEC) of Foster, Kakade, Qian and Rakhlin (arXiv:2112.13487) is a single complexity measure that bounds the minimax regret of interactive decision making (bandits, reinforcement learning, and their structured variants) from above and from below. Its lower bound (Theorem 3.2 of the paper) states that every algorithm suffers expected regret at least a constant times $\mathsf{dec}_\gamma(\mathcal{M}^\infty_{\varepsilon_\gamma}(\overline{M}), \overline{M}) \cdot T$, so concrete lower bounds on regret follow from concrete lower bounds on the DEC of localized model classes.

The multi-armed bandit is the first test of this program. Its minimax regret $\Theta(\sqrt{AT})$ is classical (Auer et al., 2002; Audibert and Bubeck, 2010). Section 5.1 of the paper recovers it through the DEC: posterior sampling (Proposition 5.1) and inverse gap weighting (Proposition 5.2) bound the DEC by $A/\gamma$ from above, and Proposition 5.3 bounds it by $2^{-6} A/\gamma$ from below. The lower bound is proved through a hard family of models (Definition 5.1, Lemma 5.1), the device that the paper reuses for linear, ReLU and gap-dependent lower bounds in §§6–7.

Setting

A decision space $\Pi$ is a finite set; here $\Pi = [A] = \{1, \dots, A\}$, the arms. A model $M$ assigns to every arm $\pi$ a distribution $M(\pi)$ over rewards in $\mathcal{R} = [0,1]$ (observations are trivial). Its mean reward is $f^M(\pi) = \mathbb{E}_{r \sim M(\pi)}[r]$, and $\pi_M \in \arg\max_\pi f^M(\pi)$ is an optimal arm. The squared Hellinger distance between distributions $P, Q$ on a finite set is $D^2_{\mathrm{H}}(P, Q) = \sum_y (\sqrt{P(y)} - \sqrt{Q(y)})^2$ (no factor $\tfrac12$, the paper's (5)).

For a class $\mathcal{M}$ of models, a reference model $\overline{M}$ and $\gamma > 0$, the DEC (2) is

$$\mathsf{dec}_\gamma(\mathcal{M}, \overline{M}) = \inf_{p \in \Delta(\Pi)} \sup_{M \in \mathcal{M}} \mathbb{E}_{\pi \sim p}\Bigl[ f^M(\pi_M) - f^M(\pi) - \gamma \cdot D^2_{\mathrm{H}}\bigl(M(\pi), \overline{M}(\pi)\bigr) \Bigr].$$

With $g^M(\pi) = f^M(\pi_M) - f^M(\pi)$, the $L_\infty$-localized class (12) is $\mathcal{M}^\infty_\varepsilon(\overline{M}) = \{ M \in \mathcal{M} : |g^M(\pi) - g^{\overline{M}}(\pi)| \le \varepsilon\ \forall \pi \}$.

A reference model $\overline{M} \in \mathcal M$ and models $M_1, \dots, M_N \in \mathcal M$, $N \ge 2$, form an $(\alpha, \beta, \delta)$-family (Definition 5.1) if there are $u_i, v_i : \Pi \to [0,1]$ with $\sum_i u_i(\pi) \le N/2$, $\sum_i v_i(\pi) \le 1$, $f^{M_i}(\pi_{M_i}) - f^{M_i}(\pi) \ge \alpha(1 - u_i(\pi))$ and $D^2_{\mathrm{H}}(M_i(\pi), \overline{M}(\pi)) \le \beta v_i(\pi) + \delta$. $\mathrm{Ber}(q)$ is the Bernoulli distribution with mean $q$.

Formalization targets

Goal: Proposition 5.3

For $A \ge 2$ arms, $\overline{M}(\pi) = \mathrm{Ber}(\tfrac12)$ and every $\gamma \ge A/3$, with $\varepsilon_\gamma = \frac{A}{12\gamma}$,

$$\mathsf{dec}_\gamma\bigl(\mathcal{M}^\infty_{\varepsilon_\gamma}(\overline{M}), \overline{M}\bigr) \ge 2^{-6} \cdot \frac{A}{\gamma}.$$

Milestones

1. Lemma A.7: $D^2_{\mathrm{H}}(\mathrm{Ber}(p), \mathrm{Ber}(q)) \le (p-q)^2\bigl(\frac{1}{p+q} + \frac{1}{2-p-q}\bigr)$, and in particular $D^2_{\mathrm{H}}(\mathrm{Ber}(\tfrac12 + \Delta), \mathrm{Ber}(\tfrac12)) \le 3\Delta^2$ for $\Delta \in (0, \tfrac12)$.
2. Lemma 5.1: an $(\alpha, \beta, \delta)$-family $\mathcal{M}'$ with $\beta \ge 0$ satisfies $\mathsf{dec}_\gamma(\mathcal{M}', \overline{M}) \ge \frac{\alpha}{2} - \gamma(\frac{\beta}{N} + \delta)$ for all $\gamma > 0$.
3. The hard family of the proof: $M_i(\pi) = \mathrm{Ber}(\tfrac12 + \Delta\,\mathbb{I}\{\pi = i\})$ is a $(\Delta, 3\Delta^2, 0)$-family around $\mathrm{Ber}(\tfrac12)$.
4. Localization: this family lies in $\mathcal{M}^\infty_\Delta(\overline{M})$.

Companions

The mission also states monotonicity of the DEC in the class (the step from the family to the localized class), Proposition 5.1 (posterior sampling bounds the dual square-loss DEC by $A/\gamma$), and Proposition 6.7, the gap-dependent variant: for bandits with gap exactly $\Delta \in (0, \tfrac18)$, some $\overline{M}$ in the class has $\mathsf{dec}_\gamma(\mathcal{M}^\infty_\Delta(\overline{M}), \overline{M}) \ge \frac{\Delta}{4}\mathbb{I}\{\gamma \le \frac{A}{48\Delta}\}$. Proposition 5.2 (inverse gap weighting) and the decoupling step of Proposition 5.1 are already proved on the platform and are included as references.

Significance

Proposition 5.3 is the DEC half of the $\Omega(\sqrt{AT})$ minimax lower bound for multi-armed bandits: combined with Theorem 3.2 and $\gamma \asymp \sqrt{AT}$, it shows that the general DEC theory loses nothing in rate on the most basic interactive problem, and that the $A/\gamma$ upper bounds of Propositions 5.1 and 5.2 are tight up to constants. Lemma 5.1 is reusable: any lower bound on the DEC of a class can be obtained by exhibiting a hard family, and the paper uses it for linear bandits (Proposition 6.2), ReLU bandits (Proposition 6.6) and gap-dependent bounds (Propositions 6.7, 6.8).

The results are proved in the paper. As far as is known, none of them is machine-checked. A formal development provides a verified Bernoulli Hellinger bound, a reusable hard-family lemma for the DEC as published on the platform, and the first verified DEC lower bound for a concrete class.

Difficulty

The DEC is an inf-sup, so a lower bound must hold against every exploration distribution $p$. A natural first attempt picks a single alternative model and compares; this fails because $p$ can concentrate on the arm where that alternative differs and then the Hellinger penalty cancels the regret. The family must be spread so that no single $p$ is good for all of its members at once, and the constants must balance the regret term against the information term at the chosen $\Delta$. In Lean, an additional difficulty is that the DEC is written with real sInf/sSup, which are $0$ on empty or unbounded sets: every lower bound requires showing that the relevant sets are nonempty and bounded, and passing from the family to the localized class needs monotonicity of the DEC, which the paper uses without comment.

Formalization scope

• Finite alphabets. The paper works over measurable spaces; this mission formalizes the finite-alphabet case, as the published FoundationsRL layer does. A model is m : S → Y → ℝ with every m π a probability vector; expectations are finite sums. The DEC is the published FoundationsRL.GeneralDM.decGf, the Hellinger distance hellingerSq, the mean reward fM.
• Bernoulli subclass. The bandit class is the Bernoulli bandits (Y = Bool, reward $1$ on true), a subclass of the paper's all-distributions-on-$[0,1]$ class. The DEC is monotone in the class and the localized class shrinks with the class, so the Bernoulli lower bounds imply the paper's.
• Optimal-arm selector. $\pi_M$ is a parameter piStar with the hypothesis that it picks a maximizer of $f^M$; every statement holds for every such selector, so for whichever maximizer the paper meant (the reference $\mathrm{Ber}(\tfrac12)$ has every arm optimal).
• Added or dropped hypotheses. Lemma 5.1 makes the page's nonempty decision space explicit; its optimal-arm selector also implies nonemptiness. It adds $\beta \ge 0$, necessary for the printed averaging argument: without it, even identical models can contradict (52). The family definition includes membership of the reference and family models in a probability-model class. The localization claim inherits $A \ge 2$ from Proposition 5.3. Proposition 6.7 states $A \ge 2$, implicit on the page since a gap needs two arms. Proposition 5.1 represents models by their mean vectors and priors as finitely supported (footnote 5).
• Constants. All constants are the page's: $2^{-6}$, $A/(12\gamma)$, $\gamma \ge A/3$, $3\Delta^2$, $5\Delta^2$, $\Delta/4$, $A/(48\Delta)$. The page's proof of Proposition 6.7 names a $(\Delta, 5\Delta^2, 0)$-family but computes with $12\Delta^2$; the stated proposition is the one its arithmetic supports.
• No trivialization. A formalization in which the localized class could be empty, or the payoffs unbounded, would make decGf evaluate to the junk value $0$; the goal is stated over a class containing $\overline{M}$ with bounded rewards, so the inequality is the genuine one, and its right side $2^{-6} A/\gamma$ is strictly positive.

Contributions welcome: proofs of the milestones in attack order, sorry-free lemmas on nonemptiness and boundedness of the DEC's inner sets (reusable for every DEC lower bound in this series), and a proof of the gap-dependent companion.

Selected references

• D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, 2021 (v3, 2023). https://arxiv.org/abs/2112.13487
• D. J. Foster, A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, lecture notes, 2023. https://arxiv.org/abs/2312.16730
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• J.-Y. Audibert, S. Bubeck, Regret Bounds and Minimax Policies under Partial Monitoring, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/audibert10a.html
• D. J. Foster, A. Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, ICML, 2020. https://arxiv.org/abs/2002.04926