Picard-Lindelof

Stream: maths

[Yury G. Kudryashov]

branch#picard-lindelof has a proof of the Picard-Lindelöf/Cauchy-Lipschitz theorem with one sorry about ∫ x in interval a..b, |x-a|^n and absolutely no documentation.
It also includes a few refactors that I'm going to PR during the week-end.

The main result is that an ODE defined here has a solution in this sense.

Of course, a lot of things should be added to this file:

• a version that does not use the auxiliary structure;
• local version(s) that use filter.eventually instead of specific intervals here and there;
• dependence on parameters / smoothness of the solution;

Probably, not all of this should go into the first PR.

[Patrick Massot]

Amazing!

[Kevin Buzzard]

This ("do initial value problems have unique solutions?") was one of the questions that the applied guy who teaches the introductory module at Imperial with me asked the students when he was in charge of them

[Yury G. Kudryashov]

We already have uniqueness in mathlib, see docs#ODE_solution_unique

[Yury G. Kudryashov]

Ready for review: #9791. Of course, we'll need quite a few more theorems to make it really useful (more smoothness, dependency on the parameters and the initial condition, ability to extend the solution till we hit the boundary etc).