Abstract
Session Ordinary-Differential-Equations 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-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_C0, Lorenz_C1: Verified algorithms for checking C1-information according to Tucker's proof, computation of C0-information.
License
History
- September 20, 2017
- 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.
- August 3, 2016
- numerical algorithms for reachability analysis (using second-order Runge-Kutta methods, splitting, and reduction) implemented using Lammich's framework for automatic refinement
- April 14, 2016
- added flow and variational equation
- February 13, 2014
- added an implementation of the Euler method based on affine arithmetic
Topics
Session Ordinary_Differential_Equations
- ODE_Auxiliarities
- MVT_Ex
- Vector_Derivative_On
- Interval_Integral_HK
- Gronwall
- Initial_Value_Problem
- Picard_Lindeloef_Qualitative
- Bounded_Linear_Operator
- Multivariate_Taylor
- Flow
- Upper_Lower_Solution
- Poincare_Map
- Reachability_Analysis
- Flow_Congs
- Cones
- Linear_ODE
- ODE_Analysis
Session HOL-ODE-Numerics
- GenCF_No_Comp
- Refine_Dflt_No_Comp
- Autoref_Misc
- Weak_Set
- Enclosure_Operations
- Refine_Vector_List
- Transfer_Analysis
- Transfer_ODE
- Transfer_Euclidean_Space_Vector
- Refine_Hyperplane
- Refine_Unions
- Refine_Intersection
- Refine_Invar
- Refine_Interval
- Refine_Info
- Abstract_Rigorous_Numerics
- Refine_Rigorous_Numerics
- Refine_Rigorous_Numerics_Aform
- Concrete_Rigorous_Numerics
- Refine_String
- Refine_Folds
- One_Step_Method
- Runge_Kutta
- Abstract_Reachability_Analysis
- Concrete_Reachability_Analysis
- Refine_Parallel
- Refine_Default
- Refine_Phantom
- Refine_ScaleR2
- Abstract_Reachability_Analysis_C1
- Concrete_Reachability_Analysis_C1
- Refine_Reachability_Analysis
- Refine_Reachability_Analysis_C1
- Init_ODE_Solver
- Example_Utilities
- ODE_Numerics