Rigorous Computational ODEs Formalization

Stream: mathlib4

[Fengyang Wang]

Hi everyone. I've been working on formalizing some analysis results for ODEs. The main result is the Radii Polynomial Theorem. The equation/theorem numbers in the comments are not very helpful, as they are based on a textbook that's still in manuscript, which I'm not authorized to make public. Please refer to the leanblueprint page for the informal statements and proofs.

However, I'd love to have technical feedback on the way I coded the theorems up. If you are familiar with Mathlib and willing to kindly waste your leisure time on my sloppy code, please let me know your thoughts on the code's structure.

The leanblueprint repository is here. Readme contains the directory structure. The main theorem is formalized in RadiiPolyGeneral.lean under the folder RadiiPolynomial.