[Merged by Bors] - feat: Lemma for fderiv of scalar function
#14502
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…alar is multiplication of deriv
github-actions
bot
added
the
new-contributor
This comment was marked as outdated.
This comment was marked as outdated.
|
Thanks for your contribution to mathlib! I guess you'd like code to be reviewed - hence I have labelled it |
eric-wieser
changed the title
fderiv of scalar functionfderiv of scalar function
fpvandoorn
reviewed
Jul 13, 2024
fpvandoorn
added
the
awaiting-author
|
This lemma looks good to me. I would like a different name though (we want to avoid primes, and also the other two names are not great). |
|
Actually, can you add a version for |
|
|
adomasbaliuka
removed
the
awaiting-author
|
Thanks! bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jul 14, 2024
Adds lemma for simplifying the Fréchet derivative when applied to a function maping scalars to scalars. This (currently named `fderiv_deriv'`) is a special case of `fderiv_deriv`. Neither of `simp`, `fun_prop`, `aesop`, `exact?` , `apply?` currently seems to make progress on it. Possibly, it should be instead stated as `(fderiv 𝕜 f x : 𝕜 → 𝕜) = ((deriv f x) * ·)` if that makes it more likely to be applied by `simp`? I think it should be marked `@[simp]` because one would basically always prefer the right hand side to the left hand side of the equality. Does that make sense? I also think `fderiv_deriv` should be marked `@[simp]`, though maybe there is a reason why it isn't. Marking it such requires a change to the proof of `deriv_fderiv`, which was using a `simp` rather than a `simp only` (not a [non-terminal simp](https://leanprover-community.github.io/glossary.html#non-terminal-simp) but still to be avoided, I would assume?). Maybe other things are also likely to break, however, if those are added to simp?
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
fderiv of scalar functionfderiv of scalar function
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Adds lemma for simplifying the Fréchet derivative when applied to a function maping scalars to scalars.
This (currently named
fderiv_deriv') is a special case offderiv_deriv. Neither ofsimp,fun_prop,aesop,exact?,apply?currently seems to make progress on it.Possibly, it should be instead stated as
(fderiv 𝕜 f x : 𝕜 → 𝕜) = ((deriv f x) * ·)if that makes it more likely to be applied bysimp?I think it should be marked
@[simp]because one would basically always prefer the right hand side to the left hand side of the equality. Does that make sense?I also think
fderiv_derivshould be marked@[simp], though maybe there is a reason why it isn't. Marking it such requires a change to the proof ofderiv_fderiv, which was using asimprather than asimp only(not a non-terminal simp but still to be avoided, I would assume?). Maybe other things are also likely to break, however, if those are added to simp?