[isabelle] New AFP entry: Ordinary Differential Equations

Ordinary Differential Equations
Fabian Immler and Johannes Hölzl

We formalize initial value problems (IVPs) of ODEs and prove the existence of a
unique solution, i.e. the Picard-Lindelöf theorem. We introduce general one-step
methods for numerical approximation of the solution and provide an analysis
regarding the local and global error of one-step methods. We give an executable
specification of the Euler method to approximate the solution of IVPs and prove
an explicit bound for the global error. We use arbitrary-precision
floating-point numbers and also handle rounding errors when we truncate the
numbers for efficiency reasons.

(Currently only in the development version)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.