The flow of ODEs: formalization of variational equation and Poincaré map (Q1722644): Difference between revisions

@@ Property / describes a project that uses @@
+Transfer
@@ Property / describes a project that uses: Transfer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lifting
@@ Property / describes a project that uses: Lifting / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Ergodic theory
@@ Property / describes a project that uses: Ergodic theory / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lp spaces
@@ Property / describes a project that uses: Lp spaces / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Ordinary Differential Equations
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+RODES
@@ Property / describes a project that uses: RODES / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-018-9449-5
+Normal rank
@@ Property / OpenAlex ID @@
+W2793741686
@@ Property / OpenAlex ID: W2793741686 / rank @@
+Normal rank
@@ Property / cites work @@
+Wave equation numerical resolution: a comprehensive mechanized proof of a C program
+Normal rank
@@ Property / cites work @@
+Coquelicot: a user-friendly library of real analysis for Coq
+Normal rank
@@ Property / cites work @@
+Formalization of real analysis: a survey of proof assistants and libraries
+Normal rank
@@ Property / cites work @@
+Mechanizing Nonstandard Real Analysis
@@ Property / cites work: Mechanizing Nonstandard Real Analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+The HOL Light theory of Euclidean space
@@ Property / cites work: The HOL Light theory of Euclidean space / rank @@
+Normal rank
@@ Property / cites work @@
+Q2885005
@@ Property / cites work: Q2885005 / rank @@
+Normal rank
@@ Property / cites work @@
+Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+The Flow of ODEs
@@ Property / cites work: The Flow of ODEs / rank @@
+Normal rank
@@ Property / cites work @@
+A formalization of metric spaces in HOL Light
@@ Property / cites work: A formalization of metric spaces in HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+The Picard Algorithm for Ordinary Differential Equations in Coq
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q2706801
@@ Property / cites work: Q2706801 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4226356
@@ Property / cites work: Q4226356 / rank @@
+Normal rank
@@ Property / cites work @@
+A rigorous ODE solver and Smale's 14th problem
@@ Property / cites work: A rigorous ODE solver and Smale's 14th problem / rank @@
+Normal rank