feat(analysis/calculus/deriv): one-dimensional derivatives

[gebner]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[jcommelin]

In this design, f' is a term of type F. I haven't thought hard about this, but I would expect a function f' : 𝕜 → F which you then might evaluate at a point x when needed. Does this make sense, or should this only come at a later step?

[gebner]

I haven't thought hard about this, but I would expect a function f' : 𝕜 → F which you then might evaluate at a point x when needed. Does this make sense, or should this only come at a later step?

It's the same approach as taken for the Fréchet derivative: we only define the derivative at a single point. If we need to state that a function f' : \bbk \to F is a derivative on a subset U : set \bbk, then this should be a separate definition on top.

[sgouezel]

Thanks a lot for this, this looks great to me! I can spot two missing bits in the API: composition of a function f from k to E and of a function g from E to F (where the derivative of g o f is the Fréchet derivative of g applied to the derivative of f), and multiplication of a function f from k to k with a function g from k to E, but these two can be added later when they are needed.

I leave this PR open as others might want to add more comments. Unless there are more comments, I will merge it in a few days (if you fix the broken build inbetween :)

[urkud]

Another possible addition to the API: derivatives of the inner product and of the norm and distance induced by an inner product.

[sgouezel]

In this design, f' is a term of type F. I haven't thought hard about this, but I would expect a function f' : 𝕜 → F which you then might evaluate at a point x when needed. Does this make sense, or should this only come at a later step?

has_deriv f f' x is really a pointwise statement. If you want to write down a global statement, you would rather use the function deriv f (which is the derivative of f when it exists and 0 otherwise) and an assumption differentiable f (saying that f has everywhere a derivative).

[gebner]

Another possible addition to the API: derivatives of the inner product and of the norm and distance induced by an inner product.

Another useful generalization of multiplication would be normed algebras over the base field. (Such as the complex numbers over the reals.)