Reinforcement Learning

Motivation

In a structured bandit problem a learner repeatedly chooses a decision $\pi$ from a set $\Pi$ and observes a noisy reward whose mean $f^M(\pi)$ is an unknown function from a known class $\mathcal{F}_{\mathcal{M}}$. Classical analyses of such problems measure the complexity of $\mathcal{F}_{\mathcal{M}}$ by the eluder dimension (Russo and Van Roy, 2013; 2014) or the star number, and prove regret bounds for posterior sampling (Thompson sampling) or optimistic algorithms in terms of these quantities.

Foster, Kakade, Qian and Rakhlin (2021) introduced the Decision-Estimation Coefficient (DEC), a single complexity measure that yields both upper and lower bounds on the minimax regret of interactive decision making. Section 6.2 of that paper connects the DEC to the older parameters: it shows that the square-loss DEC is bounded by the disagreement coefficient of the class, a quantity introduced in Foster, Rakhlin, Simchi-Levi and Xu (2020) and itself bounded by the star number and the eluder dimension. The bound is certified by posterior sampling, so it also explains why posterior sampling works for these classes.

Setting

Let $\Pi$ be a set of decisions. A model $M$ assigns to each decision a reward distribution; here a model enters only through its mean-reward function $f^M : \Pi \to [0, 1]$ and an optimal decision $\pi_M \in \arg\max_\pi f^M(\pi)$. The class $\mathcal{F}_{\mathcal{M}} = \{f^M : M \in \mathcal{M}\}$ collects the mean-reward functions of a model class $\mathcal{M}$. A reference model $\overline{M}$, not necessarily in $\mathcal{M}$, has mean reward $f^{\overline{M}} : \Pi \to [0, 1]$.

A prior $\mu$ is a finitely supported distribution $\mu = \sum_i w_i \delta_{M_i}$ over $\mathcal{M}$. The posterior sampling strategy plays $\rho_\mu(\pi) := \mu(\{\pi_M = \pi\})$, the law of $\pi_M$ when $M \sim \mu$.

The prior-dependent square-loss DEC (display (70) of the paper) is

$$\underline{\mathrm{dec}}^{\mathrm{Sq}}_\gamma(\mu, \overline{M}) = \inf_{p \in \Delta(\Pi)} \mathbb{E}_{M\sim\mu}\, \mathbb{E}_{\pi\sim p}\Bigl[ f^M(\pi_M) - f^M(\pi) - \gamma \bigl(f^M(\pi) - f^{\overline{M}}(\pi)\bigr)^2 \Bigr],$$

the best trade-off between regret and squared estimation error that a decision distribution $p$ can achieve against a model drawn from the prior.

For a class $\mathcal{F}$ of functions $\Pi \to \mathbb{R}$ and a distribution $\rho$ on $\Pi$, the disagreement coefficient (Definition 6.3) is

$$\theta(\mathcal{F}, \Delta_0, \varepsilon_0; \rho) = \sup_{\Delta \ge \Delta_0,\ \varepsilon \ge \varepsilon_0} \left\{ \frac{\Delta^2}{\varepsilon^2}\, \mathbb{P}_{\pi\sim\rho}\bigl( \exists f \in \mathcal{F} : |f(\pi)| > \Delta,\ \mathbb{E}_{\pi'\sim\rho}[f^2(\pi')] \le \varepsilon^2 \bigr) \right\} \vee 1,$$

where $\pi' \sim \rho$ is drawn independently of $\pi$. It measures how much mass $\rho$ puts on decisions where some function of the class is large although it is small in $L_2(\rho)$. The shifted class $\mathcal{F}_{\mathcal{M}} - f^M$ consists of the differences $f - f^M$, $f \in \mathcal{F}_{\mathcal{M}}$.

Formalization targets

Goal: Theorem 6.2

For every $\gamma \ge e$, posterior sampling certifies

$$\underline{\mathrm{dec}}^{\mathrm{Sq}}_\gamma(\mu, \overline{M}) \le \inf_{\Delta > 0} \left\{ 2\Delta + 24\, \frac{\sup_{M\in\mathcal{M}} \theta(\mathcal{F}_{\mathcal{M}} - f^M, \Delta, \gamma^{-1}; \rho_\mu) \log^2(\gamma)}{\gamma} \right\}.$$

In the formal statement, the objective of (70) evaluated at $p = \rho_\mu$ is bounded by $2\Delta + 24\Theta \log^2(\gamma)/\gamma$ for every $\Delta > 0$ and every upper bound $\Theta$ of the disagreement coefficients of the shifted classes.

Milestones

1. The disagreement coefficient bounds the probability of disagreement at every pair of scales (proof of Lemma E.2, p. 105).
2. The unit-scale decoupling bound with free parameters $\Delta, \varepsilon \in (0, 1]$, $\eta > 0$ (proof of Lemma E.2, p. 105).
3. Lemma E.2, the decoupling lemma: for $\mathcal{F} \subseteq (\Pi \to [-R, R])$, $\{f_z\} \subseteq \mathcal{F}$, $\{\pi_z\} \subseteq \Pi$ indexed by $z \sim \mu$,

$$\mathbb{E}_{z\sim\mu}\bigl[|f_z(\pi_z)|\bigr] \le \inf_{\Delta > 0} \left\{ 2\Delta + 6\, \frac{\theta(\mathcal{F}, \Delta, \gamma^{-1}; \rho_\mu) \log^2(R\gamma \vee e)}{\gamma} \right\} + \gamma\, \mathbb{E}_{z, z'\sim\mu}\bigl[f_z^2(\pi_{z'})\bigr].$$

4. The factor-four comparison of the decoupled squared error against a second prior draw with the squared error against $\overline{M}$ (proof of Theorem 6.2, p. 106).
5. Lemma E.2 applied to the shifted class $\mathcal{F}_{\mathcal{M}} - f^{\widetilde{M}}$ at parameter $\gamma/4$, for a fixed $\widetilde{M}$ (proof of Theorem 6.2, p. 106).

Significance

Theorem 6.2 bounds the DEC of any structured bandit class by its disagreement coefficient. With the bounds of the disagreement coefficient by the star number and the eluder dimension (Lemma 6.1 of the paper, from Foster et al. 2020) and the minimax theorem, it yields Theorem 6.1, which recovers the $\widetilde{O}(\sqrt{\mathfrak{e} T})$ regret bound of Russo and Van Roy for posterior sampling as a special case, and gives a $\widetilde{O}(\sqrt{\mathfrak{s}^2 T})$ bound in terms of the star number. The decoupling lemma (Lemma E.2) is a general tool: it controls a coupled quantity $\mathbb{E}[|f_z(\pi_z)|]$ by a decoupled second moment, and applies wherever an algorithm's decision and the function evaluated there are drawn from the same distribution.

The results are proved in the paper. None of them has a machine-checked proof; this mission produces the first formal statement of the disagreement coefficient and of the decoupling lemma, on which formal versions of eluder-dimension and star-number bounds can build.

Difficulty

The obvious argument fails at the decoupling step. The quantity $\mathbb{E}_{z\sim\mu}[|f_z(\pi_z)|]$ evaluates each function at its own decision, while the estimation error controls only $\mathbb{E}_{z, z'}[f_z^2(\pi_{z'})]$, with independent indices. For a finite set of $A$ decisions, Cauchy–Schwarz bridges the two at the price of a factor $A$; for an infinite decision space this gives nothing. The disagreement coefficient replaces the cardinality, but it controls disagreement only at one pair of scales at a time (the size of $|f(\pi)|$ and the $L_2(\rho_\mu)$ norm of $f$), while the coupled quantity involves all scales at once; obtaining only a $\log^2(\gamma)$ loss from this is the technical core of Lemma E.2.

Formalization scope

• Decisions form an arbitrary type $\Pi$; no finiteness or measurability is assumed. Priors and decision distributions are finitely supported (the paper's footnote 5 equips the model class with the discrete topology), encoded as finite weighted families, so every expectation is a finite sum and $\rho_\mu$ is the family of atoms $\pi_{M_i}$ with weights $w_i$.
• Models enter only through their mean-reward function and their optimal decision, which is all the square-loss DEC depends on; $\pi_M$ is a datum with the hypothesis $f^M(\pi) \le f^M(\pi_M)$ for all $\pi$.
• The disagreement coefficient uses the real supremum. All statements assume $\Delta > 0$, $\gamma^{-1} > 0$ and a uniformly bounded class, under which the supremum is finite; the inner expectation of (71) is over an independent copy of the decision.
• Infima and suprema of the page are stated as universally quantified bounds ("for every $\Delta > 0$", "for every upper bound $\Theta$"), which are equivalent and immune to Lean's default values.
• Lemma E.2 assumes $R \ge 1$: the page states it for every $R$, but its proof treats $R = 1$ and extends to $R \ge 1$ by rescaling; Theorem 6.2 needs only $R = 1$.
• $\log$ is the natural logarithm; $e = \exp(1)$.

The goal is not trivialized by a junk value: the disagreement coefficient is a genuine supremum under the stated hypotheses (a sorry-free check accompanies the definitions), $\gamma \ge e$ rules out negative logarithms, the class $\mathcal{F}_{\mathcal{M}}$ is the whole class rather than the prior's support, and the reference model is not assumed to lie in the class.

Contributions welcome: proofs of the milestones in attack order; a general layer-cake lemma for finite sums; a formal disagreement coefficient bound by the star number or the eluder dimension (Lemma 6.1), which would lead to Theorem 6.1.

Selected references

• D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, 2021 (v3, 2023). https://arxiv.org/abs/2112.13487
• D. J. Foster, A. Rakhlin, D. Simchi-Levi, Y. Xu, Instance-Dependent Complexity of Contextual Bandits and Reinforcement Learning: A Disagreement-Based Perspective, Conference on Learning Theory (cited in the paper as Foster et al. 2020b). https://arxiv.org/abs/2010.03104
• D. Russo, B. Van Roy, Eluder Dimension and the Sample Complexity of Optimistic Exploration, Advances in Neural Information Processing Systems 26, pp. 2256–2264, 2013. https://papers.nips.cc/paper_files/paper/2013
• D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4):1221–1243, 2014. https://doi.org/10.1287/moor.2014.0650 (arXiv: https://arxiv.org/abs/1301.2609)

Motivation

Interactive decision making covers bandits, contextual bandits and reinforcement learning: a learner repeatedly chooses a decision, observes a reward and an observation drawn from an unknown model, and tries to accumulate nearly as much reward as the best decision for that model. Foster, Kakade, Qian and Rakhlin (arXiv:2112.13487) introduced the Decision-Estimation Coefficient (DEC), a single quantity that gives lower bounds on the regret of every algorithm and, through the Estimation-to-Decisions (E2D) meta-algorithm, matching upper bounds. This mission formalizes the upper-bound side in its strongest form: E2D run with Hellinger confidence sets (Option II of Algorithm 1) has regret controlled by the localized DEC, the same quantity that appears in the paper's lower bounds (Theorems 3.1 and 3.2).

The basic E2D guarantee (33) in terms of the global DEC is already posed on Prove2Me as an open goal (FoundationsRL.GeneralDM.e2d_general_regret_bound_v2, the restatement in Foster and Rakhlin's lecture notes, arXiv:2312.16730, Proposition 26). It is not posed again here.

Setting

A decision space $\Pi$ is a finite set. An outcome $y = (r, o)$ consists of a reward and an observation and ranges over a finite set $Y$, and $\mathrm{rew}(y) \in [0,1]$ is its reward. A model $M$ assigns to every decision $\pi$ a probability distribution $M(\pi)$ on $Y$. Its mean reward is $f^M(\pi) = \mathbb E_{y\sim M(\pi)}[\mathrm{rew}(y)]$, and $\pi_M$ is a decision maximizing $f^M$. The learner knows a model class $\mathcal M$ that contains the true model $M^\star$. At round $t$ it plays a distribution $p^{(t)}$ on $\Pi$, and its regret is

$$\mathrm{Reg}_{\mathrm{DM}} = \sum_{t=1}^T \mathbb E_{\pi\sim p^{(t)}}\big[f^{M^\star}(\pi_{M^\star}) - f^{M^\star}(\pi)\big].$$

Write $D^2_{\mathrm H}(P,Q) = \sum_y (\sqrt{P(y)} - \sqrt{Q(y)})^2$ for the squared Hellinger distance. For a reference model $\bar M$ and $\gamma > 0$ the DEC is

$$\mathrm{dec}_\gamma(\mathcal M, \bar M) = \inf_{p\in\Delta(\Pi)} \sup_{M\in\mathcal M} \mathbb E_{\pi\sim p}\big[f^M(\pi_M) - f^M(\pi) - \gamma\, D^2_{\mathrm H}(M(\pi), \bar M(\pi))\big].$$

The localized class $\mathcal M_\varepsilon(\bar M) = \{M\in\mathcal M : f^{\bar M}(\pi_{\bar M}) \ge f^M(\pi_M) - \varepsilon\}$ keeps only the models whose optimal value exceeds that of $\bar M$ by at most $\varepsilon$.

E2D with Option II receives at each round an estimate $\widehat M^{(t)}$ from an online estimation oracle. It keeps the confidence set $\mathcal M^{(t)}$ of models whose accumulated Hellinger error against past estimates, $\sum_{i<t}\mathbb E_{\pi\sim p^{(i)}}[D^2_{\mathrm H}(M(\pi), \widehat M^{(i)}(\pi))]$, is at most $R^2$. It plays a minimizer $p^{(t)}$ of the DEC problem over $\mathcal M^{(t)}$ at $\widehat M^{(t)}$. Assumption D.1 asks that, with probability $1-\delta$, the oracle's Hellinger error on the rounds where $M^\star \in \mathcal M^{(t)}$ is at most a known bound $\widetilde{\mathrm{Est}}_{\mathrm H}(T,\delta)$. It also asks that $\widehat M^{(t)} \in \mathrm{co}(\mathcal M^{(t)})$.

Formalization targets

Goal: Theorem 4.1, (35) (in the form (137) of Theorem 4.1a)

With $R^2 = \widetilde{\mathrm{Est}}_{\mathrm H}(T,\delta)$, rewards in $[0,1]$ and $\gamma > 0$, with probability at least $1-\delta$,

$$\mathrm{Reg}_{\mathrm{DM}} \le \sum_{t=1}^T \sup_{\bar M\in\mathrm{co}(\mathcal M)} \mathrm{dec}_\gamma\big(\mathcal M_{\varepsilon_t}(\bar M), \bar M\big) + \gamma\, \widetilde{\mathrm{Est}}_{\mathrm H}(T,\delta),$$ $$\varepsilon_t = 6\frac{\gamma}{t}\widetilde{\mathrm{Est}}_{\mathrm H}(T,\delta) + \sup_{\bar M\in\mathrm{co}(\mathcal M)}\mathrm{dec}_\gamma(\mathcal M,\bar M) + (2\gamma)^{-1}.$$

Milestones (the steps of the proof in App. D.1)

1. (138): the per-round step. At a minimizer $p^{(t)}$, the instantaneous regret minus $\gamma$ times the Hellinger error of $M^\star$ is at most $\mathrm{dec}_\gamma(\mathcal M^{(t)}, \widehat M^{(t)})$.
2. Lemma D.1: on the event of Assumption D.1, $M^\star \in \mathcal M^{(t)}$ for every $t$, and the total Hellinger error is at most $\widetilde{\mathrm{Est}}_{\mathrm H}(T,\delta)$.
3. Lemma D.2: if $M\in\mathcal M^{(i)}$ for all $i\le t$, then for any model $\bar M$, $f^M(\pi_M) - f^{\bar M}(\pi_{\bar M})$ is bounded by $(2\gamma)^{-1}$ plus the average over $i\le t$ of the DEC values and Hellinger errors.
4. Containment: $\mathcal M^{(t)} \subseteq \mathcal M_{\varepsilon_t}(\widehat M^{(t)})$ for every round, with the radius derived on p. 99 using $2\sup\mathrm{dec}$.

Companion results

• Theorem 4.3, (47): E2D for a general divergence $D \ge 0$ and randomized estimators $\nu^{(t)}$ satisfies $\mathrm{Reg}_{\mathrm{DM}} \le \sup_{\nu\in\Delta(\widehat{\mathcal M})}\mathrm{dec}^D_\gamma(\mathcal M,\nu)\cdot T + \gamma\,\mathrm{Est}_D$ almost surely. With $D = D^2_{\mathrm H}$ and point estimates it contains (33), so it is a generalization of the open goal above, not the same statement.
• Theorem 8.1, (87): contextual E2D with arbitrary contexts satisfies $\mathrm{Reg}_{\mathrm{DM}} \le \sup_{x}\mathrm{dec}^D_\gamma(\mathcal M|_x, \widehat{\mathcal M}|_x)\cdot T + \gamma\,\mathrm{Est}_D$.

Significance

The bound is the paper's most general upper bound. Together with the lower bounds of §3, it shows that the localized DEC characterizes the regret of interactive decision making up to the estimation term. With an aggregating estimator satisfying $\widehat M^{(t)}\in\mathrm{co}(\mathcal M^{(t)})$ (App. A.3), it recovers the finite-class guarantee of Theorem 3.3. The companions extend E2D to general divergences, randomized estimators and adversarially chosen contexts. That last setting contains SquareCB for contextual bandits.

All results of this mission are proved in the paper. None was machine-checked before. Formalizing them produces a checked reduction from decision making to estimation for finite decision and outcome spaces, stated against the published DEC and localized-class definitions, so that later bounds on the DEC of specific classes (bandits, tabular RL) can be combined with it.

Difficulty

The non-localized bound follows from the per-round step (138) by summation. The localized bound does not: the per-round DEC is taken over the confidence set $\mathcal M^{(t)}$, and replacing it by a localized class requires that every model surviving in $\mathcal M^{(t)}$ have optimal value close to that of the current estimate $\widehat M^{(t)}$. The confidence set constrains Hellinger errors against past estimates, not optimal values, and the estimate itself is in general not a member of the class. Bridging these is the content of Lemma D.2 and the containment. The first round is a boundary case: there the confidence set is the whole class, so the containment holds only if the radius $\varepsilon_1$ is at least the full range of the rewards.

Formalization scope

• Finite alphabets. The paper works over measurable spaces. This mission takes a finite decision set $\Pi$ (a Fintype), a finite outcome set $Y$, and models m : S → Y → ℝ with every m π a probability vector. Expectations are finite sums. Contexts in Theorem 8.1 range over an arbitrary type.
• Published layer. Hellinger distance, $f^M$, regret, the DEC (decGf, and dec for the supremum over $\mathrm{co}(\mathcal M)$) and the localized class are the published FoundationsRL.GeneralDM definitions, referenced and not redefined.
• Pathwise statements. A run is a realized sequence of estimates, distributions and confidence sets tied to Algorithm 1 by IsOptionIIRun (lines 7 and 8 and $\widehat M^{(t)}\in\mathrm{co}(\mathcal M^{(t)})$). "With probability at least $1-\delta$" becomes the hypothesis EventD1, the event of Assumption D.1. Line 8's arg min is relaxed to "certifies the minimax value from above", as Remark 4.1 permits. Rounds are 0-based, and $\varepsilon_t$ is evaluated at the paper's index.
• Added hypothesis $R^2 \ge 1/12$ in the goal and the containment. Without it the goal is false. With $R^2 = 0$, two decisions, two Bernoulli models and $\gamma = 10$, the first round has positive regret while the right side is $0$. In applications $\widetilde{\mathrm{Est}}_{\mathrm H}(T,\delta)\ge 2\log(1/\delta)$.
• Radius. The goal uses the printed theorem radius with $1\cdot\sup\mathrm{dec}$. The containment milestone uses the p. 99 proof radius with $2\cdot\sup\mathrm{dec}$. Averaging the DEC terms over the $t-1$ earlier rounds gives the goal's sharper factor.
• Junk values. When a localized class is empty, its Lean DEC is $0$ instead of $-\infty$, which only weakens the bound. All other suprema are over nonempty bounded sets.
• Ruled out. Leaving the confidence sets, estimates or distributions unconstrained would make the goal false or trivial; they are tied to the algorithm by IsOptionIIRun. The open bound (33) is not restated.
• Welcome contributions. Convexity and the triangle inequality for $D^2_{\mathrm H}$, the bound $|f^M - f^{\bar M}| \le D_{\mathrm H}$ for rewards in $[0,1]$, and monotonicity of decGf in the class are reusable beyond this mission.

Selected references

• D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, v3, 2023. https://arxiv.org/abs/2112.13487
• D. J. Foster, A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, lecture notes, 2023. https://arxiv.org/abs/2312.16730
• D. J. Foster, A. Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, ICML 2020. https://arxiv.org/abs/2002.04926

Why a lower bound on the DEC for linear bandits

In a linear bandit a learner repeatedly chooses a decision $\pi$ from a set $\Pi \subseteq \mathbb{R}^d$ and observes a noisy reward whose mean is $\langle \theta^\star, \pi\rangle$ for an unknown parameter $\theta^\star$. It is the standard model for sequential decisions with many correlated actions, such as ad placement, routing and recommendation, and its minimax regret over $T$ rounds is known to scale as $d\sqrt{T}$ up to logarithmic factors (Dani, Hayes and Kakade, COLT 2008; see Lattimore and Szepesvári, 2020, Ch. 19–24).

Foster, Kakade, Qian and Rakhlin (2021) introduce the Decision-Estimation Coefficient (DEC), a single complexity measure that yields both upper and lower bounds on the regret of every interactive decision problem. A complexity measure of this kind is only useful if it is tight on the classical examples. Proposition 6.2 of that paper checks this for linear bandits on the Euclidean unit ball: the localized DEC is at least of order $d/\gamma$, which, through the paper's general lower bound (Theorem 3.2), gives the regret lower bound $\Omega(\sqrt{dT})$. Proposition 6.8 gives the analogous statement for linear bandits whose models have a fixed gap $\Delta$.

Setting

Let $\mathbb{B}^d = \{v \in \mathbb{R}^d : \|v\|_2 \le 1\}$ be the closed Euclidean unit ball. It is both the decision space $\Pi$ and the parameter set $\Theta$. A model with parameter $\theta \in \Theta$ returns, at decision $\pi$, an outcome in $\{-1, +1\}$ drawn from the Rademacher distribution $\mathrm{Rad}(\langle\theta,\pi\rangle)$, which puts mass $(1+\mu)/2$ on $+1$ and $(1-\mu)/2$ on $-1$ when its mean is $\mu$. The mean reward is $f^\theta(\pi) = \langle \theta, \pi\rangle$.

A maximizer selector $\theta \mapsto \pi_\theta$ picks a decision with $\langle\theta,\pi\rangle \le \langle\theta,\pi_\theta\rangle$ for all $\pi$. The regret of a decision is $g^\theta(\pi) = f^\theta(\pi_\theta) - f^\theta(\pi)$. Two outcome laws are compared by the squared Hellinger distance $D^2_{\mathrm{H}}(P,Q) = \sum_y (\sqrt{P(y)}-\sqrt{Q(y)})^2$.

Given a reference model $\overline{M}$, the $L_\infty$-localized class at radius $\varepsilon$ is

$$\mathcal{M}^\infty_\varepsilon(\overline{M}) = \{ M \in \mathcal{M} : |g^M(\pi) - g^{\overline{M}}(\pi)| \le \varepsilon \ \ \forall \pi \in \Pi \},$$

and the DEC at scale $\gamma > 0$ is

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

the infimum running over all Borel probability measures $p$ on $\Pi$.

Formalization targets

Goal: Proposition 6.2

For all $d \ge 4$ and $\gamma \ge 2d/3$ there is $\overline{M} \in \mathcal{M}$ with

$$\mathsf{dec}_\gamma\bigl(\mathcal{M}^\infty_{\varepsilon_\gamma}(\overline{M}), \overline{M}\bigr) \ge \frac{d}{12\gamma}, \qquad \varepsilon_\gamma = \frac{2d}{3\gamma}.$$

The page prints $\varepsilon_\gamma = d/(3\gamma)$. The hard family of its proof has regret functions $\Delta(1-\pi_i)$, which reach $2\Delta$ at $\pi = -e_i$ while the reference regret is identically $0$, so the family lies in the class of radius $2\Delta$ and not in the class of radius $\Delta$. The goal is stated at the radius the proof supports.

Milestones

1. Lemma A.8: $D^2_{\mathrm{H}}(\mathrm{Rad}(\mu), \mathrm{Rad}(0)) \le \tfrac34\mu^2$ on $[-1,1]$, together with the two general bounds of the lemma.
2. Lemma 5.1: an $(\alpha,\beta,\delta)$-family forces $\mathsf{dec}_\gamma \ge \alpha/2 - \gamma(\beta/N + \delta)$, stated for a general measurable decision space.
3. The hard family $\theta_i = \Delta e_i$: regret $\Delta(1-\pi_i)$ and $D^2_{\mathrm{H}}(M_i(\pi), \mathrm{Rad}(0)) \le \tfrac34\Delta^2\pi_i^2$. With the coordinate bounds $\sum_i \pi_i \le \sqrt d \le d/2$ ($d \ge 4$) and $\sum_i \pi_i^2 \le 1$, stated as a separate item, this makes the family a $(\Delta, \tfrac34\Delta^2, 0)$-family.
4. Localization: the family lies in $\mathcal{M}^\infty_{2\Delta}(\mathrm{Rad}(0))$.

Companion: Proposition 6.8

For $\Delta \in (0, 1/4)$ and $d \ge 2$, an explicit class of linear bandit models on $\{e_1,\dots,e_d\}$, each with gap $\Delta$, satisfies $\mathsf{dec}_\gamma(\mathcal{M}^\infty_\Delta(\overline{M}),\overline{M}) \ge (\Delta/4)\,\mathbb{I}\{\gamma \le d/(12\Delta)\}$ for all $\gamma > 0$.

Significance

The bound shows that the DEC of linear bandits under Euclidean geometry is of order $d/\gamma$, which matches, up to constants, the upper bound $\mathsf{dec}^{\mathrm{Sq}}_\gamma \le d/(4\gamma)$ on the square-loss variant of the DEC certified by the strategy of Proposition 6.1. Through Theorem 3.2 it gives the regret lower bound $\Omega(\sqrt{dT})$ for every algorithm. Proposition 6.8 shows that the DEC gives meaningful lower bounds even for classes of models with a fixed gap.

All results are proved in the paper. None has a machine-checked proof. The mission produces a formal statement of the linear-bandit lower bound with its radius corrected, the hard-family lemma (Lemma 5.1) in a form that applies to infinite decision spaces and to range-free $u_i$, and the Rademacher Hellinger estimates that later DEC lower bounds reuse.

Difficulty

The arithmetic of the construction is short. The work is in the infrastructure.

• The infimum runs over all Borel probability measures on the ball, not over finitely supported ones. Lemma 5.1 must therefore be proved for Bochner integrals, with the integrability of the payoff established from its continuity on the compact ball.
• The bound $\sum_i \pi_i \le \sqrt d \le d/2$ is Cauchy–Schwarz on $\mathbb{R}^d$ and needs $d \ge 4$.
• The value $\langle\theta_i, \pi_{\theta_i}\rangle = \Delta$ must come from the selector hypothesis plus Cauchy–Schwarz, because the selector is not given explicitly.
• Lemma 5.1 cannot be applied in the form printed in Definition 5.1: there $u_i$ takes values in $[0,1]$, but the family's $u_i(\pi) = \pi_i$ can be negative. The lemma is needed without the range conditions.

Formalization scope

• Outcomes. They are finite: the $\pm1$ outcome is encoded on Bool, and models are the Rademacher laws $\mathrm{Rad}(\langle\theta,\pi\rangle)$, identified with their parameters $\theta \in \mathbb{B}^d$. The paper's class contains every reward law on $[-1,1]$ with linear mean. The Rademacher subclass has a smaller localized class, so a lower bound for it implies the paper's.
• Decisions. For the goal they range over the ball itself (an infinite space with its Borel $\sigma$-algebra), and decision distributions are arbitrary ProbabilityMeasures on it.
• The DEC is unfolded. For every $p$ some model of the localized class attains the bound. This is what the proof shows, and it implies the inf–sup inequality.
• Selectors. $\pi_M$ is a selector with a maximizer hypothesis, so statements hold for every choice of maximizer.
• Added hypotheses. Lemma 5.1 carries $\alpha, \beta \ge 0$ and integrability of its four functions. Proposition 6.8 carries $d \ge 2$.
• No trivializing reading. The integrals in the goal are genuine: the integrand is bounded and continuous, and a sanity file proves integrability, so the Bochner convention $\int f = 0$ for non-integrable $f$ never applies. The goal's quantifier over $p$ is not restricted. The radius $2d/(3\gamma)$ is the smallest the construction allows.
• Definitions and reuse. The mission defines the unit ball, $\mathrm{Rad}$, the linear model, the regret $g^\theta$, and the localized class over a measurable decision space. It references the published hellingerSq, fM and decGf. The general Lemma 5.1 and Lemma A.8 are reusable for every DEC lower bound in §§5–7.

Contributions welcome: proofs of the milestones, a version of the goal through an explicit inf–sup definition of the DEC over measures, and the general model class with arbitrary reward laws on $[-1,1]$.

Selected references

• D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, v3, 2023. https://arxiv.org/abs/2112.13487
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020 (linear bandits, Ch. 19–24). https://doi.org/10.1017/9781108571401
• D. J. Foster, C. Gentile, M. Mohri, J. Zimmert, Adapting to Misspecification in Contextual Bandits, NeurIPS 2020 (Proposition 6.1's strategy). https://arxiv.org/abs/2107.05745

Why expected regret needs a lower bound

In interactive decision making, an algorithm chooses actions while learning which model governs its observations. A low-regret guarantee for one algorithm does not by itself say whether every algorithm could do better. The Decision-Estimation Coefficient (DEC) was introduced to express the cost of choosing useful decisions while distinguishing plausible models. Foster, Kakade, Qian and Rakhlin's Theorem 3.2 gives the corresponding lower bound: when a localized model class has large DEC, an adaptive algorithm must incur expected regret under at least one model in the class. This mission formalizes that result for finite decision and outcome alphabets.

The paper's protocol covers bandits, partial monitoring, and reinforcement-learning examples through a common model that maps each decision to a distribution over rewards and observations. Its lower bound concerns the protocol itself, rather than any one algorithm or application. The theorem therefore gives a common test for the limits of learning in several interactive settings. The finite-alphabet representation here retains adaptive decision kernels, which are central to the theorem.

Models, algorithms and the coefficient

Let $\Pi$ be the set of decisions, $Y$ the set of joint reward–observation outcomes, and $r:Y\to\mathbb R$ the reward map. A model $M$ assigns a probability distribution $M(\pi)$ on $Y$ to each $\pi\in\Pi$. Its mean reward is $f^M(\pi)=\mathbb E_{y\sim M(\pi)}r(y)$, and $\pi_M$ is a maximizing decision. The gap function is $g^M(\pi)=f^M(\pi_M)-f^M(\pi)$.

At round $t$, an adaptive algorithm assigns a distribution $p^{(t)}(\cdot\mid H^{(t-1)})$ on decisions using the full preceding history. It samples a decision from that distribution and receives an outcome drawn from $M(\pi^{(t)})$. The joint law of the length-$T$ history is $P^{M,p}$. Following equation (1) of the paper, regret sums the gaps averaged under the algorithm's chosen distribution at each round. Thus its expectation is over the history law, while the inner gap is averaged under $p^{(t)}$. This formulation retains the algorithm's dependence on earlier outcomes.

For probability distributions $P,Q$ on $Y$, write $D_H^2(P,Q)=\sum_y(\sqrt{P(y)}-\sqrt{Q(y)})^2$ for squared Hellinger distance. For a reference model $\bar M$ and $\gamma>0$, the DEC of a class $\mathcal N$ is

$$\operatorname{dec}_\gamma(\mathcal N,\bar M)= \inf_{q\in\Delta(\Pi)}\sup_{M\in\mathcal N} \mathbb E_{\pi\sim q}\left[g^M(\pi)-\gamma D_H^2(M(\pi),\bar M(\pi))\right].$$

The uniformly localized class $\mathcal M^\infty_\varepsilon(\bar M)$ contains those $M\in\mathcal M$ for which $|g^M(\pi)-g^{\bar M}(\pi)|\le\varepsilon$ for every decision. The density-ratio bound $V(\mathcal M)$ is the supremum of event likelihood ratios $M(A\mid\pi)/M'(A\mid\pi)$ over both models, decisions and events, with a lower cutoff of $e$. It may be infinite. These conventions are equations (2), (5), and (12), and the definition immediately before Theorem 3.1 in the source.

Formalization targets

Localized DEC lower bound

Suppose $\mathcal M$ is nonempty, every model is a probability kernel, and $f^M(\pi)\in[0,1]$ for every $M\in\mathcal M$ and $\pi\in\Pi$. For $T\ge1$, set $C(T)=2^{11}\log(2T\wedge V(\mathcal M))$ and $\bar\varepsilon_\gamma=\gamma/(C(T)T)$. The goal is the following supremum form of Theorem 3.2, equation (13):

$$\sup_{M\in\mathcal M}\mathbb E^{M,p}[\operatorname{Reg}_{\rm DM}] \ge \frac{T}{6}\operatorname{dec}_\gamma \bigl(\mathcal M^\infty_{\bar\varepsilon_\gamma}(\bar M),\bar M\bigr) \qquad(\gamma>0,\ \bar M\in\mathcal M).$$

The paper writes the result with a maximum over $\gamma$ and a supremum over $\bar M$, and says that one model attains the resulting bound. Its proof explicitly permits a limit sequence when the inner supremum is not attained. The displayed statement records exactly the resulting bound on the supremum of expected regret. It implies an arbitrarily close model-specific bound for each fixed $\gamma$ and $\bar M$.

Supporting targets

The milestones follow the statements the paper's proof (App. C.1.3, pp. 90–91) uses, in attack order: the multiplicative Hellinger comparison of Lemma A.11; the difference comparison of Lemma A.12; the Hellinger bound on adaptive history laws, $D_H^2(P^M,P^{\bar M})\le C_T\,T\,\mathbb E_{\pi\sim p_{\bar M}}[D_H^2(M(\pi),\bar M(\pi))]$ with $C_T=2^8\log(2T\wedge(V^{\bar M}(\mathcal M)\vee e))$; the DEC comparison at the reference model's average play $p_{\bar M}$, (129); the localized gap comparison (132); and the final inequality $\mathbb E_{p_M}[g^M]+\mathbb E_{p_{\bar M}}[g^{\bar M}]\ge\frac13\operatorname{dec}_\gamma$ for $\varepsilon\le\gamma/(8C_TT)$. Their source wording and page citations are preserved in the milestone list.

What the result supplies

The theorem supplies a quantitative obstruction to uniformly small expected regret. It uses the same coefficient that appears in the paper's upper-bound framework, so a model class with matching upper and lower DEC estimates can have its regret scale characterized through one object. In particular, the coefficient is sensitive to the model neighborhood relevant at horizon $T$; replacing it by a global coefficient would lose the theorem's stated localization. The paper applies this framework to bandit and reinforcement-learning classes.

The goal and milestone declarations here are open Lean statements with checked syntax and types. A complete formalization would supply proofs of the Hellinger comparisons, the history-law inequality, and the lower bound itself. The history and density-ratio definitions are reusable for other adaptive finite-alphabet lower bounds; the published FoundationsRL mean reward, Hellinger distance and DEC definitions are reused directly.

Where the difficulty lies

A fixed sequence of decision distributions does not describe the theorem's algorithms: later decisions depend on outcomes produced by the unknown model. The comparison must therefore use two different laws on entire histories generated by the same adaptive kernels under two models. A bound on a single round's divergence cannot simply be multiplied by $T$ without accounting for the dependence of future decision distributions on past observations. The DEC itself involves a minimum over decision distributions and a supremum over models, which need not be attained.

Formalization scope

The Lean representation uses finite $\Pi$ and $Y$; probability laws and expectations are finite vectors and sums. This is a finite-alphabet specialization of the paper's measurable-space setting. Histories are functions from round indices to decision–outcome pairs. The algorithm is a family of kernels from every possible past history to a decision distribution. Its law is the product of its decision probabilities and the model's outcome probabilities. Rounds are indexed from zero in Lean, corresponding to the paper's rounds $1,\ldots,T$.

Every model in $\mathcal M$ and every algorithm kernel is normalized and nonnegative. The mean reward range $[0,1]$, nonempty model class, maximizing selector, and positive horizon are explicit hypotheses. They keep the real-valued supremum and infimum in the published DEC from taking Lean's default values on empty or unbounded sets. An event with positive numerator and zero denominator has infinite likelihood ratio; $V(\mathcal M)=+\infty$ remains allowed because the theorem uses $2T\wedge V(\mathcal M)$. Its logarithm therefore has a finite, positive argument for $T\ge1$. The goal uses the exact constants $2^{11}$ and $1/6$. The proof's constant $C_T$ is printed on p. 90 as $2^8(\log(2T)\wedge\log V^{\bar M}(\mathcal M))$; the formalization uses $V^{\bar M}(\mathcal M)\vee e$, the hypothesis $V\ge e$ of Lemma A.13 (98) from which $C_T$ is derived. Without it the history bound fails for two nearly equal models, and with it $8C_T\le C(T)$ still holds, so the goal is unaffected. The intermediate results that select a model approaching a supremum carry an arbitrary slack $\eta>0$, the paper's "limit sequence".

Contributions should preserve the adaptive history law and equation (1)'s decision-distribution regret. A statement restricted to predetermined decisions would leave out the central quantifier of Theorem 3.2. The published FoundationsRL definitions of $f^M$, $D_H^2$ and $\operatorname{dec}_\gamma$ provide the shared finite model interface; the new history and density-ratio layer can support further lower bounds in this series.

Selected references

• Dylan J. Foster, Sham M. Kakade, Jian Qian, and Alexander Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, version 3, 2023. arXiv:2112.13487v3.
• Dylan J. Foster and Alexander Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, arXiv preprint, 2023. arXiv:2312.16730v1.

Motivation

Policy gradient methods optimize a parameterized policy for a Markov decision process by local search on its expected cost. The objective is nonconvex, so local search can in principle stall at a poor stationary point. Bhandari and Russo, Global Optimality Guarantees for Policy Gradient Methods show that for a broad family of control problems this does not happen, and, in quantitative form, that the objective is gradient dominated: its suboptimality is bounded by a multiple of the size of its gradient. The multiple involves a single problem-dependent quantity, the effective concentrability coefficient $\kappa_\rho$, which measures how well the initial state distribution $\rho$ covers the states that matter for optimal behaviour. Theorem 2 and the convergence rates of Theorem 5 of the paper are only informative when $\kappa_\rho$ is finite, so sufficient conditions for a finite $\kappa_\rho$ are what make those results usable. This mission formalizes the paper's three such conditions (Theorem 4).

Distribution-mismatch coefficients of this kind go back to Kakade and Langford (2002), and appear in the analyses of approximate dynamic programming by Scherrer and Geist (2014) and of policy gradient methods in finite MDPs by Agarwal et al. (2021).

Setting

A discounted Markov decision process consists of a measurable state space $\mathcal S$, nonempty feasible action sets $\mathcal A_s$, a bounded measurable per-period cost $g(s,a)$, a transition kernel $P(\cdot\mid s,a)$, a discount factor $\gamma\in(0,1)$ and an initial probability distribution $\rho$ on $\mathcal S$. A feasible measurable stationary policy $\pi$ ($\pi\in\Pi$) picks an action $\pi(s)\in\mathcal A_s$ in every state. Its cost-to-go $J_\pi(s)$ is the expected discounted cost from $s$, its discounted state-occupancy measure is

$$\eta_\pi(\cdot)=(1-\gamma)\sum_{t\ge0}\gamma^t\,\Pr{}^\pi_\rho(s_t\in\cdot),$$

and its average cost is $\ell(\pi)=(1-\gamma)\int J_\pi\,d\rho$. The Bellman operator acts on bounded measurable functions by

$$(TJ)(s)=\min_{a\in\mathcal A_s}\Big[g(s,a)+\gamma\int J(s')\,P(ds'\mid s,a)\Big].$$

An optimal policy $\pi^*$ minimizes $J_\pi$ at every state; $J^*=J_{\pi^*}$. A policy class $\Pi_\Theta=\{\pi_\theta:\theta\in\Theta\}$ is indexed by a convex set $\Theta\subseteq\mathbb R^d$, and $\mathcal J_\Theta=\{J_{\pi_\theta}:\theta\in\Theta\}$.

The effective concentrability coefficient $\kappa_\rho$ (Definition 3) is the smallest scalar $\kappa$ such that

$$\|J-J^*\|_{1,\rho}\le\frac{\kappa}{1-\gamma}\,\|J-TJ\|_{1,\rho}\qquad\forall J\in\mathcal J_\Theta,\tag{13}$$

with $\|J\|_{1,\rho}=\int|J|\,d\rho$, and $\kappa_\rho=\infty$ if no scalar works. It converts a $\rho$-weighted Bellman error into a $\rho$-weighted optimality gap.

Formalization targets

Goal: Theorem 4(b)

If $\eta_{\pi^*}(B)\le C\rho(B)$ for every measurable set $B$, then $C$ satisfies (13); equivalently

$$\kappa_\rho\le\Big\|\frac{d\eta_{\pi^*}}{d\rho}\Big\|_\infty .$$

Companions: Theorem 4(a) and 4(c)

(a) If $\mathcal S$ is finite and $\rho(s)>0$ for all $s$, then $\kappa_\rho\le 1/\min_{s}\rho(s)$. (c) If $T$ is a contraction with modulus $\gamma$ in a norm $\|\cdot\|$ with $c\|J\|\le\|J\|_{1,\rho}\le C\|J\|$, then $\kappa_\rho\le C/c$.

Milestones

The element-wise inequalities $TJ\preceq T_\pi J$, $TJ_\pi\preceq J_\pi$ (5); the performance difference identity $\ell(\pi)-\ell(\bar\pi)=\int[T_\pi J_{\bar\pi}-J_{\bar\pi}]\,d\eta_\pi$ (29); the sup-norm bound $\|J_\pi-J^*\|_\infty\le(1-\gamma)^{-1}\|J_\pi-TJ_\pi\|_\infty$ (26); the occupancy-weighted inequality $(1-\gamma)\int(J_\pi-J^*)\,d\rho\le\int(J_\pi-TJ_\pi)\,d\eta_{\pi^*}$ from the proof of part (b); and the contraction step $\|J-J^*\|\le(1-\gamma)^{-1}\|J-TJ\|$ from the proof of part (c).

Significance

Theorem 4 is what turns the paper's gradient-dominance theorem into a usable statement: with part (b), the constant in Theorem 2 is bounded by the worst-case likelihood ratio between the optimal policy's state distribution and the initial distribution, a quantity that can be checked without knowing the policy class. Part (a) shows that in finite problems any fully supported initial distribution suffices, and part (c) gives a route through weighted norms, used in the paper for optimal stopping (Lemma 13).

The results are proved in the paper. None of them is machine-checked. The mission produces a general-state-space formalization of the discounted cost MDP (kernels, occupancy measures, Bellman operators, measurable selection) together with the performance difference identity on measurable state spaces; existing formal developments of policy gradient theory on the platform are for finite MDPs only. The occupancy-measure and Bellman-operator layer is shared with the other missions of this series.

Difficulty

The argument for part (b) is short on paper, but each step is a measure-theoretic statement about infinite-horizon objects. The performance difference identity (29) exchanges an infinite discounted sum with integration against the chain's laws and needs the occupancy measure to be built from the $t$-step kernels of the controlled chain. The change of measure from $\eta_{\pi^*}$ to $\rho$ needs the Bellman error $J_\pi-TJ_\pi$ to be nonnegative and integrable; its measurability is not automatic, because $TJ$ is a pointwise minimum over uncountably many actions, and is supplied by the measurable selection assumption. Part (c) needs the fixed-point property $TJ^*=J^*$ of the optimal cost-to-go, which again rests on measurable selection.

Formalization scope

All statements use one Lean layer: MDP S A with measurable spaces S, A (a generalization of the paper's Borel subsets of Euclidean spaces), the cost and kernel given on all of $\mathcal S\times\mathcal A$, measurable stationary policies MPolicy S A, and costToGo, occupancy, loss, bellmanPi, bellmanOpt. The paper prints the Bellman operators (3)–(4) without the discount factor; every later use includes it, and so does the formalization. The optimal policy is a binder πstar with IsOptimal M πstar. Assumptions 1 and 2 of the paper are standing hypotheses of every main statement.

The coefficient $\kappa_\rho$ is never formed as a number: "$\kappa_\rho\le X$" is the predicate IsConcBound M Θ πθ πstar X, which says that $X$ satisfies (13); because the right-hand side of (13) is nondecreasing in the scalar, the two are equivalent. Part (b) quantifies over every $C$ with $\eta_{\pi^*}\le C\rho$ setwise, which is equivalent to $\|d\eta_{\pi^*}/d\rho\|_\infty\le C$; a real-valued essential supremum is avoided because it reads $0$ exactly when the paper's bound is infinite. Part (a) assumes $\rho(s)>0$ for every state, since otherwise $1/\min\rho$ is $+\infty$ on paper and $0$ in Lean. Part (c) requires the norm comparison (21) on all bounded measurable functions, as its proof uses it on $J-J^*$ and $J-TJ$, and encodes "a norm" by subadditivity, the one property used.

A formalization in which (13) or the occupancy-weighted inequality is assumed, or in which $\kappa_\rho$ is a junk value of an empty infimum, would make the goal trivial; neither is used.

Contributions are welcome on every milestone, in particular on the performance difference identity and the measurability of the cost-to-go and of $TJ$, which are reusable for any discounted MDP on a measurable state space.

Selected references

• J. Bhandari, D. Russo, Global Optimality Guarantees for Policy Gradient Methods, Operations Research, 2024; cited version arXiv:1906.01786v3, 2022. https://arxiv.org/abs/1906.01786v3 (DOI 10.1287/opre.2021.0014)
• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• B. Scherrer, M. Geist, Local Policy Search in a Convex Space and Conservative Policy Iteration as Boosted Policy Search, ECML PKDD 2014. https://arxiv.org/abs/1306.1520
• A. Agarwal, S. Kakade, J. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22, 2021. https://arxiv.org/abs/1908.00261
• D. Bertsekas, Dynamic Programming and Optimal Control, Athena Scientific, 1995.

Motivation

Policy gradient methods optimize a parameterized policy by gradient descent on its expected total cost. They are a staple of reinforcement learning and of simulation-based optimization in operations research, but the objective is nonconvex in the policy parameters, and the standard theory guarantees convergence only to a stationary point. J. Bhandari and D. Russo (arXiv:1906.01786v3, Operations Research, 2024, DOI 10.1287/opre.2021.0014) identify structural conditions under which every stationary point is globally optimal.

Their first result (Theorem 1) requires the policy class to be closed under policy improvement. That excludes many classes used in practice, where it is known only that some member of the class is optimal: base-stock policies in finite-horizon inventory control are the standard example (Bertsekas, Dynamic Programming and Optimal Control, 1995). For stationary policy classes, containing an optimal policy is not enough: the paper's Example 1 has a policy class that contains the optimal policy, and policy gradient still gets stuck in a bad local minimum. Theorem 3 shows that for finite-horizon problems with a non-stationary policy class (separate parameters for each period), containing an optimal policy suffices, together with a single-period regularity condition imposed only at the optimal cost-to-go. This mission formalizes Theorem 3.

Setting

A Markov decision process consists of a state space $\mathcal S$, nonempty feasible action sets $\mathcal A_s$, a bounded measurable cost $g(s,a)$, a transition kernel $P(\cdot\mid s,a)$, a discount factor $\gamma\in(0,1)$ and an initial distribution $\rho$. A policy is a measurable map $\pi$ with $\pi(s)\in\mathcal A_s$; $\Pi$ is the set of all of them. The cost-to-go is $J_\pi(s)=\mathbb E^\pi_s[\sum_{t\ge0}\gamma^t g(s_t,\pi(s_t))]$, the loss is $\ell(\pi)=(1-\gamma)\int J_\pi\,d\rho$, and the discounted state-occupancy measure is $\eta_\pi=(1-\gamma)\sum_{t\ge0}\gamma^tP^\pi_\rho(s_t\in\cdot)$. An optimal policy $\pi^*$ has $J_{\pi^*}\le J_\pi$ pointwise for all $\pi\in\Pi$; $J^*=J_{\pi^*}$. With the Bellman operator $(T_\pi J)(s)=g(s,\pi(s))+\gamma\int J(s')P(ds'\mid s,\pi(s))$, the weighted policy-iteration objective is

$$\mathcal B(\bar\pi\mid\eta,J)=\int (T_{\bar\pi}J)(s)\,\eta(ds).$$

A parameterized policy class is $\Pi_\Theta=\{\pi_\theta:\theta\in\Theta\}$ for a convex $\Theta\subseteq\mathbb R^d$, and $\ell(\theta)=\ell(\pi_\theta)$. A point $\theta\in\Theta$ is stationary for $\min_\Theta f$ if $f$ is differentiable at $\theta$ and $\langle\nabla f(\theta),\theta'-\theta\rangle\ge0$ for all $\theta'\in\Theta$.

The finite-horizon structure (Condition 3) embeds a time-inhomogeneous problem in this discounted formulation: the states split into stages $\mathcal S_1,\dots,\mathcal S_H,\mathcal S_{H+1}$; from a state in $\mathcal S_h$, $h\le H$, every feasible action leads to $\mathcal S_{h+1}$; and $\mathcal S_{H+1}=\{\tau\}$ is a costless absorbing state. The parameter is a concatenation $\theta=(\theta_1,\dots,\theta_H)$, the parameter set is a product $\Theta=\Theta_1\times\cdots\times\Theta_H$, and on $\mathcal S_h$ the action $\pi_\theta(s)$ depends only on $\theta_h$. The stage objectives are $\mathcal B_h(\bar\theta_h\mid\eta,J)=\int_{\mathcal S_h}(T_{\pi_{\bar\theta}}J)\,d\eta$.

Condition 4 asks that for every $\eta\in\{\eta_\pi:\pi\in\Pi_\Theta\}$, the problem $\min_{\theta\in\Theta}\mathcal B(\theta\mid\eta,J^*)$ has no suboptimal stationary points. Assumption 3 asks that $\eta_\pi\ll\rho$ for every $\pi\in\Pi_\Theta$. Condition 0 asks that the policy-iteration objective be continuously differentiable in the parameters.

Formalization targets

Goal: Theorem 3 (p. 17)

Under Conditions 0, 3 and 4 and Assumption 3, if $\pi_{\theta^*}$ is an optimal policy for some $\theta^*\in\Theta$, then every stationary point $\theta$ of $\ell$ on $\Theta$ satisfies

$$\ell(\pi_\theta)=\ell(\pi^*).$$

Milestones

1. Lemma 6 (policy gradient theorem): $\nabla\ell(\theta)=\nabla_{\bar\theta}\mathcal B(\bar\theta\mid\eta_{\pi_\theta},J_{\pi_\theta})|_{\bar\theta=\theta}$.
2. Lemma 17 (balance equation): $\eta_\pi(\mathcal M)=\int[(1-\gamma)\rho(\mathcal M)+\gamma P(\mathcal M\mid s,\pi(s))]\,\eta_\pi(ds)$.
3. The stage-wise balance equation: for $\mathcal M\subseteq\mathcal S_{h+1}$, $\eta_\pi(\mathcal M)=(1-\gamma)\rho(\mathcal M)+\gamma\int_{\mathcal S_h}P(\mathcal M\mid s,\pi(s))\,\eta_\pi(ds)$.
4. Separability (30): $\theta$ minimizes $\mathcal B(\cdot\mid\eta,J)$ over $\Theta$ iff each $\theta_h$ minimizes $\mathcal B_h(\cdot\mid\eta,J)$ over $\Theta_h$.
5. Stage-wise stationarity (31): $\theta$ is stationary for $\ell$ iff each $\theta_h$ is stationary for $\mathcal B_h(\cdot\mid\eta_{\pi_\theta},J_{\pi_\theta})$ on $\Theta_h$.
6. Lemma 1: $\pi\in\arg\min_{\Pi}\ell$ iff $J_\pi=J^*$ $\rho$-almost surely.

Significance

Theorem 3 covers finite-horizon dynamic programs in which a structured class of time-varying policies is known to contain an optimal policy, but is not closed under policy improvement: the paper's Example 8, multi-period inventory control with base-stock policies, is the motivating case. Policy gradient on such a class has no suboptimal stationary points, so any method that finds a stationary point finds a globally optimal policy, optimal among all policies and not only within the class. Condition 4 involves only the Bellman objective of the optimal cost-to-go $J^*$, which often has regularity (for instance convexity) that the cost-to-go of an arbitrary policy lacks.

The result is proved in the paper. To our knowledge no part of it, nor the policy gradient theorem for deterministic policies on general state spaces, has a machine-checked proof. Formalizing it requires a measure-theoretic treatment of occupancy measures, the stage-wise decomposition of the weighted policy-iteration objective, and the backward induction of App. D.2.

Difficulty

The obvious approach reasons stage by stage directly on $\ell$, but $\ell$ couples the stages: changing $\theta_h$ changes the distribution of states visited after stage $h$. The paper's argument instead passes through the policy gradient theorem, which turns stationarity of $\ell$ into stationarity of single-period problems weighted by the occupancy measure of the current policy. These single-period problems involve $J_{\pi_\theta}$, while Condition 4 speaks about $J^*$; relating them requires a backward induction over stages in which almost-sure equality $J_{\pi_\theta}=J^*$ on stage $h+1$ is transported to stage $h$ through the balance equation. This step needs the occupancy measures of all policies in the class, including policies other than $\pi_\theta$, to be equivalent to $\rho$, which is where Assumption 3 enters. The naive variant with a stationary policy class fails (Example 1).

Formalization scope

The state and action spaces are arbitrary measurable spaces (the paper takes Borel subsets of Euclidean spaces; no argument uses that structure). Cost and kernel are given on all state-action pairs; the cost is bounded. Policies are deterministic, stationary and measurable; parameters live in EuclideanSpace ℝ (Fin d), so gradients and norms are Euclidean. $J^*$ is never defined as an infimum: an optimal policy $\pi^*$ is a hypothesis, with $J^*=J_{\pi^*}$. Stages and sub-vectors are numbered from $1$ by a measurable stage index and a block index on coordinates; the product structure of $\Theta$ is encoded as closure under exchanging one block.

Hypotheses beyond the printed sentence of Theorem 3, all disclosed in the item statements: Assumption 3 (announced on p. 17 as required, used in the proof); Condition 0 (needed for Lemma 6, which the proof invokes), in a joint form that the proof of Lemma 6 uses and that implies the printed partial-map form; the standing Assumptions 1 and 2 of §2; and, inside Condition 4, differentiability of $\theta\mapsto\mathcal B(\theta\mid\eta,J^*)$ on $\Theta$, the premise of Definition 1. The Bellman operators carry the factor $\gamma$ omitted in the printed (3)–(4). The stage-wise balance equation is stated for $h<H$; the printed range $h\le H$ fails at the absorbing state.

A formalization in which the goal assumes the stage-wise characterization (31), the balance equation, or $J_{\pi_\theta}=J^*$ on any stage is not Theorem 3; neither is one where "contains an optimal policy" means optimal only within $\Pi_\Theta$. Stationarity includes differentiability, so a junk zero gradient never makes a point stationary.

Needed infrastructure: occupancy measures as series of iterated kernels and their balance equation, the cost-to-go as a bounded measurable function, the performance difference identity, the policy gradient theorem, and the decomposition of integrals over the stage partition. The occupancy-measure and policy gradient results are reusable for every mission of this series; contributions of these general lemmas are welcome.

Selected references

• J. Bhandari, D. Russo, Global Optimality Guarantees for Policy Gradient Methods, arXiv:1906.01786v3, 2022; Operations Research, 2024. https://arxiv.org/abs/1906.01786 , https://doi.org/10.1287/opre.2021.0014
• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML, 2002. https://dl.acm.org/doi/10.5555/645531.656005
• I. Osband, B. Van Roy, D. Russo, Z. Wen, Deep Exploration via Randomized Value Functions, JMLR 20, 2019. https://jmlr.org/papers/v20/18-339.html
• D. Silver, G. Lever, N. Heess, T. Degris, D. Wierstra, M. Riedmiller, Deterministic Policy Gradient Algorithms, ICML, 2014. https://proceedings.mlr.press/v32/silver14.html
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Athena Scientific, 1995. https://www.athenasc.com/dpbook.html