feat(analysis/calculus/fderiv): define has_strict_fderiv_at

[urkud]

Prove strict differentiability of all functions found in this file, cleanup.

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 the tactic doc entries
  • write an example of use of the new feature in test/tactics.lean or another test file
• 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

[gebner]

With this PR, we now have four notions of differentiability (not counting the single-variable specializations), and we don't even have has_strict_fderiv_within and has_strict_fderiv_filter yet.

Would it make sense to change has_fderiv_* to use strict differentiability instead?

[urkud]

has_strict_fderiv_at is mostly useful for the inverse function theorem, so I don't think that it makes sense to introduce _within and _filter variants. It is introduced in fderiv.lean because it is stronger than has_fderiv_at, so we can prove, e.g., prove strong differentiability of bilinear forms, then deduce has_fderiv_at instead of proving has_fderiv_at in fderiv.lean, then proving a stronger statement in inverse.lean.

There are has_fderiv_* differentiable functions that are not strictly differentiable, and I'd prefer to have theorems that don't need has_strict_fderiv_at to be stated in full generality.

[urkud]

The first commit moves code around. Important changes are in the next two commits.

[sgouezel]

Looks very good to me, cleaning up existing code and adding the strict differentiability which is useful for the local inverse theorem. I agree that the main player should remain the usual differentiability, so the content of the PR is fine with me. I just have a few minor comments in the code.

One more general comment though: often, when you clean up proofs, you tend to remove calc blocks and replace them by shorter strings of rewrites or applies. I don't think we should always favor conciseness above clarity: longer but easier to read proofs are sometimes preferable...

[urkud]

@sgouezel Which calc proof are you talking about? It's OK with me to reverse any diff hunk if you think it reduces readability.

[sgouezel]

I am not asking you to revert anything here, it is just a general remark to keep in the back of your mind. For instance, the proof of differentiability of bilinear maps has become harder to read, I think (but the new version is shorter and you prove a stronger result!)

[urkud]

I'll add some comments (and possibly some suffices and/or have) to this proof in inverse_function branch. I had to rewrite this proof to get a stronger result, and moved from explicit estimates to some is_O magic.