Reinforcement Learning

Motivation

Every algorithm in the first three chapters of Foster and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making — ε-Greedy and UCB for the multi-armed bandit, Inverse Gap Weighting and SquareCB for contextual bandits — is a special case of the same two-step recipe: estimate a model of the world with an online regression oracle, then convert the estimate into a decision that trades exploration against exploitation. Chapter 4 asks whether this recipe can be made generic: given any structured decision-making problem, specified only by a function class $F$ and a decision space $\Pi$, is there a single quantity that governs the best achievable regret, the way $\sqrt{A/\gamma}$ governs the multi-armed bandit and $\sqrt{d/\gamma}$ governs the linear bandit? The chapter's answer is the Decision-Estimation Coefficient (DEC), introduced by Foster, Kakade, Qian, and Rakhlin [40] as a complexity measure that both upper- and lower-bounds achievable regret for a general decision-making protocol, unifying results that were previously proved from scratch, case by case, for each structured setting. This mission formalizes the chapter's central upper bound (Proposition 13) together with the machinery that makes it computable in two concrete cases — the multi-armed bandit (Proposition 14) and the linear bandit (Propositions 16–17).

Setting

Fix a finite decision space $\Pi$ and a class $F \subseteq \mathbb{R}^\Pi$ of candidate mean-reward functions, with a ground-truth $f^\star \in F$ (realizability). Over $T$ rounds, at each round $t$ the learner observes an estimate $\hat f_t$ produced by an online regression oracle, plays a decision distribution $p_t \in \Delta(\Pi)$ (possibly depending on $\hat f_t$ and the history), and the regret is

where $\pi^\star = \arg\max_\pi f^\star(\pi)$. The oracle's cumulative estimation error is assumed bounded: $\sum_{t=1}^T \mathbb{E}_{\pi \sim p_t}[(\hat f_t(\pi) - f^\star(\pi))^2] \le \mathrm{EstSq}(F,T,\delta)$ with probability at least $1-\delta$ (Definition 7). Writing $\pi_f := \arg\max_\pi f(\pi)$, the DEC game value at a reference model $\hat f$ and scale $\gamma > 0$ is the min-max quantity

and the DEC of $F$ itself is $\mathrm{dec}_\gamma(F) := \sup_{\hat f \in \mathrm{co}(F)} \mathrm{dec}_\gamma(F, \hat f)$. The Estimation-to-Decisions (E2D) algorithm plays, at each round, a $p_t$ certifying (i.e. attaining or beating) the value of this min-max game at $\hat f_t$.

Formalization targets

Goal — Proposition 13 (E2D regret bound)

with probability at least $1-\delta$, for any exploration parameter $\gamma > 0$. This is the weakest stable statement the chapter proves about E2D: it holds for an arbitrary function class and an arbitrary regression oracle, with no structural assumption on $F$ beyond realizability, and the chapter's later sections instantiate it rather than strengthen it.

Milestones

• Lemma 9 (Decoupling), general form: for any distribution $\nu$ over a finite model class and any $\bar f$, $\mathbb{E}_{f\sim\nu}[f(\pi_f) - \bar f(\pi_f)] \le \sqrt{A \cdot \mathbb{E}_{f\sim\nu}\mathbb{E}_{\pi\sim p}[(f(\pi)-\bar f(\pi))^2]}$ — the estimation-to-decisions bridge the whole chapter's approach rests on, decoupling the model index from the played decision.
• Proposition 14 (IGW minimizes the DEC): for the multi-armed bandit ($\Pi=[A]$, $F=\mathbb{R}^A$), Inverse Gap Weighting is the exact minimizer of the DEC game, giving $\mathrm{dec}_\gamma(F) = (A-1)/(4\gamma)$ — the first concrete computation of an abstract quantity, recovering Chapter 3's rate from Proposition 13 alone.
• Proposition 16 (G-optimal design): existence, for any compact full-dimensional-span set $Z \subseteq \mathbb{R}^d$, of a distribution $p$ with $\sup_{z\in Z}\langle \Sigma_p^{-1}z,z\rangle \le d$ — the classical convex-analysis primitive Proposition 17 needs.
• Proposition 17 (DEC for linear bandits): combining the G-optimal design with inverse gap weighting gives $\mathrm{dec}_\gamma(F) \lesssim d/\gamma$ for the linear bandit function class, leading via Proposition 13 to a $\sqrt{dT}$ regret bound.

Significance

The Decision-Estimation Coefficient is, in the book's own words, "the main result" of this line of work: Foster, Kakade, Qian, and Rakhlin [40] show it is not merely an upper bound but (in a suitable localized form, developed further in Chapter 6) a tight characterization of the minimax regret for structured bandits and, more generally, for the interactive decision-making protocol the rest of the book studies. Proposition 13 is the mechanism that makes this useful in practice: it reduces regret analysis for a new structured problem to a single, purely convex-analytic computation of $\mathrm{dec}_\gamma(F)$, in place of a bespoke exploration argument. Propositions 14–17 are the demonstration that this reduction is not vacuous — they recompute, via the DEC alone, the two rates (multi-armed and linear bandit) that earlier chapters of the book derived by direct, setting-specific arguments, and the match is exact. Formalizing this chapter therefore captures the book's unifying abstraction itself, not just one more instance of it. No formalization of the Decision-Estimation Coefficient, in any form, currently exists on the platform (see Formalization scope).

Difficulty

The obvious formalization mistake is to state Proposition 13's conclusion with $\mathrm{dec}_\gamma(F)$ left as an unconstrained free real-number parameter satisfying only the inequality the theorem asserts — a formalization under which the "theorem" would be a triviality about an arbitrary real number, since nothing about the actual min-max game would ever be checked. The chapter's content is precisely the opposite: that this specific minimax quantity can be computed (Proposition 14) or bounded via a concrete strategy (Proposition 17), and — as Chapter 6 shows for a lower bound outside this chunk's scope — that no smaller quantity would do. A second difficulty is proof-theoretic rather than notational: the book's own proof of Proposition 13 bounds regret by an unconstrained supremum over all reference functions $\hat f : \Pi \to \mathbb{R}$, and only identifies this with the official, $\mathrm{co}(F)$-restricted $\mathrm{dec}_\gamma(F)$ of Eq. (4.16) via Proposition 24 — a fact stated on p. 80, outside this chapter's numbered range, whose own proof the book defers to an exercise. A formalization that quietly imports Proposition 24 to close this gap would rest the goal theorem on an unverified fact; this mission instead states the hypothesis the book's own text uses to motivate restricting to $\mathrm{co}(F)$ in the first place (online estimation algorithms produce $\hat f_t \in \mathrm{co}(F)$), so the goal is faithful to what is actually established within the chapter's own pages.

Formalization scope

Every item fixes a finite decision space (Fin A, Fin n, or a generic Fintype S) and states the DEC as the literal sInf-of-sSup transcription of the min-max game (Eqs. (4.15)–(4.16)), never as an opaque bound — this is the trivializing formalization the chunk's own reading of the chapter rules out (see Difficulty). piStar : (S → ℝ) → S is a hypothesized global maximizer selector throughout, constrained to be a genuine argmax only on the function class in scope (F or Set.univ), matching how the book treats $\pi_f$ as a fixed but arbitrary tie-breaking choice. The goal theorem (Proposition 13) adds the explicit hypothesis hfhat : ∀ t, fhat t ∈ convexHull ℝ F, replacing an appeal to the out-of-range Proposition 24 (see Difficulty); this is the one place this mission's statement is not a line-by-line transcription of the book's own displayed proof steps, and it is recorded here and in MODERATION_NOTES.md. Proposition 14's and Proposition 17's $\lesssim$ are replaced by the explicit constants the book's own proofs establish ($(A-1)/(4\gamma)$ exactly, and $(4d+1)/(2\gamma)$ respectively — the latter obtained by summing the three terms the proof of Proposition 17 isolates). Proposition 14's Lean statement splits the book's single equality $\mathrm{dec}_\gamma(F,\hat f) = (A-1)/(4\gamma)$ into an upper bound on the literal decGf, a lower bound restricted to full-support distributions, and IGW's own exact game value, because the book's min over the whole simplex is not provable as a literal Lean equality: a distribution with a zero-weight arm makes the inner supremum genuinely unbounded, and Lean's total Real.sSup returns a junk value smaller than $(A-1)/(4\gamma)$ there (caught in moderation, MODERATION_NOTES.md); the three-conjunct statement recovers exactly the book's real content without asserting that false literal equality. Lemma 9 is restated inside FoundationsRL.Structured rather than imported from the Chapter 2 mission, since draft items across chunks cannot import one another; its source citation still points to its original location (p. 32). Proposition 16 is not drafted: the platform's existing BanditAlgorithm.kiefer_wolfowitz_equivalence (Lattimore & Szepesvári, Theorem 21.1) states the identical existence claim — compact set with full-dimensional span, a design with G-value at most $d$ — as one clause of a larger equivalence, and is reused as a reference item rather than redrafted. Proposition 22 (primal/dual DEC equivalence, §4.4) is deliberately excluded: the book states it "under mild regularity conditions" it does not pin down in the statement itself, which is exactly the kind of unquantified hypothesis this series' faithfulness standard excludes from a goal or milestone. Contributions extending this mission with Chapter 6's lower bound (matching $\mathrm{dec}_\gamma(F)$ from below, establishing tightness) or with a formalization of Proposition 24 itself (removing this mission's hfhat hypothesis) are welcome.

Selected references

• D. Foster, S. Kakade, J. Qian, and A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv:2112.13487, 2021. https://arxiv.org/abs/2112.13487
• D. Foster and A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, arXiv:2312.16730, 2023. https://arxiv.org/abs/2312.16730
• T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020.
• J. Kiefer and J. Wolfowitz, The Equivalence of Two Extremum Problems, Canadian Journal of Mathematics, 1960.

Motivation

Reinforcement learning with large or continuous state spaces is done in practice with function approximation: the agent represents value functions in a low-dimensional parametric family instead of a table indexed by states. For tabular Markov decision processes, regret bounds of order $\sqrt{H^2SAT}$ have been known since the work on UCRL and UCBVI, but they scale with the number of states $S$ and actions $A$ and say nothing when $S$ is infinite. Before 2019, provable guarantees for function approximation either needed a simulator, assumed deterministic transitions, or had regret exponential in the horizon.

Jin, Yang, Wang and Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation (arXiv:1907.05388, COLT 2020), identified a model, the linear MDP, in which an optimistic version of least-squares value iteration has regret polynomial in the feature dimension $d$ and the horizon $H$ and independent of $S$ and $A$. The model and the algorithm, LSVI-UCB, became a standard reference point for the theory of RL with function approximation.

Timeline:

• 2017–2018: Azar, Osband, Munos (arXiv:1703.05449) and Jin, Allen-Zhu, Bubeck, Jordan (arXiv:1807.03765) give near-optimal $\sqrt T$ regret for tabular episodic MDPs.
• 2019: Yang and Wang (arXiv:1902.04779) study linear transition models with a simulator; Jin, Yang, Wang, Jordan prove Theorem 3.1 below without a simulator.
• 2020: Zanette, Lazaric, Kochenderfer, Brunskill (arXiv:2003.00153) improve the dependence on $d$ under a low inherent Bellman error assumption.

Setting

An episodic MDP $\mathrm{MDP}(\mathcal S,\mathcal A,H,\mathbb P,r)$ has a measurable state space $\mathcal S$, a finite action set $\mathcal A$, a horizon $H$, transition kernels $\mathbb P_h(\cdot\mid x,a)$ and deterministic rewards $r_h(x,a)\in[0,1]$ for steps $h=1,\dots,H$. A policy $\pi(x,h)$ chooses an action at each state and step. Its value functions satisfy the Bellman equation $Q^\pi_h=r_h+\mathbb P_hV^\pi_{h+1}$, $V^\pi_h(x)=Q^\pi_h(x,\pi(x,h))$, $V^\pi_{H+1}=0$, where $\mathbb P_hV(x,a)=\int V\,d\mathbb P_h(\cdot\mid x,a)$; the optimal values $V^\star_h$, $Q^\star_h$ satisfy the same recursion with a maximum over actions.

The MDP is linear (Assumption A) with feature map $\phi:\mathcal S\times\mathcal A\to\mathbb R^d$ if $\|\phi\|\le1$ and for each step there are signed measures $\boldsymbol\mu_h=(\mu_h^{(1)},\dots,\mu_h^{(d)})$ and a vector $\theta_h$ with

and $\|\theta_h\|\le\sqrt d$, $\|(|\mu_h^{(1)}|(\mathcal S),\dots,|\mu_h^{(d)}|(\mathcal S))\|\le\sqrt d$.

In each episode $k=1,\dots,K$ an adversary chooses the initial state $x^k_1$; the agent then plays $H$ steps, the next state $x^k_{h+1}$ being drawn from $\mathbb P_h(\cdot\mid x^k_h,a^k_h)$. LSVI-UCB (Algorithm 1) computes, backwards over $h$, the Gram matrix $\Lambda^k_h=\sum_{\tau<k}\phi^\tau_h(\phi^\tau_h)^\top+\lambda I$ of the past features $\phi^\tau_h=\phi(x^\tau_h,a^\tau_h)$, the ridge-regression weight $w^k_h$ for the targets $r_h+\max_aQ^k_{h+1}$, and the optimistic estimate

and then plays greedily with respect to $Q^k_h$. Its policy in episode $k$ is $\pi_k$, and the regret is

Formalization targets

Goal: Theorem 3.1

There are absolute constants $c,C>0$ such that for every linear MDP, every $p\in(0,1)$ and every run of LSVI-UCB with $\lambda=1$ and $\beta=c\cdot dH\sqrt\iota$, $\iota=\log(2dT/p)$,

Milestones

The milestones follow Appendix B of the paper: linearity of $Q^\pi$ (Proposition 2.3) and the weight bounds (Lemmas B.1, B.2, with Lemma D.1); the covering bound for the value class (Lemma D.6, with the Euclidean-ball covering of Lemma D.5); the uniform self-normalized concentration (Lemma D.4, with Theorem D.3) and the good event (Lemma B.3); the error propagation (Lemma B.4), optimism (Lemma B.5) and the recursion (Lemma B.6); and the bonus-sum bound (17)–(18), with Lemma D.2. Lemma D.2, Theorem D.3 and Lemma D.5 are already on the platform and are referenced.

A companion statement, not a milestone, formalizes Proposition 5.1 (§5): on a finite state space with non-degenerate features, if the Bellman operators $\mathbb T^\pi_h$ of (8) map linear action-value functions to linear ones for every policy, then $\mathbb P_h$ is linear in $\phi$.

Significance

The theorem shows that exploration with function approximation can be sample-efficient without a simulator: the regret depends on the intrinsic dimension $d$ of the features and polynomially on $H$, not on the size of the state space. Its analysis, a uniform concentration bound over a data-dependent class of value functions combined with optimism, is the template for a large later literature: misspecified and low-rank MDPs, kernel and neural function approximation, and reward-free exploration.

The result has a published proof, but no machine-checked one. A formalization supplies the measure-theoretic episodic MDP on a general state space, an interaction protocol with adaptive initial states, the LSVI-UCB algorithm, and a checked chain from self-normalized martingale bounds to the regret theorem. The formal statements also record two points where the printed paper is imprecise: the normalization of the measures $\boldsymbol\mu_h$ (see Formalization scope) and the existential reading of the weights in Lemma B.1.

Difficulty

The regression targets $r_h+\max_aQ^k_{h+1}(x^\tau_{h+1},\cdot)$ depend on all past data through $Q^k_{h+1}$. The self-normalized bound for vector-valued martingales (Theorem D.3) therefore cannot be applied to them directly: the natural first idea, conditioning on the past and treating $V^k_{h+1}$ as fixed, fails because $V^k_{h+1}$ is not measurable with respect to the past at the time $x^\tau_{h+1}$ is drawn. The concentration must hold uniformly over a function class, which requires a covering-number bound for a class parametrized by vectors and matrices (Lemma D.6) and a union bound in the right scale.

A second difficulty is formal: the probabilistic protocol mixes an adversary, a learning algorithm reading its own past outputs, and transition kernels on a general measurable space, and the martingale argument (Azuma–Hoeffding over the $KH$ steps) needs every object to be measurable with respect to the right σ-algebra.

Formalization scope

• Model. $\mathcal S$ is any measurable space; $\mathcal A$ is a finite nonempty type with its discrete σ-algebra and a linear order used only to break ties in the argmax. Steps and episodes are 1-based. $V^\pi$, $Q^\pi$, $V^\star$, $Q^\star$ are defined by the Bellman recursions (1) and (2), with value $0$ outside $1\le h\le H$; theorems about general policies assume them measurable.
• Assumption A is stated with the total-variation normalization $\|(|\mu_h^{(i)}|(\mathcal S))_i\|\le\sqrt d$ instead of the printed $\|\boldsymbol\mu_h(\mathcal S)\|\le\sqrt d$; under the printed condition Lemma B.1 is false. The feature map is assumed measurable.
• Runs. A run is a process on a probability space with a filtration over the flattened time $(k-1)(H+1)+(h-1)$: states are adapted, actions are those of Algorithm 1, and the conditional law of $x^k_{h+1}$ given the past is $\mathbb P_h(\cdot\mid x^k_h,a^k_h)$. The initial states are otherwise unrestricted.
• Constants. $c$ and $C$ are quantified before the spaces, $d$, $H$, $K$, $p$, the MDP and the run; $d,H,K\ge1$ and $p\in(0,1)$. "With probability $1-p$" is an upper bound on the outer measure of the failure event.
• Ruling out trivializations. The goal does not assume the good event, optimism, or any milestone conclusion; $\beta$ is fixed by the existentially quantified $c$, not free; the regret uses the model value of the greedy policy, not a realized return. A sorry-free check exhibits a linear MDP and a run satisfying all hypotheses.
• Known gap. Algorithm 1 clips $Q^k_h$ only from above, so the bound $|V^k_{h+1}|\le H$ that Lemma B.3's proof needs (and the target bound in Lemma B.2's proof, here an explicit hypothesis) is not automatic off the good event. Lemma B.3 is stated as printed, for every $c_\beta>0$; a solver who finds it unprovable should report this in the discussion.
• Infrastructure needed: covering numbers of norm balls, the self-normalized martingale bound, Azuma–Hoeffding (in Mathlib), integration against signed measures, and measurability of the algorithm's outputs. The MDP and run definitions are reusable for other episodic RL results; contributions of general lemmas about them are welcome.

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, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
• M. G. Azar, I. Osband, R. Munos, Minimax Regret Bounds for Reinforcement Learning, ICML 2017. https://arxiv.org/abs/1703.05449
• C. Jin, Z. Allen-Zhu, S. Bubeck, M. I. Jordan, Is Q-learning Provably Efficient?, NeurIPS 2018. https://arxiv.org/abs/1807.03765
• L. F. Yang, M. Wang, Sample-Optimal Parametric Q-Learning Using Linearly Additive Features, ICML 2019. https://arxiv.org/abs/1902.04779
• A. Zanette, A. Lazaric, M. Kochenderfer, E. Brunskill, Learning Near Optimal Policies with Low Inherent Bellman Error, ICML 2020. https://arxiv.org/abs/2003.00153

Motivation

Value iteration computes the optimal value function of a Markov decision process by applying the dynamic programming backup to every state until the values stop changing. When the state space is too large for a lookup table, practitioners replace the table by a function approximator: after each backup, the new values are computed only at a sample of states and an approximator (a neural net, a spline, a nearest-neighbour rule) is fitted to them. This approximate value iteration is the basis of much of reinforcement learning, and in the early 1990s it was known to work well in some experiments and to diverge in others, with no theory separating the two. Boyan and Moore (NIPS 7, 1995) exhibited divergence with linear regression and neural nets, and Tsitsiklis and Van Roy (1996) later studied the same question for feature-based architectures.

Gordon's technical report (CMU-CS-95-103, 1995; a shorter, differently numbered version appeared at ICML 1995) isolated a property of the approximator that guarantees convergence: the approximator must not exaggerate differences between target value functions in max norm. It identified a broad class with this property, the averagers (k-nearest-neighbour, kernel averaging, linear and bilinear interpolation on a mesh), and proved that in a discounted problem approximate value iteration through an averager always converges, with an explicit error bound. This mission formalizes that discounted theory: the report's §2–§3 and its error bound of §6.1.

Setting

A finite Markov decision process $M$ has states $1,\dots,n$, a finite nonempty set $U(i)$ of actions at each state $i$, an expected one-step cost $c_{ia}$ for action $a$ at state $i$, and transition probabilities $p_{aij}\ge0$ with $\sum_j p_{aij}=1$. It is discounted with factor $0\le\gamma<1$. A value function is a vector $V\in\mathbb R^n$, measured in the max norm $\|V\|=\max_i|V(i)|$.

The parallel value backup operator $T_M$ updates every state at once:

Its fixed point $V^*$ is the optimal value function, the minimal expected discounted cost from each state.

A function approximator is studied through its mapping $M_F$: the function sending a vector of target values to the vector of fitted values. Two operators $M_F$ and $T$ are compatible if the iterates $(M_F\circ T)^k(x_0)$ converge from every initial guess $x_0$.

An averager $A$ is given by constants $k_i$ and nonnegative weights $\beta_i,\beta_{ij}$ with $\beta_i+\sum_j\beta_{ij}=1$ for every $i$; its mapping is

The weights are fixed in advance and do not depend on the targets $Y$.

Formalization targets

Goal: Theorem 6.2 (p. 12)

Let $V^A$ be any fixed point of $M_A$ and $\varepsilon=\|V^A-V^*\|$. Then there is $V_0$ such that $(T_M\circ M_A)^k(V)\to V_0$ from every initial guess $V$, and

The goal has two parts: convergence from every start to a common limit $V_0$, and the error bound on that limit.

Milestones

1. Theorem 2.2, first clause (p. 4). $\|T_MV-T_MW\|\le\gamma\|V-W\|$.
2. Theorem 3.2 (p. 7). $M_A$ is a max-norm nonexpansion, $\|M_A(Y)-M_A(Z)\|\le\|Y-Z\|$, and is compatible with $T_M$ for every discounted MDP.
3. Theorem 3.1 (p. 5). If $M_F$ is any max-norm nonexpansion, then $M_F$ is compatible with $T_M$ and $\|M_F(T_MV)-M_F(T_MW)\|\le\gamma\|V-W\|$.
4. Corollary 3.1 (p. 6). There is $V_\infty$ with $\|(M_F\circ T_M)^k(V)-V_\infty\|\le\gamma^k\|V-V_\infty\|$ for all $V$ and $k$.

A further item, not a milestone, is the display after the proof of Theorem 6.2 (p. 13), the bound on the fitted output: $\|V^*-M_A(V_0)\|\le2\varepsilon+2\gamma\varepsilon/(1-\gamma)$.

Significance

Theorem 6.2 gives a guarantee that depends only on how well the approximator can represent $V^*$, not on how the iteration is started: if some fixed point of the averager lies within $\varepsilon$ of $V^*$, approximate value iteration finds a function within $2\gamma\varepsilon/(1-\gamma)$ of $V^*$. Theorems 3.1 and 3.2 explain why: an averager is a max-norm nonexpansion, and composing a nonexpansion with a $\gamma$-contraction leaves a $\gamma$-contraction. Together they separate the approximators that are safe to use with value iteration from those that are not (linear regression is not a nonexpansion: the report's Figure 2 shows it can expand max-norm distances).

All results of this mission are proved in the report; none is open. The contraction of the discounted Bellman operator and the identification of its fixed point with the optimal value function are proved on Prove2Me (BertsekasDP.discounted_main_theorem, used here as a reference item). No machine-checked proof of Gordon's averager results or of the $2\gamma\varepsilon/(1-\gamma)$ bound is known to exist; this mission produces one, on top of the published finite MDP model.

Difficulty

Each step is short on paper; the difficulty is in the bookkeeping that a formal proof cannot skip. The nonexpansion of an averager rests on nonnegative weights summing to at most one, which must be extracted from the row constraint $\beta_i+\sum_j\beta_{ij}=1$ in the max norm on $\mathbb R^n$. The goal's convergence clause asks for one limit $V_0$ shared by all initial guesses, which needs completeness of $\mathbb R^n$ and the contraction-mapping theorem applied to $T_M\circ M_A$, not to $T_M$. The error bound compares three different fixed points ($V^*$ of $T_M$, $V^A$ of $M_A$, $V_0$ of $T_M\circ M_A$) in a chain of triangle inequalities. The order of composition matters throughout: the compatibility results iterate $M_F\circ T_M$ (fit after the backup), while the goal iterates $T_M\circ M_A$ (back up after the fit), and the two may not be interchanged.

Formalization scope

• The MDP is the published BertsekasSSPModel (Fin n states, a finite action type, nonempty admissible action sets $U(i)$, costs g, transition probabilities p), and $T_M$ is its BertsekasDiscountedBellmanOp M γ. That model allows substochastic rows; every statement adds the hypothesis $\sum_j p_{aij}=1$ for admissible $a$, which makes it the report's MDP. Action sets may depend on the state, a harmless generalization of the report's single action set. The initial-state distribution $S_0$ never enters a statement and is omitted.
• The discount satisfies $0\le\gamma<1$ in every item. Theorem 6.2's page says only "with discount factor $\gamma$"; it belongs to the report's discounted discussion and its proof uses that $T_M$ is a $\gamma$-contraction.
• $\|\cdot\|$ on Fin n → ℝ is Mathlib's sup norm, i.e. the max norm.
• $V^*$ is a hypothesis: a fixed point of $T_M$. Theorem 2.2's last clause, proved on the platform as BertsekasDP.discounted_main_theorem, identifies it with the optimal value function.
• The averager acts on whole value functions $\mathbb R^n\to\mathbb R^n$, indexed by the states. The report's approximator fits a sample $X_0$ of states; ignoring the value at a state $j$ outside the sample is the special case $\beta_{ij}=0$.
• Theorem 3.1 is printed with "$X=S\times A$" and $M_F\in\mathbb R^{|X|}\mapsto\mathbb R^{|X|}$; since $T_M$ acts on value functions of the state, $M_F$ is stated on $\mathbb R^n$.
• "Converges at the rate $\gamma$" (Corollary 3.1) is the geometric rate of the contraction-mapping theorem, $\gamma^k$ times the initial distance to the limit.
• Theorem 6.2 keeps $\varepsilon=\|V^A-V^*\|$ as an equality, as printed, and its conclusion keeps the convergence clause. A statement asserting only the existence of some $V_0$ with $\|V_0-V^*\|\le2\gamma\varepsilon/(1-\gamma)$ would be trivial ($V_0=V^*$) and is not the theorem.
• Lemma 2.1 and the Contraction Mapping theorem (Theorem 2.1) are in Mathlib (LipschitzWith.comp, ContractingWith) and are not posed.

Proofs of any item are welcome, as are reusable lemmas on max-norm nonexpansions of row-stochastic linear maps, which also serve the nondiscounted companion mission (Stable Function Approximation in Dynamic Programming II).

Selected references

• G. J. Gordon, Stable Function Approximation in Dynamic Programming, Technical Report CMU-CS-95-103, Carnegie Mellon University, 1995; shorter version in Machine Learning Proceedings 1995 (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 (the report's [BT89]; no DOI).
• J. A. Boyan and A. W. Moore, Generalization in Reinforcement Learning: Safely Approximating the Value Function, Advances in Neural Information Processing Systems 7, MIT Press, 1995 (the report's [BM95]).
• J. N. Tsitsiklis and B. Van Roy, Feature-Based Methods for Large Scale Dynamic Programming, Machine Learning 22, 1996, pp. 59–94. https://doi.org/10.1007/BF00114724

Why natural policy gradient

Policy gradient methods optimize a parameterized policy directly by gradient ascent on its expected discounted return. They underlie most practical reinforcement-learning systems, yet for a long time their convergence was understood only locally: the objective $\theta\mapsto V^{\pi_\theta}(\rho)$ is not concave, and plain gradient ascent can stall on plateaus. The natural policy gradient (NPG) of Kakade (2001) preconditions the gradient by the pseudoinverse of the Fisher information matrix of the policy, so that steps are measured in the geometry of the induced action distributions rather than in parameter space. NPG is the conceptual ancestor of trust-region methods such as TRPO and PPO.

Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 2021) prove that exact NPG with softmax policies converges to the optimal value at rate $O(1/T)$, with constants that depend on neither the number of states, nor the number of actions beyond $\log|\mathcal A|$, nor any distribution mismatch coefficient. This mission formalizes that result, Theorem 5.3 of the paper, and the lemmas its proof rests on.

Timeline. Kakade (2001) introduced NPG and observed that, for softmax policies, it moves toward the greedy policy. Kakade and Langford (2002) proved the performance difference lemma. Even-Dar, Kakade and Mansour (2009) analyzed experts algorithms in changing MDPs, whose regret argument this proof adapts; Geist, Scherrer and Pietquin (2019) studied regularized policy iteration with related rates. Agarwal et al. (preprint 2019, journal 2021) gave the dimension-free $\log|\mathcal A|/(\eta T)+1/((1-\gamma)^2T)$ bound formalized here.

Setting

A finite discounted MDP consists of finite sets $\mathcal S$ (states) and $\mathcal A$ (actions, nonempty), 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 distribution $\pi(\cdot\mid s)$ over actions. Its value $V^\pi(s)$ is the expected discounted sum of rewards started from $s$; for a start distribution $\rho$, $V^\pi(\rho)=\sum_s\rho(s)V^\pi(s)$. The state–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

An optimal policy $\pi^\star$ has $V^{\pi^\star}(s)\ge V^\pi(s)$ for every policy $\pi$ and every state $s$; write $V^\star=V^{\pi^\star}$.

The softmax policy with parameter $\theta\in\mathbb R^{|\mathcal S||\mathcal A|}$ is $\pi_\theta(a\mid s)=\exp(\theta_{s,a})/\sum_{a'}\exp(\theta_{s,a'})$. The Fisher information matrix with respect to $\rho$ is

and the NPG update with step size $\eta$ is

where $M^\dagger$ is the Moore–Penrose pseudoinverse and $\pi^{(t)},V^{(t)},A^{(t)}$ are the quantities of $\theta^{(t)}$. Following §5.3, every state is assumed reachable from $\rho$: for each $s$ some policy $\pi$ has $d^\pi_\rho(s)>0$. The normalizer $Z_t(s)=\sum_a\pi^{(t)}(a\mid s)\exp(\eta A^{(t)}(s,a)/(1-\gamma))$ appears in the lemmas.

Formalization targets

Goal: Theorem 5.3

For NPG (15) from $\theta^{(0)}=0$ with any fixed $\eta>0$, for all $T>0$,

Companion: iteration complexity

If moreover $\eta\ge(1-\gamma)^2\log|\mathcal A|$ and $\epsilon>0$, then $V^\star(\rho)-V^{(T)}(\rho)\le\epsilon$ for every $T\ge 2/((1-\gamma)^2\epsilon)$.

Milestones

1. Lemma 3.2 (performance difference): $V^\pi(s_0)-V^{\pi'}(s_0)=\frac{1}{1-\gamma}\mathbb E_{s\sim d^\pi_{s_0}}\mathbb E_{a\sim\pi(\cdot\mid s)}[A^{\pi'}(s,a)]$.
2. Lemma 5.1 (soft policy iteration, policy form): $\pi^{(t+1)}(a\mid s)=\pi^{(t)}(a\mid s)\exp(\eta A^{(t)}(s,a)/(1-\gamma))/Z_t(s)$.
3. Lemma 5.2 (improvement): $V^{(t+1)}(\mu)-V^{(t)}(\mu)\ge\frac{1-\gamma}{\eta}\mathbb E_{s\sim\mu}\log Z_t(s)\ge0$ for every $\mu\in\Delta(\mathcal S)$.
4. Monotonicity (proof of Theorem 5.3): $V^{(t+1)}(s)\ge V^{(t)}(s)$ for all $s$.

Significance

The result. Theorem 5.3 is a global, non-asymptotic guarantee for a non-concave policy optimization problem, with no dependence on $|\mathcal S|$ and no distribution mismatch coefficient: the same analysis does not go through for plain softmax policy gradient, whose rates in the same paper carry such coefficients or are only asymptotic. It explains why Fisher preconditioning helps, and it is the template for the paper's later analysis of NPG with function approximation (§6) and for subsequent work on linear convergence of NPG and on entropy-regularized variants.

Formalizing it. The theorem is proved on paper; no machine-checked proof is known. A formal development needs: a policy-gradient identity for softmax policies, the computation of the Moore–Penrose pseudoinverse of a singular, block-structured Fisher matrix acting on the policy gradient, the performance difference lemma in the unnormalized convention, and a telescoping regret argument with Kullback–Leibler divergences between action distributions. Each of these is reusable: the performance difference lemma and the visitation-distribution calculus serve every result of the paper and much of the reinforcement-learning literature.

Difficulty

The obvious approach, treating NPG as gradient ascent on a smooth objective, fails: $V^{\pi_\theta}(\rho)$ is non-concave and its smoothness constant grows with $1/(1-\gamma)^3$, which would give a rate depending on the state space and on distribution mismatch. The dimension-free rate comes only after the NPG step is rewritten exactly as a multiplicative-weights update on each state's action distribution, and this rewriting is itself delicate. The Fisher matrix is always singular (each state's block annihilates the all-ones vector), the pseudoinverse returns the minimum-norm solution, which is not $A^{(t)}/(1-\gamma)$ but differs from it by a state-dependent offset; and the identity holds at a state only if that state carries positive visitation weight, which is why reachability from $\rho$ is assumed. A newcomer's first idea, replacing $F^\dagger$ by "any solution of $Fu=\nabla V$" or by an ordinary inverse, does not define the algorithm.

Formalization scope

Lean conventions (Mathlib, namespace PolicyGradTheory.NPG):

• Policies are functions S → A → ℝ (π s a $=\pi(a\mid s)$) satisfying the published IsPolicy; transitions P s a s' $=P(s'\mid s,a)$; values, $Q$-functions and state occupation probabilities are the published FoundationsML definitions PolicyValue, QFunction, OccupationDist, and optimality is IsOptimalPolicy. $V^\star(\rho)$ is the value of a policy assumed optimal, never a supremum over arbitrary functions.
• Parameters live in EuclideanSpace ℝ (S × A), so norms are Euclidean and gradient is $\nabla_\theta$.
• The pseudoinverse is the published predicate VectorSpaceOpt.IsPseudoinverse (minimum-norm least-squares inverse, which on Euclidean space is the Moore–Penrose pseudoinverse); Mathlib has none.
• Standing assumptions carried by every statement: rewards in $[0,1]$, $\gamma\in[0,1)$, $\mathcal A$ nonempty, $\rho\in\Delta(\mathcal S)$, every state reachable from $\rho$ (§5.3, footnote 6). The goal also assumes $\theta^{(0)}=0$ and $\eta>0$, as the page does. Lemmas 5.1 and 5.2 hold from any start.
• $\log$ is the natural logarithm; $T$ counts updates and $T>0$ is a natural number.

The goal does not assume the soft-policy-iteration form, the improvement bound or monotonicity; those are milestones to be proved, and a statement taking any of them as a hypothesis would not be Theorem 5.3. The parameter form "$\theta^{(t+1)}=\theta^{(t)}+\frac{\eta}{1-\gamma}A^{(t)}$" of Lemma 5.1 is not stated, since the pseudoinverse step differs from it by a state-dependent offset (as the lemma's own proof on p. 70 shows); only the policy form, which is invariant to that offset, is a target.

Contributions welcome: the softmax policy-gradient identity and score-function formula, existence and uniqueness of the minimum-norm least-squares inverse on Euclidean space, Kullback–Leibler identities for finite distributions, and the summability facts behind the visitation distribution.

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; preprint arXiv:1908.00261v5, 2020. https://arxiv.org/abs/1908.00261v5
• S. M. Kakade, A Natural Policy Gradient, NeurIPS 2001. https://proceedings.neurips.cc/paper/2001/hash/4b86abe48d358ecf194c56c69108433e-Abstract.html
• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• E. Even-Dar, S. M. Kakade, Y. Mansour, Online Markov Decision Processes, Mathematics of Operations Research 34(3), 2009. https://doi.org/10.1287/moor.1090.0396
• M. Geist, B. Scherrer, O. Pietquin, A Theory of Regularized Markov Decision Processes, ICML 2019. https://arxiv.org/abs/1901.11275

Motivation

Every RL guarantee proved earlier in this series — UCB-VI's regret bound, the contextual bandit oracle reductions — scales with the size of the state space $S$, because the algorithms maintain a separate statistic per state. Real environments (images, sensor readouts, natural language) have combinatorially or infinitely many states, so a tabular guarantee is vacuous there: the only hope is to generalize across states via a class of value functions, the way supervised learning generalizes across inputs via a hypothesis class. The chapter develops two algorithms along this line: LSVI-UCB, the linear-function-approximation analogue of UCB-VI whose regret is independent of $|S|$ (a low-rank MDP result originating with Jin, Yang, Wang, and Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020, arXiv:1907.05388), and BiLinUCB, which attains an analogous sample-complexity guarantee under the strictly more general structural condition of low Bellman rank (Jiang, Krishnamurthy, Agarwal, Langford, and Schapire, Contextual Decision Processes with Low Bellman Rank are PAC-Learnable, ICML 2017, arXiv:1610.09512; the Q-type variant formalized here follows Du, Kakade, Wang, and Yang, Is a Good Representation Sufficient for Sample Efficient Reinforcement Learning?, ICLR 2020, arXiv:1910.03016). This mission formalizes the second, strictly more general track: BiLinUCB and its Bellman-rank guarantee; LSVI-UCB is left out of scope (see Formalization scope).

Setting

Both algorithms act on the finite-horizon episodic MDP $M = (S,A,\{P_h\}_{h=1}^H, \{R_h\}_{h=1}^H,d_1)$ of the earlier chapters of this series (RLBasics.Core), with value $f^M(\pi) = \mathbb E_{s_1\sim d_1}[V_1^{M,\pi}(s_1)]$. For a state-action value function $Q = (Q_h)_{h=1}^H$ (with the convention $Q_{H+1}\equiv 0$), the Bellman residual of $Q$ under policy $\pi$ at layer $h$ is

which vanishes identically when $Q = Q^{M,\star}$, the optimal value function (Bellman optimality). Given a class $\mathcal Q$ of candidate value functions, $M$ has Bellman rank $d$ relative to $\mathcal Q$ (Definition 8) if $d$ is the least integer such that, at every layer $h$, there exist embeddings $X_h(\pi), W_h(Q) \in \mathbb R^d$ with $E_h(\pi,Q) = \langle X_h(\pi), W_h(Q)\rangle$ for every policy $\pi$ and $Q\in\mathcal Q$ — equivalently, the least rank of the $\Pi\times\mathcal Q$ matrix of Bellman residuals, at any layer. A linear MDP (the setting of LSVI-UCB, §7.2) is the special case where the transition kernel and reward themselves factor through a known feature map $\phi : S\times A \to \mathbb R^d$; every linear MDP has Bellman rank at most $d$ relative to the linear value-function class, but Bellman rank captures far more (kernel/neural function classes, and low-rank MDPs whose feature map is unknown).

The chapter presents two algorithms. LSVI-UCB (§7.2.1) runs $T$ episodes of ridge regression per layer against the linear feature map, forming a confidence ellipsoid of radius $\rho \propto \sqrt d$ around each layer's estimated parameter and acting greedily with respect to an upper-confidence bonus built from that ellipsoid — the same optimism-under-uncertainty template as UCB-VI, now regularized rather than tabular; it motivates Bellman rank but is not itself formalized by this mission (see Formalization scope). BiLinUCB (§7.3.1), the algorithm this mission formalizes, instead proceeds in $K$ iterations of $n$ episodes: each iteration plays the greedy policy for the current optimistic-on-average value function $Q_k = \arg\max_{Q\in\mathcal Q_k}\mathbb E_{s_1\sim d_1}[Q_1(s_1, \pi_Q(s_1))]$, collects $n$ fresh episodes, and shrinks the confidence set $\mathcal Q_{k+1}$ by discarding value functions whose empirical Bellman residual along the played policy is large; after $K$ iterations it outputs the policy with the best empirical return observed at any iteration.

Formalization targets

Goal — Proposition 47 (BiLinUCB, sample complexity under Bellman rank)

for $M^\star$ of Bellman rank $d$ relative to $\mathcal Q\ni Q^{M^\star,\star}$, where $\hat\pi$ is BiLinUCB's output policy after $K$ iterations of $n$ episodes. This is the weakest stable form: it fixes the shape of the sample complexity (polynomial in $H,d,\log|\mathcal Q|,1/\varepsilon$, logarithmic in $1/\delta$, independent of $|S|$) and leaves the leading constants — which the book itself introduces only as "a sufficiently large numerical constant" — outside the formal claim. Unlike every other goal in this series, this is a PAC (sample-complexity) guarantee on the algorithm's final output policy, not a bound on cumulative regret accrued while learning: BiLinUCB commits to $\hat\pi$ only after the training phase ends, and its suboptimality is measured post-training.

Reaching it rests on two structural facts about BiLinUCB's confidence sets, each formalized as a milestone in attack order:

• Lemma 29 (confidence-set validity): with the stated threshold $\beta$, with probability at least $1-\delta$, simultaneously at every iteration $k$, every retained value function has true (population) Bellman residual along the played policies bounded by $\beta$ up to a constant, and the realizable $Q^{M^\star,\star}$ is itself always retained.
• Lemma 30 (optimism and elliptic-norm bound): conditioned on Lemma 29's event, every retained value function's embedding $W_h(Q)$ has bounded norm with respect to the Gram matrix of the played policies' embeddings, and the optimistic value function $Q_k$ BiLinUCB selects at each iteration has initial-state value at least $f^{M^\star}(\pi^{M^\star})$.

Significance

Proposition 47 shows that a single structural parameter — Bellman rank — is sufficient for sample-efficient RL with function approximation, with a sample complexity that depends only on the horizon, the rank, and the value-function class's log-cardinality, never on $|S|$. This subsumes the linear-MDP guarantee of Proposition 46 (LSVI-UCB, §7.2.1; not itself a target of this mission, see Formalization scope) as a special case — every linear MDP has Bellman rank $\le d$ — while covering strictly more models (kernelized and neural value-function classes with a low-dimensional Bellman-residual factorization that need not come from a known linear feature map). The result is proved in the source and this mission formalizes its statement and the two structural lemmas its proof rests on, as stated; no new mathematics is contributed. Formalizing it commits, for the first time on this platform, to machine-checkable statements of the Bellman rank abstraction, the elliptic-norm confidence-set machinery it drives, and a PAC- (rather than regret-) style learning guarantee, none of which appear in the platform's existing bandit or tabular-RL missions.

Difficulty

The obvious first attempt is to formalize Bellman rank as an unconstrained integer parameter $d$ attached to the MDP, sidestepping the actual rank condition on the Bellman-residual matrix; this is a trivializing formalization; Bellman rank must be the least dimension admitting the stated bilinear factorization; see Formalization scope. A second obstacle is that BiLinUCB's optimism is only "on average" with respect to the initial state distribution (initValue), unlike LSVI-UCB's pointwise optimism over every state and action — conflating the two confidence-set constructions collapses the chapter's main conceptual contrast. Finally, the two technical lemmas (29 and 30) separate a purely probabilistic statement (validity of the empirical confidence set, via Hoeffding and a union bound) from a purely deterministic consequence (the elliptic-norm bound and optimism, which hold on any sample path where the probabilistic event occurred); keeping this separation is what lets Proposition 47's proof combine them cleanly, and collapsing it into one monolithic high-probability statement would misrepresent the book's proof structure.

Formalization scope

The MDP, policy, and trajectory/history machinery (EpisodicMDP, Policy, IsPolicy, Trajectory, Learner, probEvent) are reused unchanged from the series' published RLBasics.Core/RLBasics.UCBVI definitions. The value-function class $\mathcal Q$ is realized as an abstract finite, nonempty type Qc together with an evaluation map qeval : Qc → ℕ → S → A → ℝ, kept fully abstract rather than specialized to any concrete function class — specializing it to, e.g., linear functions would collapse Proposition 47 back into a restatement of Proposition 46, which is exactly the trivializing formalization this mission avoids. Bellman rank (IsBellmanRank) is defined as the least natural number admitting the bilinear factorization (an IsLeast over the coercion to HasBellmanRankLE), never as a free parameter. Every realized per-step reward is taken equal to its conditional mean $R_h(s,a)$ throughout (exact, by the tower property, and not a restriction to deterministic rewards). The elliptic norm of Lemma 30 is expressed via the direct sum-of-squared-inner-products identity $\|v\|^2_\Sigma = \sum_{x\in xs}\langle x,v\rangle^2$ rather than introducing Matrix/matrix-inverse machinery, since no milestone here needs an explicit matrix inverse. Every place the book writes ≲/∝/"a sufficiently large numerical constant" is formalized as an existentially quantified universal constant, fixed ahead of every MDP, value-function class, and $(\varepsilon,\delta)$ instance — never depending on the instance itself. This mission scopes entirely to the Bellman-rank track (Definition 8, BiLinUCB, Lemmas 29-30, Proposition 47); Proposition 46 (LSVI-UCB) and its supporting Lemmas 27-28 are the chapter's motivating linear special case (Section 7.2) but are left out of this mission's scope for time and are not claimed as proved by it — LSVI-UCB's confidence-ellipsoid construction is materially different from BiLinUCB's empirical-Bellman-residual confidence set (see Difficulty) and would need its own milestone chain. A complete development needs no infrastructure beyond what is already published in RLBasics.Core/RLBasics.UCBVI; contributions completing the sorrys in the two technical lemmas and the goal are welcome.

Selected references

• Foster, D. J. and Rakhlin, A. Foundations of Reinforcement Learning and Interactive Decision Making. arXiv:2312.16730v1, 2023. arXiv:2312.16730
• Jin, C., Yang, Z., Wang, Z., and Jordan, M. I. Provably Efficient Reinforcement Learning with Linear Function Approximation. COLT 2020. arXiv:1907.05388
• Jiang, N., Krishnamurthy, A., Agarwal, A., Langford, J., and Schapire, R. E. Contextual Decision Processes with Low Bellman Rank are PAC-Learnable. ICML 2017. arXiv:1610.09512
• Du, S. S., Kakade, S. M., Wang, R., and Yang, L. F. Is a Good Representation Sufficient for Sample Efficient Reinforcement Learning? ICLR 2020. arXiv:1910.03016

Motivation

Reinforcement learning (RL) formalizes sequential decision-making under uncertainty: an agent repeatedly observes a state, takes an action, receives a reward, and transitions to a new state, with the goal of maximizing cumulative reward over an unknown environment. It underlies applications from game-playing agents to robotics and adaptive medical treatment. What separates RL from the bandit and contextual bandit problems of earlier chapters in this series is state: the environment carries information forward across time steps, so a good action now can pay off many steps later, and a poor exploration strategy can take exponentially long to discover it. This mission formalizes the foundational results of finite-horizon episodic RL — the Markov Decision Process (MDP) model, the Bellman-optimality principle that makes dynamic programming possible, and the analytical toolkit (the performance-difference and Bellman-residual-decomposition lemmas) used throughout the field's regret analyses — culminating in a polynomial regret guarantee for UCB-VI, the canonical optimism-based algorithm for tabular RL introduced by Azar, Osband, and Munos (Minimax Regret Bounds for Reinforcement Learning, ICML 2017, arXiv:1703.05449).

Setting

A finite-horizon episodic Markov Decision Process $M = (S, A, \{P^M_h\}_{h=1}^H, \{R^M_h\}_{h=1}^H, d_1)$ consists of a finite state space $S$, a finite action space $A$, a horizon $H$, per-layer transition kernels $P^M_h : S\times A \to \Delta(S)$ and reward distributions $R^M_h : S\times A \to \Delta(\mathbb R)$, and an initial state distribution $d_1 \in \Delta(S)$. An episode unrolls for $h=1,\dots,H$: the learner selects an action $a_h \sim \pi_h(s_h)$ under a randomized non-stationary policy $\pi = (\pi_1,\dots,\pi_H) \in \Pi^{\mathrm{rns}}$ (each $\pi_h : S \to \Delta(A)$), receives reward $r_h \sim R^M_h(s_h,a_h)$, and transitions to $s_{h+1}\sim P^M_h(s_h,a_h)$. The value of $\pi$ is $f^M(\pi) := \mathbb E^{M,\pi}[\sum_h r_h]$, and the state-action and state value functions $Q^{M,\pi}_h(s,a)$, $V^{M,\pi}_h(s)$ are the analogous reward-to-go quantities from layer $h$ onward. In the online RL problem, $M^\star$ is unknown, the learner interacts with it for $T$ episodes, and the goal is to minimize the regret $\mathrm{Reg} = \sum_{t=1}^T \big(f^{M^\star} (\pi^{M^\star}) - f^{M^\star}(\pi^t)\big)$ against the best policy $\pi^{M^\star} \in \arg\max_{\pi\in\Pi^{\mathrm{rns}}} f^{M^\star}(\pi)$.

Formalization targets

Goal — Theorem 1 (UCB-VI regret)

for the UCB-VI algorithm run with the explicit bonus $b^t_{h,\delta}(s,a) = 2\sqrt{\log(2SAHT/\delta)/n^t_h(s,a)}$, under Assumption 6 (deterministic, known, $[0,1]$-bounded rewards). This is the weakest stable form of the guarantee: it fixes only the shape of the bound (polynomial in $S,A,H,T$, logarithmic in $1/\delta$), leaving the exact leading constant — which the book itself does not pin down on this page — outside the formal claim.

Reaching it rests on three structural facts, each formalized as a milestone in attack order:

• Proposition 25 (Bellman optimality): existence of a single deterministic policy simultaneously optimal at every state, computable by backward induction — the reason dynamic programming solves planning at all.
• Lemma 13 (Performance difference) and Lemma 14 (Bellman residual decomposition): two "credit assignment" identities decomposing a value gap (between two policies, or one policy under two models) into a sum of per-layer, on-roll-in terms.
• Lemma 15 (Error decomposition for optimistic policies): the fact that a greedy policy driven by any optimistic value estimate suffers sub-optimality controlled additively — not exponentially — by that estimate's own Bellman residuals, evaluated on-policy.

Significance

The result itself. Theorem 1 is the chapter's headline result: the first guarantee, in this development, that a learning algorithm — one that does not know the environment's transitions in advance — can achieve regret growing only polynomially in the size of the state space, the action space, and the horizon, and only as $\sqrt T$ in the number of episodes. The chapter's own "combination lock" example (Figure 8) shows this is not automatic: naive exploration strategies (such as $\varepsilon$-greedy, which suffices for ordinary bandits) incur regret exponential in the horizon on some MDPs with as few as $H+2$ states. UCB-VI's guarantee is the sample-complexity foundation on which essentially every subsequent result on tabular, linear, and general function-approximation RL in the book is built.

Formalizing it. No part of this chapter's mathematical content already has a faithful counterpart on the platform (see Difficulty, below, and Formalization scope). This mission contributes: (i) a from-scratch Lean formalization of the finite-horizon episodic MDP model and its value functions, faithful to the book's $0$/$1$-indexing and reward-distribution conventions; (ii) faithful statements (drafted with sorry, not yet proved) of Proposition 25 and Lemmas 13–15; and (iii) a faithful statement of Theorem 1 itself, including a from-scratch construction of the finite $T$-episode adaptive interaction process needed to make sense of a high-probability regret guarantee. Proving these — Proposition 25 by backward induction, Lemmas 13–15 by telescoping, and Theorem 1 by combining Lemma 15's optimism bound with a concentration argument bounding the estimation-error and martingale terms of Eqs. (5.30)–(5.33) (omitted here; see Difficulty) — is open work for solvers.

Difficulty

The obvious approach to Theorem 1 — bound the regret episode-by-episode using only the fact that $Q^t$ is close to $Q^{M^\star,\star}$ in some fixed sense — fails because $Q^t$'s error is itself random (it depends on the transitions observed so far) and compounds across $H$ layers of dynamic programming. Lemma 15 defuses the compounding: it shows the sub-optimality gap is additive in the per-layer Bellman residuals rather than multiplicative, provided $Q^t$ is optimistic. Making $Q^t$ optimistic with high probability, in turn, requires a concentration argument for the empirical transition estimates $\widehat P^t_h$ (an application of Freedman's or the Azuma–Hoeffding inequality, not included among this mission's milestones) and a union bound over all $(s,a,h,t)$ — accounting for the $SAHT$ inside the bonus's logarithm. The final regret sum further requires bounding $\sum_t \sum_h 1/\sqrt{n^t_h(s^t_h,a^t_h)}$ by a pigeonhole/potential-function argument over the visitation counts, which is where the $S\sqrt{AT}$ scaling — rather than a naive $SA\sqrt{T}$ — originates. None of this concentration or counting machinery is included in the current milestones; a solver attempting Theorem 1 needs it as prerequisite lemmas.

Formalization scope

MDP and value functions. States and actions are finite types (Fintype); layers are represented $0$-indexed throughout the Lean development (the book's layer $h$ is h - 1), with the terminal convention V _ _ H _ = 0 matching $V_{H+1}\equiv 0$. Since every value/expectation formula in this chapter uses the reward distribution $R_h(s,a)\in\Delta(\mathbb R)$ only through its mean, EpisodicMDP.R records that mean directly — equivalent, by linearity of expectation, to carrying the full distribution, and changing no theorem's content. Transition kernels and policies are represented as plain real-valued functions (S → A → ℝ-style) rather than as Mathlib's PMF, with IsPolicy/the EpisodicMDP structure's own proof fields asserting the probability-distribution properties (nonnegativity, summing to $1$) where the book requires membership in $\Pi^{\mathrm{rns}}$ or a well-formed kernel; this keeps every expectation a finite Finset.sum, needing no measure theory. The optimal value functions Qstar/Vstar are defined as literal suprema over the entire (uncountable, since $|A|\ge2$) policy type — not via a recursive shortcut — which is what rules out the trivializing formalization of Proposition 25: defining Vstar by the very recursion the proposition asserts would make the proposition a tautology, whereas here it is a genuine claim about a supremum over an enormous space of competitor policies.

UCB-VI and Theorem 1. Because $S$, $A$, $H$, and $T$ are all finite, the $T$-episode adaptive interaction (in which round $t$'s policy is a function of the realized history of the first $t-1$ episodes) is modeled as a finite probability space: the outcome type Fin T → Trajectory S A H is a Fintype, "probability" is a finite sum over it, and "with probability $\ge 1-\delta$" is a plain inequality between two real numbers — no MeasureTheory is used anywhere in this mission. The universal constant $C$ in Theorem 1 is existentially quantified (∃ C > 0, …) rather than given as a literal numeral, since its value is not pinned down by the book on this page and this mission does not carry out the (non-milestoned) concentration argument that would derive it; this is the convention adopted throughout for the book's own "$\lesssim$" notation. The empirical-transition estimator inside $Q^t_h$ is defined to be $0$ when $n^t_h(s,a)=0$ (no data yet collected for that pair) — a boundary case Eq. (5.25) does not address, resolved here by convention rather than proof.

Prior art. The platform's existing BanditAlgorithm.UCRL2Algorithm mission formalizes UCRL2 for the average-reward, infinite-horizon MDP setting with a diameter parameter, and its Bellman-optimality statement is the average-cost optimality equation — genuinely different from this chapter's finite-horizon episodic Bellman recursion, even though both go by the name "Bellman optimality." No reference item was reused; every definition and theorem in this mission is drafted from scratch. Both missions bound regret via optimism over a confidence set of models, but for different objectives (average reward vs. finite-horizon cumulative reward) and different MDP classes.

Reusable infrastructure and open contributions. EpisodicMDP, Policy, V/Q/Qstar/Vstar, and stateDist/stateExp are reusable by any future mission on finite-horizon episodic RL in this book's later chapters. Contributions welcome: proofs of the four milestone lemmas (by backward induction and telescoping, respectively); the concentration lemmas underlying Theorem 1's optimism guarantee (Eqs. (5.30)–(5.33) of the source, not milestoned here); and the final regret proof combining them.

Selected references

• Foster, D. J. and Rakhlin, A., Foundations of Reinforcement Learning and Interactive Decision Making, 2023. arXiv:2312.16730v1
• Azar, M. G., Osband, I., and Munos, R., Minimax Regret Bounds for Reinforcement Learning, ICML 2017. arXiv:1703.05449
• Jaksch, T., Ortner, R., and Auer, P., Near-optimal Regret Bounds for Reinforcement Learning, JMLR 11 (2010).

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

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