The flow of ODEs: formalization of variational equation and Poincaré map
type: Item
instance of: scholarly article
title: The flow of ODEs: formalization of variational equation and Poincaré map
zbMATH Open document ID: 1468.68325
author: Fabian Immler
author: Christoph Traut
published in: Journal of Automated Reasoning
publication date: 2019-02-18T00:00:00Z
Mathematics Subject Classification ID: 68V20
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 34A12
Mathematics Subject Classification ID: 34A26
Mathematics Subject Classification ID: 37C10
Mathematics Subject Classification ID: 65L05
Mathematics Subject Classification ID: 65P99
zbMATH DE Number: 7024457
zbMATH Keywords: Isabelle/HOL
zbMATH Keywords: ordinary differential equation
zbMATH Keywords: dynamical system
zbMATH Keywords: Poincaré map
describes a project that uses: HOL
describes a project that uses: Coq
describes a project that uses: Isabelle
describes a project that uses: Isabelle/HOL
describes a project that uses: Coquelicot
describes a project that uses: Transfer
describes a project that uses: Lifting
describes a project that uses: Ergodic theory
describes a project that uses: Lp spaces
describes a project that uses: Ordinary Differential Equations
describes a project that uses: Archive Formal Proofs
describes a project that uses: RODES
MaRDI profile type: Publication
full work available at URL: s10817-018-9449-5
OpenAlex ID: W2793741686
cites work: Wave equation numerical resolution: a comprehensive mechanized proof of a C program
cites work: Coquelicot: a user-friendly library of real analysis for Coq
cites work: Formalization of real analysis: a survey of proof assistants and libraries
cites work: Mechanizing Nonstandard Real Analysis
cites work: Theorem Proving in Higher Order Logics
cites work: The HOL Light theory of Euclidean space
cites work: Differential equations, dynamical systems, and an introduction to chaos
cites work: Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
cites work: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
cites work: Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
cites work: The Flow of ODEs
cites work: A formalization of metric spaces in HOL Light
cites work: The Picard Algorithm for Ordinary Differential Equations in Coq
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Q2706801
cites work: Q4226356
cites work: A rigorous ODE solver and Smale's 14th problem
DOI: 10.1007/S10817-018-9449-5
Recommended article: Path differentiability of ODE flows
Recommended article: Q4499818
Recommended article: Fine asymptotic expansion of the ODE's flow
Recommended article: Poincar normal forms for partial differential equations
Recommended article: Generalized flows and singular ODEs on differentiable manifolds
Recommended article: On the variational form of evolution equations
Recommended article: A flow-on-manifold formulation of differential-algebraic equations
Recommended article: Q3722860
Recommended article: Vector fields with distributions and invariants of ODEs
description: scientific article; zbMATH DE number 7024457