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.

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

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).

Motivation

Approximate policy iteration and policy-gradient methods stop when they can no longer find a direction of improvement. Kakade and Langford (ICML 2002) asked what such a stopping point guarantees. Their algorithm, conservative policy iteration, halts at a policy $\pi$ for which no policy can improve much on $\pi$ as measured under a restart distribution $\mu$; the quantity that is small is the optimal policy advantage $\mathrm{OPT}(\mathbb A_{\pi,\mu})$. Theorem 6.2 of the paper translates this local condition into a global statement: the performance of $\pi$ is close to optimal, with a loss controlled by how well $\mu$ covers the states an optimal policy visits.

The bound is the origin of the distribution mismatch coefficient $\|d_{\pi^*,\tilde\mu}/\mu\|_\infty$, which reappears in the analysis of approximate dynamic programming (concentrability coefficients, Munos 2003), of conservative and trust-region methods, and of the convergence of policy gradient methods (Agarwal, Kakade, Lee, Mahajan 2021), where it governs the rate. The performance difference lemma (Lemma 6.1) used in its proof has become a standard tool of reinforcement learning theory.

Setting

A finite Markov decision process has a finite nonempty state set $S$, a finite nonempty action set $A$, transition probabilities $P(s';s,a)$ (for each $s,a$ a probability distribution over $s'$), a reward function $\mathcal R:S\times A\to[0,R]$ with $R>0$, and a discount factor $0\le\gamma<1$. A stochastic policy $\pi(a;s)$ is, for each state $s$, a probability distribution over actions. A state distribution is a probability vector $\mu$ on $S$.

The normalized value function is $V_\pi(s)=(1-\gamma)E[\sum_{t\ge0}\gamma^t\mathcal R(s_t,a_t)\mid\pi,s]$, where $s_0=s$, $a_t\sim\pi(\cdot;s_t)$ and $s_{t+1}\sim P(\cdot;s_t,a_t)$. The state–action value is $Q_\pi(s,a)=(1-\gamma)\mathcal R(s,a)+\gamma\sum_{s'}P(s';s,a)V_\pi(s')$ and the advantage is $A_\pi(s,a)=Q_\pi(s,a)-V_\pi(s)$. The discounted future state distribution from $\mu$ is

and the performance of $\pi$ from $\mu$ is $\eta_\mu(\pi)=\sum_s\mu(s)V_\pi(s)$.

The policy advantage of $\pi'$ with respect to $\pi$ and $\mu$ is $\mathbb A_{\pi,\mu}(\pi')=\sum_sd_{\pi,\mu}(s)\sum_a\pi'(a;s)A_\pi(s,a)$: the expected advantage of $\pi'$ over $\pi$ on the states $\pi$ itself visits. Its maximum over all stochastic policies is $\mathrm{OPT}(\mathbb A_{\pi,\mu})=\max_{\pi'}\mathbb A_{\pi,\mu}(\pi')$ (Definition 4.3). An optimal policy $\pi^*$ satisfies $V_\pi(s)\le V_{\pi^*}(s)$ for every policy $\pi$ and every state $s$. For nonnegative $f,g$ on $S$, $\|f/g\|_\infty=\max_sf(s)/g(s)$ (p. 5).

Formalization targets

Goal: Theorem 6.2 (p. 6)

If $\mathrm{OPT}(\mathbb A_{\pi,\mu})<\varepsilon$ and $\pi^*$ is optimal, then for every state distribution $\tilde\mu$

The goal states both inequalities and the outer bound. The evaluation distribution $\tilde\mu$ is arbitrary and unrelated to the restart distribution $\mu$; taking $\tilde\mu=D$, the start distribution, gives Corollary 4.5 (p. 5).

Milestone: Lemma 6.1 (p. 6)

For any policies $\tilde\pi$, $\pi$ and any starting distribution $\mu$,

The states are weighted by the future state distribution of the new policy $\tilde\pi$, the advantage is that of the old policy $\pi$.

Significance

Theorem 6.2 is the quality guarantee for conservative policy iteration: combined with the paper's Theorem 4.4 (the algorithm stops with $\mathrm{OPT}(\mathbb A_{\pi,\mu})<2\varepsilon$ after polynomially many calls), it bounds the suboptimality of the returned policy for any target distribution, independently of the size of the state space except through the mismatch coefficient. It also explains the role of the restart distribution: a more uniform $\mu$ makes $\|d_{\pi^*,\tilde\mu}/\mu\|_\infty$ small. Lemma 6.1 is used throughout later theory, from trust-region policy optimization to the global convergence of policy gradient methods.

Both results are proved in the paper, with short arguments. The contribution of this mission is a machine-checked version of the infinite-horizon discounted statement in the paper's normalization, with the $\|\cdot\|_\infty$ ratios handled exactly, including states where a denominator vanishes. Neither the discounted performance difference lemma for stochastic policies nor the distribution mismatch bound is known to be formalized in Mathlib; a finite-horizon performance difference identity has been formalized separately and is a different statement.

Difficulty

The mathematics is short; the difficulty is in the infinite-horizon bookkeeping. The value function and $d_{\pi,\mu}$ are infinite series, and Lemma 6.1 relates the series of two different policies: its natural one-line argument uses the Bellman equation for $V_\pi$, which is not the definition here, together with interchanges of infinite sums over time with finite sums over states and actions, each of which needs summability. Theorem 6.2 then needs two facts that are not stated as results in the paper: that $\mathrm{OPT}(\mathbb A_{\pi,\mu})$ equals $\sum_sd_{\pi,\mu}(s)\max_aA_\pi(s,a)$ (the supremum over policies is attained by a greedy policy, and $\max_aA_\pi(s,a)\ge0$), and that $d_{\pi,\mu}(s)\ge(1-\gamma)\mu(s)$. Reading the $\ell_\infty$ ratio with real division would give a false statement when a denominator is zero; the statement avoids this.

Formalization scope

States and actions are finite nonempty types; policies and kernels are real-valued functions π s a (the paper's $\pi(a;s)$) and P s a s' (the paper's $P(s';s,a)$), with their distribution properties as explicit hypotheses. The published definitions IsTransitionKernel, IsPolicy, InducedTransition, OccupationDist, InducedReward and PolicyValue from the Foundations of Machine Learning series are reused; $V_\pi$ is $(1-\gamma)$ times PolicyValue, the defining series. $\mathrm{OPT}$ is the supremum of the policy advantages over stochastic policies, which is the paper's maximum. Optimality of $\pi^*$ is relative to stationary stochastic policies, the paper's policy class; the existence of an optimal policy (the paper's "well known result", p. 2) is not part of this mission.

Every hypothesis is explicit: rewards in $[0,R]$ with $R>0$, $0\le\gamma<1$, $P$ a kernel, $\pi$ and $\pi^*$ stochastic policies, $\mu$ and $\tilde\mu$ state distributions. Each $\|f/g\|_\infty$ bound is stated multiplicatively: "$X\le K\|f/g\|_\infty$" is "$X\le KC$ for every $C$ with $f(s)\le Cg(s)$ for all $s$". When some $g(s)=0<f(s)$ no such $C$ exists and the bound is empty, which matches $\|f/g\|_\infty=+\infty$; no full-support assumption is made on $\mu$ or $\tilde\mu$. The hypothesis $\mathrm{OPT}(\mathbb A_{\pi,\mu})<\varepsilon$ is on the supremum itself, not on the closed form $\sum_sd_{\pi,\mu}(s)\max_aA_\pi(s,a)$, which is a step of the proof; a formalization that assumed the closed form, or that divided by $d_{\pi,\mu}$ in real arithmetic, would not be this theorem. The proof of the theorem uses only that $\pi^*$ is a policy; optimality is kept as a hypothesis because the paper states it.

The proof on p. 7 twice writes $d_{\pi,\mu}(s)\le(1-\gamma)\mu(s)$; the inequality it uses, and the one stated on p. 5, is $d_{\pi,\mu}(s)\ge(1-\gamma)\mu(s)$. This slip is in the proof, not in the statement. Pages are PDF pages; the paper has no printed page numbers.

Useful reusable infrastructure: summability and Bellman equations for the normalized discounted value, $d_{\pi,\mu}$ as a probability distribution with $d_{\pi,\mu}\ge(1-\gamma)\mu$, and attainment of $\mathrm{OPT}$ by a greedy policy. Contributions of any of these as separate lemmas are welcome.

Selected references

• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002. https://dl.acm.org/doi/10.5555/645531.656005
• R. Munos, Error Bounds for Approximate Policy Iteration, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041903
• A. Agarwal, S. Kakade, J. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. https://jmlr.org/papers/v22/19-736.html
• J. Schulman, S. Levine, P. Abbeel, M. Jordan, P. Moritz, Trust Region Policy Optimization, ICML 2015. https://arxiv.org/abs/1502.05477

Motivation

Approximate policy iteration and policy gradient methods are the two classical families of reinforcement learning algorithms that work with approximate, sampled information instead of an exact model. Kakade and Langford (ICML 2002) observed that neither family answers three basic questions: is there a performance measure that is guaranteed to improve at every step, how hard is it to verify that an update improves it, and what performance is reached after a reasonable number of updates. Greedy approximate policy iteration can make the policy worse when the value estimates are slightly wrong at a few states, and policy gradient methods can stall on plateaus where estimating the gradient needs an enormous number of samples.

Their answer is conservative policy iteration: instead of jumping to a greedy policy, move only a controlled fraction of the way toward it, with a step size chosen from an estimate of how much the greedy policy helps. The paper proves that this update improves a restart-distribution performance measure monotonically, terminates after a number of iterations that depends only on the reward range and the target accuracy, and stops at a policy that the greedy oracle can no longer improve by much. The idea is the direct ancestor of trust-region and proximal policy optimization methods (TRPO, Schulman et al. 2015; PPO, Schulman et al. 2017), whose improvement bounds are refinements of the paper's Theorem 4.1.

Setting

A finite Markov decision process has a finite nonempty set of states $S$, a finite nonempty set of actions $A$, transition probabilities $P(s';s,a)$ (for each state $s$ and action $a$, a probability distribution over next states $s'$), a reward function $\mathcal R : S\times A\to[0,R]$ with $R>0$, and a discount factor $0\le\gamma<1$. A stochastic policy $\pi(a;s)$ gives, for each state $s$, a probability distribution over actions.

The normalized value of $\pi$ from $s$ is $V_\pi(s) = (1-\gamma)E[\sum_{t\ge0}\gamma^t\mathcal R(s_t,a_t)\mid\pi,s]$, where $s_0=s$, $a_t\sim\pi(\cdot\,;s_t)$, $s_{t+1}\sim P(\cdot\,;s_t,a_t)$; it lies in $[0,R]$. The state-action value is $Q_\pi(s,a) = (1-\gamma)\mathcal R(s,a)+\gamma E_{s'\sim P(s';s,a)}[V_\pi(s')]$ and the advantage is $A_\pi(s,a) = Q_\pi(s,a)-V_\pi(s)\in[-R,R]$.

For a state distribution $\mu$ (a restart distribution), the discounted future state distribution is $d_{\pi,\mu}(s) = (1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s;\pi,\mu)$ (eq. (2.1)), and the performance measure is $\eta_\mu(\pi) = E_{s\sim\mu}[V_\pi(s)]$.

The policy advantage of a policy $\pi'$ with respect to $\pi$ and $\mu$ is

and $\mathrm{OPT}(\mathbb A_{\pi,\mu}) = \max_{\pi'}\mathbb A_{\pi,\mu}(\pi')$. The conservative update (4.1) is $\pi_{new} = (1-\alpha)\pi+\alpha\pi'$ with $\alpha\in[0,1]$. An $\varepsilon$-greedy policy chooser $G_\varepsilon$ (Definition 4.3) returns, for every policy $\pi$, a policy $\pi'$ with $\mathbb A_{\pi,\mu}(\pi')\ge\mathrm{OPT}(\mathbb A_{\pi,\mu})-\varepsilon$.

Conservative policy iteration (§5) starts from any policy and repeats: call $G_\varepsilon(\pi,\mu)$ to get $\pi'$; form an $\frac\varepsilon3$-accurate estimate $\hat{\mathbb A}$ of $\mathbb A_{\pi,\mu}(\pi')$ from $\mu$-restarts; if $\hat{\mathbb A}<\frac{2\varepsilon}3$, stop and return $\pi$; otherwise apply (4.1) with $\alpha = \frac{(1-\gamma)(\hat{\mathbb A}-\varepsilon/3)}{4R}$ and repeat.

Formalization targets

Goal: Theorem 4.4 (p. 5)

With probability at least $1-\delta$, conservative policy iteration (i) strictly improves $\eta_\mu$ with every policy update, (ii) stops after at most $72R^2/\varepsilon^2$ policy updates, and (iii) returns a policy $\pi$ with

The estimation step is represented by its guarantee: each reached loop's estimate fails to be $\frac\varepsilon3$-accurate with probability at most $\delta/(N+1)$, $N=\lfloor72R^2/\varepsilon^2\rfloor$.

Milestones

Lemma 6.1 (p. 6), the performance difference identity:

Theorem 4.1 (p. 4), with $\varepsilon=\max_s|E_{a\sim\pi'(a;s)}[A_\pi(s,a)]|$ and all $\alpha\in[0,1]$:

Corollary 4.2 (p. 5): if $\mathbb A\ge0$, the step size $\alpha=\frac{(1-\gamma)\mathbb A}{4R}$ gives

Significance

Theorem 4.4 is the first guarantee of its kind for approximate reinforcement learning: the number of iterations is bounded by $72R^2/\varepsilon^2$, independent of the number of states and of the restart distribution, and every iteration provably helps. Lemma 6.1 is the standard performance difference lemma, used throughout the analysis of policy optimization, including natural policy gradient and trust-region methods; Theorem 4.1 is the prototype of the "surrogate objective minus a penalty" bound that TRPO refines.

These results are proved in the paper. As far as a search of the platform shows, none is formalized: the platform's finite-horizon performance difference lemma (Foster and Rakhlin's Lemma 13) is a different statement, for episodic problems with non-stationary policies. This mission produces machine-checked versions of the discounted performance difference identity, the conservative improvement bound with its exact constants, and the high-probability termination and quality guarantee of the algorithm, all on top of an explicit infinite-horizon model rather than an assumed Bellman equation.

Difficulty

The obvious argument for the improvement bound expands $\eta_\mu(\pi_{new})$ to first order in $\alpha$; that only gives $\frac{\alpha}{1-\gamma}\mathbb A+O(\alpha^2)$ with an unspecified constant, which cannot fix a step size. The exact bound needs control of how far the state distribution of the mixed policy drifts from that of the old policy, uniformly in time, and the performance difference identity is only useful once the states are weighted by the new policy's distribution. On the formal side, $V_\pi$ and $d_{\pi,\mu}$ are infinite discounted series, so summability, exchanges of sums and the identities $\sum_s d_{\pi,\mu}(s)=1$ and $\sum_a\pi(a;s)A_\pi(s,a)=0$ must all be established from the definitions. For Theorem 4.4, the algorithm is a random process whose policies depend on all earlier estimates; the argument has to be made pathwise on the event that every reached loop is accurate, together with a union bound over the loops that can be reached.

Formalization scope

Policies are functions π : S → A → ℝ with π s a the paper's $\pi(a;s)$, and P s a s' is $P(s';s,a)$; both are constrained by the published predicates IsPolicy and IsTransitionKernel. $V_\pi$ is $(1-\gamma)$ times the published series PolicyValue, so values are normalized as in the paper. $\mathrm{OPT}$ is a real supremum over all stochastic policies; the set is nonempty and bounded, and the maximum is attained. Every theorem carries the standing assumptions of §2: finite nonempty $S$ and $A$, a transition kernel, rewards in $[0,R]$ with $R>0$, $0\le\gamma<1$, and a state distribution $\mu$. In Corollary 4.2, $R$ is any upper bound on the rewards rather than necessarily the attained maximum.

In Theorem 4.4 the run is formalized pathwise, driven by arbitrary real random estimates on a probability space; the conclusion bounds the probability of the failure event by $\delta$. Two deviations from the printed statement are disclosed. First, (ii) is stated for policy updates: the proof bounds updates, and the algorithm calls $G_\varepsilon$ once more than it updates, so "at most $72R^2/\varepsilon^2$ calls" is off by one. Second, the per-loop failure budget is $\delta/(N+1)$, which covers the $N+1$ loops that may be reached. The Hoeffding estimate (5.1) is not formalized: as printed it concerns the $\frac\varepsilon6$-biased target, and its role is taken by the accuracy hypothesis. The step size is clipped at $1$, which never binds when the estimate is accurate. No trivializing reading is available: the accuracy hypothesis is satisfied by a perfect estimator and a $0$-greedy chooser exists, so the theorem is not vacuous, and strict improvement at every update is required, not merely nonnegative change.

Pages are PDF pages; the paper has no printed page numbers.

A complete development needs summability and algebra of discounted occupation measures, the performance difference identity, and a union bound over the loops of a random process; the first two are reusable for any discounted policy-optimization result. Proofs of the milestones in any order are welcome.

Selected references

• S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002. https://dl.acm.org/doi/10.5555/645531.656005
• J. Schulman, S. Levine, P. Moritz, M. Jordan, P. Abbeel, Trust Region Policy Optimization, ICML 2015. https://arxiv.org/abs/1502.05477
• J. Schulman, F. Wolski, P. Dhariwal, A. Radford, O. Klimov, Proximal Policy Optimization Algorithms, 2017. https://arxiv.org/abs/1707.06347
• D. J. Foster and A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, 2023. https://arxiv.org/abs/2312.16730

Motivation

Online decision-making problems — multi-armed bandits, contextual bandits, structured bandits, and episodic reinforcement learning — look superficially different but share a common shape: a learner repeatedly acts, observes feedback, and is scored by regret against the best action in hindsight. Foster, Kakade, Qian and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making (Foster & Rakhlin, arXiv:2312.16730v1) develops a unifying account of this shape and asks a sharper question than "does this specific algorithm work?": for a given class of possible environments, what is the best regret any algorithm can achieve? The Decision-Estimation Coefficient (DEC), introduced by Foster, Kakade, Qian and Rakhlin (2021, "The Statistical Complexity of Interactive Decision Making") and refined by Foster, Golowich, Qian, Rakhlin and Sekhari (2023), was proposed as the answer: a single real-valued complexity measure of a model class that simultaneously (i) drives a generic optimal-up-to-constants algorithm (Estimation-to-Decisions, E2D), and (ii) lower-bounds the regret of every algorithm. Item (ii) is what turns the DEC from "a complexity measure that happens to work for the algorithms we know" into a genuine characterization of statistical difficulty, in the same sense that minimax rates characterize the difficulty of estimation problems in classical statistics. This mission formalizes that lower bound.

Setting

Chapter 6 of the book (pp. 93–128) introduces Decision Making with Structured Observations (DMSO), a protocol general enough to subsume the contextual-bandit, structured-bandit and episodic tabular-RL protocols of earlier chapters. Over $T$ rounds, the learner selects a decision $\pi_t$ from a decision space $\Pi$; nature draws a reward-observation pair $(r_t, o_t)$ from a fixed, unknown model $M^\star(\cdot \mid \pi_t)$, where a model $M$ maps each decision to a distribution over a reward space $R$ and an observation space $O$. The learner has access to a model class $\mathcal{M}$ containing $M^\star$ (realizability). For $M \in \mathcal{M}$, write $f^M(\pi) := \mathbb{E}_{M,\pi}[r]$ for the mean reward function and $\pi_M := \arg\max_\pi f^M(\pi)$ for the optimal decision; regret is $\mathrm{Reg} := \sum_{t=1}^T f^{M^\star}(\pi_{M^\star}) - \mathbb{E}_{\pi_t \sim p_t}[f^{M^\star}(\pi_t)]$, exactly as in the bandit chapters, now for the general model class.

Because observations, not just mean rewards, now carry information, the DEC needs a way to measure distance between the full conditional distributions $M(\pi)$ and $\hat M(\pi)$, not just between scalars $f^M(\pi)$ and $f^{\hat M}(\pi)$. The chapter uses the squared Hellinger distance $D_H^2$, one of a family of Csiszár $f$-divergences that also includes total variation ($D_{TV}$) and Kullback-Leibler ($D_{KL}$) divergence. For a reference model $\hat M$ and scale $\gamma > 0$, the general Decision-Estimation Coefficient is the min-max game value

and $\mathrm{dec}_\gamma(\mathcal{M}) := \sup_{\hat M \in \mathrm{co}(\mathcal{M})} \mathrm{dec}_\gamma(\mathcal{M}, \hat M)$. This mission's Lean development (FoundationsRL.GeneralDM) formalizes discrete versions of $D_{TV}$, $D_H^2$, $D_{KL}$ for a finite outcome type, the DMSO regret, and this DEC.

Formalization targets

The goal is Proposition 28 (DEC Lower Bound), p. 105:

Here $\mathrm{dec}^c_\varepsilon$ is the constrained DEC (§6.5.1), a variant of the offset DEC above that hard-constrains the information gain rather than subtracting it — a technical refinement needed to make the lower-bound direction go through — and the "localization condition" $\mathrm{dec}^c_{\varepsilon_T}(\mathcal{M}) \ge 10\varepsilon_T$ is a genuine hypothesis of the proposition, not a footnote. Unlike almost every other target in this series of missions, the statement quantifies over every algorithm rather than naming one: it is a genuine impossibility result. Two supporting divergence facts are included as milestones because the DEC's information-theoretic argument rests on them: Lemma 19 ($D_{TV}^2 \le D_H^2 \le D_{KL}$) and Lemma 20 (a bounded-likelihood-ratio refinement bounding $D_{KL}$ in terms of $D_H^2$). The chapter's own matching upper bound, Proposition 26 (the E2D regret bound for the general DMSO protocol, the direct analogue of Chapter 4's Proposition 13), is included as a milestone to give the reader the matching pair the chapter presents together. Finally, Corollary 1 restates the lower bound in terms of the localized offset DEC (combining Proposition 28 with Proposition 27), included as a milestone showing the lower bound's reach beyond the constrained DEC alone.

Significance

Proposition 28 is what makes the DEC a genuine characterization of the statistical complexity of interactive decision making, rather than merely a sufficient condition for a particular algorithm family to succeed. Combined with the (uncited, technically deeper) matching upper bound for the constrained DEC — Proposition 29, stated but not proved in the book — it shows that for any finite model class, the constrained DEC is necessary and sufficient for low regret up to a $\sqrt{\log|\mathcal{M}|}$ factor in the localization radius: no complexity measure that is substantially different from the DEC can characterize the same problems. This is the general decision-making analogue of how minimax rates pin down statistical estimation, now for interactive protocols with adaptive feedback.

Formalizing the lower bound is new work: no result of this shape exists on the Prove2Me platform (searches for "decision-estimation", "general divergence", "constrained DEC" and "Hellinger" — the last of which surfaces two related-but-distinct affinity/Le Cam bounds from a different mission on bandit lower bounds — return no faithful prior art; see MODERATION_NOTES.md). The formal statement is the boxed proposition; the book gives a self-contained but simplified proof (two named simplifying assumptions, §6.5.3) and cites Foster, Golowich, Qian, Rakhlin & Sekhari (2023) for the unrestricted argument. This mission's Lean items are draft statements (:= by sorry), not proofs; formalizing the proof itself — a two-point adaptive testing argument using the chain rule for KL divergence and a change-of-measure step — is the open contribution this mission proposes.

Difficulty

The obvious first attempt is to try to prove the lower bound by exhibiting one fixed pair of hard models $M, \hat M$, as in classical two-point minimax lower bounds (Le Cam's method, Fano's inequality). This fails here because the decision-making protocol is interactive and adaptive: the algorithm's queries depend on what it has observed, so a model pair chosen obliviously (before seeing the algorithm) cannot in general be made indistinguishable to every algorithm — an adaptive algorithm can be constructed that distinguishes any two fixed models quickly by querying where they differ. The book's proof instead selects the "hard" alternative model $M$ as a function of the algorithm's own strategy (via the constrained DEC's arg max, Eq. (6.36)), so that the pair is hard specifically for the algorithm under consideration, then uses the chain rule for KL divergence plus the change-of-measure identity between the algorithm's induced distributions under $M$ and $\hat M$ to conclude that the algorithm's realized decisions must look similar under both models — hence it cannot get low regret on both simultaneously. Every step of this argument depends on the exact game structure of the constrained DEC, not just its numerical value; a formalization that leaves $\mathrm{dec}^c_\varepsilon$ as an unconstrained real parameter (rather than the actual $\inf$-$\sup$ game with its information-gain constraint) would make the lower bound's conclusion vacuous, since the hypothesis $\mathrm{dec}^c_{\varepsilon_T}(\mathcal{M}) \ge 10\varepsilon_T$ would no longer track any actual property of $\mathcal{M}$.

Formalization scope

The decision space $\Pi$ and the outcome (reward, observation) alphabet $Y$ are both taken as finite types (Fintype); a model $m : \Pi \to Y \to \mathbb{R}$ is a conditional probability vector, and a reward-extraction map $\mathrm{rew} : Y \to \mathbb{R}$ recovers the mean reward $f^m(\pi) = \sum_y m(\pi)(y)\cdot\mathrm{rew}(y)$. hellingerSq, totalVariationDiscrete, klDivDiscrete specialize the book's general dominating-measure divergence formula (Eq. (6.5)) to the counting measure on this finite type; klDivDiscrete returns an ENNReal so its $+\infty$ case (when $P$ is not absolutely continuous w.r.t. $Q$) is represented honestly. The DEC, the constrained DEC and the localized subclass are literal sInf-of-sSup/sSup-of-sSup transcriptions of the book's min-max games — the same convention this series uses for the Chapter-4 DEC — not opaque free real numbers, which rules out the trivializing formalization named above.

Three deviations from this series' usual convention of pinning every constant to the value the book's own proof derives are deliberate and disclosed. First, the numerical constant $c$ in $\varepsilon_T := c/\sqrt{T}$ is explicitly called "not important" by the authors themselves (footnote a, p. 105); it is existentially quantified (∃ c > 0) rather than pinned to a numeral. Second — added at moderation, round 2, 2026-09-19, after the constant was found to be pinned incorrectly — the lower bound's own multiplicative constant is also existentially quantified (∃ c' > 0) rather than pinned to 1/20. The book's printed proof (§6.5.3, pp. 107–110) derives 1/20 (p. 110, not p. 109 as an earlier draft of this mission stated) only under two named simplifying assumptions the theorem's hypotheses do not carry (p. 107, "Simplifications": a class-wide bounded-curvature hypothesis, Eq. (6.34); and a bound on the unaugmented $\sup_{\hat M\in\mathcal M}\mathrm{decc}_\varepsilon(M,\hat M)$ rather than the officially-defined, augmented $\mathrm{decc}_\varepsilon(M) = \sup_{\hat M\in\mathrm{co}(\mathcal M)} \mathrm{decc}_\varepsilon(M\cup\{\hat M\},\hat M)$ this mission's decC implements). Since augmenting either supremum's domain can only raise its value, the printed proof's bound on the narrower, unaugmented quantity does not license a pinned 1/20 against the fully general decC this theorem states; the book itself attributes the proof of the general statement to an external reference (Foster, Golowich, Qian, Rakhlin & Sekhari 2023) not in this document. The existential c' matches the book's own unpinned $\gtrsim$ for Proposition 28 as printed on pp. 105–106. Third, "any algorithm" and $\mathbb{E}[\mathrm{Reg}(T)]$ are formalized, as throughout this series, without a full stochastic-process/history model: regret is a deterministic quantity evaluated at a fixed realized decision-distribution sequence $p : \mathrm{Fin}\,T \to \Pi \to \mathbb{R}$, rather than an expectation over an adaptive, history-dependent algorithm's own randomness. Formalizing the fully adaptive, measure-theoretic version of "any algorithm" — with an explicit filtration and expectation over the induced process law $P_M$ — is future work a solver could add; the current statement is faithful to the book's deterministic-per-realization content but not to its full generality over randomized, history-dependent strategies. The DMSO protocol (Def_FoundationsRL_GeneralDM_Protocol) and the DEC (Def_FoundationsRL_GeneralDM_DEC) are restated locally rather than imported from Chapter 4's mission (FoundationsRL.Structured), since draft items cannot import another chunk's drafts; contributions extending either mission to reuse the other's substrate once both are published are welcome.

Selected references

• Foster, D. J., Kakade, S. M., Qian, J., & Rakhlin, A. (2023). Foundations of Reinforcement Learning and Interactive Decision Making. arXiv:2312.16730.
• Foster, D. J., Kakade, S. M., Qian, J., & Rakhlin, A. (2021). The Statistical Complexity of Interactive Decision Making. arXiv:2112.13487.
• Foster, D. J., Golowich, N., Qian, J., Rakhlin, A., & Sekhari, A. (2023). A Unified Model and Dimension for Interactive Estimation. arXiv:2306.06184.
• Polyanskiy, Y., & Wu, Y. Information Theory: From Coding to Learning. Cambridge University Press (draft edition cited by the book as [68]).

Motivation

Decision-making problems rarely present the same fixed choice twice. A doctor prescribing a treatment sees each patient's medical history and symptoms before deciding; a website choosing which article to show sees the visitor's profile first. The multi-armed bandit model — where the learner repeatedly picks from a fixed set of arms with no side information — cannot express this: it is blind to the covariates that any real decision-maker actually observes. The contextual bandit model closes this gap by letting the learner see a context before acting, and asks for a decision rule that generalizes across contexts rather than memorizing a policy per context. Foster and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making (arXiv:2312.16730v1, Section 3, pp. 38–53) develops this model and its algorithms as the bridge between supervised learning and sequential decision making, en route to general reinforcement learning. Contextual bandits with a learned reward-function class underlie production systems for content recommendation, online advertising, and adaptive clinical trial design (Li et al., A Contextual-Bandit Approach to Personalized News Article Recommendation, 2010, https://arxiv.org/abs/1003.0146; Agarwal et al., Making Contextual Decisions with Low Technical Debt, 2016, https://arxiv.org/abs/1606.03966).

The algorithmic history in this chapter runs through two distinct principles. The optimism principle (LinUCB, Section 3.2) generalizes the UCB algorithm to contexts under a linear reward model, but the chapter's own Example 3.1 (Section 3.3) shows optimism fails outside such structured classes, incurring regret linear in the size of the context space or the class. Foster and Rakhlin then present two "black-box" alternatives that use any function class $F$ through an abstract regression subroutine: the naive $\varepsilon$-Greedy method (Section 3.4), and the Inverse Gap Weighting (IGW) strategy underlying the SquareCB algorithm (Bietti, Agarwal & Langford, A Contextual Bandit Bake-off, 2018, https://arxiv.org/abs/1802.04064; Foster & Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, 2020, https://arxiv.org/abs/2002.04926). SquareCB attains a regret rate that both generalizes across contexts (no dependence on the size of the context space) and matches the optimal $\sqrt{T}$ rate — improving on $\varepsilon$-Greedy's $T^{2/3}$ rate — while remaining agnostic to the internal structure of $F$.

Setting

Over $T$ rounds, a decision-maker faces the contextual bandit protocol: at each round $t$, it observes a context $x_t \in X$, selects a decision $\pi_t$ from a finite action set $\Pi = \{1,\dots,A\}$, and observes a reward $r_t \in \mathbb{R}$. Rewards are generated independently as $r_t \sim M^\star(\cdot \mid x_t, \pi_t)$ for a fixed, unknown conditional model $M^\star$; write $f^\star(x,\pi) := \mathbb{E}[r \mid x, \pi]$ for the mean reward function and $\pi^\star(x) := \arg\max_\pi f^\star(x,\pi)$ for the optimal, context-dependent policy. The context sequence $x_1,\dots,x_T$ is arbitrary — fixed in advance or adversarially chosen — while rewards remain stochastic. Performance is measured by regret against $\pi^\star$:

where $p_t$ is the learner's (possibly randomized) action distribution at round $t$.

To generalize across contexts, the learner is given a class $F \subseteq \{f : X\times\Pi \to \mathbb{R}\}$ with $f^\star \in F$, and aims for regret scaling with the statistical complexity $\log|F|$ rather than with $|X|$. Both algorithms in this mission access $F$ only through an online regression oracle (Definition 3, p. 47): given the history $(x_1,\pi_1,r_1),\dots,(x_{t-1},\pi_{t-1},r_{t-1})$, it returns an estimate $\hat f_t : X\times\Pi\to\mathbb{R}$ satisfying, with probability at least $1-\delta$, $\sum_{t=1}^T \mathbb{E}_{\pi_t\sim p_t}[(\hat f_t(x_t,\pi_t)-f^\star(x_t,\pi_t))^2] \le \mathrm{EstSq}(F,T,\delta)$ — for instance, exponential weights on a finite class $F$ achieves $\mathrm{EstSq}(F,T,\delta) = \log(|F|/\delta)$. SquareCB (p. 50–51) then samples its action from the Inverse Gap Weighting distribution (Definition 4, p. 50): given a vector of estimated values $\hat f \in \mathbb{R}^A$ with greedy action $\bar\pi = \arg\max_\pi \hat f(\pi)$, and an exploration parameter $\gamma \ge 0$, $p = \mathrm{IGW}_\gamma(\hat f)$ is $p(\pi) = 1/(\lambda + 2\gamma(\hat f(\bar\pi)-\hat f(\pi)))$ for the unique $\lambda \in [1,A]$ making $p$ a probability distribution.