Exponentially stable nonlinear systems have polynomial Lyapunov functions on bounded regions

This paper presents a proof that existence of a polyno-mial Lyapunov function is necessary and sufficient for exponential stability of sufficiently smooth nonlinear or-dinary differential equations on bounded sets. The main result implies that if there exists an n-times continuously differentiable Lyapunov function which proves exponen-tial stability on a bounded subset of Rn, then there exists a polynomial Lyapunov function which proves exponen-tial stability on the same region. Such a continuous Lya-punov function will exist if, for example, the right-hand side of the differential equation is polynomial or at least n-times continuously differentiable. Our investigation is motivated by the use of polynomial optimization algo-rithms to construct polynomial Lyapunov functions for systems of nonlinear ordinary differential equations.