Papers With

← All papers
First page of A Priori Integral Persistent Excitation in Conservative Polynomial ODEs with Higher-Order Interactions

A Priori Integral Persistent Excitation in Conservative Polynomial ODEs with Higher-Order Interactions

Aleksandr Semenov, Alexander Fradkov

math.OC Jun 30, 2026 · v1
formalization analysis
Read PDF arXiv abstract Code
TL;DR
The proof of the main theorem on absence of trajectory sticking to hyperplanes and affine integral persistent excitation is formalized in Lean.
Abstract
The paper proposes an approach for verifying integral persistent excitation, which is important in problems of parameter identification and adaptive control in nonlinear dynamical systems. The approach works for conservative polynomial ODEs a priori without knowledge of the parameters. Rigorous proofs of the corresponding theorems are provided. An example of a nonlinear dynamical system with higher-order interactions and the application of the proposed method to it are analyzed. The proof of the main result is formalized in the Lean formal verification language.
Problem

Verifying the persistent excitation condition for parameter identification and adaptive control is difficult, and a priori methods that work without knowing system parameters are poorly developed. The goal is to establish integral persistent excitation for conservative polynomial ODEs a priori.

Approach

An affine integral excitation condition is defined for measurable bounded trajectories and shown equivalent to trajectories not sticking to affine hyperplanes. Under compact invariance, an absolutely continuous invariant measure, and a nondegeneracy condition, the main theorem establishes that the fraction of time spent near any hyperplane tends to zero. The proof relies on the Birkhoff–Khinchin ergodic theorem and the Novikov–Yakovenko theorem, and is formalized in the Lean proof assistant.

Results

The main theorem yields affine integral persistent excitation for almost every trajectory. The method is applied to a reduced three-wave interaction model in R^6, demonstrating applicability to systems with higher-order interactions.