All missions

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:

$$V_{m+1}(s) = V_m(s) + \alpha\sum_{\text{visits } t \text{ of } s}\big[R_{t+1} + \gamma V_m(S_{t+1}) - V_m(S_t)\big].$$

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,

$$\hat v(s) = \sum_{k\ge0}\gamma^k\big(\hat P^k\hat r\big)(s).$$

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$,

$$\lim_{m\to\infty} V_m(s) = \hat v(s)\quad\text{for every visited } s, \qquad V_m(s) = V_0(s)\ \text{otherwise}.$$

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

Motivation

A single machine must process $n$ jobs that arrive over time. Job $j$ is released at time $r_j$, needs $p_j$ units of uninterrupted processing, and has weight $w_j > 0$; the goal is to minimize the total weighted completion time $\sum_j w_j C_j$. Offline, with all release dates equal to zero, Smith's rule (sequence by nondecreasing $p_j/w_j$) is optimal (Smith 1956); with arbitrary release dates the problem $1\,|\,r_j\,|\,\sum w_j C_j$ is strongly NP-hard (Lenstra, Rinnooy Kan and Brucker 1977).

In the online version the scheduler learns of job $j$ only at time $r_j$, and at each moment must either start a released job or keep the machine idle. Its quality is measured by its competitive ratio: the worst case, over all instances, of the ratio between the online schedule's cost and the offline optimum. Release-date scheduling is one of the basic test cases of online optimization.

Timeline:

• 1996. Hoogeveen and Vestjens show that no online algorithm has competitive ratio below 2, even with equal weights, and give the 2-competitive algorithm Delayed SPT for equal weights.
• 1997. Hall, Schulz, Shmoys and Wein give a $(3+\varepsilon)$-competitive algorithm for arbitrary weights, based on geometric intervals and linear programming.
• 1998. Phillips, Stein and Wein give another 2-competitive algorithm for equal weights, which does not extend to arbitrary weights.
• 2002. Goemans, Queyranne, Schulz, Skutella and Wang obtain a $(1+\sqrt2)$-competitive deterministic algorithm from an LP relaxation.
• 2004. Anderson and Potts show that Delayed SWPT has competitive ratio exactly 2 for arbitrary positive weights, matching the lower bound.

Setting

An instance has jobs $j \in J = \{1,\dots,n\}$ with integer release dates $r_j \ge 0$, integer processing times $p_j \ge 1$ and real weights $w_j > 0$. A schedule assigns each job an integer start time $S_j$. It is feasible if $S_j \ge r_j$ for every $j$ and no two intervals $[S_j, S_j + p_j)$ overlap; idle time is allowed. Its cost is $C(S) = \sum_j w_j (S_j + p_j)$.

Delayed SWPT runs over unit time slots $[t, t+1)$. When the machine is available at time $t$, it looks at the jobs released by $t$ and not yet started, and selects one with the smallest ratio $p_j/w_j$. Ties go to the smaller $p_j$, then to the smaller index. If $p_j \le t$, it starts $j$ at $t$ and the machine is busy until $t + p_j$. Otherwise the machine stays idle and the rule is applied again at $t+1$. The resulting schedule is written $\pi$, or dswpt I in Lean. In particular no job starts before time $p_j$.

The proof uses three auxiliary problems:

• the doubled problem (2P), with data $(2r_j, 2p_j, w_j)$;
• the extended problem (E), with release dates $r'_j = \max\{p_j, f(r_j)\}$, where $f(t)$ is the first time at or after $t$ at which $\pi$ leaves the machine free;
• one unit-length gap job $g_t$ for each slot $[t,t+1)$ in which Delayed SWPT idles although a job $j$ is available. The gap job has release date $f(r_j)$ and weight $w_j/p_j$.

The schedule $\pi_E$ of (E) runs the original jobs as in $\pi$ and each $g_t$ in $[t,t+1)$.

Formalization targets

Goal: Theorem 8

$$\min\Bigl\{\rho \;:\; \sum_j w_j C_j(\pi) \le \rho \sum_j w_j C_j(S)\ \text{for every instance and every feasible schedule } S\Bigr\} = 2.$$

Lean: IsLeast {ρ | ∀ n I S, IsFeasible I.r I.p S → cost I.w I.p (dswpt I) ≤ ρ * cost I.w I.p S} 2. Both halves are required: the upper bound $2$ and the fact that no smaller constant is valid for this algorithm.

Milestones

1. $\pi_j \ge p_j$ for every job (§2) and $r'_j \le \max\{2r_j, p_j\}$ (§3.2).
2. $\pi_E$ is feasible for (E) (§3.2).
3. Lemma 1. If $\pi^*$ and $\mu^*$ are optimal for (P) and (2P), then $C(\mu^*) = 2\,C(\pi^*)$.
4. Lemma 2. $\pi_E$ is optimal for (E).
5. Lemma 3. If $\mu^*$ is optimal for (2P) and a feasible $\sigma_E$ for (E) satisfies

$$\sum_{j\in J} w_j C_j(\sigma_E) + \sum_{g\in G} w_g C_g(\sigma_E) \le \sum_{j\in J} w_j C_j(\mu^*) + \sum_{g\in G} w_g C_g(\pi_E), \tag{1}$$

then $C(\pi) \le 2\,C(S)$ for every feasible $S$. 6. Inequality (1) holds for some feasible $\sigma_E$, for every optimal $\mu^*$ of (2P) (§§3.4–3.6).

Significance

The theorem shows that a deterministic online algorithm can match the lower bound of Hoogeveen and Vestjens for arbitrary positive weights. This settles the best competitive ratio for deterministic online algorithms for $1\,|\,r_j\,|\,\sum w_j C_j$. The algorithm needs no linear program. The analysis also does not compare the algorithm with a lower bound on the optimum. Instead it shows that the online schedule is optimal for a modified problem (E), and it converts an optimal schedule of (2P) into a schedule of (E).

The result was proved on paper in 2004. Neither Mathlib nor the Prove2Me catalog contains a machine-checked proof of it, or of any competitive ratio for online scheduling with release dates. This mission provides several reusable pieces:

• an executable, verified-terminating definition of an online scheduling rule;
• the doubling lemma for release-date problems;
• the optimality criterion behind Lemma 2;
• the block-by-block exchange argument of §§3.3–3.6.

Difficulty

The obvious argument fails at Lemma 2. Delayed SWPT is far from optimal for (P) itself, and its idle time is unbounded in relative terms. The proof therefore has to show that the inserted gap jobs make every idle slot "justified", so that a preemptive best-available argument becomes valid for (E). That argument rests on an optimality criterion of Belouadah, Posner and Potts (1992), which is not in Mathlib.

The second difficulty is inequality (1). Once $\mu^*$ is doubled and the gap jobs are inserted, nongap jobs must be shifted, and the gain of each gap-generating job must be charged against the delay of the gap jobs in its block. That accounting (Lemmas 4–7 of the paper) is an induction over blocks with signed differences of completion times.

The natural first idea, plain online SWPT (start the available job with the smallest $p_j/w_j$ whenever the machine is free), has no finite competitive ratio (Example 1 of the paper), so the delay $\pi_j \ge p_j$ is essential to the bound and must be tracked through the whole argument.

Formalization scope

Conventions committed to in Lean:

• Data. Jobs are Fin n (0-based, so "smallest index" is the order of Fin n). Times are natural numbers, the paper's standing integer-data assumption (p. 688), and weights are real. Every instance carries $p_j \ge 1$ and $w_j > 0$.
• Schedules and optimality. Schedules are integer start times. Feasibility, cost and optimality are defined for any finite job type, so (E), with job type Fin n ⊕ gapTimes I, uses the same notions. "Optimal" means optimal among all feasible nonpreemptive schedules with integer start times.
• The algorithm. Delayed SWPT is a def: a unit-time simulation that compares ratios by cross-multiplication and re-applies the rule at every slot. It runs to the horizon $\sum_j (r_j + 2p_j) + 1$. A sorry-free check (not uploaded) shows that every job has started by then, and that the simulation reproduces Examples 3 and 4 of the paper, including the gap times $0,2,3,4,5,6$ of Table 2.
• Completion times. In (2P) the completion time is $\mu^*_j + 2p_j$, and gap jobs have unit length.

The goal quantifies over every feasible schedule of every instance. It cannot be met by restricting the competitor to schedules without idle time or to list schedules, by dropping release-date feasibility, or by leaving jobs unscheduled.

Out of scope:

• The general lower bound "no online algorithm beats 2" (Example 2 of the paper, due to Hoogeveen and Vestjens) is not part of the mission. The lower half of the goal concerns Delayed SWPT only.
• The Belouadah–Posner–Potts optimality criterion is an external ingredient of Lemma 2. Solvers may formalize it as a supporting theorem.

Infrastructure that a complete development needs:

• simulation invariants for the algorithm;
• exchange and left-shift arguments for single-machine schedules;
• the job-splitting relaxation behind the best-available criterion.

The schedule vocabulary and the criterion are reusable for other release-date scheduling results. Contributions toward the block lemmas of §§3.3–3.6 (Lemmas 4–7, the bound (9)) are welcome as supporting theorems.

Selected references

• E. J. Anderson and C. N. Potts, Online Scheduling of a Single Machine to Minimize Total Weighted Completion Time, Mathematics of Operations Research 29(3), 686–697, 2004. https://doi.org/10.1287/moor.1040.0092
• J. A. Hoogeveen and A. P. A. Vestjens, Optimal On-Line Algorithms for Single-Machine Scheduling, IPCO 1996, LNCS 1084, 404–414. https://doi.org/10.1007/3-540-61310-2_30
• L. A. Hall, A. S. Schulz, D. B. Shmoys and J. Wein, Scheduling to Minimize Average Completion Time: Off-line and On-line Approximation Algorithms, Mathematics of Operations Research 22(3), 513–544, 1997. https://doi.org/10.1287/moor.22.3.513
• C. Phillips, C. Stein and J. Wein, Minimizing Average Completion Time in the Presence of Release Dates, Mathematical Programming 82, 199–223, 1998. https://doi.org/10.1007/BF01585872
• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella and Y. Wang, Single Machine Scheduling with Release Dates, SIAM Journal on Discrete Mathematics 15(2), 165–192, 2002. https://doi.org/10.1137/S089548019936223X
• H. Belouadah, M. E. Posner and C. N. Potts, Scheduling with Release Dates on a Single Machine to Minimize Total Weighted Completion Time, Discrete Applied Mathematics 36(3), 213–231, 1992. https://doi.org/10.1016/0166-218X(92)90255-9
• J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3, 59–66, 1956. https://doi.org/10.1002/nav.3800030106

Motivation

Nash equilibrium is the standard solution concept for strategic games, but it is usually justified by appeal to what players "would" do once they somehow coordinate on a profile. Correlated equilibrium, introduced by Aumann (J. Math. Econ. 1, 1974), enlarges the set of outcomes by letting players condition their actions on correlated private signals. In Correlated Equilibrium as an Expression of Bayesian Rationality (Econometrica 55, 1987), Aumann gave the concept a decision-theoretic foundation: if the players share a common prior over the states of the world and each player maximizes expected utility given his information at every state, then what they play is a correlated equilibrium — and every correlated equilibrium arises this way. The result is a standard entry point to the epistemic foundations of game theory, and correlated equilibria are central in algorithmic game theory because no-swap-regret learning dynamics converge to them (Foster–Vohra 1997; Hart–Mas-Colell 2000).

Timeline:

• 1974, Aumann: correlated equilibrium defined, in a measure-theoretic model with subjective probabilities and information σ-fields.
• 1987, Aumann: the Main Theorem (Bayes rationality at every state under a common prior implies correlated equilibrium play) and its converse, in a finite model with information partitions.

Setting

A game $G$ in strategic form has players $i$, action sets $S^i$, action $n$-tuples $s\in S=S^1\times\dots\times S^n$, and payoffs $h^i(s)\in\mathbb R$.

A correlated strategy $n$-tuple is a function $f:\Gamma\to S$ on a finite probability space $(\Gamma,q)$, with $q\ge 0$ and $\sum_\gamma q(\gamma)=1$. Its expected payoff is $Eh^i(f)=\sum_\gamma q(\gamma)h^i(f(\gamma))$. For $g^i:\Gamma\to S^i$, the profile $(f^{-i},g^i)$ replaces player $i$'s coordinate of $f$ by $g^i$. The function $f$ is a correlated equilibrium (Definition 2.1) if

$$Eh^i(f)\ \ge\ Eh^i(f^{-i},g^i)\qquad(2.2)$$

for every player $i$ and every $g^i$ that is a function of $f^i$ (i.e. $g^i=\varphi\circ f^i$). The distribution of $f$ assigns to each $s\in S$ the number $q\{f^{-1}(s)\}$, and a correlated equilibrium distribution (c.e.d.) is the distribution of some correlated equilibrium.

An information system consists of a finite set $\Omega$ of states of the world, a common prior $p$ on $\Omega$, an information partition $\mathcal P^i$ of $\Omega$ for each player, and action functions $\mathbf s^i:\Omega\to S^i$ with $\mathbf s=(\mathbf s^1,\dots,\mathbf s^n)$, each $\mathbf s^i$ constant on the elements of $\mathcal P^i$ (each player knows his own action). For a random variable $x$, $E(x\mid\mathcal P^i)(\omega)$ is the $p$-average of $x$ over the element of $\mathcal P^i$ containing $\omega$. Player $i$ is Bayes rational at $\omega$ if

$$E\big(h^i(\mathbf s)\mid\mathcal P^i\big)(\omega)\ \ge\ E\big(h^i(\mathbf s^{-i},a)\mid\mathcal P^i\big)(\omega)\quad\text{for every }a\in S^i .$$

Formalization targets

Goal: Main Theorem with its converse

$$Q\ \text{is a c.e.d. of }G\iff\exists\ \text{information system }(\Omega,p,(\mathcal P^i),\mathbf s):\ \text{every player is Bayes rational at every state, and } Q(a)=p\{\mathbf s=a\}\ \forall a.$$

This is the two-sided statement the paper announces in its introduction (p. 2) and closes in Sect. 4d (p. 11): "under Bayesian rationality, the set of all information systems corresponds precisely to the set of all correlated equilibria."

Milestones

1. Main Theorem, proof: summing the cell-wise inequalities over the partition, $Eh^i(\mathbf s^{-i},g^i)\le Eh^i(\mathbf s)$ for $g^i$ constant on the cells of $\mathcal P^i$.
2. Main Theorem, proof: $\mathbf s$ itself is a correlated equilibrium on $(\Omega,p)$.
3. Main Theorem (p. 7): the distribution of $\mathbf s$ is a c.e.d.
4. Sect. 4d: in the system generated by $f$ (partitions generated by $f^i$), Bayes rationality everywhere is equivalent to (2.2).
5. Sect. 4d: every correlated equilibrium is realized by a Bayes-rational information system with the same distribution.

The mission also states, as a supporting lemma without a milestone, the cell-wise step of the proof of the Main Theorem: Bayes rationality at every state gives $E(h^i(\mathbf s^{-i},g^i)\mid P)\le E(h^i(\mathbf s)\mid P)$ on every cell $P$ for $g^i$ constant on cells.

Significance

The theorem identifies correlated equilibrium as the outcome of individual Bayesian decision making under a common prior, without any assumption that players randomize or that their choices are independent. It shows that the Nash equilibrium's independence requirement is not implied by rationality alone, and it is the template for later epistemic characterizations of solution concepts. On the computational side, correlated equilibrium distributions form a polytope described by linear inequalities (the companion mission of this series), which is why they are the tractable equilibrium notion in algorithmic game theory.

The result is proved in the paper; it has no machine-checked formalization known to this mission. Formalizing it pins down the exact role of the standing assumptions — finiteness, a common prior, measurability of each player's action with respect to his own partition, rationality at every state — and of the conditional expectation on cells of probability zero. The definitions (information systems, Bayes rationality, correlated equilibria as functions on a finite probability space) are reusable for later formalizations of the paper's Sect. 5 (subjective correlated equilibrium) and of other epistemic results.

Difficulty

The mathematics is short; the difficulty lies in the bookkeeping that the paper's notation hides. The hypothesis is interim (a conditional inequality at each state), while Definition 2.1 is ex ante (an unconditional inequality). Passing between them requires the law of total expectation over a partition whose cells may have probability zero, where conditional expectations are undefined. Deviations in Definition 2.1 are functions of $f^i$, not arbitrary maps, and must be shown constant on cells, which uses measurability of $\mathbf s^i$. A tempting first idea — that rationality against every fixed action already gives rationality against every deviation — fails without measurability: a player who does not know his own action could be rational at each state against constant deviations while a deviation $\varphi\circ\mathbf s^i$ varies inside his cells. The converse direction needs an information system that satisfies every axiom of the goal's right-hand side, not just one that is Bayes rational.

Formalization scope

• Players form a finite type ι with decidable equality; action sets S i are arbitrary types (the paper's finiteness of $S^i$ is not used); payoffs are h : ι → (∀ i, S i) → ℝ.
• Probability spaces are finite types with a real weight vector satisfying AGT.IsLottery (from the published definition agt_games). State spaces and the witnessing probability spaces of a c.e.d. range over Type; for finite sets this loses nothing.
• Partitions are Setoids. The Common Prior Assumption is built into the information system, which has a single prior. Measurability of each action function is a field of the structure.
• Conditional expectation on a cell is a ratio of finite sums; on a cell of probability zero Lean returns $0$, so Bayes rationality at such states holds vacuously. The prior is not required to have full support. This matches the paper, whose argument multiplies each cell inequality by the cell's probability.
• Deviations in Definition 2.1 are exactly the compositions $\varphi\circ f^i$; neither all maps nor only constant maps. A c.e.d. requires a genuine probability vector, ruling out the trivializing reading in which the zero weight function witnesses every $Q$.
• Contributions welcome: proofs of the milestones, a general law-of-total-expectation lemma for finite partitions, and lemmas relating distr to sums over action profiles.

Selected references

• R. J. Aumann, Correlated Equilibrium as an Expression of Bayesian Rationality, Econometrica 55 (1987), no. 1, 1–18. https://doi.org/10.2307/1911154
• R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• D. P. Foster and R. V. Vohra, Calibrated Learning and Correlated Equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
• S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68 (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153

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

$$v_\pi(s) = E_\pi\Big[\sum_{k=0}^\infty \gamma^k R_{t+k+1}\ \Big|\ S_t=s\Big],$$

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

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

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'$,

$$\big(\forall s,\ q_\pi(s,\pi'(s))\ge v_\pi(s)\big)\ \Longrightarrow\ \big(\forall s,\ v_{\pi'}(s)\ge v_\pi(s)\big),$$

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

A reproducing kernel is the function $K(x,y)$ that represents point evaluation in a Hilbert space of functions: $f(y) = (f, K(\cdot, y))$. Kernels are combined all the time. In machine learning, a kernel on pairs of objects is routinely built as the pointwise product of two simpler kernels, and in complex analysis the product $|K(x,y)|^2 = K(x,y)K(y,x)$ of a kernel with its conjugate appears naturally. That the pointwise product of two positive matrices is again a positive matrix goes back to I. Schur (1911). What Schur's theorem does not say is which space of functions the product kernel belongs to and what its norm is.

N. Aronszajn answered this in §8 of Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404, doi:10.1090/S0002-9947-1950-0051437-7), the paper that fixed the general theory of reproducing kernel Hilbert spaces. He notes (p. 358, footnote 7) that the idea of the proof was found independently by R. Godement, who applied it only to positive definite functions. The answer has three ingredients developed in the same paper: the functional completion of an incomplete class of functions (§4), the restriction of a kernel to a subset (§5), and the direct product $F_1 \otimes F_2$ of two classes of functions (§8).

Setting

Let $E$ be an arbitrary set. A class with a reproducing kernel is a complex Hilbert space $F$ of functions $f : E \to \mathbb{C}$ such that every point evaluation $f \mapsto f(y)$ is continuous. Its reproducing kernel $K : E \times E \to \mathbb{C}$ is characterized by: $K(\cdot, y) \in F$ for each $y$, and $f(y) = (f, K(\cdot, y))$ for all $f \in F$, where the scalar product $(f, g)$ is linear in $f$ and conjugate-linear in $g$.

Functional completion. Suppose $F$ is a linear class of functions on $E$ with a scalar product satisfying every Hilbert-space axiom except completeness. A functional completion of $F$ is a Hilbert space of functions on $E$, with continuous point evaluations, that contains $F$ isometrically as a dense subset.

Restriction. For $E_1 \subseteq E$, the restriction of $f$ is $f|_{E_1}$, and $F|_{E_1}$ is the class of all restrictions.

Direct product. Given classes $F_1$, $F_2$ on $E$ with kernels $K_1$, $K_2$ and norms $\|\cdot\|_1$, $\|\cdot\|_2$, consider on $E' = E \times E$ the functions

$$f'(x_1,x_2) = \sum_{k=1}^n f_1^{(k)}(x_1) f_2^{(k)}(x_2), \qquad f_1^{(k)} \in F_1,\ f_2^{(k)} \in F_2,$$

with scalar product $(f', g')' = \sum_{k,l} (f_1^{(k)}, g_1^{(l)})_1 (f_2^{(k)}, g_2^{(l)})_2$. Their functional completion is the direct product $F' = F_1 \otimes F_2$, with norm $\|\cdot\|'$.

In Lean, kernelFn H x y is the scalar kernel $K(x,y)$ of a space H, IsFunctionalCompletion ι H says H is a functional completion of the class presented by ι, and IsDirectProduct H₁ H₂ H' says H' is $F_1 \otimes F_2$.

Formalization targets

Goal: §8, Theorem II

The kernel $K(x,y) = K_1(x,y) K_2(x,y)$ is the reproducing kernel of the class $F$ of restrictions of the functions of $F_1 \otimes F_2$ to the diagonal $\{(x,x)\}$, and

$$\|f\| = \min\{\|g'\|' : g' \in F_1 \otimes F_2,\ g'(x,x) = f(x)\ \forall x \in E\}.$$

Milestones

1. §4, Theorem. A functional completion of $F$ exists if and only if every evaluation $f \mapsto f(y)$ is bounded on $F$ and every Cauchy sequence $(f_m) \subset F$ with $f_m(y) \to 0$ for every $y$ satisfies $\|f_m\| \to 0$; the functional completion, when it exists, is unique.
2. §8, Theorem I. $F_1 \otimes F_2$ has reproducing kernel

$$K'(x_1,x_2,y_1,y_2) = K_1(x_1,y_1)\,K_2(x_2,y_2).$$

3. §5, Theorem. $K|_{E_1 \times E_1}$ is the reproducing kernel of $F|_{E_1}$, with $\|f_1\|_1 = \min\{\|f\| : f|_{E_1} = f_1\}$.
4. §8, Remark. For a complete orthonormal system $\{g_1^{(k)}\}$ of $F_1$, every $f$ in the class of $K_1K_2$ is $f = \sum_k f_2^{(k)} g_1^{(k)}$ with $f_2^{(k)} \in F_2$, $\sum_k \|f_2^{(k)}\|_2^2 < \infty$; exactly one such representation minimizes $\sum_k \|f_2^{(k)}\|_2^2$, and the minimum is $\|f\|^2$.

Significance

The result. Theorem II turns the Schur product theorem from a statement about matrices into a statement about function spaces: it says which functions the product kernel can represent and how their norms are computed, through a minimal decomposition. It is the standard description of the reproducing kernel Hilbert space of a product kernel, used to reason about which functions product kernels can express and with what norm, and the Remark gives a concrete series description of the same space. §5 (restriction) and §4 (functional completion) are general tools in their own right: restriction underlies every comparison of kernels on nested domains, and §4 is the criterion for when an incomplete space of functions can be completed without leaving the world of functions.

Formalizing it. All four results are classical and proved on paper. Mathlib has reproducing kernel Hilbert spaces (RKHS, RKHS.kernel, the construction RKHS.OfKernel from a positive semidefinite kernel) and Schur's product theorem (Matrix.PosSemidef.hadamard, for an arbitrary index type), but no restriction theorem, no functional completion and no tensor product of reproducing kernel Hilbert spaces. None of these statements has a machine-checked proof that the mission is aware of.

Difficulty

The kernel identity is the easy part: by Schur's theorem $K_1K_2$ is positive, so some space with kernel $K_1K_2$ exists. The content is the identification of that space and its norm. The direct product has to be constructed before anything can be said about it: the class of finite sums of products is not complete, the scalar product (2) must be shown independent of the representation and positive definite, and the completion must stay a class of functions, which is exactly the question §4 answers and which can fail (p. 349 gives a class satisfying the first condition but not the second). The norm formula is an attained minimum over an infinite-dimensional affine set of preimages, not merely an infimum.

Formalization scope

Scalars are complex throughout ("From now on … we shall consider only complex Hilbert spaces", p. 343). The underlying set $E$ is an arbitrary type X, with no topology, measure or nonemptiness assumption. A class with a reproducing kernel is a complex Hilbert space H with Mathlib's RKHS ℂ H X ℂ structure; its functions are the coercions ⇑f. The scalar kernel is kernelFn H x y = RKHS.kernel H x y 1. Mathlib's inner product $\langle u, v\rangle$ is conjugate-linear in $u$, so Aronszajn's $(f,g)$ is $\langle g, f\rangle$.

Conventions and reading decisions:

• Statements of the form "$K$ is the reproducing kernel of the class $\mathcal{C}$ with norm $N$" assert that a space with kernel $K$ exists and that every space with kernel $K$ has exactly the functions $\mathcal{C}$ and the norm $N$. They never define the space as RKHS.OfKernel K, which would make the kernel identity true by construction.
• The direct product is characterized by its elementary products $f_1(x_1)f_2(x_2)$, the scalar product (2) on them, and density of their span (IsDirectProduct); it is never defined through its kernel. With that, Theorem I is not a definitional identity and Theorem II is not a restatement of §5.
• "min" is an attained minimum (IsLeast). In Theorem II and §5 it is the minimum of the norm, not its square; in the Remark it is the minimum of the sum of squared norms, as printed.
• The diagonal of $E\times E$ is identified with $E$ through $x \mapsto (x,x)$, and the restriction of $g'$ is $x \mapsto g'(x,x)$.
• §4's "incomplete" Hilbert space is a complex inner product space, not assumed complete; completeness is not excluded either.
• The complete orthonormal system of the Remark is a Mathlib HilbertBasis over an arbitrary index set, and the series converges unconditionally at each point.

Results already in Mathlib are not restated: Schur's product theorem (Matrix.PosSemidef.hadamard, the first sentence of §8 and the sentence after Theorem I), positivity of a kernel (RKHS.posSemidef_kernel) and existence of a space for a positive kernel (RKHS.OfKernel, RKHS.kernel_ofKernel).

A complete development needs a Hilbert tensor product of reproducing kernel Hilbert spaces realized as functions on $E\times E$, the restriction construction (quotient by the subspace of functions vanishing on $E_1$), and uniqueness of a reproducing kernel Hilbert space with given kernel. The restriction theorem and the functional completion theorem are reusable well beyond this mission; contributions of either, or of a Hilbert tensor product for RKHS, are welcome.

Selected references

• N. Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
• I. Schur, Bemerkungen zur Theorie der beschränkten Bilinearformen mit unendlich vielen Veränderlichen, J. Reine Angew. Math. 140 (1911), 1–28. https://doi.org/10.1515/crll.1911.140.1
• J. von Neumann and F. J. Murray, On rings of operators, Ann. of Math. 37 (1936), 116–229 (direct products of Hilbert spaces). https://doi.org/10.2307/1968693
• V. I. Paulsen and M. Raghupathi, An Introduction to the Theory of Reproducing Kernel Hilbert Spaces, Cambridge Univ. Press, 2016. https://doi.org/10.1017/CBO9781316219232

Motivation

Reproducing kernel Hilbert spaces are Hilbert spaces of functions in which evaluation at a point is a continuous linear functional. They appear wherever a space of functions carries a natural quadratic norm: Bergman and Hardy spaces of analytic functions, spaces of harmonic functions and solutions of elliptic equations, Sobolev spaces in one dimension, and, since the 1990s, the hypothesis classes of kernel methods in machine learning (support vector machines, Gaussian process regression, kernel ridge regression). In all of these settings, kernels are routinely combined: a sum of kernels is used to model a function as a sum of components, and the question is which space of functions, and which norm, the combined kernel describes.

N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) organised the subject as a calculus of operations on kernels. Its §6 answers the question for sums.

Timeline. E. H. Moore (Bull. Amer. Math. Soc. 1916; General Analysis, 1935) introduced positive Hermitian matrices on arbitrary sets and their associated function classes. S. Bergman (1920s–1930s) studied the kernel of square-integrable analytic functions of a domain. R. Godement (C. R. Acad. Sci. Paris notes, 1945–1946) found the sum theorem for positive definite functions on a group (footnote 6 of the paper). Aronszajn (1950) proved it for arbitrary kernels on arbitrary sets, with the description of the norm as a minimum over decompositions.

Setting

Let $E$ be an arbitrary set. A class of functions $F$ on $E$ is a complex vector space of functions $f:E\to\mathbb C$ carrying a norm $\|\cdot\|$ that makes it a complex Hilbert space. A function $K:E\times E\to\mathbb C$ is the reproducing kernel (r.k.) of $F$ if, for every $y\in E$, the function $K(\cdot,y)$ belongs to $F$ and

$$f(y)=(f,K(\cdot,y))\qquad\text{for every } f\in F,$$

where $(f,g)$ is the scalar product, linear in $f$. A kernel exists exactly when every evaluation $f\mapsto f(y)$ is continuous.

A function $K:E\times E\to\mathbb C$ is a positive matrix if $\sum_{i,j=1}^n K(y_i,y_j)\bar\xi_i\xi_j\ge 0$ for all finite families of points $y_i\in E$ and complex numbers $\xi_i$. Every reproducing kernel is a positive matrix.

A class $F_1$ is a subclass of $F_2$ if every function of $F_1$ belongs to $F_2$, and a subspace if moreover the two norms agree on $F_1$. Two classes $F_1$, $F_2$ with kernels $K_1$, $K_2$ have a sum class $F_1+F_2=\{f_1+f_2: f_i\in F_i\}$, a set of functions; a function of it may have many decompositions $f=f_1+f_2$, since $F_1$ and $F_2$ may share functions.

Formalization targets

Goal: the sum theorem (§6, Theorem, p. 353)

For complex Hilbert spaces $F_1$, $F_2$ of functions on $E$ with kernels $K_1$, $K_2$: the kernel $K=K_1+K_2$ is the reproducing kernel of the class of all $f=f_1+f_2$, with

$$\|f\|^2=\min\big[\|f_1\|_1^2+\|f_2\|_2^2\big],$$

the minimum taken over all decompositions $f=f_1+f_2$, $f_i\in F_i$. The goal asserts that a space with kernel $K_1+K_2$ exists, and that every such space consists exactly of the sums and has exactly this norm, the minimum being attained.

Milestones

1. §2 (4), Moore's theorem (p. 344): a positive matrix is the kernel of one and only one class of functions with a uniquely determined norm. This makes "the class with kernel $K_1+K_2$" well defined.
2. §2 (7) (p. 345): every closed subspace $F'$ of $F$ has a kernel $K'$, and for the orthogonal complement $F''$, $K'+K''=K$.
3. §3, Theorem (p. 347): $K$ is the kernel of a finite-dimensional class if and only if $K(x,y)=\sum_{i,j}\beta_{ij}w_i(x)\overline{w_j(y)}$ with $\{\beta_{ij}\}$ positive definite and the $w_k$ linearly independent; the class is then spanned by the $w_k$, with norm given by the inverse of $\{\bar\beta_{ij}\}$.
4. §6, p. 354, the disjoint case: when $F_1\cap F_2=\{0\}$, $\|f\|^2=\|f_1\|_1^2+\|f_2\|_2^2$, and this happens if and only if $F_1$ and $F_2$ are complementary closed subspaces of $F$.
5. §6, p. 354, Eq. (1): the class of conjugates $\bar F$ has kernel $K(y,x)$, and $\operatorname{Re}K=2^{-1}(K(x,y)+K(y,x))$ is the kernel of the class of all $f+\bar g$, with $\|\varphi\|_0^2=2\min[\|f\|^2+\|g\|^2]$.

Significance

The result itself. The sum theorem is the first operation of Aronszajn's calculus and the base of the next ones: the order $K_1\ll K$ between kernels and the inclusion theorem of §7 are derived from it, as are the kernel $\operatorname{Re}K$ of the class of all $f+\bar g$ and the characterisation of kernels of real spaces (§6, p. 354). In machine learning, it is the statement behind additive kernels and multiple-kernel learning: the hypothesis class of $K_1+K_2$ is the set of sums, and the regulariser is the infimal convolution of the two squared norms. In complex analysis, it describes the space attached to a sum of Bergman-type kernels.

Formalizing it. The results are classical and proved in the paper; none of them is formalized in Mathlib beyond the existence half of Moore's theorem. Mathlib (2026) has reproducing kernel Hilbert spaces with operator-valued kernels (RKHS, RKHS.kernel, RKHS.kerFun, RKHS.posSemidef_kernel) and the construction of a space from a positive semidefinite matrix (RKHS.OfKernel, RKHS.kernel_ofKernel). This mission adds uniqueness, the sum theorem, kernels of closed subspaces, the finite-dimensional case and the conjugate class.

Difficulty

The kernel $K_1+K_2$ is the kernel of some space by Moore's existence theorem, so the content is the identification of that space. The obvious candidate, the external direct sum $F_1\oplus F_2$ mapped to functions by $(f_1,f_2)\mapsto f_1+f_2$, is not injective as soon as $F_1$ and $F_2$ share a nonzero function; the class of sums is the image of a quotient, and its norm is the norm of a minimal representative, which has to be shown to exist and to make the class complete. Proving that the resulting space has kernel $K_1+K_2$ and that every other space with this kernel coincides with it requires the uniqueness half of Moore's theorem, which is not in Mathlib. The disjoint case needs, in addition, that an isometric image of a complete space is closed, and the converse direction of its "only in this case".

Formalization scope

• Scalars and sets. Complex scalars throughout (the paper's convention from §1 on). $E$ is an arbitrary type X with no topology, measure, or nonemptiness assumption.
• Spaces. A class with a kernel is a Mathlib RKHS ℂ H X ℂ on a complex Hilbert space H; its functions are Set.range (⇑ : H → X → ℂ).
• Kernel. The scalar kernel kernelFn H x y is RKHS.kernel H x y 1.
• Scalar products. The paper's $(f,g)$, linear in $f$, is Mathlib's ⟪g, f⟫_ℂ.
• Positivity. A positive matrix is (Matrix.of K).PosSemidef, and "positive definite" is Matrix.PosDef.
• Decompositions are of functions: $f=f_1+f_2$ pointwise with $f_i$ in $F_i$.
• Minima. "min" is an attained minimum (IsLeast), never an infimum.
• Quantification. Statements about "the" class with a given kernel quantify over every RKHS with that kernel, in any universe, and assert separately that one exists.

Reading decisions, recorded in the item notes:

• In §2 (7), "complementary subspaces" means a closed subspace and its orthogonal complement, and the kernels of the two subspaces are any kernels with the reproducing property there, not projections of $K$.
• In §3, $\{\bar\beta_{ij}\}$ is the entrywise conjugate of $\{\beta_{ij}\}$ (consistent with §3 (5), $\sum_j\alpha_{ij}\bar\beta_{jk}=\delta_{ik}$), not its conjugate transpose.
• In §6, p. 354, "subspace" is the paper's §1 notion (norms agree), and the scalar-product remark on $\bar F$ follows from the norm statement by polarization.

Trivialization ruled out. The goal does not define the sum class as RKHS.OfKernel (K₁ + K₂) and assert that its kernel is $K_1+K_2$, which is Mathlib's kernel_ofKernel. Its content is the description of the functions (exactly the sums) and of the norm (the attained minimum) for every space with that kernel.

Infrastructure. A complete development needs:

• uniqueness of an RKHS given its kernel (milestone 1);
• orthogonal projections onto closed subspaces (Mathlib Submodule.starProjection);
• quotients of Hilbert spaces by closed subspaces, or the orthogonal complement of the kernel of the sum map;
• for §3, Gram matrices and their inverses.

Milestone 1 and the RKHS structure on a closed subspace are reusable beyond this mission and are natural Mathlib contributions. Independent proofs of any milestone are welcome.

Selected references

• N. Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), no. 3, 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
• E. H. Moore, General Analysis, Part I, Memoirs of the American Philosophical Society 1, 1935.
• R. Godement, Sur les fonctions de type positif, C. R. Acad. Sci. Paris 221 (1945), 69; and further notes in vols. 221–222 (1945–1946), as cited by Aronszajn [Godement 1].
• E. H. Moore, On properly positive Hermitian matrices, Bull. Amer. Math. Soc. 23 (1916), 59.
• V. I. Paulsen and M. Raghupathi, An Introduction to the Theory of Reproducing Kernel Hilbert Spaces, Cambridge Univ. Press, 2016. https://doi.org/10.1017/CBO9781316219232

Motivation

Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) is the standard introductory text of the field. Its Chapter 3 sets up the model that the rest of Part I works in: the finite Markov decision process (MDP), the value functions of a policy, and the Bellman equations that relate the value of a state to the values of its successors. Section 3.6 then states the fact every planning and control method of the book relies on: in a finite MDP there is an optimal policy, its value is the unique solution of a system of nonlinear equations, and a policy that acts greedily with respect to that solution is optimal. Dynamic programming (Chapter 4), Monte Carlo control (Chapter 5), Sarsa and Q-learning (Chapter 6) are all methods for solving the Bellman optimality equation; their correctness statements presuppose that it has exactly one solution and that it identifies optimal behaviour.

The book is deliberately informal ("we chose not to produce a rigorous formal treatment", p. xiii): §3.6 asserts these facts without proof. The results themselves are classical, going back to Bellman (1957), Howard (1960) and Blackwell (1965); a textbook proof for discounted finite MDPs is in Puterman, Markov Decision Processes (Wiley, 1994), Chapter 6.

Setting

A finite MDP has a finite set of states $\mathcal S$, a finite nonempty set of actions $\mathcal A$, a finite set of rewards $\mathcal R \subset \mathbb R$, and dynamics

$$p(s', r \mid s, a) = \Pr\{S_t = s', R_t = r \mid S_{t-1} = s, A_{t-1} = a\}, \qquad \sum_{s' \in \mathcal S}\sum_{r \in \mathcal R} p(s', r \mid s, a) = 1,$$

Eqs. (3.2)–(3.3). From $p$ one derives $p(s' \mid s, a) = \sum_r p(s', r \mid s, a)$ and $r(s, a) = \sum_r r \sum_{s'} p(s', r \mid s, a)$, Eqs. (3.4)–(3.5).

A policy $\pi$ gives a probability $\pi(a \mid s)$ of each action in each state. Fix a discount rate $0 \le \gamma < 1$. The return of a reward sequence is $G_t = \sum_{k \ge 0} \gamma^k R_{t+k+1}$ (3.8). The state-value function and action-value function of $\pi$ are the expected returns

$$v_\pi(s) = \mathbb E_\pi[G_t \mid S_t = s], \qquad q_\pi(s, a) = \mathbb E_\pi[G_t \mid S_t = s, A_t = a] \qquad (3.12)\text{–}(3.13).$$

In the Lean development these are stateValue M γ π s and actionValue M γ π s a, computed as $\sum_k \gamma^k (P_\pi^k r_\pi)(s)$ from the transition matrix $P_\pi(s, s') = \sum_a \pi(a \mid s)\,p(s' \mid s, a)$ and the expected reward $r_\pi(s) = \sum_a \pi(a \mid s)\,r(s, a)$ of the Markov chain the policy induces. A policy $\pi$ is optimal (IsOptimalPolicy) if $v_\pi(s) \ge v_{\pi'}(s)$ for every policy $\pi'$ and every state $s$. The optimal value functions are

$$v_*(s) = \max_\pi v_\pi(s) \quad (3.15), \qquad q_*(s, a) = \max_\pi q_\pi(s, a) \quad (3.16),$$

optimalValue and optimalActionValue, with the maximum over all stochastic policies.

Formalization targets

Goal: the Bellman optimality equation and optimal policies (§3.6, pp. 62–64)

For every finite MDP and $0 \le \gamma < 1$:

1. the maximum in (3.15) is attained at every state;
2. an optimal policy exists;
3. $v_*$ satisfies the Bellman optimality equation

$$v_*(s) = \max_{a} \sum_{s', r} p(s', r \mid s, a)\big[r + \gamma v_*(s')\big] \quad \text{for all } s; \qquad (3.19)$$

4. $v_*$ is the only function on $\mathcal S$ satisfying (3.19);
5. every policy that assigns positive probability only to actions attaining the maximum in (3.19) is optimal.

Milestones

• (3.9) $G_t = R_{t+1} + \gamma G_{t+1}$ for bounded rewards, with the series convergent.
• (3.14) the Bellman equation $v_\pi(s) = \sum_a \pi(a \mid s) \sum_{s', r} p(s', r \mid s, a)[r + \gamma v_\pi(s')]$, and (p. 60) its uniqueness: $v_\pi$ is its only solution.
• Exercise 3.15 adding a constant $c$ to all rewards adds $v_c = c/(1-\gamma)$ to every value.
• Exercises 3.18 and 3.19 $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 + \gamma v_\pi(s')]$.
• (3.16)–(3.17) the maximum defining $q_*$ is attained and $q_*(s, a) = \sum_{s', r} p(s', r \mid s, a)[r + \gamma v_*(s')]$.
• (3.20) the Bellman optimality equation for action values, $q_*(s, a) = \sum_{s', r} p(s', r \mid s, a)[r + \gamma \max_{a'} q_*(s', a')]$.

Significance

The goal is what turns "find a good policy" into "solve a system of equations". Parts 3 and 4 identify $v_*$ with the unique solution of (3.19), so any procedure that finds a solution of (3.19) has found $v_*$; part 5 converts $v_*$ into an optimal policy by a one-step search. Parts 1 and 2 say that the book's definition (3.15) makes sense: a single policy is simultaneously best at every state, so "the optimal value function" is well defined and shared by all optimal policies. Chapter 4's policy iteration and value iteration, and the fixed points of Q-learning, are statements about this equation. Exercises 3.18 and 3.19 are used, by number, in the proof of the policy gradient theorem (p. 325).

The mathematics is classical and proved in many texts; what is missing is a machine-checked version in the book's own model. Platform relatives exist in different models: FoundationsML.ReinforcementLearning.bellman_equations_unique_solution (uniqueness for a fixed policy, with an expected-reward kernel instead of $p(s', r \mid s, a)$), BertsekasDP.discounted_main_theorem (cost minimization over deterministic stationary policies), BanditAlgorithm.mdp_discounted_bellman_solution (existence of a solution with a greedy deterministic policy, rewards in $[0,1]$) and FoundationsRL.RLBasics.bellman_optimality (finite horizon). None of them states the book's result: the four-argument dynamics, stochastic policies, the maximum over all of them, uniqueness of the solution of (3.19), and optimality of every policy supported on greedy actions. This mission produces that statement and, with it, a vocabulary of finite-MDP definitions that the later missions of the series reuse.

Difficulty

The book's derivation of (3.19) (p. 63) starts from $v_*(s) = \max_a q_{\pi_*}(s, a)$ with a policy $\pi_*$ that is optimal at every state at once. The existence of such a policy is the substance of the goal, and it does not follow from the definition: (3.15) takes a separate maximum at each state, and a priori the maximizing policy could depend on the state. Uniqueness for (3.19) is likewise not a consequence of linear algebra, as it is for (3.14): the equation is nonlinear because of the maximum. The fixed point must be related to the value of an actual policy, and every policy's value must be bounded above by it.

Formalization scope

• Model. S and A are finite types with A nonempty (without an action, $\max_a$ is undefined). One action set serves every state, as the book's footnote 3 (p. 48) allows. Rewards form a finite set M.R : Finset ℝ and the dynamics are the four-argument M.p s a s' r with the normalization (3.3).
• Discounting. All statements assume $0 \le \gamma < 1$ (the continuing discounted case of §3.3). The episodic case with $\gamma = 1$ is not covered: the book's uniqueness claims then need every episode to terminate under every policy, which the chapter never states, and without it (3.19) can have many solutions (a state that loops to itself with reward $0$ satisfies $v(s) = v(s)$ for any value).
• Value functions from returns. $v_\pi$ and $q_\pi$ are expected discounted returns, computed from the Markov chain the policy induces. They are not defined as solutions of the Bellman equations, and $v_*$ is not defined as a solution of (3.19): either would make the goal true by definition. The Bellman equations are theorems.
• Maxima. $v_*$ and $q_*$ are real suprema over the type of stochastic policies (Lean gives a supremum that does not exist the value $0$); the goal and milestone (3.17) assert that these suprema are attained, so they are the book's maxima.
• Conditional expectations. (3.17), (3.18) and (3.20) are stated in their finite-sum form over $(s', r)$.
• Exercises. Exercises 3.15, 3.18 and 3.19 have no printed solutions; the statements give the formalization's answers ($v_c = c/(1-\gamma)$ and the two displayed identities).
• Reusable infrastructure. The definitions (MDP, Policy, trans, expReward, policyTrans, policyReward, stateValue, actionValue, optimalValue, optimalActionValue, IsOptimalPolicy) follow the conventions shared by the whole series and are meant to be merged with the finite-MDP layers of the later chapters. Lemmas on summability of the value series, the Bellman operator as a $\gamma$-contraction in the sup norm, and the Markov-chain identities for $P_\pi^k$ are welcome as separate contributions.

Selected references

• R. S. Sutton, A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 3. http://incompleteideas.net/book/the-book-2nd.html
• R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://doi.org/10.2307/j.ctv1nxcw0f
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• D. Blackwell, "Discounted dynamic programming", Annals of Mathematical Statistics 36(1), 1965, 226–235. https://doi.org/10.1214/aoms/1177700285
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887