一个没有多项式李雅普诺夫函数的全局渐近稳定平面齐次多项式向量场
A Globally Asymptotically Stable Planar Homogeneous Polynomial Vector Field With No Polynomial Lyapunov Function
浏览论文内容
中文总结 AI 辅助
研究反驳了全局渐近稳定齐次多项式向量场必有齐次多项式李雅普诺夫函数的猜想，以具整数系数的平面齐次三次多项式向量场为反例，其无特定性质的齐次多项式李雅普诺夫函数，但有明确二次齐次李雅普诺夫函数，还给出机器验证形式化。
中文摘要 AI 辅助
我们反驳了每个全局渐近稳定的齐次多项式向量场都有一个齐次多项式李雅普诺夫函数的猜想。反例是一个具有整数系数的平面齐次三次多项式向量场。它没有具有非正李导数的正定齐次多项式，更强的是，甚至局部都没有实解析李雅普诺夫函数。然而，它有一个明确的二次齐次李雅普诺夫函数，径向无界，处处连续可微，且在原点外光滑。我们还提供了主要结果的机器验证的Lean 4形式化。
英文摘要
We disprove the conjecture that every globally asymptotically stable homogeneous polynomial vector field admits a homogeneous polynomial Lyapunov function. The counterexample is a planar homogeneous cubic polynomial vector field with integer coefficients. It admits no positive definite homogeneous polynomial with nonpositive Lie derivative and, more strongly, no real-analytic Lyapunov function even locally. Nevertheless, it has an explicit degree-two homogeneous Lyapunov function that is radially unbounded, continuously differentiable everywhere, and smooth away from the origin. We also provide a machine-checked Lean 4 formalization of the main result.
