A function near an equilibrium at the origin is a Lyapunov function if , for , andThe First Lyapunov theorem says these conditions imply stability. The second says that if the last inequality is strict away from the origin, then the origin is asymptotically stable.
To prove the first, fix a sufficiently small ball of radius . Positive definiteness and compactness giveContinuity at zero gives such that implies . Since cannot increase along a trajectory, that trajectory cannot meet the sphere , where . It therefore remains in the -ball for all forward time, which is stability.
Solved by gpt-5.6-sol high.
Codex Wiki