# Ordinary Differential Equations

 Title: Ordinary Differential Equations Authors: Fabian Immler and Johannes Hölzl Submission date: 2012-04-26 Abstract: Session Ordinary-Differential-Equations formalizes ordinary differential equations (ODEs) and initial value problems. This work comprises proofs for local and global existence of unique solutions (Picard-Lindelöf theorem). Moreover, it contains a formalization of the (continuous or even differentiable) dependency of the flow on initial conditions as the flow of ODEs. Not in the generated document are the following sessions: HOL-ODE-Numerics: Rigorous numerical algorithms for computing enclosures of solutions based on Runge-Kutta methods and affine arithmetic. Reachability analysis with splitting and reduction at hyperplanes. HOL-ODE-Examples: Applications of the numerical algorithms to concrete systems of ODEs. Lorenz_C0, Lorenz_C1: Verified algorithms for checking C1-information according to Tucker's proof, computation of C0-information. Change history: [2014-02-13]: added an implementation of the Euler method based on affine arithmetic [2016-04-14]: added flow and variational equation [2016-08-03]: numerical algorithms for reachability analysis (using second-order Runge-Kutta methods, splitting, and reduction) implemented using Lammich's framework for automatic refinement [2017-09-20]: added Poincare map and propagation of variational equation in reachability analysis, verified algorithms for C1-information and computations for C0-information of the Lorenz attractor. BibTeX: @article{Ordinary_Differential_Equations-AFP, author = {Fabian Immler and Johannes Hölzl}, title = {Ordinary Differential Equations}, journal = {Archive of Formal Proofs}, month = apr, year = 2012, note = {\url{https://isa-afp.org/entries/Ordinary_Differential_Equations.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Affine_Arithmetic, List-Index, Triangle Used by: Differential_Dynamic_Logic, Hybrid_Systems_VCs