All missions

Motivation

For a real-analytic function $f : U \to \mathbb{R}$ on an open set $U \subseteq \mathbb{R}^n$ and a critical point $a$ (so $\nabla f(a) = 0$), the Łojasiewicz gradient inequality says that there is an exponent $\theta \in [0,1)$ such that $|f - f(a)|^{\theta} / \|\nabla f\|$ stays bounded near $a$. It is the standard tool for proving that bounded gradient trajectories $\dot x = -\nabla f(x)$ have finite length and converge to a single critical point, and, in its descendants (the Kurdyka–Łojasiewicz property), for proving convergence of the whole iterate sequence of nonconvex descent methods: proximal gradient, alternating minimization, PALM, ADMM. Those algorithmic results all assume a nonsmooth version of the inequality, for functions that may take the value $+\infty$ and are not differentiable.

Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007)) supplied that nonsmooth version. This mission formalizes their first main result, Theorem 3.1: the inequality at critical points of subanalytic functions that are continuous on a closed domain.

Timeline.

• 1963: Łojasiewicz proves the inequality for real-analytic functions (Une propriété topologique des sous-ensembles analytiques réels), and in 1984 derives convergence of bounded analytic gradient trajectories.
• 1998: Kurdyka (Ann. Inst. Fourier 48) extends it to $C^1$ functions definable in an o-minimal structure, with a desingularizing function in place of the power.
• 2006: Bolte, Daniilidis and Lewis prove a nonsmooth Sard theorem (J. Math. Anal. Appl. 321): a subanalytic function continuous on its closed domain is constant on each connected component of its critical set.
• 2007: The present paper proves the nonsmooth inequality for continuous subanalytic functions (Theorem 3.1) and for lower semicontinuous convex ones (Theorem 3.3).
• 2007: Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18) extend it to lower semicontinuous functions definable in o-minimal structures (the KL property).

Setting

Write $\mathbb{R}^n$ with its Euclidean norm. A function $f : \mathbb{R}^n \to \mathbb{R} \cup \{+\infty\}$ has domain $\operatorname{dom} f = \{x : f(x) < +\infty\}$.

Subanalytic sets (Definition 2.1). A set $A \subseteq \mathbb{R}^n$ is semianalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ on which $A \cap V = \bigcup_{i=1}^{p}\bigcap_{j=1}^{q}\{x \in V : f_{ij}(x) = 0,\ g_{ij}(x) > 0\}$ with $f_{ij}, g_{ij}$ real-analytic on $V$. It is subanalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ such that $A \cap V$ is the projection onto $\mathbb{R}^n$ of a bounded semianalytic subset of $\mathbb{R}^n \times \mathbb{R}^m$, $m \ge 1$. A function $f$ is subanalytic if its graph $\{(x,\lambda) \in \mathbb{R}^n \times \mathbb{R} : f(x) = \lambda\}$ is subanalytic. Semialgebraic functions, and functions locally built from analytic ones by finitely many algebraic operations, max/min and compositions, are subanalytic.

Subdifferentials (Definition 2.10). The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y \to x,\, y \ne x} \frac{f(y) - f(x) - \langle x^*, y - x\rangle}{\|y - x\|} \ge 0$ (empty off $\operatorname{dom} f$). The limiting subdifferential $\partial f(x)$ is the set of limits of $x^*_k \in \hat\partial f(x_k)$ along $x_k \to x$ with $f(x_k) \to f(x)$.

Slope and critical points. The nonsmooth slope is $m_f(x) = \inf\{\|x^*\| : x^* \in \partial f(x)\}$, equal to $+\infty$ when $\partial f(x) = \emptyset$ (equation (4)). The critical set is $\operatorname{crit} f = \{x : 0 \in \partial f(x)\}$ (Definition 2.11).

Formalization targets

Goal: Theorem 3.1

Let $f$ be subanalytic with closed domain and $f|_{\operatorname{dom} f}$ continuous, and let $a \in \operatorname{crit} f$. Then there is $\theta \in [0,1)$ such that

$$\frac{|f - f(a)|^{\theta}}{m_f} \ \text{ is bounded around } a,$$

with the conventions $0^0 = 1$ and $\infty/\infty = 0/0 = 0$. In division-free form: there are $C$ and a neighbourhood $U$ of $a$ with $|f(x) - f(a)|^{\theta} \le C\|x^*\|$ for all $x \in U$ and $x^* \in \partial f(x)$. The exponent is existential; the goal fixes no value of $\theta$ or $C$.

Milestones

1. Remark 2.12, for $f$ continuous on a closed domain: the graph of $\partial f$ is closed; $\operatorname{crit} f$ is closed; $m_f$ is lower semicontinuous; $\operatorname{crit} f = m_f^{-1}(0)$.
2. Proposition 2.13(ii), its clause on the critical set: if $f$ is subanalytic and relatively bounded on its domain, then $\operatorname{crit} f$ is subanalytic.
3. Equation (6), recalled from the nonsmooth Sard theorem: $f$ is constant on the connected component of $\operatorname{crit} f$ containing $a$.
4. The curve selection lemma, recalled from Bierstone–Milman: a boundary point of a subanalytic set is the origin of an analytic arc entering the set.

Significance

The result. Theorem 3.1 is the nonsmooth Łojasiewicz inequality at critical points. With the subgradient in place of the gradient, it yields finite length of bounded trajectories of subgradient systems $\dot x \in -\partial f(x)$ (Section 4 of the paper) and is the template for the Kurdyka–Łojasiewicz property that underlies convergence proofs for proximal and splitting methods on nonconvex, nonsmooth problems (e.g. Attouch–Bolte–Redont–Soubeyran 2010, Bolte–Sabach–Teboulle 2014). Those papers assume the KL property and cite this line of results to know it holds for semialgebraic and subanalytic objectives.

Formalizing it. The theorem is proved; this mission produces a machine-checked proof. To our knowledge no proof assistant has a formal definition of subanalytic sets or of the nonsmooth Łojasiewicz inequality. The definitions layer (semianalytic and subanalytic sets, the slope, the inequality) is reusable by any later formalization of KL-based convergence analyses, and the milestones on Remark 2.12 are general facts about limiting subdifferentials that apply well beyond subanalytic geometry.

Difficulty

The obvious argument restricts $f$ and $m_f$ to an analytic curve and compares their Puiseux expansions. That step needs three pieces of subanalytic geometry that no library has: curve selection, the structure of one-variable subanalytic functions (monotonicity and Puiseux expansions), and the fact that the sets built in the proof (sets of points with a subgradient satisfying an inequality, level-wise infima of $m_f$) are again subanalytic, which in the paper goes through global subanalyticity and the projection theorem. The second obstacle is that $f$ is not smooth: the classical proof differentiates $f$ along a curve, while here only Fréchet subgradients are available, and the chain rule along an analytic curve holds only almost everywhere. The constancy of $f$ on critical components, equation (6), is itself a nonsmooth Sard-type theorem whose published proof uses stratification. A solver who replaces subanalytic by semialgebraic, or assumes $f$ real-valued and $C^1$, proves a different and much weaker statement.

Formalization scope

• Space and values. The space is EuclideanSpace ℝ (Fin n). The function is f : E → EReal with f x ≠ ⊥ for every x. The domain is {x | f x ≠ ⊤}; it is assumed closed, and f is assumed ContinuousOn it.
• Subdifferentials. $\hat\partial f$ and $\partial f$ are the published platform definitions NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff, which match Definition 2.10 for functions never equal to $-\infty$.
• Subanalyticity. It is defined on any finite-dimensional real normed space, so that the same definition covers $\mathbb{R}^n$, $\mathbb{R}^n \times \mathbb{R}$ and $\mathbb{R}^n \times \mathbb{R}^m$. Analyticity is AnalyticOnNhd ℝ. The boundedness of the semianalytic set in Definition 2.1(ii) is part of the definition: without it every projection of a semianalytic set would count.
• Slope. The slope is valued in $[0,+\infty]$, with $+\infty$ on points without subgradients.
• The inequality. It is the predicate LojIneqAt f a θ: one constant $C$ and one neighbourhood of $a$, quantified over all limiting subgradients. Under $0^0 = 1$ the value $\theta = 0$ never works at a critical point, as under the paper's conventions.
• Not assumed. The goal does not assume lower semicontinuity, real values, global subanalyticity, compactness of the critical set, or $f(a) = 0$. These are reductions inside the paper's proof. Any formalization that adds them, fixes $\theta$, or replaces the class of $f$ by semialgebraic or $C^1$ functions trivializes the target.
• Infrastructure. A complete proof needs: curve selection; the monotonicity lemma and Puiseux expansions for one-variable globally subanalytic functions; the projection theorem or an equivalent definability argument; the nonsmooth Sard theorem (6); and a chain rule for Fréchet subgradients along analytic curves. Each of these is welcome as a separate contribution, and the subanalytic-geometry results are reusable well beyond this mission.

Selected references

• J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17 (2007) 1205–1223. https://doi.org/10.1137/050644641
• J. Bolte, A. Daniilidis, A. Lewis, A Sard theorem for non-differentiable functions, J. Math. Anal. Appl. 321 (2006) 729–740.
• E. Bierstone, P. Milman, Semianalytic and subanalytic sets, Publ. Math. IHÉS 67 (1988) 5–42. https://doi.org/10.1007/BF02699126
• K. Kurdyka, On gradients of functions definable in o-minimal structures, Ann. Inst. Fourier 48 (1998) 769–783. https://doi.org/10.5802/aif.1638
• J. Bolte, A. Daniilidis, A. Lewis, M. Shiota, Clarke subgradients of stratifiable functions, SIAM J. Optim. 18 (2007) 556–572. https://doi.org/10.1137/060670080
• S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, in Les Équations aux Dérivées Partielles, CNRS, Paris, 1963, 87–89.
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Grundlehren 317, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Why stability bounds

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

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

Setting

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

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

$$R(A,S) = \mathbb E_z[\ell(A_S, z)], \qquad R_{\mathrm{emp}}(A,S) = \frac1m \sum_{i=1}^m \ell(A_S, z_i), \qquad R_{\mathrm{loo}}(A,S) = \frac1m \sum_{i=1}^m \ell(A_{S^{\setminus i}}, z_i).$$

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

Formalization targets

Goal: Theorem 11

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

$$R(A,S) \le R_{\mathrm{emp}}(A,S) + \sqrt{\frac{M^2 + 6Mm(\beta_1+\beta_2)}{2m\delta}}, \qquad R(A,S) \le R_{\mathrm{loo}}(A,S) + \sqrt{\frac{M^2 + 6Mm\beta_1}{2m\delta}} .$$

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

Learning from a finite sample is useful only if changing the sample has a controlled effect on the learned predictor. Uniform stability asks for a bound on the change in loss at every test point when one training example is removed. Bousquet and Elisseeff use this property to obtain generalization bounds for learning algorithms, and identify regularization as a source of stability in methods built from reproducing kernels. The present mission isolates their result for a squared norm penalty in a reproducing kernel Hilbert space (RKHS). It concerns the sensitivity of the optimizer itself, before any probability bound on a random training sample is applied. The result is Theorem 22 of Bousquet and Elisseeff (2002).

Setting

Let $X$ be an input space, $Y$ a label space, and $H$ a real reproducing kernel Hilbert space of real-valued predictors on $X$. A kernel $K:X\times X\to\mathbb R$ and a feature representative $\Phi(x)\in H$ express the reproducing identity $f(x)=\langle f,\Phi(x)\rangle_H$ and $K(x,x')=\langle\Phi(x),\Phi(x')\rangle_H$. Thus $K(x,x)=\|\Phi(x)\|_H^2$. The source assumes that all diagonal kernel values satisfy $K(x,x)\le\kappa^2$.

A labeled example is $z=(x,y)\in X\times Y$. Its loss under $f$ is $\ell(f,z)=c(f(x),y)$, where $c$ is a real-valued cost. Let $D_H$ be the set of predictions that some element of $H$ can produce at some input. The loss is $\sigma$-admissible when $c(\cdot,y)$ is convex for every label $y$ and $|c(a,y)-c(b,y)|\le\sigma|a-b|$ for all $a,b\in D_H$ and $y\in Y$. Here $\sigma$ is a nonnegative Lipschitz constant. The definition compares any two attainable predictions, even when they arise at different inputs.

Fix a sample $S=(z_1,\ldots,z_m)$, a deleted index $i$, and a regularization weight $\lambda>0$. The paper's full and truncated objectives, with squared RKHS norm regularization, are

$$R_r(g)=\frac1m\sum_{j=1}^{m}\ell(g,z_j)+\lambda\|g\|_H^2, \qquad R_r^{\setminus i}(g)=\frac1m\sum_{j\ne i}\ell(g,z_j)+\lambda\|g\|_H^2.$$

The factor in both objectives is $1/m$. Let $f$ and $f^{\setminus i}$ be minimizers of these respective objectives over all of $H$. The statements allow any minimizer satisfying the relevant global optimality condition; they do not choose one by an arbitrary fallback rule.

Formalization targets

The central target is the explicit deletion stability estimate of Theorem 22. For every test point $z\in X\times Y$,

$$|\ell(f,z)-\ell(f^{\setminus i},z)| \le \frac{\sigma^2\kappa^2}{2\lambda m}.$$

Its four milestones follow the paper's route through Lemma 20, the point-evaluation inequality (25), and the two quantitative inequalities displayed in the proof of Theorem 22. In particular, the intermediate RKHS distance bound is $\|f^{\setminus i}-f\|_H\le\kappa\sigma/(2\lambda m)$ when $\kappa\ge0$. The main theorem uses $\kappa^2$, so it does not need a choice of sign for $\kappa$. These numerical constants are part of the target, rather than placeholders for unspecified bounds.

Significance

The theorem supplies a deterministic, uniform sensitivity estimate for kernel methods trained by squared norm regularization. The bound applies simultaneously to every test example and decreases as either the sample size or the regularization weight increases. It is one of the ingredients that lets the paper apply its earlier stability-to-generalization results to concrete learning procedures. The loss need not be bounded for this theorem; bounding it is a separate question addressed later in the paper.

The result is proved in the source article. This mission asks for a machine-checked version of its exact pairwise claim and the reusable infrastructure around it: the paper's admissibility condition, the two objectives, the general regularizer inequality, and the RKHS evaluation bound. The existing Prove2Me library already has definitions for loss, empirical error, and the RKHS reproducing identity, so the new definitions concentrate on what is specific to these pages. The related replace-one estimate in Mohri, Rostamizadeh and Talwalkar's Foundations of Machine Learning uses a different perturbation and constant; it is not interchangeable with this result.

Difficulty

The two minimizers solve different objectives, and the deleted example appears in only one of them. A comparison of their objective values alone does not directly give a bound on their distance in the Hilbert norm. The source also distinguishes an abstract convex class of functions in Lemma 20 from the full RKHS used in Theorem 22. A proof must keep those domains straight while preserving the precise normalization of the truncated objective. Another delicate point is that the kernel bound controls evaluations through the reproducing identity; a bound on $K(x,x)$ is not by itself a bound on loss unless the admissibility condition is also used.

Formalization scope

The Lean model uses an abstract complete real inner product space $H$, an evaluation map $\operatorname{ev}:H\to(X\to\mathbb R)$, a feature map $\Phi:X\to H$, and the published IsRKHSOf predicate tying these to $K$. The completeness instance matches the source's Hilbert-space assumption. Samples have type Fin m → X × Y, so an index i : Fin m already forces $m\ge1$. Minimization ranges over the entire $H$ for Theorem 22 and over the declared convex class for Lemma 20. The objective definitions use the published Loss and EmpiricalError objects. No probability measure or measurability assumption is needed for these deterministic assertions.

There is a printed mismatch that affects what “deletion” means. Theorem 22 names an algorithm defined by equation (26), which, run afresh on $m-1$ points, would normalize its data term by $1/(m-1)$. Lemma 20 and the proof of Theorem 22 instead compare the full objective with equation (20), whose data term uses $1/m$. The formalized goal states that comparison, with its explicit constant, and records the discrepancy for audit. This excludes the tempting shortcut of treating the two normalizations as identical. The regularizer is the genuine squared norm and the second minimizer is required to minimize the genuine truncated objective; neither a restricted hypothesis ball nor an artificially assumed distance bound enters the goal. Contributions that establish minimizer existence or connect the pairwise bound to an algorithmic selection would extend this core without changing its statement.

Selected references

• Olivier Bousquet and André Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002), 499–526. Article and PDF.
• Mehryar Mohri, Afshin Rostamizadeh, and Ameet Talwalkar, Foundations of Machine Learning, second edition, MIT Press, 2018, Chapter 14. Book information.

Motivation

Eligibility traces are one of the basic mechanisms of reinforcement learning. A trace is a short-term memory vector $z_t$ with one component per weight. It records which components contributed to recent value estimates, so that an error observed now can be credited to the right components without storing the past. Chapter 12 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) organizes the topic around two ways of describing an algorithm. A forward view updates each state toward a target built from rewards that arrive later. A backward view makes an update at every step from the current error and the trace.

The chapter proves one exact equivalence between the two views itself, in §12.6: "This is the only equivalence of forward- and backward-views that we explicitly demonstrate in this book" (p. 301). The setting is linear Monte Carlo prediction, and the backward view uses a dutch trace. The same trace appears in true online TD($\lambda$), whose exact equivalence to the online $\lambda$-return algorithm (van Seijen and Sutton, 2014; van Seijen et al., 2016) the book cites without proof. Of that proof, §12.6 "gives some of the flavor ... but is much simpler" (p. 301).

The older equivalence of §§12.1–12.2 goes back to Sutton (1988). If the weights are held fixed during an episode, the summed updates of TD($\lambda$) with accumulating traces equal the summed updates of the off-line $\lambda$-return algorithm. The book leaves it as Exercises 12.3–12.4.

Setting

Fix a dimension $d$, a step size $\alpha$ and an episode of length $T \ge 1$ with feature vectors $x_0, \dots, x_{T-1} \in \mathbb R^d$. The episode ends with a single return $G \in \mathbb R$ ("a single reward received at the end of the episode ... and ... no discounting", p. 301). The forward view is the linear gradient Monte Carlo, or LMS, rule (12.13): from an initial $w_0$,

$$w_{t+1} = w_t + \alpha\,[G - w_t^\top x_t]\,x_t, \qquad 0 \le t < T .$$

Let $F_t = I - \alpha x_t x_t^\top$ be the fading matrix. The backward view keeps two vectors that are updated at each step in $O(d)$ time without knowledge of $G$. The dutch trace is $z_0 = x_0$, $z_t = z_{t-1} + (1 - \alpha z_{t-1}^\top x_t)\,x_t$. The auxiliary vector is $a_t = a_{t-1} - \alpha x_t x_t^\top a_{t-1}$, with $a_0 = F_0 w_0$.

For the second part, an episode $S_0, R_1, S_1, \dots, R_T, S_T$ carries states and rewards, and $\hat v(s, w)$ is a differentiable value function with $\hat v(\text{terminal}, \cdot) = 0$. For one fixed weight vector $w$, define the following, with $\gamma \in [0,1]$ and $\lambda \in [0,1)$:

• the return $G_t$;
• the $n$-step return $G_{t:t+n}$ (12.1), with $G_{t:t+n} = G_t$ once $t + n \ge T$;
• the $\lambda$-return $G^\lambda_t = (1-\lambda)\sum_{n \ge 1}\lambda^{n-1} G_{t:t+n}$ (12.2);
• the TD error $\delta_t = R_{t+1} + \gamma\hat v(S_{t+1}, w) - \hat v(S_t, w)$ (12.6);
• the accumulating trace $z_{-1} = 0$, $z_t = \gamma\lambda z_{t-1} + \nabla\hat v(S_t, w)$ (12.5).

Formalization targets

Goal: the dutch-trace equivalence (12.14), corrected

$$w_T = a_{T-1} + \alpha G\, z_{T-1}.$$

The left side is the forward view after $T$ LMS updates. On the right, $a_{T-1}$ and $z_{T-1}$ are produced by the incremental recursions above. The goal is about the two algorithms, not only about the closed-form product identity.

Milestones on the goal's path (§12.6, p. 302)

1. $w_{t+1} = F_t w_t + \alpha G x_t$.
2. $w_T = F_{T-1}\cdots F_0 w_0 + \alpha G \sum_{k=0}^{T-1} F_{T-1}\cdots F_{k+1} x_k$, the first line of (12.14).
3. $z_t = \sum_{k=0}^{t} F_t \cdots F_{k+1} x_k$ for the dutch-trace recursion.
4. $a_t = F_t \cdots F_0 w_0$ for the auxiliary-vector recursion (corrected initialization).

Milestones on the $\lambda$-return (§§12.1–12.2)

5. (12.3): $G^\lambda_t = (1-\lambda)\sum_{n=1}^{T-t-1}\lambda^{n-1}G_{t:t+n} + \lambda^{T-t-1}G_t$ for $t < T$.
6. Exercise 12.1: $G^\lambda_t = R_{t+1} + \gamma[(1-\lambda)\hat v(S_{t+1}, w) + \lambda G^\lambda_{t+1}]$.
7. Exercise 12.3: $G^\lambda_t - \hat v(S_t, w) = \sum_{k=t}^{T-1}(\gamma\lambda)^{k-t}\delta_k$.
8. Exercise 12.4: $\sum_{t<T}\alpha\delta_t z_t = \sum_{t<T}\alpha[G^\lambda_t - \hat v(S_t, w)]\nabla\hat v(S_t, w)$.

Significance

The goal says that an $O(d)$-per-step algorithm reproduces the Monte Carlo/LMS result exactly. That algorithm never stores the feature vectors or the $T$ intermediate weight vectors. The book draws the conclusion that eligibility traces "are not specific to TD learning at all" (p. 303). The dutch trace in the case $\gamma\lambda = 1$ is the same object that true online TD($\lambda$) (12.11) uses for general $\gamma\lambda$. The fading-matrix products and their incremental forms are therefore the vocabulary of any later formalization of true online TD($\lambda$) and of the online $\lambda$-return algorithm.

Exercises 12.3–12.4 are the fixed-weight equivalence of TD($\lambda$) and the off-line $\lambda$-return algorithm. They are the standard justification for calling TD($\lambda$) an approximation of the $\lambda$-return algorithm. Exercise 12.1 and (12.3) are the identities the rest of the chapter uses to manipulate $\lambda$-returns.

On status: all of these results are known and elementary on paper, and the book prints the derivation of (12.14). To our knowledge none of them has a machine-checked proof, and the platform has no statement about $\lambda$-returns, eligibility traces or TD($\lambda$). What this mission adds is formal statements with every convention fixed, including one correction to the printed text. It also adds reusable definitions of $n$-step returns, $\lambda$-returns and traces.

Difficulty

The algebra is elementary. The difficulty lies in the conventions, and a careless reading of the page produces a false statement. The book initializes $a_0 = w_0$, and taken literally that makes the goal false. The $\lambda$-return is an infinite series, whose tail collapses only because every $n$-step return that reaches past termination equals the full return. That convention has to be built into the definition of $G_{t:t+n}$, together with the terminal value $\hat v(\text{terminal}, \cdot) = 0$. Exercises 12.3 and 12.4 are true only when the weights stay fixed. With the algorithms' changing weights $w_t$ the $n$-step returns (12.1) use $w_{t+n-1}$, and neither identity holds. The boundary indices ($t = T-1$, the empty product at $k = T-1$, $G^\lambda_T = 0$) must come out right.

Formalization scope

Namespace SuttonBartoRL.Traces. Vectors of §12.6 are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and $x x^\top$ is Matrix.vecMulVec x x. The ordered product fadeProd α x j t is $F_t \cdots F_j$, the identity when $t < j$. Feature sequences are indexed by $\mathbb N$; only $x_0, \dots, x_{T-1}$ enter. $T \ge 1$ is a hypothesis wherever $T - 1$ appears. The identities of §12.6 are stated for every real $\alpha$ and $G$, a harmless strengthening of the book's positive step size.

For §§12.1–12.2, weights are EuclideanSpace ℝ (Fin d), $\nabla$ is Mathlib's gradient, and each $\hat v(s,\cdot)$ is assumed differentiable in Exercise 12.4. An episode is a length $T$, states and rewards. The value at time $t \ge T$ is $0$. (12.2) is a tsum over $n \ge 0$ of $\lambda^n G_{t:t+n+1}$, and $\lambda \in [0,1)$, the range the book gives with (12.2). Milestone 5 concludes summability, so the junk value of a divergent tsum cannot make it trivial. Exercises 12.3–12.4 take one weight binder w, used in every return, TD error and gradient. That is the book's fixed-$w$ assumption, stated in the binders.

Correction. The printed initialization $a_0 = w_0$ (p. 302) contradicts the printed definition $a_t \doteq F_t\cdots F_0 w_0$ and (12.14). The counterexample is $d = 1$, $T = 1$, $x_0 = 1$, $\alpha = 1/2$, $w_0 = 1$, $G = 0$: the forward view gives $w_1 = 1/2$, while $a_0 + \alpha G z_0 = 1$. The mission states the corrected result with $a_0 = F_0 w_0$, equivalently the same recursion started from $a_{-1} = w_0$. The printed text is kept verbatim in the milestone.

A trivializing formalization is ruled out: the goal is not the closed-form identity with $a_{T-1}$ and $z_{T-1}$ defined as the products and sums. Those vectors are defined by their $G$-free incremental recursions, and the closed forms are separate milestones.

Out of scope: the equivalence of true online TD($\lambda$) and the online $\lambda$-return algorithm (cited, p. 300), the truncated-return identity (12.10), the error bound (12.8), and all convergence claims. Proofs of the milestones, and reuse of the definitions in later missions on true online TD($\lambda$), are welcome.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 12, pp. 287–320. http://incompleteideas.net/book/the-book-2nd.html
• R. S. Sutton, "Learning to predict by the methods of temporal differences", Machine Learning 3 (1988), 9–44. https://doi.org/10.1007/BF00115009
• H. van Seijen and R. S. Sutton, "True online TD(λ)", Proceedings of ICML 2014, PMLR 32, 692–700. https://proceedings.mlr.press/v32/seijen14.html
• H. van Seijen, A. R. Mahmood, P. M. Pilarski, M. C. Machado and R. S. Sutton, "True online temporal-difference learning", Journal of Machine Learning Research 17 (2016), 1–40. https://jmlr.org/papers/v17/15-599.html

Motivation

Stochastic approximation algorithms are recursions $x_{n+1}-x_n=\gamma_{n+1}(F(x_n)+U_{n+1})$ driven by small steps $\gamma_n$ and noise $U_{n+1}$; they include the Robbins–Monro scheme, stochastic gradient methods and learning dynamics in games. The ODE method studies their long-run behaviour by comparing a time-interpolation of the iterates with the trajectories of a deterministic dynamical system. In Benaïm's lecture notes (Benaïm 1999) this comparison is formalized by the notion of an asymptotic pseudotrajectory, introduced in Benaïm and Hirsch (1996): a path that, over every window of fixed length, shadows the deterministic orbit started at its current position with an error that vanishes as time goes to infinity.

The pathwise results of the earlier sections of the notes concern algorithms whose step sizes decrease fast enough, typically $\gamma_n=o(1/\log n)$ or $\gamma_n=O(n^{-\alpha})$. When the step sizes go to zero more slowly, the limit sets of the process can no longer be characterized precisely: with steps of order $1/\log n$ the process may fail to converge even when the chain recurrent set of the ODE consists of isolated equilibria. Section 10, which is mainly based on work of Benaïm and Schreiber, describes instead the statistical behaviour of such processes in terms of the deterministic dynamics. It introduces a weaker, conditional notion, the weak asymptotic pseudotrajectory, and proves in Theorem 10.1 that the empirical distribution of the time spent by the process in different regions of the state space accumulates only on invariant measures of the deterministic dynamics. This is an ergodic-theoretic counterpart of the limit-set theorems of Section 5.

Setting

A semiflow on a metric space $(M,d)$ is a continuous map $\Phi:\mathbb R_+\times M\to M$, $(t,x)\mapsto\Phi_t(x)$, with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$ for $t,s\ge0$. Throughout, $M$ is a separable metric space with its Borel $\sigma$-algebra.

Let $(\Omega,\mathcal F,P)$ be a probability space and $\{\mathcal F_t\}_{t\ge0}$ a nondecreasing family of sub-$\sigma$-algebras. A process $X:\mathbb R_+\times\Omega\to M$ is a weak asymptotic pseudotrajectory of $\Phi$ if

1. it is progressively measurable: for every $T>0$ the restriction of $X$ to $[0,T]\times\Omega$ is measurable for the product of the Borel $\sigma$-field of $[0,T]$ and $\mathcal F_T$;
2. for each $\alpha>0$ and $T>0$, almost surely

$$\lim_{t\to\infty}P\Big\{\sup_{0\le h\le T}d\big(X(t+h),\Phi_h(X(t))\big)\ge\alpha\ \Big|\ \mathcal F_t\Big\}=0 .$$

Let $\mathcal P(M)$ be the space of Borel probability measures on $M$ with the topology of weak convergence. A measure $\mu\in\mathcal P(M)$ is $\Phi$-invariant if $(\Phi_t)_*\mu=\mu$ for every $t\ge0$; the set of invariant measures is $\mathcal M(\Phi)$. The occupation measure of the process at time $t>0$ is the random probability measure

$$\mu_t(\omega)=\frac1t\int_0^t\delta_{X(s,\omega)}\,ds ,$$

and $\mathcal M(X,\omega)\subset\mathcal P(M)$ is the set of its weak limit points as $t\to\infty$.

Formalization targets

Goal: Theorem 10.1

If $X$ is a weak asymptotic pseudotrajectory of $\Phi$, there is a set $\tilde\Omega\subset\Omega$ with $P(\tilde\Omega)=1$ such that for all $\omega\in\tilde\Omega$

$$\mathcal M(X,\omega)\subset\mathcal M(\Phi).$$

No tightness is assumed, so $\mathcal M(X,\omega)$ may be empty; the statement asserts the inclusion, not nonemptiness.

Milestones

Fix a uniformly continuous $f:M\to[0,1]$ and $T>0$, and set $U_n(f,T)=\int_{(n-1)T}^{nT}f(X(s))\,ds$ for $n\ge1$. The milestones are the numbered displays of the proof on pp. 62–63:

• Eq. (47): $\frac1n\sum_{i=1}^n[U_i(f,T)-E(U_i(f,T)\mid\mathcal F_{(i-1)T})]\to0$ almost surely (stated for every continuous $f$ with values in $[0,1]$, since the proof also applies it to $f\circ\Phi_T$);
• Eq. (50): the same with $U_{i+1}(f,T)$ conditioned on $\mathcal F_{(i-1)T}$;
• Eq. (51): $E(U_{i+1}(f,T)-U_i(f\circ\Phi_T,T)\mid\mathcal F_{(i-1)T})\to0$ almost surely;
• Eq. (52): $\frac1n\sum_{i=1}^nU_{i+1}(f,T)-\frac1n\sum_{i=1}^nU_i(f\circ\Phi_T,T)\to0$ almost surely;
• Eq. (53): for a single measurable path whose occupation measures converge weakly to $\mu$ along $t_j\to\infty$, the averages $\frac1{n_jT}\sum_{i=0}^{n_j-1}\int_{iT}^{(i+1)T}f(x_s)\,ds$ with $n_j=\lfloor t_j/T\rfloor$ converge to $\int f\,d\mu$ for every bounded continuous $f$.

Significance

The result. Theorem 10.1 locates the long-run statistics of a stochastic process that only shadows a deterministic semiflow in conditional probability. When the occupation measures are tight, for example when the path has compact closure, $\mathcal M(X,\omega)$ is nonempty, and the theorem restricts where the process spends its time to the supports of invariant measures. Right after the theorem the notes define the minimal center of attraction of the process from the supports of the measures in $\mathcal M(X,\omega)$; the conclusion applies to processes, such as slowly decreasing step-size algorithms, for which the pathwise limit-set theorem of Section 5 is not available.

Formalizing it. The theorem has a complete published proof. No machine-checked version of it, of weak asymptotic pseudotrajectories, or of occupation-measure limit theorems for continuous-time processes is known to exist. The mission produces a formal definition of progressively measurable weak asymptotic pseudotrajectories, occupation measures of measurable paths and their weak limit points, and a proof that combines a martingale law of large numbers in discrete time with weak convergence in $\mathcal P(M)$.

Difficulty

The obvious route is to apply the pathwise argument for asymptotic pseudotrajectories along each path. It fails, because condition 2 controls only conditional probabilities: the deviation events may occur infinitely often along almost every path while their conditional probabilities tend to zero. The proof therefore has to work with averages and conditional expectations instead of with individual paths: a strong law of large numbers for bounded martingale differences transfers conditional statements to time averages, and this must be done for one test function and one horizon at a time. Passing from countably many test functions to invariance requires a countable family of uniformly continuous functions that determines weak convergence on the separable space $M$, and the a.s. sets must be intersected over that family and over rational horizons. Measurability is a second difficulty: paths are not assumed continuous, so the integrals, suprema and conditional expectations involved must be shown to be well defined from progressive measurability alone.

Formalization scope

Time is $\mathbb R_{\ge0}$; the semiflow is Mathlib's Flow ℝ≥0 M; the filtration is a Filtration ℝ≥0; $\mathcal P(M)$ is ProbabilityMeasure M with its topology of weak convergence. $M$ is a separable metric space with its Borel $\sigma$-algebra; it is not assumed compact, complete or Polish. Progressive measurability is stated literally for every $T>0$. The conditional probability in condition 2 is the conditional expectation of the indicator of the deviation event, which is required to be measurable (the paper's $P\{\cdot\mid\mathcal F_t\}$ presupposes an event); the supremum over $h\in[0,T]$ is taken in $[0,\infty]$. Invariance for the semiflow is $(\Phi_t)_*\mu=\mu$ for all $t\ge0$, the form the proof establishes; for a flow it agrees with the definition $\mu(A)=\mu(\Phi_t(A))$ of Section 8.3. Weak limit points are cluster points of $t\mapsto\mu_t(\omega)$ as $t\to\infty$; the occupation measure is a genuine probability measure for every measurable path and $t>0$.

The following formalizations would trivialize the statement and are excluded by the definitions: an "occupation measure" equal to the zero measure for a non-measurable path; a conditional probability of a non-measurable event, which Lean evaluates to $0$ and which would make condition 2 vacuous; invariance defined through images $\Phi_t(A)$, which need not be Borel for a semiflow; and a compactness or Polish assumption on $M$, which the theorem does not make.

A complete development needs: Fubini-type measurability for progressively measurable processes, square-integrable martingale convergence and Kronecker's lemma (both largely in Mathlib), conditional expectations of time integrals, a convergence-determining countable family of uniformly continuous functions on a separable metric space, and the identification of weak convergence with convergence of integrals of bounded continuous functions. The martingale law of large numbers (Eqs. (47), (50)) and Eq. (53) are reusable outside this mission. Proofs of any milestone, and alternative arguments for the goal, are welcome.

Selected references

• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. Section 10, Theorem 10.1, pp. 60–63. https://doi.org/10.1007/BFb0096509
• M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617

Motivation

A stochastic approximation algorithm updates an estimate by small noisy steps, $x_{n+1}-x_n=\gamma_{n+1}(F(x_n)+U_{n+1})$, with step sizes $\gamma_n\to0$ and noise $U_n$. Such recursions underlie stochastic gradient descent, adaptive control, reinforcement learning (Q-learning, temporal-difference methods) and learning in games (fictitious play, reinforcement models). The ODE method compares the long-run behaviour of the algorithm with that of the ordinary differential equation $\dot x=F(x)$. Classical versions of this comparison (Ljung 1977, Kushner and Clark 1978) assume the ODE has a globally asymptotically stable equilibrium, or a Lyapunov function, and cannot describe algorithms whose ODE has periodic orbits, heteroclinic cycles or chaotic sets.

Benaïm and Hirsch (1996) replaced these special assumptions by a single dynamical statement: the interpolated algorithm is an asymptotic pseudotrajectory of the flow of $F$, and the limit set of every precompact asymptotic pseudotrajectory is internally chain transitive. This mission formalizes that limit set theorem as it is presented in Michel Benaïm's lecture notes Dynamics of Stochastic Approximation Algorithms (Séminaire de Probabilités XXXIII, 1999).

Timeline. Bowen (1975) and Conley (1978) introduced $(\delta,T)$-pseudo-orbits and chain recurrence, and Conley proved that the chain recurrent set of a flow on a compact space is internally chain recurrent. Benaïm (1996, SIAM J. Control Optim.) related limit sets of stochastic approximation processes to the chain recurrence of the ODE; Benaïm and Hirsch (1996) introduced asymptotic pseudotrajectories for semiflows on metric spaces and proved the limit set theorem in the form formalized here. The 1999 notes give a self-contained proof through the translation semiflow on a space of curves.

Setting

Let $(M,d)$ be a metric space. A semiflow $\Phi$ on $M$ is a continuous map $\mathbb R_+\times M\to M$, $(t,x)\mapsto\Phi_t(x)$, with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$. A set $A$ is invariant if $\Phi_t(A)=A$ for every $t\ge0$; then $\Phi|A$ denotes the restricted semiflow on $A$.

A continuous curve $X:\mathbb R_+\to M$ is an asymptotic pseudotrajectory of $\Phi$ if

$$\lim_{t\to\infty}\sup_{0\le h\le T}d\big(X(t+h),\Phi_h(X(t))\big)=0\quad\text{for every }T>0,$$

and it is precompact if $X(\mathbb R_+)$ has compact closure. Its limit set is $L(X)=\bigcap_{t\ge0}\overline{X([t,\infty))}$.

For $\delta>0$, $T>0$, a $(\delta,T)$-pseudo-orbit from $a$ to $b$ consists of $k\ge1$ partial trajectories, given by points $y_0,\dots,y_{k-1}$ (and an endpoint $y_k$) and times $t_0,\dots,t_{k-1}\ge T$ with $d(y_0,a)<\delta$, $d(\Phi_{t_j}(y_j),y_{j+1})<\delta$ for $j<k$, and $y_k=b$. One writes $a\hookrightarrow b$ if such pseudo-orbits exist for all $\delta,T>0$. A nonempty compact invariant set $\Lambda$ is internally chain transitive if $a\hookrightarrow b$ for the restricted semiflow $\Phi|\Lambda$ for all $a,b\in\Lambda$, so that all $y_i$ lie in $\Lambda$; it is internally chain recurrent if $a\hookrightarrow a$ for $\Phi|\Lambda$ for every $a\in\Lambda$. An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ such that $\operatorname{dist}(\Phi_tx,A)\to0$ uniformly in $x\in W$.

Formalization targets

Goal: Theorem 5.7 (i)

For every semiflow $\Phi$ on a metric space $M$ and every precompact asymptotic pseudotrajectory $X$ of $\Phi$,

$$L(X)\ \text{is internally chain transitive.}$$

Milestones (in the order of the proof)

• Lemma 3.1. $X$ is an asymptotic pseudotrajectory iff $d(\Theta^t(X),\hat\Phi\circ\Theta^t(X))\to0$, where $\Theta$ is the translation semiflow on $C^0(\mathbb R_+,M)$ and $\hat\Phi(Y)=\Phi^{Y(0)}$.
• Theorem 3.2. For precompact continuous $X$: $X$ is an asymptotic pseudotrajectory iff $X$ is uniformly continuous and every limit point of $\Theta^{t}(X)$, $t\to\infty$, is a trajectory of $\Phi$; and then $\{\Theta^t(X)\}_{t\ge0}$ is relatively compact.
• Lemma 5.2. A nonempty open $U$ with compact closure and $\Phi_T(\overline U)\subset U$ for some $T>0$ contains an attractor whose basin contains $\overline U$.
• Proposition 5.3. For nonempty $\Lambda$: internally chain transitive $\iff$ connected and internally chain recurrent $\iff$ compact, invariant and $\Phi|\Lambda$ has no proper attractor.
• Theorem 5.5. On a nonempty compact $M$, the chain recurrent set $R(\Phi)$ is internally chain recurrent.
• Corollary 5.6. If $\overline{\gamma^+(x)}$ is compact, then $\omega(x)$ is internally chain transitive.

Significance

The result. Theorem 5.7 (i) is the bridge between probability and dynamics in the ODE method. Once a stochastic approximation process is shown to be an asymptotic pseudotrajectory (missions 2 to 4 of this series do that under martingale-noise conditions), every statement about its limit points becomes a statement about internally chain transitive sets of the ODE: convergence to equilibria when a Lyapunov function exists (Proposition 6.4), convergence to attractors with positive probability (Theorem 7.3), and the analysis of learning dynamics in games. The theorem is sharp in the sense that every internally chain transitive set is a limit set of some asymptotic pseudotrajectory (Theorem 5.7 (ii), proved in Benaïm and Hirsch 1996 and not part of this mission).

Formalizing it. The result is proved in the literature; it is not formalized. Mathlib has semiflows (Flow), omega limit sets and the compact-open topology, but no pseudo-orbits, chain recurrence, Conley's theory of attractors, or asymptotic pseudotrajectories. This mission produces that layer for semiflows on general metric spaces, which is reusable for any later formalization of the ODE method, of Conley theory, or of learning in games.

Difficulty

The obvious approach follows $X$ from a point $a\in L(X)$ to a point $b\in L(X)$: $X$ returns near $a$ and near $b$ infinitely often, and on windows of length $T$ it is close to a trajectory, so concatenating windows gives a pseudo-orbit. The pseudo-orbit obtained this way has its points on the curve $X$, not in $L(X)$; this only shows that $L(X)$ is chain transitive for $\Phi$ on $M$, a strictly weaker property. Producing pseudo-orbits whose points lie in $L(X)$ itself is the central difficulty, and it is where precompactness of $X$ is used. Invariance $\Phi_t(L(X))=L(X)$, with equality, also needs a compactness argument, since a semiflow is not invertible.

Formalization scope

A semiflow is Mathlib's Flow ℝ≥0 M on a [MetricSpace M]; $M$ is arbitrary, with no compactness, completeness or local compactness. Time is ℝ≥0. Curves are functions ℝ≥0 → M; continuity is part of being an asymptotic pseudotrajectory, and precompactness is IsCompact (closure (Set.range X)). Invariance is equality $\Phi_t(A)=A$. Internally chain recurrent and internally chain transitive sets are nonempty by definition, and their pseudo-orbits are those of the restricted semiflow on the subtype $\Lambda$, so every point of the pseudo-orbit lies in $\Lambda$. Attractors converge uniformly on a neighbourhood. Lemma 3.1 and Theorem 3.2 are stated on $C^0(\mathbb R_+,M)$ (C(ℝ≥0, M), compact-open topology) with the half-line distance; the notes write $C^0(\mathbb R,M)$, but with the convention $\Phi^p(t)=p$ for $t<0$ that version fails for semiflows (a periodic trajectory is a counterexample), and the notes themselves describe asymptotic pseudotrajectories as points of $C^0(\mathbb R_+,M)$.

Ruled out: pseudo-orbits with no trajectory piece ($k=0$), pseudo-orbits allowed to leave $L(X)$, invariance as mere inclusion $\Phi_t(A)\subset A$, and any compactness assumption on $M$. Each of these makes the goal weaker than the theorem of the notes.

A complete development needs: elementary properties of pseudo-orbits (concatenation, continuity estimates), Arzelà–Ascoli on C(ℝ≥0, M), Conley's attractor construction, and the conjugacy between $\Phi$ and the translation semiflow on $S_\Phi$. Proofs of the milestones, alternative direct proofs of the goal (Benaïm 1996), and reusable lemmas about chain recurrence for Flow are all welcome.

Selected references

• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
• M. Benaïm, A dynamical system approach to stochastic approximations, SIAM J. Control Optim. 34 (1996), 437–472. https://doi.org/10.1137/S0363012993253534
• C. Conley, Isolated Invariant Sets and the Morse Index, CBMS Regional Conference Series in Mathematics 38, AMS, 1978. https://doi.org/10.1090/cbms/038

Motivation

A stochastic approximation algorithm is a recursion

$$x_{n+1}-x_n=\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$$

in $\mathbb R^d$, driven by a vector field $F$, decreasing step sizes $\gamma_n$ and perturbations $U_n$. Robbins–Monro root finding, stochastic gradient descent, adaptive filters, learning dynamics in games (fictitious play, reinforcement learning) and urn models all have this form. The ODE method, introduced by Ljung (1977) and developed by Kushner and Clark (1978), Métivier and Priouret (1987) and Kushner and Yin (1997), studies such a recursion by comparing it with the differential equation $\dot x=F(x)$.

Benaïm and Hirsch (1996) gave the comparison a dynamical form: the continuous-time interpolation of $\{x_n\}$ is an asymptotic pseudotrajectory of the flow of $F$. Proposition 4.1 of Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) states that deterministic comparison theorem under two assumptions: a noise condition (A1) and either bounded iterates (A2) or a Lipschitz, bounded vector field near the iterates (A2′). The notes then verify A1 almost surely for martingale noise (Propositions 4.2 and 4.4) and use the asymptotic pseudotrajectory property to describe limit sets, attractors and nonconvergence.

Setting

Let $F:\mathbb R^d\to\mathbb R^d$ be continuous. It is globally integrable if through every point there is exactly one integral curve $y:\mathbb R\to\mathbb R^d$, $\dot y=F(y)$; the flow $\Phi_t(p)$ is the value at time $t$ of the integral curve through $p$.

The step sizes satisfy $\gamma_n\ge0$, $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$. Set $\tau_0=0$, $\tau_n=\sum_{i=1}^n\gamma_i$, and $m(t)=\sup\{k\ge0:\tau_k\le t\}$. The affine interpolated process $X:\mathbb R_+\to\mathbb R^d$ and the piecewise constant processes $\overline X,\overline U,\bar\gamma$ are, for $0\le s<\gamma_{n+1}$,

$$X(\tau_n+s)=x_n+s\,\frac{x_{n+1}-x_n}{\gamma_{n+1}},\qquad \overline X(\tau_n+s)=x_n,\quad \overline U(\tau_n+s)=U_{n+1},\quad \bar\gamma(\tau_n+s)=\gamma_{n+1}.$$

The noise enters through

$$\Delta(t,T)=\sup_{0\le h\le T}\Big\|\int_t^{t+h}\overline U(s)\,ds\Big\| .$$

• A1: for every $T>0$, $\sup\{\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\|:n<k\le m(\tau_n+T)\}\to0$ as $n\to\infty$; equivalently $\Delta(t,T)\to0$ as $t\to\infty$.
• A2: $\sup_n\|x_n\|<\infty$.
• A2′: $F$ is Lipschitz and bounded on a neighbourhood of $\{x_n\}$.

A continuous $X:\mathbb R_+\to\mathbb R^d$ is an asymptotic pseudotrajectory of $\Phi$ if for every $T>0$

$$\lim_{t\to\infty}\sup_{0\le h\le T}\big\|X(t+h)-\Phi_h(X(t))\big\|=0 .$$

Formalization targets

Goal: Proposition 4.1

$$F\ \text{continuous, globally integrable},\quad \text{A1},\quad \text{A2 or A2}'\quad\Longrightarrow\quad X\ \text{is an asymptotic pseudotrajectory of}\ \Phi .$$

No rate and no constant appear; the statement holds under either alternative.

Milestones

1. Eq. (9): $X(t)-X(0)=\int_0^t[F(\overline X(s))+\overline U(s)]\,ds$.
2. A1: the discrete and the continuous forms of A1 are equivalent, for each $T>0$.
3. Theorem 3.2: for a flow on a metric space and a continuous $X$ with relatively compact image, $X$ is an asymptotic pseudotrajectory iff $X$ is uniformly continuous and every limit point of the translates $\Theta^t(X)$ in $C^0(\mathbb R,M)$ is a trajectory of the flow; both imply that $\{\Theta^t(X)\}$ is relatively compact.
4. Comparison of $X$ and $\overline X$ (p. 13): if $\|F(x_n)\|\le K$, then for $t$ large, $\sup_{t\le u\le t+T}\|X(u)-\overline X(u)\|\le2\Delta(t-1,T+1)+\sup_{t\le u\le t+T}K\bar\gamma(u)$.
5. Estimate (11): under A1 and A2′, for $t$ large,

$$\sup_{0\le h\le T}\|X(t+h)-\Phi_h(X(t))\|\le C(T)\Big[\Delta(t-1,T+1)+\sup_{t\le s\le t+T}\bar\gamma(s)\Big],$$

with $C(T)$ depending only on $T$ and on $F$ (through its Lipschitz constant and bound on the neighbourhood).

Significance

Proposition 4.1 separates the dynamics of a stochastic approximation algorithm from its noise. Any noise condition implying A1 almost surely (Propositions 4.2 and 4.4 of the notes for $L^q$-bounded and subgaussian martingale differences) combines with it to give: almost every sample path, after interpolation, is an asymptotic pseudotrajectory of $\dot x=F(x)$. The limit set theorem (Theorem 5.7: limit sets are internally chain transitive), the Lyapunov-function criterion (Proposition 6.4) and the attractor results (Section 7) then apply path by path. Estimate (11) gives the quantitative version used for rates.

The result is proved in the notes, building on Benaïm and Hirsch (1996). No machine-checked proof of it, or of the asymptotic pseudotrajectory framework, is known to exist. A formal proof would supply a checked bridge between discrete recursions with step sizes and flows of vector fields, which every ODE-method convergence proof crosses.

Difficulty

The obvious argument compares $X$ directly with the flow by Gronwall's inequality. It needs $F$ Lipschitz along both the interpolated path and the flow line, which holds under A2′ but not under A2, where $F$ is only continuous and solutions are unique without any Lipschitz bound. Under A2 the comparison must go through compactness instead: equicontinuity of the translates, identification of every limit point as an integral curve, and uniqueness of integral curves. The last step is where global integrability is used, and it cannot be replaced by a quantitative estimate.

Under A2′ the iterates may be unbounded, so no compactness is available, and the path and the flow line must be kept inside the region where $F$ is controlled for the whole window $[t,t+T]$.

Formalization scope

• Space $\mathbb R^d$ is EuclideanSpace ℝ (Fin d); time is ℝ≥0 for the pseudotrajectory and ℝ inside integrals. Sequences are ℕ → · with the paper's indices; $\gamma_0$ and $U_0$ are unused.
• $m(t)$ is the largest $k$ with $\tau_k\le t$, so the divisor $\gamma_{m(t)+1}$ is positive even when some steps vanish.
• Limits are written with $\varepsilon$; the suprema that remain ($\Delta$, $\sup\bar\gamma$) are over bounded nonempty sets, and $\overline U$ is a step function with finitely many pieces on bounded intervals, so no integral or supremum takes a default value.
• The flow of $F$ is a function satisfying the integral-curve property, together with global integrability (existence and uniqueness of integral curves on $\mathbb R$); continuity of the flow is not assumed.
• A2′ is read with a uniform neighbourhood: $F$ is Lipschitz and bounded on $\{y:\operatorname{dist}(y,\{x_n\})<r\}$ for some $r>0$. Under the reading "some open set containing $\{x_n\}$" the proposition fails for unbounded iterates.
• Theorem 3.2 is stated for flows on $C^0(\mathbb R,M)$ (compact-open topology); for semiflows with the convention $\Phi^p(t)=p$ for $t<0$, the implication (i)⇒(ii) is false as printed.

Trivializing formalizations are ruled out: the goal keeps both alternatives A2 and A2′ (neither a global Lipschitz condition nor bounded iterates is assumed in place of the disjunction), $X$ is the explicit piecewise affine interpolation rather than any curve with the desired property, and the constant in (11) is fixed before the sequences, so it cannot depend on the run.

A complete development needs Gronwall's inequality (in Mathlib), Arzelà–Ascoli on $C^0(\mathbb R,M)$, continuous dependence of solutions on initial data under uniqueness (Kamke's theorem, not in Mathlib), and interval integrals of step functions. The asymptotic pseudotrajectory definitions and Theorem 3.2 are reusable for the other missions on these notes. Proofs of individual milestones are welcome; Eq. (9) and the comparison of $X$ and $\overline X$ are the natural entry points.

Selected references

• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
• M. Métivier and P. Priouret, Théorèmes de convergence presque sûre pour une classe d'algorithmes stochastiques à pas décroissant, Probab. Theory Related Fields 74 (1987), 403–428. https://doi.org/10.1007/BF00699098
• H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997. https://doi.org/10.1007/978-1-4899-2696-8
• L. Ljung, Analysis of recursive stochastic algorithms, IEEE Trans. Automat. Control 22 (1977), 551–575. https://doi.org/10.1109/TAC.1977.1101561