fderiv subgradient connection, sumrule 1 fderiv

[ISIPINK]

Builds on PR #251, ISIPINK/LML branch Subgradient

Showed that for convex functions fderiv is a subgradient, also showed sum rule for convex + convex and fderiv

[RemyDegenne]

Thanks for the PRs! I'll review this one (and close the two previous smaller PRs) because it gives a good picture of how the new definitions relate to each other and how they relate to the existing library.

1. I don't understand why you use E →+ F for subgradients and for the argument of the Bregman divergence. It introduces coercions everywhere when you link it to fderiv. Also it looks like your version is too general and lost some desirable properties: for example eq_of_mem_subdifferential is uniqueness over the continuous linear maps, but does not give you ∂[V, x] f = {↑g}. I don't see a setting in which we would want to work with something that is not at least a linear map. I suggest you change it to a continuous linear map, to link better with fderiv.
2. You phrase things in terms of membership of the subdifferential set (..._mem_subdifferential), but the Mathlib way is to use a predicate: you should formulate your hypotheses and results with IsSubgradient instead of ∈ ∂[V, y] f.
3. I think the code would be cleaner if you dropped y ∈ V from the IsSubgradient definition. Also you could take inspiration from Mathlib and have a version within a set (like HasFDerivWithinAt) and a global version (like HasFDerivAt).
4. I think the unexpanders are not needed as some are already automatically generated? Not sure I checked properly.

[ISIPINK]

Thank you for the review.

1. I updated to continuous maps as suggested because coercion is annoying. Thought that the coercion would not be an issue and additive maps are more general. Now there is topology in pure algebra section but it is acceptable I think. I added ∂[V, x] (f) = {g} lemma which require existence of the subgradient which I get by assuming convexity.
2. I liked the notation before better, think now I cant use ∂[V, x] (f) for the lemmas .
3. Really good suggestions. Now it reads "f" has subgradient "g" within "s" at "y".
4. No unexpanders needed.

[RemyDegenne]

I pushed some changes directly to the branch. You can review them, reverse and discuss what you don't like. If you are happy with them, I think we can now merge the PR (I'm waiting for your confirmation to push the button).
Here are the main changes:

• move the files to folders that correspond to the Mathlib folders
• remove the namespace Analysis.Convex, which is not a Mathlib namespace. I placed the new definitions at the root, because other derivative deinitions are there.
• minimize the imports of the files
• make the ring explicit in the subdifferential definition and notation (it could not be inferred)
• change the way the hypotheses of convexity lemmas are written to reflect how Mathlib does it
• change some names
• add convex_subdifferentialWithin
• add HasFDerivWithinAt.hasSubgradientWithinAt which generalizes HasFDerivAt.hasSubgradientWithinAt
• generalize the Real section of the deriv file to generic F

[ISIPINK]

Looks ok to me. We can probably add full support of HasFDerivWithinAt later and then derive HasFDerivAt as special cases.