Machine Learning

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

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

Why stability bounds

A learning algorithm is judged by its generalization error, its expected loss on a fresh example, which cannot be computed because the data distribution is unknown. Practitioners estimate it either by the empirical error on the training set or by the leave-one-out error, which retrains the algorithm once per example. Classical learning theory justifies these estimates through uniform convergence over the whole hypothesis space (VC dimension, covering numbers). That route says nothing useful about algorithms such as nearest-neighbour rules or regularized kernel methods, whose effective hypothesis space is huge or unknown.

An alternative is to bound the deviation through a property of the algorithm itself: how much its output changes when one training example is removed. This idea goes back to Rogers and Wagner (1978) and Devroye and Wagner (1979) for local rules, and Kearns and Ron (1999) gave it a name. Bousquet and Elisseeff (JMLR 2002) systematized it with several stability notions and corresponding bounds; their paper is the standard reference for algorithmic stability in learning theory. This mission formalizes its first family of results, the polynomial bounds of §4.1.

Setting

Let $Z = X \times Y$ and let $D$ be a probability distribution on $Z$. A training set $S = \{z_1, \dots, z_m\}$ consists of $m$ examples drawn i.i.d. from $D$. A learning algorithm $A$ maps a training set $S$ to a hypothesis $A_S : X \to Y'$; it is deterministic and symmetric, meaning it does not depend on the order of the examples. A cost $c$ with $0 \le c(y', y) \le M$ defines the loss $\ell(f, z) = c(f(x), y)$ of a hypothesis $f$ at $z = (x, y)$.

For each index $i$, $S^{\setminus i}$ is $S$ with $z_i$ removed, and $S^i$ is $S$ with $z_i$ replaced by an independent fresh draw $z'_i \sim D$. The three error quantities are

Two stability notions (Definitions 3 and 4) control them. $A$ has hypothesis stability $\beta_1$ if $\mathbb E_{S,z}[|\ell(A_S,z) - \ell(A_{S^{\setminus i}},z)|] \le \beta_1$ for every $i$, and pointwise hypothesis stability $\beta_2$ if $\mathbb E_{S}[|\ell(A_S,z_i) - \ell(A_{S^{\setminus i}},z_i)|] \le \beta_2$ for every $i$.

Formalization targets

Goal: Theorem 11

For $m \ge 1$, under hypothesis stability $\beta_1$ and pointwise hypothesis stability $\beta_2$, for every $\delta > 0$, each of the following holds with probability at least $1 - \delta$ over $S \sim D^m$:

Milestones

1. Lemma 25 (p. 520), a generalized Rogers–Wagner identity: upper bounds on $\mathbb E_S[(R - R_{\mathrm{emp}})^2]$ and $\mathbb E_S[(R - R_{\mathrm{loo}})^2]$ by correlations of the loss.
2. Lemma 9, (8) and (9) (p. 505): $\mathbb E_S[(R - R_{\mathrm{emp}})^2] \le \frac{M^2}{2m} + 3M\,\mathbb E_{S,z'_i}[|\ell(A_S,z_i) - \ell(A_{S^i},z_i)|]$ and $\mathbb E_S[(R - R_{\mathrm{loo}})^2] \le \frac{M^2}{2m} + 3M\,\mathbb E_{S,z}[|\ell(A_S,z) - \ell(A_{S^{\setminus i}},z)|]$.
3. The replace-one term (proof of Theorem 11): $\mathbb E_{S,z'_i}[|\ell(A_S,z_i) - \ell(A_{S^i},z_i)|] \le \beta_1 + \beta_2$.
4. The second-moment bounds (proof of Theorem 11): $\mathbb E_S[(R - R_{\mathrm{emp}})^2] \le \frac{M^2}{2m} + 3M(\beta_1+\beta_2)$ and $\mathbb E_S[(R - R_{\mathrm{loo}})^2] \le \frac{M^2}{2m} + 3M\beta_1$.

Significance

Theorem 11 is the weakest-assumption bound in the paper: it requires only average-case stability, not the uniform (worst-case) stability behind the exponential bounds of §4.2. It shows that both the resubstitution and the deleted estimate are within $O(1/\sqrt{m\delta})$ of the risk whenever the stability parameters decay like $1/m$, with no reference to the size of the hypothesis class. It also extends Devroye and Wagner's leave-one-out analysis for classification to bounded regression losses and to the empirical estimator. Later work on average stability and on generalization of stochastic gradient methods (for example Hardt, Recht and Singer, 2016) starts from these notions.

The result is proved in the paper; as far as is known it has no machine-checked proof. A formal development has two concrete payoffs. First, it fixes the constants: in checking the argument, two printed slips were found (the empirical constant in Theorem 11 and the third term of Lemma 25's first inequality), and the formal statements record the versions that the paper's proof actually establishes. Second, the Lemma 25 and Lemma 9 machinery — exchangeability of i.i.d. samples under renaming, and second-moment control through stability — is reusable for any later stability result.

Difficulty

The obvious route is the Efron–Stein (Steele) variance inequality, Theorem 1 of the paper. It bounds the variance of $R - R_{\mathrm{emp}}$, not its second moment, and leaves the bias to be handled separately; the paper notes that it gives worse constants. The direct route of Appendix A instead expands $\mathbb E_S[(R - R_{\mathrm{emp}})^2]$ and rewrites each correlation term by renaming i.i.d. variables: training points, fresh test points and replacement points are exchanged with one another, and the algorithm is retrained on sets $T \cup \{z, z'\}$ with $T = S^{\setminus \{i,j\}}$. Every renaming is a measure-preserving map on a product of $m + 2$ copies of $D$, and each must be justified by the symmetry of $A$. Doing this rigorously, rather than as "a matter of renaming", is the core of the work. The leave-one-out case is only sketched in the paper ("it is easy to see"), so its formal proof has to be reconstructed.

Formalization scope

• An algorithm is a function Multiset (X × Y) → (X → Y'). Symmetry in the training set is built into the type, and the same algorithm acts on sets of every size, as $S$ and $S^{\setminus i}$ require. A sample is S : Fin m → X × Y with law $D^m$ (Measure.pi); fresh points $z$, $z'$, $z'_i$ are further independent coordinates, via product measures $D^m \otimes D$ and $(D^m \otimes D) \otimes D$.
• The loss, empirical error and generalization error are the published FoundationsML.Stability definitions (Loss, EmpiricalError, GeneralizationError).
• The cost satisfies $0 \le c \le M$ everywhere. The paper's assumption that "all functions are measurable" becomes one hypothesis: for every $n$, $(S, z) \mapsto \ell(A_S, z)$ is measurable on $(X \times Y)^n \times (X \times Y)$. Both stability definitions also require their integrands to be integrable. Together these rule out the trivializing reading in which a non-integrable expectation equals Lean's default value $0$ and the stability hypotheses hold vacuously.
• "With probability $1 - \delta$" is stated as a bound on the failure event: $D^m\{S : R > R_{\mathrm{emp}} + \cdots\} \le \delta$ for every $\delta > 0$, separately for each estimator.
• $m \ge 2$ is assumed in Lemmas 9 and 25 and in the two second-moment steps of the proof, because the lemmas refer to two distinct indices. Theorem 11 itself is stated for every $m \ge 1$, as printed.
• Corrected statements. (i) Theorem 11's empirical bound is stated with $6Mm(\beta_1+\beta_2)$, not the printed $12Mm\beta_2$: the proof bounds a hypothesis-stability term by $\beta_2$ when it is bounded by $\beta_1$. The two coincide when $\beta_1 = \beta_2$. Accordingly the replace-one milestone is stated as $\le \beta_1 + \beta_2$ (printed $2\beta_2$), and the empirical second-moment bound as $\frac{M^2}{2m} + 3M(\beta_1+\beta_2)$ (printed $6M\beta_2$). (ii) Lemma 25's empirical inequality has $\mathbb E_S[\ell(A_S,z_i)\ell(A_S,z_j)]$ as its third term, as its proof gives, not the printed leave-one-out term. (iii) The leave-one-out second-moment bound follows from (9), not from (10) as printed.

Contributions are welcome at every level: proofs of the milestones, a general exchangeability lemma for symmetric algorithms on product measures, and Markov/Chebyshev glue for the final step.

Selected references

• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002), 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• W. H. Rogers and T. J. Wagner, A finite sample distribution-free performance bound for local discrimination rules, Annals of Statistics 6(3) (1978), 506–514. https://doi.org/10.1214/aos/1176344196
• L. Devroye and T. J. Wagner, Distribution-free performance bounds for potential function rules, IEEE Transactions on Information Theory 25(5) (1979), 601–604. https://doi.org/10.1109/TIT.1979.1056087
• M. Kearns and D. Ron, Algorithmic stability and sanity-check bounds for leave-one-out cross-validation, Neural Computation 11(6) (1999), 1427–1453. https://doi.org/10.1162/089976699300016304
• M. Hardt, B. Recht and Y. Singer, Train faster, generalize better: stability of stochastic gradient descent, ICML 2016. https://arxiv.org/abs/1509.01240

Motivation

An agent learning to control an unknown environment must balance rewards it can collect now against information that improves later decisions. In a finite Markov decision process (MDP), every action changes the distribution of the next state, so a mistaken transition estimate can affect decisions many steps later. Regret measures this loss against a policy that already knows the transition probabilities. The paper of Azar, Osband and Munos gives high-probability regret bounds for two variants of upper confidence bound value iteration (UCBVI) in finite-horizon reinforcement learning. This mission targets its Chernoff–Hoeffding variant, UCBVI-CH, whose bonus depends only on the horizon and the visit count. Theorem 1 improves the paper's cited earlier dependence on the number of states from $S$ to $\sqrt S$ in the leading term for sufficiently many interactions. Azar, Osband and Munos, 2017, pp. 2, 4–5.

The paper was released in 2017 alongside work on the attainable dependence of episodic regret on the horizon $H$, state count $S$, action count $A$, and total interaction time $T$. Its second algorithm, UCBVI-BF, uses a variance-dependent bonus and is the subject of the next mission in this series. UCBVI-CH has a simpler bonus and its own explicit bound, making it a distinct mathematical target. Azar, Osband and Munos, 2017, pp. 1–5.

Setting

The state set $\mathcal S$ and action set $\mathcal A$ are finite and nonempty, with cardinalities $S$ and $A$. A stationary transition kernel $P(y\mid x,a)$ gives the probability of moving to state $y$ after action $a$ in state $x$; each row is nonnegative and sums to one. The known, deterministic reward $R(x,a)$ lies in $[0,1]$. An episode lasts $H\ge1$ steps. The environment chooses its starting state $x_{k,1}$ before episode $k$ and may base that choice on earlier episodes. It cannot see the current episode's future random draws. Azar, Osband and Munos, 2017, §2 and Assumption 1, pp. 2–3.

A policy $\pi$ selects an action from the current state and the step number. Its value $V_h^\pi(x)$ is the expected sum of rewards from step $h$ through step $H$ when starting in state $x$. The terminal value is $V_{H+1}^\pi=0$, and $V_h^*(x)$ is the maximum of $V_h^\pi(x)$ over all such policies. Since the state, action and step sets are finite, this maximum is over a finite nonempty policy class. The paper's sentence describing $H-h$ rewards uses a shifted terminal convention; this series follows the $H$ reward steps of Algorithms 1–2. Azar, Osband and Munos, 2017, pp. 3–4.

At the start of episode $k$, UCBVI-CH forms visit counts $N_k(x,a,y)$ and $N_k(x,a)$ from earlier completed transitions. On a visited pair it uses the empirical row $\widehat P_k(y\mid x,a)=N_k(x,a,y)/N_k(x,a)$. Algorithm 2 computes values backward from zero at the terminal step. For a visited pair, $Q_{k,h}(x,a)$ is the minimum of the preceding episode's $Q_{k-1,h}(x,a)$, $H$, and the empirical Bellman value plus Algorithm 3's bonus. For an unvisited pair, $Q_{k,h}(x,a)=H$. A maximizing action is chosen at every state, including states outside the realized path. Azar, Osband and Munos, 2017, Algorithms 1–3, pp. 3–4.

Formalization targets

Theorem 1: UCBVI-CH regret

For $K$ episodes and $T=KH$, regret sums the gap $V_1^*(x_{k,1})-V_1^{\pi_k}(x_{k,1})$. The goal is the paper's printed bound, with its constants:

Algorithm 3 itself uses $L_{\rm alg}=\ln(5SAT/\delta)$ in its bonus $7HL_{\rm alg}/\sqrt{N_k(x,a)}$. Both logarithms remain as printed. The probability is over the MDP's next-state draws, for every admissible starting-state rule and every way of breaking ties between maximizing actions. Azar, Osband and Munos, 2017, Algorithm 3, p. 4; Theorem 1, p. 5.

Supporting results

Four milestones retain the source's indexed attack path: the Bernstein bound (9) for the empirical value error, the count-deviation display before (11), Lemma 18 on optimism, and the weighted recursion displayed in the proof of Lemma 3. The last milestone preserves the signed weights that appear before the paper's final simplification. Azar, Osband and Munos, 2017, pp. 17, 20–21, 28.

Significance

Theorem 1 gives a finite-sample failure probability with explicit dependence on $H,S,A,K$ and $\delta$. It covers a learner whose initial state can change between episodes, a feature that matters in episodic learning where the experimenter does not fix a single starting distribution. For the regime stated after Theorem 1, the leading rate is $\widetilde O(H\sqrt{SAT})$. This is a result claimed by the paper; the present Lean declarations are open proof targets, not machine-checked proofs of that claim. Azar, Osband and Munos, 2017, p. 5.

Formalizing the result creates reusable finite objects for adaptive interaction: a constructed probability law on complete paths, empirical transition counts pooled across steps, a policy value defined by its expected reward, and confidence events with their domains stated explicitly. The concentration and optimism milestones can then be investigated independently of the final regret bound. The later UCBVI-BF mission uses the same paper's model with a different bonus. Azar, Osband and Munos, 2017, pp. 3–5, 14–17.

Difficulty

The visit count $N_k(x,a)$ is random and depends on earlier observations and decisions. A concentration inequality for a predetermined number of samples therefore does not immediately give a statement that holds at every episode start. The algorithm also reuses the previous episode's $Q$ estimate through a minimum. Any optimism claim must account for this dependence across episodes as well as the backward dependence across steps. In the regret analysis, the terms called martingale differences can have either sign, so replacing a positive weight by a larger common bound can reverse an inequality. These are concrete obstacles to the printed chain of estimates. Azar, Osband and Munos, 2017, pp. 4, 17, 20–21, 28.

Formalization scope

States, actions, steps, episodes and complete outcome arrays are finite. Probabilities are finite sums of products of transition rows. The transition-row predicate is a published general definition; this mission defines the paper-specific reward-bounded MDP, policies, UCBVI-CH recursion, and path law on top of it. The starting-state rule can inspect only earlier episodes. Greedy tie-breaking is universally quantified. $V^*$ is a maximum over policies, and the bonus is read only at positive counts. A model that assigns an arbitrary probability law, fixes one starting state, or omits Algorithm 2's minimum does not represent this target. Azar, Osband and Munos, 2017, pp. 2–4.

Lean uses steps $0,\dots,H-1$ and terminal index $H$ in place of the paper's algorithmic $1,\dots,H+1$. The appendix sometimes puts the terminal value at $H$. The weighted recursion therefore runs through the final reward step, rather than ending one step early. Its typical-state threshold is $4H^2L$, as required by (34)–(36), whereas Appendix B.1 prints $2H^2L$. The proof's correction term $c_4$ dominates its other terms under $A\ge2$, which is made explicit in that milestone. The printed (11) loses a factor of two from the count display before it; only the preceding display is a milestone. Lemma 18 is stated under the empirical-model part of the confidence event and $\delta\le1$, the domain on which its bonus comparison holds. The weighted milestone retains its coefficients because the bracketed martingale terms can be negative. Azar, Osband and Munos, 2017, pp. 14–17, 20–21, 28.

The goal retains Theorem 1's constant $20$. Appendix C.1 cites Lemmas 15 and 18, but the sketch of Lemma 15 does not track that constant explicitly. Formalizing the printed bound may therefore expose a gap in its proof; the mission records the claim without weakening its constants. Contributions establishing or repairing the explicit bound, as well as the four stated milestones and reusable finite concentration results, are within scope. Azar, Osband and Munos, 2017, pp. 5, 27, 29.

Selected references

• M. G. Azar, I. Osband and R. Munos, Minimax Regret Bounds for Reinforcement Learning, arXiv:1703.05449v2, 2017. Pinned preprint.

Why batch TD(0) and batch Monte Carlo disagree

Temporal-difference (TD) learning estimates the value of each state of a Markov reward process from observed experience, updating an estimate toward a target built from the next reward and the current estimate of the next state. Monte Carlo (MC) methods instead update toward the full observed return. Both are standard prediction methods in reinforcement learning, and their relationship is a recurring question of the field (Sutton 1988).

When only a finite amount of experience is available, a common practice is to present the same data repeatedly until the estimates stop changing. Chapter 6 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) uses this setting to explain why TD(0) is often faster: under such batch updating, both methods converge deterministically, but to different answers. Batch MC finds the least-squares fit to the observed returns; batch TD(0) finds the value function of the maximum-likelihood Markov model of the data, the certainty-equivalence estimate. The comparison appears in §6.3, Optimality of TD(0) (pp. 126–128), and is illustrated by Example 6.4, You are the Predictor. The book states these conclusions without proof. This mission formalizes them.

Setting

Let $\mathcal S$ be a finite set of nonterminal states and $\mathcal S^+ = \mathcal S \cup \{\text{terminal}\}$. An episode is a finite sequence $S_0, R_1, S_1, \dots, S_{T-1}, R_T, S_T$ with $S_0, \dots, S_{T-1} \in \mathcal S$, real rewards $R_1, \dots, R_T$, and $S_T$ terminal. A batch is a finite list of episodes. A visit of $s$ is an (episode, time $t < T$) pair with $S_t = s$, and $n(s)$ counts all visits (every-visit counting).

A value array $V : \mathcal S \to \mathbb R$ is extended by $V(\text{terminal}) = 0$. For a discount rate $\gamma \in [0,1]$, the return is $G_t = \sum_{k=t+1}^{T}\gamma^{k-t-1}R_k$ and the TD error is $\delta_t = R_{t+1} + \gamma V(S_{t+1}) - V(S_t)$.

Batch TD(0) with step size $\alpha$ computes the TD(0) increment for every visit in the batch and changes $V$ once, by their sum:

Batch constant-$\alpha$ MC is the same iteration with the increment $G_t - V_m(S_t)$.

The maximum-likelihood model of the batch has transition probabilities $\hat p(j \mid i) = N(i,j)/n(i)$, where $N(i,j)$ counts the observed transitions from $i$ to $j \in \mathcal S^+$, and expected rewards $\hat r(i,j)$ equal to the average reward observed on those transitions. With $\hat P = (\hat p(s'\mid s))_{s,s'\in\mathcal S}$ and $\hat r(s) = \sum_j \hat p(j\mid s)\hat r(s,j)$, the certainty-equivalence estimate is the value function of this Markov reward process,

Formalization targets

Goal: batch TD(0) converges to the certainty-equivalence estimate

For every finite batch and every $\gamma \in [0,1]$, the series defining $\hat v$ converges, and there is $\bar\alpha > 0$ such that for all $\alpha \in (0,\bar\alpha)$ and all initial arrays $V_0$,

The limit depends neither on $\alpha$ nor on $V_0$ at visited states.

Milestones

1. (6.6): with $V$ held fixed, $G_t - V(S_t) = \sum_{k=t}^{T-1}\gamma^{k-t}\delta_k$.
2. Exercise 6.8: the same identity for action values, $\delta_t = R_{t+1} + \gamma Q(S_{t+1},A_{t+1}) - Q(S_t,A_t)$.
3. Least squares: the sample averages $\bar G(s)$ of the returns after the visits to $s$ minimize $\sum_{\text{visits}}(G_t - V(S_t))^2$ over all arrays $V$.
4. Batch MC: for small $\alpha$, batch constant-$\alpha$ MC converges to $\bar G(s)$ at every visited $s$.
5. Fixed points: the batch TD(0) increments vanish everywhere if and only if $V = \hat v$ on visited states.
6. Example 6.4: on the eight episodes $A,0,B,0$; $B,1$ (six times); $B,0$ with $\gamma = 1$, the certainty-equivalence estimate is $\hat v(A) = \hat v(B) = 3/4$ and batch TD(0) converges to it, while batch MC converges to $V(A) = 0$, $V(B) = 3/4$.

Significance

The result explains the empirical observation of Figure 6.2 in the book: batch TD(0) has lower error than batch MC on Markov data, because it computes the certainty-equivalence estimate, while batch MC fits the training returns. It also gives a precise meaning to the claim that TD methods approximate the certainty-equivalence solution with memory linear in the number of states, where computing it directly needs a model of quadratic size and cubic time (p. 128). Identity (6.6) is the starting point of the $n$-step and eligibility-trace methods of later chapters.

The comparison under repeated presentation of a finite training set goes back to Sutton 1988, but the textbook states the conclusions without proof, and no machine-checked version is known to exist. The formalization pins down every hypothesis the text leaves implicit: the step-size threshold, the treatment of unvisited states, every-visit counting, and the undiscounted case.

Difficulty

The fixed-point equation of batch TD(0) is $D(\hat r + \gamma\hat PV - V) = 0$ on visited states, with $D$ the diagonal of visit counts, and convergence of the iteration $V \mapsto V + \alpha D(\hat r + \gamma\hat P V - V)$ requires every eigenvalue of $D(I - \gamma\hat P)$ to have positive real part. For $\gamma < 1$ this follows from $\hat P$ being substochastic. For $\gamma = 1$, the case of Example 6.4, $\hat P$ is only substochastic and the naive contraction argument fails: invertibility of $I - \hat P$ must be derived from the structure of the data, since every episode ends in the terminal state. The matrix $D(I - \gamma\hat P)$ is not symmetric, so symmetric positive-definiteness arguments do not apply. The same issue makes convergence of the series defining $\hat v$ nontrivial at $\gamma = 1$.

Formalization scope

An episode is a Lean List (X × ℝ) of transitions $(S_t, R_{t+1})$, with the terminal state represented by none : Option X; a batch is a list of episodes; states form a Fintype. Values at the terminal state are $0$ by definition. The certainty-equivalence estimate is defined from returns as the series $\sum_k\gamma^k\hat P^k\hat r$, not as the solution of a Bellman equation, and its convergence is part of the goal, not assumed. "Sufficiently small $\alpha$" is an existential threshold $\bar\alpha > 0$ quantified before $\alpha$ and $V_0$; a statement for one fixed $\alpha$, or for some $\alpha$, would be weaker than the book's and is ruled out. Unvisited states receive no increment and keep their initial value; the goal records this rather than claiming convergence to $\hat v$ there. The standing assumption $\gamma \in [0,1]$ includes $\gamma = 1$. Every visit is counted in both the TD increments and the model; mixing first-visit and every-visit counts would make the goal false.

The mission needs only finite sums, matrix powers and limits of real sequences; Mathlib's Matrix and Filter.Tendsto suffice. A lemma that a nonnegative matrix whose rows reach an absorbing mass has spectral radius below one would be reusable beyond this mission, as would a convergence criterion for $V \mapsto V + \alpha(b - MV)$ when $M$ is a nonsingular M-matrix. Contributions of either kind, and of the elementary milestones 1–3, are welcome.

Selected references

• Richard S. Sutton and Andrew G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §6.1 and §6.3, pp. 119–129. http://incompleteideas.net/book/the-book-2nd.html
• Richard S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3, 9–44, 1988. https://doi.org/10.1007/BF00115009

Why policy improvement matters

Reinforcement learning methods search for good behaviour by alternating two activities: estimating how good the current behaviour is, and changing the behaviour in the direction those estimates suggest. Sutton and Barto call this pattern generalized policy iteration and use it as the organizing idea of their textbook (Sutton & Barto 2018, §4.6). Its mathematical justification is a single result of Chapter 4, the policy improvement theorem (p. 78): a comparison made one step ahead, at each state separately, certifies that a changed policy is at least as good everywhere. Policy iteration, value iteration, Monte Carlo control with ε-greedy policies (Chapter 5), Sarsa and Q-learning are all motivated by it.

The chapter's results go back to the foundations of dynamic programming: the Bellman optimality equation (Bellman 1957), and policy iteration with its finite termination for discounted finite Markov decision processes (Howard 1960). Standard modern treatments are Puterman 1994, Ch. 6, and Bertsekas 2012, Vol. II, Ch. 1.

Setting

A finite Markov decision process has a finite state set $\mathcal S$, a finite nonempty action set $\mathcal A$, a finite reward set $\mathcal R\subset\mathbb R$ and dynamics $p(s', r\mid s, a)$: for each state $s$ and action $a$, a probability distribution over the next state $s'$ and reward $r$ (Eqs. (3.2)–(3.3)). A policy $\pi$ gives probabilities $\pi(a\mid s)$ of choosing each action in each state; a deterministic policy is a map $\pi:\mathcal S\to\mathcal A$.

Fix a discount rate $0\le\gamma<1$. The state-value function of $\pi$ is the expected discounted return

and the action-value function is defined from it by (4.6):

the value of taking $a$ once in $s$ and following $\pi$ afterwards. A policy is optimal if its value is at least that of every policy at every state, and the optimal value function is $v_*(s)=\max_\pi v_\pi(s)$. A deterministic policy $\pi'$ is greedy with respect to $q_\pi$ if $\pi'(s)\in\operatorname{argmax}_a q_\pi(s,a)$ for all $s$ (4.9).

Formalization targets

Goal: the policy improvement theorem, (4.7)–(4.8), p. 78

For deterministic policies $\pi,\pi'$,

and at every state where the hypothesis is strict, the conclusion is strict at that same state.

Milestones

1. Iterative policy evaluation (4.5), p. 74. From any $v_0$, the iterates $v_{k+1}(s)=\sum_a\pi(a\mid s)\sum_{s',r}p(s',r\mid s,a)[r+\gamma v_k(s')]$ converge to $v_\pi$.
2. Greedy improvement (4.9), p. 79. A greedy $\pi'$ with respect to $q_\pi$ satisfies (4.7), hence $v_{\pi'}\ge v_\pi$.
3. The stochastic case, p. 79. For stochastic $\pi,\pi'$, with $q_\pi(s,\pi'(s))=\sum_a\pi'(a\mid s)q_\pi(s,a)$ as in (5.2), the theorem holds as stated, strictness included.
4. Equality forces optimality, p. 79. If a greedy $\pi'$ has $v_{\pi'}=v_\pi$, then $v_{\pi'}$ solves the Bellman optimality equation (4.1), $v_{\pi'}=v_*$, and $\pi$ and $\pi'$ are optimal.
5. Policy iteration, p. 80. For every sequence of deterministic policies with $\pi_{k+1}$ greedy with respect to $q_{\pi_k}$: each step is a strict improvement unless $\pi_k$ is optimal, and from some $K$ on every $\pi_k$ is optimal with $v_{\pi_k}=v_*$.
6. Value iteration (4.10), p. 83. $v_*$ is attained by one policy at all states, and from any $v_0$ the iterates $v_{k+1}(s)=\max_a\sum_{s',r}p(s',r\mid s,a)[r+\gamma v_k(s')]$ converge to $v_*$.

Significance

The results. The policy improvement theorem turns a local test into a global guarantee: it is enough to check, state by state, that one step of the new policy followed by the old one does no worse than the old one. Combined with the finiteness of the set of deterministic policies, it yields the finite termination of policy iteration and, with the equality case, the existence of a deterministic optimal policy. The stochastic form is what Chapter 5 invokes for ε-greedy control. Value iteration is the other classical way to compute $v_*$.

Formalizing them. All of these results are classical and proved in the literature cited above; they are not open. The textbook presents them informally ("we chose not to produce a rigorous formal treatment", p. xiii): the improvement theorem is argued by an unbounded chain of expansions, and the policy evaluation and value iteration convergence claims are stated without proof. The mission makes each claim precise with explicit hypotheses and asks for machine-checked proofs against the book's own model with four-argument dynamics and stochastic policies. Related platform results use different models (cost minimization with deterministic policies in Bertsekas's Dynamic Programming; an expected-reward kernel and an assumed fixed point in Foundations of Machine Learning), and none states the policy improvement theorem itself.

Difficulty

The book's proof expands $q_\pi$ with (4.6) and reapplies (4.7) indefinitely, ending with "$\le\cdots=v_{\pi'}(s)$". Made rigorous, the chain is an inequality between truncated returns plus a remainder $\gamma^n E_{\pi'}[v_\pi(S_{t+n})]$, and the passage to the limit needs the remainder to vanish and the truncated returns to converge to $v_{\pi'}$. Since $v_\pi$ is defined here as a series of expected rewards under the induced Markov chain, connecting it to the one-step quantities requires first establishing the Bellman equation for $v_\pi$ from that series. The strictness part does not follow from the weak inequality alone: strictness at one state must be shown to survive the averaging over later states, which requires tracking the contribution of the first step exactly. The policy iteration statement additionally requires handling ties: a greedy step taken from an optimal policy can move to a different optimal policy, so the sequence need not become constant.

Formalization scope

All objects live in the namespace SuttonBartoRL.DP. States and actions are finite types, actions nonempty where a maximum is taken; one action set serves all states (footnote 3, p. 48). Rewards form a finite set $\mathcal R\subset\mathbb R$, and the dynamics are a function $p(s',r\mid s,a)$ whose values off $\mathcal R$ are never used. Policies are stochastic; deterministic policies are embedded as policies that choose one action with probability one.

Committed conventions:

• Discount $0\le\gamma<1$ throughout. The book also allows $\gamma=1$ when "eventual termination is guaranteed" (p. 74) but never states that hypothesis precisely; the episodic case with a terminal state is out of scope. This is the only restriction relative to the text.
• $v_\pi$ from returns. $v_\pi(s)=\sum_k\gamma^k(P_\pi^k r_\pi)(s)$, with $P_\pi$ the state transition matrix of $\pi$ and $r_\pi$ its expected one-step reward. $q_\pi$ is defined by (4.6), as the book does. The Bellman equation (4.4) is not assumed. Defining $v_\pi$ as the fixed point of a Bellman operator would make the goal an order property of that operator and is excluded.
• $v_*$ is the real supremum over all stochastic policies; the value iteration item also asserts it is attained. Optimality of a policy means dominance over all stochastic policies.
• Greedy means $\pi'(s)$ is any maximizer of $q_\pi(s,\cdot)$; tie-breaking is arbitrary and may differ between iterations.
• Stochastic case. The book only says the theorem "carries through as stated"; the meaning $q_\pi(s,\pi'(s))=\sum_a\pi'(a\mid s)q_\pi(s,a)$ is taken from the book's (5.2), p. 101.
• Policy iteration is the idealized sequence with exact evaluation. The item does not claim that the boxed pseudocode on p. 80 stops, which it may fail to do under ties (Exercise 4.4, p. 82).
• Convergence of iterates is in the product topology on $\mathbb R^{\mathcal S}$, equivalent to the sup norm for finite $\mathcal S$.

In-place (asynchronous) sweeps (§4.5) and truncated policy iteration are not formalized.

Needed infrastructure: summability of discounted series of bounded expected rewards, the Bellman equation for $v_\pi$ derived from the return definition, contraction arguments in the sup norm on $\mathbb R^{\mathcal S}$, and finiteness of the set of deterministic policies. The definitions here duplicate those of the series' Chapter 3 mission and are intended to be merged with them; lemmas about $v_\pi$, the Bellman equation and contraction are reusable by every later mission of the series, and contributions of such lemmas are welcome.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 4. http://incompleteideas.net/book/the-book-2nd.html
• R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://press.princeton.edu/books/paperback/9780691146683/dynamic-programming
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960. https://mitpress.mit.edu/9780262080095/dynamic-programming-and-markov-processes/
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. II, 4th ed., Athena Scientific, 2012. http://www.athenasc.com/dpbook.html

Motivation

Online decision makers often have to choose an action before seeing the cost assigned to it. A no-regret algorithm performs almost as well, in total, as the best single action that could have been chosen after the costs were known. In a related repeated-game problem, Blackwell approachability asks a player to keep the average of vector payoffs close to a desired set despite an adversary's choices. These two performance criteria look different: one compares scalar costs to a fixed benchmark, while the other measures a geometric distance. Abernethy, Bartlett, and Hazan establish algorithmic reductions between them, with explicit finite-horizon bounds in their COLT 2011 paper. This mission isolates the direction that turns an approachability algorithm into an online linear optimization algorithm.

The bound matters even when the input algorithm has no known rate. It relates the regret of the resulting online algorithm to the actual distance attained on the corresponding sequence. Any subsequent guarantee on that distance then yields a regret guarantee through the same reduction. The paper also gives the reverse reduction and an application to calibrated forecasting; those are separate missions in this series.

Setting

Fix a dimension $d$ and a nonempty compact convex decision set $K\subseteq\mathbb R^d$. On round $t$, an algorithm selects $x_t\in K$ using only the preceding cost vectors $f_1,\ldots,f_{t-1}$. The adversary then reveals $f_t$ in the Euclidean unit ball $B_2(1)$. The incurred linear cost is $\langle f_t,x_t\rangle$. For a horizon $T$, regret compares these costs with the cost of the best single point of $K$ evaluated on all $T$ rounds:

The minimum exists because $K$ is nonempty and compact. No probabilistic model for the cost sequence is assumed. The round index begins at one, and $x_t$ cannot depend on $f_t$.

The reduction uses $\kappa=\max_{x\in K}\|x\|$, the maximum norm of a decision. Write $a\oplus x$ for Euclidean concatenation of a scalar and a vector, an element of $\mathbb R^{d+1}$. The generated cone of a set $M$ consists of its nonnegative scalar multiples, $\operatorname{cone}(M)=\{\alpha m:\alpha\ge0,\ m\in M\}$. For a set $C$, its polar cone is $C^0=\{\theta:\langle\theta,z\rangle\le0\text{ for every }z\in C\}$. This negative-sign convention is fixed throughout the mission.

Algorithm 1 of the paper constructs a vector-payoff game. Its player actions are $K$, its adversary actions are $B_2(1)$, its payoff and target are

A Blackwell approachability algorithm for this game chooses each $x_t$ from the preceding adversary moves. Its finite-horizon approachability rate on a given sequence is $D_T(A)=\operatorname{dist}(T^{-1}\sum_{t=1}^T u(x_t,f_t),S)$, where distance means the Euclidean distance from a point to a set. The online algorithm created by Algorithm 1 uses precisely the same choices $x_t$.

Formalization targets

The goal is Theorem 16 of the paper. For every admissible history-based algorithm, every sequence of unit-ball costs, and every $T\ge1$, it asserts

This is a statement about the rate actually obtained on the chosen cost sequence. It assumes no upper bound on $D_T(A)$ and does not require an oracle call in the statement. Thus it also covers algorithms whose behavior is specified directly rather than through an implementation of the oracle.

The milestone targets are the distance formula of Lemma 13, the conic distance identity in display (8) of Theorem 16's proof, and the existence of a valid halfspace oracle in Lemma 15. Lemma 13 says distance to a nonempty convex cone equals the attained maximum of a linear functional over the polar cone's unit ball. Display (8) specializes this geometry to Algorithm 1's lifted target. Lemma 15 says that every halfspace containing that target admits a player action whose payoff remains in the halfspace against every permitted adversary move. Together these statements specify the geometry and the oracle needed by the reduction.

Significance

Theorem 16 gives a numerical transfer rule: a bound on approachability distance for Algorithm 1's game immediately bounds average regret for the same sequence. Its factor depends only on the size $\kappa$ of the decision set. This permits comparison of algorithms in a common finite-horizon language, without replacing the online cost sequence by a distribution or an asymptotic limit. The source paper uses this direction as one half of its equivalence between approachability and no-regret learning Abernethy, Bartlett, and Hazan, 2011.

The mathematical results are established in that paper; the goal here is a machine-checked Lean development of their statements and eventually their proofs. The mission also supplies reusable definitions of generated and polar cones, a Euclidean lift, a finite-history online algorithm, and regret over a compact decision set. Lemma 13 is useful outside this reduction whenever distance to a cone is compared with linear functionals on its polar. The proposed theorem items currently carry open proofs, while their statements and definition files are checked for elaboration in the pinned Lean environment.

Difficulty

The main obstacle is the change of viewpoint from a scalar regret comparison to distance from a set of lifted vector payoffs. A direct comparison of individual round costs does not describe that distance. The target is a polar cone in one additional Euclidean dimension, so a faithful account must keep the lift's geometry, the cone's sign convention, and the normalization by $\kappa$ aligned. The distance formula also asserts that its maximum is attained. An encoding that merely writes an infimum or supremum with default values can silently make an edge case look valid without representing the paper's claim.

The oracle milestone has a separate quantifier demand. One selected action must work against every adversary move for each halfspace containing the target. It cannot be replaced by a possibly different action for each move, or by a claim only about tangent halfspaces. The theorem includes halfspaces with arbitrary offsets and zero normals because the source oracle accepts any containing halfspace.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d), and $a\oplus x$ lives in EuclideanSpace ℝ (Fin (d+1)) with the Euclidean norm. The generated cone uses exactly one nonnegative multiple of a point of the generating set, as in Definition 11. The polar uses $\langle\theta,z\rangle\le0$, the opposite sign from a positive dual-cone convention. Distances are Euclidean point-to-set distances. All arithmetic is over exact real numbers, and the regret minimum ranges over the image of the nonempty compact set $K$.

The statements require $\kappa>0$ because the source payoff divides by $\kappa$. This excludes the degenerate case $K=\{0\}$, in which the source instance is undefined. They require $T\ge1$ wherever an average is formed. Admissible histories consist of unit-ball adversary moves, and each round's decision belongs to $K$. The dimension may be zero syntactically, but the positive-$\kappa$ hypothesis excludes that case in results using Algorithm 1. These conditions keep the bound from being satisfied through Lean's default values for division by zero, distance to an empty set, or infima over empty sets.

The paper's display (8) writes $\operatorname{cone}(\kappa\oplus K)$ and labels its unit ball with dimension $d$; the formalization uses the cone of $\{\kappa\}\times K$ in $\mathbb R^{d+1}$, matching Algorithm 1. Lemma 12's printed bipolar claim omits closedness; this mission does not use that uncorrected sentence as a milestone. The oracle statement covers all containing halfspaces. Contributions are welcome for the distance identity, the oracle existence result, and the final regret inequality, as well as geometric lemmas supporting those proofs.

Selected references

• Jacob Abernethy, Peter L. Bartlett, and Elad Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, Proceedings of the 24th Annual Conference on Learning Theory, JMLR Workshop and Conference Proceedings 19, 2011, pp. 27–46. Published paper.