Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Ordinary Differential Equations


view this post on Zulip 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: Mar 29 2024 at 04:18 UTC