Probability

Motivation

An optimization model often needs a probability distribution for an uncertain cost or demand, while a practitioner has only a finite sample from that distribution. Replacing the distribution by the empirical one can hide uncertainty in its estimated mean and covariance. Delage and Ye use a finite-sample confidence region for these two moments to justify a distributional ambiguity set in data-driven stochastic programming Delage and Ye, 2010. The present mission concerns the confidence region itself: it asks how far the population moments can be from the sample estimates when the normalized random vector has bounded support.

The source for every theorem index and page number here is the authors' draft dated 20 February 2008, not an independently checked pagination of the published article. Its §4 starts from independent observations and Assumption 4, then obtains a sample-mean bound, a covariance bound around the known mean, and finally the joint bound for estimates computed entirely from the sample.

Setting

Let $\xi\in\mathbb R^m$ have distribution $P$, mean $\mu=\mathbb E_P[\xi]$, and covariance $\Sigma=\mathbb E_P[(\xi-\mu)(\xi-\mu)^\mathsf T]$. Assume $\Sigma$ is positive definite. For $M\ge1$ independent observations $\xi_1,\ldots,\xi_M$, the empirical mean and empirical covariance in this section are

$$\widehat\mu=\frac1M\sum_{i=1}^M\xi_i,\qquad \widehat\Sigma=\frac1M\sum_{i=1}^M(\xi_i-\widehat\mu)(\xi_i-\widehat\mu)^\mathsf T.$$

The divisor is $M$, including for the covariance; the paper's earlier discussion of an unbiased estimator with divisor $M-1$ does not govern §4. When the true mean is known, write $\widehat\Sigma(\mu)=M^{-1}\sum_i(\xi_i-\mu)(\xi_i-\mu)^\mathsf T$. Matrix order $A\preceq B$ means $B-A$ is positive semidefinite. The squared Mahalanobis distance of a vector $v$ is $v^\mathsf T\Sigma^{-1}v$.

Assumption 4 bounds the normalized observations: for some $R\ge0$, $(\xi-\mu)^\mathsf T\Sigma^{-1}(\xi-\mu)\le R^2$ with probability one. Equivalently, $\zeta=\Sigma^{-1/2}(\xi-\mu)$ lies almost surely in a Euclidean ball of radius $R$; it has mean zero and covariance $I$. The sample law is $P^M$, the product measure of $M$ identical copies. These choices make the probability in each target an assertion about genuinely independent observations.

Formalization targets

Simultaneous confidence region

For $0<\delta<1$, set

$$\alpha(t)=\frac{R^2}{\sqrt M}\left(\sqrt{1-\frac m{R^4}}+\sqrt{\log(1/t)}\right),\qquad \beta(t)=\frac{R^2}{M}\left(2+\sqrt{2\log(1/t)}\right)^2.$$

Theorem 2 is the goal. Write $a=\alpha(\delta/4)$ and $b=\beta(\delta/2)$, and assume $a+b<1$. The target is the simultaneous event

$$(\widehat\mu-\mu)^\mathsf T\Sigma^{-1}(\widehat\mu-\mu)\le b, \qquad \Sigma\preceq\frac{\widehat\Sigma}{1-a-b}, \qquad \frac{\widehat\Sigma}{1+a}\preceq\Sigma$$

with probability at least $1-\delta$. The last denominator is a correction: printed (12c) says $1-a$, while the authors' union-bound display on draft p. 13 says $1+a$. The printed version fails, for example, for symmetric $\pm1$ observations, whose sample covariance is $1-\widehat\mu^2$ and for which its claimed lower bound would require an implausibly large sample-mean square. The proof's displayed bound gives the stated $1+a$ draft pp. 13–14.

Supporting results

Lemma 2 bounds the normalized sample mean. Corollary 1 turns it into the Mahalanobis bound for $\widehat\mu-\mu$. Lemma 3 gives a two-sided matrix bound for $M^{-1}\sum_i\zeta_i\zeta_i^\mathsf T$; Corollary 2 transfers that bound to $\widehat\Sigma(\mu)$. A separate theorem item states the centring identity $\widehat\Sigma(\mu)=\widehat\Sigma+(\widehat\mu-\mu)(\widehat\mu-\mu)^\mathsf T$. The final milestone is the rank-one matrix inequality used in Theorem 2's proof. Their statements follow the draft's §4.1–4.2.

Significance

The joint region places both true moments inside explicit data-dependent matrix inequalities at a chosen confidence level. That is the statistical input for the paper's later moment-based distributional uncertainty sets. The result is known in the source; this mission asks for machine-checked proofs of its corrected statement and its supporting concentration and matrix results. The Lean items are currently open theorem statements, so a successful draft compilation does not constitute formal verification of the inequalities.

Related platform results include a proved two-sided constant-bound McDiarmid inequality (UnderstandingML.mcdiarmid_inequality_pi) and an open per-coordinate upper-tail version (StabGen.Uniform.mcdiarmid_inequality). Neither is identical to the cited Theorem 1 of this draft, so the milestone list starts with the paper's Lemma 2 and does not restate Theorem 1.

Difficulty

The known-mean covariance estimate is a sum of outer products of normalized observations. Controlling its largest and smallest eigenvalues together requires concentration of a matrix-valued statistic, rather than a separate scalar bound for each entry. Once the true mean is replaced by $\widehat\mu$, the covariance changes by a rank-one matrix; the mean bound must control that correction in Loewner order. A direct replacement of $\widehat\Sigma(\mu)$ by $\widehat\Sigma$ therefore does not preserve both sides of Corollary 2 automatically.

Formalization scope

Vectors are Fin m → ℝ, and matrices are real Fin m × Fin m matrices. The Euclidean squared length is a dot product; Lean's generic norm on functions is a supremum norm and is not used for it. The Loewner order is (B - A).PosSemidef. The distribution has a probability measure and coordinatewise finite $L^2$ moments, so its real-valued mean and covariance integrals are well defined. The true covariance is positive definite, reflecting the section's nonsingularity assumption. Samples have the product law $P^M$. The chapter's normalized case records zero mean, identity covariance, and the almost-sure ball bound.

Every statistical result assumes $0<\delta<1$; the logarithms and confidence levels are then in their intended domain. Positive $M$ rules out division by zero in empirical averages. Lemma 3 carries the paper's explicit sample-size threshold, and the goal reads “$M$ large enough” as $a+b<1$, which keeps the upper covariance denominator positive. The expression under the other square root is nonnegative in every satisfiable positive-dimensional normalized setting, because $\mathbb E\|\zeta\|_2^2=m\le R^2$. It is not an added assumption. The probability conclusions use $\ge1-\delta$, which is what the paper's proofs show despite the phrase “greater than.”

The goal assumes the source's distributional and support conditions, not the probability conclusions of its supporting corollaries. This prevents a vacuous route that merely postulates the desired confidence event. A complete proof will need reusable product-measure concentration facts, moment and matrix algebra, and a positive-definite quadratic-form bridge. Contributions to those components and to each milestone are in scope. Corollary 3's data-derived radius is excluded because the draft's conditioning argument does not establish its claimed confidence level. Corollary 4 as a probability statement, Theorem 3, and Corollary 5 depend on it; Remark 2 concerns a separate Gaussian eigenvalue density.

Selected references

• Erick Delage and Yinyu Ye, Distributionally Robust Optimization under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3), 595–612, 2010; source used here: authors' draft of 20 February 2008. DOI.

Motivation

In most control problems the controller does not see the state of the system. It sees noisy observations, remembers its past controls, and must act on that record. Inventory systems with delayed or inaccurate counts, maintenance of machines whose wear is only inspected, target tracking, and medical treatment planned from test results all have this form. The standard device for such problems is to replace the hidden state by a summary of the record, most often the conditional distribution of the state given the observations, and to solve a dynamic program whose state is that summary.

For finite or countable spaces this reduction goes back to Åström (1965) and Striebel (1965), who introduced the conditional distribution of the state as a "sufficient statistic" for control. Chapter 10 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996) carries it out for Borel state, control and observation spaces, with universally measurable policies and costs that are only lower semianalytic. In that generality the measurability of the reduced model is the whole difficulty, and the chapter isolates exactly what a summary must satisfy for the reduction to be exact.

Setting

The imperfect state information model (ISI) of Definition 10.3 has a nonempty Borel state space $S$, control space $C$ and observation space $Z$; a discount factor $\alpha>0$; a lower semianalytic cost $g:SC\to R^*=[-\infty,\infty]$; a Borel state transition kernel $t(dx'\mid x,u)$; Borel observation kernels $s_0(dz\mid x)$ and $s(dz\mid u,x)$; and a horizon $N$. The initial state $x_0$ has distribution $p\in P(S)$, $z_0\sim s_0(\cdot\mid x_0)$, and then $x_{k+1}\sim t(\cdot\mid x_k,u_k)$, $z_{k+1}\sim s(\cdot\mid u_k,x_{k+1})$. The controller knows the information vector $i_k=(z_0,u_0,\dots,u_{k-1},z_k)\in I_k$ and must choose $u_k\in U_k(i_k)$, where the constraint set $\Gamma_k=\{(i_k,u)\mid u\in U_k(i_k)\}$ is analytic.

A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ consists of universally measurable stochastic kernels $\mu_k(du_k\mid p;i_k)$ that respect the constraints (Definition 10.4). Together with $p$ it determines probability measures $P_k(\pi,p)$ on the histories $(x_0,z_0,u_0,\dots,x_k,z_k,u_k)$, the cost

$$J_{N,\pi}(p)=\int\Big[\sum_{k=0}^{N-1}\alpha^k g(x_k,u_k)\Big]dP_{N-1}(\pi,p),$$

and the optimal cost $J^*_N(p)=\inf_\pi J_{N,\pi}(p)$ (Definition 10.5). Assumption $(F^+)$ asks that the expected discounted negative part of the cost be finite for every policy and initial distribution; $(F^-)$ asks the same of the positive part.

A statistic is a sequence of Borel maps $\eta_k:P(S)I_k\to Y_k$ into nonempty Borel spaces. It is sufficient for control (Definition 10.6) if (a) the constraints can be read off from it, $\Gamma_k=\{(i_k,u)\mid(\eta_k(p;i_k),u)\in\hat\Gamma_k\}$ with $\hat\Gamma_k$ analytic; (b) the conditional law of $\eta_{k+1}$ given $(\eta_k,u_k)$ is a Borel kernel $\hat t_k(dy_{k+1}\mid y_k,u_k)$, for every $p$ and every policy; and (c) the conditional expectation of $g(x_k,u_k)$ given $(\eta_k,u_k)$ is a lower semianalytic function $\hat g_k(y_k,u_k)$. The perfect state information model (PSI) of Definition 10.7 has states $y_k\in Y_k$, constraints $\hat U_k(y_k)=(\hat\Gamma_k)_{y_k}$, costs $\hat g_k$ and transitions $\hat t_k$; its cost and optimal cost at $y\in Y_0$ are $\hat J_{N,\hat\pi}(y)$ and $\hat J^*_N(y)$. The initial distribution of $y_0$ is

$$\varphi(p)(\underline Y_0)=\int_S s_0(\{z_0\mid\eta_0(p;z_0)\in\underline Y_0\}\mid x_0)\,p(dx_0).$$

A Markov (PSI) policy $\hat\mu_k(du\mid y_k)$ acts in (ISI) through $\mu_k(du\mid p;i_k)=\hat\mu_k(du\mid\eta_k(p;i_k))$.

Formalization targets

Goal: Proposition 10.3

Under $(F^+,\hat F^+)$ or $(F^-,\hat F^-)$,

$$J^*_N(p)=\int_{Y_0}\hat J^*_N(y_0)\,\varphi(p)(dy_0)\qquad\forall p\in P(S),$$

and a Markov (PSI) policy that is optimal, $\varphi(p)$-optimal or weakly $\varphi(p)$-$\varepsilon$-optimal for (PSI) is respectively optimal, optimal at $p$, or $\varepsilon$-optimal at $p$ for (ISI); under $(F^+,\hat F^+)$ an $\varepsilon$-optimal (PSI) policy is $\varepsilon$-optimal for (ISI). Here $\hat\pi$ is weakly $q$-$\varepsilon$-optimal if $\int\hat J_{N,\hat\pi}\,dq\le\int\hat J^*_N\,dq+\varepsilon$ when $\int\hat J^*_N\,dq>-\infty$ and $\int\hat J_{N,\hat\pi}\,dq\le-1/\varepsilon$ otherwise, and $q$-optimal if $q(\{y_0\mid\hat J_{N,\hat\pi}(y_0)=\hat J^*_N(y_0)\})=1$ (Definition 10.8).

Milestones

1. Lemma 10.1: the process $(\eta_0,u_0,\dots,\eta_k,u_k)$ generated in (ISI) by a Markov (PSI) policy has the law $\hat P_k[\hat\pi,\varphi(p)]$.
2. Proposition 10.2: $J_{N,\hat\pi}(p)=\int\hat J_{N,\hat\pi}\,d\varphi(p)$ for Markov $\hat\pi$.
3. Corollary 10.2.1: $J^*_N(p)\le\int\hat J^*_N\,d\varphi(p)$.
4. Lemma 10.2: every (ISI) policy is matched in cost by some Markov (PSI) policy.
5. Proposition 10.4: $\varepsilon$-optimal nonrandomized (ISI) policies that depend on $i_k$ only through $\eta_k(p;i_k)$.
6. Proposition 10.6: the identity maps on $P(S)I_k$ form a statistic sufficient for control.

Significance

Proposition 10.3 says that an imperfect-information problem loses nothing by being solved in the reduced model: the optimal cost is the $\varphi(p)$-average of the reduced optimal cost, and good reduced policies are good original policies. Combined with Proposition 10.6, every (ISI) model has such a reduction, so the finite-horizon dynamic programming theory of Chapter 8 (existence of $\varepsilon$-optimal policies, the dynamic programming algorithm) transfers to partially observed problems on Borel spaces. Proposition 10.4 turns this into a structural statement about the original problem: nearly optimal controllers need to retain only the statistic.

These results are proved in the book. None of them is formalized: the platform's related results (Bäuerle–Rieder's partially observable models with observation densities, and the linear-quadratic-Gaussian separation theorem) work in different models and do not cover universally measurable policies, analytic constraints, or lower semianalytic costs. A machine-checked version makes the conditional-expectation bookkeeping of the reduction explicit, and the definitions of this mission (universal measurability, lower semianalytic functions, the book's extended integral, history measures built from universally measurable kernels) are reusable by every other chapter of the book.

Difficulty

The obvious argument says: replace the state by the statistic, observe that costs and transitions depend only on the statistic, and conclude. In the Borel setting each step is a measurability claim that the naive argument does not supply. The conditions of Definition 10.6 are almost-everywhere statements about conditional distributions under every pair $(p,\pi)$, while the reduced model needs genuine kernels; the policies are only universally measurable, so integrals and compositions must be taken with respect to completions; the costs take the values $\pm\infty$, so interchanging sums and integrals requires the finiteness assumptions $(F^\pm)$ and $(\hat F^\pm)$; and the inequality $J^*_N\ge\int\hat J^*_N\,d\varphi(p)$ requires producing, from an arbitrary history-dependent (ISI) policy, a Markov (PSI) policy with the same cost, which the naive argument does not do.

Formalization scope

• Horizon. Only finite horizons $N\ge1$ are covered, hence only the cases $(F^+,\hat F^+)$ and $(F^-,\hat F^-)$ of the book's statements; the infinite-horizon cases $(P,\hat P)$, $(N,\hat N)$, $(D,\hat D)$ are out of scope.
• Extended reals. Costs live in EReal with the book's convention $\infty-\infty=+\infty$ written out explicitly (badd, bsum, extIntegral); Mathlib's EReal subtraction ($\top-\top=\bot$) is never used where both terms can be infinite.
• Spaces and measures. $S$, $C$, $Z$, $Y_k$ are Borel spaces in the sense of Definition 7.7 with their Borel $\sigma$-algebras; $P(S)$ carries the weak topology and the Giry $\sigma$-algebra. Policies are families of maps into ProbabilityMeasure C that are measurable for the completion of every probability measure. History measures are characterized by their values on rectangles. Families indexed by the stage are indexed by all of $\mathbb N$; only stages $k<N$ are constrained.
• Conditional statements. Conditions (22) and (23) are stated through the defining relations of conditional probability and expectation, for every $p$ and every policy, with (23) required when $g(x_k,u_k)$ is quasi-integrable.
• Policies in Proposition 10.3. The (PSI) policies in the optimality transfers are Markov, as in Proposition 10.2.
• No trivialization. Definition 10.6 is the full definition: analytic $\hat\Gamma_k$ with full projection, Borel kernels $\hat t_k$ satisfying (22) for every $p$ and policy, and lower semianalytic $\hat g_k$ satisfying (23); a weaker notion would make Proposition 10.6 empty.

Contributions are welcome on any milestone. Basic facts that a full development needs, such as composition of universally measurable maps (Proposition 7.44), measurability of integrals against universally measurable kernels (Proposition 7.46), and existence of the history measures (Proposition 7.45), can be posed and proved as supporting lemmas; they are reusable across the book.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific, 1996, Chapter 10. https://web.mit.edu/dimitrib/www/soc.html
• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10 (1965) 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
• C. Striebel, Sufficient statistics in the optimum control of stochastic systems, Journal of Mathematical Analysis and Applications 12 (1965) 576–592. https://doi.org/10.1016/0022-247X(65)90027-2
• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5. https://doi.org/10.1007/978-3-642-18324-9

Motivation

Finite-horizon stochastic control on general state and control spaces — inventory levels, queue lengths, positions, beliefs — cannot be written down without measure theory, and the measure theory turns out to be the hard part. The dynamic programming (DP) recursion "start from zero and minimise one stage at a time" is easy to state, but on uncountable spaces the minimisation in each step produces functions that need not be Borel-measurable, and the infimum over policies has to be taken over a class large enough to contain near-minimisers. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978; Athena reprint 1996) resolved this by working with universally measurable policies and lower semianalytic costs. Chapter 8 is the finite-horizon core of that theory, and the infinite-horizon results of Chapter 9 and the imperfect-information reduction of Chapter 10 are built on it.

Timeline. Blackwell (1965) treated discounted problems on Borel spaces with bounded costs and Borel policies, where ε-optimal Borel policies may fail to exist. Strauch (1966) studied positive and negative models. Blackwell, Freedman and Orkin (1974) introduced analytic sets and analytically measurable policies into DP. Bertsekas and Shreve (1978, Chapters 7–8) gave the universally measurable finite-horizon theory formalized here, including the unbounded-cost assumptions (F⁺)/(F⁻).

Setting

A finite horizon stochastic optimal control model is a nine-tuple $(S,C,U,W,p,f,\alpha,g,N)$. The state space $S$, control space $C$ and disturbance space $W$ are nonempty Borel spaces (topological spaces homeomorphic to Borel subsets of complete separable metric spaces). The constraint $U(x)\subseteq C$ is nonempty and $\Gamma=\{(x,u)\mid u\in U(x)\}$ is analytic in $S\times C$. Disturbances are drawn from a Borel stochastic kernel $p(dw\mid x,u)$, the system moves by $x_{k+1}=f(x_k,u_k,w_k)$ with $f$ Borel, the discount factor $\alpha$ is a positive real, the one-stage cost $g:\Gamma\to[-\infty,\infty]$ is lower semianalytic ($\{g<c\}$ is analytic for every real $c$), and $N\ge1$ is the horizon. The state transition kernel is $t(B\mid x,u)=p(\{w\mid f(x,u,w)\in B\}\mid x,u)$.

A set is universally measurable if it is measurable for the completion of the Borel σ-algebra under every probability measure. A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ chooses $u_k$ from a universally measurable stochastic kernel $\mu_k(du_k\mid x_0,u_0,\dots,x_k)$ concentrated on $U(x_k)$; it is Markov if $\mu_k$ depends on $x_k$ only, and nonrandomized if every $\mu_k(\cdot\mid\cdot)$ is a point mass. $\Pi'$ denotes all policies and $\Pi$ the Markov ones. A policy and an initial distribution $p$ determine a probability measure $r_N(\pi,p)$ on state–control paths, and the $K$-stage cost and optimal cost are

$$J_{K,\pi}(x)=\int\Big[\sum_{k=0}^{K-1}\alpha^k g(x_k,u_k)\Big]dr_N(\pi,p_x),\qquad J^*_K(x)=\inf_{\pi\in\Pi'}J_{K,\pi}(x).$$

Assumption (F⁺) requires $\int g^-\,dq_k(\pi,p_x)<\infty$, and (F⁻) requires $\int g^+\,dq_k(\pi,p_x)<\infty$, for every policy, initial state and stage, where $q_k$ is the marginal of $r_N$ on the $k$-th pair. The DP operators are

$$T_\mu(J)(x)=\int_C\Big[g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big]\mu(du\mid x),\qquad T(J)(x)=\inf_{u\in U(x)}\Big\{g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big\}.$$

Formalization targets

Goal: Proposition 8.2

$$J^*_K=T^K(J_0),\qquad K=1,\dots,N,$$

under (F⁺) or (F⁻), where $J_0\equiv0$. The goal leaves the horizon, the discount factor and the sign of $g$ unrestricted beyond (F⁺)/(F⁻), and it compares an infimum over all history-dependent randomized policies with a pointwise recursion.

Milestones

In attack order: Lemma 8.1 (the cost of a Markov policy equals $T_{\mu_0}\cdots T_{\mu_{K-1}}(J_0)$), Proposition 8.1 and Corollary 8.1.1 (Markov policies suffice), Lemma 8.2 (an ε-optimal universally measurable kernel for one application of $T$), Lemma 8.3 (under (F⁺), $T^K(J_0)>-\infty$), Lemma 8.4 (monotone and bounded convergence for $T_\mu$). Two consequences of the goal complete the chapter's existence theory: Corollary 8.2.1 ($J^*_K$ is lower semianalytic) and Proposition 8.3 (ε-optimal nonrandomized Markov policies under (F⁺); nonrandomized semi-Markov and randomized Markov ones under (F⁻)).

Significance

Proposition 8.2 says the DP algorithm computes the true optimal cost of the Borel model, with no restriction to Markov or nonrandomized policies and with costs that may be unbounded in either direction. Corollary 8.2.1 identifies the regularity of the value function — lower semianalytic, possibly not Borel (Example 1 of Chapter 8) — and Proposition 8.3 turns the recursion into near-optimal policies. These results are the base case for the infinite-horizon theory of Chapter 9 (positive, negative and discounted models are analysed as limits of finite-horizon problems) and for the sufficient-statistic reduction of Chapter 10.

All results here are proved in the book. None is formalized: the platform has finite-state, finite-action DP theorems and Borel models with Borel-measurable policies, but no universally measurable policies, no lower semianalytic costs and no Ionescu-Tulcea construction for universally measurable kernels. The mission poses the finite-horizon Borel theory, with reusable infrastructure: the universal σ-algebra, universally measurable kernels, iterated path integrals representing integration against the induced path measure, and the operator calculus on extended-real functions with the convention $\infty-\infty=\infty$.

Difficulty

The obvious argument fails at measurability. On countable spaces, Proposition 8.2 follows from the Part I argument: induct on $K$, choose near-minimising controls state by state, assemble them into a policy. On Borel spaces, a pointwise choice of near-minimisers is not a policy unless it is measurable, and $T(J)$ is generally not Borel even when $J$ and $g$ are; Borel policies are too few for $\varepsilon$-optimal ones to exist. The book's way out needs the selection theorem for lower semianalytic functions (Proposition 7.50), integration of universally measurable functions against universally measurable kernels (Propositions 7.45–7.46), and care with infinite values: without (F⁺) or (F⁻), the integral of the stage sum and the sum of the stage integrals can disagree, and Lemma 8.1 fails.

Formalization scope

Lean conventions:

• Spaces carry [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [IsBorelSpace X] [Nonempty X]. IsBorelSpace is the book's Definition 7.7.
• Extended reals are EReal. Addition inside costs and integrands uses the book's convention $-\infty+\infty=+\infty$ (badd), not Mathlib's, which gives $\bot+\top=\bot$. Integrals are $\int f^+-\int f^-$ with $\infty-\infty=\infty$ (extInt).
• The universal σ-algebra is the intersection of all completions (universalSigma). Kernels are universally measurable in the sense of Lemma 7.28(b).
• The integral against $r_N(\pi,p)$ is the iterated integral of Eq. (4) of Chapter 8 (pathInt).
• Stages are indexed $0,\dots,N-1$, and a history is $k$ state–control pairs plus the current state.
• $g$ is stored on $S\times C$, but only its values on $\Gamma$ are constrained or used.

A trivializing formalization is excluded by construction. $J^*_K$ is the infimum over all policies in $\Pi'$, not over Markov or nonrandomized ones. $J_{K,\pi}$ is the integral of the stage sum against the path measure, never the operator composition of Lemma 8.1, so the goal does not collapse to the Part I result.

A complete development needs:

• the analytic-set and universal-measurability theory of §7.6–7.7: closure of analytic sets under projections and sections, measurability of integrals against universally measurable kernels (Proposition 7.46), and the selection theorem (Proposition 7.50);
• extended-real integration lemmas in the style of Lemma 7.11.

This infrastructure is reusable for the infinite-horizon Borel models (Chapter 9), for the imperfect-information reduction (Chapter 10), and for papers that cite this book. Contributions of these supporting lemmas as separate theorems are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996, Chapter 8. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
• R. E. Strauch, Negative dynamic programming, Ann. Math. Statist. 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
• D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Ann. Probab. 2 (1974), 926–941. https://doi.org/10.1214/aop/1176996558
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Math. Oper. Res. 4 (1979), 15–30. https://doi.org/10.1287/moor.4.1.15

Motivation

In a multi-armed bandit problem a learner chooses one of $K$ actions in each of $n$ rounds and observes only the reward of the chosen action. Two models of the rewards have separate theories. In the stochastic model, each arm pays independent draws from a fixed distribution; algorithms such as UCB1 (Auer, Cesa-Bianchi & Fischer 2002) have regret of order $\sum_i \log(n)/\Delta_i$, logarithmic in $n$. In the adversarial model, an adversary chooses the rewards; Exp3 and its variants (Auer, Cesa-Bianchi, Freund & Schapire 2002) have regret of order $\sqrt{nK}$, which is optimal there. An algorithm tuned for one model fails in the other: stochastic algorithms can suffer linear regret against an adversary, and adversarial algorithms pay $\sqrt n$ even when the rewards are i.i.d.

Bubeck and Slivkins (arXiv:1202.4473, COLT 2012) asked whether one algorithm can be near-optimal in both models without knowing which one it faces. They answered yes with the algorithm SAO. This result started the "best of both worlds" line of work on bandits. Later contributions include EXP3++ (Seldin & Slivkins 2014) and Tsallis-INF (Zimmert & Seldin 2021).

Setting

There are $K\ge2$ arms and $n\ge K$ rounds. On round $t$ the algorithm draws an arm $I_t$ from a probability vector $p_t=(p_{1,t},\dots,p_{K,t})$ computed from the history it has observed. At the same time a reward vector $g_t\in[0,1]^K$ is fixed, and the algorithm observes only $g_{I_t,t}$.

• Adversarial model. The vector $g_t$ is chosen by an adaptive adversary: a function of the arms $I_1,\dots,I_{t-1}$ played earlier, but not of $I_t$. The regret is $R_n=\max_i\sum_{t=1}^n g_{i,t}-\sum_{t=1}^n g_{I_t,t}$.
• Stochastic model. There are distributions $\nu_1,\dots,\nu_K$ on $[0,1]$ with means $\mu_i$, and all $g_{i,t}\sim\nu_i$ are independent. The pseudo-regret is $\overline R_n=\sum_{t=1}^n(\max_i\mu_i-\mu_{I_t})$. The gap of arm $i$ is $\Delta_i=\max_j\mu_j-\mu_i$, and the minimal gap is $\Delta=\min_{i:\Delta_i>0}\Delta_i$.

The analysis uses importance-weighted estimates $\widetilde H_{i,t}=\frac1t\sum_{s\le t}g_{i,s}\mathbb 1_{\{I_s=i\}}/p_{i,s}$, the sample means $\widehat H_{i,t}$, the averages $H_{i,t}=\frac1t\sum_{s\le t}g_{i,s}$, and the play counts $T_i(t)$.

SAO (Algorithm 1 of the paper) takes a parameter $\beta>1$. It keeps a set of active arms, initially all arms, and samples them uniformly at first. On each round it applies a test, (12), that deactivates an arm whose estimate $\widetilde H_{i,t}$ falls far below the best active one. The probability of a deactivated arm then decays as $q_i\tau_i/t$, where $\tau_i$ is the deactivation time and $q_i$ the arm's probability at that moment. Three further tests, (13)–(15), check that the observations stay consistent with stochastic rewards. If any of them fails on round $\tau_0$, SAO switches permanently to the adversarial algorithm Exp3.P (Bubeck & Cesa-Bianchi 2012, Fig. 3.1) for the remaining rounds.

Formalization targets

Goal: Theorem 4.1, high-probability form

For every $\delta\in(0,1)$ let $\beta=10Kn^3\delta^{-1}$. With probability at least $1-\delta$, SAO with parameter $\beta$ satisfies, in the stochastic model (whenever some arm has $\Delta_i>0$),

$$\overline R_n\le\frac{260K(1+\log K)\log^2(\beta)}{\Delta},$$

and, against every adaptive adversary with rewards in $[0,1]$,

$$R_n\le60(1+\log K)(1+\log n)\sqrt{nK\log(\beta)+5K^2\log^2(\beta)}+200K^2\log^2(\beta).$$

Milestones

The milestones follow the paper's proof in order:

• Freedman's inequality (Theorem 4.3) in the paper's two-sided form, and its variance-adaptive form, Lemma 4.4.
• The concentration lemmas for SAO's estimates (Lemmas 4.5, 4.6, 4.7) and the Exp3.P phase (Lemma 4.8).
• The two good events of §4.1, (21)–(25).
• The deterministic consequences on those events: Exp3.P is never started in the stochastic model; suboptimal arms are deactivated by time $260K\log(\beta)/\Delta_i^2$; $\sum_iq_i\le1+\log K$, (27); and the adversarial regret bound of §4.3.
• The two halves of Theorem 4.1.

Significance

The theorem shows that the stochastic and adversarial regret rates are not in conflict. A single algorithm, with no information about the model, gets $O(K\log K\log^2(n/\delta)/\Delta)$ pseudo-regret on stochastic rewards and $\tilde O(\sqrt{nK})$ regret against adaptive adversaries. Each rate is within polylogarithmic factors of optimal for its model. Later algorithms improved the logarithmic factors and removed the explicit switching, but they are compared against this result.

The theorem is proved in the paper. It is not known to have a machine-checked proof. Formalizing it requires a precise model of an adaptive adversary interacting with a randomized algorithm, martingale concentration with random variance (Lemma 4.4), and an exact statement of SAO including its boundary cases. The pieces are reusable: the interaction model, the estimators, Exp3.P and its high-probability guarantee all apply to other adversarial bandit results.

Difficulty

Neither standard analysis carries over. In the stochastic model, SAO's sampling probabilities are random and depend on the past, and a deactivated arm's probability keeps changing. Hoeffding-type bounds for a fixed sampling scheme therefore do not apply to $\widetilde H_{i,t}$. The variance of the importance-weighted estimate grows like $\sum_s1/p_{i,s}$, which is controlled only through the algorithm's own schedule (16). This is why Lemma 4.5 has the two-part radius with $\max(t-\tau_i,0)/(q_i\tau_it)$. In the adversarial model, the deterministic argument has to show that whenever the consistency tests pass, the regret accumulated before the switch is already small, for an adversary that adapts to the arms played. A union bound over all quantities, all arms and all times (§4.1) is needed before any deterministic reasoning, so every constant in the event matters.

Formalization scope

All declarations live in the namespace BestBothWorlds.SAO.

• Arms and paths. Arms are Fin K and rounds are $1,\dots,n$. An arm path is Fin n → Fin K.
• Algorithms and adversaries. An algorithm is a deterministic map from the observed history to a probability vector. A deterministic adaptive adversary is a map from the list of earlier arms to a reward vector; randomized adversaries are mixtures of these.
• Probabilities. For a fixed adversary, the probability of an event is $\sum_{I\in E}\prod_tp_{I_t,t}$. In the stochastic model this is integrated against the product law of the reward table.
• Logarithms and constants. Real.log is the natural logarithm. All constants of Theorem 4.1 are explicit, with $\beta=10Kn^3\delta^{-1}$.
• SAO. It is defined exactly as Algorithm 1. Arms are tested in order within a round, and the active set changes during the loop. Test (13) is false when $T_i(t)=0$, and test (14) is false when $\tau_i=1$.
• Exp3.P. After the switch, Exp3.P runs from scratch for $n-\tau_0$ rounds. Its parameters are those of Bubeck–Cesa-Bianchi Theorem 3.2 with confidence $K/\beta$, and $\gamma$ and $\beta_{\mathrm P}$ are clipped at $1$.
• §4 notation. $\tau_0$, $\tau_i\leftarrow\min(\tau_i,\tau_0)$ and $q_i=p_{i,\min(\tau_i,\tau_0)}$ are computed from the run, never assumed.

A trivializing formalization is ruled out. The goal's hypotheses concern only the instance ($K$, $n$, $\delta$, the distributions or the adversary). The algorithm's quantities ($\tau_0$, $\tau_i$, $q_i$, the sampling probabilities) are computed by the definition of SAO and are never free variables or hypotheses. The adversarial half covers adaptive adversaries, not only oblivious reward tables.

The expectation form of Theorem 4.1 ($O(\cdot)$ bounds with $\beta=n^4$), Theorem 1.1 and the two-armed warm-up of §3 are out of scope. Proofs of any milestone are welcome, as are alternative proofs of the concentration lemmas from Mathlib's martingale library.

Selected references

• S. Bubeck and A. Slivkins, The best of both worlds: stochastic and adversarial bandits, COLT 2012; arXiv:1202.4473v1. https://arxiv.org/abs/1202.4473
• S. Bubeck and N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://doi.org/10.1561/2200000024
• D. A. Freedman, On tail probabilities for martingales, Annals of Probability 3(1), 1975. https://doi.org/10.1214/aop/1176996452
• P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• P. Auer, N. Cesa-Bianchi, Y. Freund and R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• Y. Seldin and A. Slivkins, One practical algorithm for both stochastic and adversarial bandits, ICML 2014. https://proceedings.mlr.press/v32/seldinb14.html
• J. Zimmert and Y. Seldin, Tsallis-INF: an optimal algorithm for stochastic and adversarial bandits, JMLR 22, 2021. https://jmlr.org/papers/v22/19-753.html

Motivation

Many queues observed at well-chosen instants are Markov chains on the nonnegative integers. For the single-server queue with Poisson arrivals and general service times (M/G/1), D. G. Kendall showed in 1951 that the number of customers left behind at successive departure epochs is such a chain, the imbedded Markov chain (Kendall 1951; Kendall 1953). Whether the queue settles into a steady state, keeps returning to empty without settling, or grows without bound is then a question about this chain: is it ergodic, null recurrent, or transient?

F. G. Foster's 1953 paper (doi:10.1214/aoms/1177728976) answers this question by first proving general criteria for an irreducible chain on $\{0,1,2,\dots\}$, stated as solvability conditions for linear inequalities in the transition matrix, and then applying them to the M/G/1 and GI/M/1 chains. Theorem 2 of the paper is the drift condition now known as Foster's criterion, the starting point of the Lyapunov-function method for the stability of queues and stochastic networks (Meyn and Tweedie 2009). This mission is the M/G/1 half of the paper.

Timeline:

• 1951–1953, Kendall. Introduces the imbedded chains of M/G/1 and GI/M/1 and obtains most of their classification by direct methods.
• 1953, Foster. Derives the classification from general criteria: Theorem 2 (ergodicity), Theorems 4–6 (transience and recurrence).
• 1950s onward. The criteria become the standard tools (Feller's text; later the drift conditions of Meyn and Tweedie).

Setting

A Markov chain on the states $\{0,1,2,\dots\}$ is given by a transition matrix $P=[p_{ij}]$: $p_{ij}\ge0$ and $\sum_j p_{ij}=1$ for every row $i$. Write $f_{ij}^{(n)}$ for the probability that the chain started in $i$ first reaches $j$ (for $i=j$, first returns to $j$) at step $n\ge1$. The chain is irreducible if every state can be reached from every other, and aperiodic if for every state the return times have greatest common divisor $1$. A state $j$ is recurrent if $f_{jj}=\sum_n f_{jj}^{(n)}=1$ and transient if $f_{jj}<1$; a recurrent state is ergodic (positive recurrent, "recurrent-nonnull") if in addition its mean recurrence time $\sum_n n f_{jj}^{(n)}$ is finite. The mean first-passage time from $i$ to $j$ is $\mu_{ij}=\sum_{n\ge1} n f_{ij}^{(n)}\in[0,\infty]$.

The M/G/1 matrix is built from a sequence $k_0,k_1,\dots$ of positive numbers summing to one ($k_n$ is the probability of $n$ arrivals during one service):

$$[p_{ij}] = \begin{bmatrix} k_0 & k_1 & k_2 & \cdots \\ k_0 & k_1 & k_2 & \cdots \\ 0 & k_0 & k_1 & \cdots \\ 0 & 0 & k_0 & \cdots \\ \vdots & \vdots & \vdots & \end{bmatrix},$$

that is, $p_{0j}=k_j$ and, for $i\ge1$, $p_{ij}=k_{j-i+1}$ when $j\ge i-1$ and $0$ otherwise. The traffic intensity is

$$\rho=\sum_{n=1}^{\infty}n\,k_n\in[0,\infty],$$

the mean number of arrivals per service.

Formalization targets

Goal: the M/G/1 classification (§3, p. 358)

$$\text{the chain is ergodic}\iff\rho<1,\qquad\text{the chain is recurrent}\iff\rho\le1 .$$

The goal leaves $k$ arbitrary apart from positivity and normalization; in particular $\rho=\infty$ is allowed and falls in the transient case.

Milestones (the paper's general theorems and the step of §3 they feed)

1. Theorem 2 (drift criterion): a nonnegative solution of $\sum_j p_{ij}y_j\le y_i-1$ ($i\ne0$) with $\sum_j p_{0j}y_j<\infty$ makes the system ergodic. Already posed on the platform and referenced here.
2. Theorem 3: in an ergodic system the mean first-passage times $d_j=\mu_{j0}$ are finite and satisfy $\sum_{j\ge1}p_{ij}d_j=d_i-1$ ($i\ne0$), $\sum_{j\ge1}p_{0j}d_j<\infty$.
3. §3 display: for the ergodic M/G/1 chain, $\mu_{i,i-1}=\mu_{10}$ and $\mu_{i0}=i\mu_{10}$ ($i\ne0$).
4. Theorem 5: a solution of $\sum_j p_{ij}y_j\le y_i$ ($i\ne0$) with $y_i\to\infty$ makes the system recurrent.
5. Theorem 7: for a probability distribution $\{p_n\}$ with $p_0>0$, $\sum_n z^np_n=z$ has a root in $(0,1)$ iff $\sum_{n\ge1}np_n>1$.
6. Theorem 4: the system is transient iff $\sum_j p_{ij}y_j=y_i$ ($i\ne0$) has a bounded nonconstant solution.

Significance

The result. The classification is the stability theorem for the M/G/1 queue: for $\rho<1$ the departure-epoch queue length has a stationary distribution, which is what the Pollaczek–Khinchine formula describes; for $\rho=1$ the queue empties infinitely often but has no steady state; for $\rho>1$ it grows without bound. The general criteria behind it (Theorems 2, 4, 5) apply to any chain on the nonnegative integers and are reused in the companion GI/M/1 mission and throughout queueing and Markov-chain stability theory.

Formalizing it. All results here are proved on paper (Kendall and Foster, 1951–1953, with Theorems 3 and 7 classical lemmas from Feller). None of them is known to have a machine-checked proof against a Lean development of countable-state Markov chains. The mission produces such proofs on the published discrete-chain vocabulary (transition matrices, first-passage probabilities, return probabilities, positive recurrence), together with the general Foster criteria as reusable theorems. Theorem 2 is already posed as an open platform theorem and is reused here.

Difficulty

The queue-specific part of the argument is short once the general criteria are available; the weight of the mission is in those criteria. They relate qualitative properties of an infinite chain (ergodicity, recurrence, transience) to solvability of infinite systems of linear inequalities, and this needs limit behaviour of the $n$-step probabilities $p_{ij}^{(n)}$ and of hitting probabilities of state $0$, none of which follows from finite-state arguments. Two further points resist the naive approach. The converse directions (ergodic $\Rightarrow\rho<1$, recurrent $\Rightarrow\rho\le1$) need exact identities for mean first-passage times, not just bounds, and these must be handled in $[0,\infty]$ because the means may be infinite. And the boundary case $\rho=1$ (null recurrence) separates the two equivalences: an argument that only compares the mean drift $\rho-1$ with $0$, such as a law of large numbers for the increments, cannot tell recurrence from transience there.

Formalization scope

• The chain is the published QueueingFundamentals.Foundations.TransitionMatrix (entries P.p i j, rows summing to $1$ as a HasSum), with its firstPassage, returnProb, Irreducible, Aperiodic and PositiveRecurrent. "Ergodic" is P.PositiveRecurrent; aperiodicity is the paper's standing assumption and is not folded into it a second time.
• States are indexed from $0$, as in the paper; "$i\ne0$" is i ≠ 0.
• The M/G/1 matrix is a function mg1Matrix k : ℕ → ℕ → ℝ; the goal and the §3 display quantify over every TransitionMatrix P with P.p = mg1Matrix k. Such a P exists for every admissible k (checked in a sorry-free local file for $k_i=2^{-(i+1)}$).
• $\sum_n k_n=1$ is added as the meaning of "stochastic matrix"; §3 writes only $k_i>0$.
• $\rho$ and all mean first-passage times are extended nonnegative reals ($[0,\infty]$), so divergent means are $\infty$, never $0$. Theorem 7's mean is also taken in $[0,\infty]$.
• Recurrent means $f_{jj}=1$ for every state $j$; transient means $f_{jj}<1$ for every state. For irreducible chains these are complementary, which is a theorem, not a definition.
• The general Theorems 3, 4 and 5 assume irreducibility and aperiodicity, the paper's standing assumption of §1. The goal does not assume them: they follow from $k_i>0$.
• Every series in a hypothesis carries its convergence (Summable or HasSum); Theorem 3's equation (6) is written as $d_i=1+\sum_{j\ge1}p_{ij}d_j$ in $[0,\infty]$ together with finiteness of the $d_j$, $j\ne0$.
• Theorem 7's distribution is renamed $q$ in Lean to avoid a clash with $p_{ij}$. Theorem 1 of the paper (§2) and Theorem 6 are not targets of this mission.

Ruled out: $\rho$ as a real tsum (which is $0$ for a divergent series and would call a heavy-tailed chain ergodic); defining "ergodic" or "recurrent" through the existence of Lyapunov or drift functions (which would make the criteria tautological); a goal over a matrix $P$ that need not exist.

Contributions welcome: proofs of the general criteria (Theorems 2–5) on the published chain vocabulary, the limit theorem $p_{ij}^{(n)}\to\pi_j$ for irreducible aperiodic chains, first-step analysis for hitting times, and Theorem 7 as a lemma on probability generating functions; all of these are reusable beyond this mission.

Selected references

• F. G. Foster, On the stochastic matrices associated with certain queuing processes, The Annals of Mathematical Statistics 24(3), 355–360, 1953. https://doi.org/10.1214/aoms/1177728976
• D. G. Kendall, Some problems in the theory of queues, Journal of the Royal Statistical Society B 13(2), 151–185, 1951. https://doi.org/10.1111/j.2517-6161.1951.tb00093.x
• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, The Annals of Mathematical Statistics 24(3), 338–354, 1953. https://doi.org/10.1214/aoms/1177728975
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, Wiley, 1950.
• S. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, 2nd ed., Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511626630

Motivation

Temporal-difference (TD) learning estimates the value function of a Markov chain — the expected discounted sum of future rewards from each state — from a single stream of observed transitions, without knowing the transition probabilities. With a linear function approximator the value of state $x$ is represented as $\phi_x'\theta$ for a feature vector $\phi_x$ and a parameter $\theta$. Classical TD($\lambda$) updates $\theta$ by stochastic approximation, and its behaviour depends on a step-size schedule that must be tuned.

Bradtke and Barto (Machine Learning 22, 1996) replaced the stochastic-approximation update by a least-squares solve: LS TD (Eq. (11)) recomputes $\theta_t$ at every step as the instrumental-variable least-squares solution of the empirical consistency condition. The method, later generalized as LSTD($\lambda$) by Boyan (Machine Learning 49, 2002), is the basis of least-squares policy iteration and of the "LSTD" methods in standard reinforcement-learning texts (Sutton and Barto, Reinforcement Learning, 2nd ed., 2018, §9.8). Its appeal is that it has no step size; the question this mission formalizes is whether it nonetheless converges, with probability one, to the true parameter.

Timeline. Sutton (1988) introduced TD($\lambda$). Watkins and Dayan (1992) and Tsitsiklis (1994) proved probability-one convergence of tabular TD(0) and Q-learning. Bradtke and Barto (1996) proved probability-one convergence of LS TD on absorbing chains (Theorem 1) and on ergodic chains (Theorem 2). Tsitsiklis and Van Roy (IEEE TAC 42, 1997) proved convergence of linear TD($\lambda$) with general features on ergodic chains.

Setting

A finite Markov chain on a finite nonempty set $X$ is a matrix $P$ with $P(x,y)\ge0$ and $\sum_yP(x,y)=1$. A transition $x\to y$ earns reward $R(x,y)$; the expected reward out of $x$ is $\bar r_x=\sum_yP(x,y)R(x,y)$. For a discount factor $\gamma$ the value function is

$$V(x)=E\Big\{\sum_{k=0}^\infty\gamma^kr_k\ \Big|\ x_0=x\Big\}=\sum_{k=0}^\infty\gamma^k(P^k\bar r)(x).$$

The chain is ergodic (Kemeny and Snell) if every state can be reached from every state: for all $x,y$ there is $n$ with $P^n(x,y)>0$. An invariant distribution is a probability vector $\pi$ with $\pi P=\pi$; write $\Pi=\operatorname{diag}(\pi)$.

Each state has a feature vector $\phi_x\in\mathbb R^m$; $\Phi$ is the matrix with rows $\phi_x$. The true parameter $\theta^*$ is a vector with $V(x)=\phi_x'\theta^*$ for all $x$.

The algorithm (Figure 3) starts at an arbitrary state $x_0$, lets the chain move $x_0\to x_1\to\cdots$, and after $t$ transitions computes

$$\theta_t=\Big[\frac1t\sum_{k}\phi_{x_k}(\phi_{x_k}-\gamma\phi_{x_{k+1}})'\Big]^{-1}\Big[\frac1t\sum_k\phi_{x_k}R(x_k,x_{k+1})\Big],\tag{11}$$

the sums running over the $t$ transitions observed so far.

Formalization targets

Goal: Theorem 2 (p. 44)

If $P$ is ergodic, (1) $\{\phi_x\}$ is linearly independent, (2) each $\phi_x$ has dimension $|X|$, and (3) $0<\gamma<1$, then $\theta^*$ is finite and, from any initial law,

$$\theta_t\longrightarrow\theta^*\qquad\text{with probability }1 .$$

The goal leaves the chain, the rewards, the features and the initial law arbitrary.

Milestones, in the order of the proof

1. Visit frequencies (Proof of Theorem 2, p. 45): an ergodic chain visits every state infinitely often and $\#\{k<t:x_k=x\}/t\to\pi_x$ almost surely.
2. Invertibility (Proof of Theorem 2, p. 45): $\pi_x>0$ for all $x$, and $\Phi'\Pi(I-\gamma P)\Phi$ is invertible.
3. The pathwise limit (Proof of Lemma 5, pp. 54–55): along any path whose transition frequencies converge to $\pi_xP(x,y)$, $\theta_t\to[\Phi'\Pi(I-\gamma P)\Phi]^{-1}[\Phi'\Pi\bar r]$.
4. Lemma 5 (p. 43): for any chain, if almost surely every state is visited infinitely often and in proportion $\pi$, and $\Phi'\Pi(I-\gamma P)\Phi$ is invertible, then $\theta_t\to[\Phi'\Pi(I-\gamma P)\Phi]^{-1}[\Phi'\Pi\bar r]$ almost surely.
5. Eq. (12) (p. 44): the value series converges and $\bar r=(I-\gamma P)\Phi\theta^*$.

Significance

The result. Theorem 2 shows that an LS TD learner running on one long trajectory recovers the exact value function whenever the features can represent every function on the states, with no step-size schedule. It is the step-size-free counterpart of the tabular TD(0) convergence theorems and the starting point for the later analysis of LSTD with fewer features than states, where the limit is the TD fixed point $[\Phi'\Pi(I-\gamma P)\Phi]^{-1}\Phi'\Pi\bar r$ rather than $\theta^*$. Lemma 5 is the general identification of that fixed point as the almost-sure limit of LSTD.

Formalizing it. The result is proved in the paper; it has not been machine-checked. A formalization adds three things the paper delegates: the strong law of large numbers for occupation times of a finite irreducible Markov chain, which the paper cites to Kemeny and Snell and which is not in Mathlib; the per-state transition frequencies used in the first sentence of the proof of Lemma 5; and the linear algebra of the limit. The first is reusable well beyond reinforcement learning.

Difficulty

The algebra is short once the empirical averages in (11) are known to converge. The difficulty is probabilistic: the averages are over a dependent sequence, so the ordinary strong law of large numbers does not apply. Two facts are needed: that the fraction of time in each state converges to $\pi_x$ almost surely for any starting law, including periodic chains, where $P^n$ itself does not converge; and that, among the visits to $x$, the fraction followed by a move to $y$ converges to $P(x,y)$, which needs the strong Markov property at successive visit times. Neither follows from convergence of the chain's distribution, and neither holds for a chain started at a fixed state without an argument that every state is reached.

Formalization scope

• The model is a finite state type X with Fintype, DecidableEq, Nonempty, a row-stochastic matrix P : Matrix X X ℝ (structure Chain), rewards R : X → X → ℝ, features φ : X → Fin m → ℝ. Condition (2) is m = Fintype.card X; condition (1) is LinearIndependent ℝ φ.
• "Ergodic" is read as irreducible, periodic chains allowed (Kemeny–Snell's aperiodic case is "regular"). "Arbitrary initial state" is read as every initial law $\nu$, which contains every point mass.
• The path is any process $Z$ on any probability space whose finite-dimensional distributions are $\nu(x_0)P(x_0,x_1)\cdots P(x_{n-1},x_n)$, with measurable events $\{Z_t=x\}$.
• $V$ is the discounted series, never $(I-\gamma P)^{-1}\bar r$; Lean's tsum is $0$ on a divergent series, so "θ* is finite" is stated as convergence of the series together with existence of $\theta^*$ with $V=\Phi\theta^*$. $\theta^*$ is existential, never defined as Lemma 5's limit.
• (11) uses the transitions $k=0,\dots,t-1$ (the paper prints $k=1,\dots,t$ with $\phi_{t+1}$; an index shift), keeps the factors $1/t$, and uses Lean's matrix inverse, which is $0$ on a singular matrix: the paper notes $\theta_t$ is undefined for small $t$, and finitely many junk values do not affect convergence. No $\varepsilon I$ regularization, no pseudo-inverse.
• $\theta_{\rm LSTD}=\lim_t\theta_t$ is formalized as convergence of $\theta_t$ (existence of the limit is part of the claim).
• The convergence is almost sure. A formalization that assumes the visit frequencies converge in the goal, starts the chain from $\pi$, or weakens the conclusion to convergence in probability or along a subsequence is a different theorem.

Needed infrastructure: the strong law for occupation times of a finite irreducible chain under an arbitrary initial law (milestone 1), the strong Markov property at visit times, positivity of the invariant distribution of an irreducible chain, and the invertibility of $I-\gamma P$ for $|\gamma|<1$. Contributions to any of these, as standalone lemmas, are welcome.

Selected references

• S. J. Bradtke and A. G. Barto, Linear Least-Squares Algorithms for Temporal Difference Learning, Machine Learning 22, 33–57, 1996. https://doi.org/10.1023/A:1018056104778
• J. G. Kemeny and J. L. Snell, Finite Markov Chains, Springer, 1976.
• J. A. Boyan, Technical Update: Least-Squares Temporal Difference Learning, Machine Learning 49, 233–246, 2002. https://doi.org/10.1023/A:1017936530646
• J. N. Tsitsiklis and B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, IEEE Transactions on Automatic Control 42(5), 674–690, 1997. https://doi.org/10.1109/9.580874
• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018. http://incompleteideas.net/book/the-book-2nd.html

Motivation

A classifier built from a neural network produces a real score and predicts a binary label from its sign. A network can have many hidden units, so a guarantee based only on the number of parameters can be uninformative even when its output weights are small. Bartlett's 1998 paper asks whether a classifier's margin on training examples and the total magnitude of its weights can control its probability of error without fixing the number of units. Its Theorem 28 gives such a statement for two-layer networks whose activation is bounded and nondecreasing. The paper also discusses why this parameter-magnitude view supports weight decay and early stopping as learning heuristics, while leaving their algorithmic behavior outside the theorem's scope (Bartlett 1998, pp. 526, 534–535).

The theorem combines two results in the same paper. Theorem 2 turns the fat-shattering dimension of a real-valued function class into a margin generalization bound. Corollary 24 controls that dimension for finite combinations of affine-input units when the sum of the absolute combination weights is bounded. Lemmas 19, 22, and 23 supply covering estimates along that path. These are the milestones of this mission, with the source statements preserved in the milestone record (Bartlett 1998, pp. 527, 532–534).

Setting

An input is a vector $x\in\mathbb R^n$, represented in Lean as Fin n → ℝ. A label is $y\in\{-1,+1\}$; Lean's Bool is converted by pm, where true means $+1$. A probability distribution $P$ lives on labeled inputs. From an independent sample $z=((x_i,y_i))_{i=1}^m$, the empirical margin error at scale $\gamma>0$ is the fraction of indices with $y_i h(x_i)<\gamma$. The population error is the probability that $\operatorname{sgn}(h(x))\ne y$, where $\operatorname{sgn}(0)=+1$. The inequality in the empirical error is strict, as in the paper's definition (Bartlett 1998, p. 526).

Fix a bounded nondecreasing activation $\sigma:\mathbb R\to[-1,1]$. The first-layer class $F$ contains every $x\mapsto\sigma(w\cdot x+w_0)$, with an arbitrary weight vector and bias. The network class $H$ contains all finite sums $\sum_{i=1}^N\alpha_i f_i$ with $f_i\in F$ and $\sum_i|\alpha_i|\le A$. Thus $A$ bounds the output layer's total weight magnitude, while $N$ can vary without an imposed width limit. The bias $w_0$ is part of every unit. For a class $G$, $\operatorname{fat}_G(\eta)$ records the largest length of an input sequence whose every sign pattern can be realized with separation at least $\eta$ around one vector of thresholds (Bartlett 1998, pp. 526, 533–534).

Formalization targets

Two-layer generalization

For $0<\gamma\le1$, $0<\delta<1/2$, $A\ge1$, and an independent sample of length $m\ge1$, the goal is one universal $c>0$ such that, with probability at least $1-\delta$, every $h\in H$ satisfies

$$\operatorname{er}_P(h)<\widehat{\operatorname{er}}_z^\gamma(h)+ \sqrt{\frac{c}{m}\left( \frac{A^2n}{\gamma^2}\log\!\left(\frac{32A}{\gamma}\right)(\log m)^2+ \log\!\left(\frac1\delta\right)\right)}.$$

The paper prints $\log(A/\gamma)$ in this display. That term vanishes at $A=\gamma=1$, although the class can then contain halfspace classifiers with nonzero sample complexity. The proof obtains a positive factor at that corner through Corollary 24 at scale $\gamma/16$, giving $\log(32A/\gamma)$. The goal states this correction and records the printed statement separately in the moderation notes. The constant precedes all network, distribution, margin, confidence, and sample parameters in Lean; it cannot be selected after observing the instance (Bartlett 1998, pp. 533–534).

Capacity and margin milestones

Corollary 24 bounds $\operatorname{fat}_H(\eta)$ by a constant multiple of $M^2A^2n\eta^{-2}\log(MA/\eta)$ when the activation has range $[-M/2,M/2]$. Theorem 2 then converts a finite fat dimension at scale $\gamma/16$ into a simultaneous bound on population error for all members of $H$. The three covering lemmas track how shattering, pseudodimension, and an $\ell_1$ weight budget affect covers in sample $\ell_1$, $\ell_\infty$, and $\ell_2$ distances. Each bound retains the scale and explicit constants printed by the paper, subject to the stated corrections to undefined or false boundary cases (Bartlett 1998, pp. 527, 532–533).

Significance

The goal gives a width-independent generalization guarantee for a chosen network when its empirical margin error and total output weight are small. It applies to the entire class $H$ at once, so choosing a network after inspecting the sample does not turn the bound into a claim about only one fixed predictor. It does not assert that a learning algorithm finds such a network or that the displayed constants are optimal. Bartlett notes that later work had improved a logarithmic factor, and that empirical agreement with neural-network performance remained an open experimental question at the time (Bartlett 1998, pp. 534–535).

The paper proves the mathematical result. This mission asks for a machine-checked proof of its corrected formal statement and the stated supporting results; the draft theorem files currently contain proof obligations. A completed development would also make the fat dimension and strict external sample-cover definitions available for other margin analyses. Those objects differ from the platform's fixed-architecture neural networks and closed-ball covering numbers, so they are defined here with the conventions of this paper.

Difficulty

Counting hidden units gives no finite width-independent capacity bound, because $H$ permits arbitrarily many terms. Bounding each unit separately also does not control the full combination class: different small contributions can produce distinct values on a sample. The challenging step is relating covers of the base class to covers of all finite combinations under the total absolute-weight constraint, and then relating those covers back to fat-shattering. Even once a finite capacity estimate is available, the probability statement must hold simultaneously for every $h\in H$, including a network selected after sampling (Bartlett 1998, pp. 532–534).

Formalization scope

Lean uses $\mathbb N\cup\{\infty\}$ for fat dimensions and covering numbers, so an unbounded class cannot acquire a spurious dimension zero. Covers are external finite sets of real functions and use the strict distance $<\varepsilon$ of Definition 3. Sample $\ell_1$ and $\ell_2$ distances are normalized by $m$. Pseudodimension is the supremum of positive-scale fat dimensions, matching the paper's right limit. Theorems assume $m\ge1$, and sample indices are zero-based. The network class is generated from its weights rather than supplied as an arbitrary set satisfying the desired bound.

The paper says it ignores measurability issues and assumes all sets considered are measurable (Bartlett 1998, p. 526). The goal makes the event of a violating network measurable. Its individual network functions are measurable from monotonicity of $\sigma$ and finite sums; the restated Theorem 2 has explicit hypotheses for measurable class members, the violating event, and the double-sample event in its proof. Theorem 2 additionally restricts $d=\operatorname{fat}_H(\gamma/16)$ to $d\le34m$, where its printed logarithmic bound remains valid. Corollary 24 uses $n\ge1$ because a zero-dimensional input still permits a biased constant unit. Lemma 23 uses $d\ge1$ and $0<\gamma<emM/d$ in place of the printed $\gamma\ge0$: at $\gamma=0$ or $d=0$, or for $\gamma\ge emM/d$, the printed strict inequality fails, while on the rest of the printed range it is kept. These are recorded as corrections rather than attributed to the printed wording.

The deeper-network part of Theorem 28 is outside this proposal. Its printed chain through Corollary 27 has an unresolved range issue when the input box bound $B$ is smaller than the activation range, and the displayed $\log n$ factor also vanishes at $n=1$. This mission's goal is Part 1 and uses none of those claims. Contributions that establish the corrected covering lemmas, the capacity corollary, or the simultaneous margin bound fit the present proof frontier (Bartlett 1998, pp. 533–534).

Selected references

• P. L. Bartlett, The Sample Complexity of Pattern Classification with Neural Networks: The Size of the Weights is More Important than the Size of the Network, IEEE Transactions on Information Theory 44(2), 525–536, 1998. DOI.