refactor(analysis/calculus/times_cont_diff): massive refactor

[sgouezel]

There are three serious problems with the current implementation of C^n functions in mathlib:

• Being C^n in a domain is defined by requiring that some choice of the iterated derivative (given by iterated_fderiv) is continuous up to n. In a domain where the derivative is not unique, this creates problems (for instance, the sum of two C^n functions might not be C^n). This means that the notion is well behaved only in sets with unique derivatives. As a consequence, further files using this API spend a lot of time checking the unique derivative property, while this could be avoided with a more clever choice of definition.
• The n-th iterated derivative is defined currently as the n-1-th derivative of the derivative. Hence, it is a function in E -> (E -> (E -> .... (E -> F))...), which is pretty much unusable from a practical point of view.
• Defining the n-th derivative as the n-1-th derivative of the derivative is a definition by induction, but generalizing the target space: to define the n-th derivative of a function from E to F, one needs to know how to define the n-1-th derivative of a function from E to E -> F. Such an inductive definition only makes sense if the spaces F and E -> F are in the same universe, i.e., if E and F are in the same universe. This is the choice that is made currently, preventing universe polymorphism.

This PR solves these three issues, essentially by rewriting the file analysis/calculus/times_cont_diff_on from scratch.

• Being C^n on a domain is now defined as the existence of a sequence of derivatives with the right properties. Being on a domain with unique derivatives becomes irrelevant for most statements.
• The n-th derivative is now defined as a multilinear map, by adding suitable currification steps in the inductive definition.
• We define now the n-th derivative as the derivative of the n-1-th derivative. This avoids universe issues, at the cost of having somewhat more complicated proofs in some places (as inductive proofs are not really usable any more). In fact, it turned out to be not so bad. The only tricky place is the proof that the composition of C^n maps is C^n, where the inductive proof is really the good one. In the PR, I do the induction when all spaces are in the same universe, and then I use some lifting trick to generalize it to the general situation.

TL;DR The old file is bad. The new file is much better.

[kim-em]

Looks fantastic (I only attempted to read the comments and statements, none of the code.)

[robertylewis]

I can't review the content here, but I feel uncomfortable seeing something titled "massive refactor" sitting for over a week! @sgouezel @urkud is this ready to go, or are we waiting on comments from someone else?

[kim-em]

I understand the mathematical issues and this seems a good resolution of the previous problem. I never attempted to read the actual proofs, but the documentation and statements are great, and I'm happy to trust @sgouezel's judgement constructing nice enough proofs...

[kim-em]

I think we should merge now.