[Merged by Bors] - doc(Analysis/Convex/Slope) : fix a typo, add docstrings#13929
[Merged by Bors] - doc(Analysis/Convex/Slope) : fix a typo, add docstrings#13929LorenzoLuccioli wants to merge 3 commits intomasterfrom
Conversation
PR summary 18f0eeebefImport changesNo significant changes to the import graph Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit> |
grunweg
left a comment
There was a problem hiding this comment.
Thanks for the typo fixes and removed porting notes, these changes look good!
I think the docstrings have a "mathematical typo"; can you fix them, please?
| linarith only [hf.secant_mono_aux1 hx hz hxy hyz] | ||
| #align convex_on.secant_mono_aux3 ConvexOn.secant_mono_aux3 | ||
|
|
||
| /-- If `f : 𝕜 → 𝕜` is convex, then for any point `a` the slope of the secant line of `f` through `a` |
There was a problem hiding this comment.
This is not fully accurate: f is convex on s, and a and x are points in s. Can you rephrase this doc-string accordingly, please?
There was a problem hiding this comment.
Thank you for your comment.
Actually I had the same doubt, but I decided to write it like this in order to mimic the style of the other doc-strings in the same file. I thought that the fact that everything happens in s had been left implicit on purpose, so that the docs are easier to read.
What do you think is better: leave everything like it is, modify only the 3 new doc-strings or modify all the doc-strings in the file?
There was a problem hiding this comment.
Good point! I had not noticed this fact about the other doc-strings. I have asked on zulip now.
There was a problem hiding this comment.
I'm personally happy with this small lie.
maintainer merge
| linarith only [hf.secant_strict_mono_aux1 hx hz hxy hyz] | ||
| #align strict_convex_on.secant_strict_mono_aux3 StrictConvexOn.secant_strict_mono_aux3 | ||
|
|
||
| /-- If `f : 𝕜 → 𝕜` is strictly convex, then for any point `a` the slope of the secant line of `f` |
There was a problem hiding this comment.
Similarly here, f is strictly convex on s, not globally.
| · exact hf.secant_strict_mono_aux2 ha hy hxa hxy | ||
| #align strict_convex_on.secant_strict_mono StrictConvexOn.secant_strict_mono | ||
|
|
||
| /-- If `f : 𝕜 → 𝕜` is strictly concave, then for any point `a` the slope of the secant line of `f` |
There was a problem hiding this comment.
Similarly here, f is strictly convace on s, not globally.
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
- Fix a typo in the docstrings (`[x, z]` instead of `[y, z]`). Happens multiple times in the file. - Add docstrings for `ConvexOn.secant_mono`, `StrictConvexOn.secant_strict_mono` and `StrictConcaveOn.secant_strict_mono`. - Remove a `show` tactic. It was added during the porting, but it seems that it is no longer needed. Happens twice.
|
Pull request successfully merged into master. Build succeeded: |
- Fix a typo in the docstrings (`[x, z]` instead of `[y, z]`). Happens multiple times in the file. - Add docstrings for `ConvexOn.secant_mono`, `StrictConvexOn.secant_strict_mono` and `StrictConcaveOn.secant_strict_mono`. - Remove a `show` tactic. It was added during the porting, but it seems that it is no longer needed. Happens twice.
- Fix a typo in the docstrings (`[x, z]` instead of `[y, z]`). Happens multiple times in the file. - Add docstrings for `ConvexOn.secant_mono`, `StrictConvexOn.secant_strict_mono` and `StrictConcaveOn.secant_strict_mono`. - Remove a `show` tactic. It was added during the porting, but it seems that it is no longer needed. Happens twice.
- Fix a typo in the docstrings (`[x, z]` instead of `[y, z]`). Happens multiple times in the file. - Add docstrings for `ConvexOn.secant_mono`, `StrictConvexOn.secant_strict_mono` and `StrictConcaveOn.secant_strict_mono`. - Remove a `show` tactic. It was added during the porting, but it seems that it is no longer needed. Happens twice.
[x, z]instead of[y, z]). Happens multiple times in the file.ConvexOn.secant_mono,StrictConvexOn.secant_strict_monoandStrictConcaveOn.secant_strict_mono.showtactic. It was added during the porting, but it seems that it is no longer needed. Happens twice.