Integral Curves and Flows on Banach Manifolds in Lean

Weichen Winston Yin, Yury Kudryashov

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 properti…