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

The law of the iterated logarithm (LIL) gives the exact almost-sure size of the fluctuations of a sum of random variables. For independent fair $\pm1$ increments $x_1,x_2,\dots$ with partial sums $S_n$, Khinchin (1924) showed that $\limsup_n |S_n|/\sqrt{2n\log\log n}=1$ almost surely; Kolmogorov (1929) extended this to bounded independent increments, and Hartman and Wintner (1941) to independent, identically distributed increments with variance $1$. Weighted sums $a_1x_1+\dots+a_nx_n$ appear in summability theory, in stochastic approximation and in the analysis of orthogonal series, and there the natural normalisation replaces $n$ by the sum of squared weights.

Independence is often not available. In martingale settings (sequential estimation, online learning, adaptive algorithms) the increments are only conditionally centred given the past. In 1967 Kazuoki Azuma (Azuma 1967) introduced a conditional sub-Gaussian condition on martingale differences, called property [G], and proved for it an iterated-logarithm upper bound for weighted sums. The moment-generating-function bound that drives his proof, display (2.4), is the inequality now known as the Azuma–Hoeffding inequality. This mission formalizes Theorem 2 of that paper and the lemmas its proof rests on.

Timeline.

• 1924: Khinchin proves the LIL for fair coin tossing.
• 1929: Kolmogorov proves it for bounded independent increments under a growth condition.
• 1941: Hartman and Wintner prove it for i.i.d. increments with finite variance.
• 1963: Hoeffding proves the exponential tail bound for sums of bounded independent variables.
• 1965: Gaposhkin proves a LIL for weighted (Cesàro and Abel) means of independent variables.
• 1967: Azuma proves the conditional mgf bound (2.4), its maximal version (Lemma 2) and the upper-half LIL for weighted sums of class [G] martingale differences (Theorem 2).

Setting

Let $(\Omega,\mathfrak A,P)$ be a probability space and $(\mathfrak A_n)_{n\ge0}$ an increasing family of sub-$\sigma$-fields of $\mathfrak A$ (a filtration). A sequence of real random variables $(x_n)_{n\ge1}$ is a martingale-difference sequence if each $x_n$ is $\mathfrak A_n$-measurable and integrable and $E\{x_n\mid\mathfrak A_{n-1}\}=0$ almost surely.

The sequence satisfies [G] with $\tau(x_n)\le1$ if, in addition, for every $n\ge1$ and every real $t$,

$$E\{\exp(tx_n)\mid\mathfrak A_{n-1}\}\le\exp(t^2/2)\quad\text{a.s.}$$

Every martingale-difference sequence with $|x_n|\le1$ almost surely has this property, but the class also contains unbounded increments, for instance conditionally standard Gaussian ones.

Fix real weights $(a_n)_{n\ge1}$ of arbitrary sign and write

$$D_n^2=\sum_{j=1}^n a_j^2,\qquad S_n=a_1x_1+\dots+a_nx_n .$$

For the lemmas the weights are called $(b_k)$, and the maximal partial sum is $S_n^*(\omega)=\max_{1\le m\le n}\big|\sum_{k=1}^m b_kx_k(\omega)\big|$.

In Lean these objects are IsMartingaleDiff, IsCondSubgaussianOne, weightedSum ($S_n$), sqWeightSum ($D_n^2$) and maxAbsWeightedSum ($S_n^*$), all in the namespace AzumaWeightedSums.IteratedLog.

Formalization targets

Goal: Theorem 2, display (4.2)

If $(x_n)$ satisfies [G] with $\tau(x_n)\le1$ and the weights satisfy

$$a_n^2/D_n^2\to0,\qquad D_n^2\to\infty,$$

then

$$\limsup_{n\to\infty}\frac{|S_n|}{\sqrt{2D_n^2\log\log D_n^2}}\le1\quad\text{a.s.}$$

The constant $1$ is sharp, as Gaussian increments show, so the goal is stated with the paper's constant and in no weaker form.

Milestones

1. Display (2.4). For every $n$, every real $(b_k)$ and every real $t$,

$$E\Big\{\exp\Big(t\sum_{k=1}^n b_kx_k\Big)\Big\}\le\exp\Big(\frac{t^2}{2}\sum_{k=1}^n b_k^2\Big).$$

2. Doob's $L^\alpha$ maximal inequality, cited on p. 359: for a nonnegative submartingale $(f_m)$ and $\alpha>1$, $E\{(\max_{m\le n}f_m)^\alpha\}\le(\alpha/(\alpha-1))^\alpha E\{f_n^\alpha\}$.
3. Lemma 2, display (2.3). $E\{\exp(tS_n^*)\}\le8\exp\big(\frac{t^2}{2}\sum_{k=1}^n b_k^2\big)$ for every real $t$.
4. Maximal tail bound. If $V_n=\sum_{k=1}^n b_k^2>0$ and $\lambda\ge0$, then $P\{S_n^*>\lambda\}\le8\exp(-\lambda^2/(2V_n))$.

Significance

The result. Theorem 2 controls weighted sums of dependent increments almost surely, uniformly in $n$, at the iterated-logarithm scale. It needs no independence and no boundedness: a conditional sub-Gaussian bound is enough. Bounded martingale differences are a special case, so the theorem covers martingale noise in stochastic approximation and the error terms of adaptive estimators. Milestones 1, 3 and 4 are reusable concentration inequalities: the conditional-expectation form of the Azuma–Hoeffding bound, and its maximal version with an explicit constant.

Formalizing it. The theorem is proved in the literature; nothing here is open. Mathlib has the sub-Gaussian mgf bound for sums in kernel form (HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF, under a standard Borel assumption that this mission does not make), and Doob's weak-type maximal inequality (Submartingale.maximal_ineq). It has no $L^p$ form of Doob's inequality and no law of the iterated logarithm of any kind. Prove2Me has an Azuma–Hoeffding tail bound without the maximum, and nothing at the iterated-logarithm scale. A complete development would therefore add Doob's $L^\alpha$ inequality and the first machine-checked iterated-logarithm upper bound, for a dependent class.

Difficulty

The tail bound (milestone 4) is not enough on its own: applied at each fixed $n$ and summed over $n$, it gives a divergent series at the $\sqrt{2D_n^2\log\log D_n^2}$ scale. The proof has to pass to a subsequence of times and control the maximum over each block, and the blocks have to be fine enough that no constant is lost. The paper's printed proof chooses blocks along which $D_n^2$ roughly doubles. Its third displayed estimate uses the increment $D_{n_{k+1}}^2-D_{n_k}^2$ where the maximal inequality actually delivers the full $D_{n_{k+1}}^2$; with that correction, blocks of ratio $2$ prove (4.2) only with $\sqrt2$ in place of $1$. A faithful formal proof must recover the constant $1$, so the block ratio has to be tuned to $\varepsilon$. Here the hypothesis $a_n^2/D_n^2\to0$ is essential, because it means a single term cannot carry $D_n^2$ past the next block boundary.

Lemma 2 needs Doob's inequality in $L^\alpha$ form for every even integer $\alpha=2j$, uniformly enough to sum an exponential series. The weak-type inequality available in Mathlib does not give this directly.

Formalization scope

• Index base and filtration. Sequences are ℕ → Ω → ℝ with sums over Finset.Icc 1 n; $x_0$ and $a_0$ are ignored. The paper fixes $\mathfrak A_0=\{\emptyset,\Omega\}$; here $\mathfrak A_0$ is arbitrary, which makes every statement at least as strong.
• [G]. For each $n\ge1$ and each real $t$, the conditional bound holds almost surely, in the paper's quantifier order, and $\exp(tx_n)$ is assumed integrable. Without integrability, Lean's conditional expectation is $0$ and the hypothesis would be empty. $\tau$ is not defined as an infimum: "$\tau(x_n)\le1$" is stated as admissibility of the constant $1$.
• Expectations. Expectations of exponentials and powers are lower Lebesgue integrals in $[0,\infty]$, so the inequalities also assert finiteness. A Bochner integral, which is $0$ for non-integrable functions, would make them trivially true.
• The lim sup is not Lean's real-valued limsup, which is $0$ on unbounded sequences. The goal states the equivalent: for every $\varepsilon>0$, almost surely, $|S_n|\le(1+\varepsilon)\sqrt{2D_n^2\log\log D_n^2}$ for all sufficiently large $n$. Because $D_n^2\to\infty$, $\log\log D_n^2>0$ for those $n$, so Real.log is never evaluated at a junk argument that matters.
• Ruled-out trivialisations. Dropping $a_n^2/D_n^2\to0$, replacing [G] by boundedness, weakening the constant $1$, or stating the bound with Lean's real limsup would each change the theorem. None of these is used.
• Infrastructure. A complete proof needs conditional-expectation pull-out lemmas for the induction in (2.4), Doob's $L^p$ inequality (reusable well beyond this mission), Chernoff's bound and the first Borel–Cantelli lemma (both in Mathlib), and a block construction. Proofs of any milestone are welcome, as is a proof of Doob's $L^\alpha$ inequality in Mathlib's own form.

Selected references

• K. Azuma, Weighted sums of certain dependent random variables, Tôhoku Mathematical Journal 19 (1967) 357–367. https://doi.org/10.2748/tmj/1178243286
• J. L. Doob, Stochastic Processes, Wiley, New York, 1953 (the $L^\alpha$ maximal inequality, p. 317; reference [2] of Azuma 1967).
• W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830
• P. Hartman and A. Wintner, On the law of the iterated logarithm, American Journal of Mathematics 63 (1941) 169–176. https://doi.org/10.2307/2371287
• V. F. Gaposhkin, The law of the iterated logarithm for Cesàro's and Abel's methods of summation, Theory of Probability and its Applications 10 (1965) 411–420 (reference [3] of Azuma 1967).

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