Machine Learning

Motivation

Blackwell approachability is the vector-payoff analogue of von Neumann's minimax theorem. In a repeated game where each round's outcome is a vector $u(x_t, y_t) \in \mathbb R^d$, a player wants the running average of these vectors to converge to a target set $S$, whatever the opponent does. Blackwell (1956) showed when this is possible, and approachability has since become a standard tool for calibrated forecasting, regret minimization with respect to general benchmarks, and learning in games.

Online linear optimization (OLO) is the problem of choosing points $\theta_t$ in a fixed decision set $\mathcal K$ against a sequence of linear losses $\langle f_t, \cdot\rangle$, with performance measured by regret against the best fixed point in hindsight. Algorithms with regret $o(T)$ — "no-regret" algorithms such as online gradient descent (Zinkevich, 2003) — are among the most studied objects of machine learning.

Abernethy, Bartlett and Hazan (COLT 2011) showed that the two problems are algorithmically equivalent: each can be converted into the other with explicit control of the rates. This mission covers the direction from OLO to approachability.

Timeline:

• 1956: Blackwell proves the approachability theorem for convex sets, via a geometric projection strategy.
• 2003: Zinkevich introduces online gradient descent, a no-regret algorithm for any bounded convex decision set.
• 2009: Even-Dar, Kleinberg, Mannor and Mansour state approachability in the response-satisfiability form (as cited on p. 32 of the 2011 paper).
• 2011: Abernethy, Bartlett and Hazan give the two reductions, with explicit rates, and apply them to efficient calibration.

Setting

A Blackwell instance $(\mathcal X, \mathcal Y, u, S)$ consists of compact convex sets $\mathcal X \subseteq \mathbb R^n$, $\mathcal Y \subseteq \mathbb R^m$, a payoff $u : \mathcal X \times \mathcal Y \to \mathbb R^d$ that is affine in each argument (biaffine), and a closed convex target set $S \subseteq \mathbb R^d$. Write $\mathtt{dist}(z, U) = \inf_{w \in U}\|z - w\|$ for the Euclidean distance to a set, and $B_2(r)$ for the closed Euclidean ball of radius $r$.

A halfspace oracle takes a halfspace $H = \{z : \langle a, z\rangle \le c\}$ and returns a point $\mathcal O(H) \in \mathcal X$; it is valid if for every halfspace $H \supseteq S$, $u(\mathcal O(H), y) \in H$ for all $y \in \mathcal Y$.

A set $X \subseteq \mathbb R^d$ is a cone if $\alpha z \in X$ for all $z \in X$, $\alpha \ge 0$. For $K \subseteq \mathbb R^d$, $\mathtt{cone}(K) = \{\alpha x : \alpha \ge 0, x \in K\}$, and the polar cone of $C$ is $C^0 = \{\theta : \langle \theta, x\rangle \le 0 \ \forall x \in C\}$.

An OLO algorithm $\mathcal L$ maps past loss vectors $(f_1, \dots, f_{t-1})$ to a point $\theta_t \in \mathcal K$, and its regret is

$$\mathrm{Regret}_T = \sum_{t=1}^T \langle f_t, \theta_t\rangle - \min_{\theta \in \mathcal K} \sum_{t=1}^T \langle f_t, \theta\rangle .$$

Algorithm 2 runs $\mathcal L$ on $\mathcal K = S^0 \cap B_2(1)$ when $S$ is a cone: at round $t$ it sets $\theta_t = \mathcal L(f_1, \dots, f_{t-1})$, plays $x_t = \mathcal O(\{z : \langle \theta_t, z\rangle \le 0\})$, observes $y_t \in \mathcal Y$, and feeds $f_t = -u(x_t, y_t)$ back to $\mathcal L$.

When $S$ is compact but not a cone, it is lifted: with $\kappa = \max_{s\in S}\|s\|$ and $\kappa \oplus z \in \mathbb R^{d+1}$ the concatenation, put $u'(x, y) = \kappa \oplus u(x, y)$ and $S' = \mathtt{cone}(\{\kappa\} \times S)$, and run Algorithm 2 on $(\mathcal X, \mathcal Y, u', S')$.

Formalization targets

Goal: Corollary 18 (p. 39)

For a Blackwell instance with $S$ nonempty and compact, any valid halfspace oracle for the lifted instance, any OLO algorithm with values in $\mathcal K' = (S')^0 \cap B_2(1)$, any $T \ge 1$ and any $y_1, \dots, y_T \in \mathcal Y$, the run of Algorithm 2 on the lifted instance satisfies

$$\mathtt{dist}\Big(\frac1T\sum_{t=1}^T u(x_t,y_t), S\Big) \le 2\,\mathtt{dist}\Big(\frac1T\sum_{t=1}^T u'(x_t,y_t), S'\Big) \le \frac2T\,\mathrm{Regret}_T .$$

The bound holds for every $T$ and every adversary, with no rate assumed for $\mathcal L$; a no-regret $\mathcal L$ then gives approachability.

Milestones

1. Lemma 13 (p. 35): for a nonempty convex cone $C$, $\mathtt{dist}(x, C) = \max_{\theta \in C^0 \cap B_2(1)} \langle \theta, x\rangle$.
2. Theorem 17 (p. 38): if $S$ is a cone, Algorithm 2 achieves $\mathtt{dist}\big(\frac1T\sum_t u(x_t,y_t), S\big) \le \mathrm{Regret}(\mathcal L_{\mathcal K}; f_{1:T})/T$.
3. Lemma 14 (p. 35): for nonempty compact convex $\mathcal K$, $\kappa = \max_{\mathcal K}\|\cdot\|$ and $x \notin \mathcal K$, $\mathtt{dist}(\kappa\oplus x, \mathtt{cone}(\{\kappa\}\times\mathcal K)) \le \mathtt{dist}(x, \mathcal K) \le 2\,\mathtt{dist}(\kappa\oplus x, \mathtt{cone}(\{\kappa\}\times\mathcal K))$.

Significance

The result. Corollary 18 turns any no-regret algorithm into an approachability strategy for a compact convex target, provided a valid halfspace oracle is available, with rate $2\,\mathrm{Regret}_T/T$. Combined with online gradient descent it gives an $O(1/\sqrt T)$ approachability rate, and through the choice of OLO algorithm it lets approachability inherit the computational efficiency of online learning. The paper uses this route to build an efficient calibrated forecaster (Section 5). Together with the converse reduction (Theorem 16), it shows that the two problems are equivalent.

Formalizing it. The results are proved in the paper; none of them has been machine-checked. Formalizing them requires the conic duality formula for distances (Lemma 13), a quantitative lifting lemma (Lemma 14) and the bookkeeping of an interactive protocol. The proof of Lemma 14 on the page is a sketch: it refers to an undefined point and uses a triangle-similarity argument, so a complete proof is new work.

Difficulty

The reduction's core is Lemma 13: the distance to a cone is a maximum of a linear function over the polar cone's unit ball. Lemma 13 needs projection onto a cone in Euclidean space; for a non-closed cone the projection may not exist, and the argument must go through the closure. The lifting Lemma 14 is a geometric statement whose page proof relies on a picture and an undefined point, so the factor 2 has no complete written argument. Finally, connecting the average lifted payoff to the lift of the average payoff, and the halfspace guarantee $\langle\theta_t, f_t\rangle \ge 0$ to the regret, requires keeping the round indexing and the oracle's validity domain exactly aligned.

Formalization scope

All spaces are EuclideanSpace ℝ (Fin d). The concatenation $\kappa\oplus z$ lives in EuclideanSpace ℝ (Fin (d+1)) with coordinate 0 equal to $\kappa$, so $\|\kappa\oplus z\|^2 = \kappa^2 + \|z\|^2$; a product type with the sup norm would change every distance and is ruled out. Distances are Metric.infDist. The polar cone uses the paper's sign ($\le 0$), the negative of Mathlib's innerDual. A halfspace is the pair $(a, c)$; a valid oracle must answer every halfspace containing $S$, including $a = 0$, not only the halfspaces the algorithm happens to query. The OLO algorithm is a map from histories Fin t → ℝᴰ with values in $S^0 \cap B_2(1)$ at every history. Rounds are $t = 1, \dots, T$, and the run of Algorithm 2 is given as hypotheses on sequences $\theta, x, f$, which exist and are unique by recursion. The minimum in the regret and $\kappa$ are written as sInf/sSup of images over nonempty compact sets, where they are attained.

Hypotheses added relative to the page: $S \neq \emptyset$ and $T \ge 1$ in the goal; $C \ne \emptyset$ in Lemma 13 (the empty set is a cone under Definition 11 and the identity fails for it); $\mathcal K \ne \emptyset$ in Lemma 14. Corrected misprints, each disclosed in the item's note: "$\mathrm{Regret}_T(\mathcal A)$" in Corollary 18 and (9) denotes the regret of the OLO algorithm $\mathcal L$ on the lifted losses; Lemma 14's "$\mathcal K \subseteq \mathcal H$" has a stray $\mathcal H$; $\kappa$ is the maximal norm of the set, not its diameter. The oracle in the goal is a valid oracle for the lifted instance, which is what applying Algorithm 2 to $(\mathcal X, \mathcal Y, u', S')$ requires.

A formalization in which the oracle is valid only at the run's own queries, the OLO algorithm is unconstrained, the regret's minimum ranges over all of $\mathbb R^{d+1}$, or the middle term of the goal is dropped, is a different statement and is ruled out.

The development needs: the dual formula for the distance to a convex cone, nearest-point projection onto closed convex sets (in Mathlib), compactness of polar-cone slices, and finite sums of biaffine payoffs. The cone layer (Lemma 13) is reusable for the converse direction of the paper and for conic duality generally. Proofs of any milestone, and of the bridge from an oracle for the original instance to one for the lifted instance, are welcome.

Selected references

• J. Abernethy, P. L. Bartlett, E. Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, JMLR W&CP 19 (COLT 2011), pp. 27–46. https://proceedings.mlr.press/v19/abernethy11b.html
• D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6(1), 1956, pp. 1–8. https://doi.org/10.2140/pjm.1956.6.1
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf

Motivation

Policy iteration alternates two steps: evaluate the current policy, then replace it by a policy that is greedy with respect to the evaluated action values. The policy improvement theorem guarantees that each greedy step does not make the policy worse, and that the process stops only at an optimal policy. When the action values are estimated from experience rather than computed from a model, as in Monte Carlo control, a greedy policy is a problem: it never tries the actions it does not currently prefer, so their values are never re-estimated. Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., 2018), §5.4, resolve this without the unrealistic assumption of exploring starts by moving the policy only toward a greedy one, to an ε-greedy policy that keeps every action's probability at least ε/|A|.

The question this mission formalizes is whether policy iteration still works under that restriction. The book's answer (pp. 101–102) is yes, in a precise sense: an ε-greedy step never makes an ε-soft policy worse, and it fails to make it strictly better only when the policy is already the best among all ε-soft policies. This is the dynamic-programming fact that justifies on-policy first-visit Monte Carlo control for ε-soft policies, and more broadly every ε-greedy on-policy control scheme that is analysed with exact action values.

Setting

A finite Markov decision process has a finite state set S, a finite nonempty action set A used in every state, a finite reward set R ⊂ ℝ and dynamics p(s′, r | s, a) ≥ 0 with $\sum_{s', r} p(s', r \mid s, a) = 1$. A policy π gives, for each state s, a probability distribution π(· | s) on A. With a discount rate $0 \le \gamma < 1$, the state value $v_\pi(s)$ is the expected discounted return $\mathbb E_\pi[\sum_{k \ge 0} \gamma^k R_{t+k+1} \mid S_t = s]$, and the action value is

$$q_\pi(s, a) = \sum_{s', r} p(s', r \mid s, a)\,[r + \gamma v_\pi(s')].$$

For ε > 0, a policy is ε-soft if $\pi(a \mid s) \ge \varepsilon/|A|$ for all s and a. A policy π′ is ε-greedy with respect to $q_\pi$ if at each state some maximizer $A^*(s)$ of $q_\pi(s, \cdot)$ receives probability $1 - \varepsilon + \varepsilon/|A|$ and every other action receives $\varepsilon/|A|$; ties among maximizers are broken arbitrarily. A policy π is optimal among the ε-soft policies if it is ε-soft and $v_{\pi''}(s) \le v_\pi(s)$ for every ε-soft π″ and every state s.

The book's analysis uses a new environment with the same states, actions and rewards, in which with probability 1 − ε the chosen action is executed and with probability ε a uniformly random action replaces it:

$$\tilde p(s', r \mid s, a) = (1 - \varepsilon)\, p(s', r \mid s, a) + \sum_{a'} \frac{\varepsilon}{|A|}\, p(s', r \mid s, a').$$

Its optimal value function is written $\tilde v_*$.

Formalization targets

Goal: ε-greedy improvement with the equality case

For $0 \le \gamma < 1$, $0 < \varepsilon \le 1$, an ε-soft policy π and any ε-greedy policy π′ with respect to $q_\pi$,

$$v_{\pi'}(s) \ge v_\pi(s) \quad \text{for all } s, \qquad \text{and} \qquad v_{\pi'} = v_\pi \;\Longrightarrow\; \pi, \pi' \text{ are optimal among the ε-soft policies}.$$

The goal is stated in terms of the original MDP and ε-soft policies only; the new environment appears only in the milestones.

Milestones

1. Policy improvement theorem for stochastic policies (4.7)–(4.8), p. 78: $\sum_a \pi'(a \mid s) q_\pi(s, a) \ge v_\pi(s)$ for all s implies $v_{\pi'} \ge v_\pi$, strictly at every state where the hypothesis is strict.
2. Eq. (5.2), pp. 101–102: $\sum_a \pi'(a \mid s) q_\pi(s, a) = \frac{\varepsilon}{|A|}\sum_a q_\pi(s, a) + (1-\varepsilon)\max_a q_\pi(s, a) \ge v_\pi(s)$.
3. Characterization, p. 102: an ε-soft π is optimal among ε-soft policies if and only if $v_\pi = \tilde v_*$.
4. Uniqueness, p. 102: $\tilde v_*$ is the unique solution of the Bellman optimality equation with the altered transition probabilities $\tilde p$, and that equation splits as $(1-\varepsilon)\max_a(\cdot) + \frac{\varepsilon}{|A|}\sum_a(\cdot)$.
5. Fixed-point equation, p. 102: if $v_{\pi'} = v_\pi$, then $v_\pi(s) = (1-\varepsilon)\max_a q_\pi(s, a) + \frac{\varepsilon}{|A|}\sum_a q_\pi(s, a)$.

Significance

The result is what makes ε-greedy on-policy control a form of generalized policy iteration: monotone improvement at every step, and a characterization of where the process can stop. It also locates precisely what is lost by exploring, namely that the fixed point is optimal among ε-soft policies, not among all policies. The value $\tilde v_*$ of the new environment is the benchmark against which ε-greedy methods converge when action values are exact.

The book presents the argument informally and states the stochastic policy improvement theorem without proof ("we will not go through the details", p. 79). A formalization supplies the missing proof of the stochastic case, the identification of the best ε-soft policy value with the optimal value of a modified MDP, and the uniqueness of that value. As far as a search of the platform shows, no statement about ε-soft or ε-greedy policies has been formalized there; existing finite-MDP results (Bellman optimality in the Foundations of Machine Learning and Bertsekas series) use different reward models and do not cover the modified environment.

Difficulty

The improvement half follows from (5.2) and the policy improvement theorem, but both need work in the return-based model: the theorem requires comparing infinite discounted sums under two different Markov chains, and (5.2) uses the identity $v_\pi(s) = \sum_a \pi(a \mid s) q_\pi(s, a)$, which is a theorem about returns, not a definition. The equality half is where the obvious argument fails. The deterministic-policy argument of Chapter 4 shows that an unimproved greedy policy satisfies the ordinary Bellman optimality equation; here the unimproved policy satisfies a different equation, and nothing in the original MDP identifies its solution with the best ε-soft value. That identification needs two further facts: every policy of the new environment corresponds to an ε-soft policy of the original one with the same values, and conversely (at ε = 1 only the uniform policy is ε-soft); and the altered optimality equation has exactly one solution.

Formalization scope

Everything is stated in the namespace SuttonBartoRL.EpsSoft on a finite MDP with four-argument dynamics, one finite nonempty action set for all states (so $|A(s)| = |A|$, the book's footnote 3, p. 48), and a finite reward set. The conventions are:

• $v_\pi$ is defined from expected discounted returns as $\sum_k \gamma^k (P_\pi^k r_\pi)(s)$ with $0 \le \gamma < 1$; Bellman equations are theorems, never definitions. $q_\pi$ is the one-step lookahead (4.6) on this $v_\pi$.
• $\tilde v_*$ is the supremum of the new environment's policy values over all stochastic policies, a bounded family for $\gamma < 1$.
• ε ranges over (0, 1]: the book requires ε > 0, and for ε > 1 no ε-soft policy exists. The equality in (5.2) is stated without the book's intermediate division by 1 − ε, so the case ε = 1 is included.
• "Any ε-greedy policy" is encoded by quantifying over every choice of maximizer at every state.
• "Optimal among ε-soft policies" means ε-soft and pointwise at least as good as every ε-soft policy.

Defining $v_\pi$ as the solution of the Bellman expectation equation, or $\tilde v_*$ as the solution of the altered optimality equation, would make milestones 3–5 and the goal's equality half hold by definition; the formalization does neither. The goal is not the statement "$v_{\pi'} \ge v_\pi$" alone: the equality case is part of the book's claim and part of the goal.

The finite-MDP definitions duplicate those of other missions in this series and are expected to be merged later. Useful contributions include the Neumann-series identity $v_\pi = (I - \gamma P_\pi)^{-1} r_\pi$, the Bellman expectation equation, the contraction property of Bellman operators, and the correspondence between policies of the new environment and ε-soft policies of the original one; these are reusable for the other finite-MDP missions of the series.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §4.2 (pp. 76–79) and §5.4 (pp. 100–103). http://incompleteideas.net/book/the-book-2nd.html
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960 (policy iteration).
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, doi:10.1002/9780470316887.

Motivation

Many statistical procedures minimize an average observed loss. This treats two candidates with the same average as equally attractive even when one has much more variable losses across the sample. Adding a multiple of the empirical standard deviation can distinguish them, but the resulting objective need not be convex even when each individual loss is convex. Duchi and Namkoong study a distributionally robust alternative: they maximize expected loss over a small neighborhood of the empirical distribution, then minimize that worst-case value. Their paper identifies when this convex robust value agrees exactly with the mean-plus-standard-deviation expression and how far apart the two can be otherwise. The finite-sample statement is Theorem 1 of the pinned preprint.

The relation matters to someone choosing a loss function for stochastic optimization. The variance expression has a direct statistical interpretation, while the robust expression preserves convexity in a decision parameter when the loss is convex. Theorem 1 makes the relationship quantitative for a single bounded random variable, before the paper turns to uniform guarantees over whole classes of losses. This mission isolates that first step and its finite optimization model.

Setting

Take observed real values $z_1,\ldots,z_n$, with $n\ge1$. Their empirical mean and empirical variance are

$$\bar z=\frac1n\sum_{i=1}^n z_i,\qquad s_n^2=\frac1n\sum_{i=1}^n z_i^2-\bar z^2.$$

The variance uses $1/n$, not the unbiased-estimator factor $1/(n-1)$. A weight vector $p=(p_1,\ldots,p_n)$ is feasible when its entries are nonnegative, sum to one, and satisfy

$$\frac12\sum_{i=1}^n(np_i-1)^2\le\rho,\qquad \rho\ge0.$$

This is the paper's χ² neighborhood $\mathcal P_n(\rho)$ of the uniform empirical weights. Its robust sample expectation is

$$R_n(z,\rho)=\sup_{p\in\mathcal P_n(\rho)}\sum_{i=1}^n p_i z_i.$$

For a random variable $Z$ with law $P$ supported on $[M_0,M_1]$, write $M=M_1-M_0$ and $\sigma^2=\operatorname{Var}_P(Z)$. An independent sample $Z_1,\ldots,Z_n$ supplies the vector $z$. The paper describes $\mathcal P_n$ through a $\phi$-divergence from the empirical distribution, with $\phi(t)=\tfrac12(t-1)^2$; its finite maximization problem (8) is the weight-vector form used here. The preprint, pp. 2 and 5–7 fixes these conventions.

Formalization targets

Deterministic bound

For every sample in $[M_0,M_1]$, the robust value lies between the empirical mean plus a corrected variance penalty and the full penalty:

$$\left(\sqrt{\frac{2\rho s_n^2}{n}}-\frac{2M\rho}{n}\right)_+\le R_n(z,\rho)-\bar z\le\sqrt{\frac{2\rho s_n^2}{n}}.$$

This is inequality (10). The correction is explicit, so this target records more than an asymptotic approximation.

Exact expansion

When $\sigma^2>0$ and the sample size obeys

$$n\ge\max\left\{5,\frac{M^2}{\sigma^2}\max\{8\sigma,44,44\rho\}\right\},$$

the goal is the high-probability equality

$$\Pr\left\{R_n(Z_{1:n},\rho)\ne\bar Z+\sqrt{\frac{2\rho s_n^2}{n}}\right\}\le\exp\left(-\frac{n\sigma^2}{11M^2}\right).$$

This is Theorem 1's equality (11) with the missing $\rho$-dependent sample-size requirement supplied from the proof. The exact expansion is the mission goal; display (30), inequality (10), and Lemma A.2 form the milestone list, and the exact value under condition (9) is a further statement of the mission.

Significance

The deterministic result states how large the discrepancy between a convex robust risk and a variance penalty can be for any bounded sample. The equality says that, with the stated confidence, no discrepancy remains once the population variance and sample size make the penalty compatible with nonnegative probability weights. These are the numerical facts later sections need when they move from one loss variable to families of losses and minimizers. The claims and constants come from Theorem 1 and Section 2.1.

The paper develops arguments for these results, although its printed (11) needs the correction described below; the statements in this mission have no machine-checked proofs yet. The formalization work includes the finite χ² feasible set, its real supremum, exact handling of tied observations, empirical moments with the paper's normalization, and a product-law event for the probability estimate. The Samson concentration milestone is reusable for other bounded independent-coordinate models. Solvers can also contribute a different route to the corrected exact expansion; the goal concerns the statement, not one chosen argument.

Difficulty

Without the nonnegativity requirement on $p$, optimizing a linear function over the centered Euclidean ball gives the mean plus a standard-deviation term. The candidate weights can become negative when a sample coordinate is far below the mean, so that calculation alone cannot certify the robust value. Condition (9) records precisely when the candidate is feasible. The probability target then needs a quantitative guarantee that the sample variance is large enough often enough, with the stated exponential constant. A pointwise inequality for a fixed sample does not by itself yield that probability estimate. These are separate obligations in Section 2.1 and Appendix A.

Formalization scope

The sample is a function Fin n → ℝ; feasible weights have the same type. chiSqBall, robustSup, empMean, and empVar mirror equations (8) and the definitions on p. 6. Every theorem assumes $n>0$ and $\rho\ge0$, so the weight ball is nonempty and its real supremum is bounded. The high-probability theorem uses a probability measure $P$ on the reals, supported on $[M_0,M_1]$, and the independent product measure on Fin n → ℝ. Its conclusion bounds the measure of the event on which equality fails. The positive population variance hypothesis makes division by $\sigma^2$ and $M^2$ meaningful. The deterministic bounds include every sample in the interval and use $x_+=\max\{x,0\}$.

The paper prints the threshold without $44\rho$ in (11), but its Appendix A invokes the corresponding inequality, and the printed claim fails for sufficiently large $\rho$. The goal includes that term. The paper's route through Lemmas A.1 and A.4 contains misprinted lower-tail and moment claims, so those are not milestones. Lemma A.3's displayed (31b) is also omitted because its correction term has the wrong scaling; the corrected goal stands as a target to establish independently. These discrepancies are detailed in the local moderation notes and the pinned source, pp. 7 and 32–35.

No hypothesis may force the bad event to be empty, and the robust value must optimize over all feasible weights, not a selected optimizer. The supporting definitions are intended for reuse in later missions on uniform variance expansions. Contributions to the finite optimization facts, the concentration statement, and the probability goal are welcome.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv preprint arXiv:1610.02581v3, 2017. Pinned preprint.

Motivation

Many sequential decision problems ask a learner to choose, round after round, a combination of items: a set of $m$ ads out of $d$, a path in a network, a matching. After each choice the learner sees the loss of the items it used, not of those it did not. This is online combinatorial optimization with semi-bandit feedback. It contains the classical adversarial multi-armed bandit (choose one of $d$ arms) and is a standard model in online advertising, routing and ranking.

Chapter 5 of Bubeck and Cesa-Bianchi's monograph arXiv:1204.5721v2 treats this problem with one algorithm, Online Stochastic Mirror Descent (OSMD). Every regret bound in the chapter comes from a single mirror-descent inequality, specialized through the choice of a convex "regularizer". The chapter's capstone, Theorem 5.7, shows that a polynomial regularizer gives pseudo-regret $O(\sqrt{mdn})$ with no logarithmic factor. For $m=1$ this is the minimax-optimal rate of the adversarial bandit, first attained by the INF strategy of Audibert and Bubeck (2009). The semi-bandit version is due to Audibert, Bubeck and Lugosi (2014).

Setting

Vectors live in $\mathbb R^d$. The arm set is a nonempty $\mathcal C\subseteq\{0,1\}^d$ with $\|v\|_1=m$ for every $v\in\mathcal C$, and $\mathcal K=\mathrm{Conv}(\mathcal C)$. An oblivious adversary fixes loss vectors $\ell_1,\dots,\ell_n\in[0,1]^d$. In round $t$ the learner plays a random arm $v_t\in\mathcal C$, pays $\ell_t^\top v_t$, and observes $(\ell_t(1)v_t(1),\dots,\ell_t(d)v_t(d))$. The pseudo-regret is

$$\bar R_n=\mathbb E\sum_{t=1}^n\ell_t^\top v_t-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t^\top x .$$

A Legendre function on $\bar D$, for a nonempty open convex $D$, is a continuous $F:\bar D\to\mathbb R$ that is strictly convex and $C^1$ on $D$ and whose gradient norm tends to $+\infty$ at $\bar D\setminus D$. Its Bregman divergence is $D_F(x,y)=F(x)-F(y)-(x-y)^\top\nabla F(y)$, and its Legendre–Fenchel transform is $F^*(u)=\sup_{x\in\bar D}(x^\top u-F(x))$.

Online Mirror Descent with learning rate $\eta>0$ and vectors $g_t$ starts at $x_1\in\arg\min_{\mathcal K}F$. It then sets $\nabla F(w_{t+1})=\nabla F(x_t)-\eta g_t$ and $x_{t+1}=\arg\min_{y\in\mathcal K}D_F(y,w_{t+1})$. OSMD uses a random estimate $g_t=\tilde\ell_t$ of the loss. In the semi-bandit case it plays $v_t$ with $\mathbb E[v_t\mid x_t]=x_t$ and uses

$$\tilde\ell_t(i)=\frac{\ell_t(i)\,v_t(i)}{x_t(i)}. \tag{5.5}$$

A $0$-potential is a convex, $C^1$, increasing $\psi:(-\infty,a)\to(0,\infty)$ with $\psi(-\infty)=0$, $\psi(a^-)=+\infty$ and $\int_0^1|\psi^{-1}|<\infty$. It defines the Legendre function $F_\psi(x)=\sum_i\int_0^{x_i}\psi^{-1}(s)\,ds$ on $[0,\infty)^d$. With $\psi=\exp$ this is the negative entropy.

Formalization targets

Goal: Theorem 5.7 (p. 80)

For every $0$-potential $\psi$ and non-negative unbiased estimates,

$$\bar R_n\le\frac{\sup_{\mathcal K}F_\psi-F_\psi(x_1)}{\eta}+\frac\eta2\sum_{t=1}^n\sum_{i=1}^d\mathbb E\left[\frac{\tilde\ell_t(i)^2}{(\psi^{-1})'(x_t(i))}\right].$$

For $\psi(x)=(-x)^{-q}$ with $q>1$, the estimate (5.5) and $\eta=\sqrt{\tfrac{2}{q-1}\,m^{1-2/q}/(n\,d^{1-2/q})}$,

$$\bar R_n\le q\sqrt{\tfrac{2}{q-1}\,mdn},\qquad\text{and }\ \bar R_n\le2\sqrt{2mdn}\ \text{ at }q=2.$$

Milestones

1. Lemma 5.1: $F^{**}=F$, $\nabla F^*=(\nabla F)^{-1}$ on $D^*$, and $D_F(x,y)=D_{F^*}(\nabla F(y),\nabla F(x))$.
2. Lemma 5.2: existence, uniqueness and the Pythagorean inequality of Bregman projections.
3. Theorem 5.3: $\sum_t\ell_t(x_t)-\sum_t\ell_t(x)\le\frac{F(x)-F(x_1)}\eta+\frac1\eta\sum_tD_{F^*}(\nabla F(x_t)-\eta\nabla\ell_t(x_t),\nabla F(x_t))$.
4. Theorem 5.5, linear losses, and its corrected general form.
5. Lemma 5.3: $F_\psi$ is Legendre and $D_{F_\psi^*}(u,v)\le\frac12\sum_i\psi'(v_i)(u_i-v_i)^2$ for $u\le v$.
6. Theorem 5.6: with the negative entropy, $\bar R_n\le\sqrt{2mdn\ln(d/m)}$.

Significance

Theorem 5.7 is the sharpest semi-bandit bound in the monograph. It shows that removing the $\sqrt{\ln(d/m)}$ factor of the exponential-weights analysis (Theorem 5.6) is a matter of the regularizer, not of a new algorithm. The same OSMD template gives the Euclidean-ball bound of Theorem 5.8 and is reused for bandit convex optimization in Chapter 6. Lemma 5.1, Lemma 5.2 and Theorem 5.3 are the standard mirror-descent toolkit, used throughout online learning and optimization.

All results of the chapter are proved in the book. Lemmas 5.1 and 5.2 are cited from Cesa-Bianchi and Lugosi (2006). None of them is formalized on Prove2Me. The published mirror-descent bound of Bandit Algorithms XII treats linear losses with a comparator inside $D$ and Euclidean-space vectors; it is not Theorem 5.3. The mission adds a machine-checked version of the whole chain, from Legendre duality to the explicit constant $q\sqrt{2mdn/(q-1)}$, with two of the printed statements corrected (below).

Difficulty

The pathwise mirror-descent inequality is a telescoping argument, but several of its steps rest on convex analysis that Mathlib does not package. One is the existence and interior location of Bregman projections onto a set that touches the boundary of $D$. Another is the differentiability of $F^*$ on the open dual space and the identity $\nabla F^*=(\nabla F)^{-1}$. A third is the closed form of $F_\psi^*$ for a potential defined through an improper integral of $\psi^{-1}$.

The probabilistic step is not a martingale argument. Only conditioning on the current iterate $x_t$ is available. The estimate (5.5) divides by $x_t(i)$, so its integrability and unbiasedness have to be derived from the fact that the iterates stay in the open orthant. Finally, the explicit constant requires a Hölder step, $\sum_ix_1(i)^{1-1/q}\le m^{(q-1)/q}d^{1/q}$, and the matching bound $\sum_ix_t(i)^{1/q}\le m^{1/q}d^{1-1/q}$.

Formalization scope

Vectors are Fin d → ℝ. The arm set is a Set of $0/1$ vectors with coordinate sum $m$, and $\mathcal K$ is convexHull ℝ C. Rounds are $t=1,\dots,n$, sums run over Finset.Icc 1 n, and index $0$ is unused. A randomized run is a family of measurable processes $x_t, v_t, \tilde\ell_t, w_t$ on a probability space, with the deterministic OMD recursion holding on every sample path. $\mathbb E[\cdot\mid x_t]$ is the coordinatewise conditional expectation given $\sigma(x_t)$, which is exactly what the book's proofs use. Losses are oblivious, so $\bar R_n\le B$ is stated as "for every $x\in\mathcal K$, $\mathbb E\sum_t\ell_t^\top v_t-\sum_t\ell_t^\top x\le B$". $F^*$ is valued in EReal, and $D_{F^*}$ is evaluated only on the open dual space, where $F^*$ is finite. Wherever an expectation of a possibly non-integrable quantity appears on a right-hand side, its integrability is assumed: the book's bound is then $+\infty$ and trivial, while Lean's integral would be $0$.

Corrections and instantiations, each labelled in the item's Formalization Note:

• Theorem 5.7, corrected misprint. The book prints $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{d^{1-2/q}}}$. The proof (p. 81) gives the stated bound only for $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{n\,d^{1-2/q}}}$, which is stated. At $q=2$ this is $\eta=\sqrt{2/n}$.
• Theorem 5.5, corrected misprint. In the first bound the book prints $\mathbb E[\|x_t-\tilde x_t\|\,\|\tilde g_t\|_*]$. That statement fails for $\ell_t(x)=x^2$ on $[-1,1]$ with $F=x^2/2$ and $\tilde x_t=\pm1$. The version stated uses $\|\nabla\ell_t(\tilde x_t)\|_*$, as the proof's first inequality does. The linear-loss bound is stated as printed.
• Lemma 5.2. "For all $z\in K\cap D$" is read as "for the projection $z$", which lies in $K\cap D$.
• Hypotheses made explicit: $q>1$; non-negativity of the estimates in Theorem 5.6 (used in its proof); unbiasedness $\mathbb E[\tilde\ell_t\mid x_t]=\ell_t$ in the general parts of Theorems 5.6 and 5.7; $\mathcal K\cap(0,\infty)^d\ne\emptyset$ (OMD's requirement $K\cap D\ne\emptyset$); a subgradient selection as an explicit input.
• Theorem 5.6's particular bound uses the book's $\eta=\sqrt{\frac{2m}{nd}\ln\frac dm}$ as printed. There are no O(·) constants in the chapter's statements.

A trivializing formalization would let $\eta$, $x_t$ or the estimate be junk values: an OSMD step at $\eta=0$, a Lean division $x/0=0$, or a regret written as a real infimum over an unbounded set. Here every run is the book's algorithm on the open orthant, and each bound is stated against every comparator in $\mathcal K$.

Reusable beyond this mission: the Legendre/Bregman layer, the OMD run predicate and the $\omega$-potential layer. Proofs of Lemmas 5.1 and 5.2 in this generality would be welcome additions to the library.

Selected references

• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012; arXiv:1204.5721v2. https://arxiv.org/abs/1204.5721
• N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921
• J.-Y. Audibert, S. Bubeck, Regret bounds and minimax policies under partial monitoring, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/audibert10a.html
• J.-Y. Audibert, S. Bubeck, G. Lugosi, Regret in online combinatorial optimization, Mathematics of Operations Research 39(1), 2014. https://doi.org/10.1287/moor.2013.0598

Motivation

In the adversarial (non-stochastic) multi-armed bandit problem a forecaster repeatedly chooses one of $K$ actions while an opponent sets the rewards, and only the reward of the chosen action is revealed. The model was proposed as a way of playing an unknown repeated game: Baños (1968) studied the repeated game in which the player observes only its own payoff, which is exactly the bandit problem against an opponent who reacts to the player's past moves. It is the basic model of online decision making under partial feedback without statistical assumptions, and it underlies regret minimization in games, adversarial routing and online advertising. Chapter 3 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2) collects its fundamental results: the Exp3 forecaster of Auer, Cesa-Bianchi, Freund and Schapire (SIAM J. Comput. 2002), its high-probability variant Exp3.P, and the $\sqrt{nK}$ minimax lower bound.

Setting

There are $K \ge 2$ arms and rounds $t = 1, 2, \dots, n$. At each round an adversary assigns a gain $g_{i,t} \in [0,1]$ to every arm $i$; the forecaster picks an arm $I_t$, possibly at random, and observes only $g_{I_t,t}$. The adversary may be non-oblivious (adaptive): $g_{i,t} = g_{i,t}(I_1,\dots,I_{t-1})$ may depend on the forecaster's past actions. A forecaster rule maps the past actions to a probability vector $p_t$ on the arms, and a run is a sequence of random arms with $I_t \sim p_t$ given the past. The regret is the random variable

$$R_n = \max_{i=1,\dots,K}\sum_{t=1}^n g_{i,t} - \sum_{t=1}^n g_{I_t,t},$$

and, in the loss version $\ell_{i,t} \in [0,1]$, the pseudo-regret is $\overline R_n = \mathbb E\sum_t \ell_{I_t,t} - \min_i \mathbb E\sum_t \ell_{i,t}$. Since the maximum sits inside the expectation, $\overline R_n \le \mathbb E R_n$ in the gain version, and against an adaptive adversary the two can differ.

Exp3 draws $I_t$ from exponential weights $p_{i,t+1} \propto \exp(-\eta_t \tilde L_{i,t})$ of importance-weighted cumulative loss estimates $\tilde L_{i,t} = \sum_{s \le t} \ell_{i,s}\mathbb 1_{I_s = i}/p_{i,s}$. Exp3.P uses biased gain estimates $\tilde g_{i,t} = (g_{i,t}\mathbb 1_{I_t=i} + \beta)/p_{i,t}$ and mixes in the uniform distribution:

$$p_{i,t+1} = (1-\gamma)\frac{\exp(\eta\tilde G_{i,t})}{\sum_k \exp(\eta \tilde G_{k,t})} + \frac{\gamma}{K}, \qquad \tilde G_{i,t} = \sum_{s=1}^t \tilde g_{i,s}.$$

Formalization targets

Goal: Theorem 3.3 (expected regret of Exp3.P)

With $\beta = \sqrt{\ln K/(nK)}$, $\eta = 0.95\sqrt{\ln K/(nK)}$, $\gamma = 1.05\sqrt{K\ln K/n}$, against every adaptive adversary,

$$\mathbb E R_n \le 5.15\sqrt{nK\ln K} + \sqrt{\frac{nK}{\ln K}}.$$

Milestones

• Lemma 3.1: for $\beta \in (0,1]$ and a fixed arm $i$, with probability at least $1-\delta$, $\sum_t g_{i,t} \le \sum_t \tilde g_{i,t} + \ln(\delta^{-1})/\beta$.
• Eq. (3.12): if $\gamma \le 1/2$ and $(1+\beta)K\eta \le \gamma$, then with probability at least $1-\delta$,

$$R_n \le \beta nK + \gamma n + (1+\beta)\eta Kn + \frac{\ln(K\delta^{-1})}{\beta} + \frac{\ln K}{\eta}.$$

• Theorem 3.2: with $\beta = \sqrt{\ln(K\delta^{-1})/(nK)}$, $R_n \le 5.15\sqrt{nK\ln(K\delta^{-1})}$ (3.10); with $\beta = \sqrt{\ln K/(nK)}$, $R_n \le \sqrt{nK/\ln K}\,\ln(\delta^{-1}) + 5.15\sqrt{nK\ln K}$ (3.11), each with probability at least $1-\delta$.
• Theorem 3.1: Exp3 with $\eta = \sqrt{2\ln K/(nK)}$ has $\overline R_n \le \sqrt{2nK\ln K}$ (3.2); with $\eta_t = \sqrt{\ln K/(tK)}$, $\overline R_n \le 2\sqrt{nK\ln K}$ (3.3).
• Lemma 3.2 and Theorem 3.4: for $n \ge K \ge 2$ and every forecaster there is a Bernoulli instance with $\max_i \mathbb E\sum_t Y_{i,t} - \mathbb E\sum_t Y_{I_t,t} \ge \sqrt{nK}/20$.

Significance

The goal bounds the expected regret, not the pseudo-regret, against an opponent that adapts to the forecaster's randomized past choices. A pseudo-regret bound says nothing about $\mathbb E R_n$ in that setting, and the book obtains the expected-regret bound by first proving a high-probability bound valid at every confidence level, (3.11), and integrating its tail. Together with Theorem 3.4 the chapter shows that $\sqrt{nK}$ is the minimax rate of adversarial bandits up to a $\sqrt{\ln K}$ factor. Lemma 3.1, the concentration of biased importance-weighted estimates, holds for any forecaster rule and is the step that turns exponential weights into a high-probability guarantee.

All results are proved in the book. On the formal side, the platform has the pseudo-regret bound of Exp3 against an oblivious adversary (a fixed reward table, Bandit Algorithms V) and an Exp3-IX high-probability bound; it has no Exp3.P, no regret bound against adaptive adversaries and no Bernoulli $\sqrt{nK}/20$ lower bound. This mission adds an explicit model of adaptive adversaries and randomized forecaster runs, and the chapter's statements with the book's exact constants.

Difficulty

Against an adaptive adversary the gains are random and depend on the forecaster's own past draws, so the argument used for a fixed reward table (take expectations of an inequality that holds for every fixed sequence) does not control $\mathbb E R_n$: the maximum over arms does not commute with the expectation. Unbiased estimates do not help either, because the variance of $\ell_{i,t}/p_{i,t}$ is of order $1/p_{i,t}$, which can be arbitrarily large; even with uniform mixing at rate $n^{-1/2}$ the cumulative variance is of order $n^{3/2}$. The bias $\beta$ and the mixing $\gamma$ have to be tuned jointly so that the estimate concentrates while the exponential-weights analysis survives, and the constants $0.95$, $1.05$ and $5.15$ come out of that tuning. The lower bound needs an information-theoretic comparison of a forecaster's behaviour on $K+1$ Bernoulli instances, against forecasters that may be randomized.

Formalization scope

Arms are Fin K with $K \ge 2$; rounds are numbered $1,\dots,n$; logarithms are natural. Action sequences are functions $\mathbb N \to$ Fin K whose entry $0$ is ignored. An adversary is a structure holding values in $[0,1]$ that may depend on the past actions only (gains for Exp3.P, losses for Exp3); a randomized adversary with independent external randomness reduces to this case by conditioning. A run of a forecaster rule $p$ on a probability space is pinned down by the cylinder identity $\mathbb P(I_1 = h_1,\dots,I_t = h_t) = \mathbb P(I_1=h_1,\dots,I_{t-1}=h_{t-1})\,p_t(h)(h_t)$, which determines the law of $(I_1,\dots,I_n)$. "With probability at least $1-\delta$" is $\mathbb P(\text{event}) \ge 1-\delta$ for $\delta \in (0,1)$, and $\mathbb E R_n$ is the Bochner integral of the bounded, measurable regret. The lower bounds use a stochastic model in which the forecaster sees past actions and the rewards of the played arms, and rewards are i.i.d. product Bernoulli.

Constants and conventions:

• Every constant is the book's exact one: $0.95$, $1.05$, $5.15$, $1/20$. No $O(\cdot)$ is involved.
• Exp3.P with $1.05\sqrt{K\ln K/n} > 1$ is outside the box's range $\gamma \in [0,1]$; its vector can then have negative entries, and if it does on a history of positive probability no run exists. This happens only when $n < 1.11\,K\ln K$, where the printed bounds already follow from $R_n \le n$, so the statements are true there whether or not a run exists.
• Corrected misprints: the Exp3 box's $\tilde\ell_{i,s}$ is $\tilde\ell_{i,t}$; the sign in (3.16) is the box's $\exp(+\eta\tilde G)$; the proof of (3.10) says the bound is trivial "if $n \ge 5.15\sqrt{\cdots}$", which should be $n \le$. The statements carry no lower bound on $n$.
• Added standing hypotheses: $K \ge 2$ everywhere, $n \ge K$ in Theorem 3.4 (from the protocol box, p. 6; Theorem 3.4 is false without it), $\beta > 0$ and $p_{i,t} > 0$ in Lemma 3.1.
• Theorem 3.4 is stated as "for every forecaster there is a Bernoulli instance with regret at least $\sqrt{nK}/20$", which implies the book's $\inf\sup$ (3.18).

A trivializing formalization is ruled out: the forecasters are fixed rules of the observed history drawn with fresh randomness, the adversary is not restricted to a fixed sequence, and the lower bounds quantify over all forecasters and exhibit the instance.

Welcome contributions: a reusable construction of runs (existence of a probability space carrying a run for every rule), the supermartingale form of Lemma 3.1, the exponential-weights potential argument, a tail-integration lemma $\mathbb E W \le \int_0^1 \delta^{-1}\mathbb P(W > \ln\delta^{-1})\,d\delta$, and a KL/Pinsker comparison for bandit runs.

Selected references

• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2, doi:10.1561/2200000024
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 2002. doi:10.1137/S0097539701398375
• J.-Y. Audibert, S. Bubeck, Regret bounds and minimax policies under partial monitoring, Journal of Machine Learning Research 11, 2010. jmlr.org/papers/v11/audibert10a
• N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. doi:10.1017/CBO9780511546921

Motivation

Policy gradient methods learn a parameterized policy $\pi(a \mid s, \theta)$ directly, by stochastic gradient ascent on a scalar performance measure $J(\theta)$, instead of deriving the policy from learned action values. They are how reinforcement learning handles continuous action spaces, stochastic optimal policies and prior knowledge built into the policy's form, and they underlie REINFORCE (Williams, 1992) and the actor–critic family. Every such method needs an estimate of $\nabla J(\theta)$. The difficulty is that $J$ depends on $\theta$ in two ways: through the action choices in each state, and through the distribution of states those choices produce. The second effect depends on the unknown environment dynamics.

The policy gradient theorem (Sutton, McAllester, Singh and Mansour, 2000; Marbach and Tsitsiklis, 2001) gives $\nabla J(\theta)$ as an expectation over the on-policy state distribution that involves no derivative of that distribution. Chapter 13 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) states it as Eq. (13.5), proves it in a box for the episodic case (p. 325) and in a second box for the continuing case (pp. 334–335), and builds REINFORCE, REINFORCE with baseline and actor–critic methods on it. This mission formalizes that chapter's theorem and the identities around it, in the book's own model.

Setting

A finite episodic MDP has a finite set $\mathcal S$ of nonterminal states, a terminal state, a finite action set $\mathcal A$, a finite reward set $\mathcal R \subset \mathbb R$ and dynamics $p(s', r \mid s, a)$: for each nonterminal $s$ and action $a$, a probability distribution over next state $s' \in \mathcal S^+ = \mathcal S \cup \{\text{terminal}\}$ and reward $r$. The terminal state is absorbing and pays nothing. Write $p(s' \mid s, a) = \sum_r p(s', r \mid s, a)$ and $r(s, a)$ for the expected reward.

A differentiable policy parameterization assigns to every $\theta \in \mathbb R^{d'}$ and state $s$ a distribution $\pi(\cdot \mid s, \theta)$ over actions, with $\theta \mapsto \pi(a \mid s, \theta)$ differentiable. Under $\pi_\theta$ the nonterminal states form a substochastic chain with matrix $P_\theta(s, s') = \sum_a \pi(a \mid s, \theta) p(s' \mid s, a)$; $\Pr(s \to x, k, \pi) = P_\theta^k(s, x)$. Episodes terminate when $\sum_{k} P_\theta^k(s, s') < \infty$ for all $s, s'$.

There is no discounting ($\gamma = 1$, p. 324). The state value $v_{\pi}(s) = \sum_{k \ge 0} (P_\theta^k r_\theta)(s)$ is the expected total reward from $s$, with $r_\theta(s) = \sum_a \pi(a\mid s,\theta) r(s,a)$; the action value $q_\pi(s,a)$ is the expected total reward after taking $a$ in $s$. The episode starts in a fixed state $s_0$, and the performance is $J(\theta) = v_{\pi_\theta}(s_0)$ (13.4). The expected number of visits to $s$ in an episode is $\eta(s) = \sum_{k \ge 0} \Pr(s_0 \to s, k, \pi)$, and the on-policy distribution is $\mu(s) = \eta(s) / \sum_{s'} \eta(s')$ (9.3).

In the continuing case there is no terminal state, $J(\theta) = r(\pi)$ is the average reward per step (13.15), $\mu$ is the steady-state distribution, and $v_\pi$, $q_\pi$ are differential values, defined from the return $\sum_k (R_{t+k+1} - r(\pi))$ (13.17).

Formalization targets

Goal: the policy gradient theorem, episodic case (13.5)

If episodes terminate under $\pi_{\theta_0}$, then $J$ is differentiable at $\theta_0$ and

$$\nabla J(\theta_0) = \sum_s \eta(s) \sum_a q_\pi(s,a)\, \nabla \pi(a \mid s, \theta_0) = \Big(\sum_{s'} \eta(s')\Big) \sum_s \mu(s) \sum_a q_\pi(s,a)\, \nabla \pi(a \mid s, \theta_0),$$

with $\sum_{s'} \eta(s') \ge 1$. The book writes $\nabla J(\theta) \propto \sum_s \mu(s) \sum_a q_\pi(s,a) \nabla \pi(a \mid s,\theta)$ and names the constant, the average length of an episode, in words (p. 326). The goal states it.

Milestones

1. Exercises 3.18–3.19 with $\gamma = 1$: $v_\pi(s) = \sum_a \pi(a\mid s) q_\pi(s,a)$ and $q_\pi(s,a) = \sum_{s',r} p(s',r\mid s,a)(r + v_\pi(s'))$.
2. The recursion $\nabla v_\pi(s) = \sum_a [\nabla\pi(a\mid s) q_\pi(s,a) + \pi(a\mid s) \sum_{s'} p(s'\mid s,a) \nabla v_\pi(s')]$, including the differentiability of $v_\pi$.
3. The unrolled gradient $\nabla v_\pi(s) = \sum_{x} \sum_{k=0}^\infty \Pr(s \to x, k, \pi) \sum_a \nabla\pi(a\mid x) q_\pi(x,a)$ for every $s$.
4. The theorem with a baseline (13.10): $\sum_a b(s) \nabla \pi(a\mid s,\theta) = 0$, hence $q_\pi$ may be replaced by $q_\pi - b$.
5. The log form behind REINFORCE: where $\pi(\cdot\mid s,\theta) > 0$, $\sum_a q_\pi(s,a) \nabla\pi(a\mid s,\theta) = \sum_a \pi(a\mid s,\theta) q_\pi(s,a) \nabla \ln \pi(a\mid s,\theta)$, and hence $\nabla J(\theta) = (\sum_{s'}\eta(s')) \sum_s \mu(s) \sum_a \pi(a\mid s,\theta) q_\pi(s,a) \nabla \ln \pi(a\mid s,\theta)$, the exact form of $\nabla J \propto \mathbb E_\pi[q_\pi(S_t,A_t) \nabla\pi(A_t\mid S_t,\theta)/\pi(A_t\mid S_t,\theta)]$.
6. Exercise 13.3, (13.9): for the linear soft-max, $\nabla \ln \pi(a\mid s,\theta) = x(s,a) - \sum_b \pi(b\mid s,\theta) x(s,b)$.
7. Exercise 13.4: the eligibility vectors of the Gaussian policy (13.19)–(13.20).
8. The continuing case: under ergodicity, $\nabla r(\pi_\theta) = \sum_s \mu(s) \sum_a \nabla\pi(a\mid s,\theta) q_\pi(s,a)$ with differential $q_\pi$.

Significance

The theorem turns $\nabla J$ into a quantity that can be sampled by following the policy: weighting states by $\mu$ is what visiting them under $\pi$ does, and the log form makes the action sum an expectation over $A_t \sim \pi$. REINFORCE (13.8), REINFORCE with baseline (13.11) and one-step and eligibility-trace actor–critic methods all rest on it, and so does their claim that the expected update is in the direction of the performance gradient (p. 329). The baseline identity is why a learned state value can reduce variance without introducing bias.

The results are proved, in the book and in the literature. What this mission adds is a machine-checked version in the book's model: random episode lengths with $\gamma = 1$, vector parameters $\theta \in \mathbb R^{d'}$, four-argument dynamics, and values defined from expected returns. The platform already has a proved finite-horizon policy gradient theorem (policy_gradient_finite_horizon, with a baseline and log-form companion) for a fixed horizon $T$, a scalar parameter $\theta \in \mathbb R$ and an expected-reward kernel; it does not cover the book's statement. The mission also makes explicit two points the text leaves informal: that episodes terminate, and what exact constant hides behind "$\propto$".

Difficulty

The book's proof is a formal manipulation: differentiate the Bellman equation, substitute it into itself, and "unroll" infinitely often. Two steps are not justified on the page. First, it presupposes that $\nabla v_\pi(s)$ exists; with $\gamma = 1$ the value is an infinite series whose convergence depends on $\theta$ through termination, so differentiability of $v_\pi$ at $\theta_0$ has to be established, and termination is assumed only at $\theta_0$. Second, "repeated unrolling" is a limit: after $n$ unrollings a remainder $\sum_x P_\theta^{n}(s,x) \nabla v_\pi(x)$ is left over, and it vanishes only because $P_\theta^n \to 0$. Differentiating the series for $v_\pi$ term by term is not an alternative shortcut without a uniform bound on the derivatives of $P_\theta^k$.

In the continuing case the corresponding obstacle is the differentiability of the steady-state distribution and of the differential values, which the book's proof uses without comment; here they are part of what is to be proved, from ergodicity at $\theta_0$ alone.

Formalization scope

• Model. $\mathcal S^+$ is Option S, with none the single terminal state (several terminal states can be merged, all having value 0). One action type for all states. $\theta$ lives in EuclideanSpace ℝ (Fin d), and $\nabla$ is Mathlib's gradient; conclusions are HasGradientAt, so differentiability is asserted, not assumed.
• Values from returns. $v_\pi$, $q_\pi$, $\eta$ are series in powers of $P_\theta$; Bellman equations are theorems (milestone 1). The continuing-case average reward and steady-state distribution are the limits of (13.15), and the differential values are the series of (13.17).
• Implicit hypotheses made explicit. Termination under $\pi_{\theta_0}$ is a hypothesis of every episodic result that involves values; the continuing case assumes the book's ergodicity (the limit of $\Pr\{S_t = s'\}$ exists and does not depend on $S_0$) at $\theta_0$. The positivity of $\pi(a \mid s,\theta_0)$ is assumed where a logarithm is differentiated.
• "∝". The episodic goal states the exact equality with the constant $\sum_{s'} \eta(s')$ and proves it is at least 1. A formalization of the form "$\exists c,\ \nabla J = c \cdot \ldots$" is ruled out: it holds with $c = 0$ and loses the book's constant.
• Fixed start state. $s_0$ is a fixed state, as in the book (p. 324); no start distribution.
• Not included. Convergence of REINFORCE or actor–critic under stochastic-approximation conditions (p. 329) rests on unstated conditions and is not an item. The baseline is a deterministic function of the state, not the random variable the book also allows.

Reusable infrastructure: the episodic value layer (substochastic chains, expected visits, termination) is needed by any undiscounted episodic RL result; the soft-max and Gaussian eligibility computations are needed by every policy-gradient algorithm. Proofs of any milestone, and general lemmas on the differentiability of values and stationary distributions of parameterized finite Markov chains, are welcome.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 13. http://incompleteideas.net/book/the-book-2nd.html
• R. S. Sutton, D. McAllester, S. Singh and Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, NeurIPS 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/464d828b85b0bed98e80ade0a5c43b0f-Abstract.html
• P. Marbach and J. N. Tsitsiklis, Simulation-Based Optimization of Markov Reward Processes, IEEE Transactions on Automatic Control 46(2), 2001. https://doi.org/10.1109/9.905687
• R. J. Williams, Simple Statistical Gradient-Following Algorithms for Connectionist Reinforcement Learning, Machine Learning 8, 1992. https://doi.org/10.1007/BF00992696