Email Gateway (Aug 18 2022 at 20:04): Email Gateway (Aug 18 2022 at 20:04):From: Tobias Nipkow <nipkow@in.tum.de>
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.
http://afp.sourceforge.net/devel-entries/Ordinary_Differential_Equations.shtml
(Currently only in the development version)
Last updated: Nov 21 2024 at 12:39 UTC