Motivation

Nguyen and Tang study the irreversible catalytic network $\mathcal A+\mathcal B\to\mathcal B+\mathcal C$, $\mathcal B+\mathcal C\to\mathcal A+\mathcal B$, a simple reaction–diffusion system with both a positive and a boundary equilibrium (catalyst used up). They settle every mass regime but one and leave it as a conjecture (AIM problem 416).

Timeline. 2021: Fellner–Morgan–Tang give global classical solutions with uniform bounds. 2026: Nguyen–Tang prove convergence for $M_1<M_2$ and $M_1\ge2M_2$ and local results in between, conjecturing global attraction there.

Setting

On a bounded connected smooth domain $\Omega\subset\mathbb R^n$ with $|\Omega|=1$ and $d_1,d_2,d_3>0$:

$$a_t-d_1\Delta a=b(c-a),\quad b_t-d_2\Delta b=b(c-a),\quad c_t-d_3\Delta c=-b(c-a),$$

with homogeneous Neumann conditions and strictly positive $C^2$ compatible initial data. The masses $M_1=\int_\Omega(a_0+c_0)$, $M_2=\int_\Omega(b_0+c_0)$ are conserved. The equilibria are the positive one $(\frac{M_1}2,\,M_2-\frac{M_1}2,\,\frac{M_1}2)$ and the boundary one $(M_1-M_2,\,0,\,M_2)$.

Formalization target

If $M_2\le M_1<2M_2$, every classical solution converges uniformly on $\Omega$ to the positive equilibrium (no rate required).

Significance

This is the last open regime of Nguyen–Tang's stability analysis. Strict positivity is essential: with $b_0\equiv0$ the solution stays away from the positive equilibrium.

Difficulty

For $M_1\ge M_2$ there is no positive lower bound on $\int_\Omega b$, so entropy dissipation can degenerate near the boundary equilibrium ($b=0$), and the local results do not exclude trajectories approaching it.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and $\Delta$ is Mathlib's Laplacian. The domain is $\Omega=\{\varphi<0\}$ for a $C^\infty$ function $\varphi$ with $\nabla\varphi\ne0$ on $\{\varphi=0\}$; the Neumann condition is the derivative within $\overline\Omega$ in the direction $\nabla\varphi$. Solutions are continuous on $[0,\infty)\times\overline\Omega$ and $C^{1,2}$ for $t>0$, and $L^\infty$ convergence is TendstoUniformlyOn. The goal quantifies over classical solutions; their existence is proved in the literature (Fellner–Morgan–Tang; Nguyen–Tang, Theorem 2.1) but is not part of this statement.

Selected references

• T. L. Nguyen, B. Q. Tang, Stability analysis of irreversible chemical reaction-diffusion systems with boundary equilibria, Z. Angew. Math. Phys. 77, 2026, 199. DOI
• K. Fellner, J. Morgan, B. Q. Tang, Uniform-in-time bounds for quadratic reaction-diffusion systems with mass dissipation in higher dimensions, DCDS-S 14, 2021, 635–651. DOI
• AIM open problems list, problem 416. github.com/MColbrook/AIM

Motivation

The first step in analysing a nonlinear differential equation $\dot x = f(x)$ near an equilibrium is usually to replace $f$ by its derivative there and study the linear system $\dot x = Ax$, which can be solved explicitly. This step is justified only if the linearization predicts the qualitative behaviour of the nonlinear system correctly. The Hartman–Grobman theorem makes that precise. If no eigenvalue of $A$ lies on the imaginary axis, then near the equilibrium the nonlinear flow is a continuous deformation of the linear flow $e^{tA}$. The phase portrait, including which solutions approach the equilibrium and which leave it, is the linear one up to a homeomorphism.

The theorem was proved independently by D. M. Grobman (1959) and P. Hartman (1960, Proc. AMS 11). C. Pugh gave the proof by a global contraction argument (1969, Amer. J. Math. 91) that most textbooks follow, including this one.

This mission formalizes the Hartman–Grobman part of Chapters 9 and 10 of Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012; author's preliminary version): the linear stable and unstable subspaces, the conjugacy lemma for maps, and the theorem for flows and for maps.

Setting

Let $n \in \mathbb{N}$ and let $A$ be a real $n \times n$ matrix. Its eigenvalues $\alpha_j$ are the complex numbers $z$ with $Av = zv$ for some nonzero $v \in \mathbb{C}^n$. For a set $S \subseteq \mathbb{C}$, the spectral subspace $E_S(A) \subseteq \mathbb{R}^n$ is the set of real vectors lying in the sum of the generalized eigenspaces $\operatorname{Ker}(A - \alpha_j)^{a_j}$ with $\alpha_j \in S$, where $a_j$ is the algebraic multiplicity.

For the linear flow $e^{tA}$, the stable subspace is $E^+ = E_{\{\operatorname{Re} z < 0\}}(A)$ and the unstable subspace is $E^- = E_{\{\operatorname{Re} z > 0\}}(A)$. $A$ is hyperbolic (for flows) if no eigenvalue has zero real part. For the linear map $x \mapsto Ax$, the contracting and expanding subspaces are $E^+(A) = E_{\{|z| < 1\}}(A)$ and $E^-(A) = E_{\{|z| > 1\}}(A)$, and $A$ is hyperbolic (for maps) if no eigenvalue lies on the unit circle.

A vector field is a $C^1$ map $f : M \to \mathbb{R}^n$ on an open set $M \subseteq \mathbb{R}^n$. Its flow $\Phi(t, x)$ is the maximal solution of $\dot x = f(x)$, $x(0) = x$, defined for $t$ in the maximal interval $I_x \ni 0$. A point $x_0$ with $f(x_0) = 0$ is a fixed point. It is hyperbolic if the Jacobian matrix $A = df_{x_0}$ is hyperbolic. Two flows $\Phi, \Psi$ are topologically conjugate if there is a homeomorphism $\phi$ of $\mathbb{R}^n$ with $\phi \circ \Phi_t = \Psi_t \circ \phi$.

Formalization targets

Goal: Theorem 9.9 (Hartman–Grobman)

Let $0 \in M$ be a hyperbolic fixed point of the $C^1$ vector field $f$, with $A = df_0$ and flow $\Phi$. Then there are a homeomorphism $\phi(x) = x + h(x)$ of $\mathbb{R}^n$, with $h$ bounded, and a neighborhood $U$ of $0$ such that

$$\phi\big(e^{tA} x\big) = \Phi\big(t, \phi(x)\big), \qquad t \in I_{\phi(x)},$$

for all $x$ and $t$ with $e^{sA}x \in U$ for every $s$ between $0$ and $t$.

Milestones

In attack order:

1. Theorem 9.2: $E^\pm$ are invariant under $e^{tA}$ and $|e^{tA}x^\pm| \le C e^{\mp t\alpha}|x^\pm|$ for $\pm t \ge 0$, for every $\alpha$ below the relevant spectral gap.
2. Lemma 9.7: for $A$ invertible and hyperbolic for maps, a norm adapted to $A$, and bounded $g$ with small Lipschitz constant, there is a unique bounded continuous $h$ with

$$(\mathrm{id} + h) \circ A = (A + g) \circ (\mathrm{id} + h),$$

and $\mathrm{id} + h$ is a homeomorphism when $A + g$ is invertible. 3. Corollary 9.8: such a conjugating homeomorphism of the form identity plus bounded is unique. 4. Theorem 10.4 (Hartman–Grobman for maps): a $C^1$ local diffeomorphism with a hyperbolic fixed point $0$ satisfies $\phi \circ A = f \circ \phi$ near $0$, with $A = df_0$. 5. Theorem 9.10: two hyperbolic linear flows whose stable and unstable subspaces have equal dimensions are topologically conjugate.

Significance

The result itself. Hartman–Grobman reduces the local topological classification of hyperbolic equilibria to linear algebra. Together with Theorem 9.10 it shows that, near a hyperbolic fixed point, a $C^1$ vector field is determined up to local topological conjugacy by two integers: the dimensions of the stable and unstable subspaces. In particular, stability and instability of a hyperbolic equilibrium can be read off the eigenvalues of the Jacobian.

Formalizing it. Mathlib has the matrix exponential, generalized eigenspaces and homeomorphisms. It has no hyperbolic splitting of a matrix, no conjugacy theory for flows or maps, and no local flow of an ODE with maximal intervals; none of these results has a machine-checked proof on this platform. The mission builds the linear hyperbolic layer (spectral subspaces with exponential rates), the functional-analytic conjugacy lemma, and the local theorems on top of them.

Difficulty

The naive idea is to conjugate the nonlinear flow to its linearization directly on a small ball. That fails because a small ball is not invariant: orbits of a saddle leave every neighborhood of the fixed point, and a conjugacy defined only on the ball cannot be propagated along them. The book's route first makes the problem global and then solves a functional equation. Solving it requires an operator-norm estimate on a space of bounded continuous functions, with a norm on $\mathbb{R}^n$ adapted to the hyperbolic splitting.

A second difficulty is passing from one time to all times. A conjugacy for the time-one map has to be upgraded to one for the whole flow, which needs a uniqueness statement (Corollary 9.8) and control of the derivative of the flow through the variational equation. Throughout, the flow is local, so every identity $\Phi(t, \phi(x)) = \dots$ also carries the claim that $t$ lies in the maximal interval of $\phi(x)$.

Formalization scope

The state space is Fin n → ℝ; matrices are Matrix (Fin n) (Fin n) ℝ, $e^{tA}$ is NormedSpace.exp (t • A) acting by mulVec, and eigenvalues are those of the complexified matrix. The subspaces $E^\pm$ are defined spectrally, exactly as the book's (9.2), with the book's sign convention ($+$ is the stable or contracting side for both flows and maps). The flow is local and enters through IsMaximalFlow f M I Φ, the unique maximal integral curves on an open phase space $M$. No completeness is assumed.

Conventions and quantifier readings:

• Smoothness. "Differentiable vector field" in Theorem 9.9 is read as $C^1$ on $M$, since the proof uses continuity of $\partial f/\partial x$. "Local diffeomorphism" in Theorem 10.4 is read as $C^1$ with invertible derivative everywhere.
• Local conjugacy. "In a sufficiently small neighborhood of $0$" is made explicit as $\exists\, U \in \mathcal{N}(0)$, chosen after $\phi$. For flows, the identity is required along every linear orbit segment $\{e^{sA}x : s \text{ between } 0 \text{ and } t\}$ contained in $U$, for both signs of $t$, together with $t \in I_{\phi(x)}$. For maps, it is required for all $x \in U$.
• Constants. "Some $C > 0$ depending on $\alpha$" (Theorem 9.2) is $\forall \alpha\ \exists C > 0\ \forall t\ \forall x$.
• Adapted norm. Lemma 9.7's "choose a norm such that $\alpha = \max(\|A_-^{-1}\|, \|A_+\|) < 1$" is a norm $N$ passed as a parameter, with the two operator bounds as hypotheses. The lemma also assumes that the projections onto $E^\pm$ do not increase $N$. The book's proof uses this when it bounds $\|L^{-1}\| \le 2/(1-\alpha)$, and the norms it constructs satisfy it. This is the one hypothesis added to a printed statement.

A trivializing formalization is ruled out. The conjugacy at the single point $0$, or at $t = 0$ only, holds for every $\phi$ (both sides are $0$, respectively $\phi(x)$). The goal instead fixes $\phi$ and $U$ first and requires the identity on every orbit segment inside $U$, with $\Phi$ the maximal flow of $f$ rather than an arbitrary map.

Needed infrastructure:

• the hyperbolic splitting $\mathbb{R}^n = E^+ \oplus E^-$ with exponential estimates and adapted norms;
• Neumann series and contraction arguments on the Banach space of bounded continuous functions;
• smooth cut-off of the nonlinearity;
• differentiability of the flow in the initial condition (variational equation) and Gronwall's inequality;
• maximal solutions of $C^1$ ODEs.

The linear layer and the conjugacy lemma are reusable for the stable manifold theorem, for periodic orbits (Chapter 12) and for the horseshoe (Chapter 13). Standalone contributions of those layers are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012; author's preliminary version, Chapters 9–10, pp. 253–290. https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf (published book: https://doi.org/10.1090/gsm/140)
• P. Hartman, A lemma in the theory of structural stability of differential equations, Proceedings of the AMS 11 (1960), 610–620. https://doi.org/10.1090/S0002-9939-1960-0121542-7
• D. M. Grobman, Homeomorphism of systems of differential equations, Doklady Akademii Nauk SSSR 128 (1959), 880–881.
• C. C. Pugh, On a theorem of P. Hartman, American Journal of Mathematics 91 (1969), 363–367. https://doi.org/10.2307/2373513

Motivation

Many linear differential equations of mathematical physics have coefficients with singular points. Examples are the Bessel equation $z^2u'' + zu' + (z^2 - \nu^2)u = 0$, which comes from separating variables in the Laplace and wave equations in cylindrical coordinates, and the Legendre, hypergeometric and confluent hypergeometric equations. Near a singular point the usual power-series method breaks down, and the practical question is how solutions behave as $z$ approaches the singularity. Evaluating special functions, matching asymptotics and computing connection coefficients all depend on the answer.

For second-order equations the answer goes back to Lazarus Fuchs (Zur Theorie der linearen Differentialgleichungen mit veränderlichen Coefficienten, J. reine angew. Math. 66 (1866), 121–160, doi:10.1515/crll.1866.66.121) and to Georg Frobenius (Ueber die Integration der linearen Differentialgleichungen durch Reihen, J. reine angew. Math. 76 (1873), 214–235, doi:10.1515/crll.1873.76.214). Frobenius's generalized power-series ansatz $u = z^\alpha \sum_j h_j z^j$ is known as the Frobenius method. This mission follows Chapter 4 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012, doi:10.1090/gsm/140), in the author's preliminary version.

Setting

All functions are complex-valued functions of a complex variable $z$, and derivatives are complex derivatives. The object is the second-order linear equation

$$u''(z) + p(z)\,u'(z) + q(z)\,u(z) = 0 \qquad (4.20)$$

near the point $z = 0$, where the coefficients may be singular. A function $f$ that is holomorphic on a punctured disc $0 < |z| < r$ has a pole of order at most $k$ at $0$ if $z^k f(z)$ extends to a function analytic at $0$. The point $0$ is a regular singular point of (4.20) if $p$ has a pole of order at most one and $q$ a pole of order at most two there:

$$p(z) = \frac1z\sum_{j\ge0} p_j z^j, \qquad q(z) = \frac1{z^2}\sum_{j\ge0} q_j z^j, \qquad |z| < R. \qquad (4.30)$$

In Lean these hypotheses are functions $P, Q$ holomorphic on $|z| < R$ with $zp(z) = P(z)$ and $z^2q(z) = Q(z)$ for $0 < |z| < R$. The general notion is TeschlODE.Frobenius.HasPoleOfOrderAtMost f k.

The indicial equation is $\alpha^2 + (p_0 - 1)\alpha + q_0 = 0$. Its roots, the characteristic exponents, are

$$\alpha_{1,2} = \tfrac12\Big(1 - p_0 \pm \sqrt{(p_0-1)^2 - 4q_0}\Big), \qquad (4.37)$$

where the square root is the principal branch, so that $\operatorname{Re}\alpha_1 \ge \operatorname{Re}\alpha_2$. In Lean they are charExponents p₀ q₀.

The functions $z^\alpha = e^{\alpha\log z}$ and $\log z$ are single-valued only after a branch cut is chosen. As the book does, solutions are considered on the slit punctured disc $\{0 < |z| < R\} \setminus (-\infty, 0]$ (slitDisc R), using the principal branches. A solution of (4.20) on an open set $D$ is IsSolution p q D u. A fundamental system is a pair of solutions that are linearly independent over $\mathbb{C}$ on $D$.

Formalization targets

Goal: Fuchs's theorem (Theorem 4.5)

Let $0$ be a regular singular point as in (4.30), with $P, Q$ holomorphic on $|z| < R$, $0 < R \le \infty$. Let $\alpha_1, \alpha_2$ be the characteristic exponents of $p_0 = P(0)$, $q_0 = Q(0)$. Then there are functions $h_1, h_2$, holomorphic on the whole disc $|z| < R$ with $h_1(0) = h_2(0) = 1$, such that on $\{0<|z|<R\}\setminus(-\infty,0]$ the following holds.

• Case 1. If $\alpha_1 - \alpha_2 \notin \mathbb{N}_0$, then $u_j(z) = z^{\alpha_j}h_j(z)$ for $j = 1, 2$ form a fundamental system.
• Case 2. If $\alpha_1 - \alpha_2 = m \in \mathbb{N}_0$, then for some $c \in \mathbb{C}$, with $c \ne 0$ when $m = 0$,

$$u_1(z) = z^{\alpha_1}h_1(z), \qquad u_2(z) = z^{\alpha_2}h_2(z) + c\log(z)\,u_1(z)$$

form a fundamental system.

The requirement that $h_j$ be holomorphic on the full disc is the book's statement that the radius of convergence of $h_j$ is at least the smaller of the radii of convergence of $p$ and $q$.

Milestones

In attack order:

1. Theorem 4.1. For $f$ analytic and bounded on the bidisc $\{|z-z_0|<\varepsilon, |w-w_0|<\delta\}$ with $M = \sup|f|$, the problem $w' = f(z,w)$, $w(z_0) = w_0$ has a unique analytic solution on $|z - z_0| < \min(\varepsilon, \delta/M)$.
2. Lemma 4.4. For $p$ holomorphic on $0<|z|<R$, the equation $u' + p(z)u = 0$ has a solution $z^\alpha h(z)$ with $h$ analytic at $0$ and $h(0) = 1$ if and only if $p$ has at most a first-order pole. In that case $\alpha = -\lim_{z\to0} zp(z)$, and $h$ has radius of convergence at least $R$.
3. Theorem 4.7. For $A$, $b$ analytic on a simply connected domain $\Omega$, the problem $w' = A(z)w + b(z)$, $w(z_0) = w_0$ has a unique solution on all of $\Omega$. Its power series at $z_0$ converges on the largest disc about $z_0$ contained in $\Omega$.
4. Theorem 4.6 (Fuchs, converse). For $p, q$ holomorphic on a punctured disc, (4.20) has a fundamental system of the form in Theorem 4.5 if and only if $p$ and $zq$ have at most first-order poles.

Significance

Theorem 4.5 is the basic structural theorem for linear equations at a regular singular point. It determines the leading behaviour $z^{\alpha_j}$ of each solution from two numbers read off the coefficients. It says exactly when a logarithm can occur, and it guarantees that the series part converges on the full disc on which the coefficients converge. Theorem 4.6 shows that the regular-singular hypothesis cannot be weakened. The series expansions of Bessel functions $J_\nu$, of Legendre functions and of the hypergeometric function $F(a,b,c;z)$, and the logarithmic second solutions for integer order, are all instances of the theorem. The theorem is also the local ingredient of the classification of Fuchsian equations, including the Riemann $P$-symbol.

Mathlib has holomorphic functions, power series with radius of convergence, the principal complex power and logarithm, and a real-variable ODE layer. It has no complex-analytic existence theorem for differential equations and no Frobenius theory. The results here are classical and proved in the book, but to our knowledge none of them has a machine-checked proof. The platform has real-variable regular-singular estimates (the RegularSingular namespace), which are a different setting. A formal Theorem 4.5 would give a foundation for formal special-function theory, for example Bessel functions defined as solutions of their equation.

Difficulty

The formal power-series computation is mechanical: substitute $z^\alpha\sum h_jz^j$, compare coefficients, and read off the indicial equation and a recursion for the $h_j$. The difficulty is everything around it. First, the recursion for the second exponent breaks down exactly when $\alpha_1 - \alpha_2 \in \mathbb{N}_0$, and the form of the second solution changes there. Whether a logarithm really appears depends on a compatibility condition that can go either way when $m \ge 1$. Second, the claim is about actual solutions on a slit domain, not formal series. This needs convergence estimates for the recursion and the principal branches of $z^\alpha$ and $\log z$. Third, the radius claim asks for convergence on the whole disc of the coefficients, not just on some small disc. Fourth, linear independence of the two solutions has to be proved on the slit domain.

Milestones 1 and 3 need the complex analogues of Picard iteration and analytic continuation, which Mathlib does not supply for differential equations.

Formalization scope

Namespace TeschlODE.Frobenius. Complex derivatives are HasDerivAt/deriv/DifferentiableAt ℂ, and holomorphy on a set is DifferentiableOn ℂ. Radii are ENNReal, so $R = \infty$ is allowed. Discs are Metric.eball 0 R. Powers and logarithms are Mathlib's principal Complex.cpow and Complex.log, used only on slitDisc R = Metric.eball 0 R ∩ Complex.slitPlane. On the full punctured disc these functions are discontinuous along the negative axis, and the theorem would be false there. "Fundamental system" is linear independence over $\mathbb{C}$ on the solution domain. Without independence Case 1 would hold trivially with $u_2 = u_1$. "$\alpha_1 - \alpha_2 \in \mathbb{N}_0$" is ∃ m : ℕ, α₁ - α₂ = m. The book's "the constant $c$ might be zero unless $m=0$" is the clause $m = 0 \Rightarrow c \ne 0$.

Quantifier readings:

• "Analytic near $z = 0$" is strengthened to holomorphic on the whole disc of radius $R$, as the book's radius claim asserts.
• "Poles of order at most one and two" is given explicitly: $P, Q$ holomorphic on $|z|<R$ with $zp = P$, $z^2q = Q$ on $0<|z|<R$.
• In Theorem 4.1, the case $M = 0$ is read as $\varepsilon_0 = \varepsilon$. The supremum is over the nonempty bidisc, and a boundedness hypothesis is included.
• In Lemma 4.4, "a solution of the form (4.29)" means one on some slit punctured disc of positive radius. The book's "the radii are the same" is corrected to "at least": $h(z) = 1 - z$, $p(z) = 1/(1-z)$ is a counterexample to equality.
• In Theorem 4.6, "as in the previous theorem" means the form (4.49) for some exponents and some $c$ (Case 1 is $c = 0$), on some slit punctured disc of radius $0 < \rho \le R$.
• In Theorem 4.7, "simply connected domain" is IsOpen Ω together with SimplyConnectedSpace Ω. "The largest disc" has radius Metric.infEDist z₀ Ωᶜ.

The trivializing formalization, with the two solutions not required to be linearly independent or with $h_j$ unconstrained away from $0$, is ruled out by the independence clause and by requiring $h_j$ to be holomorphic on the whole disc with $h_j(0) = 1$.

A full development needs the following: the complex Picard iteration, analytic continuation along paths (the monodromy theorem), Cauchy-type estimates for recursively defined power series, and the calculus of $z^\alpha$ and $\log z$ on the slit plane. The definitions slitDisc, IsSolution, charExponents and HasPoleOfOrderAtMost can be reused for the Bessel, Legendre and hypergeometric equations (Problems 4.5–4.18 of the book). Contributions such as a general complex-analytic ODE existence theorem are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012, doi:10.1090/gsm/140; author's preliminary version, Chapter 4, mat.univie.ac.at/~gerald/ftp/book-ode/.
• L. Fuchs, Zur Theorie der linearen Differentialgleichungen mit veränderlichen Coefficienten, J. reine angew. Math. 66 (1866), 121–160, doi:10.1515/crll.1866.66.121.
• G. Frobenius, Ueber die Integration der linearen Differentialgleichungen durch Reihen, J. reine angew. Math. 76 (1873), 214–235, doi:10.1515/crll.1873.76.214.
• E. L. Ince, Ordinary Differential Equations, Longmans, Green and Co., 1926 (Dover reprint 1956), Chapters XV–XVI.

Motivation

Many control tasks come with a deadline: a consensus protocol or a regulation task must reach its target by a time fixed in advance, whatever the initial condition. Prescribed-time stabilization asks for a feedback law that brings every trajectory of a control system to the equilibrium by a user-chosen time $T$. The basic test case is the chain of integrators $x_1^{(n)}=u$, the normal form of every single-input feedback-linearizable system.

Two routes to prescribed-time stabilization exist. Time-varying gains that blow up as $t\to T$ (Song, Wang, Holloway and Krstić, Automatica 2017) are fragile under measurement noise. Fixed-time stabilization gives a settling time bounded uniformly over all initial conditions, and a time rescaling then turns the uniform bound into any prescribed $T$. Chitour, Ushirobira and Bouhemou (SIAM J. Control Optim. 2020) follow the second route with an explicit, continuous feedback. It combines Hong's backstepping homogeneous controller (Systems Control Lett. 2002) with a degree of homogeneity that depends on the state (Harmouche, Laghrouche, Chitour and Hamerlain, Int. J. Control 2017). A continuity device of Lopez-Ramirez, Efimov, Polyakov and Perruquetti (Int. J. Robust Nonlinear Control 2018) makes that degree a continuous function of the state. This mission formalizes the construction and its main results, §4.1–4.2 of the paper.

Setting

Fix $n\ge1$ and write $x=(x_1,\dots,x_n)\in\mathbb R^n$ with the Euclidean norm. Let $J_n$ be the $n$-th Jordan block ($J_ne_i=e_{i-1}$, $e_0=0$). The pure chain of integrators (31) is

$$\dot x=J_nx+u\,e_n .$$

For $y\in\mathbb R$ and $a>0$ write $\lceil y\rfloor^a=\operatorname{sign}(y)|y|^a$. Given gains $\ell_1,\dots,\ell_n>0$ and $\kappa\in[-\tfrac1{2n},\tfrac1{2n}]$, set $r_j=1+(j-1)\kappa$ and $\beta_j=(2+\kappa)/r_{j+1}-1$. Define $v_0=0$ and

$$v_j=-\ell_j\Big\lceil\lceil x_j\rfloor^{\beta_{j-1}}-\lceil v_{j-1}\rfloor^{\beta_{j-1}}\Big\rfloor^{\frac{r_j+\kappa}{r_j\beta_{j-1}}} .$$

The homogeneous feedback is $\omega^H_\kappa(x)=v_n(x)$ (Definition 23). The associated Lyapunov function is

$$V_\kappa(x)=\sum_{j=1}^n\frac{|x_j|^{\beta_{j-1}+1}-|v_{j-1}|^{\beta_{j-1}+1}}{\beta_{j-1}+1}-\lceil v_{j-1}\rfloor^{\beta_{j-1}}(x_j-v_{j-1}),$$

and (36) is the decay inequality $\dot V_\kappa\le-CV_\kappa^{1+\alpha(\kappa)}$, with $\alpha(\kappa)=\kappa/(2+\kappa)$ and one constant $C$ for all $\kappa$ in the range.

For $m\in(0,1)$ and $\kappa_0\in(0,\tfrac1{2n})$, the state-dependent degree $\kappa(x)$ of (49) equals $\kappa_0$ where $V_0(x)>1+m$ and $-\kappa_0$ where $V_0(x)<1-m$, and it interpolates linearly in $V_0$ in between. The closed-loop controller is $\omega^H_{\kappa(x)}(x)$. With $B^\kappa_{<a}=\{V_\kappa<a\}$, let $r(m,\kappa_0)$ be the largest $r$ with $B^{\kappa_0}_{<r}\subseteq B^0_{<1+m}$, and $r(m,-\kappa_0)$ the smallest $r$ with $B^{-\kappa_0}_{<r}\supseteq B^0_{<1-m}$. Set

$$T^\ast(m,\kappa_0)=\frac1C\Big(\frac{r(m,\kappa_0)^{-\alpha(\kappa_0)}}{\alpha(\kappa_0)}-2\ln(2m)+\frac{r(m,-\kappa_0)^{-\alpha(-\kappa_0)}}{-\alpha(-\kappa_0)}\Big).$$

Finally $D^{\mathbf r}_\lambda=\operatorname{diag}(\lambda^{n-i+1})$ is the dilation of (5).

A system is globally fixed-time stable with settling time at most $T$ if the origin is an equilibrium, solutions exist from every initial state, it is Lyapunov stable, and every solution vanishes for all $t\ge T$ (Definition 1 with $\Omega=\mathbb R^n$).

Formalization targets

Goal: Theorem 30 (p. 1038)

Let the gains and $C>0$ satisfy (36). There are $m\in(0,1)$ and $\kappa_0\in(0,\tfrac1{2n})$ such that, for every $T>0$ and every $\lambda>0$ with

$$\lambda\ \ge\ T^\ast(m,\kappa_0)/T,$$

the feedback $u=\omega^H_{\kappa(D^{\mathbf r}_\lambda x)}(D^{\mathbf r}_\lambda x)$ makes (31) globally fixed-time stable with settling time at most $T$.

Milestones

• Proposition 24 (p. 1034): gains exist for which (36) holds uniformly in $\kappa$, $V_\kappa$ is $C^1$, positive definite and $\mathbf r(\kappa)$-homogeneous of degree $2+\kappa$, and $\omega^H_\kappa$ is globally asymptotically stabilizing.
• Lemma 31 (p. 1038): on the shell $B^\kappa_{1-m,1+m}$, $|x_j|$ and $|v_j|$ are bounded uniformly in $\kappa$.
• Lemma 32 (p. 1039): on that shell, $|\omega^H_\kappa-\omega^H_0|$ and $|V_\kappa-V_0|$ are at most a constant times $|\kappa|^{\min(1,r_n)}$.
• Proposition 33 (p. 1040): for every $m$ there is $\kappa_0(m)>0$ below which the closed loop is fixed-time stable, with an explicit settling-time bound that coincides with (52) for $m\le(\sqrt{17}-3)/4$.
• Theorem 28 (pp. 1036–1037): with an input gain $b(t)\in[\underline b,\bar b]$ and the feedback $\omega^H_{\kappa(x)}(x)/\underline b$, the closed loop is globally fixed-time stable with settling time at most $T^\ast(m,\kappa_0)$.

Significance

The result gives a static, continuous state feedback for the chain of integrators with an explicit settling-time bound. It is robust to a bounded uncertain input gain, and the rescaled controller meets any prescribed deadline. Unlike time-varying designs, the gains stay bounded, which is what the paper's ISS analysis in §4.3 builds on. The constants in (52) are explicit in terms of $C$ and the radii $r(m,\pm\kappa_0)$, so the rescaling factor $\lambda$ is computable.

The results are proved on paper; no machine-checked proof is known. A formalization would check the parameter bookkeeping of the construction: index shifts, exponents, the three-phase settling-time estimate, and the interplay of two different dilations. It would also produce reusable definitions of Carathéodory solutions and of finite-, fixed- and prescribed-time stability, which the platform does not yet have.

Difficulty

The obvious argument uses the Lyapunov function $V_{\kappa(x)}$ for the varying-degree controller. That fails: $\kappa$ depends on $x$, so $V_{\kappa(x)}(x)$ acquires a term from the derivative of $\kappa$. The proof instead handles three regions separately, with $V_{\kappa_0}$ outside $B^0_{1+m}$, $V_0$ on the shell $B^0_{1-m,1+m}$, and $V_{-\kappa_0}$ inside $B^0_{1-m}$. On the shell the controller is a perturbation of the linear one, and bounding that perturbation needs uniform Hölder estimates in $\kappa$ (Lemmas 31–32). The closed loop is only continuous, so solutions need not be unique and every stability claim is about all solutions. Proposition 24 itself is a recursive gain construction whose constants must be uniform in $\kappa$.

Formalization scope

States are EuclideanSpace ℝ (Fin n); the paper's index $j\in\{1,\dots,n\}$ is j.val + 1. Solutions are Carathéodory solutions on $[0,\infty)$ in integral form, with integrability stated. Every stability property quantifies over all solutions, and existence of a solution from each initial state is part of Lyapunov stability. $\lceil y\rfloor^a$ is read as $\operatorname{sign}(y)|y|^a$; the paper never defines it. $\dot V$ is the Fréchet derivative applied to the vector field. $r(m,\kappa_0)$ and $r(m,-\kappa_0)$ are the supremum and infimum of the admissible radii.

Hypotheses and readings that differ from the page:

• The gains and $C$ in Theorems 28 and 30 and Proposition 33 are data satisfying (36), not existentially chosen. An unconstrained $\exists C$ would make (52) false, and Proposition 24 shows (36) is satisfiable.
• $b$ is assumed measurable in Theorem 28.
• "Adapted" is the feedback divided by $\underline b$, as the page says.
• Corrected printed slips:
  • (51) lacks $e_n$.
  • Theorem 30 writes $\kappa_0\in(0,1/n)$; Theorem 28's $(0,\tfrac1{2n})$ is used.
  • Proposition 33 prints $\kappa_0(m)\in[-\tfrac1{2n},-\tfrac1{2n}]$; the value is positive and at most $\tfrac1{2n}$.
  • (37) prints $\beta_{i-1}$ for $\beta_{j-1}$.
  • The proof of Lemma 32 prints the exponent of (33) as $(r_j+1)/(r_j\beta_{j-1})$; (33) is used.
• Lemma 32's maxima are read pointwise, with $r_n=r_n(\kappa)$.
• In Proposition 33 the middle term $-2\ln(2m)$ of (52) is replaced by $\max(-2\ln(2m),\,2\ln\frac{1+m}{1-m})$: the page's crossing-time estimate $-2\ln(2m)/C$ is justified only for $m\le(\sqrt{17}-3)/4$, where the two bounds coincide.
• "Explicit" constants are stated as existing.

A formalization in which (36) is dropped, or $C$ is chosen freely, or a trajectory is only required to exist, would be trivial or false. Any trivializing reading of this kind is ruled out: stability is required of every solution, and $C$ is tied to (36).

Needed infrastructure: signed powers and their Hölder estimates (42), differentiability of $V_\kappa$, weighted homogeneity, Carathéodory existence for continuous right-hand sides, and comparison lemmas for $\dot V\le-cV^{1+\alpha}$. The stability definitions and the comparison lemmas are reusable beyond this mission. Contributions of any of these are welcome.

Selected references

• Y. Chitour, R. Ushirobira, H. Bouhemou, Stabilization for a Perturbed Chain of Integrators in Prescribed Time, SIAM J. Control Optim. 58(2), 1022–1048, 2020. https://doi.org/10.1137/19M1285937
• Y. Hong, Finite-time stabilization and stabilizability of a class of controllable systems, Systems Control Lett. 46, 231–236, 2002. https://doi.org/10.1016/S0167-6911(02)00119-6
• M. Harmouche, S. Laghrouche, Y. Chitour, M. Hamerlain, Stabilisation of perturbed chains of integrators using Lyapunov-based homogeneous controllers, Int. J. Control 90, 2631–2640, 2017. https://doi.org/10.1080/00207179.2016.1262967
• F. Lopez-Ramirez, D. Efimov, A. Polyakov, W. Perruquetti, Fixed-time output stabilization and fixed-time estimation of a chain of integrators, Int. J. Robust Nonlinear Control 28, 4647–4665, 2018. https://doi.org/10.1002/rnc.4275
• Y. Song, Y. Wang, J. Holloway, M. Krstić, Time-varying feedback for regulation of normal-form nonlinear systems in prescribed finite time, Automatica 83, 243–251, 2017. https://doi.org/10.1016/j.automatica.2017.06.008
• S. P. Bhat, D. S. Bernstein, Geometric homogeneity with applications to finite-time stability, Math. Control Signals Systems 17, 101–127, 2005. https://doi.org/10.1007/s00498-005-0151-x

Motivation

Many engineered systems switch between a finite number of operating modes at random times: a power grid after a line failure, a networked controller whose links drop, a manufacturing plant whose machines break down and are repaired. A standard model for such systems is a hybrid stochastic differential equation, also called an SDE with Markovian switching: the state follows an Itô equation whose coefficients depend on a mode that evolves as a continuous-time Markov chain. The monograph of Mao and Yuan (Stochastic Differential Equations with Markovian Switching, 2006) develops the stability theory of these equations.

A controller that stabilizes such a system usually needs the current state. In practice the state is sampled: it is observed at times $0,\tau,2\tau,\dots$ and the control is held between observations. Mao (Automatica 49, 2013) showed that, under a global Lipschitz condition on the drift and diffusion, a feedback control based on discrete-time observations makes a hybrid SDE mean-square exponentially stable when $\tau$ is small enough. You, Liu, Lu, Mao and Qiu (SIAM J. Control Optim. 53(2), 2015) replaced that condition by local Lipschitz continuity plus linear growth, gave an explicit bound (3.5) on the admissible observation interval, and proved $H_\infty$-stability, asymptotic stability, and, in Section 4, exponential stability in mean square and almost surely with an explicit rate. This mission formalizes that exponential stability result, Theorem 4.2, and the steps of its proof.

Setting

Let $(\Omega,\mathcal F,\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a probability space with a filtration satisfying the usual conditions (increasing, right-continuous, $\mathcal F_0$ contains the null sets). On it live an $m$-dimensional $\{\mathcal F_t\}$-Brownian motion $w$ and a right-continuous $\{\mathcal F_t\}$-Markov chain $r$ on $S=\{1,\dots,N\}$ with generator $\Gamma=(\gamma_{ij})$ ($\gamma_{ij}\ge0$ for $i\ne j$, zero row sums), independent of $w$. Fix $\tau>0$ and the sampling time $\delta_t=[t/\tau]\tau$. The controlled system is

$$dx(t)=\big(f(x(t),r(t),t)+u(x(\delta_t),r(t),t)\big)dt+g(x(t),r(t),t)\,dw(t),\qquad x(0)=x_0,\ r(0)=r_0,\tag{2.1}$$

with $f,u:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^n$ and $g:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^{n\times m}$.

The hypotheses are:

• Assumption 2.1: $f,g$ locally Lipschitz in $x$, and $|f(x,i,t)|\le K_1|x|$, $|g(x,i,t)|\le K_2|x|$ ($|g|$ the trace norm).
• Assumption 2.2: $|u(x,i,t)-u(y,i,t)|\le K_3|x-y|$ and $u(0,i,t)=0$.
• Assumption 3.1: there are $U\in C^{2,1}(\mathbb R^n\times S\times\mathbb R_+;\mathbb R_+)$ and $\lambda_1,\lambda_2>0$ with $\mathcal LU(x,i,t)+\lambda_1|U_x(x,i,t)|^2\le-\lambda_2|x|^2$, where

$$\mathcal LU=U_t+U_x[f+u]+\tfrac12\operatorname{trace}[g^TU_{xx}g]+\sum_j\gamma_{ij}U(x,j,t).$$

• Assumption 4.1: $c_1|x|^2\le U(x,i,t)\le c_2|x|^2$ with $c_1,c_2>0$.
• Condition (3.5): $\lambda_2>\frac{\tau K_3^2}{\lambda_1}\big[2\tau(K_1^2+2K_3^2)+K_2^2\big]$ and $\tau\le\frac1{4K_3}$.

Put $\theta=K_3^2/\lambda_1$, $\lambda=\lambda_2-\theta\tau[2\tau(K_1^2+2K_3^2)+K_2^2]$ (positive by (3.5)), and

$$H_1=\theta\tau\big(2\tau(K_1^2+2K_3^2)+K_2^2\big)+\frac{24\theta\tau^4K_3^4}{1-6\tau^2K_3^2},\qquad H_2=\frac{12\theta\tau^2K_3^2(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}.$$

In Lean these are Assumption21, Assumption22, C21, LU, Assumption31, Assumption41, Condition35, theta, lam, H1, H2, rateEquationLHS; the basis is HybridSetup, the Itô integral IsItoIntegral, the sampling time delta, solutions SolvesSampledHybridSDE, and the functional (4.7) Vbar, all in the namespace You2015.Expo.

Formalization targets

Goal: Theorem 4.2 (exponential stability)

Under the hypotheses above, the equation

$$2\tau\gamma e^{2\tau\gamma}(H_1+\tau H_2)+\gamma c_2=\lambda\tag{4.4}$$

has a unique root $\gamma>0$, and every solution of (2.1) satisfies

$$\limsup_{t\to\infty}\frac1t\log\big(\mathbb E|x(t)|^2\big)\le-\gamma,\qquad\limsup_{t\to\infty}\frac1t\log|x(t)|\le-\frac\gamma2\quad\text{a.s.}$$

for all $x_0\in\mathbb R^n$, $r_0\in S$.

Milestones, in the order the proof uses them

1. (3.15) $\mathbb E|x(t)-x(\delta_t)|^2\le2\mathbb E\int_{\delta_t}^t[\tau|f+u(x(\delta_s),\cdot)|^2+|g|^2]ds$.
2. Theorem 3.2 ($H_\infty$-stability): $\int_0^\infty\mathbb E|x(s)|^2ds<\infty$.
3. (3.21) $\mathbb E|x(s)-x(\delta_s)|^2\le\frac{3(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}\int_{\delta_s}^s\mathbb E|x(z)|^2dz+\frac{6\tau^2K_3^2}{1-6\tau^2K_3^2}\mathbb E|x(s)|^2$.
4. (4.11) $\mathbb E\bar V(\hat x_z,\hat r_z,z)\le(H_1+\tau H_2)\int_{z-2\tau}^z\mathbb E|x(y)|^2dy$ for $z\ge2\tau$.
5. (4.14) $c_1e^{\gamma t}\mathbb E|x(t)|^2\le C$ for $t\ge2\tau$.
6. (4.14) $\Rightarrow$ (4.3), the mean-square-to-almost-sure transfer cited from Mao–Yuan [23, Theorem 8.8].

Significance

The result. Theorem 4.2 gives a quantitative guarantee: a controller that samples the state every $\tau$ units makes the switching system decay exponentially, with a rate $\gamma$ computable from the constants of the assumptions. Asymptotic stability (Section 3 of the paper) says nothing about how fast trajectories settle; the rate is what a designer trades against the sampling cost when choosing $\tau$. The almost sure statement concerns individual trajectories, which is what an operator observes.

Formalizing it. The results are proved in the paper; none of them is machine-checked. Mathlib has real Brownian motion but no Itô integral, no stochastic differential equations and no continuous-time Markov chains. The mission therefore also produces a definition layer: a filtration under the usual conditions, a multidimensional $\{\mathcal F_t\}$-Brownian motion, an $\{\mathcal F_t\}$-Markov chain with a given generator, the $L^2$ Itô integral of vector-valued integrands, and the solution notion of an SDE with Markovian switching and a sampled-state delay. A related but different layer exists on Prove2Me for Ethier–Kurtz (EthierKurtz_IsStandardBrownian, EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE); it has no mode switching and no sampled state, so it cannot express (2.1). Formalization also checks the constants: it found that the printed $H_1$ in (4.5) disagrees with the paper's own derivation (see below).

Difficulty

Equation (2.1) is a stochastic differential delay equation whose delay $t-\delta_t$ is bounded but jumps at every observation time, so the delay-equation stability theorems that require a differentiable delay with derivative below one (Mao–Yuan, p. 285) do not apply. A Lyapunov function of the current state alone leaves the term $U_x[u(x(t))-u(x(\delta_t))]$, which has no sign and depends on the path over a whole observation interval. An exponential rate requires controlling this delay term with an exponential weight, and the weight inflates the delay contribution by a factor $e^{2\tau\gamma}$; the rate equation (4.4) records exactly this balance. The almost sure part does not follow from the mean-square part by Chebyshev's inequality at fixed times alone: a pathwise bound needs control of the supremum of $|x|$ over each unit interval, which involves the martingale part of the solution.

Formalization scope

Conventions committed to in Lean:

• The state space is EuclideanSpace ℝ (Fin n), so $|x|$ is the Euclidean norm; the explicit constants in (3.5), (3.21), (4.5) depend on it. The diffusion $g$ is given by its $m$ columns and $|g|^2=\sum_k|g_k|^2$ (trace norm). Modes are Fin N (0-based). Time is ℝ≥0; time integrals are over subsets of $\mathbb R$ at s.toNNReal.
• Every expectation of a nonnegative quantity ($\mathbb E|x|^2$, $\mathbb E\bar V$) and every time integral of one is a lower Lebesgue integral in $[0,\infty]$, so a non-integrable process cannot produce a junk value $0$.
• Logarithms. The paper's $\log$ takes the value $-\infty$ at $0$. For a finite $a(t)\ge0$, $\limsup_{t\to\infty}\frac1t\log a(t)\le-\gamma$ is stated in the equivalent form "for every $\gamma'<\gamma$, eventually $a(t)\le e^{-\gamma't}$". Lean's Real.log 0 = 0 never enters. In (4.3) the almost-sure quantifier is outside the quantifier over $\gamma'$.
• Correction of (4.5). The page prints the last term of $H_1$ as $24\tau^3K_3^4/(1-6\tau^2K_3^2)$. Substituting (3.21) into (4.9), as the proof does, gives $24\theta\tau^4K_3^4/(1-6\tau^2K_3^2)$ (the same computation reproduces the printed $H_2$). The mission uses the corrected $H_1$ in the goal, (4.11) and (4.14). With the printed value the claimed rate could exceed what the proof yields whenever $\theta\tau>1$.
• "The unique root" is a conjunct of the goal ($\exists!\,\gamma>0$); the stability conclusions are stated for every positive root. "(so $\lambda>0$)" is a consequence of (3.5), not a hypothesis. (4.4) is kept as an equality.
• "The solution of (2.1)" is read as every process satisfying the solution definition: progressively measurable, almost surely continuous paths, $\mathbb E|x(t)|^2<\infty$ for each $t$, and for each $t$, almost surely, the integral equation with Itô integrals in the $L^2$ sense. Existence and uniqueness (cited from Mao–Yuan on p. 908) are not asserted.
• "An $m$-dimensional Brownian motion" and "a Markov chain with generator $\Gamma$" are read in the Mao–Yuan framework the paper cites: an $\{\mathcal F_t\}$-Brownian motion with independent coordinates and increments independent of the past, and an $\{\mathcal F_t\}$-Markov chain with transition matrix $e^{t\Gamma}$. The usual conditions are kept as hypotheses.
• "Locally Lipschitz" is uniform in the mode and time on each ball. $C^{2,1}$ carries its derivatives $U_t,U_x,U_{xx}$ as witnesses tied to $U$ by derivative relations and joint continuity.
• "$\tau>0$ sufficiently small for (3.5)" means every $\tau>0$ satisfying both inequalities of (3.5). $U,\lambda_1,\lambda_2,c_1,c_2,\tau$ are data. The constant $C$ of (4.14) is chosen after $x_0$, $r_0$, the solution and $\gamma$, and before $t$.
• (3.15), (3.21) and the transfer (4.14) $\Rightarrow$ (4.3) are stated under fewer hypotheses than the surrounding proof has (Assumptions 2.1, 2.2, $\tau>0$, and for (3.21) $\tau\le1/(4K_3)$), because their derivations use no more. $\bar V$ of (4.7) is used only for $z\ge2\tau$, where no extension of the solution to negative times is needed. Other misprints on the page ($g(x,i,s)=f(x,i,0)$ on p. 909, $V(\hat x_0,\hat r_0,t)$ for $V(\hat x_0,\hat r_0,0)$ on p. 918, the swapped $\vee,\wedge$ on p. 907) are not formalized.

A trivializing formalization is ruled out: the expectations are not Bochner integrals, $\log 0$ is never evaluated, the goal asserts that the rate equation has exactly one positive root (so the stability clauses are not vacuous), the solution notion admits the true solution and requires path continuity, and the derivative witnesses of $U$ are tied to $U$. A sorry-free local check confirms that Assumptions 2.1, 2.2, 4.1, condition (3.5) and $\lambda>0$ hold for $n=m=N=1$, $f=g=0$, $u(x)=-x$, $U=|x|^2$, $K_1=K_2=K_3=1$, $\lambda_1=1/4$, $\lambda_2=1$, $c_1=c_2=1$, $\tau=1/10$; for these data $\mathcal LU+\lambda_1|U_x|^2=-|x|^2$ by hand.

Welcome contributions: the Itô isometry and Itô's formula for the $L^2$ integral defined here, a generalized Itô formula for functions of a Markov-modulated Itô process, the Burkholder–Davis–Gundy inequality, and the Borel–Cantelli argument that turns mean-square exponential decay into almost sure decay. These are reusable far beyond this mission. Section 3 of the paper (asymptotic stability) is a separate mission of the same series.

Selected references

• S. You, W. Liu, J. Lu, X. Mao, Q. Qiu, Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations, SIAM J. Control Optim. 53(2), 905–925, 2015. https://doi.org/10.1137/140985779
• X. Mao, C. Yuan, Stochastic Differential Equations with Markovian Switching, Imperial College Press, 2006. https://doi.org/10.1142/p473
• X. Mao, Stabilization of continuous-time hybrid stochastic differential equations by discrete-time feedback control, Automatica 49(12), 3677–3681, 2013. https://doi.org/10.1016/j.automatica.2013.09.005

Motivation

Stochastic approximation is the family of recursive algorithms that locate a zero of a vector field $h$ from noisy evaluations of it. Temporal-difference learning, Q-learning, actor–critic methods and stochastic gradient descent are all instances. In practice these algorithms are often run with a constant or bounded, non-vanishing stepsize: the iterate keeps adapting to new data and never freezes, at the price of never converging exactly. The natural question for such a scheme is quantitative: how far from the target does the iterate stay in the long run, and how does that distance scale with the stepsize?

Borkar and Meyn (SIAM J. Control Optim. 38(2), 2000) answer both halves of the question under one set of hypotheses. First, stability of a "fluid" ODE obtained by scaling $h$ at infinity implies that the iterates have bounded second moments, with no a priori boundedness or projection assumption. Second, if the ODE $\dot x = h(x)$ has a globally exponentially stable equilibrium $x^*$, the asymptotic mean-square error is of the order of the largest stepsize. The first result replaced the usual stochastic-Lyapunov-function verification in reinforcement-learning applications (Section 3 of the paper). This mission formalizes the bounded-stepsize branch of the paper. A companion mission (… I: Stability and Almost-Sure Convergence under Tapering Stepsizes) covers the vanishing-stepsize branch.

Setting

Fix $d \ge 1$ and a Lipschitz vector field $h : \mathbb{R}^d \to \mathbb{R}^d$. The stochastic approximation recursion (1.1) is

$$X(n+1) = X(n) + a(n)\big[h(X(n)) + M(n+1)\big], \qquad n \ge 0,$$

with a deterministic step sequence $\{a(n)\}$ and a noise sequence $\{M(n)\}$ on a probability space $(\Omega, \mathcal F, \mathsf P)$. The associated ODE (1.2) is $\dot x = h(x)$.

• The scaled fields are $h_r(x) = r^{-1} h(rx)$. Assumption (A1) asks that $h$ be Lipschitz, that $h_r(x) \to h_\infty(x)$ for every $x$ as $r \to \infty$, and that the origin be an asymptotically stable equilibrium of the fluid ODE $\dot x = h_\infty(x)$.
• Let $\mathcal F_n = \sigma(X(0), \dots, X(n))$. Assumption (A2) asks that $\{M(n)\}$ be a martingale difference sequence, $\mathsf E[M(n+1) \mid \mathcal F_n] = 0$, with conditional second moments $\mathsf E[\|M(n+1)\|^2 \mid \mathcal F_n] \le C_0(1 + \|X(n)\|^2)$ for a constant $C_0$.
• Assumption (BS), bounded stepsizes: $0 < \underline\alpha \le a(n) \le \bar\alpha < 1$ for all $n$, with $\underline\alpha < \bar\alpha$.
• The error (2.2) is $e(n) = \|X(n) - x^*\|$.

An equilibrium $x^*$ of (1.2) is globally asymptotically stable if it is Lyapunov stable and attracts every solution. It is globally exponentially asymptotically stable if there are $b$ and $\delta > 0$ with $\|x(t) - x^*\| \le b\,e^{-\delta t}\|x(0) - x^*\|$ for every solution.

The proofs compare the iterates with ODE solutions on a time grid: $t(n) = \sum_{i<n} a(i)$, blocks $T(j) = t(m(j))$ of length about $T$, the interpolated path $\psi$ of the iterates, its rescaled version $\phi_j = \psi/r(j)$ with $r(j) = \max(1, \|X(m(j))\|)$, and the ODE solutions $\hat\psi$, $\hat\phi_j$ restarted at each block.

Formalization targets

Goal: Theorem 2.3(ii)

Under (A1), (A2) and (BS), if $x^*$ is a globally asymptotically and globally exponentially asymptotically stable equilibrium of (1.2), there are $\alpha^* > 0$ and $b_2 < \infty$ such that for all $0 < \bar\alpha \le \alpha^*$ and every initial condition $X(0)$,

$$\limsup_{n \to \infty} \mathsf E\big[e(n)^2\big] \le b_2\, \bar\alpha .$$

The constant $b_2$ is uniform in the stepsizes and in $X(0)$. No rate constant is fixed: only the linear dependence on $\bar\alpha$ is asserted.

Milestones

1. Lemma 4.7. For fixed $T > 0$ there is $C_2$, independent of the stepsizes, with $\mathsf E[\|\phi_j(t) - \hat\phi_j(t)\|^2 \mid \mathcal F_{m(j)}] \le C_2\bar\alpha$ and $\mathsf E[\|\phi_j(t)\|^2 \mid \mathcal F_{m(j)}] \le C_2$ on every block.
2. Theorem 2.1(ii). There are $\alpha^* > 0$ and $C_1$ with $\limsup_n \mathsf E\|X(n)\|^2 \le C_1$ whenever $\bar\alpha < \alpha^*$.
3. Lemma 4.8. For $\bar\alpha \le \alpha^*$, $\sup_{t \ge 0} \mathsf E\|\hat\psi(t) - \psi(t)\|^2 \le C_3 \bar\alpha$.

Significance

The result. Theorem 2.1(ii) says that a stability property of a deterministic ODE at infinity controls a stochastic recursion in mean square, uniformly over initial conditions. Theorem 2.3(ii) turns this into an error bound: with a non-vanishing stepsize the iterate does not converge, but its mean-square distance from $x^*$ is eventually $O(\bar\alpha)$. This is the quantitative justification for constant-stepsize stochastic approximation in reinforcement learning and adaptive control, and it is the starting point of the trade-off between bias (small stepsize) and speed (large stepsize) discussed in Section 2.2 of the paper.

Formalizing it. The results are proved in the paper, partly by sketch: Lemma 4.8's proof refers to "familiar arguments using the Bellman–Gronwall lemma", and the paper writes several bounds as $O(\bar\alpha)$. A formal proof makes every constant and its dependence explicit, which the paper's quantifier order leaves partly implicit (see the scope section). No machine-checked proof of these results, or of any stochastic-approximation stability theorem in this generality, is known to exist.

Difficulty

The natural first argument, that the iterates track the ODE and the ODE converges, needs the iterates to be bounded. Bounded iterates are exactly what is being proved, so the argument is circular. The paper breaks the circularity by rescaling: on each block the iterate is divided by $r(j)$, so that on large scales it tracks the fluid ODE, whose stability contracts the norm by a fixed factor per block. Making this work in mean square requires conditional second-moment estimates that are uniform in the stepsize and the scale (Lemma 4.7). A second difficulty is that the stepsize does not vanish: the tracking error per block does not go to zero, and the goal's content is precisely that it is of order $\bar\alpha$ with a constant that does not depend on $\bar\alpha$.

Formalization scope

• The state space is EuclideanSpace ℝ (Fin d). ODE solutions are forward solutions: continuous on $[0,\infty)$ with right derivatives. Stability notions are the standard ones, with exponential stability in the form the proof of Theorem 2.3(ii) uses.
• The filtration is the natural filtration of the iterates. (A2) includes integrability of $M(n+1)$ and $\|M(n+1)\|^2$ so that the conditional expectations are meaningful. Each theorem quantifies over every probability space, every measurable process satisfying (1.1) and (A2), and every deterministic $X(0)$.
• Second moments, suprema and $\limsup$ are computed in $[0,\infty]$, so a bound is a genuine finiteness claim.
• Constant placement. $\alpha^*$, $C_1$ and $b_2$ depend only on $h$, $h_\infty$, $C_0$ (and $x^*$). $C_2$ depends in addition on $T$, and $C_3$ on $T$ and $X(0)$. None depends on the stepsizes. Theorem 2.3's page text puts $b_2$ after $\alpha$. Read literally, that would allow $b_2 = C_1/\bar\alpha$ and make the goal a restatement of Theorem 2.1(ii). The formal goal fixes $b_2$ before the stepsizes and the initial condition, as the proof ($16C_3\bar\alpha$) gives. $\alpha^*$ is existential in Theorem 2.3(ii) and Lemma 4.8 rather than tied to Theorem 2.1(ii)'s witness.
• The proof objects $\hat\psi$, $\hat\phi_j$ are characterized by predicates (initial value, continuity, ODE on the block). Lemmas 4.7 and 4.8 hold for every function satisfying them.
• Not included: Theorem 2.3(i) (its proof chooses a radius depending on $\bar\alpha$), Theorem 2.4 and the Markov-chain results of Section 4.3, and the asynchronous extension (Theorem 2.5). The deterministic ODE lemmas 4.1–4.4 belong to the companion mission.

Useful infrastructure, reusable beyond this mission: Bellman–Gronwall inequalities in discrete time (Lemma 4.3 of the paper), stability of scaled ODEs, and conditional second-moment estimates for martingale-difference-driven recursions. Contributions of any of these as separate lemmas are welcome.

Selected references

• V. S. Borkar and S. P. Meyn, The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning, SIAM J. Control Optim. 38(2):447–469, 2000. https://doi.org/10.1137/S0363012997331639
• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999. https://doi.org/10.1007/BFb0096509
• H. J. Kushner and G. G. Yin, Stochastic Approximation and Recursive Algorithms and Applications, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97441