| Home |
| About |
| Submission Guidelines |
| Updating entries |
| Search |
| Index |
| Download |
project summary
Ordinary Differential Equations
| Title: | Ordinary Differential Equations |
| Author: | Fabian Immler and Johannes Hölzl |
| Submission date: | 2012-04-26 |
| Abstract: | 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. |
| 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{http://afp.sf.net/entries/Ordinary_Differential_Equations},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|