The flow of ODEs

Abstract

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 and we prove advanced properties of the flow, most notably, differentiable dependence on initial conditions via the variational equation and a rigorous numerical algorithm to solve it.