巴拿格流形上的积分曲线与流动在 Lean 中的形式化
微分几何
2026-02-17 v1
摘要
我们在 Lean 定理证明器中对巴拿格流形上向量场积分曲线的存在性与唯一性定理进行形式化。首先，我们对巴拿格空间上的微分方程性质进行形式化（Picard-Lindel"of 定理、Gr"onwall 不等式及其推论），随后将结果迁移到抽象巴拿格流形。基于 Mathlib 中的微分积分计算与巴拿格流形库，本工作旨在为通用、稳健且亲和经典数学家的动力系统与微分几何库奠定基础。
引用
@article{arxiv.2602.13247,
title = {Integral Curves and Flows on Banach Manifolds in Lean},
author = {Weichen Winston Yin and Yury Kudryashov},
journal= {arXiv preprint arXiv:2602.13247},
year = {2026}
}