Dynamical Systems

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$, where $F$ is a vector field, $\gamma_n$ are small step sizes and $U_{n+1}$ is noise. Such recursions go back to Robbins and Monro's root-finding scheme (Robbins–Monro 1951) and underlie stochastic gradient descent, temporal-difference learning, adaptive control and learning in games. The ODE method studies them by comparing the iterates with the trajectories of $\dot x=F(x)$.

Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (together with a boundedness condition on the iterates), the interpolated process is an asymptotic pseudotrajectory of the flow of $F$. A probabilistic step then verifies A1 for concrete noise models. Proposition 4.2 does this for martingale difference noise with bounded $q$-th moments, at the price of step sizes with $\sum_n\gamma_n^{1+q/2}<\infty$. This mission formalizes the second verification, Proposition 4.4: when the noise is subgaussian, A1 holds almost surely under the much weaker requirement that $\sum_ne^{-c/\gamma_n}<\infty$ for every $c>0$, which allows step sizes decaying only slightly faster than $1/\log n$. The notes attribute the result to Duflo (1997), see also Kushner and Yin (1997) and Benaïm and Hirsch (1996).

Setting

Let $\{\gamma_n\}_{n\ge1}$ be a deterministic sequence with $\gamma_n\ge0$, $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$ (a step sequence). Put $\tau_0=0$, $\tau_n=\sum_{i=1}^n\gamma_i$, and let

$$m(t)=\sup\{k\ge0:\ t\ge\tau_k\}$$

be the index of the step that contains time $t\ge0$. For a sequence $\{U_n\}_{n\ge1}$ define the piecewise constant processes $\bar U(t)=U_{m(t)+1}$ and $\bar\gamma(t)=\gamma_{m(t)+1}$, so that step $n+1$ occupies the time interval $[\tau_n,\tau_{n+1})$ of length $\gamma_{n+1}$.

Assumption A1 asks that for every $T>0$

$$\lim_{n\to\infty}\sup\Big\{\Big\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\|:\ k=n+1,\dots,m(\tau_n+T)\Big\}=0,$$

or, in the form the notes call equivalent, $\lim_{t\to\infty}\Delta(t,T)=0$ for every $T>0$, where

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

Let $(\Omega,\mathcal F,P)$ be a probability space with a nondecreasing sequence $\{\mathcal F_n\}$ of sub-$\sigma$-algebras, and $F:\mathbb R^d\to\mathbb R^d$ continuous. A sequence $\{x_n\}$ given by the recursion above is a Robbins–Monro algorithm if $\gamma$ is deterministic, $U_n$ is $\mathcal F_n$-measurable, and $E(U_{n+1}\mid\mathcal F_n)=0$. The noise is subgaussian if there is a number $\Gamma>0$ such that for all $n$ and all $\theta\in\mathbb R^d$

$$E\big(\exp\langle\theta,U_{n+1}\rangle\,\big|\,\mathcal F_n\big)\le\exp\Big(\frac\Gamma2\|\theta\|^2\Big).$$

Bounded noise, $\|U_n\|\le\sqrt\Gamma$, is an example.

Formalization targets

Goal: Proposition 4.4

For a Robbins–Monro algorithm with subgaussian noise and a deterministic step sequence such that

$$\sum_ne^{-c/\gamma_n}<\infty\qquad\text{for each }c>0,$$

with probability one the realised noise sequence satisfies A1, in both of its forms, simultaneously for all $T>0$.

Milestones

1. The exponential supermartingale. For every $\theta\in\mathbb R^d$,

$$Z_n(\theta)=\exp\Big[\sum_{i=1}^n\langle\theta,\gamma_iU_i\rangle-\frac\Gamma2\sum_{i=1}^n\gamma_i^2\|\theta\|^2\Big]$$

is a supermartingale. 2. Directional maximal tail bound. For every unit vector $e$, $\alpha>0$, $n$ and $T>0$,

$$P\Big(\sup_{n<k\le m(\tau_n+T)}\Big\langle e,\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\rangle\ge\alpha\Big)\le\exp\Big(\frac{-\alpha^2}{2\Gamma\sum_{i=n}^{m(\tau_n+T)-1}\gamma_{i+1}^2}\Big).$$

3. Eq. (18). There are $C,C'>0$ depending only on $d$ and $\Gamma$ with

$$P(\Delta(t,T)\ge\alpha)\le C\exp\Big(\frac{-\alpha^2}{C'\int_t^{t+T}\bar\gamma(s)\,ds}\Big)\qquad(t\ge0,\ T>0,\ \alpha>0).$$

4. Block comparison. $\Delta(t,T)\le2\Delta(kT,T)+\Delta((k+1)T,T)$ for $kT\le t<(k+1)T$.

Significance

Proposition 4.4 is the sufficient condition for the ODE method when the noise has Gaussian-type tails. Its step-size condition holds whenever $\gamma_n\log n\to0$, so it admits steps that decrease far more slowly than the $\sum\gamma_n^2<\infty$ of the classical $L^2$ theory; slowly decreasing steps are what practitioners use to keep algorithms responsive. Combined with Proposition 4.1 it shows that the interpolated process of such an algorithm, with bounded iterates, is almost surely an asymptotic pseudotrajectory of the flow of $F$, and the limit set theorems of the notes then locate the limit points of the algorithm.

The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would add reusable pieces: an exponential supermartingale and maximal inequality for vector-valued martingale differences with a conditional subgaussian bound (Mathlib's conditional subgaussian notion is scalar), a Borel–Cantelli argument along the grid $kT$, and the continuous-time bookkeeping of $\bar U$, $\bar\gamma$ and $\Delta$ shared with the other missions of this series.

Difficulty

The moment method of Proposition 4.2 does not reach this regime: any fixed polynomial moment of the window sums decays only polynomially in the window's step sizes, and under $\sum e^{-c/\gamma_n}<\infty$ alone polynomial bounds are not summable over windows. Exponential tail bounds are needed, and they must be maximal (uniform over the window) and must hold for the norm of a vector, not only for a scalar. The continuous-time deviation $\Delta(t,T)$ involves partial steps at both ends of $[t,t+h]$, so the bound must be stated in terms of $\int_t^{t+T}\bar\gamma$ rather than a sum over whole steps, with constants that do not depend on $t$, $T$ or $\alpha$. Finally, A1 quantifies over all $T>0$: the almost-sure statement must hold on a single event of full probability for every $T$.

Formalization scope

The space is $\mathbb R^d$ as EuclideanSpace ℝ (Fin d) (the paper writes $\mathbb R^m$); time is real. The sequences $\gamma$ and $U$ are indexed by $\mathbb N$, and their values at $0$ are unused, as the paper indexes them from $1$. The filtration is a Mathlib Filtration ℕ; $U_{n+1}$ is $\mathcal F_{n+1}$-strongly measurable and integrable, and $E(U_{n+1}\mid\mathcal F_n)=0$ almost surely. The subgaussian condition requires $\exp\langle\theta,U_{n+1}\rangle$ to be integrable for every $\theta$ and $n$. The summand $e^{-c/\gamma_n}$ is taken to be $0$ when $\gamma_n=0$, its limiting value. The suprema in A1 and $\Delta$ are taken in $[0,\infty]$; the supremum over an empty range of $k$ is $0$. In Eq. (18) the constants are chosen before the probability space, the algorithm and $t,T,\alpha$.

The following readings are excluded and are not acceptable formalizations: a subgaussian condition that holds vacuously because the exponential is not integrable (Lean's conditional expectation of a non-integrable function is $0$); a summability condition made trivial or false by the convention $c/0=0$; and the conclusion "for each $T$, A1 holds almost surely" in place of "almost surely, A1 holds for all $T$". The second sentence of Proposition 4.4 (the asymptotic pseudotrajectory conclusion) is outside this mission.

All hypotheses are satisfiable: $U=0$, $x=0$, $F=0$, $\Gamma=1$ and $\gamma_n=1/n$ satisfy every one of them.

Contributions welcome: a maximal inequality for nonnegative supermartingales in the form needed here, vector subgaussian tail bounds for martingale transforms with deterministic weights (reusable well beyond this mission), lemmas on the step processes and $\Delta$ (measurability, local integrability, additivity), and the proofs of the milestones.

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. https://doi.org/10.1007/BFb0096509
• M. Duflo, Random Iterative Models, Applications of Mathematics 34, Springer, 1997.
• H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997.
• 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
• H. Robbins and S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586

Motivation

A stochastic approximation algorithm is a recursion $x_{n+1}=x_n+\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$ with decreasing step sizes $\gamma_n$ and a noise term $U_{n+1}$. Recursions of this form appear in stochastic gradient methods, adaptive control, learning in games (fictitious play, reinforcement learning) and urn models. The ODE method compares the iterates with the solutions of $\dot x=F(x)$. In Benaïm's lecture notes (Benaïm 1999), the comparison is phrased through the continuous-time interpolated process $X$. Under standard noise conditions, $X$ is almost surely an asymptotic pseudotrajectory of the flow of $F$, and its limit set is almost surely internally chain transitive.

That theorem constrains where the process may end up. It does not say which of several candidate sets the process actually reaches. When the ODE has several attractors, for example several stable equilibria of a learning dynamic or several stable compositions of an urn, an application needs to know that each attractor is reached with positive probability. Section 7 of the notes answers this question. The answer is a criterion of attainability: if the process can, with positive probability and at arbitrarily late times, enter the basin of an attractor, then it converges to that attractor with positive probability.

Timeline.

• Kushner and Clark (1978) proved convergence statements for processes that visit a compact subset of the domain of attraction of an asymptotically stable equilibrium infinitely often.
• Arthur, Ermoliev and Kaniovski (1983) and Pemantle (1990) studied urn processes whose limit points depend on the trajectory.
• Benaïm (1997) and Duflo (1997, Random Iterative Models) developed the attainability argument for general stochastic approximation processes.
• Benaïm (1999) states it for arbitrary attractors of a semiflow on a locally compact metric space, under a single conditional shadowing condition (24).

Setting

Let $(M,d)$ be a metric space and let $\Phi=(\Phi_t)_{t\ge0}$ be a semiflow on $M$: a continuous map $(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 all $t\ge0$, and positively invariant if $\Phi_t(A)\subset A$.
• An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ on which $\operatorname{dist}(\Phi_tx,A)\to0$ uniformly. Its basin $B(A)$ is the set of points $x$ with $\operatorname{dist}(\Phi_tx,A)\to0$.
• A continuous curve $X:\mathbb R_+\to M$ is an asymptotic pseudotrajectory if $\sup_{0\le h\le T}d(X(t+h),\Phi_h(X(t)))\to0$ as $t\to\infty$, for every $T>0$.
• The limit set of $X$ is $L(X)=\bigcap_{t\ge0}\overline{X([t,\infty))}$.
• For $T>0$, $d_X(T)=\sup_{k\in\mathbb N}d(\Phi_T(X(kT)),X(kT+T))$.

Now let $X=(X(t))_{t\ge0}$ be a process on a probability space $(\Omega,\mathcal F,P)$ with continuous paths in $M$, adapted to a filtration $(\mathcal F_t)_{t\ge0}$. The standing assumption of Section 7 is that for all $\delta>0$, $T>0$ and $t\ge0$,

$$P\Big(\sup_{s\ge t}\ \sup_{0\le h\le T}d\big(X(s+h),\Phi_h(X(s))\big)\ge\delta\ \Big|\ \mathcal F_t\Big)\le w(t,\delta,T)\tag{24}$$

for a function $w\ge0$ with $w(t,\delta,T)\downarrow0$ as $t\to\infty$.

A point $p$ is attainable if $P(\exists s\ge t: X(s)\in U)>0$ for every $t>0$ and every open neighbourhood $U$ of $p$. $\mathrm{Att}(X)$ is the set of attainable points.

Formalization targets

Goal: Theorem 7.3, first statement

If $M$ is locally compact, $A$ is an attractor of $\Phi$, and $\mathrm{Att}(X)\cap B(A)\neq\emptyset$, then

$$P\big(L(X)\subset A\big)>0 .$$

This statement contains no constants and no rates, so it does not depend on how (24) is quantified for a particular algorithm.

Theorem 7.3, second statement

If $U$ is open and relatively compact with $\overline U\subset B(A)$, there are $T,\delta>0$, depending only on $U$ (and on $\Phi$, $A$), such that for every process satisfying the standing assumption and every $t\ge0$

$$P\big(L(X)\subset A\big)\ge\big(1-w(t,\delta,T)\big)\,P\big(\exists s\ge t:\ X(s)\in U\big).$$

Milestones

• Lemma 6.8. For a nonempty compact $K\subset B(A)$ there are $T,\delta>0$ such that every asymptotic pseudotrajectory with $X(0)\in K$ and $d_X(T)<\delta$ has $L(X)\subset A$.
• Lemma 7.1, in three parts:
  • $\mathrm{Att}(X)$ is closed;
  • it is positively invariant;
  • it contains $L(X)$ almost surely.

Significance

The result. Theorem 7.3 turns a question about the long-run limit of a random process into a question about where the process can go. Attainability is usually checked by a controllability argument: the noise can push the iterates in every direction. For urn processes with an urn function mapping the simplex into its interior, every point is attainable (Example 7.2 of the notes). Then every attractor of the mean ODE is reached with positive probability. Combined with nonconvergence results for unstable sets (Section 9 of the notes), this characterizes the possible limits of many learning and urn processes. Theorem 7.3 is the positive half of that picture.

Formalizing it. The theorem has a published proof (p. 32 of the notes) and no machine-checked version. A formal proof needs the following:

• a precise reading of the conditional shadowing condition (24) as a conditional expectation of an indicator;
• the stopping-time decomposition of the event $\{\exists s\ge t: X(s)\in U\}$ over dyadic times;
• the deterministic Lemma 6.8, which rests on the limit set theorem for precompact asymptotic pseudotrajectories (Theorem 5.7 of the notes, the subject of mission 1 of this series).

Difficulty

The obvious argument says: once $X$ enters a compact part of the basin, the flow carries it into $A$. That fails because $X$ is not a trajectory of the flow. Each window of length $T$ adds an error, and errors over infinitely many windows can push the process out of the basin.

Two things are needed instead:

• A uniform version of the deterministic statement, with $T$ and $\delta$ fixed in advance from the compact set alone. This is Lemma 6.8, which needs local compactness of $M$ and the structure of limit sets of asymptotic pseudotrajectories.
• A probabilistic step that applies (24) at the random time when $X$ first enters $U$. That time is not a stopping time on a continuum, and conditioning at it needs care.

A naive union bound over all times is useless: it does not use the conditional form of (24).

Formalization scope

• The semiflow is Mathlib's Flow ℝ≥0 M on a metric space; local compactness is LocallyCompactSpace M.
• The process is X : ℝ≥0 → Ω → M with continuous paths. The paper's alternative of càdlàg paths is not covered.
• Adaptedness is Borel measurability of $X(t)$ with respect to $\mathcal F_t$, for a Mathlib Filtration ℝ≥0. $P$ is a probability measure.
• The suprema in (24) and in $d_X(T)$ are computed in $[0,\infty]$ with the extended distance, so that "sup $\ge\delta$" and "sup $<\delta$" are exact even when the supremum is infinite or not attained.
• The conditional probability in (24) is the conditional expectation of the indicator of the event. The event is required to be measurable, so the condition cannot hold vacuously through a junk conditional expectation.
• $w$ is required to be both nonincreasing in $t$ and convergent to $0$.
• The events $\{L(X)\subset A\}$ and $\{\exists s\ge t: X(s)\in U\}$ are measured with $P$ as an outer measure, so no measurability hypothesis is added for them.
• In the second statement of Theorem 7.3, $T$ and $\delta$ are chosen before the probability space, the process, $w$ and $t$.
• Invariance in the definition of an attractor is the equality $\Phi_t(A)=A$, not inclusion.
• The almost-sure clause of Lemma 7.1 is stated for separable $M$. Without separability it cannot be proved in ordinary set theory.

These choices rule out the trivializing formalizations: a conditional-probability hypothesis that holds vacuously, invariance read as inclusion, constants $T,\delta$ that depend on the process or on $t$, and a probability bound $w$ without monotonicity.

A complete development needs:

• limit sets of asymptotic pseudotrajectories and the fact that an internally chain transitive set meeting the basin of an attractor lies in the attractor (shared with missions 1 and 5 of this series);
• measurability of path functionals of continuous processes;
• conditioning on events of the form $\{\tau=t_n(k)\}$ at dyadic times.

The first and second are reusable well beyond this mission. Contributions toward either, and alternative proofs of Lemma 6.8, 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. https://doi.org/10.1007/BFb0096509
• M. Benaïm, 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
• M. Benaïm, Vertex-reinforced random walks and a conjecture of Pemantle, Annals of Probability 25 (1997), 361–392. https://doi.org/10.1214/aop/1024404292
• M. Duflo, Random Iterative Models, Applications of Mathematics 34, Springer, 1997. https://doi.org/10.1007/978-3-662-12880-0
• H. J. Kushner, D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8
• 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$, where $F$ is a vector field, $\gamma_n$ are small step sizes and $U_{n+1}$ is noise. Such recursions go back to Robbins and Monro's root-finding scheme (Robbins–Monro 1951) and underlie stochastic gradient descent, temporal-difference learning, adaptive control and learning in games. The ODE method studies them by comparing the iterates with the trajectories of $\dot x=F(x)$.

Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (and the iterates are bounded, or $F$ is Lipschitz and bounded on a neighbourhood of them), the interpolated process is an asymptotic pseudotrajectory of the flow of $F$. A probabilistic step then verifies A1 for concrete noise models. This mission formalizes the first such verification, Proposition 4.2: martingale difference noise with bounded $q$-th moments and step sizes with $\sum_n\gamma_n^{1+q/2}<\infty$. The result is described as a particular case of a general theorem of Métivier and Priouret (1987); the same estimates reappear later in the notes.

Setting

Let $\{\gamma_n\}_{n\ge1}$ be a deterministic sequence with $\gamma_n\ge0$, $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$ (a step sequence). Put $\tau_0=0$, $\tau_n=\sum_{i=1}^n\gamma_i$, and let

$$m(t)=\sup\{k\ge0:\ t\ge\tau_k\}$$

be the index of the step that contains time $t\ge0$. For a sequence $\{U_n\}_{n\ge1}$ define the piecewise constant processes $\bar U(t)=U_{m(t)+1}$ and $\bar\gamma(t)=\gamma_{m(t)+1}$, so that step $n+1$ occupies the time interval $[\tau_n,\tau_{n+1})$ of length $\gamma_{n+1}$.

Assumption A1 asks that for every $T>0$

$$\lim_{n\to\infty}\sup\Big\{\Big\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\|:\ k=n+1,\dots,m(\tau_n+T)\Big\}=0,$$

or, in the form the notes call equivalent, $\lim_{t\to\infty}\Delta(t,T)=0$ for every $T>0$, where

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

Let $(\Omega,\mathcal F,P)$ be a probability space with a nondecreasing sequence $\{\mathcal F_n\}$ of sub-$\sigma$-algebras, and $F:\mathbb R^d\to\mathbb R^d$ continuous. A sequence $\{x_n\}$ given by the recursion above is a Robbins–Monro algorithm if $\gamma$ is deterministic, $U_n$ is $\mathcal F_n$-measurable, and $E(U_{n+1}\mid\mathcal F_n)=0$.

Formalization targets

Goal: Proposition 4.2

For a Robbins–Monro algorithm and some real $q\ge2$, if

$$\sup_nE\big(\|U_{n+1}\|^q\big)<\infty\qquad\text{and}\qquad\sum_n\gamma_n^{1+q/2}<\infty,$$

then with probability one the realised noise sequence satisfies A1, in both of its forms, simultaneously for all $T>0$.

Milestones

1. Eq. (13), an instance of Burkholder's inequality with a universal constant $C_q$:

$$E\Big\{\sup_{n<k\le m(\tau_n+T)}\Big\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\|^q\Big\}\le C_q\,E\Big\{\Big[\sum_{i=n}^{m(\tau_n+T)-1}\gamma_{i+1}^2\|U_{i+1}\|^2\Big]^{q/2}\Big\}.$$

2. Inequality (14), for finite families with $\alpha_i\ge0$, $u>1$, $0<\delta<1$:

$$\Big(\sum_i|\alpha_i\beta_i|\Big)^u\le\Big(\sum_i\alpha_i^{\delta u/(u-1)}\Big)^{u-1}\sum_i\alpha_i^{(1-\delta)u}|\beta_i|^u.$$

3. Eq. (16): for every $T>0$ there is $C(q,T)$ with $E(\Delta(t,T)^q)\le C(q,T)\int_t^{t+T}\bar\gamma^{q/2}(s)\,ds$ for all $t\ge0$.
4. Eq. (17): $\sum_{k\ge0}E(\Delta(kT,T)^q)<\infty$ for every $T>0$.
5. Block comparison: $\Delta(t,T)\le2\Delta(kT,T)+\Delta((k+1)T,T)$ for $kT\le t<(k+1)T$.

Significance

Proposition 4.2 is the standard sufficient condition under which the ODE method applies to stochastic gradient-type recursions with martingale noise. With $q=2$ it covers step sizes with $\sum\gamma_n^2<\infty$ (for example $\gamma_n=1/n$) and noise with bounded variance; larger $q$ trades stronger moment assumptions for slower decay of the steps, down to $\sum\gamma_n^{1+q/2}<\infty$. Combined with Proposition 4.1 it shows that the interpolated process of a Robbins–Monro algorithm with bounded iterates is almost surely an asymptotic pseudotrajectory of the flow of $F$; the limit set theorems of the notes then locate the limit points of the algorithm.

The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would supply reusable pieces that Mathlib currently lacks, most notably a Burkholder (or Burkholder–Davis–Gundy) inequality for discrete-time vector martingales in $L^q$, and the continuous-time bookkeeping of the step processes $\bar U$, $\bar\gamma$ and the noise deviation $\Delta$, shared by the other missions of this series.

Difficulty

The obvious argument controls each window by Doob's $L^2$ maximal inequality and sums over windows. That works for $q=2$ only. For $q>2$ the second moment of the window sums is not summable under $\sum\gamma_n^{1+q/2}<\infty$, and one needs an $L^q$ maximal inequality whose right-hand side is the $q/2$-th moment of the square function. That inequality, Burkholder's, is not in Mathlib. Converting the square function into the moment bound requires a Hölder-type inequality with tuned exponents, and passing from the discrete sums to $\Delta(t,T)$ requires handling partial steps at both ends of $[t,t+h]$. A second subtlety is that A1 quantifies over all $T>0$: the almost-sure statement must hold on a single event of full probability for every $T$, not on an event that depends on $T$.

Formalization scope

The space is $\mathbb R^d$ as EuclideanSpace ℝ (Fin d); time is real; $q$ is a real number with $q\ge2$, and all powers are real powers of nonnegative quantities. The sequences $\gamma$ and $U$ are indexed by $\mathbb N$, and their values at $0$ are unused, as the paper indexes them from $1$. The filtration is a Mathlib Filtration ℕ, $U_{n+1}$ is required to be $\mathcal F_{n+1}$-strongly measurable and integrable, and the martingale difference condition is $E(U_{n+1}\mid\mathcal F_n)=0$ almost surely. Expectations of nonnegative quantities, the suprema in A1 and $\Delta$, and the moment bound are taken in $[0,\infty]$, so no default value of a non-integrable expectation or of an empty supremum can make a statement hold vacuously; the supremum over an empty range of $k$ is $0$.

The following readings are excluded and are not acceptable formalizations: a moment hypothesis that holds vacuously, a conditional expectation hypothesis on non-integrable noise, the conclusion "for each $T$, A1 holds almost surely" in place of "almost surely, A1 holds for all $T$", and $q$ fixed to $2$ or restricted to integers.

All hypotheses are satisfiable: $U=0$, $x=0$, $F=0$ and $\gamma_n=1/n$ with $q=2$ satisfy every one of them.

Contributions welcome: a general Burkholder inequality for discrete-time martingales in finite-dimensional spaces (reusable well beyond this mission), lemmas on the step processes and $\Delta$ (measurability, local integrability, additivity), and the proofs of the milestones.

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. 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
• M. Métivier and P. Priouret, Théorèmes de convergence presque sûre pour une classe d'algorithmes stochastiques à pas décroissant, Probability Theory and Related Fields 74 (1987), 403–428.
• D. L. Burkholder, Distribution function inequalities for martingales, Annals of Probability 1 (1973), 19–42. https://doi.org/10.1214/aop/1176997023
• D. W. Stroock, Probability Theory: An Analytic View, Cambridge University Press, 1993.
• H. Robbins and S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586
• H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997.

Motivation

A stochastic approximation algorithm is a recursion $x_{n+1}=x_n+\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$ with decreasing steps $\gamma_n$ and noise $U_n$. Stochastic gradient descent, the Robbins–Monro procedure, reinforcement-learning updates and learning dynamics in games all have this form. The ODE method compares such a recursion with the deterministic dynamics $\dot x=F(x)$. Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) do this in two steps. First, the limit set of the interpolated process is internally chain transitive for the semiflow of $F$ (Theorem 5.7, the subject of mission 1 of this series). Second, internally chain transitive sets are located using properties of the dynamics alone.

The most common tool in the second step is a Lyapounov function: a function that decreases strictly along every trajectory outside a set $\Lambda$ and is constant on $\Lambda$. Proposition 6.4 of the notes states exactly when such a function forces every internally chain transitive set into $\Lambda$. It is the step behind the convergence of stochastic gradient algorithms to critical points (Corollary 6.7) and behind convergence results for learning in potential games.

Timeline.

• Conley (Isolated Invariant Sets and the Morse Index, CBMS 38, 1978) introduced chain recurrence and the attractor–repeller description of it.
• Benaïm and Hirsch (J. Dyn. Diff. Eq. 8, 1996) identified limit sets of asymptotic pseudotrajectories with internally chain transitive sets.
• Benaïm (SIAM J. Control Optim. 34, 1996) developed the dynamical-systems approach to stochastic approximation built on these notions.
• Bowen (J. Differential Equations 18, 1975) characterized chain transitivity by the absence of proper attractors, the content of Proposition 5.3 of the notes.
• The 1999 notes state the Lyapounov criterion in the form used here, for semiflows on arbitrary metric spaces.

Setting

Let $(M,d)$ be a metric space, with no compactness or completeness assumed. 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$. For an invariant $\Lambda$, the restriction $\Phi|\Lambda$ is the semiflow $\Phi$ acting on $\Lambda$.
• For $\delta,T>0$, a $(\delta,T)$-pseudo-orbit from $a$ to $b$ is a list of points $y_0,\dots,y_k$ ($k\ge1$) 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$.
• A set $L$ is internally chain transitive if it is nonempty, compact and invariant, and for all $a,b\in L$ and all $\delta,T>0$ there is a $(\delta,T)$-pseudo-orbit of $\Phi|L$, so with every $y_i\in L$, from $a$ to $b$.
• An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ on which $\mathrm{dist}(\Phi_t x,A)\to0$ uniformly. Its basin is the set of points $x$ with $\mathrm{dist}(\Phi_t x,A)\to0$.
• Let $\Lambda\subset M$ be compact and invariant. A continuous $V:M\to\mathbb R$ is a Lyapounov function for $\Lambda$ if $t\mapsto V(\Phi_t(x))$ is constant for $x\in\Lambda$ and strictly decreasing for $x\notin\Lambda$.

Formalization targets

Goal: Proposition 6.4

Let $\Lambda$ be compact invariant and $V$ a Lyapounov function for $\Lambda$, and assume that $V(\Lambda)$ has empty interior in $\mathbb R$. Then for every internally chain transitive set $L$,

$$L\subset\Lambda\qquad\text{and}\qquad V|_L\ \text{is constant}.$$

Milestones

1. Lemma 5.2. If $U$ is open with compact closure and $\Phi_T(\overline U)\subset U$ for some $T>0$, there is an attractor $A\subset U$ whose basin contains $\overline U$.
2. 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.
3. The claim of the proof of 6.4. For $L$ internally chain transitive and $v^*=\inf_L V$: $L\cap\Lambda\ne\emptyset$ and $v^*=\inf_{L\cap\Lambda}V$.
4. The sublevel step of the proof of 6.4. For every $c>v^*$ with $c\notin V(\Lambda)$, $V<c$ on all of $L$.

Significance

The result. Proposition 6.4 converts a statement about real numbers, that $V(\Lambda)$ has empty interior, into a statement about dynamics: the chain recurrent behaviour of $\Phi$ is confined to $\Lambda$. With Theorem 5.7 it gives the following. If $\Phi$ has such a Lyapounov function, then the limit set of any precompact asymptotic pseudotrajectory, in particular of a bounded stochastic approximation process, lies in $\Lambda$, and $V$ is constant on it. When $\Lambda$ is the set of equilibria and $V(\Lambda)$ is Lebesgue-null by Sard's theorem, this is the convergence of stochastic gradient algorithms to connected sets of critical points (Corollary 6.7). Remark 6.5 gives a flow on the circle with a strict Lyapounov function, where the circle itself is internally chain transitive. So the empty-interior hypothesis cannot be removed.

Formalizing it. The result is proved, in the notes and in the earlier literature. No machine-checked version of chain recurrence for semiflows on metric spaces, Conley's attractor lemma, or Bowen's characterization of chain transitive sets is known to us. The mission therefore adds the following:

• a formal definition layer for these notions on Mathlib's Flow;
• formal proofs of Lemma 5.2 and Proposition 5.3, which are reused across this series (missions 1 and 6);
• the Lyapounov criterion itself.

Difficulty

The obvious argument does not work. It runs: $V$ decreases along trajectories, so along an orbit in $L$ the value of $V$ must settle on $\Lambda$. But points of an internally chain transitive set are joined only by pseudo-orbits. At each of the $k$ jumps, $V$ may increase by an amount that is small but not controlled in number, so monotonicity of $V$ along true trajectories says nothing directly about $L$. Remark 6.5 shows that the conclusion is genuinely false without a condition on $V(\Lambda)$. The difficulty is therefore global: pseudo-orbits that climb back up $V$ through many small jumps must be excluded using information about the restricted semiflow $\Phi|L$ as a whole, not the monotonicity of $V$ along single trajectories. Milestones 1 and 2 are the general facts about chain transitive sets that this requires, and their own proofs involve compactness and uniform-continuity estimates over arbitrarily long pseudo-orbits.

Formalization scope

• Representation. $M$ is any MetricSpace, and the semiflow is Flow ℝ≥0 M.
• Invariance is equality $\Phi_t(A)=A$ for every $t$, not inclusion.
• Pseudo-orbits have at least one trajectory piece ($k\ge1$), times $\ge T$, an exact endpoint, and, in the internal notions, all their points in the set.
• Nonemptiness. Internally chain transitive and internally chain recurrent sets are nonempty by definition. Accordingly, Proposition 5.3 assumes $\Lambda\neq\emptyset$ and Lemma 5.2 assumes $U\neq\emptyset$.
• Lyapounov function. The predicate contains the standing assumptions of its definition: $\Lambda$ is compact and invariant, $V$ is continuous, $V(\Phi_t x)=V(x)$ on $\Lambda$, and $t\mapsto V(\Phi_t x)$ is strictly antitone off $\Lambda$.
• Empty interior is interior (V '' Λ) = ∅ in $\mathbb R$, not countability, finiteness or measure zero.
• Infima are stated with IsGLB, not a real sInf.

The following formalizations are trivializing and are excluded:

• chains with no jumps, under which every point is chain recurrent;
• invariance as inclusion;
• a non-strict decrease condition, under which constant functions are Lyapounov functions and the goal is false;
• chains of $\Phi$ that leave $L$, a strictly weaker notion;
• quantifying only over limit sets instead of every internally chain transitive set.

A complete development needs elementary facts about ω-limit sets of points of a compact invariant set: they are nonempty, compact and invariant. It also needs the attractor construction $A=\bigcap_{t\ge0}\overline{\bigcup_{s\ge t}\Phi_s(U)}$ and the open sets $\{y: x\hookrightarrow_{\delta,T}y\}$ used in Proposition 5.3. These are reusable for any work on Conley theory. Contributions of any of these lemmas, or of proofs of the milestones in any order, 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. https://doi.org/10.1007/BFb0096509
• M. Benaïm, M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218613
• 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
• R. Bowen, ω-limit sets for Axiom A diffeomorphisms, J. Differential Equations 18 (1975), 333–339. https://doi.org/10.1016/0022-0396(75)90065-0

Why the horseshoe

The Smale horseshoe is the standard example of a smooth invertible map of the plane with chaotic dynamics. Smale introduced it in the 1960s as the mechanism behind the complicated orbits near a transverse homoclinic point, and it became the basic model of hyperbolic invariant sets (Smale 1967). Its importance for differential equations is the Smale–Birkhoff theorem: whenever the stable and unstable manifolds of a hyperbolic fixed point intersect transversally, some iterate of the map contains a horseshoe. Melnikov's method then turns this into a checkable criterion for chaos in periodically forced planar systems such as Duffing's equation.

This mission formalizes the horseshoe as it is treated in Chapter 13 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012). It takes along the one-dimensional results from §§11.4–11.5 that the chapter's argument reuses: the tent map's Cantor set, the one-sided shift, and the metric on two-sided sequences.

Setting

Fix parameters $\lambda$ and $\mu$ and let $D = [0,1]^2$. The two horizontal strips

$$J_0 = [0,1] \times [0, 1/\mu], \qquad J_1 = [0,1] \times [1 - 1/\mu, 1]$$

are mapped by

$$F(x,y) = (\lambda x, \mu y) \text{ on } J_0, \qquad F(x,y) = (1 - \lambda x, \mu(1-y)) \text{ on } J_1 .$$

Each strip is contracted horizontally by $\lambda$ and stretched vertically by $\mu$ into a vertical strip crossing $D$. The book specifies $F$ only on $J_0 \cup J_1$ and leaves the fold between them to a picture. A horseshoe map here is any $F : \mathbb{R}^2 \to \mathbb{R}^2$ given by these formulas on $J_0 \cup J_1$. On $K_0 = F(J_0) = [0, \lambda] \times [0,1]$ and $K_1 = F(J_1) = [1-\lambda, 1] \times [0,1]$ the inverse $g$ is given by explicit formulas.

The tent map $T_\nu(x) = \frac{\nu}{2}(1 - |2x-1|)$ on $\mathbb{R}$ has the invariant set

$$\Lambda(T_\nu) = \{x \in \mathbb{R} : T_\nu^n(x) \in [0,1] \text{ for all } n \ge 0\}.$$

The second coordinate of $F$ is $T_\mu(y)$ and the first coordinate of $g$ is $T_{1/\lambda}(x)$. The horseshoe's invariant set is

$$\Lambda = \Lambda(T_{1/\lambda}) \times \Lambda(T_\mu).$$

The two-sided shift space is $\Sigma_2 = \{0,1\}^{\mathbb{Z}}$. It carries the metric

$$d(s,t) = \tfrac12 \sum_{n \ge 0} \frac{|s_n - t_n| + |s_{-n} - t_{-n}|}{2^n}$$

and the shift $\sigma(s)_n = s_{n+1}$. The itinerary $\varphi(x,y) \in \Sigma_2$ of a point of $\Lambda$ records, for $n \ge 0$, which strip $J_{y_n}$ contains $F^n(x,y)$. For $n < 0$ it records which strip $K_{x_{-n-1}}$ contains $g^{-n-1}(x,y)$.

A system $(M, f)$ is chaotic in the book's sense (p. 296) under four conditions: $f$ is continuous, $M$ is infinite, $f$ is topologically transitive (for nonempty open $U, V$ some $f^n(U)$ meets $V$), and the periodic points are dense. A Cantor set is a compact, perfect, totally disconnected set.

Formalization targets

Goal: Theorem 13.1 (p. 333)

For $0 < \lambda < \tfrac12$, $\mu > 2$ and every horseshoe map $F$:

$$\Lambda \text{ is a Cantor set}, \quad F(\Lambda) = \Lambda, \quad \varphi : \Lambda \to \Sigma_2 \text{ is a homeomorphism with } \sigma \circ \varphi = \varphi \circ F \text{ on } \Lambda,$$ $$\text{and } (\Lambda, F|_\Lambda) \text{ is chaotic.}$$

The book's sentence is: "The Smale horseshoe map has an invariant Cantor set $\Lambda$ on which the dynamics is equivalent to the double sided shift on two symbols. In particular it is chaotic."

Milestones, in attack order

• Lemma 11.15 (p. 306). On two-sided sequences, $d(s,t) \le N^{-n}$ when $s, t$ agree on $|j| \le n$, and $d(s,t)$ is bounded below by a multiple of $N^{-n}$ when they differ at some $|j| \le n$.
• Lemma 11.8 (p. 303). The one-sided shift on $\Sigma_N = \{0, \dots, N-1\}^{\mathbb{N}_0}$ has countably many periodic points, and they are dense.
• Lemma 11.9 (p. 303). The one-sided shift has a dense forward orbit.
• Lemma 11.4 (p. 299). For $\nu > 2$, $\Lambda(T_\nu)$ is a Cantor set.
• Theorem 11.5 (p. 301). For $\nu > 2$, the itinerary map conjugates $(\Lambda(T_\nu), T_\nu)$ to the one-sided shift on $\{0,1\}^{\mathbb{N}_0}$ by a homeomorphism.

Significance

Theorem 13.1 exhibits a two-dimensional invertible system with an explicit invariant set on which the dynamics is exactly the two-sided shift. Every property of the shift is then inherited:

• infinitely many periodic orbits of every period;
• a dense orbit;
• sensitive dependence (Lemma 11.3);
• orbits with any prescribed forward and backward itinerary.

Theorem 13.1 is the model to which the Smale–Birkhoff theorem (13.2) reduces the dynamics near a transverse homoclinic point. It is therefore the terminal object of the book's route from Melnikov integrals to chaos in forced oscillators.

The results are classical and fully proved in the literature. Their proofs have not been formalized. Mathlib has Cantor-type sets (the middle-thirds set), totally disconnected and perfect sets, and product topologies. It has no tent-map invariant set, no two-sided symbolic dynamics with the book's metric, and no conjugacy theorem of this kind. A formal proof would supply a machine-checked conjugacy between a concrete planar map and a full shift, together with the symbolic-dynamics layer it rests on.

Difficulty

The book's own argument for Theorem 13.1 has two gaps that a formal proof must fill. First, it asserts that a product of two Cantor sets is again a Cantor set and leaves this as an exercise. Second, it treats continuity of the itinerary map and of its inverse as an exercise. It also leans on "all other results hold with no further modifications" to transfer the one-sided lemmas (11.7–11.9) to the two-sided shift.

The two-sided transfer is not literally a restatement. The metric (11.35) weights each off-centre index by $\tfrac12$, and so the one-sided closeness estimate does not carry over verbatim; see the correction to Lemma 11.15 below.

The inverse $g$ must also be tracked alongside $F$. The negative half of the itinerary is defined through $g$ rather than through $F$, so the conjugacy at index $-1$ couples the two halves.

Finally, the parameter endpoints need care. The book allows $\lambda = \tfrac12$ and $\mu = 2$. At $\mu = 2$ the defining formulas are inconsistent on $y = \tfrac12$, and at either endpoint one factor of $\Lambda$ is the whole interval $[0,1]$.

Formalization scope

• Parameters. The goal is stated for $0 < \lambda < \tfrac12$ and $\mu > 2$, a correction of the book's closed endpoints recorded in the statement.
• Lemma 11.15 is stated with the lower bound $\tfrac12 N^{-n}$ instead of the printed $N^{-n}$. The printed bound fails for the metric (11.35): for $N = 2$, $n = 1$ and sequences differing only at index $1$, $d = \tfrac14$. The first clause is as printed.
• The map. IsHorseshoeMap λ μ F is a predicate fixing $F$ only on $J_0 \cup J_1$, and the goal quantifies over all such $F$. Its conclusion therefore cannot depend on how the fold is drawn. The inverse horseshoeInv is the explicit formula (13.5)–(13.6).
• Spaces. $\mathbb{R}^2$ is ℝ × ℝ; its max-distance has the Euclidean topology. Sequence spaces are ℕ → Fin N and ℤ → Fin N. The metrics (11.28) and (11.35) are functions symDist and symDistZ, not type-class instances. Density and continuity are stated in $\varepsilon$–$\delta$ form against them, so no unmentioned product topology enters.
• Topological equivalence is spelled out: $F$ maps $\Lambda$ onto $\Lambda$, $\varphi$ is a bijection $\Lambda \to \Sigma_2$, $\sigma \circ \varphi = \varphi \circ F$ on $\Lambda$, and $\varphi$, $\varphi^{-1}$ are continuous.
• Chaos is the book's definition (continuous, infinite, transitive, dense periodic points), applied to $F$ restricted to the subtype $\Lambda$. It is not the three-axiom definition with sensitive dependence.
• Cantor set means compact, Preperfect and IsTotallySeparated, the last being the book's definition of total disconnectedness on p. 302.

$\Lambda$ is constructed as in (13.8) and $\varphi$ as in (13.9), not quantified over. The goal asserts the full conjunction, so it cannot be discharged by exhibiting some other invariant set or some other conjugacy. For $\mu > 2$ maps satisfying IsHorseshoeMap exist, so the hypothesis is not vacuous.

A complete development needs:

• the product of Cantor sets in a product of metric spaces;
• the tent-map coding (Theorem 11.5) for both $T_\mu$ and $T_{1/\lambda}$;
• the two-sided shift's Cantor, periodic-point and transitivity properties;
• transport of chaos along a conjugacy.

The tent-map and one-sided shift lemmas duplicate those of the interval-maps mission of this series and are reusable there. Contributions proving the two-sided analogues of Lemmas 11.7–11.9 as auxiliary lemmas are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012. Author's preliminary version: https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf
• S. Smale, Differentiable dynamical systems, Bull. Amer. Math. Soc. 73 (1967), 747–817. https://doi.org/10.1090/S0002-9904-1967-11798-1
• R. L. Devaney, An Introduction to Chaotic Dynamical Systems, 2nd ed., Addison-Wesley, 1989.
• C. Robinson, Dynamical Systems: Stability, Symbolic Dynamics, and Chaos, 2nd ed., CRC Press, 1999.

Motivation

Periodic solutions are the simplest non-stationary long-time behaviour of an autonomous system $\dot x = f(x)$: limit cycles in oscillators and population models, closed orbits of conservative systems. The first question about a periodic orbit is whether it is stable. Poincaré introduced the first-return map on a transversal section, which turns this question into a question about a fixed point of a map in one dimension less. Floquet theory attacks the same question through the linear periodic system obtained by linearizing along the orbit. This mission formalizes Chapter 12, §§12.1–12.2 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012; author's preliminary version, DOI of the published book). That chapter proves the two approaches agree and derives the standard stability and persistence criteria from this.

Setting

Let $M \subseteq \mathbb{R}^n$ be open, $f \in C^k(M, \mathbb{R}^n)$ with $k \ge 1$, and let $\Phi(t, x)$ be the flow of $\dot x = f(x)$ with maximal intervals $I_x$: $t \mapsto \Phi(t,x)$ is the unique maximal solution with $\Phi(0,x) = x$. A point $x_0 \in M$ is periodic with period $T > 0$ if $\Phi(T, x_0) = x_0$ and $\Phi(t, x_0) \neq x_0$ for $0 < t < T$. Its orbit $\gamma(x_0) = \{\Phi(t, x_0)\}$ is then a closed curve.

Linearization along the orbit. Put $A(t) = df_{\Phi(t, x_0)}$, a $T$-periodic matrix. The first variational equation is $\dot y = A(t) y$, and $\Pi_{x_0}(t, t_0)$ denotes its principal matrix solution: $\partial_t \Pi = A(t)\Pi$, $\Pi(t_0, t_0) = \mathbb{I}$. The monodromy matrix based at $\Phi(t_0,x_0)$ is

$$M_{x_0}(t_0) = \frac{\partial \Phi_T}{\partial x}\big(\Phi(t_0, x_0)\big).$$

The Poincaré map. A transversal section is $\Sigma = \{x \in U \mid S(x) = 0\}$ with $U$ open, $S \in C^k(U)$, $\partial S/\partial x \ne 0$ and $(\partial S/\partial x)\, f \neq 0$ on $\Sigma$. If $x_0 \in \Sigma$ there is a $C^k$ return time $\tau$ near $x_0$ with $\tau(x_0) = T$ and $\Phi(\tau(y), y) \in \Sigma$. The Poincaré map is

$$P_\Sigma(y) = \Phi(\tau(y), y).$$

Its derivative $dP_\Sigma(x_0)$ is a linear map of the $(n-1)$-dimensional tangent space $T_{x_0}\Sigma = \ker \frac{\partial S}{\partial x}(x_0)$ into itself.

Stability. The orbit $\gamma$ is stable if every neighborhood $U$ of $\gamma$ contains a neighborhood $V$ of $\gamma$ from which solutions stay in $U$ for all $t \ge 0$. It is asymptotically stable if moreover $d(\Phi(t,x), \gamma) \to 0$ for all $x$ in some neighborhood of $\gamma$. A periodic orbit is hyperbolic if $dP_\Sigma(x_0)$ has no eigenvalue on the unit circle.

Formalization targets

Goal: Theorem 12.4

For every $t_0 \in \mathbb{R}$,

$$\chi_{M_{x_0}(t_0)}(X) = (X - 1)\,\chi_{dP_\Sigma(x_0)}(X),$$

where $\chi$ is the characteristic polynomial. So the eigenvalues of $dP_\Sigma(x_0)$ together with the single value $1$ are exactly the eigenvalues of the monodromy matrix, with multiplicities. In particular they depend neither on the section $\Sigma$ nor on the base point on the orbit.

Milestones

• Lemma 12.1. $\Pi_{x_0}(t,t_0) = \frac{\partial\Phi_{t-t_0}}{\partial x}(\Phi(t_0,x_0))$, and $f(\Phi(t,x_0)) = \Pi_{x_0}(t,t_0) f(\Phi(t_0,x_0))$.
• Corollary 12.3. If every eigenvalue of $dP_\Sigma(x_0)$ has modulus $< 1$, then $\gamma(x_0)$ is asymptotically stable.
• Corollary 12.5. $\det dP_\Sigma(x_0) = \det M_{x_0}(t_0) \neq 0$, and $P_\Sigma$ is a local $C^k$ diffeomorphism of $\Sigma$ at $x_0$.
• Lemma 12.6. For $n = 2$, $\gamma(x_0)$ is asymptotically stable if $\int_0^T \operatorname{div} f(\Phi(t,x_0))\,dt < 0$ and unstable if the integral is positive.
• Lemma 12.7. If $f(x,0)$ has a hyperbolic periodic orbit through $x_0$ and $f(x,\mu)$ is $C^k$, then on a neighborhood of $\mu = 0$ there is a $C^k$ family $x_0(\mu)$ with $x_0(0) = x_0$ and each $x_0(\mu)$ periodic for $f(\cdot,\mu)$.

Significance

The result. Theorem 12.4 is the bridge between the two standard tools for periodic orbits. The Floquet multipliers of $\dot y = A(t)y$ can often be computed or estimated, for instance through Liouville's formula $\det M_{x_0}(t_0) = \exp\int_0^T \operatorname{div} f(\Phi(t,x_0))\,dt$. The Poincaré map is where the dynamics is decided, for instance through the fixed-point stability theory of maps. Corollaries 12.3 and 12.5 and Lemma 12.6 are the resulting stability tests. Lemma 12.7 is the structural-stability statement for hyperbolic orbits that bifurcation theory starts from. Theorems 12.8–12.10 (stable manifolds of periodic orbits) build on the same objects.

Formalizing it. All results are classical and proved in the book. None has a machine-checked proof on the platform or, as far as is known, in Mathlib, which has neither Poincaré maps nor the linearization of flows along orbits. The work is a formalization of the known proofs. It needs differentiability of the flow with respect to initial conditions, and that part is reusable across the whole of qualitative ODE theory.

Difficulty

The algebra of Theorem 12.4 is short. The two linear maps act on different spaces: $M_{x_0}(0)$ on $\mathbb{R}^n$, and $dP_\Sigma(x_0)$ on the hyperplane $T_{x_0}\Sigma$. That hyperplane is in general not orthogonal to $f(x_0)$, not a coordinate hyperplane, and not invariant under $M_{x_0}(0)$. Any comparison has to go through the derivative of $y \mapsto \Phi(\tau(y), y)$, which involves the derivative of the implicitly defined return time. Behind all this sits the differentiability of $\Phi$ in $x$ and the variational equation it satisfies, which Mathlib does not provide for local flows. For the stability milestones, the delicate step is passing from the discrete iterates of $P_\Sigma$ on $\Sigma$ back to the continuous flow near the whole orbit. That requires uniform control over one period.

Formalization scope

The state space is Fin n → ℝ. Norm-dependent notions (distance to the orbit, neighborhoods) do not depend on the choice of norm. The flow is local: IsMaximalFlow f M I Φ characterizes $\Phi$ and $I_x$ by maximality and uniqueness, and $\Phi$'s values outside its domain are never used. Derivatives are Mathlib's fderiv. The section $\Sigma$ is the book's general $\{S = 0\}$ with $(\partial S/\partial x)f \neq 0$, not a hyperplane chosen orthogonal to $f(x_0)$. The return time $\tau$ is any $C^k$ function on a neighborhood of $x_0$ with $\tau(x_0) = T$ and $\Phi(\tau(y),y) \in \Sigma$; such a function agrees with the book's $\tau$ near $x_0$. $dP_\Sigma(x_0)$ is an endomorphism L of LinearMap.ker (fderiv ℝ S x₀) that agrees with the derivative of $y \mapsto \Phi(\tau(y), y)$ there (IsPoincareDerivative). Theorems 12.4 and 12.5 assert that it exists. Eigenvalues are complex roots of characteristic polynomials.

Conventions and readings:

• The goal compares characteristic polynomials, so multiplicities count. Equality of eigenvalue sets, a statement at a single convenient $t_0$, or a hyperplane section would each be weaker than the book's theorem and do not count as solving the goal.
• The monodromy matrix is $\frac{\partial\Phi_T}{\partial x}(\Phi(t_0,x_0))$. The book prints $\Phi_{T-t_0}$ on p. 316, a typo inconsistent with (12.5) and (12.8).
• "Periodic orbit" means positive least period. Fixed points are excluded, since there is no transversal section through them. In dimension $n \le 1$ no such orbit exists, and the statements are vacuous there as in the book.
• "Hyperbolic periodic orbit" is not defined in the preliminary version. The definition used is the one the proof of Lemma 12.7 uses: no eigenvalue of $dP_\Sigma(x_0)$ on the unit circle, for some transversal section.
• Lemma 12.7: "in a sufficiently small neighborhood of $0$" is read as: there exists an open $W \ni 0$ inside the parameter set on which $x_0(\cdot)$ is $C^k$. The parameter lies in $\mathbb{R}^p$.
• Corollary 12.5: "local diffeomorphism at $x_0$" is read as: $P_\Sigma$ maps $W \cap \Sigma$ bijectively onto $W' \cap \Sigma$ for open $W, W' \ni x_0$, with an inverse that is the restriction of a $C^k$ map on $W'$.
• (12.1) is stated for all $x$ in a neighborhood of the orbit. The book writes $U(x_0)$ right after introducing $U(\gamma(x_0))$.

Needed infrastructure: existence, uniqueness and $C^k$ dependence on initial conditions for local flows; the implicit function theorem (Mathlib); characteristic polynomials and determinants of endomorphisms of finite-dimensional subspaces (Mathlib); Liouville's formula; stability of fixed points of $C^1$ maps with contracting linearization. Contributions of any of these as standalone lemmas are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012. https://doi.org/10.1090/gsm/140 (preliminary version: https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf)
• H. Poincaré, Mémoire sur les courbes définies par une équation différentielle, J. Math. Pures Appl. (3) 7 (1881) 375–422. http://www.numdam.org/item/JMPA_1881_3_7__375_0/
• G. Floquet, Sur les équations différentielles linéaires à coefficients périodiques, Ann. Sci. ÉNS (2) 12 (1883) 47–88. https://doi.org/10.24033/asens.220
• P. Hartman, Ordinary Differential Equations, 2nd ed., SIAM Classics in Applied Mathematics 38, 2002. https://doi.org/10.1137/1.9780898719222