The Flow of ODEs: Formalization of Variational Equation and Poincaré Map

Formal analysis of ordinary differential equations (ODEs) and dynamical systems requires a solid formalization of the underlying theory. The formalization needs to be at the correct level of abstraction, in order to avoid drowning in tedious reasoning about technical details. The flow of an ODE, i.e., the solution depending on initial conditions, and a dedicated type of bounded linear functions yield suitable abstractions. The dedicated type integrates well with the type-class based analysis in Isabelle/HOL and we prove advanced properties of the flow, most notably, differentiable dependence on initial conditions via the variational equation. Moreover, we formalize the notion of first return or Poincaré map and prove its differentiability. We provide rigorous numerical algorithm to solve the variational equation and compute the Poincaré map.