Title: |
Ordinary Differential Equations |
Authors:
|
Fabian Immler and
Johannes Hölzl
|
Submission date: |
2012-04-26 |
Abstract: |
Session HOL-ODE 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-Refinement:
Intermediate session combining \texttt{HOL-ODE} and Lammich's (automatic) refinement framework.
- 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_Approximation, 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{http://isa-afp.org/entries/Ordinary_Differential_Equations.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Affine_Arithmetic, Collections, Deriving, List-Index, Show, Triangle |
Used by: |
Akra_Bazzi, Bertrands_Postulate, Differential_Dynamic_Logic |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|