Integral Curves and Flows on Banach Manifolds in Lean
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866912904180137984 |
|---|---|
| author | Yin, Weichen Winston Kudryashov, Yury |
| author_facet | Yin, Weichen Winston Kudryashov, Yury |
| contents | We present a formalisation of the existence and uniqueness theorems of integral curves of vector fields on Banach manifolds in the Lean theorem prover. First, we formalize properties of differential equations on Banach spaces (the Picard-Lindelöf theorem, the Grönwall inequality, and corollaries), and then transfer results to abstract Banach manifolds. Built upon the differential and integral calculus and Banach manifolds libraries in Mathlib, our work aims to lay the foundation for dynamical systems and differential geometry libraries that are general, robust, and friendly to classical mathematicians. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_13247 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Integral Curves and Flows on Banach Manifolds in Lean Yin, Weichen Winston Kudryashov, Yury Differential Geometry We present a formalisation of the existence and uniqueness theorems of integral curves of vector fields on Banach manifolds in the Lean theorem prover. First, we formalize properties of differential equations on Banach spaces (the Picard-Lindelöf theorem, the Grönwall inequality, and corollaries), and then transfer results to abstract Banach manifolds. Built upon the differential and integral calculus and Banach manifolds libraries in Mathlib, our work aims to lay the foundation for dynamical systems and differential geometry libraries that are general, robust, and friendly to classical mathematicians. |
| title | Integral Curves and Flows on Banach Manifolds in Lean |
| topic | Differential Geometry |
| url | https://arxiv.org/abs/2602.13247 |